Run.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Api.Gz
2import ZlibF.Spec.Api.Compress
3
4/-!
5# API model: operations and runs
6
7One datatype of operations per stream family, with the model relation that dispatches to the
8single-function relations, and the notion of a *run*: a sequence of calls in which the caller
9re-presents the input that was not consumed (`A-stream-progress`). The goals quantify over runs,
10so they hold for every chunking of the input and of the output room.
11-/
12
13namespace ZlibF.Spec.Api
14
15open ZlibF.Spec
16
17/-! ## Inflate operations -/
18
19/-- The operations on an initialised inflate stream. -/
20inductive InflOp where
21  | inflate (c : InflCall)
22  | reset
23  | reset2 (wb : Int)
24  | prime (bits value : Int)
25  | setDictionary (d : List UInt8)
26  | getDictionary
27  | sync (inp : List UInt8)
28  | syncPoint
29  | mark
30  | getHeader (req : HdrReq)
31  | undermine (subvert : Int)
32  | validate (check : Int)
33
34/-- What an inflate operation returns. `consumed` is for `inflate` and `sync`. -/
35structure InflRes where
36  rc : Int := 0
37  out : InflOut := ⟨0, [], 0⟩
38  buf : List UInt8 := []
39  consumed : Nat := 0
40
41/-- The model of an inflate operation: the operation, what it returned, the state after. -/
42def InflModel (st : InflState) : InflOp → InflRes → InflState → Prop
43  | .inflate c, r, st' => InflStep st c r.out st' ∧ r.rc = r.out.rc
44  | .reset, r, st' => InflReset st r.rc st'
45  | .reset2 wb, r, st' => InflReset2 st wb r.rc st'
46  | .prime b v, r, st' => InflPrime st b v r.rc st'
47  | .setDictionary d, r, st' => InflSetDict st d r.rc st'
48  | .getDictionary, r, st' => InflGetDict st r.buf r.rc ∧ st' = st
49  | .sync inp, r, st' => InflSync st inp r.consumed r.rc st'
50  | .syncPoint, r, st' => InflSyncPoint st r.rc ∧ st' = st
51  | .mark, r, st' => InflMark st r.rc ∧ st' = st
52  | .getHeader req, r, st' => InflGetHeader st req r.rc st'
53  | .undermine s, r, st' => InflUndermine st s r.rc st'
54  | .validate c, r, st' => InflValidate st c r.rc st'
55
56/-! ## Deflate operations -/
57
58/-- The operations on an initialised deflate stream. `params` carries the input and the room the
59stream has at the time of the call. -/
60inductive DeflOp where
61  | deflate (c : DeflCall)
62  | params (level strategy : Int) (c : DeflCall)
63  | reset
64  | tune
65  | setDictionary (d : List UInt8)
66  | getDictionary
67  | prime (bits value : Int)
68  | pending
69  | setHeader (h : GzHead)
70  | bound (n : Nat)
71
72/-- What a deflate operation returns. -/
73structure DeflRes where
74  rc : Int := 0
75  out : DeflOut := ⟨0, [], 0⟩
76  buf : List UInt8 := []
77  pending : Nat := 0
78  bits : Nat := 0
79  bound : Nat := 0
80
81/-- The model of a deflate operation. -/
82def DeflModel (st : DeflState) : DeflOp → DeflRes → DeflState → Prop
83  | .deflate c, r, st' => DeflStep st c r.out st' ∧ r.rc = r.out.rc
84  | .params l s c, r, st' => DeflParamsFn st l s c r.out st' ∧ r.rc = r.out.rc
85  | .reset, r, st' => DeflReset st r.rc st'
86  | .tune, r, st' => DeflTune st r.rc st'
87  | .setDictionary d, r, st' => DeflSetDict st d r.rc st'
88  | .getDictionary, r, st' => DeflGetDict st r.buf r.rc ∧ st' = st
89  | .prime b v, r, st' => DeflPrime st b v r.rc st'
90  | .pending, r, st' => DeflPending st r.pending r.bits r.rc ∧ st' = st
91  | .setHeader h, r, st' => DeflSetHeader st h r.rc st'
92  | .bound n, r, st' => DeflBound st n r.bound ∧ st' = st
93
94/-! ## Gz operations -/
95
96/-- The operations on an open gz file (not open, not close). -/
97inductive GzOp where
98  | read (len : Nat) | fread (size nitems : Nat) | getc | ungetc (c : Int) | gets (len : Int)
99  | eof | error | clearerr | rewind | seek (off whence : Int) | tell | offset | direct
100  | buffer (size : Nat) | write (s : List UInt8) | fwrite (size : Nat) (s : List UInt8)
101  | putc (c : Int) | puts (s : List UInt8) | printf (s : List UInt8)
102  | setparams (level strategy : Int) | flush (flush : Int)
103
104/-- What a gz operation returns: the integer result, the bytes read, the line of `gzgets`
105(`none` is `NULL`), the number of items of `gzfread`/`gzfwrite`. -/
106structure GzRes where
107  ret : Int := 0
108  bytes : List UInt8 := []
109  line : Option (List UInt8) := none
110  items : Nat := 0
111
112/-- The model of a gz operation. -/
113def GzModel (h : GzHandle) : GzOp → GzRes → GzHandle → Prop
114  | .read n, r, h' => GzReadFn h n r.bytes r.ret h'
115  | .fread s n, r, h' => GzFread h s n r.bytes r.items h'
116  | .getc, r, h' => GzGetc h r.ret h'
117  | .ungetc c, r, h' => GzUngetc h c r.ret h'
118  | .gets n, r, h' => GzGets h n r.line h'
119  | .eof, r, h' => GzEof h r.ret ∧ h' = h
120  | .error, r, h' => GzError h r.ret ∧ h' = h
121  | .clearerr, _, h' => GzClearerr h h'
122  | .rewind, r, h' => GzRewind h r.ret h'
123  | .seek o w, r, h' => GzSeek h o w r.ret h'
124  | .tell, r, h' => GzTell h r.ret ∧ h' = h
125  | .offset, r, h' => GzOffset h r.ret ∧ h' = h
126  | .direct, r, h' => GzDirect h r.ret h'
127  | .buffer n, r, h' => GzBuffer h n r.ret h'
128  | .write s, r, h' => GzWrite h s r.ret h'
129  | .fwrite n s, r, h' => GzFwrite h n s r.items h'
130  | .putc c, r, h' => GzPutc h c r.ret h'
131  | .puts s, r, h' => GzPuts h s r.ret h'
132  | .printf s, r, h' => GzPrintf h s r.ret h'
133  | .setparams l s, r, h' => GzSetParams h l s r.ret h'
134  | .flush f, r, h' => GzFlush h f r.ret h'
135
136/-! ## Traces -/
137
138/-- A trace of inflate over the stream `Z`: `inflate` calls whose input is a prefix of the part of
139`Z` that is not consumed yet (the caller re-presents unconsumed input, whatever its chunking,
140whatever the room), and `setDictionary` calls with the dictionary `d0`. Each step is allowed by
141the model. -/
142inductive InflTrace (Z d0 : List UInt8) : InflState → InflState → Prop
143  | nil {s : InflState} : InflTrace Z d0 s s
144  | step {s s' s'' : InflState} {c : InflCall} {r : InflRes} :
145      c.inp <+: Z.drop s.seen.length → InflModel s (.inflate c) r s' → InflTrace Z d0 s' s'' →
146      InflTrace Z d0 s s''
147  | dict {s s' s'' : InflState} {r : InflRes} :
148      InflModel s (.setDictionary d0) r s' → InflTrace Z d0 s' s'' → InflTrace Z d0 s s''
149
150/-- A trace of deflate over the input `X`: `deflate` calls whose input is a prefix of the part of `X`
151not accepted yet, and `setDictionary`, `setHeader` calls (which `zlib.h` allows at the start). -/
152inductive DeflTrace (X : List UInt8) : DeflState → DeflState → Prop
153  | nil {s : DeflState} : DeflTrace X s s
154  | step {s s' s'' : DeflState} {c : DeflCall} {r : DeflRes} :
155      c.inp <+: X.drop s.input.length → DeflModel s (.deflate c) r s' → DeflTrace X s' s'' →
156      DeflTrace X s s''
157  | dict {s s' s'' : DeflState} {d : List UInt8} {r : DeflRes} :
158      DeflModel s (.setDictionary d) r s' → DeflTrace X s' s'' → DeflTrace X s s''
159  | header {s s' s'' : DeflState} {h : GzHead} {r : DeflRes} :
160      DeflModel s (.setHeader h) r s' → DeflTrace X s' s'' → DeflTrace X s s''
161
162end ZlibF.Spec.Api