Examples.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Api.Goals
2import ZlibF.Spec.Format.Examples
3import ZlibF.Proof.Format.Api
4import ZlibF.Proof.Api.InflateCausality
5
6/-!
7# API model: examples and non-vacuity
8
9Computable definitions are checked by `decide`/`rfl` on small cases. Then a tiny deflate-then-inflate
10is run through the model itself: the specification of `deflate` and of `inflate` is satisfied by
11a concrete run (so neither is contradictory), and the output of the first is accepted by the
12second. The example stream is the zlib stream of "a" of `Format/Examples.lean`.
13-/
14
15namespace ZlibF.Spec.Api
16
17open ZlibF.Spec
18
19set_option maxRecDepth 100000
20
21local macro "dk" : term => `(by decide +kernel)
22
23/-! ## Parameters (computable) -/
24
25example : inflWbits 15 = some (.zlib, 15) := by decide
26example : inflWbits 0 = some (.zlib, 0) := by decide
27example : inflWbits 31 = some (.gzip, 15) := by decide
28example : inflWbits 16 = some (.gzip, 0) := by decide
29example : inflWbits 47 = some (.auto, 15) := by decide
30example : inflWbits (-15) = some (.raw, 15) := by decide
31example : inflWbits (-8) = some (.raw, 8) := by decide
32example : inflWbits 7 = none := by decide
33example : inflWbits 48 = none := by decide
34example : inflWbits (-7) = none := by decide
35example : inflWbits (-16) = none := by decide
36example : inflWbits 16 ≠ inflWbits 0 := by decide
37
38example : deflInit? (-1) 8 15 8 0 = some ⟨6, .zlib, 15, 8, 0⟩ := by decide
39example : deflInit? 9 8 31 9 4 = some ⟨9, .gzip, 15, 9, 4⟩ := by decide
40example : deflInit? 6 8 (-15) 8 0 = some ⟨6, .raw, 15, 8, 0⟩ := by decide
41example : deflInit? 6 8 8 8 0 = some ⟨6, .zlib, 9, 8, 0⟩ := by decide
42example : deflInit? 6 8 (-8) 8 0 = none := by decide     -- raw with 8 bits is refused
43example : deflInit? 6 8 24 8 0 = none := by decide        -- gzip with 8 bits is refused
44example : deflInit? 10 8 15 8 0 = none := by decide
45example : deflInit? 6 8 15 0 0 = none := by decide
46example : deflInit? 6 8 15 8 5 = none := by decide
47example : deflInit? 6 9 15 8 0 = none := by decide
48example : deflInit? 6 8 0 8 0 = none := by decide
49
50example : compressBound 0 = 13 := by decide
51example : compressBound 4096 = 4096 + 1 + 0 + 0 + 13 := by decide
52example : compressBound (2 ^ 64 - 1) = 2 ^ 64 - 1 := by decide
53
54/-- With the parameters of `compress2` the bound of `deflateBound` is the bound of `compressBound`
55(`compress.c`: "if the default memLevel or windowBits for deflateInit() is changed, then this
56function needs to be updated"). -/
57theorem bound_default (n : Nat) (h : n < 2 ^ 60) :
58    (DeflState.fresh ⟨6, .zlib, 15, 8, 0⟩).bound n = compressBound n := by
59  unfold DeflState.bound compressBound DeflState.fresh DeflState.dictEff
60  simp only [Option.getD_none]
61  have : ¬ (n + n / 2 ^ 12 + n / 2 ^ 14 + n / 2 ^ 25 + 13 ≥ 2 ^ 64) := by omega
62  simp [this]
63
64example : (DeflState.fresh ⟨6, .gzip, 15, 8, 0⟩).bound 0 = 13 + 12 := by decide
65example : (DeflState.fresh ⟨6, .raw, 15, 8, 0⟩).bound 0 = 7 := by decide
66example : (DeflState.fresh ⟨6, .zlib, 9, 8, 0⟩).bound 0 = 4 + 6 := by decide
67example : (DeflState.fresh ⟨6, .zlib, 15, 1, 0⟩).bound 100 = 100 + 3 + 0 + 0 + 7 + 6 := by decide
68
69example : syncSearch 0 [1, 0, 0, 255, 255, 7] = (4, 5) := by decide
70example : syncSearch 0 [0, 0, 255] = (3, 3) := by decide
71example : syncSearch 3 [255, 9] = (4, 1) := by decide
72example : syncSearch 0 [0, 0, 0, 255, 255] = (4, 5) := by decide
73example : (syncSearch 0 [1, 2, 3]).1 = 0 := by decide
74
75example : gzMode? "rb".toList = some (.read, -1, 0, 1) → False := by decide
76example : gzMode? "rb".toList = some (.read, -1, 0, 0) := by decide
77example : gzMode? "wb9".toList = some (.write, 9, 0, 0) := by decide
78example : gzMode? "ab6h".toList = some (.append, 6, 2, 0) := by decide
79example : gzMode? "wT".toList = some (.write, -1, 0, 1) := by decide
80example : gzMode? "rb+".toList = none := by decide
81example : gzMode? "b".toList = none := by decide
82example : gzMode? "rT".toList = none := by decide
83example : gzMode? "wG".toList = none := by decide
84
85example : syncStep 0 0 = 1 ∧ syncStep 2 255 = 3 ∧ syncStep 2 7 = 0 ∧ syncStep 3 0 = 1 := by decide
86
87/-! ## The example stream and a model run of inflate -/
88
89/-- zlib's stream for "a" (`Format/Examples.lean`). -/
90def zA : List UInt8 := [0x78, 0x9C, 0x4b, 0x04, 0x00, 0x00, 0x62, 0x00, 0x62]
91
92theorem zA_decodes : Zlib.Decodes [] zA [0x61] :=
93  ⟨0x78, 0x9C, [], _, rfl, dk, fun _ => ⟨rfl, _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩,
94    fun h => absurd h dk⟩
95
96theorem zA_layer : Layer.Decodes .zlib 15 [] zA [0x61] :=
97  ⟨zA_decodes, Or.inr ⟨0x78, rfl, by decide⟩⟩
98
99theorem zA_not_needDict : ¬ HdrNeedsDict .zlib 15 zA := by
100  rintro ⟨_, cmf, flg, r, h, _, hb, _⟩
101  have h2 : flg = 0x9C := by simp [zA] at h; exact h.2.1.symm
102  subst h2
103  exact absurd hb dk
104
105theorem zA_not_detectable : ¬ Layer.Detectable .zlib 15 [] zA := by
106  rintro ⟨m, hm, hv⟩
107  have h1 : m ≤ 1 := by simp [detectLag, zA] at hm; omega
108  exact hv (Or.inl (by simp [hdrLag, List.length_take]; omega))
109
110/-- Everything inflate does with the whole stream in one call: one `Z_FINISH` call with room 10. -/
111def stDoneA : InflState :=
112  { (InflState.fresh .zlib 15) with
113    phase := .done, seen := zA, out := [0x61], totalIn := 9, totalOut := 1, adler := adler32 [0x61] }
114
115theorem infl_one_call :
116    InflStep (InflState.fresh .zlib 15) ⟨zA, 10, .finish, false⟩ ⟨9, [0x61], Z.streamEnd⟩ stDoneA := by
117  refine ⟨fun h => absurd h (by decide), fun _ => ?_⟩
118  show InflRun _ _ _ _
119  left
120  unfold InflRunOk
121  and_intros
122  all_goals first
123    | rfl
124    | decide
125    | (intro h; exact absurd h (by decide))
126    | (intro _ h; exact absurd h (by decide))
127    | (intro _ _; exact zA_layer)
128    | (intro _ _ _ _ _; rfl)
129    | (intro _ _ _ hD _; exact absurd hD (by simpa [InflState.dictEff, InflState.fresh] using zA_not_detectable))
130    | (intro _ _ _ hN; exact absurd hN (by simpa [InflState.fresh] using zA_not_needDict))
131    | (intro _ _ _; rfl)
132    | (intro req h; simp [InflState.fresh] at h)
133
134theorem not_zlib_short (d x o : List UInt8) (h : x.length < 2) : ¬ Zlib.Decodes d x o := by
135  rintro ⟨cmf, flg, pre, s, hs, _⟩
136  simp [hs] at h
137  omega
138
139theorem not_decodes_short (d x o : List UInt8) (b : Nat) (h : x.length < 2) :
140    ¬ Layer.Decodes .zlib b d x o := by
141  rintro ⟨⟨cmf, flg, pre, s, hs, _⟩, _⟩
142  simp [hs] at h
143  omega
144
145/-- Closes the side conditions of `InflRun` for the concrete steps below. -/
146local macro "close_infl" : tactic =>
147  `(tactic| (and_intros; all_goals first
148      | rfl
149      | decide
150      | (intro h; exact absurd h (by decide))
151      | (intro _ h; exact absurd h (by decide))
152      | (intro _ _; exact zA_layer)
153      | (intro _ _ _ _ _; rfl)
154      | (intro _ _ _ hD _; exact absurd hD zA_not_detectable)
155      | (intro _ _ _ hN; exact absurd hN zA_not_needDict)
156      | (intro _ _ h; exact absurd h (by decide))
157      | (intro _ _ _; rfl)
158      | (intro req h; cases h <;> fail)
159      | (intro _; exact ⟨Or.inl (by decide), by decide, rfl⟩)
160      | (intro _ _; exact Proofs.output_evidence_nil (Or.inl (by decide)) zA_layer _)
161      | (intro _ _ _ _ _ _ _ _; exact List.nil_prefix)
162      | (intro _ _ _ _ ⟨n, o', h1, h2, h3, _⟩; exact absurd h3 (not_decodes_short _ _ _ _ (Nat.lt_of_le_of_lt (List.length_take_le' _ _) (by simp [InflState.fresh]))))
163      | (intro _ _ _ ⟨m, hm, _⟩ _; exact absurd hm (by simp [detectLag, InflState.fresh] <;> omega))
164      | (intro _ _ h; rcases h with h | h; exact absurd rfl h; exact absurd h (by decide))))
165
166/-- Two calls with the same stream cut after the first byte: the first call only reads the byte of
167the header that it gets, with `Z_OK`. -/
168def stHalfA : InflState :=
169  { (InflState.fresh .zlib 15) with seen := [0x78], totalIn := 1 }
170
171theorem infl_step1 :
172    InflStep (InflState.fresh .zlib 15) ⟨[0x78], 10, .noFlush, false⟩ ⟨1, [], Z.ok⟩ stHalfA := by
173  refine ⟨fun h => absurd h (by decide), fun _ => ?_⟩
174  show InflRun _ _ _ _
175  left
176  unfold InflRunOk
177  close_infl
178
179theorem infl_step2 :
180    InflStep stHalfA ⟨zA.drop 1, 10, .finish, false⟩ ⟨8, [0x61], Z.streamEnd⟩ stDoneA := by
181  refine ⟨fun h => absurd h (by decide), fun _ => ?_⟩
182  show InflRun _ _ _ _
183  left
184  unfold InflRunOk
185  close_infl
186
187/-- A run of `inflate` over `zA` cut in two calls reaches the end of the stream with the
188decoded data. -/
189theorem infl_trace : InflTrace zA [] (InflStart .zlib 15 []) stDoneA :=
190  .step (c := ⟨[0x78], 10, .noFlush, false⟩) (r := { rc := Z.ok, out := ⟨1, [], Z.ok⟩ })
191    (by decide) ⟨infl_step1, rfl⟩
192    (.step (c := ⟨zA.drop 1, 10, .finish, false⟩) (r := { rc := Z.streamEnd, out := ⟨8, [0x61], Z.streamEnd⟩ })
193      (by decide) ⟨infl_step2, rfl⟩ .nil)
194
195/-! ## A model run of deflate -/
196
197/-- The parameters of `compress2` at level 6. -/
198def dP : DeflParams := ⟨6, .zlib, 15, 8, 0⟩
199
200theorem zA_valid : (DeflState.fresh dP).Valid zA [0x61] :=
201  ⟨zA_decodes, by decide, 0x78, 0x9C, _, rfl, by decide⟩
202
203/-- The state after one `Z_FINISH` call with the byte "a" and room 20 that delivers `zA`. -/
204def dDoneA : DeflState :=
205  { (DeflState.fresh dP) with
206    input := [0x61], produced := zA, totalIn := 1, totalOut := 9, adler := adler32 [0x61],
207    last := 4, finishing := true, done := true, started := true }
208
209theorem defl_one_call :
210    DeflStep (DeflState.fresh dP) ⟨[0x61], 20, .finish, false⟩ ⟨1, zA, Z.streamEnd⟩ dDoneA := by
211  refine ⟨fun h => absurd h (by decide), fun _ h => absurd h (by decide),
212    fun _ _ _ h => absurd h (by decide), fun _ _ _ _ => ?_⟩
213  unfold DeflRun DeflFrame
214  and_intros
215  all_goals first
216    | rfl
217    | decide
218    | (intro h; exact absurd h (by decide))
219    | (intro h; exact absurd h.2.1 (by decide))
220    | (intro _; refine ⟨rfl, fun v h => ?_⟩; exact (Option.some.inj h).symm)
221    | (intro _; exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, fun _ => zA_valid, fun _ h => absurd h (by decide), fun _ => by decide⟩)
222    | (intro _ _ _ _ _ _; rfl)
223    | (intro _ _ h; exact absurd h (by decide))
224    | (intro _ _; exact absurd ‹_› (by decide))
225    | (intro _ _ _; exact absurd ‹_› (by decide))
226
227/-- Deflate then inflate, through the model: the data of the example goes through both. -/
228theorem roundtrip_example :
229    DeflTrace [0x61] (DeflState.fresh dP) dDoneA ∧ InflTrace zA [] (InflStart .zlib 15 []) stDoneA ∧
230    dDoneA.produced = zA ∧ stDoneA.out = [0x61] :=
231  ⟨.step (c := ⟨[0x61], 20, .finish, false⟩) (r := { rc := Z.streamEnd, out := ⟨1, zA, Z.streamEnd⟩ })
232      (by decide) ⟨defl_one_call, rfl⟩ .nil,
233    infl_trace, rfl, rfl⟩
234
235/-- Non-vacuity of `Goal.roundtrip`'s hypotheses: this deflate trace is one the goal talks
236about, and the inflate trace is one of its runs. -/
237example : DeflCfg dP ∧ Compatible dP .zlib 15 ∧ dDoneA.done = true ∧ dDoneA.precise = true ∧
238    dDoneA.input = [0x61] ∧ dDoneA.dictEff = [] :=
239  ⟨⟨6, 8, 15, 8, 0, by decide⟩, ⟨⟨15, by decide⟩, rfl, Or.inr (Or.inl ⟨rfl, Or.inl rfl⟩)⟩, rfl, rfl, rfl, rfl⟩
240
241/-- The hypotheses of `Goal.inflate_decodes` and `Goal.inflate_completes` are satisfiable. -/
242example : InflCfg .zlib 15 ∧ Layer.Decodes .zlib 15 [] zA [0x61] ∧ FullWindow .zlib 15 zA ∧
243    ¬ HdrNeedsDict .zlib 15 zA ∧ InflTrace zA [] (InflStart .zlib 15 []) stHalfA :=
244  ⟨⟨15, by decide⟩, zA_layer, Or.inl rfl, zA_not_needDict,
245    .step (c := ⟨[0x78], 10, .noFlush, false⟩) (r := { rc := Z.ok, out := ⟨1, [], Z.ok⟩ })
246      (by decide) ⟨infl_step1, rfl⟩ .nil⟩
247
248/-- Two states of the `Goal.inflate_completes` shape: from `stHalfA` the call with the rest ends the
249stream (this is `infl_step2`, seen as the conclusion of the goal). -/
250example : (⟨zA.drop 1, 10, .finish, false⟩ : InflCall).inp = zA.drop stHalfA.seen.length ∧
251    zA_layer = zA_layer ∧ [0x61].length ≤ stHalfA.out.length + 10 := ⟨rfl, rfl, by decide⟩
252
253/-! ## `compress2` and `uncompress2` -/
254
255example : compressParams 6 = some dP := by decide
256example : compressParams (-1) = some dP := by decide
257example : compressParams 10 = none := by decide
258
259theorem compress2_example : Compress2 true 6 [0x61] 100 Z.ok zA :=
260  Or.inr (Or.inl ⟨rfl, zA_valid, by decide, by decide⟩)
261
262/-- A level outside -1 to 9: nothing is written. -/
263example : Compress2 true 10 [0x61] 100 Z.streamError [] := ⟨rfl, rfl⟩
264/-- A null argument. -/
265example : Compress2 false 6 [0x61] 100 Z.streamError [] := ⟨rfl, rfl⟩
266/-- A destination of `compressBound` bytes is enough: the same call with the room at the bound
267still succeeds. -/
268example : Compress2 true 6 [0x61] (compressBound 1) Z.ok zA :=
269  Or.inr (Or.inl ⟨rfl, zA_valid, by decide, by decide⟩)
270
271/-- The room is one byte: only the first byte of a stream fits. -/
272example : Compress2 true 6 [0x61] 1 Z.bufError [0x78] :=
273  Or.inr (Or.inr ⟨rfl, rfl, by decide, zA, zA_valid, by decide⟩)
274
275/-- `uncompress2` on an empty source: `Z_DATA_ERROR` and nothing is written. -/
276example : Uncompress2 true [] 10 Z.dataError [] 0 := by
277  refine ⟨by decide, by decide, Or.inr (Or.inr (Or.inl rfl)),
278    fun h => absurd h (by decide), fun h => absurd h (by decide), ?_, ?_, ?_⟩
279  · intro stream decoded _ _
280    exact List.nil_prefix
281  · exact Proofs.output_evidence_nil (allowed := fun dictionary => dictionary = []) rfl zA_layer []
282  · intro n o _ h
283    exact absurd h (not_zlib_short _ _ _ (by simp))
284
285/-- Null arguments to `uncompress2`. -/
286example : Uncompress2 false zA 10 Z.streamError [] 0 := ⟨rfl, rfl, rfl⟩
287
288/-! ## gz files -/
289
290/-- A file of two bytes is read as it is. -/
291theorem gz_direct_file : GzDecoded false [0x61, 0x62] [0x61, 0x62] Z.ok :=
292  Or.inl ⟨rfl, fun h => absurd h.1 (by decide), rfl, rfl⟩
293
294/-- Opening it for reading. -/
295def gzR : GzHandle :=
296  { mode := .read, level := -1, strategy := 0, direct := 0, raw := [0x61, 0x62], dec := [0x61, 0x62],
297    dstat := Z.ok, rpos := 0, pushed := [], past := false, err := Z.ok, written := [], out := [],
298    base := [], want := gzBufDefault, sized := false, failed := false }
299
300example : GzOpen "r".toList (some [0x61, 0x62]) (some gzR) :=
301  Or.inr ⟨[0x61, 0x62], [0x61, 0x62], Z.ok, fun _ => ⟨rfl, gz_direct_file⟩, rfl⟩
302
303example : GzOpen "r".toList none none := Or.inl rfl
304example : GzOpen "q".toList (some []) none := rfl
305example : GzOpen "r+".toList (some []) none := rfl
306
307/-- Reading one byte, then asking for more than is left: the second read comes up short and sets
308the end indicator. -/
309example : GzReadFn gzR 1 [0x61] 1 { gzR with rpos := 1, sized := true } := by
310  unfold GzReadFn GzHandle.avail
311  refine ⟨fun h => absurd rfl h, fun _ => ?_⟩
312  decide
313example : GzReadFn { gzR with rpos := 1 } 5 [0x62] 1 { gzR with rpos := 2, sized := true, past := true } := by
314  unfold GzReadFn GzHandle.avail
315  refine ⟨fun h => absurd rfl h, fun _ => ?_⟩
316  decide
317example : GzReadFn { gzR with rpos := 2 } 5 [] 0 { gzR with rpos := 2, sized := true, past := true } := by
318  unfold GzReadFn GzHandle.avail
319  refine ⟨fun h => absurd rfl h, fun _ => ?_⟩
320  decide
321
322example : GzEof { gzR with past := true } 1 := by unfold GzEof; decide
323example : GzEof gzR 0 := by unfold GzEof; decide
324example : GzTell { gzR with rpos := 1 } 1 := by unfold GzTell GzHandle.tell; decide
325example : GzDirect gzR 1 { gzR with sized := true } :=
326  ⟨Or.inl ⟨rfl, rfl, fun h => absurd h.1 (by decide), by decide⟩, rfl⟩
327
328/-- zlib's gzip member for "a" (`Format/Examples.lean`). -/
329def gzA : List UInt8 := [31, 139, 8, 0, 0, 0, 0, 0, 2, 19, 75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0]
330
331theorem gzA_decodes : Gzip.Decodes gzA [0x61] :=
332  ⟨0, [0, 0, 0, 0], 2, 19, [], [], [], [75, 4, 0, 67, 190, 183, 232, 1, 0, 0, 0], dk, dk, dk, dk, dk, dk,
333    _, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
334
335theorem gzip_empty (o : List UInt8) : ¬ Gzip.Decodes [] o := by
336  rintro ⟨flg, mtime, xfl, os, extra, name, comment, s, _, _, _, _, _, hm, _⟩
337  simp [Gzip.header] at hm
338
339/-- The file that a writer produces for "a" reads back as "a" (`C7`): the member is the whole
340file, there is nothing after it. -/
341theorem gzA_file : GzDecoded false gzA [0x61] Z.ok :=
342  Or.inr (Or.inr ⟨Or.inl ⟨by decide, by decide, by decide, by decide, by decide⟩,
343    [(gzA, [0x61])], [], by simpa using gzA_decodes, rfl,
344    fun ⟨m, o, t, h, hd⟩ => by
345      have hm : m = [] := (List.append_eq_nil_iff.mp h.symm).1
346      subst hm
347      exact gzip_empty _ hd,
348    Or.inl ⟨rfl, by simp, rfl, rfl⟩⟩)
349
350/-- A writer that wrote "a" and closes: the file is the member. -/
351def gzW : GzHandle :=
352  { gzR with mode := .write, raw := [], dec := [], written := [0x61], out := gzA }
353
354example : GzClose gzW Z.ok gzA := by
355  refine ⟨Or.inl rfl, fun h => absurd h (by decide), fun _ _ => Or.inr rfl, fun _ _ _ => ⟨fun h => absurd h (by decide), fun _ => ?_⟩⟩
356  exact ⟨gzA, by simp [gzW, gzR], List.prefix_refl _, gzA_decodes⟩
357
358/-! ## Witnesses for the repaired parts of the specification
359
360A `Z_FINISH` call that returns `Z_BUF_ERROR` (nothing is consumed, nothing is finished, `done` stays
361false), a completed `Z_FULL_FLUSH` (it sets `fullAt`), and an `inflate` call that returns
362`Z_MEM_ERROR` after reading input and writing output (the totals stay). The lemmas say that the
363clauses of the model are the ones that exclude the earlier errors. -/
364
365theorem defl_done_iff {st : DeflState} {c : DeflCall} {o : DeflOut} {st' : DeflState}
366    (h : DeflRun st c o st') : st'.done = true ↔ (st.done = true ∨ o.rc = Z.streamEnd) := by
367  obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, hd, -⟩ := h
368  exact hd
369
370/-- `done` is not set by a `Z_BUF_ERROR` (the first error of the review). -/
371theorem defl_no_done_on_buf_error {st : DeflState} {c : DeflCall} {o : DeflOut} {st' : DeflState}
372    (h : DeflRun st c o st') (hr : o.rc = Z.bufError) (hd : st.done = false) : st'.done = false := by
373  have := (defl_done_iff h).1
374  cases hd' : st'.done
375  · rfl
376  · rcases this hd' with h1 | h1
377    · simp [hd] at h1
378    · rw [hr] at h1; exact absurd h1 (by decide)
379
380/-- `fullAt` is kept by every call that does not complete a full flush. -/
381theorem defl_fullAt_kept {st : DeflState} {c : DeflCall} {o : DeflOut} {st' : DeflState}
382    (h : DeflRun st c o st')
383    (hn : ¬ (o.rc = Z.ok ∧ o.produced.length < c.availOut ∧ c.flush = .fullFlush)) :
384    st'.fullAt = st.fullAt := by
385  obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, hk, -⟩ := h
386  exact hk hn
387
388/-- A stream whose `Z_FINISH` was accepted but not finished: the output bytes `78` are out, three are pending. -/
389def dBusy : DeflState :=
390  { (DeflState.fresh dP) with
391    input := [0x61], produced := [0x78], totalIn := 1, totalOut := 1, adler := adler32 [0x61],
392    pend := 3, last := 4, finishing := true, started := true }
393
394/-- More input after `Z_FINISH`: `Z_BUF_ERROR`, nothing consumed, the stream is not finished. -/
395theorem defl_finish_buf_error :
396    DeflStep dBusy ⟨[0x62], 5, .finish, false⟩ ⟨0, [], Z.bufError⟩ dBusy := by
397  refine ⟨fun h => absurd h (by decide), fun _ h => absurd h (by decide),
398    fun _ _ _ h => absurd h (by decide), fun _ _ _ _ => ?_⟩
399  unfold DeflRun DeflFrame
400  and_intros
401  all_goals first
402    | rfl
403    | decide
404    | (intro h; exact absurd h (by decide))
405    | (intro h; exact absurd h.1 (by decide))
406    | (intro _ h; exact absurd h (by decide))
407    | (intro _ _; exact Or.inl rfl)
408    | (intro _ _; exact ⟨rfl, Or.inl rfl⟩)
409    | (intro _ _; exact absurd ‹_› (by decide))
410    | (intro _ _ h; exact absurd h (by decide))
411    | (intro _ _ _; exact absurd ‹_› (by decide))
412    | (intro h _; exact absurd h (by decide))
413    | (intro _ _ _ _ _ h; exact absurd h (by decide))
414
415/-- The stream state of that witness is not finished, and the `done` flag stays false, whatever
416the call: the repaired clause. -/
417example : dBusy.done = false := rfl
418
419/-- Raw deflate of "a" with a completed full flush: `4a 04 00` then the empty stored block `00 00 ff ff`
420(what zlib writes). Followed by `03 00` it is a valid stream of "a". -/
421def fullA : List UInt8 := [0x4a, 0x04, 0x00, 0x00, 0x00, 0xff, 0xff]
422
423theorem fullA_flushed : Deflate.Decodes [] (fullA ++ [3, 0]) [0x61] :=
424  ⟨_, .more rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl)))
425    (.more rfl rfl (.stored rfl rfl rfl rfl) (.last rfl rfl (.fixed (.eob rfl)))), dk⟩
426
427def dPraw : DeflParams := ⟨6, .raw, 15, 8, 0⟩
428
429def dFullA : DeflState :=
430  { (DeflState.fresh dPraw) with
431    input := [0x61], produced := fullA, totalIn := 1, totalOut := 7, last := 3, started := true,
432    clean := false, fullAt := some (7, 1) }
433
434/-- A completed full flush with `fullAt = none` before: the call has an allowed outcome and sets `fullAt`. -/
435theorem defl_full_flush :
436    DeflStep (DeflState.fresh dPraw) ⟨[0x61], 20, .fullFlush, false⟩ ⟨1, fullA, Z.ok⟩ dFullA := by
437  refine ⟨fun h => absurd h (by decide), fun _ h => absurd h (by decide),
438    fun _ _ _ h => absurd h (by decide), fun _ _ _ _ => ?_⟩
439  unfold DeflRun DeflFrame
440  and_intros
441  all_goals first
442    | rfl
443    | decide
444    | (intro h; exact absurd h (by decide))
445    | (intro h; exact absurd h.1 (by decide))
446    | (intro _ h; exact absurd h (by decide))
447    | (intro _; exact ⟨rfl, fun v h => by cases h⟩)
448    | (intro _ _ _; exact ⟨by decide, by decide, rfl⟩)
449    | (intro _ _ _; exact ⟨rfl, rfl⟩)
450    | (intro _ _ _; refine ⟨rfl, fun _ => ?_⟩; exact fullA_flushed)
451    | (intro _ _ _; rfl)
452    | (intro _ _ _ _ _ _; exact absurd ‹_› (by decide))
453    | (intro _ h; exact absurd h (by decide))
454    | (intro h; exact absurd ⟨rfl, by decide, rfl⟩ h)
455
456/-- The completed flush is not the old, contradictory outcome (`fullAt` kept `none`). -/
457example : dFullA.fullAt ≠ (DeflState.fresh dPraw).fullAt := by decide
458
459/-- An inflate call that reads the whole raw stream of "a" and writes the byte, then fails to allocate the
460window: `Z_MEM_ERROR`, consumed 3, produced 1, `total_in` and `total_out` still 0, state `mem`. -/
461def rawA : List UInt8 := [0x4b, 0x04, 0x00]
462
463def stMemA : InflState :=
464  { (InflState.fresh .raw 15) with phase := .mem, seen := rawA, out := [0x61] }
465
466theorem rawA_decodes : Layer.Decodes .raw 15 [] rawA [0x61] :=
467  ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
468
469theorem infl_mem_error :
470    InflStep (InflState.fresh .raw 15) ⟨rawA, 10, .noFlush, false⟩ ⟨3, [0x61], Z.memError⟩ stMemA := by
471  refine ⟨fun h => absurd h (by decide), fun _ => ?_⟩
472  show InflRun _ _ _ _
473  right
474  unfold InflRunMem
475  and_intros
476  all_goals first
477    | rfl
478    | decide
479    | (intro _; exact Proofs.output_evidence_of_decodes (Or.inr rfl)
480        (fun d hd => by simpa [InflState.PermitsDictionary, InflState.fresh] using hd) rawA_decodes)
481    | (intro _ dictionary _
482       change Layer.Determined .raw 15 dictionary rawA [0x61]
483       have ha : Layer.Decodes .raw 15 dictionary rawA [0x61] :=
484         ⟨_, .last rfl rfl (.fixed (.lit (s := 97) rfl dk (.eob rfl))), dk⟩
485       intro stream decoded comparable hd
486       rcases comparable with ⟨tail, heq⟩ | ⟨tail, heq⟩
487       · have hx := Proofs.Layer.ext ha (by simpa only [← heq] using hd)
488         simpa only [← hx.2] using (List.prefix_refl [0x61])
489       · have hx := Proofs.Layer.ext hd (by simpa only [← heq] using ha)
490         simpa only [hx.2] using (List.prefix_refl [0x61]))
491    | (intro req h; cases h)
492
493example : stMemA.totalIn = 0 ∧ stMemA.totalOut = 0 ∧ (3 : Nat) > 0 ∧ stMemA.out = [0x61] := ⟨rfl, rfl, by decide, rfl⟩
494
495/-- In the `mem` state every call returns `Z_MEM_ERROR` and changes nothing. -/
496example : InflStep stMemA ⟨[0], 10, .noFlush, false⟩ ⟨0, [], Z.memError⟩ stMemA :=
497  ⟨fun h => absurd h (by decide), fun _ => ⟨rfl, rfl, rfl, rfl⟩⟩
498
499/-! ## `gzseek` after the end of the data -/
500
501/-- A gzip file of "a", read to its end (`past`). -/
502def gzP : GzHandle :=
503  { gzR with raw := gzA, dec := [0x61], rpos := 1, past := true, sized := true }
504
505theorem gzA_looks : GzLooksGzip gzA := by unfold GzLooksGzip gzA; decide
506
507/-- `gzseek(f, 5, SEEK_CUR)` returns 6 but `gztell` stays 1 and `gzeof` stays 1: what the real library
508does (a quirk). The model allows exactly this. -/
509theorem gz_seek_quirk :
510    GzSeek gzP 5 1 6 { gzP with rpos := 6 } ∧ ({ gzP with rpos := 6 } : GzHandle).tell = 1 ∧
511      GzEof { gzP with rpos := 6 } 1 := by
512  refine ⟨?_, by unfold GzHandle.tell; decide, by unfold GzEof; decide⟩
513  unfold GzSeek
514  refine ⟨fun h => absurd h (by decide), fun _ => Or.inr ⟨by decide, fun h => absurd h (by decide), ?_⟩⟩
515  intro _
516  refine ⟨rfl, rfl, ?_, ?_⟩
517  · intro h
518    rcases h with hc | hc
519    · exact absurd gzA_looks hc.2.2.1
520    · exact absurd hc (by decide)
521  · intro _ _
522    exact ⟨rfl, rfl, by decide, by decide⟩
523
524/-- In a transparent file the same seek clears `past`, and `gztell` is the position. -/
525def gzC : GzHandle :=
526  { gzR with rpos := 2, past := true, sized := true }
527
528theorem gz_seek_copy :
529    GzSeek gzC 5 1 7 { gzC with rpos := 7, past := false } ∧
530      ({ gzC with rpos := 7, past := false } : GzHandle).tell = 7 := by
531  refine ⟨?_, by unfold GzHandle.tell; decide⟩
532  unfold GzSeek
533  have hc : gzC.CopyMode := ⟨rfl, by decide, fun h => absurd h.1 (by decide), by decide⟩
534  refine ⟨fun h => absurd h (by decide), fun _ => Or.inr ⟨by decide, fun h => absurd h (by decide), ?_⟩⟩
535  intro _
536  refine ⟨rfl, rfl, fun _ => ⟨by decide, rfl, rfl, by decide⟩, fun h => absurd hc h⟩
537
538end ZlibF.Spec.Api