inflate.c.window-general.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.uw»
2import ZlibF.Proof.«inflate.c.ring»
3import ZlibF.Spec.Public.Memory
4
5/-! General readable sources for the full-window update path. -/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9
10/-- Equal source slices produce the same destination for a byte copy. -/
11theorem copyRange_source_agree (dest left right : Array UInt8) (doff soff n : Nat)
12    (hagree : ∀ j, j < n → left[soff + j]! = right[soff + j]!) :
13    copyRange dest left doff soff n = copyRange dest right doff soff n := by
14  induction n with
15  | zero => rfl
16  | succ n ih =>
17    rw [copyRange_succ, copyRange_succ, ih (fun j hj => hagree j (by omega)), hagree n (by omega)]
18
19/-- A write does not change a disjoint range of the same array. -/
20theorem copyRange_read_disjoint (dest source : Array UInt8) (doff soff n read count : Nat)
21    (hd : doff + n ≤ dest.size) (hs : soff + n ≤ source.size)
22    (hr : read + count ≤ dest.size)
23    (hdis : doff + n ≤ read ∨ read + count ≤ doff) :
24    ∀ j, j < count → (copyRange dest source doff soff n)[read + j]! = dest[read + j]! := by
25  intro j hj
26  have he := copyRange_bang dest source doff soff n hd hs (read + j) (by omega)
27  have hout : ¬ (doff ≤ read + j ∧ read + j < doff + n) := by omega
28  simpa [hout] using he
29
30/-- If the next source slice is outside the first write, a second copy from
31the updated allocation has the same result as a copy from the original bytes. -/
32theorem copyRange_second_source_disjoint (dest source : Array UInt8)
33    (doff soff n doff2 soff2 n2 : Nat)
34    (hd : doff + n ≤ dest.size) (hs : soff + n ≤ source.size)
35    (hr : soff2 + n2 ≤ dest.size)
36    (hdis : doff + n ≤ soff2 ∨ soff2 + n2 ≤ doff) :
37    let mid := copyRange dest source doff soff n
38    copyRange mid mid doff2 soff2 n2 = copyRange mid dest doff2 soff2 n2 := by
39  apply copyRange_source_agree
40  exact copyRange_read_disjoint dest source doff soff n soff2 n2 hd hs hr hdis
41
42/-- Updating one byte block leaves every other represented source unchanged;
43the source becomes the updated block when it is the same allocation. -/
44theorem window_write_source {h : Heap} {w : Nat} {source : BRef} {bytes : Array UInt8}
45    (hs : Space.get h source = some bytes) (updated : Array UInt8) :
46    Space.get { h with bytes := upd h.bytes w (some updated) } source =
47      some (if source = .blk w then updated else bytes) := by
48  cases source with
49  | blk b =>
50    by_cases he : b = w
51    · subst b
52      simp [Space.get]
53    · have hb : h.bytes b = some bytes := hs
54      simp [Space.get, he, upd_ne _ _ _ _ he, hb]
55  | str b => simpa [Space.get] using hs
56  | st_dist_code => simpa [Space.get] using hs
57  | st_length_code => simpa [Space.get] using hs
58  | dstate_depth b => simpa [Space.get] using hs
59
60/-- The public separation of the complete input from the window implies
61separation of the final window-sized suffix used by the full-copy branch. -/
62theorem uw_big_public_separation {w eo : Nat} {source : BRef} {size copy : UInt32}
63    (hfit : copy.toNat ≤ eo) (hbig : size ≤ copy)
64    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
65      (.ref (.blk w) 0) size.toNat) :
66    BRef.blk w ≠ source ∨ size.toNat ≤ eo - size.toNat ∨ eo ≤ 0 := by
67  have hsize : size.toNat ≤ copy.toNat := UInt32.le_iff_toNat_le.mp hbig
68  simp only [ZlibF.Spec.Public.Separate] at hsep
69  rcases hsep with hzero | hzero | hne | hleft | hright
70  · right; left; omega
71  · right; left; omega
72  · left; exact Ne.symm hne
73  · right; right; omega
74  · right; left; omega
75
76/-- `updatewindow` with a full-window copy reads any represented byte object.
77The source and destination may be disjoint ranges of the same object. -/
78theorem uw_core_big_any {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
79    {st : InflateState} {w eo : Nat} {source : BRef} {a bytes : Array UInt8} {copy : UInt32}
80    (hl : Live h r zs z st) (hw : st.window = .ref (.blk w) 0)
81    (ha : h.bytes w = some a) (hro : h.ro w = false)
82    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size)
83    (hs : Space.get h source = some bytes) (hc : st.wsize.toNat ≤ eo) (hoff : eo ≤ bytes.size)
84    (hsep : BRef.blk w ≠ source ∨ st.wsize.toNat ≤ eo - st.wsize.toNat ∨ eo ≤ 0)
85    (hbig : st.wsize ≤ copy) :
86    updatewindow (some r) (.ref source eo) copy h = .ok (0, setI
87      { h with bytes := upd h.bytes w (some (copyRange a bytes 0 (eo - st.wsize.toNat) st.wsize.toNat)) } zs
88      { st with wnext := 0, whave := st.wsize }) := by
89  have hwn : (st.window == Ptr.null) = false := by rw [hw]; simp
90  have hws0 : (st.wsize == 0) = false := by simpa using hpos
91  have hsub : Ptr.add (Ptr.ref source eo) (-(st.wsize.toNat : Int)) h =
92      .ok (Ptr.ref source (eo - st.wsize.toNat), h) := Ptr.sub_nat_ok hs hc hoff
93  have hcp := Ptr.memcpy_ok (rd := BRef.blk w) (rs := source) (od := 0)
94    (os := eo - st.wsize.toNat) (n := st.wsize.toNat) (da := a) (sa := bytes)
95    (by simpa using ha) hs (by simpa using hro) (by omega) (by omega) (by
96      rcases hsep with hne | hafter | hbefore
97      · exact Or.inl hne
98      · exact Or.inr (Or.inl (by omega))
99      · exact Or.inr (Or.inr (by omega)))
100  have hcp' : memcpyB (.ref (.blk w) 0) (.ref source (eo - st.wsize.toNat)) st.wsize.toNat h =
101      .ok ((), { h with bytes := upd h.bytes w (some (copyRange a bytes 0 (eo - st.wsize.toNat) st.wsize.toNat)) }) := by
102    simpa [Space.put] using hcp
103  unfold updatewindow
104  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, wrI_eq, hl.hz, hl.zst, castI, hl.hs,
105    hwn, hws0, Bool.false_eq_true, ite_false]
106  simp only [ge_iff_le, hbig, ite_true, bind_app, hw, hsub]
107  simp only [hcp', wrI_eq, pure_app, hl.hs, hw]
108
109/-- The full-copy branch under the unchanged public separation condition. -/
110theorem uw_core_big_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
111    {st : InflateState} {w eo : Nat} {source : BRef} {a bytes : Array UInt8} {copy : UInt32}
112    (hl : Live h r zs z st) (hw : st.window = .ref (.blk w) 0)
113    (ha : h.bytes w = some a) (hro : h.ro w = false)
114    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size)
115    (hs : Space.get h source = some bytes) (hfit : copy.toNat ≤ eo) (hoff : eo ≤ bytes.size)
116    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
117      st.window st.wsize.toNat) (hbig : st.wsize ≤ copy) :
118    updatewindow (some r) (.ref source eo) copy h = .ok (0, setI
119      { h with bytes := upd h.bytes w (some (copyRange a bytes 0 (eo - st.wsize.toNat) st.wsize.toNat)) } zs
120      { st with wnext := 0, whave := st.wsize }) := by
121  have hsize : st.wsize.toNat ≤ copy.toNat := UInt32.le_iff_toNat_le.mp hbig
122  apply uw_core_big_any hl hw ha hro hpos hsz hs (by omega) hoff
123  · apply uw_big_public_separation hfit hbig
124    simpa only [hw] using hsep
125  · exact hbig
126
127/-- Public input/window separation implies separation of any fitting single
128copy into the initialized window, including the zero-length case. -/
129theorem uw_small_public_separation {w eo wn size copy : Nat} {source : BRef}
130    (hfit : copy ≤ eo) (hwindow : wn + copy ≤ size)
131    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy)) copy (.ref (.blk w) 0) size) :
132    BRef.blk w ≠ source ∨ wn + copy ≤ eo - copy ∨ (eo - copy) + copy ≤ wn := by
133  simp only [ZlibF.Spec.Public.Separate] at hsep
134  rcases hsep with hzero | hzero | hne | hleft | hright
135  · right; omega
136  · right; omega
137  · exact Or.inl hne.symm
138  · right; right; omega
139  · right; left; omega
140
141/-- `updatewindow` copies a short source that fits before the window end.
142The source may be any represented byte object, including a disjoint slice
143of the window allocation itself. -/
144theorem uw_core_small1_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
145    {st : InflateState} {w eo : Nat} {source : BRef} {a bytes : Array UInt8} {copy : UInt32}
146    (hl : Live h r zs z st) (hw : st.window = .ref (.blk w) 0)
147    (ha : h.bytes w = some a) (hro : h.ro w = false)
148    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size)
149    (hwn : st.wnext.toNat < st.wsize.toNat) (hs : Space.get h source = some bytes)
150    (hfit : copy.toNat ≤ eo) (hoff : eo ≤ bytes.size)
151    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
152      st.window st.wsize.toNat)
153    (hlt : ¬ st.wsize ≤ copy) (hp : st.wsize - st.wnext > copy) :
154    updatewindow (some r) (.ref source eo) copy h = .ok (0, setI
155      { h with bytes := upd h.bytes w (some (copyRange a bytes st.wnext.toNat (eo - copy.toNat) copy.toNat)) } zs
156      { st with wnext := if st.wnext + copy == st.wsize then 0 else st.wnext + copy,
157                whave := if st.whave < st.wsize then st.whave + copy else st.whave }) := by
158  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
159  have hws0 : (st.wsize == 0) = false := by simpa using hpos
160  have hpn : copy.toNat < st.wsize.toNat - st.wnext.toNat := by
161    have he := UInt32.lt_iff_toNat_lt.mp hp
162    rwa [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)] at he
163  have hadd : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) h =
164      .ok (Ptr.ref (BRef.blk w) st.wnext.toNat, h) := by
165    have he := Ptr.add_nat_ok (a := a) (r := BRef.blk w) (off := 0) (n := st.wnext.toNat)
166      (by simpa using ha) (by omega)
167    unfold OkOn at he
168    simpa using he
169  have hsub : Ptr.add (Ptr.ref source eo) (-(copy.toNat : Int)) h =
170      .ok (Ptr.ref source (eo - copy.toNat), h) := Ptr.sub_nat_ok hs hfit hoff
171  have hdis := uw_small_public_separation (source := source) (w := w) (wn := st.wnext.toNat)
172    (size := st.wsize.toNat) (copy := copy.toNat) (eo := eo)
173    hfit (by omega) (by simpa only [hw] using hsep)
174  have hcp := Ptr.memcpy_ok (rd := BRef.blk w) (rs := source) (od := st.wnext.toNat)
175    (os := eo - copy.toNat) (n := copy.toNat) (da := a) (sa := bytes)
176    (by simpa using ha) hs (by simpa using hro) (by omega) (by omega) hdis
177  have hcp' : memcpyB (.ref (.blk w) st.wnext.toNat) (.ref source (eo - copy.toNat)) copy.toNat h =
178      .ok ((), { h with bytes := upd h.bytes w (some (copyRange a bytes st.wnext.toNat (eo - copy.toNat) copy.toNat)) }) := by
179    simpa [Space.put] using hcp
180  unfold updatewindow
181  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hl.hz, hl.zst, castI, hl.hs, hwnl, hws0,
182    Bool.false_eq_true, ite_false]
183  simp only [ge_iff_le, hlt, ite_false, hp, ite_true, bind_app, hw, hadd, hsub,
184    UInt32.sub_self, bne_self_eq_false, Bool.false_eq_true]
185  simp only [hcp', wrI_eq, pure_app, hl.hs]
186  by_cases c1 : st.wnext + copy = st.wsize <;> by_cases c2 : st.whave < st.wsize <;>
187    simp [c1, c2, wrI_eq, hl.hs, setI, hw]
188
189/-- `updatewindow` copies a short source ending exactly at the window end.
190The public separation condition permits any readable object, including a
191disjoint slice in the window allocation. -/
192theorem uw_core_small3_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
193    {st : InflateState} {w eo : Nat} {source : BRef} {a bytes : Array UInt8} {copy : UInt32}
194    (hl : Live h r zs z st) (hw : st.window = .ref (.blk w) 0)
195    (ha : h.bytes w = some a) (hro : h.ro w = false)
196    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size)
197    (hwn : st.wnext.toNat < st.wsize.toNat) (hs : Space.get h source = some bytes)
198    (hfit : copy.toNat ≤ eo) (hoff : eo ≤ bytes.size)
199    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
200      st.window st.wsize.toNat)
201    (hlt : ¬ st.wsize ≤ copy) (hq : ¬ st.wsize - st.wnext > copy)
202    (hr : copy - (st.wsize - st.wnext) = 0) :
203    updatewindow (some r) (.ref source eo) copy h = .ok (0, setI
204      { h with bytes := upd h.bytes w (some (copyRange a bytes st.wnext.toNat (eo - copy.toNat)
205        (st.wsize - st.wnext).toNat)) } zs
206      { st with wnext := 0, whave := if st.whave < st.wsize then st.whave + (st.wsize - st.wnext) else st.whave }) := by
207  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
208  have hws0 : (st.wsize == 0) = false := by simpa using hpos
209  have hd : (st.wsize - st.wnext).toNat = st.wsize.toNat - st.wnext.toNat :=
210    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)
211  have hqn : st.wsize.toNat - st.wnext.toNat ≤ copy.toNat := by
212    have he : ¬ copy < st.wsize - st.wnext := hq
213    rw [UInt32.lt_iff_toNat_lt, hd] at he
214    omega
215  have hrn : copy.toNat = st.wsize.toNat - st.wnext.toNat := by
216    have he : (copy - (st.wsize - st.wnext)).toNat = 0 := by rw [hr]; rfl
217    rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le, hd]; omega), hd] at he
218    omega
219  have hcopy : copy = st.wsize - st.wnext := by
220    apply UInt32.toNat_inj.mp
221    rw [hd]
222    exact hrn
223  have hsum : st.wnext + (st.wsize - st.wnext) = st.wsize := by
224    apply UInt32.toNat_inj.mp
225    rw [UInt32.toNat_add, hd]
226    have := st.wsize.toNat_lt
227    rw [Nat.mod_eq_of_lt (by omega)]
228    omega
229  have hadd : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) h =
230      .ok (Ptr.ref (BRef.blk w) st.wnext.toNat, h) := by
231    have he := Ptr.add_nat_ok (a := a) (r := BRef.blk w) (off := 0) (n := st.wnext.toNat)
232      (by simpa using ha) (by omega)
233    unfold OkOn at he
234    simpa using he
235  have hsub : Ptr.add (Ptr.ref source eo) (-(copy.toNat : Int)) h =
236      .ok (Ptr.ref source (eo - copy.toNat), h) := Ptr.sub_nat_ok hs hfit hoff
237  have hdis := uw_small_public_separation (source := source) (w := w) (wn := st.wnext.toNat)
238    (size := st.wsize.toNat) (copy := copy.toNat) (eo := eo)
239    hfit (by omega) (by simpa only [hw] using hsep)
240  have hcp := Ptr.memcpy_ok (rd := BRef.blk w) (rs := source) (od := st.wnext.toNat)
241    (os := eo - copy.toNat) (n := copy.toNat) (da := a) (sa := bytes)
242    (by simpa using ha) hs (by simpa using hro) (by omega) (by omega) hdis
243  have hcp' : memcpyB (.ref (.blk w) st.wnext.toNat) (.ref source (eo - copy.toNat))
244      (st.wsize - st.wnext).toNat h =
245      .ok ((), { h with bytes := upd h.bytes w (some (copyRange a bytes st.wnext.toNat (eo - copy.toNat)
246        (st.wsize - st.wnext).toNat)) }) := by
247    simpa [Space.put, ← hcopy] using hcp
248  unfold updatewindow
249  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hl.hz, hl.zst, castI, hl.hs, hwnl, hws0,
250    Bool.false_eq_true, ite_false]
251  simp only [ge_iff_le, hlt, ite_false, hq, bind_app, hw, hadd, hsub, hcp', hr,
252    bne_self_eq_false, Bool.false_eq_true]
253  by_cases hwh : st.whave < st.wsize <;> simp [hwh, wrI_eq, hl.hs, setI, hw, hsum]
254
255/-- A positive source range separated from a nonempty window either belongs
256to another object or begins beyond the window. -/
257theorem uw_positive_public_separation {w eo size copy : Nat} {source : BRef}
258    (hfit : copy ≤ eo) (hc : 0 < copy) (hs : 0 < size)
259    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy)) copy (.ref (.blk w) 0) size) :
260    BRef.blk w ≠ source ∨ size ≤ eo - copy := by
261  simp only [ZlibF.Spec.Public.Separate] at hsep
262  rcases hsep with h | h | h | h | h
263  · omega
264  · omega
265  · exact Or.inl h.symm
266  · omega
267  · exact Or.inr (by omega)
268
269/-- `updatewindow` wraps a short copy into two segments under the public
270separation condition, including distinct slices of the same allocation. -/
271theorem uw_core_small2_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
272    {st : InflateState} {w eo : Nat} {source : BRef} {a bytes : Array UInt8} {copy : UInt32}
273    (hl : Live h r zs z st) (hw : st.window = .ref (.blk w) 0)
274    (ha : h.bytes w = some a) (hro : h.ro w = false)
275    (hpos : st.wsize ≠ 0) (hsz : st.wsize.toNat ≤ a.size)
276    (hwn : st.wnext.toNat < st.wsize.toNat) (hs : Space.get h source = some bytes)
277    (hfit : copy.toNat ≤ eo) (hoff : eo ≤ bytes.size)
278    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
279      st.window st.wsize.toNat)
280    (hlt : ¬ st.wsize ≤ copy) (hq : ¬ st.wsize - st.wnext > copy)
281    (hr : copy - (st.wsize - st.wnext) ≠ 0) :
282    updatewindow (some r) (.ref source eo) copy h = .ok (0, setI
283      { h with bytes := upd h.bytes w (some (copyRange
284        (copyRange a bytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat)
285        bytes 0 (eo - (copy - (st.wsize - st.wnext)).toNat)
286        (copy - (st.wsize - st.wnext)).toNat)) } zs
287      { st with wnext := copy - (st.wsize - st.wnext), whave := st.wsize }) := by
288  have hwnl : (st.window == Ptr.null) = false := by rw [hw]; simp
289  have hws0 : (st.wsize == 0) = false := by simpa using hpos
290  have hd : (st.wsize - st.wnext).toNat = st.wsize.toNat - st.wnext.toNat :=
291    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)
292  have hqn : st.wsize.toNat - st.wnext.toNat ≤ copy.toNat := by
293    have he : ¬ copy < st.wsize - st.wnext := hq
294    rw [UInt32.lt_iff_toNat_lt, hd] at he
295    omega
296  have hrem : (copy - (st.wsize - st.wnext)).toNat =
297      copy.toNat - (st.wsize.toNat - st.wnext.toNat) := by
298    rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le, hd]; omega), hd]
299  have hlt' : copy.toNat < st.wsize.toNat := by
300    have he : ¬ st.wsize ≤ copy := hlt
301    rw [UInt32.le_iff_toNat_le] at he
302    omega
303  have hrempos : 0 < (copy - (st.wsize - st.wnext)).toNat := by
304    have he : (copy - (st.wsize - st.wnext)).toNat ≠ 0 :=
305      fun hz => hr (UInt32.toNat_inj.mp (by simpa using hz))
306    omega
307  have hsizepos : 0 < st.wsize.toNat := by omega
308  have hcopypos : 0 < copy.toNat := by omega
309  have hdis := uw_positive_public_separation (source := source) (w := w) (eo := eo)
310    (size := st.wsize.toNat) (copy := copy.toNat) hfit hcopypos hsizepos
311    (by simpa only [hw] using hsep)
312  have hadd : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) h =
313      .ok (Ptr.ref (BRef.blk w) st.wnext.toNat, h) := by
314    have he := Ptr.add_nat_ok (a := a) (r := BRef.blk w) (off := 0) (n := st.wnext.toNat)
315      (by simpa using ha) (by omega)
316    unfold OkOn at he
317    simpa using he
318  have hsub : Ptr.add (Ptr.ref source eo) (-(copy.toNat : Int)) h =
319      .ok (Ptr.ref source (eo - copy.toNat), h) := Ptr.sub_nat_ok hs hfit hoff
320  let first := copyRange a bytes st.wnext.toNat (eo - copy.toNat) (st.wsize - st.wnext).toNat
321  let mid : Heap := { h with bytes := upd h.bytes w (some first) }
322  have hcp1 : memcpyB (.ref (.blk w) st.wnext.toNat) (.ref source (eo - copy.toNat))
323      (st.wsize - st.wnext).toNat h = .ok ((), mid) := by
324    have he := Ptr.memcpy_ok (rd := BRef.blk w) (rs := source) (od := st.wnext.toNat)
325      (os := eo - copy.toNat) (n := (st.wsize - st.wnext).toNat) (da := a) (sa := bytes)
326      (by simpa using ha) hs (by simpa using hro) (by omega) (by omega) (by
327        rcases hdis with hn | ha
328        · exact Or.inl hn
329        · exact Or.inr (Or.inl (by omega)))
330    simpa [Space.put, mid, first] using he
331  have hfirstsize : first.size = a.size := size_copyRange ..
332  have hmidwin : Space.get mid (BRef.blk w) = some first := by simp [mid, Space.get]
333  have hmidro : Space.ro mid (BRef.blk w) = false := by simpa [mid, Space.ro] using hro
334  let secondsrc := if source = .blk w then first else bytes
335  have hmidread : Space.get mid source = some secondsrc := by
336    simpa [mid, secondsrc] using window_write_source hs first
337  have hsrcsize : secondsrc.size = bytes.size := by
338    by_cases he : source = .blk w
339    · subst source
340      have hab : bytes = a := Option.some.inj (hs.symm.trans (by simpa using ha))
341      simp [secondsrc, hab, hfirstsize]
342    · simp [secondsrc, he]
343  have hsub2 : Ptr.add (Ptr.ref source eo) (-((copy - (st.wsize - st.wnext)).toNat : Int)) mid =
344      .ok (Ptr.ref source (eo - (copy - (st.wsize - st.wnext)).toNat), mid) :=
345    Ptr.sub_nat_ok hmidread (by omega) (by omega)
346  have hcp2 : memcpyB (.ref (.blk w) 0) (.ref source (eo - (copy - (st.wsize - st.wnext)).toNat))
347      (copy - (st.wsize - st.wnext)).toNat mid = .ok ((),
348        { mid with bytes := upd mid.bytes w (some (copyRange first bytes 0
349          (eo - (copy - (st.wsize - st.wnext)).toNat) (copy - (st.wsize - st.wnext)).toNat)) }) := by
350    have he := Ptr.memcpy_ok (rd := BRef.blk w) (rs := source) (od := 0)
351      (os := eo - (copy - (st.wsize - st.wnext)).toNat)
352      (n := (copy - (st.wsize - st.wnext)).toNat) (da := first) (sa := secondsrc)
353      hmidwin hmidread hmidro (by omega) (by omega) (by
354        rcases hdis with hn | ha
355        · exact Or.inl hn
356        · exact Or.inr (Or.inl (by omega)))
357    have heq : copyRange first secondsrc 0 (eo - (copy - (st.wsize - st.wnext)).toNat)
358        (copy - (st.wsize - st.wnext)).toNat =
359        copyRange first bytes 0 (eo - (copy - (st.wsize - st.wnext)).toNat)
360          (copy - (st.wsize - st.wnext)).toNat := by
361      by_cases heq : source = .blk w
362      · subst source
363        have hab : bytes = a := Option.some.inj (hs.symm.trans (by simpa using ha))
364        subst bytes
365        have hafter : st.wsize.toNat ≤ eo - copy.toNat := by
366          rcases hdis with hn | hb
367          · exact (hn rfl).elim
368          · exact hb
369        simpa [secondsrc, first] using
370          copyRange_second_source_disjoint a a st.wnext.toNat (eo - copy.toNat)
371            (st.wsize - st.wnext).toNat 0 (eo - (copy - (st.wsize - st.wnext)).toNat)
372            (copy - (st.wsize - st.wnext)).toNat (by omega) (by omega) (by omega) (Or.inl (by omega))
373      · simp [secondsrc, heq]
374    simpa [Space.put, heq] using he
375  unfold updatewindow
376  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hl.hz, hl.zst, castI, hl.hs, hwnl, hws0,
377    Bool.false_eq_true, ite_false]
378  simp only [ge_iff_le, hlt, ite_false, hq, bind_app, hw, hadd, hsub, hcp1]
379  have hr' : (copy - (st.wsize - st.wnext) != 0) = true := by simpa using hr
380  simp only [hr', ite_true, bind_app, hsub2, hcp2, wrI_eq, pure_app, hl.hs, hw]
381  simp [mid, first, setI, upd_upd, hl.hs, hw]
382
383#print axioms uw_core_big_any
384#print axioms uw_big_public_separation
385#print axioms uw_core_big_public
386#print axioms uw_small_public_separation
387#print axioms uw_core_small1_public
388#print axioms uw_core_small3_public
389#print axioms copyRange_second_source_disjoint
390#print axioms window_write_source
391#print axioms uw_core_small2_public
392end Zlib.Inflate.Proofs