inflate.c.init.lean

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

1import ZlibF.Proof.«inflate.c.reset»
2
3/-!
4# inflate.c: `inflateReset2`, `inflateInit2_`, `inflateInit_`, `inflateEnd`, `inflatePrime`
5-/
6
7namespace Zlib.Inflate.Spec
8open C
9
10/-- The window bits and wrapper a `windowBits` argument asks for, as `(wrap, wbits)`, and `none` when it is refused
11(`docs/spec/api/inflate-stream.md`): negative values (raw, `-15` to `-8`) have wrapper 0; 0 and 8 to 15 give
12wrapper 5, 16 and 24 to 31 give 6, 32 and 40 to 47 give 7; everything else is refused. -/
13def reset2Req (w : Int) : Option (Int × Int) :=
14  match (if w < 0 then (if w < -15 then none else some ((0 : Int), -w))
15         else some (w / 16 + 5, if w < 48 then w % 16 else w)) with
16  | none => none
17  | some (wrap, wb) => if wb ≠ 0 ∧ (wb < 8 ∨ 15 < wb) then none else some (wrap, wb)
18
19/-- The window bits are refused: not 0 and not 8 to 15. -/
20def badBits (wb : Int32) : Bool := wb != 0 && (wb < 8 || wb > 15)
21
22/-- The same computation on `int`, with the operations of the C (the arithmetic of `chkI32` never overflows here). -/
23def reset2Params (w : Int32) : Option (Int32 × Int32) :=
24  let check := fun (wrap wb : Int32) => if badBits wb then none else some (wrap, wb)
25  if w < 0 then (if w < -15 then none else check 0 (Int32.ofInt (-w.toInt)))
26  else check (Int32.ofInt ((w >>> 4).toInt + 5)) (if w < 48 then w &&& 15 else w)
27
28/-- The state record after `inflateReset2` made its changes and before `inflateReset` runs. -/
29def reset2Pre (wrap wb : Int32) (st : InflateState) : InflateState :=
30  { (if st.wbits != Zlib.Inflate.i2u wb then { st with window := .null } else st) with
31    wrap := wrap, reqwrap := wrap, wbits := Zlib.Inflate.i2u wb, reqbits := Zlib.Inflate.i2u wb }
32
33/-- The heap after the window was freed, if `inflateReset2` frees it. -/
34def reset2Heap (h : Heap) (wb : Int32) (st : InflateState) : Heap :=
35  if st.wbits != Zlib.Inflate.i2u wb then freeWin h st.window else h
36
37end Zlib.Inflate.Spec
38
39namespace Zlib.Inflate.Proofs
40open C Zlib.Inflate Zlib.Inflate.Spec
41
42theorem int32_shr4 (w : Int32) : (w >>> 4).toInt = w.toInt / 16 := by
43  have : (w >>> 4) = ⟨⟨BitVec.sshiftRight' w.toBitVec ((4 : Int32).toBitVec.smod 32)⟩⟩ := rfl
44  rw [this]
45  show (BitVec.sshiftRight' w.toBitVec ((4 : Int32).toBitVec.smod 32)).toInt = _
46  rw [BitVec.toInt_sshiftRight', Int.shiftRight_eq_div_pow]
47  have h4 : ((4 : Int32).toBitVec.smod 32).toNat = 4 := by decide
48  rw [h4]
49  rfl
50
51theorem int32_neg (w : Int32) (h1 : -15 ≤ w.toInt) (h2 : w.toInt < 0) : (-w).toInt = - w.toInt := by
52  rw [Int32.toInt_neg]
53  have := w.toInt_lt
54  have := w.le_toInt
55  rw [Int.bmod_eq_of_le (by omega) (by omega)]
56
57/-- `int` constants of the C, as integers. -/
58theorem int32_ofInt_toInt (k : Int) (h1 : -2147483648 ≤ k) (h2 : k < 2147483648) : (Int32.ofInt k).toInt = k := by
59  rw [Int32.toInt_ofInt]
60  simp only [Int32.size]
61  exact Int.bmod_eq_of_le (by omega) (by omega)
62
63
64theorem chkI32_ok {v : Int} (h1 : -2147483648 ≤ v) (h2 : v < 2147483648) : chkI32 v = pure (Int32.ofInt v) := by
65  simp [chkI32, h1, h2]
66
67theorem int32_lt_zero (w : Int32) : w < 0 ↔ w.toInt < 0 := by
68  rw [Int32.lt_iff_toInt_lt]; rfl
69
70theorem int32_lt_c (w : Int32) (k : Int) (hk : -2147483648 ≤ k) (hk2 : k < 2147483648) :
71    w < Int32.ofInt k ↔ w.toInt < k := by
72  rw [Int32.lt_iff_toInt_lt, int32_ofInt_toInt k hk hk2]
73
74theorem reset2_head_ok {w : Int32} (hw : ¬ w < -15) (hn : w < 0) :
75    chkI32 (-(w.toInt)) = pure (Int32.ofInt (-w.toInt)) := by
76  have h1 := w.le_toInt
77  have h2 := (int32_lt_zero w).1 hn
78  have h3 : -15 ≤ w.toInt := by
79    by_cases hc : w.toInt < -15
80    · exfalso
81      apply hw
82      have : (-15 : Int32) = Int32.ofInt (-15) := rfl
83      rw [this, int32_lt_c w (-15) (by omega) (by omega)]
84      exact hc
85    · omega
86  exact chkI32_ok (by omega) (by omega)
87
88theorem reset2_wrap_ok (w : Int32) : chkI32 ((w >>> 4).toInt + 5) = pure (Int32.ofInt ((w >>> 4).toInt + 5)) := by
89  have := w.le_toInt
90  have := w.toInt_lt
91  rw [int32_shr4]
92  exact chkI32_ok (by omega) (by omega)
93
94
95theorem reset2_okB {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
96    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : WindowOk h st.window) {w : Int32}
97    (h1 : w < 0) (h2 : ¬ w < -15) (hb : badBits (-w) = false) :
98    inflateReset2 (some r) w h = .ok (Z_OK, setI (r.put (reset2Heap h (-w) st)
99      (resetKeepStream z (resetPre (reset2Pre (0) (-w) st)))) zs (resetKeepState zs (resetPre (reset2Pre (0) (-w) st)))) := by
100  have hz := hL.hz
101  have hs := hL.hs
102  have hb' : ¬ (¬ w = 0 ∧ (-w < 8 ∨ 15 < -w)) := by simpa [badBits] using hb
103  unfold inflateReset2
104  by_cases hne : st.wbits = i2u (-w)
105  · isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_head_ok h2 h1, hb', hne]
106    rw [inflateReset_run]
107    rotate_left
108    · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
109    · exact hf
110    · exact Or.inl rfl
111    · have e : reset2Heap h (-w) st = h := by simp [reset2Heap, hne]
112      rw [e]
113      simp [resetHeap, resetPre, reset2Pre, hne, resetKeepState, resetKeepStream]
114  · by_cases hw : st.window = .null
115    · isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_head_ok h2 h1, hb', hne, hw]
116      rw [inflateReset_run]
117      rotate_left
118      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
119      · exact hf
120      · exact Or.inl rfl
121      · have e : reset2Heap h (-w) st = h := by simp [reset2Heap, hne, hw, freeWin_null]
122        rw [e]
123        simp [resetHeap, resetPre, reset2Pre, hne, hw, resetKeepState, resetKeepStream]
124    · obtain ⟨b, a, hb0, hba, hro⟩ : ∃ b a, st.window = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false := by
125        rcases hwo with hn | hb
126        · exact absurd hn hw
127        · exact hb
128      isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_head_ok h2 h1, hb', hne, hw, zfreeB_run hz hf (Or.inr ⟨b, a, hb0, hba, hro⟩)]
129      rw [inflateReset_run]
130      rotate_left
131      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
132      · exact hf
133      · exact Or.inl rfl
134      · simp [resetHeap, resetPre, reset2Pre, reset2Heap, hne, hw, resetKeepState, resetKeepStream]
135
136theorem reset2_okC1 {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
137    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : WindowOk h st.window) {w : Int32}
138    (h1 : ¬ w < 0) (h2 : w < 48) (hb : badBits (w &&& 15) = false) :
139    inflateReset2 (some r) w h = .ok (Z_OK, setI (r.put (reset2Heap h (w &&& 15) st)
140      (resetKeepStream z (resetPre (reset2Pre (Int32.ofInt ((w >>> 4).toInt + 5)) (w &&& 15) st)))) zs (resetKeepState zs (resetPre (reset2Pre (Int32.ofInt ((w >>> 4).toInt + 5)) (w &&& 15) st)))) := by
141  have hz := hL.hz
142  have hs := hL.hs
143  have hb' : ¬ (¬ w &&& 15 = 0 ∧ (w &&& 15 < 8 ∨ 15 < w &&& 15)) := by simpa [badBits] using hb
144  unfold inflateReset2
145  by_cases hne : st.wbits = i2u (w &&& 15)
146  · isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb', hne]
147    rw [inflateReset_run]
148    rotate_left
149    · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
150    · exact hf
151    · exact Or.inl rfl
152    · have e : reset2Heap h (w &&& 15) st = h := by simp [reset2Heap, hne]
153      rw [e]
154      simp [resetHeap, resetPre, reset2Pre, hne, resetKeepState, resetKeepStream]
155  · by_cases hw : st.window = .null
156    · isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb', hne, hw]
157      rw [inflateReset_run]
158      rotate_left
159      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
160      · exact hf
161      · exact Or.inl rfl
162      · have e : reset2Heap h (w &&& 15) st = h := by simp [reset2Heap, hne, hw, freeWin_null]
163        rw [e]
164        simp [resetHeap, resetPre, reset2Pre, hne, hw, resetKeepState, resetKeepStream]
165    · obtain ⟨b, a, hb0, hba, hro⟩ : ∃ b a, st.window = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false := by
166        rcases hwo with hn | hb
167        · exact absurd hn hw
168        · exact hb
169      isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb', hne, hw, zfreeB_run hz hf (Or.inr ⟨b, a, hb0, hba, hro⟩)]
170      rw [inflateReset_run]
171      rotate_left
172      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
173      · exact hf
174      · exact Or.inl rfl
175      · simp [resetHeap, resetPre, reset2Pre, reset2Heap, hne, hw, resetKeepState, resetKeepStream]
176
177theorem reset2_okC2 {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
178    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : WindowOk h st.window) {w : Int32}
179    (h1 : ¬ w < 0) (h2 : ¬ w < 48) (hb : badBits w = false) :
180    inflateReset2 (some r) w h = .ok (Z_OK, setI (r.put (reset2Heap h (w) st)
181      (resetKeepStream z (resetPre (reset2Pre (Int32.ofInt ((w >>> 4).toInt + 5)) (w) st)))) zs (resetKeepState zs (resetPre (reset2Pre (Int32.ofInt ((w >>> 4).toInt + 5)) (w) st)))) := by
182  have hz := hL.hz
183  have hs := hL.hs
184  have hb' : ¬ (¬ w = 0 ∧ (w < 8 ∨ 15 < w)) := by simpa [badBits] using hb
185  unfold inflateReset2
186  by_cases hne : st.wbits = i2u (w)
187  · isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb', hne]
188    rw [inflateReset_run]
189    rotate_left
190    · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
191    · exact hf
192    · exact Or.inl rfl
193    · have e : reset2Heap h (w) st = h := by simp [reset2Heap, hne]
194      rw [e]
195      simp [resetHeap, resetPre, reset2Pre, hne, resetKeepState, resetKeepStream]
196  · by_cases hw : st.window = .null
197    · isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb', hne, hw]
198      rw [inflateReset_run]
199      rotate_left
200      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
201      · exact hf
202      · exact Or.inl rfl
203      · have e : reset2Heap h (w) st = h := by simp [reset2Heap, hne, hw, freeWin_null]
204        rw [e]
205        simp [resetHeap, resetPre, reset2Pre, hne, hw, resetKeepState, resetKeepStream]
206    · obtain ⟨b, a, hb0, hba, hro⟩ : ∃ b a, st.window = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false := by
207        rcases hwo with hn | hb
208        · exact absurd hn hw
209        · exact hb
210      isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb', hne, hw, zfreeB_run hz hf (Or.inr ⟨b, a, hb0, hba, hro⟩)]
211      rw [inflateReset_run]
212      rotate_left
213      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
214      · exact hf
215      · exact Or.inl rfl
216      · simp [resetHeap, resetPre, reset2Pre, reset2Heap, hne, hw, resetKeepState, resetKeepStream]
217
218
219theorem reset2_errA {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
220    (hL : Live h r zs z st) {w : Int32} (h1 : w < 0) (h2 : w < -15) :
221    inflateReset2 (some r) w h = .ok (Z_STREAM_ERROR, h) := by
222  have hz := hL.hz
223  have hs := hL.hs
224  unfold inflateReset2
225  isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2]
226
227theorem reset2_errB {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
228    (hL : Live h r zs z st) {w : Int32} (h1 : w < 0) (h2 : ¬ w < -15) (hb : badBits (-w) = true) :
229    inflateReset2 (some r) w h = .ok (Z_STREAM_ERROR, h) := by
230  have hz := hL.hz
231  have hs := hL.hs
232  have hb' : (¬ w = 0 ∧ (-w < 8 ∨ 15 < -w)) := by simpa [badBits] using hb
233  unfold inflateReset2
234  isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_head_ok h2 h1, hb']
235
236theorem reset2_errC1 {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
237    (hL : Live h r zs z st) {w : Int32} (h1 : ¬ w < 0) (h2 : w < 48) (hb : badBits (w &&& 15) = true) :
238    inflateReset2 (some r) w h = .ok (Z_STREAM_ERROR, h) := by
239  have hz := hL.hz
240  have hs := hL.hs
241  have hb' : (¬ w &&& 15 = 0 ∧ (w &&& 15 < 8 ∨ 15 < w &&& 15)) := by simpa [badBits] using hb
242  unfold inflateReset2
243  isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb']
244
245theorem reset2_errC2 {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
246    (hL : Live h r zs z st) {w : Int32} (h1 : ¬ w < 0) (h2 : ¬ w < 48) (hb : badBits w = true) :
247    inflateReset2 (some r) w h = .ok (Z_STREAM_ERROR, h) := by
248  have hz := hL.hz
249  have hs := hL.hs
250  have hb' : (¬ w = 0 ∧ (w < 8 ∨ 15 < w)) := by simpa [badBits] using hb
251  unfold inflateReset2
252  isimp [stateCheck_live hL, hL.zst, hz, hs, h1, h2, reset2_wrap_ok w, hb']
253
254/-- **inflateReset2, evaluation.** For an initialised stream, `inflateReset2` refuses exactly the `windowBits` for which
255`reset2Params` is `none` (`Z_STREAM_ERROR`, nothing changed) and otherwise returns `Z_OK` with the heap `reset2Heap` and
256the records `resetKeepStream`/`resetKeepState` of `resetPre (reset2Pre wrap wb st)`. -/
257theorem inflateReset2_run {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
258    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : WindowOk h st.window) (w : Int32) :
259    match reset2Params w with
260    | none => inflateReset2 (some r) w h = .ok (Z_STREAM_ERROR, h)
261    | some (wrap, wb) => badBits wb = false ∧ inflateReset2 (some r) w h = .ok (Z_OK, setI (r.put (reset2Heap h wb st)
262        (resetKeepStream z (resetPre (reset2Pre wrap wb st)))) zs (resetKeepState zs (resetPre (reset2Pre wrap wb st)))) := by
263  cases hp : reset2Params w with
264  | none =>
265    simp only [hp]
266    unfold reset2Params at hp
267    by_cases h1 : w < 0
268    · by_cases h2 : w < -15
269      · exact reset2_errA hL h1 h2
270      · have e : Int32.ofInt (-w.toInt) = -w := by simp
271        simp only [h1, h2, ite_true, ite_false, e] at hp
272        have hb : badBits (-w) = true := by
273          by_cases hb : badBits (-w) = true
274          · exact hb
275          · simp [hb] at hp
276        exact reset2_errB hL h1 h2 hb
277    · by_cases h2 : w < 48
278      · simp only [h1, h2, ite_true, ite_false] at hp
279        have hb : badBits (w &&& 15) = true := by
280          by_cases hb : badBits (w &&& 15) = true
281          · exact hb
282          · simp [hb] at hp
283        exact reset2_errC1 hL h1 h2 hb
284      · simp only [h1, h2, ite_true, ite_false] at hp
285        have hb : badBits w = true := by
286          by_cases hb : badBits w = true
287          · exact hb
288          · simp [hb] at hp
289        exact reset2_errC2 hL h1 h2 hb
290  | some p =>
291    obtain ⟨wrap, wb⟩ := p
292    simp only [hp]
293    unfold reset2Params at hp
294    by_cases h1 : w < 0
295    · by_cases h2 : w < -15
296      · simp [h1, h2] at hp
297      · have e : Int32.ofInt (-w.toInt) = -w := by simp
298        simp only [h1, h2, ite_true, ite_false, e] at hp
299        have hb : badBits (-w) = false := by
300          by_cases hb : badBits (-w) = true
301          · simp [hb] at hp
302          · simpa using hb
303        simp only [hb, Bool.false_eq_true, ite_false, Option.some.injEq, Prod.mk.injEq] at hp
304        obtain ⟨rfl, rfl⟩ := hp
305        exact ⟨hb, reset2_okB hL hf hwo h1 h2 hb⟩
306    · by_cases h2 : w < 48
307      · simp only [h1, h2, ite_true, ite_false] at hp
308        have hb : badBits (w &&& 15) = false := by
309          by_cases hb : badBits (w &&& 15) = true
310          · simp [hb] at hp
311          · simpa using hb
312        simp only [hb, Bool.false_eq_true, ite_false, Option.some.injEq, Prod.mk.injEq] at hp
313        obtain ⟨rfl, rfl⟩ := hp
314        exact ⟨hb, reset2_okC1 hL hf hwo h1 h2 hb⟩
315      · simp only [h1, h2, ite_true, ite_false] at hp
316        have hb : badBits w = false := by
317          by_cases hb : badBits w = true
318          · simp [hb] at hp
319          · simpa using hb
320        simp only [hb, Bool.false_eq_true, ite_false, Option.some.injEq, Prod.mk.injEq] at hp
321        obtain ⟨rfl, rfl⟩ := hp
322        exact ⟨hb, reset2_okC2 hL hf hwo h1 h2 hb⟩
323
324
325theorem strm_pre (wrap wb : Int32) (st : InflateState) : (resetPre (reset2Pre wrap wb st)).strm = st.strm := by
326  unfold resetPre reset2Pre
327  repeat' split
328  all_goals rfl
329
330theorem bits15 {wb : Int32} (hb : badBits wb = false) : (i2u wb).toNat ≤ 15 := by
331  have hb' : ¬ (¬ wb = 0 ∧ (wb < 8 ∨ 15 < wb)) := by simpa [badBits] using hb
332  by_cases h0 : wb = 0
333  · subst h0; decide
334  · have h1 : ¬ wb < 8 := fun h => hb' ⟨h0, Or.inl h⟩
335    have h2 : ¬ 15 < wb := fun h => hb' ⟨h0, Or.inr h⟩
336    have h1' : ¬ wb < Int32.ofInt 8 := h1
337    have h2' : ¬ Int32.ofInt 15 < wb := h2
338    rw [int32_lt_c wb 8 (by omega) (by omega)] at h1'
339    rw [Int32.lt_iff_toInt_lt, int32_ofInt_toInt 15 (by omega) (by omega)] at h2'
340    have hlo := wb.le_toInt
341    have hhi := wb.toInt_lt
342    obtain ⟨k, hk⟩ : ∃ k, k = wb.toInt := ⟨_, rfl⟩
343    have hw : wb = Int32.ofInt k := by rw [hk]; exact (Int32.ofInt_toInt wb).symm
344    have hk1 : 8 ≤ k := by omega
345    have hk2 : k ≤ 15 := by omega
346    rw [hw]
347    have hc : k = 8 ∨ k = 9 ∨ k = 10 ∨ k = 11 ∨ k = 12 ∨ k = 13 ∨ k = 14 ∨ k = 15 := by omega
348    rcases hc with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
349
350theorem winInv_reset2 {h : Heap} {st : InflateState} (hW : WinInv h st) {wb : Int32} (hb : (i2u wb).toNat ≤ 15) (wrap : Int32) :
351    WinInv (reset2Heap h wb st) (resetPre (reset2Pre wrap wb st)) := by
352  by_cases hne : st.wbits = i2u wb
353  · have e : reset2Heap h wb st = h := by simp [reset2Heap, hne]
354    rw [e]
355    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
356    · simpa [resetPre, reset2Pre, hne] using hb
357    · have := hW.block
358      rw [hne] at this
359      simpa [resetPre, reset2Pre, hne] using this
360    · intro _; simp [resetPre, reset2Pre, hne]
361    · simp [resetPre, reset2Pre, hne]
362    · simp [resetPre, reset2Pre, hne]
363    · simp [resetPre, reset2Pre, hne]
364    · intro hh; simp [resetPre, reset2Pre, hne] at hh
365  · refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
366    · simpa [resetPre, reset2Pre, hne] using hb
367    · left; simp [resetPre, reset2Pre, hne]
368    · intro _; simp [resetPre, reset2Pre, hne]
369    · simp [resetPre, reset2Pre, hne]
370    · simp [resetPre, reset2Pre, hne]
371    · simp [resetPre, reset2Pre, hne]
372    · intro hh; simp [resetPre, reset2Pre, hne] at hh
373
374theorem reset2Heap_owns {h : Heap} {st : InflateState} (hU : Uniq h) (hW : WinInv h st) {wb : Int32} {S : Nat → Prop}
375    (hO : h.Owns S) : (reset2Heap h wb st).Owns (fun b => S b ∧ ¬ (st.wbits ≠ i2u wb ∧ WinBlk st b)) := by
376  have e : reset2Heap h wb st = resetHeap h { st with reqbits := i2u wb } := by simp [reset2Heap, resetHeap]
377  rw [e]
378  exact resetHeap_owns (st := { st with reqbits := i2u wb }) hU ⟨hW.wbits, hW.block, hW.nullws, hW.ws, hW.hv, hW.wn, hW.eq⟩ hO
379
380theorem uniq_reset2Heap {h : Heap} (hU : Uniq h) (wb : Int32) (st : InflateState) : Uniq (reset2Heap h wb st) := by
381  unfold reset2Heap; split
382  · exact uniq_freeWin hU _
383  · exact hU
384
385theorem fresh_reset2Heap {h : Heap} (hF : Fresh h) (wb : Int32) (st : InflateState) : Fresh (reset2Heap h wb st) := by
386  unfold reset2Heap; split
387  · exact fresh_freeWin hF _
388  · exact hF
389
390
391/-- **inflateReset2, safety.** On an initialised stream with the default `zfree`, for every `windowBits`: the call never
392faults. A refused value (`reset2Params w = none`) gives `Z_STREAM_ERROR` and changes nothing. An accepted value gives
393`Z_OK`; the window is freed if its size differs from the new one (nothing else is allocated or freed); the stream is
394initialised again with the invariants intact; the live blocks are the old ones minus the window block that was freed. -/
395theorem inflateReset2_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
396    (hG : Good h r zs z st) (hf : z.zfree = .fn "zcfree") (w : Int32) :
397    ∃ v h', C.run (inflateReset2 (some r) w) h = .ok (v, h') ∧
398      (match reset2Params w with
399       | none => v = Z_STREAM_ERROR ∧ h' = h
400       | some (wrap, wb) => v = Z_OK ∧
401          h' = setI (r.put (reset2Heap h wb st) (resetKeepStream z (resetPre (reset2Pre wrap wb st)))) zs
402            (resetKeepState zs (resetPre (reset2Pre wrap wb st))) ∧
403          Good h' r zs (resetKeepStream z (resetPre (reset2Pre wrap wb st))) (resetKeepState zs (resetPre (reset2Pre wrap wb st))) ∧
404          (∀ S, h.Owns S → h'.Owns (fun b => S b ∧ ¬ (st.wbits ≠ i2u wb ∧ WinBlk st b)))) := by
405  have hL := hG.live
406  have hrun := inflateReset2_run hL hf (windowBlock hG.inv.win) w
407  cases hp : reset2Params w with
408  | none =>
409    rw [hp] at hrun
410    exact ⟨_, _, hrun, rfl, rfl⟩
411  | some p =>
412    obtain ⟨wrap, wb⟩ := p
413    rw [hp] at hrun
414    obtain ⟨hb, hrun⟩ := hrun
415    have hU := uniq_reset2Heap hG.uniq wb st
416    have hF := fresh_reset2Heap hG.fresh wb st
417    have hz0 : r.get (reset2Heap h wb st) = some z := by unfold reset2Heap; split <;> simp [hL.hz]
418    have hs0 : (reset2Heap h wb st).istates zs = some st := by unfold reset2Heap; split <;> simp [hL.hs]
419    have hw := winInv_reset2 hG.inv.win (bits15 hb) wrap
420    have hI : StInv (reset2Heap h wb st) zs (resetKeepState zs (resetPre (reset2Pre wrap wb st))) := by
421      refine ⟨?_, ?_, ?_, by simp [resetKeepState], ?_⟩
422      · exact wf_resetKeepState (wf_resetPre (by unfold reset2Pre; split <;> exact hG.inv.wf))
423      · exact ⟨hw.wbits, hw.block, hw.nullws, hw.ws, hw.hv, hw.wn, hw.eq⟩
424      · simpa [resetKeepState, reqbits_resetPre, reset2Pre] using bits15 hb
425      · refine (StInv.resetKeep (st := resetPre (reset2Pre wrap wb st)) ⟨?_, hw, ?_, ?_, ?_⟩).ptr
426        · exact wf_resetPre (by unfold reset2Pre; split <;> exact hG.inv.wf)
427        · simpa [reqbits_resetPre, reset2Pre] using bits15 hb
428        · exact bits_resetPre (by unfold reset2Pre; split <;> exact hG.inv.bits)
429        · exact ptr_resetPre (by unfold reset2Pre; split <;> exact hG.inv.ptr)
430    refine ⟨_, _, hrun, rfl, rfl, ?_, ?_⟩
431    · refine good_set hz0 hs0 hU hF (by simp [resetKeepStream, hL.zst]) (by simpa [resetKeepStream] using hL.zalloc)
432        (by simpa [resetKeepStream] using hL.zfree)
433        (by simpa [resetKeepState, strm_pre] using hL.back)
434        (by simpa [resetKeepState] using mode_head) hI
435    · intro S hO
436      have hO' := reset2Heap_owns (wb := wb) hG.uniq hG.inv.win hO
437      exact ((shape_put hz0 _).trans (shape_setI (by simpa using hs0) _)).owns hO'
438
439end Zlib.Inflate.Proofs