Goals.lean

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

1import ZlibF.Spec.Api.Iface
2
3/-!
4# API model: the proof goals
5
6Goals about the heap-free API models, as `def ... : Prop`. Concrete implementation targets
7are in `ZlibF/Spec/Public/`. A goal is proved when a theorem listed in
8`tests/audit/theorems.txt` has exactly the registered goal as its type.
9
10*Model goals* (`Goal.format_*`, `Goal.inflate_decodes`, ..., `Goal.gz_roundtrip`) do not mention the
11heap: they say that the model of `Inflate.lean`, `Deflate.lean`, `Compress.lean`, `Gz.lean` has
12the properties `C1` to `C7` of `docs/overview.md`. Their proofs are about the model alone.
13
14*Refinement goals* (`Goal.*_refines`, `Goal.*_copy`) take a `HeapApi` (the placeholder of
15`Iface.lean`). They say that the translated C functions never fault and that every outcome is an
16outcome of the model, with `Matches` before and after. The correctness of the library is the
17composition: refinement says that the heap does what the model does; the model goals say what
18the model does.
19
20`docs/design/api-model.md` lists, for each goal, what its proof needs.
21-/
22
23namespace ZlibF.Spec.Api
24
25open ZlibF.Spec
26
27/-- The window bits and wrapper are one that `inflateInit2` / `inflateReset2` accepts. -/
28def InflCfg (w : Wrap) (b : Nat) : Prop := ∃ wb, inflWbits wb = some (w, b)
29
30/-- The parameters are one that `deflateInit2` accepts. -/
31def DeflCfg (p : DeflParams) : Prop := ∃ l m wb ml s, deflInit? l m wb ml s = some p
32
33/-- The state in which a run over a stream that needs the dictionary `d` starts: a fresh stream; a raw
34stream (which has no `Z_NEED_DICT`) is given the dictionary before the first byte, as `zlib.h`
35requires. (Without it a raw stream that uses the dictionary is rightly a data error.) -/
36def InflStart (w : Wrap) (b : Nat) (d : List UInt8) : InflState :=
37  if w = .raw then { InflState.fresh w b with dict := some d } else InflState.fresh w b
38
39/-! ## The format is deterministic and self-delimiting (needed by C1, C2, C7) -/
40
41/-- Decoding is a function: one stream has one decoding. -/
42def Goal.format_deterministic : Prop :=
43  ∀ (w : Wrap) (b : Nat) (d z o1 o2 : List UInt8),
44    Layer.Decodes w b d z o1 → Layer.Decodes w b d z o2 → o1 = o2
45
46/-- A complete stream has no complete extension: where a stream ends is determined by its bytes. -/
47def Goal.format_prefix_free : Prop :=
48  ∀ (w : Wrap) (b : Nat) (d z t o1 o2 : List UInt8),
49    Layer.Decodes w b d z o1 → Layer.Decodes w b d (z ++ t) o2 → t = []
50
51/-! ## C2, C3: inflate decodes valid streams and rejects invalid ones -/
52
53/-- `C2`. For every valid stream `z` (zlib, gzip or raw, with the dictionary `d`) decoding to `o`,
54in a configuration that accepts every format-valid stream (`FullWindow`), every run of `inflate`
55over `z` -- any way of cutting the input into calls, any room, any flush value, with or without
56`inflateSetDictionary` -- never fails, only produces a prefix of `o`, consumes only a prefix of `z`,
57and if it ends (`Z_STREAM_END`) it has produced exactly `o` from exactly `z`. -/
58def Goal.inflate_decodes : Prop :=
59  ∀ (w : Wrap) (b : Nat) (d z o : List UInt8) (s : InflState),
60    InflCfg w b → Layer.Decodes w b d z o → FullWindow w b z →
61    InflTrace z d (InflStart w b d) s →
62    s.phase ≠ .bad ∧ s.phase ≠ .syncing ∧ s.out <+: o ∧ s.seen <+: z ∧
63    (s.phase = .done → s.out = o ∧ s.seen = z)
64
65/-- `C2`, liveness. From any state of such a run in which the stream is still running, a call that
66presents all the remaining input, with room for the remaining output and a flush value
67`Z_NO_FLUSH`, `Z_SYNC_FLUSH` or `Z_FINISH`, ends the stream: `Z_STREAM_END`, the rest of `o` produced, all
68of `z` consumed; or `Z_MEM_ERROR` (the window could not be allocated, `InflRunMem`). (Streams that need a dictionary are covered by `Goal.dict_roundtrip`.) -/
69def Goal.inflate_completes : Prop :=
70  ∀ (w : Wrap) (b : Nat) (d z o : List UInt8) (s : InflState) (c : InflCall) (r : InflRes)
71    (s' : InflState),
72    InflCfg w b → Layer.Decodes w b d z o → FullWindow w b z → ¬ HdrNeedsDict w b z →
73    InflTrace z d (InflStart w b d) s → s.phase = .running →
74    c.badBuf = false → c.inp = z.drop s.seen.length → o.length ≤ s.out.length + c.availOut →
75    (c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish) →
76    InflModel s (.inflate c) r s' →
77    (r.rc = Z.streamEnd ∧ r.out.consumed = z.length - s.seen.length ∧
78      r.out.produced = o.drop s.out.length) ∨ r.rc = Z.memError
79
80/-- `C3`, inflate side. If an input has a prefix that is not viable, at least `detectLag` bytes
81before its end (`Layer.Detectable`: a corrupt stream, with the corruption not in the last bytes),
82then no run over it ends the stream, and a call that presents all the remaining input and has room
83left over answers `Z_DATA_ERROR`. -/
84def Goal.inflate_rejects_invalid : Prop :=
85  ∀ (w : Wrap) (b : Nat) (d z : List UInt8) (s : InflState),
86    InflCfg w b → Layer.Detectable w b d z → ¬ HdrNeedsDict w b z →
87    InflTrace z d (InflStart w b d) s →
88    s.phase ≠ .done ∧
89    (s.phase = .running → ∀ (c : InflCall) (r : InflRes) (s' : InflState),
90      c.badBuf = false → c.inp = z.drop s.seen.length →
91      (c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish) →
92      InflModel s (.inflate c) r s' → r.out.produced.length < c.availOut →
93      r.rc = Z.dataError ∨ r.rc = Z.memError)
94
95/-- `C3`, deflate side: whenever a run of `deflate` has delivered the whole stream
96(`Z_STREAM_END`), the output is a valid stream of the layer for exactly the input that was
97accepted (`F-deflate-valid`), for every level, strategy, `memLevel`, `windowBits`, flush schedule and
98chunking of the input. -/
99def Goal.deflate_valid : Prop :=
100  ∀ (p : DeflParams) (x : List UInt8) (s : DeflState),
101    DeflCfg p → DeflTrace x (DeflState.fresh p) s → s.done = true → s.precise = true →
102    s.Valid s.produced s.input
103
104/-- `C3`, deflate side, liveness: a `Z_FINISH` call that presents all the remaining input, with room
105for what is still owed up to `deflateBound`, delivers the whole stream. -/
106def Goal.deflate_completes : Prop :=
107  ∀ (p : DeflParams) (x : List UInt8) (s : DeflState) (c : DeflCall) (r : DeflRes) (s' : DeflState),
108    DeflCfg p → DeflTrace x (DeflState.fresh p) s → s.clean = true → s.precise = true →
109    s.finishing = false → s.done = false → c.badBuf = false → c.flush = .finish →
110    c.inp = x.drop s.input.length → 0 < c.availOut →
111    s.bound x.length ≤ s.produced.length + c.availOut →
112    DeflModel s (.deflate c) r s' → r.rc = Z.streamEnd ∧ s'.done = true ∧ s'.input = x
113
114/-- `C3`, `Z_FULL_FLUSH` (raw deflate): everything after a completed full flush is a valid
115stream by itself, for the input accepted after it. -/
116def Goal.deflate_full_flush_resync : Prop :=
117  ∀ (p : DeflParams) (x : List UInt8) (s : DeflState) (pl il : Nat),
118    DeflCfg p → p.wrap = .raw → DeflTrace x (DeflState.fresh p) s → s.done = true →
119    s.precise = true → s.dict = none → s.fullAt = some (pl, il) →
120    Deflate.Decodes [] (s.produced.drop pl) (s.input.drop il)
121
122/-! ## C1: the round trip -/
123
124/-- The inflate configuration reads what the deflate parameters write, with a full window. -/
125def Compatible (p : DeflParams) (w : Wrap) (b : Nat) : Prop :=
126  InflCfg w b ∧ b = 15 ∧
127  ((p.wrap = .raw ∧ w = .raw) ∨ (p.wrap = .zlib ∧ (w = .zlib ∨ w = .auto)) ∨
128   (p.wrap = .gzip ∧ (w = .gzip ∨ w = .auto)))
129
130/-- `C1`. Whatever the parameters, the flush schedule and the chunking of the input of `deflate`,
131whatever the chunking and the room of `inflate`: a run of `inflate` over what `deflate` delivered
132never fails, only produces a prefix of the original input, and if it ends it has produced the whole
133original input. (The dictionary, if any, is supplied.) -/
134def Goal.roundtrip : Prop :=
135  ∀ (p : DeflParams) (x : List UInt8) (sd : DeflState) (w : Wrap) (b : Nat) (si : InflState),
136    DeflCfg p → Compatible p w b →
137    DeflTrace x (DeflState.fresh p) sd → sd.done = true → sd.precise = true → sd.input = x →
138    InflTrace sd.produced sd.dictEff (InflStart w b sd.dictEff) si →
139    si.phase ≠ .bad ∧ si.out <+: x ∧ (si.phase = .done → si.out = x ∧ si.seen = sd.produced)
140
141/-- `C1`, liveness (no dictionary): from any state of such a run, a call that presents the rest of
142the stream, with room for the rest of the input, ends the stream with exactly the original input. -/
143def Goal.roundtrip_completes : Prop :=
144  ∀ (p : DeflParams) (x : List UInt8) (sd : DeflState) (w : Wrap) (b : Nat) (si : InflState)
145    (c : InflCall) (r : InflRes) (si' : InflState),
146    DeflCfg p → Compatible p w b →
147    DeflTrace x (DeflState.fresh p) sd → sd.done = true → sd.precise = true → sd.input = x →
148    sd.dictEff = [] →
149    InflTrace sd.produced [] (InflStart w b []) si → si.phase = .running →
150    c.badBuf = false → c.inp = sd.produced.drop si.seen.length →
151    x.length ≤ si.out.length + c.availOut →
152    (c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish) →
153    InflModel si (.inflate c) r si' →
154    (r.rc = Z.streamEnd ∧ r.out.produced = x.drop si.out.length) ∨ r.rc = Z.memError
155
156/-! ## C4: dictionaries and headers -/
157
158/-- `C4`, dictionary. A zlib stream that `deflate` wrote with the preset dictionary `d` (not empty)
159is accepted with `d`, is rejected with a dictionary of another Adler-32 (format level), and
160`inflateSetDictionary` of such a dictionary answers `Z_DATA_ERROR` at every point where the stream is
161waiting for its dictionary. -/
162def Goal.dict_roundtrip : Prop :=
163  ∀ (p : DeflParams) (d x : List UInt8) (sd : DeflState),
164    DeflCfg p → p.wrap = .zlib → DeflTrace x (DeflState.fresh p) sd → sd.done = true →
165    sd.precise = true → sd.input = x → sd.dict = some d → d ≠ [] →
166    Layer.Decodes .zlib 15 d sd.produced x ∧
167    (∀ d', adler32 d' ≠ adler32 d → ¬ Zlib.Decodes d' sd.produced x) ∧
168    (∀ (s : InflState) (d' : List UInt8) (rc : Int) (s' : InflState),
169      InflTrace sd.produced d (InflState.fresh .zlib 15) s → s.phase = .needDict →
170      InflSetDict s d' rc s' → adler32 d' ≠ adler32 d → rc = Z.dataError)
171
172/-- What `inflateGetHeader` stores for the header that `deflateSetHeader` was given and `deflate`
173wrote, under the buffers `req`. -/
174def expectedHdr (req : HdrReq) (p : DeflParams) (h : GzHead) : GzHdrOut :=
175  fillHeader req h.flg (h.time % 2 ^ 32) (xflOf p) (h.os % 256) (h.extra.getD []) (h.name.getD [])
176    (h.comment.getD [])
177
178/-- `C4`, header. Whatever `inflate` reads as the header of a stream that `deflate` wrote with the
179header `h` is `expectedHdr`: `deflateSetHeader` is reproduced by `inflateGetHeader`. -/
180def Goal.header_roundtrip : Prop :=
181  ∀ (p : DeflParams) (h : GzHead) (x : List UInt8) (sd : DeflState) (req : HdrReq) (g : GzHdrOut),
182    DeflCfg p → p.wrap = .gzip → h.Valid → DeflTrace x (DeflState.fresh p) sd → sd.done = true →
183    sd.precise = true → sd.hdr = some h → HeaderRead req sd.produced g → g = expectedHdr req p h
184
185/-! ## C5: bounds -/
186
187/-- `C5`, `deflateBound`. If the stream was only fed input and `Z_FINISH` (`clean`) and ended, the
188output is at most `deflateBound` of the input, whatever the input (any ratio). -/
189def Goal.deflate_bound_adequate : Prop :=
190  ∀ (p : DeflParams) (x : List UInt8) (s : DeflState),
191    DeflCfg p → DeflTrace x (DeflState.fresh p) s → s.done = true → s.clean = true →
192    s.produced.length ≤ s.bound s.input.length
193
194/-- `C5`, `compressBound`. A destination of `compressBound` bytes is enough for `compress2` at every
195level, and the output is never larger. -/
196def Goal.compress_bound_adequate : Prop :=
197  ∀ (level : Int) (src : List UInt8) (cap : Nat) (rc : Int) (dst : List UInt8),
198    compressBound src.length ≤ cap → Compress2 true level src cap rc dst →
199    rc ≠ Z.bufError ∧ dst.length ≤ compressBound src.length
200
201/-- `C1` for `compress2` and `uncompress2`: what `compress2` writes, `uncompress2` reads back, with
202a destination as large as the source. -/
203def Goal.compress_roundtrip : Prop :=
204  ∀ (level : Int) (src : List UInt8) (cap cap2 : Nat) (dst src2 : List UInt8) (used : Nat)
205    (rc2 : Int),
206    Compress2 true level src cap Z.ok dst → src.length ≤ cap2 →
207    Uncompress2 true dst cap2 rc2 src2 used →
208    (rc2 = Z.ok → src2 = src ∧ used = dst.length) ∧ (rc2 ≠ Z.ok → rc2 = Z.memError)
209
210/-! ## C7: gz files -/
211
212/-- `C7`, write then read. A file that a writer closed, with nothing failing and nothing before
213it, reads back as exactly the bytes written (`gzdirect` 0, status `Z_OK`). -/
214def Goal.gz_roundtrip : Prop :=
215  ∀ (h : GzHandle) (rc : Int) (final : List UInt8),
216    h.mode = .write → h.base = [] → h.failed = false → h.direct ≠ 1 →
217    GzClose h rc final → rc = Z.ok → GzDecoded false final h.written Z.ok
218
219/-- `C7`, seek and tell. After a successful `gzseek` of a reader, `gztell` is the position returned,
220and the next read returns the data from there. -/
221def Goal.gz_seek_read : Prop :=
222  ∀ (h h1 h2 : GzHandle) (off whence ret : Int) (n : Nat) (bytes : List UInt8) (ret2 : Int),
223    h.mode = .read → h.pushed = [] → n ≤ 2 ^ 31 - 1 →
224    (h.past = false ∨ h.CopyMode ∨ ret < h.tell) → GzSeek h off whence ret h1 → 0 ≤ ret →
225    h1.tell = ret ∧ (h1.pushed = [] → GzReadFn h1 n bytes ret2 h2 →
226      bytes = (h.dec.drop ret.toNat).take n)
227
228/-! ## Refinement goals (need the placeholder `HeapApi`) -/
229
230/-- Every inflate operation on a stream that `Matches` a model state, with its arguments in the
231heap as `zlib.h` requires: the translated function does not fault, and what it returns and
232leaves is allowed by the model (`InflModel`), with `Matches` again. -/
233def Goal.inflate_refines (A : HeapApi) : Prop :=
234  ∀ (h : A.Heap) (s : A.Strm) (st : InflState) (op : InflOp),
235    A.inflMatches h s st → A.inflArgs h s op →
236    ∀ out, A.inflRun h s op out →
237      ∃ h' r st', out = .ret h' r ∧ InflModel st op r st' ∧ A.inflMatches h' s st'
238
239/-- `inflateInit` / `inflateInit2`: no fault; the result is `InflInit`; a stream is created exactly
240when the code is `Z_OK`, otherwise `state` is null and nothing stays allocated. -/
241def Goal.inflate_init_refines (A : HeapApi) : Prop :=
242  ∀ (h : A.Heap) (s : A.Strm) (wb : Int) (vok : Bool),
243    A.inflInitArgs h s → ∀ out, A.inflInit h s wb vok out →
244      ∃ h' rc r, out = .ret h' rc ∧ InflInit wb vok rc r ∧
245        (match r with | some st => A.inflMatches h' s st | none => A.inflNoState h' s)
246
247/-- `inflateEnd`: no fault, `Z_OK`, and the stream has no state afterwards. -/
248def Goal.inflate_end_refines (A : HeapApi) : Prop :=
249  ∀ (h : A.Heap) (s : A.Strm) (st : InflState),
250    A.inflMatches h s st → ∀ out, A.inflEnd h s out →
251      ∃ h' rc, out = .ret h' rc ∧ InflEnd st rc ∧ A.inflNoState h' s
252
253/-- `inflateCopy` (`C6`): no fault; the source is unchanged; on `Z_OK` the destination is a stream
254with the same model state and its own storage (disjoint from the source). -/
255def Goal.inflate_copy_refines (A : HeapApi) : Prop :=
256  ∀ (h : A.Heap) (dst src : A.Strm) (st : InflState),
257    A.inflMatches h src st → A.inflNoState h dst → ∀ out, A.inflCopy h dst src out →
258      ∃ h' rc d, out = .ret h' rc ∧ InflCopy st rc d ∧ A.inflMatches h' src st ∧
259        (match d with | some st2 => A.inflMatches h' dst st2 ∧ A.inflDisjoint h' src dst
260                      | none => True)
261
262/-- `inflateBack`: no fault; the result is allowed by `InflBack`. -/
263def Goal.inflate_back_refines (A : HeapApi) : Prop :=
264  ∀ (h : A.Heap) (s : A.Strm) (wb : Nat) (first : List UInt8) (cb : BackCallbacks),
265    ∀ out, A.inflBack h s wb first cb out →
266      ∃ h' r, out = .ret h' r ∧ InflBack wb first cb r
267
268/-- Every deflate operation, as `Goal.inflate_refines`. -/
269def Goal.deflate_refines (A : HeapApi) : Prop :=
270  ∀ (h : A.Heap) (s : A.Strm) (st : DeflState) (op : DeflOp),
271    A.deflMatches h s st → A.deflArgs h s op →
272    ∀ out, A.deflRun h s op out →
273      ∃ h' r st', out = .ret h' r ∧ DeflModel st op r st' ∧ A.deflMatches h' s st'
274
275/-- `deflateInit` / `deflateInit2`, as `Goal.inflate_init_refines`. -/
276def Goal.deflate_init_refines (A : HeapApi) : Prop :=
277  ∀ (h : A.Heap) (s : A.Strm) (l m wb ml st : Int) (vok : Bool),
278    A.deflInitArgs h s → ∀ out, A.deflInit h s l m wb ml st vok out →
279      ∃ h' rc r, out = .ret h' rc ∧ DeflInit l m wb ml st vok rc r ∧
280        (match r with | some ds => A.deflMatches h' s ds | none => A.deflNoState h' s)
281
282/-- `deflateEnd`: no fault, `DeflEnd`, no state afterwards. -/
283def Goal.deflate_end_refines (A : HeapApi) : Prop :=
284  ∀ (h : A.Heap) (s : A.Strm) (st : DeflState),
285    A.deflMatches h s st → ∀ out, A.deflEnd h s out →
286      ∃ h' rc, out = .ret h' rc ∧ DeflEnd st rc ∧ A.deflNoState h' s
287
288/-- `deflateCopy` (`C6`), as `Goal.inflate_copy_refines`. -/
289def Goal.deflate_copy_refines (A : HeapApi) : Prop :=
290  ∀ (h : A.Heap) (dst src : A.Strm) (st : DeflState),
291    A.deflMatches h src st → A.deflNoState h dst → ∀ out, A.deflCopy h dst src out →
292      ∃ h' rc d, out = .ret h' rc ∧ DeflCopy st rc d ∧ A.deflMatches h' src st ∧
293        (match d with | some st2 => A.deflMatches h' dst st2 ∧ A.deflDisjoint h' src dst
294                      | none => True)
295
296/-- `compress2`: no fault; the result is `Compress2`. -/
297def Goal.compress2_refines (A : HeapApi) : Prop :=
298  ∀ (h : A.Heap) (ok : Bool) (level : Int) (src : List UInt8) (cap : Nat),
299    A.utilArgs h ok src cap → ∀ out, A.compress2 h ok level src cap out →
300      ∃ h' rc dst, out = .ret h' (rc, dst) ∧ Compress2 ok level src cap rc dst
301
302/-- `compress`: no fault; the result is `Compress`. -/
303def Goal.compress_refines (A : HeapApi) : Prop :=
304  ∀ (h : A.Heap) (ok : Bool) (src : List UInt8) (cap : Nat),
305    A.utilArgs h ok src cap → ∀ out, A.compress h ok src cap out →
306      ∃ h' rc dst, out = .ret h' (rc, dst) ∧ Compress ok src cap rc dst
307
308/-- `uncompress2`: no fault; the result is `Uncompress2`. -/
309def Goal.uncompress2_refines (A : HeapApi) : Prop :=
310  ∀ (h : A.Heap) (ok : Bool) (src : List UInt8) (cap : Nat),
311    A.utilArgs h ok src cap → ∀ out, A.uncompress2 h ok src cap out →
312      ∃ h' rc dst used, out = .ret h' (rc, dst, used) ∧ Uncompress2 ok src cap rc dst used
313
314/-- `uncompress`: no fault; the result is `Uncompress`. -/
315def Goal.uncompress_refines (A : HeapApi) : Prop :=
316  ∀ (h : A.Heap) (ok : Bool) (src : List UInt8) (cap : Nat),
317    A.utilArgs h ok src cap → ∀ out, A.uncompress h ok src cap out →
318      ∃ h' rc dst, out = .ret h' (rc, dst) ∧ Uncompress ok src cap rc dst
319
320/-- `gzopen` / `gzdopen`: no fault; `NULL` or a handle that `Matches` a model handle allowed by
321`GzOpen` for the content of the file. -/
322def Goal.gz_open_refines (A : HeapApi) : Prop :=
323  ∀ (h : A.Heap) (mode : List Char) (existing : Option (List UInt8)),
324    ∀ out, A.gzOpen h mode existing out →
325      ∃ h' r hd?, out = .ret h' r ∧ GzOpen mode existing hd? ∧
326        (match r, hd? with
327         | none, none => True
328         | some f, some hd => A.gzMatches h' f hd
329         | _, _ => False)
330
331/-- Every gz operation on an open file: no fault; the result is allowed by `GzModel`. -/
332def Goal.gz_refines (A : HeapApi) : Prop :=
333  ∀ (h : A.Heap) (f : A.GzFile) (hd : GzHandle) (op : GzOp),
334    A.gzMatches h f hd → A.gzArgs h f op →
335    ∀ out, A.gzRun h f op out →
336      ∃ h' r hd', out = .ret h' r ∧ GzModel hd op r hd' ∧ A.gzMatches h' f hd'
337
338/-- `gzclose`: no fault; the result and the content of the file afterwards are allowed by `GzClose`
339(`C7`: a writer's file reads back as what was written). -/
340def Goal.gz_close_refines (A : HeapApi) : Prop :=
341  ∀ (h : A.Heap) (f : A.GzFile) (hd : GzHandle),
342    A.gzMatches h f hd → ∀ out, A.gzClose h f out →
343      ∃ h' rc final, out = .ret h' (rc, final) ∧ GzClose hd rc final
344
345end ZlibF.Spec.Api