REFERENCE / ZLIB × LEAN
inffast.c.match.lean
Source snapshot ·
e9016a4db4b4f74f · Source at the matching commit ↗Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.
1import ZlibF.Proof.«inffast.c.copy»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec
5
6/-- The offset of `beg` in the output block: `next_out - (start - avail_out)`. -/
7def Env.bg (e : Env) : Nat := e.o0 - (e.start.toNat - e.sm0.avail_out.toNat)
8
9/-- The context `c` that `inflate_fast` builds is the one the situation `e` describes. -/
10structure CtxOK (e : Env) (c : Ctx) : Prop where
11 strm : c.strm = e.strm
12 state : c.state = some (InflateStateRef.tab e.stid)
13 last : c.last = .ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)
14 beg : c.beg = .ref (BRef.blk e.ob) e.bg
15 end_ : c.end_ = .ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)
16 wsize : c.wsize = e.s0.wsize
17 whave : c.whave = e.s0.whave
18 wnext : c.wnext = e.s0.wnext
19 window : c.window = e.s0.window
20 lcode : c.lcode = e.s0.lencode
21 dcode : c.dcode = e.s0.distcode
22 lmask : c.lmask = ((1 : UInt32) <<< e.s0.lenbits) - 1
23 dmask : c.dmask = ((1 : UInt32) <<< e.s0.distbits) - 1
24
25/-- The output block after a match copy: `len` bytes, `dist` back, with `o - bg` bytes of the current call before `o`
26and the window (`W` at offset `woff`, ring of size `wsize`, next write position `wnext`) before that. This follows
27the case split of `copyMatch`. -/
28def matchArr (wsize wnext woff : Nat) (W : Array UInt8) (bg o dist len : Nat) (A : Array UInt8) : Array UInt8 :=
29 if o - bg < dist then
30 let op := dist - (o - bg)
31 if wnext = 0 then
32 if op < len then cpyN (len - op) (o + op - dist) (o + op) (blitN W op (woff + wsize - op) o A)
33 else blitN W len (woff + wsize - op) o A
34 else if wnext < op then
35 if op - wnext < len then
36 if wnext < len - (op - wnext) then
37 cpyN (len - (op - wnext) - wnext) (o + (op - wnext) + wnext - dist) (o + (op - wnext) + wnext)
38 (blitN W wnext woff (o + (op - wnext)) (blitN W (op - wnext) (woff + wsize + wnext - op) o A))
39 else blitN W (len - (op - wnext)) woff (o + (op - wnext)) (blitN W (op - wnext) (woff + wsize + wnext - op) o A)
40 else blitN W len (woff + wsize + wnext - op) o A
41 else
42 if op < len then cpyN (len - op) (o + op - dist) (o + op) (blitN W op (woff + wnext - op) o A)
43 else blitN W len (woff + wnext - op) o A
44 else cpyN len (o - dist) o A
45
46theorem matchArr_size (wsize wnext woff : Nat) (W : Array UInt8) (bg o dist len : Nat) (A : Array UInt8) :
47 (matchArr wsize wnext woff W bg o dist len A).size = A.size := by
48 unfold matchArr
49 dsimp only
50 repeat' split
51 all_goals simp [blitN_size, cpyN_size]
52
53
54variable {e : Env} {c : Ctx}
55
56theorem Env.heap_ldstate (hc : CtxOK e c) (A msg m) :
57 ldInflateState c.state (e.heap A msg m) = .ok ({ e.s0 with mode := m }, e.heap A msg m) := by
58 rw [hc.state]
59 apply ldInflateState_ok
60 simp [InflateStateRef.get, e.heap_istates]
61
62theorem Env.heap_ldstrm (hc : CtxOK e c) (A msg m) :
63 ldZStream c.strm (e.heap A msg m) = .ok ({ e.sm0 with msg := msg }, e.heap A msg m) := by
64 rw [hc.strm, e.hstrm]
65 exact ldZStream_ok (e.heap_rget A msg m)
66
67/-- Setting the mode of the state: the heap `e.heap A msg m` becomes `e.heap A msg m'`. -/
68theorem Env.heap_stmode (hc : CtxOK e c) (A msg m m') (s : InflateState) (hs : s = { e.s0 with mode := m' }) :
69 stInflateState c.state s (e.heap A msg m) = .ok ((), e.heap A msg m') := by
70 rw [hc.state, hs]
71 have hg : (InflateStateRef.tab e.stid).get (e.heap A msg m) = some { e.s0 with mode := m } := by
72 simp [InflateStateRef.get, e.heap_istates]
73 rw [stInflateState_ok hg rfl, InflateStateRef.put_tab (by simpa [InflateStateRef.get] using hg)]
74 unfold Env.heap
75 rw [put_istates_comm]
76 simp only [put_istates, upd_upd]
77
78theorem Env.heap_stmsg (hc : CtxOK e c) (A msg m) (p : BPtr) (sm : ZStream) (hs : sm = { e.sm0 with msg := p }) :
79 stZStream c.strm sm (e.heap A msg m) = .ok ((), e.heap A p m) := by
80 rw [hc.strm, e.hstrm, hs]
81 rw [stZStream_ok (e.heap_rget A msg m) e.hrw]
82 unfold Env.heap
83 have hg : e.r.get { e.h0 with bytes := upd e.h0.bytes e.ob (some A), istates := upd e.h0.istates e.stid (some { e.s0 with mode := m }) } = some e.sm0 := by
84 have := e.hsm
85 cases hr : e.r <;> (rw [hr] at this; simpa [ZStreamRef.get] using this)
86 rw [put_put _ _ e.sm0 _ _ hg]
87
88/-- `strm->msg = "..."; state->mode = BAD;` -/
89theorem badData_run (hc : CtxOK e c) (A msg m) (s : String) (hs : s ∈ strTable) :
90 ∃ i, badData c s (e.heap A msg m) = .ok ((), e.heap A (.ref (BRef.str i) 0) BAD) := by
91 obtain ⟨i, hi, _⟩ := strLitRef_of_mem (h := e.heap A msg m) hs
92 refine ⟨i, ?_⟩
93 unfold badData Zlib.Zutil.strLit
94 rw [bind_ok hi, bind_ok (e.heap_ldstrm hc A msg m), bind_ok (e.heap_stmsg hc A msg m _ _ rfl),
95 bind_ok (e.heap_ldstate hc A _ m), e.heap_stmode hc A _ m BAD _ rfl]
96
97
98/-- `copyMatch`: either the match is copied (the output block becomes `matchArr ..`, `out` advances by `len`), or the
99distance is too far back (message and mode `BAD`, `broke`). -/
100theorem copyMatch_run (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (o : Nat)
101 (hout : l.out = .ref (BRef.blk e.ob) o) (hbg : e.bg ≤ o) (hop : l.op.toNat = o - e.bg)
102 (hdist : 1 ≤ l.dist.toNat) (hlen : 3 ≤ l.len.toNat) (hroom : o + l.len.toNat ≤ A.size)
103 (hbroke : l.broke = false) :
104 Wp (copyMatch c l) (e.heap A msg m) (fun l' h' =>
105 l'.in_ = l.in_ ∧ l'.hold = l.hold ∧ l'.bits = l.bits ∧ l'.againL = l.againL ∧ l'.againD = l.againD ∧
106 ((l'.broke = false ∧ l'.out = .ref (BRef.blk e.ob) (o + l.len.toNat) ∧
107 h' = e.heap (matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o l.dist.toNat l.len.toNat A) msg m) ∨
108 (l'.broke = true ∧ ∃ p, h' = e.heap A p BAD ∧ l'.out = l.out))) := by
109 have hoA : o ≤ A.size := by omega
110 unfold copyMatch
111 dsimp only
112 by_cases hd : l.dist > l.op
113 · simp only [hd, ite_true]
114 have hd1 : l.op.toNat < l.dist.toNat := UInt32.lt_iff_toNat_lt.mp hd
115 have hop1 : (l.dist - l.op).toNat = l.dist.toNat - (o - e.bg) := by
116 rw [u32_toNat_sub (by omega)]; omega
117 by_cases hw : l.dist - l.op > c.whave
118 · -- too far back
119 simp only [hw, ite_true]
120 refine Wp.bindO (e.heap_ldstate hc A msg m) ?_
121 have hsane : (({ e.s0 with mode := m } : InflateState).sane != 0) = true := by
122 simp only [bne_iff_ne, ne_eq]; exact e.hsane
123 simp only [hsane, ite_true]
124 obtain ⟨i, hi⟩ := badData_run hc A msg m "invalid distance too far back" (by decide +kernel)
125 refine Wp.bindE hi ?_
126 refine Wp.pure' ?_
127 exact ⟨rfl, rfl, rfl, rfl, rfl, Or.inr ⟨rfl, _, rfl, rfl⟩⟩
128 · simp only [hw, ite_false]
129 have hw' : (l.dist - l.op).toNat ≤ c.whave.toNat := by
130 have h1 : ¬ (c.whave < l.dist - l.op) := hw
131 have h2 : ¬ (c.whave.toNat < (l.dist - l.op).toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
132 omega
133 have hwh : c.whave.toNat ≤ c.wsize.toNat := by rw [hc.whave, hc.wsize]; exact e.hwh
134 have hwn : c.wnext.toNat ≤ c.wsize.toNat := by rw [hc.wnext, hc.wsize]; exact e.hwn
135 have hws : c.wsize.toNat ≤ 32768 := by rw [hc.wsize]; exact e.hws
136 have hwne : e.s0.whave ≠ 0 := by
137 intro h0
138 have : c.whave.toNat = 0 := by rw [hc.whave, h0]; rfl
139 omega
140 obtain ⟨hwptr, hwb, hWb, hWsz⟩ := e.hwin hwne
141 have hwptr' : c.window = Ptr.ref (BRef.blk e.wb) e.woff := by rw [hc.window]; exact hwptr
142 have hsrc : Src e e.wb (fun _ => e.W) := Src.win e e.wb e.W hwb hWb
143 have hWg : Space.get (e.heap A msg m) (BRef.blk e.wb) = some e.W := by
144 show (e.heap A msg m).bytes e.wb = some e.W
145 rw [e.heap_bytes_ne A msg m hwb]; exact hWb
146 have hwsz : c.wsize.toNat = e.s0.wsize.toNat := by rw [hc.wsize]
147 have hwnx : c.wnext.toNat = e.s0.wnext.toNat := by rw [hc.wnext]
148 by_cases hn0 : c.wnext = 0
149 · -- (i) the window has not wrapped
150 have hn0' : (c.wnext == 0) = true := by simp [hn0]
151 simp only [hn0', ite_true]
152 have hsubw : (c.wsize - (l.dist - l.op)).toNat = c.wsize.toNat - (l.dist.toNat - (o - e.bg)) := by
153 rw [u32_toNat_sub (by omega), hop1]
154 have hadd : OkOn (e.heap A msg m) (Ptr.add c.window ↑(c.wsize - (l.dist - l.op)).toNat)
155 (Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg))))) := by
156 rw [hwptr', hsubw]
157 exact Ptr.add_nat_ok hWg (by omega)
158 refine Wp.bindO hadd ?_
159 generalize l.dist - l.op = op1 at hop1 hw' hadd ⊢
160 by_cases hlt : op1 < l.len
161 · simp only [hlt, ite_true]
162 have hlt' : op1.toNat < l.len.toNat := UInt32.lt_iff_toNat_lt.mp hlt
163 have hlen1 : (l.len - op1).toNat = l.len.toNat - op1.toNat := u32_toNat_sub (by omega)
164 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A
165 { l with op := op1, len := l.len - op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) }
166 op1.toNat (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) o rfl (by omega) rfl hout
167 (by omega) (by omega)) ?_
168 dsimp only
169 generalize hA1 : blitN e.W op1.toNat (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) o A = A1
170 have hA1sz : A1.size = A.size := by rw [← hA1]; exact blitN_size _ _ _ _ _
171 have hsub2 : OkOn (e.heap A1 msg m) (subn (Ptr.ref (BRef.blk e.ob) (o + op1.toNat)) l.dist)
172 (Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat)) :=
173 subn_ok (r := BRef.blk e.ob) (a := A1) (e.heap_bytes_ob A1 msg m) (by omega) (by omega)
174 refine Wp.bindO hsub2 ?_
175 refine Wp.of_eq (a := _) (h' := _) (tailW_run (Src.out e) A1 msg m
176 { l with out := Ptr.ref (BRef.blk e.ob) (o + op1.toNat), op := 0, len := l.len - op1,
177 from_ := Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat) }
178 (l.len - op1).toNat (o + op1.toNat - l.dist.toNat) (o + op1.toNat) rfl rfl rfl (by simp; omega)
179 (by omega)) ?_
180 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, ?_, ?_⟩⟩
181 · simp only [hlen1]; rw [show o + op1.toNat + (l.len.toNat - op1.toNat) = o + l.len.toNat by omega]
182 · simp only [hlen1]
183 rw [cpyG_id]
184 unfold matchArr
185 have h1 : o - e.bg < l.dist.toNat := by omega
186 have h2 : e.s0.wnext.toNat = 0 := by rw [← hwnx]; rw [hn0]; rfl
187 simp only [h1, h2, hwsz, ite_true]
188 have h3 : op1.toNat = l.dist.toNat - (o - e.bg) := hop1
189 have h4 : op1.toNat < l.len.toNat := by omega
190 have h4' : l.dist.toNat - (o - e.bg) < l.len.toNat := by omega
191 have h5 : e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg))) =
192 e.woff + e.s0.wsize.toNat - (l.dist.toNat - (o - e.bg)) := by omega
193 simp only [h3, h4'] at hA1 ⊢
194 rw [h5] at hA1
195 rw [← hA1]
196 try simp
197 · simp only [hlt, ite_false]
198 have hlt' : l.len.toNat ≤ op1.toNat := by
199 have h1 : ¬ (op1 < l.len) := hlt
200 have h2 : ¬ (op1.toNat < l.len.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
201 omega
202 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A msg m
203 { l with op := op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) }
204 l.len.toNat (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) o rfl rfl hout
205 (by show _ ≤ e.W.size; omega) (by omega)) ?_
206 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, rfl, ?_⟩⟩
207 rw [cpyG_const]
208 unfold matchArr
209 have h1 : o - e.bg < l.dist.toNat := by omega
210 have h2 : e.s0.wnext.toNat = 0 := by rw [← hwnx]; rw [hn0]; rfl
211 have h3 : op1.toNat = l.dist.toNat - (o - e.bg) := hop1
212 have h4' : ¬ (l.dist.toNat - (o - e.bg) < l.len.toNat) := by omega
213 have h5 : e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg))) =
214 e.woff + e.s0.wsize.toNat - (l.dist.toNat - (o - e.bg)) := by omega
215 simp only [h1, h2, h4', ite_true, ite_false, h5]
216 · -- the window has wrapped (ii) or the data is contiguous (iii)
217 have hn0' : (c.wnext == 0) = false := by simp [hn0]
218 simp only [hn0']
219 have hn0n : 0 < c.wnext.toNat := by
220 have : c.wnext.toNat ≠ 0 := fun h => hn0 (UInt32.toNat_inj.mp (by simpa using h))
221 omega
222 by_cases hwl : c.wnext < l.dist - l.op
223 · -- (ii)
224 simp only [hwl, ite_true]
225 have hwl' : c.wnext.toNat < (l.dist - l.op).toNat := UInt32.lt_iff_toNat_lt.mp hwl
226 have hsum : (c.wsize + c.wnext).toNat = c.wsize.toNat + c.wnext.toNat := u32_toNat_add (by omega)
227 have hsubw : (c.wsize + c.wnext - (l.dist - l.op)).toNat =
228 c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by
229 rw [u32_toNat_sub (by omega), hsum, hop1]
230 have hadd : OkOn (e.heap A msg m) (Ptr.add c.window ↑(c.wsize + c.wnext - (l.dist - l.op)).toNat)
231 (Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg))))) := by
232 rw [hwptr', hsubw]
233 exact Ptr.add_nat_ok hWg (by omega)
234 refine Wp.bindO hadd ?_
235 generalize l.dist - l.op = op1 at hop1 hw' hadd hwl' ⊢
236 have hop2 : (op1 - c.wnext).toNat = op1.toNat - c.wnext.toNat := u32_toNat_sub (by omega)
237 generalize op1 - c.wnext = op2 at hop2 ⊢
238 have hfo1 : e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg))) =
239 e.woff + e.s0.wsize.toNat + e.s0.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by omega
240 by_cases hlt : op2 < l.len
241 · simp only [hlt, ite_true]
242 have hlt' : op2.toNat < l.len.toNat := UInt32.lt_iff_toNat_lt.mp hlt
243 have hlen1 : (l.len - op2).toNat = l.len.toNat - op2.toNat := u32_toNat_sub (by omega)
244 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A
245 { l with op := op2, len := l.len - op2, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
246 op2.toNat (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl (by omega) rfl hout
247 (by omega) (by omega)) ?_
248 dsimp only
249 generalize hA1 : blitN e.W op2.toNat (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o A = A1
250 have hA1sz : A1.size = A.size := by rw [← hA1]; exact blitN_size _ _ _ _ _
251 by_cases hwl2 : c.wnext < l.len - op2
252 · simp only [hwl2, ite_true]
253 have hwl2' : c.wnext.toNat < (l.len - op2).toNat := UInt32.lt_iff_toNat_lt.mp hwl2
254 have hlen2 : (l.len - op2 - c.wnext).toNat = l.len.toNat - op2.toNat - c.wnext.toNat := by
255 rw [u32_toNat_sub (by omega), hlen1]
256 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A1
257 { l with out := Ptr.ref (BRef.blk e.ob) (o + op2.toNat), op := c.wnext, len := l.len - op2 - c.wnext,
258 from_ := c.window }
259 c.wnext.toNat e.woff (o + op2.toNat) rfl hn0n hwptr' rfl (by omega) (by omega)) ?_
260 dsimp only
261 generalize hA2 : blitN e.W c.wnext.toNat e.woff (o + op2.toNat) A1 = A2
262 have hA2sz : A2.size = A.size := by rw [← hA2]; rw [blitN_size]; exact hA1sz
263 have hsub2 : OkOn (e.heap A2 msg m) (subn (Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat)) l.dist)
264 (Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat - l.dist.toNat)) :=
265 subn_ok (r := BRef.blk e.ob) (a := A2) (e.heap_bytes_ob A2 msg m) (by omega) (by omega)
266 refine Wp.bindO hsub2 ?_
267 refine Wp.of_eq (a := _) (h' := _) (tailW_run (Src.out e) A2 msg m
268 { l with out := Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat), op := 0,
269 len := l.len - op2 - c.wnext,
270 from_ := Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat - l.dist.toNat) }
271 (l.len - op2 - c.wnext).toNat (o + op2.toNat + c.wnext.toNat - l.dist.toNat)
272 (o + op2.toNat + c.wnext.toNat) rfl rfl rfl (by simp; omega) (by omega)) ?_
273 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, ?_, ?_⟩⟩
274 · simp only [hlen2]; rw [show o + op2.toNat + c.wnext.toNat + (l.len.toNat - op2.toNat - c.wnext.toNat) = o + l.len.toNat by omega]
275 · simp only [hlen2]
276 rw [cpyG_id]
277 unfold matchArr
278 have h1 : o - e.bg < l.dist.toNat := by omega
279 have h2 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
280 have h3 : e.s0.wnext.toNat < l.dist.toNat - (o - e.bg) := by rw [← hwnx]; omega
281 have h4 : l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat < l.len.toNat := by rw [← hwnx]; omega
282 have h5 : e.s0.wnext.toNat < l.len.toNat - (l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat) := by
283 rw [← hwnx]; omega
284 simp only [h1, h2, h3, h4, h5, ite_true, ite_false]
285 rw [← hA2, ← hA1, hfo1]
286 have hop2' : op2.toNat = l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat := by omega
287 simp only [hop2', hwnx]
288 · simp only [hwl2, ite_false]
289 have hwl2' : (l.len - op2).toNat ≤ c.wnext.toNat := by
290 have h1 : ¬ (c.wnext < l.len - op2) := hwl2
291 have h2 : ¬ (c.wnext.toNat < (l.len - op2).toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
292 omega
293 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A1 msg m
294 { l with out := Ptr.ref (BRef.blk e.ob) (o + op2.toNat), op := 0, len := l.len - op2, from_ := c.window }
295 (l.len - op2).toNat e.woff (o + op2.toNat) rfl hwptr' rfl (by show _ ≤ e.W.size; omega) (by omega)) ?_
296 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, ?_, ?_⟩⟩
297 · simp only [hlen1]; rw [show o + op2.toNat + (l.len.toNat - op2.toNat) = o + l.len.toNat by omega]
298 · simp only [hlen1]
299 rw [cpyG_const]
300 unfold matchArr
301 have h1 : o - e.bg < l.dist.toNat := by omega
302 have h2 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
303 have h3 : e.s0.wnext.toNat < l.dist.toNat - (o - e.bg) := by rw [← hwnx]; omega
304 have h4 : l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat < l.len.toNat := by rw [← hwnx]; omega
305 have h5 : ¬ (e.s0.wnext.toNat < l.len.toNat - (l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat)) := by
306 rw [← hwnx]; omega
307 simp only [h1, h2, h3, h4, h5, ite_true, ite_false]
308 rw [← hA1, hfo1]
309 have hop2' : op2.toNat = l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat := by omega
310 simp only [hop2', hwnx]
311 · simp only [hlt, ite_false]
312 have hlt' : l.len.toNat ≤ op2.toNat := by
313 have h1 : ¬ (op2 < l.len) := hlt
314 have h2 : ¬ (op2.toNat < l.len.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
315 omega
316 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A msg m
317 { l with op := op2, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
318 l.len.toNat (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl rfl hout
319 (by show _ ≤ e.W.size; omega) (by omega)) ?_
320 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, rfl, ?_⟩⟩
321 rw [cpyG_const]
322 unfold matchArr
323 have h1 : o - e.bg < l.dist.toNat := by omega
324 have h2 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
325 have h3 : e.s0.wnext.toNat < l.dist.toNat - (o - e.bg) := by rw [← hwnx]; omega
326 have h4 : ¬ (l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat < l.len.toNat) := by rw [← hwnx]; omega
327 simp only [h1, h2, h3, h4, ite_true, ite_false]
328 rw [hfo1]
329 · -- (iii)
330 simp only [hwl, ite_false]
331 have hwl' : (l.dist - l.op).toNat ≤ c.wnext.toNat := by
332 have h2 : ¬ (c.wnext.toNat < (l.dist - l.op).toNat) := fun h => hwl (UInt32.lt_iff_toNat_lt.mpr h)
333 omega
334 have hsubw : (c.wnext - (l.dist - l.op)).toNat = c.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by
335 rw [u32_toNat_sub (by omega), hop1]
336 have hadd : OkOn (e.heap A msg m) (Ptr.add c.window ↑(c.wnext - (l.dist - l.op)).toNat)
337 (Ptr.ref (BRef.blk e.wb) (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg))))) := by
338 rw [hwptr', hsubw]
339 exact Ptr.add_nat_ok hWg (by omega)
340 refine Wp.bindO hadd ?_
341 generalize l.dist - l.op = op1 at hop1 hw' hadd hwl' ⊢
342 by_cases hlt : op1 < l.len
343 · simp only [hlt, ite_true]
344 have hlt' : op1.toNat < l.len.toNat := UInt32.lt_iff_toNat_lt.mp hlt
345 have hlen1 : (l.len - op1).toNat = l.len.toNat - op1.toNat := u32_toNat_sub (by omega)
346 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A
347 { l with op := op1, len := l.len - op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
348 op1.toNat (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl (by omega) rfl hout
349 (by omega) (by omega)) ?_
350 dsimp only
351 generalize hA1 : blitN e.W op1.toNat (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o A = A1
352 have hA1sz : A1.size = A.size := by rw [← hA1]; exact blitN_size _ _ _ _ _
353 have hsub2 : OkOn (e.heap A1 msg m) (subn (Ptr.ref (BRef.blk e.ob) (o + op1.toNat)) l.dist)
354 (Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat)) :=
355 subn_ok (r := BRef.blk e.ob) (a := A1) (e.heap_bytes_ob A1 msg m) (by omega) (by omega)
356 refine Wp.bindO hsub2 ?_
357 refine Wp.of_eq (a := _) (h' := _) (tailW_run (Src.out e) A1 msg m
358 { l with out := Ptr.ref (BRef.blk e.ob) (o + op1.toNat), op := 0, len := l.len - op1,
359 from_ := Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat) }
360 (l.len - op1).toNat (o + op1.toNat - l.dist.toNat) (o + op1.toNat) rfl rfl rfl (by simp; omega)
361 (by omega)) ?_
362 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, ?_, ?_⟩⟩
363 · simp only [hlen1]; rw [show o + op1.toNat + (l.len.toNat - op1.toNat) = o + l.len.toNat by omega]
364 · simp only [hlen1]
365 rw [cpyG_id]
366 unfold matchArr
367 have h1 : o - e.bg < l.dist.toNat := by omega
368 have h2 : ¬ (e.s0.wnext.toNat < l.dist.toNat - (o - e.bg)) := by rw [← hwnx]; omega
369 have h3 : op1.toNat = l.dist.toNat - (o - e.bg) := hop1
370 have h4' : l.dist.toNat - (o - e.bg) < l.len.toNat := by omega
371 have h5 : e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg))) =
372 e.woff + e.s0.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by omega
373 have h6 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
374 simp only [h1, h2, h3, h4', h6, ite_true, ite_false] at hA1 ⊢
375 rw [h5] at hA1
376 rw [← hA1]
377 · simp only [hlt, ite_false]
378 have hlt' : l.len.toNat ≤ op1.toNat := by
379 have h1 : ¬ (op1 < l.len) := hlt
380 have h2 : ¬ (op1.toNat < l.len.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
381 omega
382 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A msg m
383 { l with op := op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
384 l.len.toNat (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl rfl hout
385 (by show _ ≤ e.W.size; omega) (by omega)) ?_
386 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, rfl, ?_⟩⟩
387 rw [cpyG_const]
388 unfold matchArr
389 have h1 : o - e.bg < l.dist.toNat := by omega
390 have h2 : ¬ (e.s0.wnext.toNat < l.dist.toNat - (o - e.bg)) := by rw [← hwnx]; omega
391 have h4' : ¬ (l.dist.toNat - (o - e.bg) < l.len.toNat) := by omega
392 have h5 : e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg))) =
393 e.woff + e.s0.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by omega
394 have h6 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
395 simp only [h1, h2, h4', h6, ite_true, ite_false, h5]
396 · simp only [hd, ite_false]
397 have hd' : l.dist.toNat ≤ o - e.bg := by
398 have h1 : ¬ (l.op < l.dist) := hd
399 have h2 : ¬ (l.op.toNat < l.dist.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
400 omega
401 have hsub : OkOn (e.heap A msg m) (subn l.out l.dist) (Ptr.ref (BRef.blk e.ob) (o - l.dist.toNat)) := by
402 rw [hout]; exact subn_ok (r := BRef.blk e.ob) (a := A) (e.heap_bytes_ob A msg m) (by omega) hoA
403 refine Wp.bindO hsub ?_
404 refine Wp.of_eq (a := _) (h' := _) (tailD_run (Src.out e) A msg m
405 { l with from_ := Ptr.ref (BRef.blk e.ob) (o - l.dist.toNat) } l.len.toNat (o - l.dist.toNat) o rfl hlen rfl hout
406 (by simp; omega) (by omega)) ?_
407 have hmb : ¬ (o - e.bg < l.dist.toNat) := by omega
408 refine ⟨rfl, rfl, rfl, rfl, rfl, Or.inl ⟨hbroke, rfl, ?_⟩⟩
409 simp [matchArr, hmb, cpyG_id]
410
411end Zlib.Inffast.Proofs