inflate.c.start.lean

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

1import ZlibF.Proof.«inflate.c.end»
2
3/-!
4# inflate.c: `inflateInit2_` and `inflateInit_`
5-/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9
10theorem inflateReset2_ok_of {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
11    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : WindowOk h st.window) {w : Int32}
12    {wrap wb : Int32} (hp : reset2Params w = some (wrap, wb)) :
13    inflateReset2 (some r) w h = .ok (Z_OK, setI (r.put (reset2Heap h wb st)
14        (resetKeepStream z (resetPre (reset2Pre wrap wb st)))) zs (resetKeepState zs (resetPre (reset2Pre wrap wb st)))) := by
15  have := inflateReset2_run hL hf hwo w
16  rw [hp] at this
17  exact this.2
18
19theorem inflateReset2_err_of {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
20    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : WindowOk h st.window) {w : Int32}
21    (hp : reset2Params w = none) : inflateReset2 (some r) w h = .ok (Z_STREAM_ERROR, h) := by
22  have := inflateReset2_run hL hf hwo w
23  rw [hp] at this
24  exact this
25
26@[simp] theorem allocIstHeap_streams (h : Heap) (st : InflateState) : (allocIstHeap h st).streams = h.streams := rfl
27@[simp] theorem allocIstHeap_gzstates (h : Heap) (st : InflateState) : (allocIstHeap h st).gzstates = h.gzstates := rfl
28@[simp] theorem allocIstHeap_bytes (h : Heap) (st : InflateState) : (allocIstHeap h st).bytes = h.bytes := rfl
29@[simp] theorem allocIstHeap_ro (h : Heap) (st : InflateState) : (allocIstHeap h st).ro = h.ro := rfl
30@[simp] theorem allocIstHeap_nextBlk (h : Heap) (st : InflateState) : (allocIstHeap h st).nextBlk = h.nextBlk + 1 := rfl
31@[simp] theorem allocIstHeap_nalloc (h : Heap) (st : InflateState) : (allocIstHeap h st).nalloc = h.nalloc + 1 := rfl
32@[simp] theorem allocIstHeap_istates_same (h : Heap) (st : InflateState) : (allocIstHeap h st).istates h.nextBlk = some st := by
33  simp [allocIstHeap]
34@[simp] theorem allocIstHeap_istates_ne (h : Heap) (st : InflateState) (x : Nat) (hx : x ≠ h.nextBlk) :
35    (allocIstHeap h st).istates x = h.istates x := by simp [allocIstHeap, upd_ne _ _ _ _ hx]
36
37@[simp] theorem ZStreamRef.get_allocIst (h : Heap) (st : InflateState) (r : ZStreamRef) :
38    r.get (allocIstHeap h st) = r.get h := by cases r <;> rfl
39
40@[simp] theorem ZStreamRef.put_allocIst (h : Heap) (st : InflateState) (r : ZStreamRef) (v : ZStream) :
41    r.put (allocIstHeap h st) v = allocIstHeap (r.put h v) st := by
42  cases r with
43  | tab i => simp only [ZStreamRef.put, allocIstHeap]; cases hh : h.streams i <;> simp
44  | in_gzstate_strm i => simp only [ZStreamRef.put, allocIstHeap]; cases hh : h.gzstates i <;> simp
45
46@[simp] theorem allocIstHeap_istates_eq (h : Heap) (st : InflateState) (x : Nat) (hx : x = h.nextBlk) :
47    (allocIstHeap h st).istates x = some st := by subst hx; simp
48
49@[simp] theorem setI_allocIst (h : Heap) (g s : InflateState) (x : Nat) (hx : x = h.nextBlk) :
50    setI (allocIstHeap h g) x s = allocIstHeap h s := by
51  subst hx; simp [setI, allocIstHeap, upd_upd]
52
53theorem zfrees_run' {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree")
54    (zs : Nat) : ZFREES (some r) (some (.tab zs)) h = freeInflateState (some (.tab zs)) h := by
55  simp [ZFREES, ldZ_eq, hz, hf]
56
57theorem zfrees_run2 {h : Heap} {r : ZStreamRef} (hf : (r.get h).map (·.zfree) = some (.fn "zcfree")) (zs : Nat) :
58    ZFREES (some r) (some (.tab zs)) h = freeInflateState (some (.tab zs)) h := by
59  cases hz : r.get h with
60  | none => simp [hz] at hf
61  | some z =>
62    simp [hz] at hf
63    exact zfrees_run' hz hf zs
64
65theorem freeI_eq (h : Heap) (zs : Nat) : freeInflateState (some (.tab zs)) h =
66    match h.istates zs with
67    | some _ => Except.ok ((), freeIst h zs)
68    | none => Except.error (Fault.ub "free of a freed or invalid pointer (inflate_state)") := rfl
69
70theorem zallocs_run {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hza : z.zalloc = .fn "zcalloc") :
71    ZALLOCS (some r) h = allocInflateState h := by
72  simp [ZALLOCS, ldZ_eq, hz, hza]
73
74theorem allocIst_ok (h : Heap) (hok : h.allocOk h.nalloc = true) (hF : Fresh h) :
75    allocInflateState h = .ok (some (.tab h.nextBlk), allocIstHeap h (InflateState.garbage (h.garbage h.nalloc))) := by
76  rw [allocInflateState_some hok hF.slotUsed_next]; rfl
77
78theorem allocIst_put {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hok : h.allocOk h.nalloc = true)
79    (hF : Fresh h) (v : ZStream) :
80    allocInflateState (r.put h v) = .ok (some (.tab h.nextBlk),
81      allocIstHeap (r.put h v) (InflateState.garbage (h.garbage h.nalloc))) := by
82  have hF' : Fresh (r.put h v) := (shape_put hz v).fresh (by simp) hF
83  rw [allocInflateState_some (by simpa using hok) hF'.slotUsed_next]
84  simp [allocIstHeap]
85
86theorem allocIst_fail_put {h : Heap} {r : ZStreamRef} (hok : ¬ h.allocOk h.nalloc = true) (v : ZStream) :
87    allocInflateState (r.put h v) = .ok (none, { r.put h v with nalloc := h.nalloc + 1 }) := by
88  have : ¬ (r.put h v).allocOk (r.put h v).nalloc = true := by simpa using hok
89  rw [allocInflateState_none this]
90  simp
91
92theorem allocIst_fail (h : Heap) (hok : ¬ h.allocOk h.nalloc = true) :
93    allocInflateState h = .ok (none, { h with nalloc := h.nalloc + 1 }) := allocInflateState_none hok
94
95theorem fresh_allocIst {h : Heap} (hF : Fresh h) (st : InflateState) : Fresh (allocIstHeap h st) := by
96  intro b hb hl
97  simp only [allocIstHeap_nextBlk] at hb
98  apply hF b (by omega)
99  have hne : b ≠ h.nextBlk := by omega
100  simpa only [Heap.live, allocIstHeap, upd_ne _ _ _ _ hne] using hl
101
102theorem uniq_allocIst {h : Heap} (hU : Uniq h) (hF : Fresh h) (st : InflateState) : Uniq (allocIstHeap h st) := by
103  intro b
104  by_cases hb : b = h.nextBlk
105  · subst hb
106    have := Heap.not_live.mp (hF _ (Nat.le_refl _))
107    obtain ⟨e0, e1, e2, e3, e4, e5, e6⟩ := this
108    simp [allocIstHeap, e0, e1, e2, e3, e4, e6]
109  · have := hU b
110    simpa only [allocIstHeap, upd_ne _ _ _ _ hb] using this
111
112theorem owns_allocIst {h : Heap} (hF : Fresh h) (st : InflateState) {S : Nat → Prop} (hO : h.Owns S) :
113    (allocIstHeap h st).Owns (fun b => S b ∨ b = h.nextBlk) := by
114  intro b
115  by_cases hb : b = h.nextBlk
116  · subst hb; simp [Heap.live, allocIstHeap]
117  · have := hO b
118    simp only [Heap.live, allocIstHeap, upd_ne _ _ _ _ hb] at this ⊢
119    simp [hb, this]
120
121theorem inflateInit2_success {h : Heap} {r : ZStreamRef} {z : ZStream} {w : Int32} {version : BPtr}
122    (hz : r.get h = some z) (hF : Fresh h) (hok : h.allocOk h.nalloc = true)
123    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
124    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49)
125    {wrap wb : Int32} (hp : reset2Params w = some (wrap, wb)) :
126    inflateInit2_ (some r) w version 112 h = .ok (Z_OK, initOkHeap h r z wrap wb) := by
127  have hv0' : index8 version 0 h = .ok (49, h) := hv0
128  unfold inflateInit2_
129  rcases hza with hza | hza <;> rcases hzf with hzf | hzf <;>
130  isimp [hz, hv, hv0', initStream, hza, hzf, zallocs_run, allocIst_put hz hok hF]
131  all_goals (
132    rw [inflateReset2_ok_of (zs := h.nextBlk) (hp := hp)]
133    rotate_left
134    · exact ⟨by simp [hz]; rfl, allocIstHeap_istates_eq _ _ _ (by simp), by simp [StateRef.ofInflateState], by simp, by simp [HEAD, SYNC], by simp [initStream, hza], by simp [initStream, hza]⟩
135    · simp
136    · exact Or.inl rfl
137    · simp [initOkHeap, initStream2, initState, initStream, hza, hzf, reset2Heap, freeWin_null, StateRef.ofInflateState])
138
139
140theorem inflateInit2_version_null (strm : ZStreamPtr) (w : Int32) (sz : Int32) (h : Heap) :
141    inflateInit2_ strm w .null sz h = .ok (Z_VERSION_ERROR, h) := by
142  simp [inflateInit2_]
143
144theorem inflateInit2_version_char (strm : ZStreamPtr) (w : Int32) (version : BPtr) (sz : Int32) (h : Heap) (c : UInt8)
145    (hv : version ≠ .null) (hc : index8 version 0 h = .ok (c, h)) (hne : c ≠ 49) :
146    inflateInit2_ strm w version sz h = .ok (Z_VERSION_ERROR, h) := by
147  simp [inflateInit2_, hv, hc, hne]
148
149theorem inflateInit2_version_size (strm : ZStreamPtr) (w : Int32) (version : BPtr) (sz : Int32) (h : Heap)
150    (hv : version ≠ .null) (hc : index8 version 0 h = .ok (49, h)) (hne : sz ≠ 112) :
151    inflateInit2_ strm w version sz h = .ok (Z_VERSION_ERROR, h) := by
152  simp [inflateInit2_, hv, hc, hne]
153
154theorem inflateInit2_nullstream (w : Int32) (version : BPtr) (h : Heap)
155    (hv : version ≠ .null) (hc : index8 version 0 h = .ok (49, h)) :
156    inflateInit2_ none w version 112 h = .ok (Z_STREAM_ERROR, h) := by
157  simp [inflateInit2_, hv, hc]
158
159theorem inflateInit2_memfail {h : Heap} {r : ZStreamRef} {z : ZStream} {w : Int32} {version : BPtr}
160    (hz : r.get h = some z) (hF : Fresh h) (hok : ¬ h.allocOk h.nalloc = true)
161    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
162    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49) :
163    inflateInit2_ (some r) w version 112 h = .ok (Z_MEM_ERROR, initMemHeap h r z) := by
164  have hv0' : index8 version 0 h = .ok (49, h) := hv0
165  unfold inflateInit2_
166  rcases hza with hza | hza <;> rcases hzf with hzf | hzf <;>
167  isimp [hz, hv, hv0', initStream, hza, hzf, zallocs_run, allocIst_fail_put (r := r) hok, initMemHeap, initStream]
168
169theorem inflateInit2_badbits {h : Heap} {r : ZStreamRef} {z : ZStream} {w : Int32} {version : BPtr}
170    (hz : r.get h = some z) (hF : Fresh h) (hok : h.allocOk h.nalloc = true)
171    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
172    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49)
173    (hp : reset2Params w = none) :
174    inflateInit2_ (some r) w version 112 h = .ok (Z_STREAM_ERROR, initBadHeap h r z) := by
175  have hv0' : index8 version 0 h = .ok (49, h) := hv0
176  unfold inflateInit2_
177  rcases hza with hza | hza <;> rcases hzf with hzf | hzf <;>
178  isimp [hz, hv, hv0', initStream, hza, hzf, zallocs_run, allocIst_put hz hok hF]
179  all_goals (
180    rw [inflateReset2_err_of (zs := h.nextBlk) (hp := hp)]
181    rotate_left
182    · exact ⟨by simp [hz]; rfl, allocIstHeap_istates_eq _ _ _ (by simp), by simp [StateRef.ofInflateState], by simp, by simp [HEAD, SYNC], by simp [initStream, hza], by simp [initStream, hza]⟩
183    · simp
184    · exact Or.inl rfl
185    · isimp [initBadHeap, initStream2, initState, initStream, hza, hzf, reset2Heap, freeWin_null, StateRef.ofInflateState, zfrees_run2, freeI_eq, Z_STREAM_ERROR, Z_OK, hz])
186
187
188theorem initState_win (r : ZStreamRef) (h : Heap) : WinInv h (initState r) := by
189  refine ⟨?_, Or.inl rfl, fun _ => rfl, Or.inl rfl, ?_, ?_, ?_⟩
190  all_goals simp [initState, InflateState.zeroed, InflateState.garbage, Junk.of]
191
192theorem reset2Heap_null (h : Heap) (wb : Int32) (st : InflateState) (hw : st.window = .null) : reset2Heap h wb st = h := by
193  unfold reset2Heap; split
194  · rw [hw]; rfl
195  · rfl
196
197theorem wf_initState (r : ZStreamRef) : (initState r).WellFormed := by
198  simp [initState, InflateState.WellFormed, InflateState.zeroed, InflateState.garbage]
199
200theorem wf_reset2Pre (wrap wb : Int32) {st : InflateState} (hw : st.WellFormed) : (reset2Pre wrap wb st).WellFormed := by
201  unfold InflateState.WellFormed at *
202  unfold reset2Pre
203  split <;> simpa using hw
204
205theorem reset2Params_bits {w wrap wb : Int32} (hp : reset2Params w = some (wrap, wb)) : badBits wb = false := by
206  unfold reset2Params at hp
207  by_cases h1 : w < 0
208  · by_cases h2 : w < -15
209    · simp [h1, h2] at hp
210    · have e : Int32.ofInt (-w.toInt) = -w := by simp
211      simp only [h1, h2, ite_true, ite_false, e] at hp
212      by_cases hb : badBits (-w) = true
213      · simp [hb] at hp
214      · simp only [hb, Bool.false_eq_true, ite_false, Option.some.injEq, Prod.mk.injEq] at hp
215        obtain ⟨-, rfl⟩ := hp
216        simpa using hb
217  · by_cases h2 : w < 48
218    · simp only [h1, h2, ite_true, ite_false] at hp
219      by_cases hb : badBits (w &&& 15) = true
220      · simp [hb] at hp
221      · simp only [hb, Bool.false_eq_true, ite_false, Option.some.injEq, Prod.mk.injEq] at hp
222        obtain ⟨-, rfl⟩ := hp
223        simpa using hb
224    · simp only [h1, h2, ite_true, ite_false] at hp
225      by_cases hb : badBits w = true
226      · simp [hb] at hp
227      · simp only [hb, Bool.false_eq_true, ite_false, Option.some.injEq, Prod.mk.injEq] at hp
228        obtain ⟨-, rfl⟩ := hp
229        simpa using hb
230
231/-- **inflateInit2_, success.** If the version arguments are right (`version[0]` is `'1'`, `stream_size` is 112), the
232allocation of the state succeeds and `windowBits` is accepted (`reset2Params w = some (wrap, wb)`), the call returns
233`Z_OK` without a fault. The new state is the block `h.nextBlk` (nothing else is allocated), the stream record has the
234default allocator functions and points to it, the stream is initialised with the invariants intact, and the stream
235owns exactly one more block (the state; the window is allocated later by `updatewindow`). The allocator functions
236of the caller's record are `NULL` or the default ones (the model has no others). -/
237theorem inflateInit2_ok {h : Heap} {r : ZStreamRef} {z : ZStream} {w : Int32} {version : BPtr}
238    (hU : Uniq h) (hF : Fresh h) (hz : r.get h = some z) (hok : h.allocOk h.nalloc = true)
239    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
240    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49)
241    {wrap wb : Int32} (hp : reset2Params w = some (wrap, wb)) :
242    ∃ h', C.run (inflateInit2_ (some r) w version 112) h = .ok (Z_OK, h') ∧ h' = initOkHeap h r z wrap wb ∧
243      Good h' r h.nextBlk (resetKeepStream (initStream2 z h.nextBlk)
244        (resetPre (reset2Pre wrap wb (initState r)))) (resetKeepState h.nextBlk (resetPre (reset2Pre wrap wb (initState r)))) ∧
245      (∀ S, h.Owns S → h'.Owns (fun b => S b ∨ b = h.nextBlk)) := by
246  have hrun := inflateInit2_success hz hF hok hza hzf hv hv0 hp
247  have hb : badBits wb = false := reset2Params_bits hp
248  have hza' : (initStream z).zalloc ≠ .null := by
249    rcases hza with hza | hza <;> simp [initStream, hza]
250  have hzf' : (initStream z).zfree ≠ .null := by
251    rcases hzf with hzf | hzf <;> simp [initStream, hzf]
252  obtain ⟨z2, hz2⟩ : ∃ z2 : ZStream, z2 = initStream2 z h.nextBlk := ⟨_, rfl⟩
253  have hzp : r.get (r.put h z2) = some z2 := by simp [hz]
254  have hFp : Fresh (r.put h z2) := (shape_put hz z2).fresh (by simp) hF
255  have hUp : Uniq (r.put h z2) := (shape_put hz z2).uniq hU
256  have hFA := fresh_allocIst hFp (initState r)
257  have hUA := uniq_allocIst hUp hFp (initState r)
258  have e0 : reset2Heap (allocIstHeap (r.put h z2) (initState r)) wb (initState r) = allocIstHeap (r.put h z2) (initState r) :=
259    reset2Heap_null _ _ _ rfl
260  have hwin := winInv_reset2 (h := allocIstHeap (r.put h z2) (initState r)) (initState_win r _) (bits15 hb) wrap
261  have hz0 : r.get (allocIstHeap (r.put h z2) (initState r)) = some z2 := by simp [hz]
262  have hs0 : (allocIstHeap (r.put h z2) (initState r)).istates h.nextBlk = some (initState r) :=
263    allocIstHeap_istates_eq _ _ _ (by simp)
264  refine ⟨_, hrun, rfl, ?_, ?_⟩
265  · unfold initOkHeap
266    simp only [← hz2]
267    rw [e0]
268    refine good_set hz0 hs0 hUA hFA ?_ ?_ ?_ ?_ ?_ ?_
269    · simp [resetKeepStream, hz2, initStream2]
270    · simpa [resetKeepStream, hz2, initStream2] using hza'
271    · simpa [resetKeepStream, hz2, initStream2] using hzf'
272    · simp [resetKeepState, strm_pre, initState]
273    · simpa [resetKeepState] using mode_head
274    · rw [← e0]
275      refine stInv_rk (wf_resetPre (wf_reset2Pre wrap wb (wf_initState r))) hwin ?_
276      simpa [reqbits_resetPre, reset2Pre] using bits15 hb
277  · intro S hO
278    have h1 := owns_allocIst hFp (initState r) ((shape_put hz z2).owns hO)
279    simp only [ZStreamRef.put_nextBlk] at h1
280    unfold initOkHeap
281    simp only [← hz2]
282    rw [e0]
283    exact ((shape_put hz0 _).trans (shape_setI (by simp only [ZStreamRef.put_istates]; exact hs0) _)).owns h1
284
285
286theorem Shape.fresh_le {h h' : Heap} (hS : Shape h h') (hn : h.nextBlk ≤ h'.nextBlk) (hF : Fresh h) : Fresh h' := by
287  intro b hb hl
288  exact hF b (by omega) ((hS.live b).1 hl)
289
290theorem shape_allocfree {H : Heap} (hF : Fresh H) (st : InflateState) :
291    Shape H (freeIst (allocIstHeap H st) H.nextBlk) := by
292  intro b
293  by_cases hb : b = H.nextBlk
294  · subst hb
295    have := Heap.not_live.mp (hF _ (Nat.le_refl _))
296    obtain ⟨e0, e1, e2, e3, e4, e5, e6⟩ := this
297    simp [freeIst, allocIstHeap, e0, e1, e2, e3, e4, e5, e6]
298  · simp [freeIst, allocIstHeap, upd_ne _ _ _ _ hb]
299
300theorem initMem_good {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hU : Uniq h) (hF : Fresh h) :
301    Uniq (initMemHeap h r z) ∧ Fresh (initMemHeap h r z) ∧ (∀ b, (initMemHeap h r z).live b ↔ h.live b) := by
302  have hS : Shape h (initMemHeap h r z) := by
303    have := shape_put hz (initStream z)
304    intro b; exact this b
305  exact ⟨hS.uniq hU, hS.fresh (by simp [initMemHeap]) hF, hS.live⟩
306
307theorem initBad_good {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hU : Uniq h) (hF : Fresh h) :
308    Uniq (initBadHeap h r z) ∧ Fresh (initBadHeap h r z) ∧ (∀ b, (initBadHeap h r z).live b ↔ h.live b) := by
309  have hFp : Fresh (r.put h (initStream2 z h.nextBlk)) := (shape_put hz _).fresh (by simp) hF
310  have hS1 := shape_allocfree hFp (initState r)
311  have hS2 : Shape h (initBadHeap h r z) := by
312    unfold initBadHeap
313    simp only [ZStreamRef.put_nextBlk] at hS1
314    exact ((shape_put hz _).trans hS1).trans (shape_put (z0 := initStream2 z h.nextBlk) (by simp [hz]) _)
315  exact ⟨hS2.uniq hU, hS2.fresh_le (by simp [initBadHeap]) hF, hS2.live⟩
316
317/-- **inflateInit2_, safety (every outcome).** For a stream record `z` whose allocator functions are `NULL` or the default
318ones (`zlib.h`: the caller sets them before the call; the model has only the defaults), a `version` that is `NULL` or
319points to a readable byte, any `stream_size` and any `windowBits`, the call never faults and keeps `Uniq` and `Fresh`.
320The outcome is exactly one of: a version error (`version` `NULL`, first character not `'1'`, or `stream_size` not 112:
321nothing changes); `Z_MEM_ERROR` (the allocation oracle says no: no block is allocated, none leaks); `Z_STREAM_ERROR`
322(`windowBits` refused: the state was allocated and is freed again, the stream's state pointer is `NULL`, the live
323blocks are the old ones); `Z_OK` (see `inflateInit2_ok`). -/
324theorem inflateInit2_safe {h : Heap} {r : ZStreamRef} {z : ZStream} {w : Int32} {version : BPtr} {sz : Int32}
325    (hU : Uniq h) (hF : Fresh h) (hz : r.get h = some z)
326    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
327    (hv : version = .null ∨ ∃ c, OkOn h (index8 version 0) c) :
328    ∃ v h', C.run (inflateInit2_ (some r) w version sz) h = .ok (v, h') ∧ Uniq h' ∧ Fresh h' ∧
329      ((v = Z_VERSION_ERROR ∧ h' = h ∧ (version = .null ∨ (∃ c, OkOn h (index8 version 0) c ∧ c ≠ 49) ∨ sz ≠ 112)) ∨
330       (v = Z_MEM_ERROR ∧ ¬ h.allocOk h.nalloc = true ∧ h' = initMemHeap h r z ∧ (∀ b, h'.live b ↔ h.live b)) ∨
331       (v = Z_STREAM_ERROR ∧ h.allocOk h.nalloc = true ∧ reset2Params w = none ∧ h' = initBadHeap h r z ∧
332          (∀ b, h'.live b ↔ h.live b)) ∨
333       (v = Z_OK ∧ sz = 112 ∧ h.allocOk h.nalloc = true ∧ ∃ wrap wb, reset2Params w = some (wrap, wb) ∧
334          h' = initOkHeap h r z wrap wb)) := by
335  by_cases hvn : version = .null
336  · subst hvn
337    exact ⟨_, _, by rw [C.run]; exact inflateInit2_version_null _ _ _ _, hU, hF, Or.inl ⟨rfl, rfl, Or.inl rfl⟩⟩
338  have hvc : ∃ c, OkOn h (index8 version 0) c := hv.resolve_left hvn
339  obtain ⟨c, hc⟩ := hvc
340  by_cases hc49 : c = 49
341  · subst hc49
342    by_cases hsz : sz = 112
343    · subst hsz
344      by_cases hok : h.allocOk h.nalloc = true
345      · cases hp : reset2Params w with
346        | none =>
347          obtain ⟨u1, f1, l1⟩ := initBad_good hz hU hF
348          exact ⟨_, _, inflateInit2_badbits hz hF hok hza hzf hvn hc hp, u1, f1,
349            Or.inr (Or.inr (Or.inl ⟨rfl, hok, rfl, rfl, l1⟩))⟩
350        | some p =>
351          obtain ⟨wrap, wb⟩ := p
352          obtain ⟨h', hr, he, hG, hO⟩ := inflateInit2_ok hU hF hz hok hza hzf hvn hc hp
353          refine ⟨_, _, hr, hG.uniq, hG.fresh, Or.inr (Or.inr (Or.inr ⟨rfl, rfl, hok, wrap, wb, rfl, he⟩))⟩
354      · obtain ⟨u1, f1, l1⟩ := initMem_good hz hU hF
355        exact ⟨_, _, inflateInit2_memfail hz hF hok hza hzf hvn hc, u1, f1, Or.inr (Or.inl ⟨rfl, hok, rfl, l1⟩)⟩
356    · exact ⟨_, _, by rw [C.run]; exact inflateInit2_version_size _ _ _ _ _ hvn hc hsz, hU, hF,
357        Or.inl ⟨rfl, rfl, Or.inr (Or.inr hsz)⟩⟩
358  · exact ⟨_, _, by rw [C.run]; exact inflateInit2_version_char _ _ _ _ _ c hvn hc hc49, hU, hF,
359      Or.inl ⟨rfl, rfl, Or.inr (Or.inl ⟨c, hc, hc49⟩)⟩⟩
360
361end Zlib.Inflate.Proofs