Inflate.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.Proof.Format.Api
3import ZlibF.Proof.Api.InflateCausality
4import ZlibF.Proof.Api.InflateDictionary
5
6/-!
7# Inflate model: determined output and regression proofs
8
9These theorems concern the heap-free API model. They do not assert refinement of the
10translated implementation.
11-/
12
13namespace ZlibF.Spec.Api.Proofs
14open ZlibF.Spec
15
16/-- Output from a complete stream is determined among all compatible complete streams. -/
17theorem inflate_determined_of_decodes {w : Wrap} {b : Nat} {dict x out : List UInt8}
18    (h : Layer.Decodes w b dict x out) : Layer.Determined w b dict x out := by
19  intro stream decoded comparable hd
20  rcases comparable with ⟨tail, heq⟩ | ⟨tail, heq⟩
21  · have hx := Layer.ext h (by simpa only [← heq] using hd)
22    simpa only [← hx.2] using (List.prefix_refl out)
23  · have hx := Layer.ext hd (by simpa only [← heq] using h)
24    simpa only [hx.2] using (List.prefix_refl out)
25
26/-- The empty stored raw stream used by the speculative-output regression is valid. -/
27theorem inflate_regression_raw_empty :
28    Layer.Decodes .raw 15 [] [1, 0, 0, 255, 255] [] :=
29  ⟨_, .last rfl rfl (.stored rfl rfl rfl rfl), by decide⟩
30
31/-- A running OK call cannot invent `a` without consuming input from a fresh raw stream. -/
32theorem inflate_no_input_ok_cannot_guess (after : InflState) :
33    ¬ InflRunOk (InflStart .raw 15 []) ⟨[], 1, .block, false⟩ ⟨0, [97], Z.ok⟩ after := by
34  intro h
35  rcases h with ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, hd, _⟩
36  have hp := hd ⟨rfl, rfl⟩ (Or.inl rfl) [] rfl [1, 0, 0, 255, 255] []
37    (Or.inl List.nil_prefix) inflate_regression_raw_empty
38  simp [InflStart, InflState.fresh] at hp
39
40/-- The window-allocation-failure outcome also cannot invent `a` without consuming input. -/
41theorem inflate_no_input_mem_cannot_guess (after : InflState) :
42    ¬ InflRunMem (InflStart .raw 15 []) ⟨[], 1, .block, false⟩ ⟨0, [97], Z.memError⟩ after := by
43  intro h
44  rcases h with ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, hd, _⟩
45  have hp := hd ⟨rfl, rfl⟩ [] rfl [1, 0, 0, 255, 255] []
46    (Or.inl List.nil_prefix) inflate_regression_raw_empty
47  simp [InflStart, InflState.fresh] at hp
48
49private theorem fullWindow_prefix {w : Wrap} {b : Nat} {part stream : List UInt8}
50    (hp : part <+: stream) (hw : FullWindow w b stream) : FullWindow w b part := by
51  rcases hp with ⟨tail, rfl⟩
52  cases part with
53  | nil =>
54    cases w with
55    | raw => exact hw
56    | gzip => exact hw
57    | zlib => rcases hw with h | ⟨h, _⟩ <;> simp_all [FullWindow]
58    | auto => rcases hw with h | ⟨h, _⟩ <;> simp_all [FullWindow]
59  | cons x xs => cases w <;> simpa only [FullWindow, List.cons_append, List.head?_cons] using hw
60
61private theorem needsDict_prefix {w : Wrap} {b : Nat} {part stream : List UInt8}
62    (hp : part <+: stream) (hlen : 2 ≤ part.length) (hn : HdrNeedsDict w b stream) :
63    HdrNeedsDict w b part := by
64  rcases hp with ⟨tail, heq⟩
65  cases part with
66  | nil => simp at hlen
67  | cons a rest =>
68    cases rest with
69    | nil => simp at hlen
70    | cons f rest =>
71      rcases hn with ⟨hw, cmf, flg, r, hz, hh, hb, hf⟩
72      have hhead : a = cmf ∧ f = flg := by
73        rw [← heq] at hz
74        simp only [List.cons_append, List.cons.injEq] at hz
75        exact ⟨hz.1, hz.2.1⟩
76      obtain ⟨rfl, rfl⟩ := hhead
77      refine ⟨hw, a, f, rest, rfl, hh, hb, ?_⟩
78      simpa only [ZlibFits, ← heq, List.cons_append, List.head?_cons] using hf
79
80private theorem needsDict_decoding_prefix_length {w : Wrap} {b : Nat}
81    {d part stream out : List UInt8} (hp : part <+: stream)
82    (hn : HdrNeedsDict w b stream) (hd : Layer.Decodes w b d part out) :
83    6 ≤ part.length := by
84  rcases hn with ⟨hw, cmf, flg, rest, hz, hh, hb, hf⟩
85  have hzlib (hd' : Zlib.Decodes d part out) : 6 ≤ part.length := by
86    rcases hd' with ⟨cmf', flg', pre, body, hs, hh', h0, h1⟩
87    rcases hp with ⟨tail, heq⟩
88    rw [hs, hz] at heq
89    simp only [List.cons_append, List.cons.injEq] at heq
90    obtain ⟨rfl, rfl, _⟩ := heq
91    have hpre := (h1 hb).1
92    rw [hs, hpre]
93    simp [be32]
94  rcases hw with rfl | rfl
95  · exact hzlib hd.1
96  · rcases hd with hd | hd
97    · exact hzlib hd.1
98    · obtain ⟨tail, hg⟩ := gzip_head hd
99      rcases hp with ⟨tail', heq⟩
100      rw [hg, hz] at heq
101      simp only [List.cons_append, List.cons.injEq] at heq
102      have hc : cmf = 31 := heq.1.symm
103      rw [hc] at hh
104      exact False.elim (absurd hh.1 (by decide))
105
106private theorem dict_step_fields {st after : InflState} {dictionary : List UInt8} {rc : Int}
107    (hd : InflSetDict st dictionary rc after) (hp : st.PermitsDictionary dictionary) :
108    after.wrap = st.wrap ∧ after.wbits = st.wbits ∧ after.seen = st.seen ∧
109      after.out = st.out ∧ after.precise = st.precise ∧ after.validate = st.validate ∧
110      after.PermitsDictionary dictionary ∧
111      (after.phase = .done → st.phase = .done) ∧
112      (after.phase = .bad → st.phase = .bad) ∧
113      (after.phase = .syncing → st.phase = .syncing) ∧
114      (after.dict = none → after.phase = .running → st.dict = none ∧ st.phase = .running) := by
115  cases hw : st.wrap <;> simp only [InflSetDict, hw] at hd
116  · rcases hd with ⟨_, ⟨_, rfl⟩ | ⟨_, rfl⟩⟩ <;> simp_all [InflState.PermitsDictionary]
117  all_goals
118    split at hd
119    · split at hd
120      · rcases hd with ⟨_, rfl⟩ | ⟨_, rfl⟩ <;> simp_all [InflState.PermitsDictionary]
121      · obtain ⟨_, rfl⟩ := hd
122        simp_all
123    · obtain ⟨_, rfl⟩ := hd
124      simp_all
125
126/-- A valid FDICT stream whose preset dictionary and decoded output are both empty. -/
127theorem inflate_regression_fdict_empty :
128    Layer.Decodes .zlib 15 []
129      [120, 32, 0, 0, 0, 1, 1, 0, 0, 255, 255, 0, 0, 0, 1] [] := by
130  refine ⟨?_, Or.inr ⟨120, rfl, by decide⟩⟩
131  refine ⟨120, 32, [0, 0, 0, 1], _, rfl, by decide, ?_, ?_⟩
132  · intro h; exact absurd h (by decide)
133  · intro _
134    refine ⟨by decide, _, .last rfl rfl (.stored rfl rfl rfl rfl), by decide⟩
135
136/-- Reading only a legal FDICT header cannot justify a data-error result. -/
137theorem inflate_fdict_header_cannot_fail (after : InflState) :
138    ¬ InflRunOk (InflStart .zlib 15 []) ⟨[120, 32], 10, .block, false⟩
139      ⟨2, [], Z.dataError⟩ after := by
140  intro h
141  rcases h with ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, hd, _⟩
142  have hn := hd ⟨rfl, rfl⟩ rfl (Or.inl rfl) [] (Or.inl (by decide))
143  apply hn
144  exact Or.inr ⟨[0, 0, 0, 1, 1, 0, 0, 255, 255, 0, 0, 0, 1], [], 15,
145    by simpa [InflStart, InflState.fresh] using inflate_regression_fdict_empty⟩
146
147/-- An unknown preset dictionary does not rule out a valid wrapped input prefix.
148The empty output is determined for every still-permitted dictionary. -/
149theorem inflate_unknown_dictionary_prefix {w : Wrap} {b : Nat}
150    {dictionary stream decoded : List UInt8} (hw : w ≠ .raw)
151    (hd : Layer.Decodes w b dictionary stream decoded) (n : Nat) :
152    (InflState.fresh w b).Consistent (stream.take n) [] ∧
153      (InflState.fresh w b).Determined (stream.take n) [] := by
154  constructor
155  · exact output_evidence_nil (Or.inl hw) hd (stream.take n)
156  · intro _ _ _ _ _ _
157    exact List.nil_prefix
158
159/-- Priming one low bit of minus one inserts a true bit. -/
160theorem inflate_prime_negative_low_bit :
161    InflPrime (InflState.fresh .raw 15) 1 (-1) Z.ok
162      { InflState.fresh .raw 15 with pre := [true], precise := false } := by
163  simp [InflPrime, InflState.fresh]
164
165/-- The earlier false-bit result of priming minus one is rejected. -/
166theorem inflate_prime_negative_rejects_false :
167    ¬ InflPrime (InflState.fresh .raw 15) 1 (-1) Z.ok
168      { InflState.fresh .raw 15 with pre := [false], precise := false } := by
169  simp [InflPrime, InflState.fresh]
170
171/-- A valid decode trace preserves its format, dictionary and output invariants.
172This is a property of the API model; implementation refinement is separate. -/
173theorem inflate_trace_fields {w : Wrap} {b : Nat} {d z o : List UInt8} {final : InflState}
174    (hdecode : Layer.Decodes w b d z o) (hwindow : FullWindow w b z)
175    (htrace : InflTrace z d (InflStart w b d) final) :
176    final.wrap = w ∧ final.wbits = b ∧ final.Exact ∧ final.PermitsDictionary d ∧
177    final.phase ≠ .bad ∧ final.phase ≠ .syncing ∧ final.out <+: o ∧ final.seen <+: z ∧
178    (final.phase = .done → final.out = o ∧ final.seen = z) ∧
179    (final.dict = none → HdrNeedsDict w b z → final.phase = .running → final.seen.length < 6) := by
180  let Inv (st : InflState) : Prop :=
181    st.wrap = w ∧ st.wbits = b ∧ st.Exact ∧ st.PermitsDictionary d ∧
182    st.phase ≠ .bad ∧ st.phase ≠ .syncing ∧ st.out <+: o ∧ st.seen <+: z ∧
183    (st.phase = .done → st.out = o ∧ st.seen = z) ∧
184    (st.dict = none → HdrNeedsDict w b z → st.phase = .running → st.seen.length < 6)
185  have keep : ∀ {start stop}, InflTrace z d start stop → Inv start → Inv stop := by
186    intro start stop trace
187    induction trace with
188    | nil => exact id
189    | @dict s0 s1 s2 r hm ht ih =>
190      intro hi
191      apply ih
192      obtain ⟨hw, hb, he, hp, hbad, hsync, ho, hz, hdone, hearly⟩ := hi
193      obtain ⟨hw', hb', hz', ho', hprec', hval', hp', hdone', hbad', hsync', hearly'⟩ :=
194        dict_step_fields hm hp
195      refine ⟨hw'.trans hw, hb'.trans hb, ⟨hprec'.trans he.1, hval'.trans he.2⟩,
196        hp', fun h => hbad (hbad' h), fun h => hsync (hsync' h), ?_, ?_, ?_, ?_⟩
197      · simpa only [ho'] using ho
198      · simpa only [hz'] using hz
199      · intro h
200        simpa only [ho', hz'] using hdone (hdone' h)
201      · intro hn hd hr
202        obtain ⟨hn', hr'⟩ := hearly' hn hr
203        simpa only [hz'] using hearly hn' hd hr'
204    | @step s0 s1 s2 c r hinput hm ht ih =>
205      intro hi
206      apply ih
207      obtain ⟨hw, hb, he, hp, hbad, hsync, ho, hz, hdone, hearly⟩ := hi
208      have hall : s0.seen ++ c.inp <+: z := by
209        obtain ⟨tail, heq⟩ := hinput
210        refine ⟨tail, ?_⟩
211        rw [List.append_assoc, heq]
212        obtain ⟨tail', rfl⟩ := hz
213        simp
214      have hnew : s0.seen ++ c.inp.take r.out.consumed <+: z := by
215        apply List.IsPrefix.trans (l₂ := s0.seen ++ c.inp) _ hall
216        refine ⟨c.inp.drop r.out.consumed, ?_⟩
217        simp only [List.append_assoc, List.take_append_drop]
218      have hdstate : Layer.Decodes s0.wrap s0.wbits d z o := by simpa only [hw, hb] using hdecode
219      have hwstate : FullWindow s0.wrap s0.wbits (s0.seen ++ c.inp) :=
220        fullWindow_prefix hall (by simpa only [hw, hb] using hwindow)
221      obtain ⟨⟨hbuf, hvalidbuf⟩, _⟩ := hm
222      cases hbf : c.badBuf with
223      | true =>
224        have heq := (hbuf hbf).2.2.2
225        subst s1
226        exact ⟨hw, hb, he, hp, hbad, hsync, ho, hz, hdone, hearly⟩
227      | false =>
228        have hrun := hvalidbuf hbf
229        cases hphase : s0.phase with
230        | bad => exact False.elim (hbad hphase)
231        | syncing => exact False.elim (hsync hphase)
232        | done | mem | needDict =>
233          simp only [hphase] at hrun
234          have heq := hrun.2.2.2
235          subst s1
236          exact ⟨hw, hb, he, hp, hbad, hsync, ho, hz, hdone, hearly⟩
237        | running =>
238          simp only [hphase] at hrun
239          rcases hrun with hrun | hrun
240          · rcases hrun with ⟨hcons, hprod, hseen, hout, _, _, hwrap, hbits, hdict,
241              hprec, hvalidate, _, _, _, hrc, hok, hbuferr, hend, hbaderr, hneed,
242              _, hdec, hdata, _, _, _, hneedlive, _, hdetermined, _⟩
243            have hp' : s1.PermitsDictionary d := by
244              simpa only [InflState.PermitsDictionary, hdict, hwrap] using hp
245            refine ⟨hwrap.trans hw, hbits.trans hb, ⟨hprec.trans he.1, hvalidate.trans he.2⟩,
246              hp', ?_⟩
247            have hforces (hnone : s0.dict = none) (hneeddict : HdrNeedsDict w b z)
248                (hlen : 6 ≤ (s0.seen ++ c.inp).length) : r.out.rc = Z.needDict := by
249              have hnd : HdrNeedsDict s0.wrap s0.wbits (s0.seen ++ c.inp) := by
250                simpa only [hw, hb] using needsDict_prefix hall (by omega) hneeddict
251              exact (hneedlive hnone (hearly hnone hneeddict hphase) hlen hnd).1
252            have hshort : s1.dict = none → HdrNeedsDict w b z → s1.phase = .running →
253                s1.seen.length < 6 := by
254              intro hn hnd hr
255              have hn0 : s0.dict = none := hdict.symm.trans hn
256              by_cases hlen : 6 ≤ (s0.seen ++ c.inp).length
257              · have hph := (hneed (hforces hn0 hnd hlen)).1
258                rw [hph] at hr
259                cases hr
260              · have hlen' : (s0.seen ++ c.inp.take r.out.consumed).length ≤
261                    (s0.seen ++ c.inp).length := by
262                  simp only [List.length_append, List.length_take]
263                  omega
264                rw [hseen]
265                omega
266            have hnotbad : r.out.rc ≠ Z.dataError := by
267              intro herr
268              have hnv := hdata he herr hwstate d hp
269              apply hnv
270              obtain ⟨tail, heq⟩ := hnew
271              exact Or.inr ⟨tail, o, z.length, by simpa only [heq, List.take_length] using hdstate⟩
272            have hprogress (hrunrc : r.out.rc = Z.ok ∨ r.out.rc = Z.bufError)
273                (hph : s1.phase = .running) :
274                s1.phase ≠ .bad ∧ s1.phase ≠ .syncing ∧ s1.out <+: o ∧ s1.seen <+: z ∧
275                  (s1.phase = .done → s1.out = o ∧ s1.seen = z) ∧
276                  (s1.dict = none → HdrNeedsDict w b z → s1.phase = .running → s1.seen.length < 6) := by
277              refine ⟨by simp [hph], by simp [hph], ?_, ?_, ?_, hshort⟩
278              · rw [hout]
279                exact hdetermined he hrunrc d hp z o (Or.inl hnew) hdstate
280              · simpa only [hseen] using hnew
281              · intro h; rw [hph] at h; cases h
282            rcases hrc with hrc | hrc | hrc | hrc | hrc
283            · exact hprogress (Or.inl hrc) (hok hrc).2.2
284            · have hdecode' := hdec he hrc
285              have hdeceff : Layer.Decodes s0.wrap s0.wbits s0.dictEff z o := by
286                by_cases heff : s0.dictEff = d
287                · simpa only [heff] using hdstate
288                · have hnone : s0.dict = none := by
289                    cases hdict0 : s0.dict with
290                    | none => rfl
291                    | some known =>
292                      have hk : d = known := by simpa only [InflState.PermitsDictionary, hdict0] using hp
293                      exact False.elim (heff (by simp [InflState.dictEff, hdict0, hk]))
294                  have hnraw : s0.wrap ≠ .raw := by
295                    intro hr
296                    have hk : d = [] := (by
297                      simpa only [InflState.PermitsDictionary, hnone, hr, ne_eq, not_true_eq_false, false_or] using hp)
298                    exact heff (by simp [InflState.dictEff, hnone, hk])
299                  have hn : ¬ HdrNeedsDict w b z := by
300                    intro hnd
301                    have hlen := needsDict_decoding_prefix_length hnew hnd
302                      (by simpa only [hw, hb] using hdecode')
303                    have halllen : 6 ≤ (s0.seen ++ c.inp).length := by
304                      simp only [List.length_append, List.length_take] at hlen ⊢
305                      omega
306                    have hc : Z.streamEnd = Z.needDict := hrc.symm.trans (hforces hnone hnd halllen)
307                    exact absurd hc (by decide)
308                  exact layer_decodes_dictionary_irrelevant hnraw (by simpa only [hw, hb] using hn) hdstate
309              have hnewcopy := hnew
310              obtain ⟨tail, heq⟩ := hnewcopy
311              have hsame := Layer.ext hdecode' (by simpa only [← heq] using hdeceff)
312              have hsfull : s0.seen ++ c.inp.take r.out.consumed = z := by simpa only [hsame.1, List.append_nil] using heq
313              have hph := hend hrc
314              refine ⟨by simp [hph], by simp [hph], ?_, ?_, ?_, hshort⟩
315              · rw [hout, hsame.2]
316                exact List.prefix_refl _
317              · simpa only [hseen] using hnew
318              · intro _
319                exact ⟨hout.trans hsame.2, hseen.trans hsfull⟩
320            · have hph := (hneed hrc).1
321              have hnil := (hneed hrc).2.1
322              refine ⟨by simp [hph], by simp [hph], ?_, ?_, ?_, hshort⟩
323              · simpa only [hout, hnil, List.append_nil] using ho
324              · simpa only [hseen] using hnew
325              · intro h; rw [hph] at h; cases h
326            · exact False.elim (hnotbad hrc)
327            · exact hprogress (Or.inr hrc) (hbuferr hrc).2
328          · rcases hrun with ⟨_, _, _, _, hphase', hseen, hout, _, _, _, hwrap, hbits,
329              hdict, hprec, hvalidate, _, _, _, _, hdetermined, _⟩
330            have hp' : s1.PermitsDictionary d := by
331              simpa only [InflState.PermitsDictionary, hdict, hwrap] using hp
332            refine ⟨hwrap.trans hw, hbits.trans hb, ⟨hprec.trans he.1, hvalidate.trans he.2⟩,
333              hp', by simp [hphase'], by simp [hphase'], ?_, ?_, ?_, ?_⟩
334            · rw [hout]
335              exact hdetermined he d hp z o (Or.inl hnew) hdstate
336            · simpa only [hseen] using hnew
337            · intro h; rw [hphase'] at h; cases h
338            · intro _ _ h; rw [hphase'] at h; cases h
339  have initial : Inv (InflStart w b d) := by
340    cases hw : w <;> simp [Inv, InflStart, InflState.fresh, InflState.Exact,
341      InflState.PermitsDictionary, hw]
342  exact keep htrace initial
343
344/-- Every model trace on a valid input preserves its decoding and ends at the exact boundary.
345This is a theorem about the API model; implementation refinement is separate. -/
346theorem inflate_decodes : Goal.inflate_decodes := by
347  intro w b d z o final _ hdecode hwindow htrace
348  have h := inflate_trace_fields hdecode hwindow htrace
349  exact ⟨h.2.2.2.2.1, h.2.2.2.2.2.1, h.2.2.2.2.2.2.1,
350    h.2.2.2.2.2.2.2.1, h.2.2.2.2.2.2.2.2.1⟩
351
352/-- A model call with the remaining input and enough space completes or reports allocation failure. -/
353theorem inflate_completes : Goal.inflate_completes := by
354  intro w b d z o st c r st' _ hdecode hwindow hnodict htrace hphase hbuf hin hroom hflush hm
355  obtain ⟨hw, hb, hexact, hperm, _, _, hout, hseen, _, _⟩ :=
356    inflate_trace_fields hdecode hwindow htrace
357  have hcat : st.seen ++ c.inp = z := by
358    rw [hin]
359    obtain ⟨tail, he⟩ := hseen
360    rw [← he, List.drop_left]
361  have hdecode' : Layer.Decodes st.wrap st.wbits st.dictEff z o := by
362    cases hd : st.dict with
363    | some known =>
364      have he : d = known := by simpa [InflState.PermitsDictionary, hd] using hperm
365      simpa [hw, hb, InflState.dictEff, hd, he] using hdecode
366    | none =>
367      by_cases hraw : st.wrap = .raw
368      · have he : d = [] := by simpa [InflState.PermitsDictionary, hd, hraw] using hperm
369        simpa [hw, hb, InflState.dictEff, hd, he] using hdecode
370      · have hdstate : Layer.Decodes st.wrap st.wbits d z o := by simpa [hw, hb] using hdecode
371        have hnstate : ¬ HdrNeedsDict st.wrap st.wbits z := by simpa [hw, hb] using hnodict
372        have he := layer_decodes_dictionary_irrelevant (d2 := []) hraw hnstate hdstate
373        simpa [InflState.dictEff, hd] using he
374  have hrun : InflRun st c r.out st' := by
375    have h := hm.1.2 hbuf
376    simpa only [hphase] using h
377  rcases hrun with hrun | hmem
378  · rcases hrun with ⟨hcons, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _,
379      _, hdec, _, _, hlive, _, _, _, _, _⟩
380    have hr : r.out.rc = Z.streamEnd := by
381      apply hlive hexact hflush
382      · simpa [hw, hb, hcat] using hwindow
383      · intro _
384        simpa [hw, hb, hcat] using hnodict
385      · refine ⟨z.length, o, ?_, ?_, ?_, hout, hroom⟩
386        · obtain ⟨tail, he⟩ := hseen
387          rw [← he, List.length_append]
388          omega
389        · simp [hcat]
390        · simpa [hcat] using hdecode'
391    have hfinal := hdec hexact hr
392    have hpart : st.seen ++ c.inp.take r.out.consumed <+: z := by
393      refine ⟨c.inp.drop r.out.consumed, ?_⟩
394      simpa [List.append_assoc, List.take_append_drop] using hcat
395    obtain ⟨tail, he⟩ := hpart
396    have hext := Layer.ext hfinal (by simpa [← he] using hdecode')
397    have hstream : st.seen ++ c.inp.take r.out.consumed = z := by
398      simpa [hext.1] using he
399    have hlen := congrArg List.length hstream
400    have hcin := congrArg List.length hcat
401    simp only [List.length_append, List.length_take] at hlen
402    simp only [List.length_append] at hcin
403    refine Or.inl ⟨hm.2.trans hr, ?_, ?_⟩
404    · omega
405    · rw [← hext.2, List.drop_left]
406  · exact Or.inr (hm.2.trans hmem.1)
407
408#print axioms inflate_completes
409
410end ZlibF.Spec.Api.Proofs