inflate.c.uw.lean

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

1import ZlibF.Proof.«inflate.c.window»
2
3/-!
4# inflate.c: `updatewindow`
5
6Safety of `updatewindow` on the real translation. The window is a ring buffer; the copy is done in at most two
7pieces (`uwPost`). The proofs cover `copy >= wsize`, a copy that fits, a copy that wraps,
8and a copy that ends at the end of the window.
9-/
10
11namespace Zlib.Inflate.Spec
12open C
13
14/-- The window block and the state record after `updatewindow` copied `copy` bytes that end at offset `eo` of the
15buffer `ebytes` into the ring buffer `a` of the state `st` (whose `wsize` is already set): the ring buffer is
16filled in at most two pieces, as in `inflate.c`. -/
17def uwPost (st : InflateState) (a ebytes : Array UInt8) (eo : Nat) (copy : UInt32) : Array UInt8 × InflateState :=
18  if st.wsize ≤ copy then
19    (copyRange a ebytes 0 (eo - st.wsize.toNat) st.wsize.toNat, { st with wnext := 0, whave := st.wsize })
20  else if st.wsize - st.wnext > copy then
21    (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) copy.toNat,
22      { st with
23        wnext := if st.wnext + copy == st.wsize then 0 else st.wnext + copy,
24        whave := if st.whave < st.wsize then st.whave + copy else st.whave })
25  else if copy - (st.wsize - st.wnext) ≠ 0 then
26    (copyRange (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)
27        ebytes 0 (eo - (copy - (st.wsize - st.wnext)).toNat) (copy - (st.wsize - st.wnext)).toNat,
28      { st with wnext := copy - (st.wsize - st.wnext), whave := st.wsize })
29  else
30    (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat,
31      { st with wnext := 0, whave := if st.whave < st.wsize then st.whave + (st.wsize - st.wnext) else st.whave })
32
33end Zlib.Inflate.Spec
34
35namespace Zlib.Inflate.Proofs
36open C Zlib.Inflate Zlib.Inflate.Spec
37
38/-- `updatewindow`, first branch (`copy >= wsize`) on a state whose window exists and whose `wsize` is set. -/
39theorem uw_core_big {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
40    {a ebytes : Array UInt8} {copy : UInt32}
41    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
42    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size)
43    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : st.wsize.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
44    (hbig : st.wsize ≤ copy) :
45    updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, setI
46      { H with bytes := upd H.bytes w (some (copyRange a ebytes 0 (eo - st.wsize.toNat) st.wsize.toNat)) } zs
47      { st with wnext := 0, whave := st.wsize }) := by
48  have hz := hL.hz
49  have hs := hL.hs
50  have hwn : (st.window == Ptr.null) = false := by rw [hw]; simp
51  have hws0 : (st.wsize == 0) = false := by simpa using hpos
52  have hn1 : OkOn H (Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(st.wsize.toNat : Int))) (Ptr.ref (BRef.blk eb) (eo - st.wsize.toNat)) :=
53    Ptr.sub_nat_ok (a := ebytes) (by simpa using heb) hc hoff
54  have hcp := memcpyB_blk_ok (nb := w) (no := 0) (pb := eb) (po := eo - st.wsize.toNat) (n := st.wsize.toNat)
55    (h := H) ha heb hro hne (by omega) (by omega)
56  unfold updatewindow
57  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, wrI_eq, hz, hL.zst, castI, hs, hwn, hws0, Bool.false_eq_true, ite_false]
58  have hn1' : Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(st.wsize.toNat : Int)) H = .ok (Ptr.ref (BRef.blk eb) (eo - st.wsize.toNat), H) := hn1
59  simp only [ge_iff_le, hbig, ite_true, bind_app, hw, hn1']
60  simp only [hcp, wrI_eq, pure_app, hs]
61  simp only [hw]
62
63/-- `updatewindow`, `copy < wsize`, the copy fits before the end of the window (`wsize - wnext > copy`). -/
64theorem uw_core_small1 {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
65    {a ebytes : Array UInt8} {copy : UInt32}
66    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
67    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size) (hwn : st.wnext.toNat < st.wsize.toNat)
68    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
69    (hlt : ¬ st.wsize ≤ copy) (hP : st.wsize - st.wnext > copy) :
70    updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, setI
71      { H with bytes := upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) copy.toNat)) } zs
72      { st with
73        wnext := if st.wnext + copy == st.wsize then 0 else st.wnext + copy,
74        whave := if st.whave < st.wsize then st.whave + copy else st.whave }) := by
75  have hz := hL.hz
76  have hs := hL.hs
77  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
78  have hws0 : (st.wsize == 0) = false := by simpa using hpos
79  have hPn : copy.toNat < st.wsize.toNat - st.wnext.toNat := by
80    have := UInt32.lt_iff_toNat_lt.mp hP
81    rwa [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)] at this
82  have hn0 : OkOn H (Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int)) (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat)) :=
83    Ptr.add_nat_ok (a := a) (by simpa using ha) (by omega)
84  have hn1 : OkOn H (Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(copy.toNat : Int))) (Ptr.ref (BRef.blk eb) (eo - copy.toNat)) :=
85    Ptr.sub_nat_ok (a := ebytes) (by simpa using heb) hc hoff
86  have hcp := memcpyB_blk_ok (nb := w) (no := 0 + st.wnext.toNat) (pb := eb) (po := eo - copy.toNat) (n := copy.toNat)
87    (h := H) ha heb hro hne (by omega) (by omega)
88  have hn0' : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) H = .ok (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat), H) := hn0
89  have hn1' : Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(copy.toNat : Int)) H = .ok (Ptr.ref (BRef.blk eb) (eo - copy.toNat), H) := hn1
90  simp only [Nat.zero_add] at hcp hn0'
91  unfold updatewindow
92  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, hwnl, hws0, Bool.false_eq_true, ite_false]
93  simp only [ge_iff_le, hlt, ite_false, hP, ite_true, bind_app, hw, hn0', hn1', UInt32.sub_self, bne_self_eq_false, Bool.false_eq_true]
94  simp only [hcp, wrI_eq, pure_app, hs]
95  by_cases c1 : st.wnext + copy = st.wsize <;> by_cases c2 : st.whave < st.wsize <;> simp [c1, c2, wrI_eq, hs, setI, hw]
96
97/-- `updatewindow`, `copy < wsize`, the copy reaches or passes the end of the window, it wraps (second piece). -/
98theorem uw_core_small2 {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
99    {a ebytes : Array UInt8} {copy : UInt32}
100    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
101    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size) (hwn : st.wnext.toNat < st.wsize.toNat)
102    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
103    (hlt : ¬ st.wsize ≤ copy) (hQ : ¬ st.wsize - st.wnext > copy) (hR : copy - (st.wsize - st.wnext) ≠ 0) :
104    updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, setI
105      { H with bytes := upd H.bytes w (some (copyRange (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)
106          ebytes 0 (eo - (copy - (st.wsize - st.wnext)).toNat) (copy - (st.wsize - st.wnext)).toNat)) } zs
107      { st with wnext := copy - (st.wsize - st.wnext), whave := st.wsize }) := by
108  have hz := hL.hz
109  have hs := hL.hs
110  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
111  have hws0 : (st.wsize == 0) = false := by simpa using hpos
112  have hD : (st.wsize - st.wnext).toNat = st.wsize.toNat - st.wnext.toNat :=
113    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)
114  have hQn : st.wsize.toNat - st.wnext.toNat ≤ copy.toNat := by
115    have : ¬ copy < st.wsize - st.wnext := hQ
116    rw [UInt32.lt_iff_toNat_lt, hD] at this; omega
117  have hRn : (copy - (st.wsize - st.wnext)).toNat = copy.toNat - (st.wsize.toNat - st.wnext.toNat) := by
118    rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le, hD]; omega), hD]
119  have hlt' : copy.toNat < st.wsize.toNat := by
120    have : ¬ st.wsize ≤ copy := hlt
121    rw [UInt32.le_iff_toNat_le] at this; omega
122  have hRpos : 0 < (copy - (st.wsize - st.wnext)).toNat := by
123    have : (copy - (st.wsize - st.wnext)).toNat ≠ 0 := fun e => hR (UInt32.toNat_inj.mp (by simpa using e))
124    omega
125  have hn0 : OkOn H (Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int)) (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat)) :=
126    Ptr.add_nat_ok (a := a) (by simpa using ha) (by omega)
127  have hn1 : OkOn H (Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(copy.toNat : Int))) (Ptr.ref (BRef.blk eb) (eo - copy.toNat)) :=
128    Ptr.sub_nat_ok (a := ebytes) (by simpa using heb) hc hoff
129  have hcp1 := memcpyB_blk_ok (nb := w) (no := 0 + st.wnext.toNat) (pb := eb) (po := eo - copy.toNat)
130    (n := (st.wsize - st.wnext).toNat) (h := H) ha heb hro hne (by omega) (by omega)
131  have hn2 : OkOn H (Ptr.add (Ptr.ref (BRef.blk eb) eo) (-((copy - (st.wsize - st.wnext)).toNat : Int)))
132      (Ptr.ref (BRef.blk eb) (eo - (copy - (st.wsize - st.wnext)).toNat)) :=
133    Ptr.sub_nat_ok (a := ebytes) (by simpa using heb) (by omega) hoff
134  have hn0' : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) H = .ok (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat), H) := hn0
135  have hn1' : Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(copy.toNat : Int)) H = .ok (Ptr.ref (BRef.blk eb) (eo - copy.toNat), H) := hn1
136  simp only [Nat.zero_add] at hcp1 hn0'
137  unfold updatewindow
138  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, hwnl, hws0, Bool.false_eq_true, ite_false]
139  simp only [ge_iff_le, hlt, ite_false, hQ, bind_app, hw, hn0', hn1', hcp1]
140  have hne' : ¬ (copy - (st.wsize - st.wnext) = 0) := hR
141  have hA1 : (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat).size = a.size := size_copyRange ..
142  have hbm : ({ H with bytes := upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)) } : Heap).bytes eb = some ebytes := by
143    simp [upd_ne _ _ _ _ hne.symm, heb]
144  have hn2m : Ptr.add (Ptr.ref (BRef.blk eb) eo) (-((copy - (st.wsize - st.wnext)).toNat : Int))
145      { H with bytes := upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)) } =
146      .ok (Ptr.ref (BRef.blk eb) (eo - (copy - (st.wsize - st.wnext)).toNat), { H with bytes := upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)) }) :=
147    Ptr.sub_nat_ok (a := ebytes) (by simpa using hbm) (by omega) hoff
148  have hcp2 := memcpyB_blk_ok (nb := w) (no := 0) (pb := eb) (po := eo - (copy - (st.wsize - st.wnext)).toNat)
149    (n := (copy - (st.wsize - st.wnext)).toNat)
150    (h := { H with bytes := upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)) })
151    (ob := copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat) (by simp) hbm (by simpa using hro) hne
152    (by omega) (by omega)
153  have hn2g : ∀ H' : Heap, H'.bytes eb = some ebytes →
154      Ptr.add (Ptr.ref (BRef.blk eb) eo) (-((copy - (st.wsize - st.wnext)).toNat : Int)) H' =
155      .ok (Ptr.ref (BRef.blk eb) (eo - (copy - (st.wsize - st.wnext)).toNat), H') := fun H' hb =>
156    Ptr.sub_nat_ok (a := ebytes) (by simpa using hb) (by omega) hoff
157  have hbm' : (upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat))).get eb = some ebytes := by
158    simpa using hbm
159  simp only [bne_iff_ne, ne_eq, hne', not_false_eq_true, ite_true]
160  rw [bind_app, hn2g _ hbm]
161  simp only [bind_app, hcp2, wrI_eq, pure_app, hs, hw]
162  simp [setI, upd_upd]
163
164/-- `updatewindow`, `copy < wsize`, the copy ends exactly at the end of the window. -/
165theorem uw_core_small3 {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
166    {a ebytes : Array UInt8} {copy : UInt32}
167    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
168    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size) (hwn : st.wnext.toNat < st.wsize.toNat)
169    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
170    (hlt : ¬ st.wsize ≤ copy) (hQ : ¬ st.wsize - st.wnext > copy) (hR : copy - (st.wsize - st.wnext) = 0) :
171    updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, setI
172      { H with bytes := upd H.bytes w (some (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)) } zs
173      { st with wnext := 0, whave := if st.whave < st.wsize then st.whave + (st.wsize - st.wnext) else st.whave }) := by
174  have hz := hL.hz
175  have hs := hL.hs
176  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
177  have hws0 : (st.wsize == 0) = false := by simpa using hpos
178  have hD : (st.wsize - st.wnext).toNat = st.wsize.toNat - st.wnext.toNat :=
179    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)
180  have hQn : st.wsize.toNat - st.wnext.toNat ≤ copy.toNat := by
181    have : ¬ copy < st.wsize - st.wnext := hQ
182    rw [UInt32.lt_iff_toNat_lt, hD] at this; omega
183  have hRn : copy.toNat = st.wsize.toNat - st.wnext.toNat := by
184    have h0 : (copy - (st.wsize - st.wnext)).toNat = 0 := by rw [hR]; rfl
185    rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le, hD]; omega), hD] at h0; omega
186  have hcopy : copy = st.wsize - st.wnext := by
187    apply UInt32.toNat_inj.mp; rw [hD]; exact hRn
188  have hsum : st.wnext + copy = st.wsize := by
189    apply UInt32.toNat_inj.mp
190    rw [UInt32.toNat_add, hRn]; have := st.wsize.toNat_lt; rw [Nat.mod_eq_of_lt (by omega)]; omega
191  have hn0 : OkOn H (Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int)) (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat)) :=
192    Ptr.add_nat_ok (a := a) (by simpa using ha) (by omega)
193  have hn1 : OkOn H (Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(copy.toNat : Int))) (Ptr.ref (BRef.blk eb) (eo - copy.toNat)) :=
194    Ptr.sub_nat_ok (a := ebytes) (by simpa using heb) hc hoff
195  have hcp := memcpyB_blk_ok (nb := w) (no := 0 + st.wnext.toNat) (pb := eb) (po := eo - copy.toNat)
196    (n := (st.wsize - st.wnext).toNat) (h := H) ha heb hro hne (by omega) (by omega)
197  have hn0' : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) H = .ok (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat), H) := hn0
198  have hn1' : Ptr.add (Ptr.ref (BRef.blk eb) eo) (-(copy.toNat : Int)) H = .ok (Ptr.ref (BRef.blk eb) (eo - copy.toNat), H) := hn1
199  simp only [Nat.zero_add] at hcp hn0'
200  unfold updatewindow
201  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, hwnl, hws0, Bool.false_eq_true, ite_false]
202  simp only [ge_iff_le, hlt, ite_false, hQ, bind_app, hw, hn0', hn1', hcp, hR, bne_self_eq_false, Bool.false_eq_true]
203  have hsum' : st.wnext + (st.wsize - st.wnext) = st.wsize := by rw [← hcopy]; exact hsum
204  by_cases c2 : st.whave < st.wsize <;> simp [c2, wrI_eq, hs, setI, hw, hsum']
205
206theorem shl_toNat_aux {b : UInt32} (hb : b.toNat ≤ 15) : ((1 : UInt32) <<< b).toNat = 2 ^ b.toNat := W.shl_toNat b hb
207
208/-- The state after the first two lines of `updatewindow` when `wsize` was 0. -/
209def initWinS (st : InflateState) : InflateState :=
210  if st.wsize == 0 then { st with wsize := (1 : UInt32) <<< st.wbits, wnext := 0, whave := 0 } else st
211
212theorem shl32_one {b : UInt32} (hb : b.toNat ≤ 15) : shl32 1 b = pure ((1 : UInt32) <<< b) := by
213  have : b < 32 := by rw [UInt32.lt_iff_toNat_lt]; have : (32 : UInt32).toNat = 32 := rfl; omega
214  simp [shl32, this]
215
216/-- Initialising `wsize` first does not change what `updatewindow` does. -/
217theorem uw_init {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w : Nat}
218    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (hb : st.wbits.toNat ≤ 15) (e : BPtr) (copy : UInt32) :
219    updatewindow (some r) e copy H = updatewindow (some r) e copy (setI H zs (initWinS st)) := by
220  have hz := hL.hz
221  have hs := hL.hs
222  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
223  have hsh := shl32_one hb
224  by_cases h0 : st.wsize = 0
225  · have hws0 : (st.wsize == 0) = true := by simp [h0]
226    have hI : initWinS st = { st with wsize := (1 : UInt32) <<< st.wbits, wnext := 0, whave := 0 } := by
227      simp [initWinS, hws0]
228    have hpos : ((1 : UInt32) <<< st.wbits) ≠ 0 := by
229      intro e; have := shl_toNat_aux hb; rw [e] at this; have h2 := Nat.two_pow_pos st.wbits.toNat
230      have h3 : (0 : UInt32).toNat = 0 := rfl
231      omega
232    rw [hI]
233    unfold updatewindow
234    simp only [bind_app, pure_app, ldI_eq, ldZ_eq, wrI_eq, hz, hL.zst, castI, hs, hwnl, hws0, hsh, hI,
235      Bool.false_eq_true, ite_false, ite_true, setI_istates_same, ZStreamRef.get_setI]
236    simp only [h0, beq_self_eq_true, ite_true, hpos, beq_iff_eq, ne_eq]
237    simp only [ite_false, ite_false, Bool.false_eq_true, ite_true, bind_app, pure_app, wrI_eq, ldI_eq, setI_istates_same]
238    done
239  · have hws0 : (st.wsize == 0) = false := by simpa using h0
240    have hI : initWinS st = st := by simp [initWinS, hws0]
241    rw [hI]
242    have : setI H zs st = H := by
243      simp only [setI]; rw [upd_self _ _ _ hs]
244    rw [this]
245
246theorem zallocb_run {H : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get H = some z) (hza : z.zalloc = .fn "zcalloc") (items size : UInt32) :
247    ZALLOCB (some r) items size H = Zlib.Zutil.zcalloc z.«opaque» items size H := by
248  simp [ZALLOCB, ldZ_eq, hz, hza]
249
250/-- The window is `NULL` and the allocation fails: `updatewindow` returns 1 and only the allocation counter moves. -/
251theorem uw_alloc_fail {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
252    (hL : Live H r zs z st) (hza : z.zalloc = .fn "zcalloc") (hb : st.wbits.toNat ≤ 15) (hw : st.window = .null)
253    (hok : ¬ H.allocOk H.nalloc = true) (e : BPtr) (copy : UInt32) :
254    updatewindow (some r) e copy H = .ok (1, setI { H with nalloc := H.nalloc + 1 } zs st) := by
255  have hz := hL.hz
256  have hs := hL.hs
257  have hsh := shl32_one hb
258  unfold updatewindow
259  have hf := Zlib.Zutil.Proofs.zcalloc_fail_run H z.«opaque» (1 <<< st.wbits) 1 hok
260  have hf' : Zlib.Zutil.zcalloc z.«opaque» (1 <<< st.wbits) 1 H = .ok (.null, { H with nalloc := H.nalloc + 1 }) := by
261    simpa [Zlib.Zutil.Proofs.failHeap] using hf
262  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, hw, beq_self_eq_true, ite_true, hsh,
263    zallocb_run hz hza, hf', wrI_eq]
264  have e : ({ st with window := Ptr.null } : InflateState) = st := by rw [← hw]
265  simp only [e, setI]
266
267theorem ZStreamRef.get_allocHeap (h : Heap) (n : Nat) (r : ZStreamRef) : r.get (Zlib.Zutil.Proofs.allocHeap h n) = r.get h := by
268  cases r <;> rfl
269
270/-- The window is `NULL` and the allocation succeeds: the call continues as on the state with the new window block. -/
271theorem uw_alloc_ok {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
272    (hL : Live H r zs z st) (hza : z.zalloc = .fn "zcalloc") (hb : st.wbits.toNat ≤ 15) (hw : st.window = .null)
273    (hok : H.allocOk H.nalloc = true) (hF : Fresh H) (e : BPtr) (copy : UInt32) :
274    updatewindow (some r) e copy H = updatewindow (some r) e copy
275      (setI (Zlib.Zutil.Proofs.allocHeap H ((1 <<< st.wbits : UInt32) * 1).toNat) zs
276        { st with window := .ref (.blk H.nextBlk) 0 }) := by
277  have hz := hL.hz
278  have hs := hL.hs
279  have hsh := shl32_one hb
280  have hc := Zlib.Zutil.Proofs.zcalloc_ok_run H z.«opaque» (1 <<< st.wbits) 1 hok hF
281  have hne : (Ptr.ref (BRef.blk H.nextBlk) 0 == (Ptr.null : BPtr)) = false := by simp
282  have hnn : (Ptr.ref (BRef.blk H.nextBlk) 0 : BPtr) ≠ Ptr.null := by simp
283  have hI : (Zlib.Zutil.Proofs.allocHeap H ((1 <<< st.wbits : UInt32) * 1).toNat).istates zs = some st := by
284    simpa [Zlib.Zutil.Proofs.allocHeap] using hs
285  unfold updatewindow
286  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, hw, beq_self_eq_true, ite_true, hsh,
287    zallocb_run hz hza, hc, wrI_eq, hne, Bool.false_eq_true, ite_false, ZStreamRef.get_setI, setI_istates_same, hI]
288  simp only [bind_app, ldI_eq, ldZ_eq, wrI_eq, setI_istates_same, hnn, ZStreamRef.get_setI, ZStreamRef.get_allocHeap, ite_false, Bool.false_eq_true, beq_iff_eq, hz, hL.zst, castI, hne, hI, hsh]
289  done
290
291/-- `updatewindow` on a state whose window block exists: `wsize` is set if it was 0, then the ring buffer is filled
292(`uwPost`); the call returns 0. -/
293theorem uw_main {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
294    {a ebytes : Array UInt8} {copy : UInt32}
295    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
296    (hwb : st.wbits.toNat ≤ 15) (hasz : a.size = 2 ^ st.wbits.toNat)
297    (hws : st.wsize.toNat = 0 ∨ st.wsize.toNat = 2 ^ st.wbits.toNat)
298    (hwn : st.wnext.toNat < st.wsize.toNat ∨ (st.wsize.toNat = 0 ∧ st.wnext.toNat = 0))
299    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
300    updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, setI
301      { setI H zs (initWinS st) with bytes := upd H.bytes w (some (uwPost (initWinS st) a ebytes eo copy).1) } zs
302      (uwPost (initWinS st) a ebytes eo copy).2) := by
303  have hpow := shl_toNat_aux hwb
304  have h2pos := Nat.two_pow_pos st.wbits.toNat
305  have hcase : (st.wsize = 0 ∧ initWinS st = { st with wsize := (1 : UInt32) <<< st.wbits, wnext := 0, whave := 0 }) ∨
306      (st.wsize ≠ 0 ∧ initWinS st = st) := by
307    by_cases h0 : st.wsize = 0
308    · left; exact ⟨h0, by simp [initWinS, h0]⟩
309    · right; exact ⟨h0, by simp [initWinS, h0]⟩
310  have hpos : (initWinS st).wsize ≠ 0 ∧ (initWinS st).wsize.toNat = 2 ^ st.wbits.toNat ∧ (initWinS st).wnext.toNat < (initWinS st).wsize.toNat := by
311    rcases hcase with ⟨h0, e⟩ | ⟨h0, e⟩
312    · rw [e]
313      have hz0 : ((1 : UInt32) <<< st.wbits).toNat = 2 ^ st.wbits.toNat := hpow
314      refine ⟨fun hh => ?_, hz0, ?_⟩
315      · have h0' : ((1 : UInt32) <<< st.wbits).toNat = 0 := by
316          have hh' : ((1 : UInt32) <<< st.wbits) = 0 := hh
317          rw [hh']; rfl
318        omega
319      · show (0 : UInt32).toNat < ((1 : UInt32) <<< st.wbits).toNat
320        rw [hz0]; simp; omega
321    · rw [e]
322      have : st.wsize.toNat ≠ 0 := fun hh => h0 (UInt32.toNat_inj.mp (by simpa using hh))
323      refine ⟨h0, by omega, by omega⟩
324  have hsz1 : (initWinS st).wsize.toNat ≤ a.size := by omega
325  have hwn1 := hpos.2.2
326  have hpos := hpos.1
327  have hL1 : Live (setI H zs (initWinS st)) r zs z (initWinS st) :=
328    ⟨by simpa using hL.hz, by simp, hL.zst, by unfold initWinS; split <;> exact hL.back, by unfold initWinS; split <;> exact hL.mode,
329      hL.zalloc, hL.zfree⟩
330  have hw1 : (initWinS st).window = .ref (.blk w) 0 := by unfold initWinS; split <;> exact hw
331  rw [uw_init hL hw hwb]
332  have ha1 : (setI H zs (initWinS st)).bytes w = some a := ha
333  have hro1 : (setI H zs (initWinS st)).ro w = false := hro
334  have heb1 : (setI H zs (initWinS st)).bytes eb = some ebytes := heb
335  by_cases hbig : (initWinS st).wsize ≤ copy
336  · have := uw_core_big hL1 hw1 ha1 hro1 hpos hsz1 heb1 hne (by have := UInt32.le_iff_toNat_le.mp hbig; omega) hoff hbig
337    simpa [uwPost, hbig] using this
338  · by_cases hP : (initWinS st).wsize - (initWinS st).wnext > copy
339    · have hlt : copy.toNat < (initWinS st).wsize.toNat := by
340        have : ¬ (initWinS st).wsize ≤ copy := hbig
341        rw [UInt32.le_iff_toNat_le] at this; omega
342      have := uw_core_small1 hL1 hw1 ha1 hro1 hpos hsz1 hwn1 heb1 hne (by omega) hoff hbig hP
343      simpa [uwPost, hbig, hP] using this
344    · by_cases hR : copy - ((initWinS st).wsize - (initWinS st).wnext) = 0
345      · have hlt : copy.toNat < (initWinS st).wsize.toNat := by
346          have : ¬ (initWinS st).wsize ≤ copy := hbig
347          rw [UInt32.le_iff_toNat_le] at this; omega
348        have := uw_core_small3 hL1 hw1 ha1 hro1 hpos hsz1 hwn1 heb1 hne (by omega) hoff hbig hP hR
349        simpa [uwPost, hbig, hP, hR] using this
350      · have hlt : copy.toNat < (initWinS st).wsize.toNat := by
351          have : ¬ (initWinS st).wsize ≤ copy := hbig
352          rw [UInt32.le_iff_toNat_le] at this; omega
353        have := uw_core_small2 hL1 hw1 ha1 hro1 hpos hsz1 hwn1 heb1 hne (by omega) hoff hbig hP hR
354        simpa [uwPost, hbig, hP, hR] using this
355
356/-- The ring-buffer indices after `updatewindow` (`uwPost`) keep the window invariant, and the other fields are kept. -/
357theorem uwPost_arith {st : InflateState} {a ebytes : Array UInt8} {eo : Nat} {copy : UInt32}
358    (hpos : st.wsize.toNat ≠ 0)
359    (hv : st.whave.toNat ≤ st.wsize.toNat) (hwn : st.wnext.toNat < st.wsize.toNat)
360    (heq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat)
361    (hcl : copy.toNat < 2 ^ 32) (hw32 : st.wsize.toNat ≤ 2 ^ 16) :
362    (uwPost st a ebytes eo copy).2.wsize = st.wsize ∧ (uwPost st a ebytes eo copy).2.wbits = st.wbits ∧
363    (uwPost st a ebytes eo copy).2.window = st.window ∧ (uwPost st a ebytes eo copy).2.reqbits = st.reqbits ∧
364    (uwPost st a ebytes eo copy).2.bits = st.bits ∧ (uwPost st a ebytes eo copy).2.next = st.next ∧
365    (uwPost st a ebytes eo copy).2.lencode = st.lencode ∧ (uwPost st a ebytes eo copy).2.distcode = st.distcode ∧
366    (uwPost st a ebytes eo copy).2.lens = st.lens ∧ (uwPost st a ebytes eo copy).2.work = st.work ∧
367    (uwPost st a ebytes eo copy).2.codes = st.codes ∧ (uwPost st a ebytes eo copy).2.strm = st.strm ∧
368    (uwPost st a ebytes eo copy).2.mode = st.mode ∧
369    (uwPost st a ebytes eo copy).2.whave.toNat ≤ (uwPost st a ebytes eo copy).2.wsize.toNat ∧
370    (uwPost st a ebytes eo copy).2.wnext.toNat < (uwPost st a ebytes eo copy).2.wsize.toNat ∧
371    ((uwPost st a ebytes eo copy).2.whave.toNat < (uwPost st a ebytes eo copy).2.wsize.toNat →
372      (uwPost st a ebytes eo copy).2.wnext.toNat = (uwPost st a ebytes eo copy).2.whave.toNat) := by
373  have e1 := st.wsize.toNat_lt
374  have e2 := st.wnext.toNat_lt
375  have e3 := st.whave.toNat_lt
376  unfold uwPost
377  repeat' split
378  all_goals
379    refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, ?_, ?_, ?_⟩
380  all_goals
381    simp only [UInt32.lt_iff_toNat_lt, UInt32.le_iff_toNat_le, UInt32.toNat_add, UInt32.toNat_sub, gt_iff_lt, beq_iff_eq,
382      bne_iff_ne, ne_eq, ← UInt32.toNat_inj, UInt32.toNat_zero, Nat.not_lt, Nat.not_le] at *
383    omega
384
385theorem initWinS_facts {st : InflateState} (hwb : st.wbits.toNat ≤ 15)
386    (hws : st.wsize.toNat = 0 ∨ st.wsize.toNat = 2 ^ st.wbits.toNat)
387    (hv : st.whave.toNat ≤ st.wsize.toNat) (hwn : st.wnext.toNat < st.wsize.toNat ∨ (st.wsize.toNat = 0 ∧ st.wnext.toNat = 0))
388    (heq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat) :
389    (initWinS st).wsize.toNat = 2 ^ st.wbits.toNat ∧ (initWinS st).wbits = st.wbits ∧ (initWinS st).window = st.window ∧
390    (initWinS st).whave.toNat ≤ (initWinS st).wsize.toNat ∧ (initWinS st).wnext.toNat < (initWinS st).wsize.toNat ∧
391    ((initWinS st).whave.toNat < (initWinS st).wsize.toNat → (initWinS st).wnext.toNat = (initWinS st).whave.toNat) ∧
392    (initWinS st).reqbits = st.reqbits ∧ (initWinS st).bits = st.bits ∧ (initWinS st).next = st.next ∧
393    (initWinS st).lencode = st.lencode ∧ (initWinS st).distcode = st.distcode ∧ (initWinS st).lens = st.lens ∧
394    (initWinS st).work = st.work ∧ (initWinS st).codes = st.codes ∧ (initWinS st).strm = st.strm ∧
395    (initWinS st).mode = st.mode := by
396  have hpow := shl_toNat_aux hwb
397  have h2pos := Nat.two_pow_pos st.wbits.toNat
398  by_cases h0 : st.wsize = 0
399  · have e : initWinS st = { st with wsize := (1 : UInt32) <<< st.wbits, wnext := 0, whave := 0 } := by simp [initWinS, h0]
400    rw [e]
401    refine ⟨hpow, rfl, rfl, ?_, ?_, ?_, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
402    · show (0 : UInt32).toNat ≤ _; simp
403    · show (0 : UInt32).toNat < ((1 : UInt32) <<< st.wbits).toNat; rw [hpow]; simp; omega
404    · intro hh; show (0 : UInt32).toNat = (0 : UInt32).toNat; rfl
405  · have e : initWinS st = st := by simp [initWinS, h0]
406    have : st.wsize.toNat ≠ 0 := fun hh => h0 (UInt32.toNat_inj.mp (by simpa using hh))
407    rw [e]
408    refine ⟨by omega, rfl, rfl, hv, by omega, heq, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
409
410theorem uwPost_size (st : InflateState) (a ebytes : Array UInt8) (eo : Nat) (copy : UInt32) :
411    (uwPost st a ebytes eo copy).1.size = a.size := by
412  unfold uwPost
413  split
414  · exact size_copyRange ..
415  · split
416    · exact size_copyRange ..
417    · split
418      · rw [size_copyRange, size_copyRange]
419      · exact size_copyRange ..
420
421/-- `updatewindow` on a good stream whose window block exists (`copy` bytes that end at offset `eo` of the block `eb`,
422which is not the window): it returns 0, fills the ring buffer as `uwPost` says, and the stream is good again. -/
423theorem uw_post {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
424    {a ebytes : Array UInt8} {copy : UInt32}
425    (hG : Good H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
426    (hasz : a.size = 2 ^ st.wbits.toNat)
427    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
428    ∃ H' st', updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, H') ∧
429      H' = setI { setI H zs (initWinS st) with bytes := upd H.bytes w (some (uwPost (initWinS st) a ebytes eo copy).1) } zs st' ∧
430      st' = (uwPost (initWinS st) a ebytes eo copy).2 ∧ Good H' r zs z st' ∧ st'.window = st.window ∧
431      H'.bytes w = some (uwPost (initWinS st) a ebytes eo copy).1 ∧ (uwPost (initWinS st) a ebytes eo copy).1.size = a.size ∧
432      (∀ b, b ≠ w → H'.bytes b = H.bytes b) ∧ (∀ b, H'.live b ↔ H.live b) ∧ H'.nextBlk = H.nextBlk := by
433  have hL := hG.live
434  have hI := hG.inv
435  have hmain := uw_main hL hw ha hro hI.win.wbits hasz hI.win.ws hI.win.wn heb hne hc hoff
436  obtain ⟨f1, f2, f3, hv1, hwn1, heq1, f4, f5, f6, f7, f8, f16, f17, f18, f12, f13⟩ :=
437    initWinS_facts hI.win.wbits hI.win.ws hI.win.hv hI.win.wn hI.win.eq
438  have hwb := hI.win.wbits
439  have hle : (initWinS st).wsize.toNat ≤ 2 ^ 16 := by
440    rw [f1]; have := Nat.pow_le_pow_right (by decide : 0 < 2) (by omega : st.wbits.toNat ≤ 16); omega
441  have hposn : (initWinS st).wsize.toNat ≠ 0 := by rw [f1]; exact Nat.pos_iff_ne_zero.mp (Nat.two_pow_pos _)
442  obtain ⟨g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, gv, gwn, geq⟩ :=
443    uwPost_arith (st := initWinS st) (a := a) (ebytes := ebytes) (eo := eo) (copy := copy) hposn hv1 hwn1 heq1 copy.toNat_lt hle
444  have hAsz := uwPost_size (initWinS st) a ebytes eo copy
445  generalize hP : uwPost (initWinS st) a ebytes eo copy = P at *
446  have hs1 : (setI H zs (initWinS st)).istates zs = some (initWinS st) := by simp
447  have hbw : (setI H zs (initWinS st)).bytes w = some a := ha
448  have hS : Shape H { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } :=
449    (shape_setI hL.hs _).trans (shape_setB (h := setI H zs (initWinS st)) hbw P.1)
450  have hS2 : Shape H (setI { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } zs P.2) :=
451    hS.trans (shape_setI (s0 := initWinS st) (by simp) _)
452  have hz0 : r.get { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } = some z := by
453    cases r <;> simpa [ZStreamRef.get] using hL.hz
454  have hs0 : ({ setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } : Heap).istates zs = some (initWinS st) := by
455    simp
456  have hUh : Uniq { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } := hS.uniq hG.uniq
457  have hFh : Fresh { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } := hS.fresh (by simp) hG.fresh
458  have hstI : StInv { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } zs P.2 := by
459    refine ⟨?_, ?_, ?_, ?_, ?_⟩
460    · obtain ⟨w1, w2, w3⟩ := hI.wf
461      exact ⟨by rw [g9, f16]; exact w1, by rw [g10, f17]; exact w2, by rw [g11, f18]; exact w3⟩
462    · refine ⟨by rw [g2, f2]; exact hI.win.wbits, Or.inr ⟨w, P.1, by rw [g3, f3]; exact hw, by simp, by simpa using hro, ?_⟩,
463        fun h0 => ?_, ?_, gv, Or.inl gwn, geq⟩
464      · rw [g2, f2, hAsz, hasz]
465      · rw [g3, f3, hw] at h0; cases h0
466      · rw [g1, f1, g2, f2]; right; rfl
467    · rw [g4, f4]; exact hI.reqbits
468    · rw [g5, f5]; exact hI.bits
469    · unfold PtrInv; rw [g6, f6, g7, f7, g8, f8]; exact hI.ptr
470  refine ⟨_, P.2, hmain, rfl, rfl, ?_, by rw [g3, f3], by simp, hAsz, ?_, fun b => hS2.live b, by simp⟩
471  · have := good_set hz0 hs0 hUh hFh hL.zst hL.zalloc hL.zfree (by rw [g12, f12]; exact hL.back)
472      (by rw [g13, f13]; exact hL.mode) hstI
473    rwa [ZStreamRef.put_self hz0] at this
474  · intro b hb; simp [upd_ne _ _ _ _ hb]
475
476theorem uniq_allocHeap {h : Heap} (hU : Uniq h) (hF : Fresh h) (n : Nat) : Uniq (Zlib.Zutil.Proofs.allocHeap h n) := by
477  intro b
478  by_cases hb : b = h.nextBlk
479  · subst hb
480    have := Heap.not_live.mp (hF _ (Nat.le_refl _))
481    obtain ⟨e0, e1, e2, e3, e4, e5, e6⟩ := this
482    simp [Zlib.Zutil.Proofs.allocHeap, e1, e2, e3, e4, e5, e6]
483  · have := hU b
484    simpa only [Zlib.Zutil.Proofs.allocHeap, upd_ne _ _ _ _ hb] using this
485
486/-- The state of a stream whose window `NULL` was just replaced by the new block. -/
487def withWin (st : InflateState) (nb : Nat) : InflateState := { st with window := .ref (.blk nb) 0 }
488
489/-- **updatewindow, window absent and the allocation succeeds.** The window is a new block (the next block number,
490`1 << wbits` bytes of arbitrary content), then filled as `uwPost` says; the stream is good again and owns the new
491block. -/
492theorem uw_null_ok {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {eb eo : Nat}
493    {ebytes : Array UInt8} {copy : UInt32}
494    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (hw : st.window = .null)
495    (hok : h.allocOk h.nalloc = true) (heb : h.bytes eb = some ebytes) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
496    ∃ H' st', updatewindow (some r) (.ref (.blk eb) eo) copy h = .ok (0, H') ∧ Good H' r zs z st' ∧
497      st'.window = .ref (.blk h.nextBlk) 0 ∧ (∃ A, H'.bytes h.nextBlk = some A) ∧
498      (∀ S, h.Owns S → H'.Owns (fun b => S b ∨ b = h.nextBlk)) ∧ H'.nextBlk = h.nextBlk + 1 ∧
499      (∀ b, b ≠ h.nextBlk → H'.bytes b = h.bytes b) := by
500  have hL := hG.live
501  have hI := hG.inv
502  have hF := hG.fresh
503  have hne : eb ≠ h.nextBlk := by
504    intro e; have := Fresh.bytes hF (b := h.nextBlk) (Nat.le_refl _); rw [← e, heb] at this; cases this
505  rw [uw_alloc_ok hL hza hI.win.wbits hw hok hF]
506  have hn : ((1 <<< st.wbits : UInt32) * 1).toNat = 2 ^ st.wbits.toNat := by
507    have := shl_toNat_aux hI.win.wbits
508    simpa using this
509  obtain ⟨A0, hA0⟩ : ∃ A0 : Array UInt8, A0 = Array.ofFn (n := ((1 <<< st.wbits : UInt32) * 1).toNat)
510      fun i => Junk.of (h.garbage h.nalloc i.val) := ⟨_, rfl⟩
511  have hA0sz : A0.size = 2 ^ st.wbits.toNat := by rw [hA0, Array.size_ofFn]; exact hn
512  have hws0 := hI.win.nullws hw
513  have hws0n : st.wsize.toNat = 0 := by rw [hws0]; rfl
514  have hA := Zlib.Zutil.Proofs.allocHeap_frame h ((1 <<< st.wbits : UInt32) * 1).toNat
515  have hAb : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).bytes h.nextBlk = some A0 := by
516    rw [hA0]; simp [Zlib.Zutil.Proofs.allocHeap]
517  have hAro : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).ro h.nextBlk = false := by
518    simp [Zlib.Zutil.Proofs.allocHeap]
519  have hS : Shape (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat)
520      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) :=
521    shape_setI (s0 := st) (by simpa [Zlib.Zutil.Proofs.allocHeap] using hL.hs) _
522  have hUa := uniq_allocHeap hG.uniq hF ((1 <<< st.wbits : UInt32) * 1).toNat
523  have hFa := hA.2.1 hF
524  have hG2 : Good (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
525      r zs z (withWin st h.nextBlk) := by
526    refine ⟨⟨?_, by simp, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩, ?_, hS.uniq hUa, hS.fresh rfl hFa⟩
527    · cases r <;> simpa [ZStreamRef.get, Zlib.Zutil.Proofs.allocHeap, setI] using hL.hz
528    · refine ⟨hI.wf, ⟨hI.win.wbits, Or.inr ⟨h.nextBlk, A0, rfl, ?_, ?_, ?_⟩, fun h0 => absurd h0 (by simp [withWin]), ?_, ?_, ?_, ?_⟩,
529        hI.reqbits, hI.bits, hI.ptr⟩
530      · simpa [setI] using hAb
531      · simpa [setI] using hAro
532      · exact hA0sz
533      · exact Or.inl hws0n
534      · have := hI.win.hv; show st.whave.toNat ≤ st.wsize.toNat; exact this
535      · right; refine ⟨hws0n, ?_⟩
536        have := hI.win.wn; show st.wnext.toNat = 0; omega
537      · intro hh; have := hI.win.hv; show st.wnext.toNat = st.whave.toNat; have := hI.win.wn; have := hI.win.hv
538        change st.whave.toNat < st.wsize.toNat at hh; omega
539  have hz2 : r.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) = some z :=
540    hG2.live.hz
541  have hbe : (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)).bytes eb = some ebytes := by
542    simp [Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hne, heb]
543  obtain ⟨H', st', hrun, -, hst', hG', hw', hb', hsz', hbo, hlive, hnb⟩ := uw_post (hG := hG2) (w := h.nextBlk) (eb := eb) (eo := eo)
544    (a := A0) (ebytes := ebytes) (copy := copy) rfl (by simpa [setI] using hAb) (by simpa [setI] using hAro)
545    (by exact hA0sz) hbe (Ne.symm hne) hc hoff
546  refine ⟨H', st', hrun, hG', by rw [hw']; rfl, ⟨_, hb'⟩, ?_, ?_, ?_⟩
547  · intro S hO
548    have h2 := hS.owns (hA.1 S hO)
549    exact fun b => (hlive b).trans (h2 b)
550  · rw [hnb]; simp [Zlib.Zutil.Proofs.allocHeap, setI]
551  · intro b hb; rw [hbo b (by exact hb)]; simp [Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hb]
552
553/-- **updatewindow, safety.** On a good stream with the default allocator, whose `copy` bytes end at offset `eo` of a
554byte block `eb` that is not the window (`copy ≤ eo ≤ size`, the buffer `zlib.h` gives to `inflate`), the call never
555faults. It returns 0 and the stream is good again (the window block exists afterwards; if it did not before, it is
556the new block `h.nextBlk` and the stream owns it), or it returns 1 because the allocation of the window failed
557(window absent, oracle says no): then only the allocation counter moved and the state is unchanged. -/
558theorem updatewindow_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {eb eo : Nat}
559    {ebytes : Array UInt8} {copy : UInt32}
560    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (heb : h.bytes eb = some ebytes)
561    (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) (hdisj : ∀ w, st.window = .ref (.blk w) 0 → eb ≠ w) :
562    ∃ v h' st', C.run (updatewindow (some r) (.ref (.blk eb) eo) copy) h = .ok (v, h') ∧ Good h' r zs z st' ∧
563      ((v = 0 ∧ st'.window ≠ .null ∧
564          (∀ S, h.Owns S → h'.Owns (fun b => S b ∨ (st.window = .null ∧ b = h.nextBlk)))) ∨
565       (v = 1 ∧ st.window = .null ∧ ¬ h.allocOk h.nalloc = true ∧ h' = setI { h with nalloc := h.nalloc + 1 } zs st ∧ st' = st)) := by
566  have hL := hG.live
567  have hI := hG.inv
568  rcases hI.win.block with hw | ⟨w, a, hw, ha, hro, hasz⟩
569  · by_cases hok : h.allocOk h.nalloc = true
570    · obtain ⟨H', st', hrun, hG', hw', -, hO, -, -⟩ := uw_null_ok hG hza hw hok heb hc hoff
571      refine ⟨0, H', st', hrun, hG', Or.inl ⟨0 |> fun _ => rfl, by rw [hw']; simp, ?_⟩⟩
572      intro S hOw
573      have := hO S hOw
574      simpa [hw] using this
575    · have hrun := uw_alloc_fail hL hza hI.win.wbits hw hok (.ref (.blk eb) eo) copy
576      refine ⟨1, _, st, hrun, ?_, Or.inr ⟨rfl, hw, hok, rfl, rfl⟩⟩
577      have hS : Shape h { h with nalloc := h.nalloc + 1 } := Shape.refl h
578      have := good_set (h0 := { h with nalloc := h.nalloc + 1 }) (z0 := z) (z' := z) (s0 := st) (st' := st) hL.hz hL.hs
579        hG.uniq hG.fresh hL.zst hL.zalloc hL.zfree hL.back hL.mode (StInv.congr (h := h) rfl rfl hI)
580      have hz' : r.get { h with nalloc := h.nalloc + 1 } = some z := by cases r <;> simpa [ZStreamRef.get] using hL.hz
581      rwa [ZStreamRef.put_self hz'] at this
582  · obtain ⟨H', st', hrun, -, -, hG', hw', -, -, -, hlive, -⟩ := uw_post hG hw ha hro hasz heb (hdisj w hw).symm hc hoff
583    refine ⟨0, H', st', hrun, hG', Or.inl ⟨rfl, by rw [hw', hw]; simp, ?_⟩⟩
584    intro S hO b
585    rw [hlive b, hO b]
586    simp [hw]
587
588end Zlib.Inflate.Proofs