inflate.c.main.check.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.main.check0»
2import ZlibF.Proof.«crc32.c»
3import ZlibF.Proof.«adler32.c»
4
5/-!
6# inflate.c: the trailer modes `LENGTH` and `CHECK`
7
8`case LENGTH:` and `case CHECK:` of `inflate()`, and the fall-through `DONE`. Every exit and every error message.
9`CHECK` calls `crc32` or `adler32` on the output written by this call; the callee theorems `crc32_z_correct` and
10`adler32_z_correct` give the value.
11-/
12
13namespace Zlib.Inflate.Proofs
14open C Zlib.Inflate Zlib.Inflate.Spec
15
16/-- `UPDATE_CHECK(check, buf, len)` on `len` bytes of a byte block: the CRC-32 of the bytes when `state->flags` is set, else the
17Adler-32 (`crc32` / `adler32` of `zlib.h`). No fault, the heap is unchanged. The Adler-32 value is the specification's
18whenever `len ≠ 1` or the high half of `check` is a canonical sum (`< 65521`: true of every value `adler32` returns); for `len = 1`
19and a non-canonical `check` the value is whatever `adler32` computes. `StaticsOK`: the static CRC tables of the heap hold their
20contents. -/
21theorem UPDATE_CHECK_run {h : Heap} {zs : Nat} {s : InflateState} {blk off : Nat} {a : Array UInt8} {len : UInt32}
22    (hS : Zlib.Crc32.Proofs.StaticsOK h) (hs : h.istates zs = some s) (hb : h.bytes blk = some a)
23    (hfit : off + len.toNat ≤ a.size) (check : UInt64) :
24    ∃ v, UPDATE_CHECK (some (.tab zs)) check (.ref (.blk blk) off) len h = .ok (v, h) ∧
25      (s.flags ≠ 0 → v = (ZlibF.Spec.crc32Update check.toUInt32 ((a.toList.drop off).take len.toNat)).toUInt64) ∧
26      (s.flags = 0 → (len ≠ 1 ∨ (check >>> 16 &&& 65535).toNat < 65521) →
27        v.toNat = Zlib.Adler32.Spec.adler32 check.toNat (Zlib.Adler32.Proofs.seg a off len.toNat)) := by
28  by_cases hf : s.flags = 0
29  · have hL : len.toNat < 2 ^ 64 := by have := UInt32.toNat_lt len; omega
30    have e64 : len.toNat.toUInt64 = len.toUInt64 := by simp
31    obtain ⟨v, hv⟩ := Zlib.Adler32.Proofs.adler32_safe h blk a hb check off len.toNat hfit (UInt32.toNat_lt len)
32    have e32 : len.toNat.toUInt32 = len := by simp at *
33    rw [e32] at hv
34    refine ⟨v, ?_, fun h1 => absurd hf h1, fun _ hv' => ?_⟩
35    · unfold UPDATE_CHECK
36      simp [bind_app, rdI_eq, hs, hf]
37      exact hv
38    · by_cases h1 : len = 1
39      · subst h1
40        have hv2 := hv'.resolve_left (by simp)
41        have := Zlib.Adler32.Proofs.adler32_z_correct h blk a hb check off 1 hfit (by decide) hv2
42        obtain ⟨r, hr, hrv⟩ := this
43        have hv1 : C.run (Zlib.Adler32.adler32 check (.ref (.blk blk) off) 1) h = .ok (v, h) := hv
44        unfold Zlib.Adler32.adler32 at hv1
45        have : (1 : UInt32).toUInt64 = (1 : Nat).toUInt64 := rfl
46        rw [this] at hv1
47        rw [hr] at hv1
48        cases hv1
49        exact hrv
50      · obtain ⟨r, hr, hrv⟩ := Zlib.Adler32.Proofs.adler32_z_correct_ne_one h blk a hb check off len.toNat hfit hL
51          (fun e => h1 (by apply UInt32.toNat_inj.mp; simpa using e))
52        have hv1 : C.run (Zlib.Adler32.adler32 check (.ref (.blk blk) off) len) h = .ok (v, h) := hv
53        unfold Zlib.Adler32.adler32 at hv1
54        rw [show len.toUInt64 = len.toNat.toUInt64 by simp, hr] at hv1
55        cases hv1
56        exact hrv
57  · obtain hc := Zlib.Crc32.Proofs.crc32_correct h hS check blk off a hb len hfit
58    refine ⟨_, ?_, fun _ => rfl, fun h1 => absurd h1 hf⟩
59    unfold UPDATE_CHECK
60    have hf' : ¬ s.flags = 0 := hf
61    simp [bind_app, rdI_eq, hs, hf']
62    exact hc
63
64/-- `case LENGTH:` with no length to check (`wrap = 0` or `flags = 0`): `state->mode = DONE; ret = Z_STREAM_END;
65goto inf_leave`. -/
66theorem inflate_LENGTH_skip {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {s : InflateState}
67    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hno : s.wrap = 0 ∨ s.flags = 0) :
68    runX (inflate_LENGTH c) l h =
69      .ok ((.error Ex.leave, { l with ret := Z_STREAM_END }), setI h zs { s with mode := DONE }) := by
70  have hb : ¬ (¬ s.wrap = 0 ∧ ¬ s.flags = 0) := by
71    rcases hno with e | e <;> simp [e]
72  unfold inflate_LENGTH
73  rw [hc]
74  simp [runX_bind, runX_lift, ldI_eq, hs, hb, runX_pure, setMode, wrI_eq, inflate_DONE, runX_modify, runX_throw]
75
76/-- `case LENGTH:` with a length to check (`wrap ≠ 0`, `flags ≠ 0`): `NEEDBITS(32)`; if the input ran out, `goto inf_leave` with
77the registers of that moment; else, when `(wrap & 4)` is set and `hold` differs from the low 32 bits of `total`, the error
78"incorrect length check" (`BAD`, `break`); else `INITBITS`, `mode = DONE`, `ret = Z_STREAM_END`, `goto inf_leave`.
79`bs` are the input bytes not yet pulled; the bit stream is preserved. -/
80theorem inflate_LENGTH_run {c : Ctx} {l : IL} {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
81    {bs : List UInt8} (hr : c.strm = some r) (hc : c.st = some (.tab zs)) (hz : r.get h = some z)
82    (hs : h.istates zs = some s) (hw : s.wrap ≠ 0) (hf : s.flags ≠ 0) (B : BitInv h l bs) :
83    ∃ rr l' j, runX (NEEDBITS 32) l h = .ok ((rr, l'), h) ∧ j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
84      stream l' (bs.drop j) = stream l bs ∧
85      (rr = .error Ex.leave → l'.have_ = 0 ∧ j = bs.length ∧ l'.bits.toNat < 32 ∧
86        runX (inflate_LENGTH c) l h = .ok ((.error Ex.leave, l'), h)) ∧
87      (rr = .ok () → 32 ≤ l'.bits.toNat ∧
88        ((s.wrap &&& 4) ≠ 0 → l'.hold ≠ (s.total &&& 0xffffffff) →
89          ∃ i, strTable[i]? = some "incorrect length check" ∧
90            runX (inflate_LENGTH c) l h = .ok ((.ok (), l'), tcBadHeap h r zs z s i)) ∧
91        (¬ ((s.wrap &&& 4) ≠ 0 ∧ l'.hold ≠ (s.total &&& 0xffffffff)) →
92          runX (inflate_LENGTH c) l h = .ok ((.error Ex.leave, { l' with hold := 0, bits := 0, ret := Z_STREAM_END }),
93            setI h zs { s with mode := DONE }))) := by
94  obtain ⟨rr, l', j, hrun, hj, B', hS, hbits, hshape, hmax, hid, hok, hleave⟩ := NEEDBITS_run B 32 (by decide)
95  have hw' : ¬ s.wrap = 0 := hw
96  have hf' : ¬ s.flags = 0 := hf
97  refine ⟨rr, l', j, hrun, hj, B', hS, ?_, ?_⟩
98  · intro e
99    obtain ⟨h1, h2, h3⟩ := hleave e
100    refine ⟨h2, h1, h3, ?_⟩
101    unfold inflate_LENGTH
102    rw [hc]
103    simp [runX_bind, runX_lift, ldI_eq, hs, hw', hf', hrun, e, runX_throw]
104  · intro e
105    refine ⟨hok e, ?_, ?_⟩
106    · intro h4 hne
107      obtain ⟨i, hi, hbad⟩ := tcBadMode_run (c := c) "incorrect length check" lit_length_check hr hc hz hs
108      refine ⟨i, hi, ?_⟩
109      unfold inflate_LENGTH
110      rw [hc]
111      simp [runX_bind, runX_lift, ldI_eq, hs, hw', hf', hrun, e, runX_get, h4, hne, hbad, runX_pure]
112    · intro hn
113      unfold inflate_LENGTH
114      rw [hc]
115      have hn' : ¬ (¬ s.wrap &&& 4 = 0 ∧ ¬ l'.hold = s.total &&& 4294967295) := hn
116      simp [runX_bind, runX_lift, ldI_eq, hs, hw', hf', hrun, e, runX_get, hn', runX_pure, runX_INITBITS, setMode, wrI_eq,
117        inflate_DONE, runX_modify, runX_throw]
118
119/-! ### `case CHECK:` -/
120
121/-- The condition of `if ((state->wrap & 4) && out) strm->adler = state->check = UPDATE_CHECK(...)`. -/
122def chkCond (s : InflateState) (out : UInt32) : Bool := (s.wrap &&& 4) != 0 && out != 0
123
124/-- The stream record after the accounting of `CHECK`: `total_out += out` and, when the check is updated, `adler = v`. -/
125def chkZ (z : ZStream) (s : InflateState) (out : UInt32) (v : UInt64) : ZStream :=
126  { z with total_out := z.total_out + out.toUInt64, adler := if chkCond s out then v else z.adler }
127
128/-- The state record after the accounting of `CHECK`: `total += out` and, when the check is updated, `check = v`. -/
129def chkS (s : InflateState) (out : UInt32) (v : UInt64) : InflateState :=
130  { s with total := s.total + out.toUInt64, check := if chkCond s out then v else s.check }
131
132/-- The heap after the accounting of `CHECK`. -/
133def chkH (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (s : InflateState) (out : UInt32) (v : UInt64) : Heap :=
134  setI (r.put h (chkZ z s out v)) zs (chkS s out v)
135
136/-- `case CHECK:` with `wrap = 0`: no check; `state->mode = LENGTH` and the fall-through into `LENGTH`. -/
137theorem inflate_CHECK_nowrap {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {s : InflateState}
138    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hw : s.wrap = 0) :
139    runX (inflate_CHECK c) l h = runX (inflate_LENGTH c) l (setI h zs { s with mode := LENGTH }) := by
140  unfold inflate_CHECK
141  rw [hc]
142  simp [runX_bind, runX_lift, ldI_eq, hs, hw, setMode, wrI_eq, runX_pure]
143
144/-- `put` addresses the byte `off` of the block `blk` (bytes `a`), and the `out` bytes before it are inside the block. -/
145def PutAt (h : Heap) (put : BPtr) (out : UInt32) (blk off : Nat) (a : Array UInt8) : Prop :=
146  put = .ref (.blk blk) off ∧ h.bytes blk = some a ∧ out.toNat ≤ off ∧ off ≤ a.size
147
148/-- `case CHECK:` with `wrap ≠ 0`. `NEEDBITS(32)`; if the input ran out, `goto inf_leave` with the registers of that moment;
149else `out -= left` (`out` below), `total_out` and `total` grow by `out`, and when `(wrap & 4)` is set and `out ≠ 0` the check
150becomes `UPDATE_CHECK(check, put - out, out)` (`v`), also copied to `strm->adler`; then `out = left`; then when `(wrap & 4)` is set
151and the stream's check word (`hold`, byte-swapped for a zlib stream) differs from the check, the error "incorrect data check"
152(`BAD`, `break`); else `INITBITS`, `mode = LENGTH` and the fall-through into `LENGTH` (the theorems `inflate_LENGTH_*`).
153Precondition on the output: whenever the check is updated, `put` addresses a byte block with the `out` bytes written by this
154call just before it (`PutAt`), which holds in every state `inflate` reaches (`put = next_out + (out - left)` at the start of
155the call, advanced by one for every byte written). `v` is the value `UPDATE_CHECK` returns: the CRC-32 or the Adler-32 of those
156bytes (for Adler-32 and `out = 1` only when the old check is a canonical sum, true of every value `adler32` returns). -/
157theorem inflate_CHECK_run {c : Ctx} {l : IL} {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
158    {bs : List UInt8} (out : UInt32) (hout : out = l.out_ - l.left)
159    (hr : c.strm = some r) (hc : c.st = some (.tab zs)) (hz : r.get h = some z)
160    (hs : h.istates zs = some s) (hw : s.wrap ≠ 0) (B : BitInv h l bs) (hS : Zlib.Crc32.Proofs.StaticsOK h)
161    (hput : chkCond s out = true → ∃ blk off a, PutAt h l.put out blk off a) :
162    ∃ rr l' j, runX (NEEDBITS 32) l h = .ok ((rr, l'), h) ∧ j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
163      stream l' (bs.drop j) = stream l bs ∧
164      (rr = .error Ex.leave → l'.have_ = 0 ∧ j = bs.length ∧ l'.bits.toNat < 32 ∧
165        runX (inflate_CHECK c) l h = .ok ((.error Ex.leave, l'), h)) ∧
166      (rr = .ok () → 32 ≤ l'.bits.toNat ∧ ∃ v,
167        (chkCond s out = true → ∀ blk off a, PutAt h l.put out blk off a →
168          (s.flags ≠ 0 → v = (ZlibF.Spec.crc32Update s.check.toUInt32 ((a.toList.drop (off - out.toNat)).take out.toNat)).toUInt64) ∧
169          (s.flags = 0 → (out ≠ 1 ∨ (s.check >>> 16 &&& 65535).toNat < 65521) →
170            v.toNat = Zlib.Adler32.Spec.adler32 s.check.toNat (Zlib.Adler32.Proofs.seg a (off - out.toNat) out.toNat))) ∧
171        ((s.wrap &&& 4) ≠ 0 → (if s.flags ≠ 0 then l'.hold else ZSWAP32 l'.hold) ≠ (chkS s out v).check →
172          ∃ i, strTable[i]? = some "incorrect data check" ∧
173            runX (inflate_CHECK c) l h =
174              .ok ((.ok (), { l' with out_ := l.left }), tcBadHeap (chkH h r zs z s out v) r zs (chkZ z s out v) (chkS s out v) i)) ∧
175        (¬ ((s.wrap &&& 4) ≠ 0 ∧ (if s.flags ≠ 0 then l'.hold else ZSWAP32 l'.hold) ≠ (chkS s out v).check) →
176          runX (inflate_CHECK c) l h =
177            runX (inflate_LENGTH c) { l' with out_ := l.left, hold := 0, bits := 0 }
178              (setI (chkH h r zs z s out v) zs { chkS s out v with mode := LENGTH }))) := by
179  obtain ⟨rr, l', j, hrun, hj, B', hS', hbits, hshape, hmax, hid, hok, hleave⟩ := NEEDBITS_run B 32 (by decide)
180  have hw' : ¬ s.wrap = 0 := hw
181  have hput' : l'.put = l.put := by rw [hshape]
182  have hleft' : l'.left = l.left := by rw [hshape]
183  have hout' : l'.out_ = l.out_ := by rw [hshape]
184  refine ⟨rr, l', j, hrun, hj, B', hS', ?_, ?_⟩
185  · intro e
186    obtain ⟨h1, h2, h3⟩ := hleave e
187    refine ⟨h2, h1, h3, ?_⟩
188    unfold inflate_CHECK
189    rw [hc]
190    simp [runX_bind, runX_lift, ldI_eq, hs, hw', hrun, e, runX_throw]
191  · intro e
192    refine ⟨hok e, ?_⟩
193    by_cases hcond : chkCond s out = true
194    · obtain ⟨blk, off, a, hP⟩ := hput hcond
195      obtain ⟨hp, hb, ho1, ho2⟩ := hP
196      have hct' : chkCond s (l.out_ - l.left) = true := by rw [← hout]; exact hcond
197      have hct3 : ¬ s.wrap &&& 4 = 0 ∧ ¬ l.out_ - l.left = 0 := by
198        simpa [chkCond, ← hout] using hcond
199      -- the heap after `total_out += out; total += out`
200      let h1 : Heap := setI (r.put h { z with total_out := z.total_out + out.toUInt64 }) zs
201        { s with total := s.total + out.toUInt64 }
202      have hb1 : h1.bytes blk = some a := by simpa [h1] using hb
203      have hs1 : h1.istates zs = some { s with total := s.total + out.toUInt64 } := by simp [h1]
204      have hst1 : h1.static = h.static := by simp [h1, setI]
205      have hS1 : Zlib.Crc32.Proofs.StaticsOK h1 := by
206        unfold Zlib.Crc32.Proofs.StaticsOK at hS ⊢
207        rw [hst1]; exact hS
208      have hg1 : (Space.get h1 (BRef.blk blk) : Option (Array UInt8)) = some a := hb1
209      have hptr : Ptr.add l.put (-(out.toNat : Int)) h1 = .ok (.ref (.blk blk) (off - out.toNat), h1) := by
210        rw [hp]; exact Ptr.sub_nat_ok hg1 ho1 ho2
211      obtain ⟨v, hv, hvf, hva⟩ := UPDATE_CHECK_run (zs := zs) (blk := blk) (off := off - out.toNat) (a := a) (len := out)
212        hS1 hs1 hb1 (by omega) s.check
213      have hspec : ∀ blk' off' a', PutAt h l.put out blk' off' a' →
214          (s.flags ≠ 0 → v = (ZlibF.Spec.crc32Update s.check.toUInt32 ((a.toList.drop (off - out.toNat)).take out.toNat)).toUInt64) ∧
215          (s.flags = 0 → (out ≠ 1 ∨ (s.check >>> 16 &&& 65535).toNat < 65521) →
216            v.toNat = Zlib.Adler32.Spec.adler32 s.check.toNat (Zlib.Adler32.Proofs.seg a (off - out.toNat) out.toNat)) := by
217        intro blk' off' a' hP'
218        obtain ⟨hp', hb', -, -⟩ := hP'
219        rw [hp] at hp'
220        obtain ⟨e1, e2⟩ := Ptr.ref.inj hp'
221        have e1' := BRef.blk.inj e1
222        subst e1' e2
223        rw [hb] at hb'
224        cases hb'
225        exact ⟨hvf, hva⟩
226      have hptr2 := hptr
227      have hv2 := hv
228      simp [h1, hout] at hptr2 hv2
229      refine ⟨v, fun _ blk' off' a' hP' => ?_, ?_, ?_⟩
230      · have := hspec blk' off' a' hP'
231        obtain ⟨hp', hb', -, -⟩ := hP'
232        rw [hp] at hp'
233        obtain ⟨e1, e2⟩ := Ptr.ref.inj hp'
234        have e1' := BRef.blk.inj e1
235        subst e1' e2
236        rw [hb] at hb'
237        cases hb'
238        exact this
239      · intro hbad hne
240        have hz2 : r.get (chkH h r zs z s out v) = some (chkZ z s out v) := by
241          simp [chkH, hz]
242        have hs2 : (chkH h r zs z s out v).istates zs = some (chkS s out v) := by simp [chkH]
243        obtain ⟨i, hi, hbm⟩ := tcBadMode_run (c := c) "incorrect data check" lit_data_check hr hc hz2 hs2
244        refine ⟨i, hi, ?_⟩
245        simp [chkH, chkZ, chkS, tcBadHeap, hcond, hct', hout] at hbm
246        have hbad2 : (¬ s.wrap &&& 4 = 0 ∧ ¬ (if s.flags = 0 then ZSWAP32 l'.hold else l'.hold) = v) := by
247          refine ⟨hbad, ?_⟩
248          simp only [chkS, hcond, ↓reduceIte] at hne
249          by_cases hf0 : s.flags = 0
250          · rw [ite_eq_left hf0]
251            rw [ite_eq_right (by simpa using hf0)] at hne
252            exact hne
253          · rw [ite_eq_right hf0]
254            rw [ite_eq_left hf0] at hne
255            exact hne
256        unfold inflate_CHECK
257        rw [hc]
258        simp [runX_bind, runX_lift, ldI_eq, hs, hw', hrun, e, hr, runX_modify, runX_get, wrZ_eq, wrI_eq, hz,
259          hout, hout', hleft', runX_pure, hct3, hct', hbad2, setMode, runX_INITBITS, chkH, chkZ, chkS, hcond, hbm, chkCond,
260          hput', hptr2, hv2]
261        simp [tcBadHeap]
262      · intro hn
263        have hn2 : ¬ (¬ s.wrap &&& 4 = 0 ∧ ¬ (if s.flags = 0 then ZSWAP32 l'.hold else l'.hold) = v) := by
264          rintro ⟨ha, hb⟩
265          apply hn
266          refine ⟨ha, ?_⟩
267          simp only [chkS, hcond, ↓reduceIte]
268          by_cases hf0 : s.flags = 0
269          · rw [ite_eq_left hf0] at hb
270            rw [ite_eq_right (by simpa using hf0)]
271            exact hb
272          · rw [ite_eq_right hf0] at hb
273            rw [ite_eq_left hf0]
274            exact hb
275        have hn3 : (if s.flags = 0 then ZSWAP32 l'.hold else l'.hold) = v := by
276          by_cases hh : (if s.flags = 0 then ZSWAP32 l'.hold else l'.hold) = v
277          · exact hh
278          · exact absurd ⟨hct3.1, hh⟩ hn2
279        unfold inflate_CHECK
280        rw [hc]
281        simp [runX_bind, runX_lift, ldI_eq, hs, hw', hrun, e, hr, runX_modify, runX_get, wrZ_eq, wrI_eq, hz,
282          hout, hout', hleft', runX_pure, hct3, hct', hn3, setMode, runX_INITBITS, chkH, chkZ, chkS, hcond, chkCond,
283          hput', hptr2, hv2]
284    · have hcf : chkCond s out = false := by simpa using hcond
285      have hcf' : chkCond s (l.out_ - l.left) = false := by rw [← hout]; exact hcf
286      have hcf2 : ¬ ((s.wrap &&& 4) != 0 && (l.out_ - l.left) != 0) = true := by
287        simpa [chkCond, ← hout] using hcond
288      have hcf3 : ¬ (¬ s.wrap &&& 4 = 0 ∧ ¬ l.out_ - l.left = 0) := by
289        simpa [chkCond, ← hout] using hcond
290      refine ⟨s.check, fun h' => absurd h' hcond, ?_, ?_⟩
291      · intro hbad hne
292        have hz2 : r.get (chkH h r zs z s out s.check) = some (chkZ z s out s.check) := by
293          simp [chkH, hz]
294        have hs2 : (chkH h r zs z s out s.check).istates zs = some (chkS s out s.check) := by simp [chkH]
295        obtain ⟨i, hi, hbm⟩ := tcBadMode_run (c := c) "incorrect data check" lit_data_check hr hc hz2 hs2
296        refine ⟨i, hi, ?_⟩
297        have hcf4 : l.out_ - l.left = 0 := by
298          by_cases hz0 : l.out_ - l.left = 0
299          · exact hz0
300          · exact absurd ⟨hbad, hz0⟩ hcf3
301        simp [chkH, chkZ, chkS, tcBadHeap, hcf, hcf', hout, hcf4, chkCond] at hbm
302        have hbad2 : (¬ s.wrap &&& 4 = 0 ∧ ¬ (if s.flags = 0 then ZSWAP32 l'.hold else l'.hold) = s.check) := by
303          refine ⟨hbad, ?_⟩
304          simp only [chkS, hcf, Bool.false_eq_true, ↓reduceIte, ite_self] at hne
305          by_cases hf0 : s.flags = 0
306          · rw [ite_eq_left hf0]
307            rw [ite_eq_right (by simpa using hf0)] at hne
308            exact hne
309          · rw [ite_eq_right hf0]
310            rw [ite_eq_left hf0] at hne
311            exact hne
312        unfold inflate_CHECK
313        rw [hc]
314        simp [runX_bind, runX_lift, ldI_eq, hs, hw', hrun, e, hr, runX_modify, runX_get, wrZ_eq, wrI_eq, hz,
315          hout, hout', hleft', runX_pure, hcf3, hcf4, hcf', hbad2, setMode, runX_INITBITS, chkH, chkZ, chkS, hcf, hbm, chkCond]
316        simp [tcBadHeap]
317      · intro hn
318        have hn2 : ¬ (¬ s.wrap &&& 4 = 0 ∧ ¬ (if s.flags = 0 then ZSWAP32 l'.hold else l'.hold) = s.check) := by
319          rintro ⟨ha, hb⟩
320          apply hn
321          refine ⟨ha, ?_⟩
322          simp only [chkS, hcf, Bool.false_eq_true, ↓reduceIte]
323          by_cases hf0 : s.flags = 0
324          · rw [ite_eq_left hf0] at hb
325            rw [ite_eq_right (by simpa using hf0)]
326            exact hb
327          · rw [ite_eq_right hf0] at hb
328            rw [ite_eq_left hf0]
329            exact hb
330        unfold inflate_CHECK
331        rw [hc]
332        simp [runX_bind, runX_lift, ldI_eq, hs, hw', hrun, e, hr, runX_modify, runX_get, wrZ_eq, wrI_eq, hz, hcf2,
333          hout, hout', hleft', runX_pure, hcf3, hcf', hn2, setMode, runX_INITBITS, chkH, chkZ, chkS, hcf]
334
335end Zlib.Inflate.Proofs