参考文档 / ZLIB × LEAN
inffast.c.body.lean
此页源文件快照 ·
addcbf08c1f31db7 · 对应提交的原文 ↗本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。
1import ZlibF.Spec.InflateFast
2import ZlibF.Proof.«inffast.c.frame»
3import ZlibF.Proof.«inffast.c.flags»
4import ZlibF.Proof.«inffast.c.advance»
5
6/-!
7# inffast.c: one concrete fast-decoder iteration
8
9The statements here concern the actual translated body and the parent-reviewed
10buffer/table precondition. Format refinement is a separate obligation.
11-/
12
13namespace Zlib.Inffast.Proofs
14open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
15
16variable {e : Env} {c : Ctx}
17
18/-- The reviewed length branch has the full one-iteration postcondition,
19including the six-byte bound that its older format-oriented summary omits. -/
20theorem dolenLen_step_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
21 (l : L) (i o s : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
22 (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
23 (hbroke : l.broke = false) (hagain : l.againL = false) (hx : l.op.toNat ≤ 5)
24 (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
25 (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
26 (hb2 : i = s + 2 → 1 ≤ l.bits.toNat) :
27 Wp (dolenLen c l) (e.heap A msg m) (StepPost e A msg m s o) := by
28 have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
29 have hAb : A.size < 2 ^ 63 := by rw [hAsz]; exact e.hAbig
30 obtain ⟨l', h', hr, hq⟩ := dolenLen_wp hc A msg m l i o s e.hdt hls hA ho hAb hbroke hx hlen hs6 hT hb2
31 refine ⟨l', h', hr, ?_⟩
32 have hag : l'.againL = false := (dolenLen_againL hr).trans hagain
33 obtain ⟨ir, hir1, hir2, hin⟩ := Wp.at_run
34 (dolenLen_advance_wp hc A msg m l i o s e.hdt hls hA ho hAb hbroke hx hlen hs6 hT hb2) hr
35 obtain ⟨i2, lx, S1, _, _, hrb, i3, H3, b3, E, cb, _, _, _, _, _, _, _, _, hend⟩ := hq
36 have hlx := readBits_value_lt hrb
37 have hlen1 : 3 ≤ l.len.toNat + lx := by omega
38 have hlen2 : l.len.toNat + lx ≤ 258 := by omega
39 rcases hend.2.2 with hgood | hbad
40 · obtain ⟨i', xv, rest, _, _, _, hb, hls', _, hh⟩ := hgood
41 have hi' : i' = ir := (Ptr.ref.inj (hls'.hin.symm.trans hin)).2
42 subst ir
43 refine ⟨i', o + (l.len.toNat + lx),
44 matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o (E.val.toNat + xv) (l.len.toNat + lx) A,
45 msg, m, hls', by omega, hir2, by omega, by omega,
46 matchArr_size _ _ _ _ _ _ _ _ _, hh, hag, ?_, ?_, ?_⟩
47 · exact fun j hj => matchArr_frame _ _ _ _ _ _ _ _ _ _ hj
48 · intro _; exact ⟨by omega, rfl, rfl⟩
49 · intro h; simp [hb] at h
50 · obtain ⟨i', p, _, _, hb, hls', hh⟩ := hbad
51 have hi' : i' = ir := (Ptr.ref.inj (hls'.hin.symm.trans hin)).2
52 subst ir
53 refine ⟨i', o, A, p, BAD, hls', by omega, hir2, by omega, by omega,
54 rfl, hh, hag, (fun _ _ => rfl), ?_, ?_⟩
55 · intro h; simp [hb] at h
56 · intro _; exact Or.inr rfl
57
58theorem dolen_eq_len (c : Ctx) (l : L) : dolen c l = (do
59 let mut l := { l with againL := false }
60 -- op = (unsigned)(here->bits);
61 let e ← l.here.load
62 l := { l with op := e.bits.toUInt32 }
63 -- hold >>= op; bits -= op;
64 l := { l with hold := ← shr64 l.hold l.op.toUInt64 }
65 l := { l with bits := l.bits - l.op }
66 -- op = (unsigned)(here->op);
67 let e ← l.here.load
68 l := { l with op := e.op.toUInt32 }
69 -- if (op == 0) { /* literal */
70 if l.op == 0 then
71 -- *out++ = (unsigned char)(here->val);
72 let e ← l.here.load
73 store8 l.out e.val.toUInt8
74 pure { l with out := ← l.out.add 1 }
75 -- else if (op & 16) { /* length base */
76 else if l.op &&& 16 != 0 then
77 -- len = (unsigned)(here->val);
78 let e ← l.here.load
79 l := { l with len := e.val.toUInt32 }
80 -- op &= 15; /* number of extra bits */
81 l := { l with op := l.op &&& 15 }
82 dolenLen c l
83 -- else if ((op & 64) == 0) { /* 2nd level length code */
84 else if l.op &&& 64 == 0 then
85 -- here = lcode + here->val + (hold & ((1U << op) - 1));
86 let e ← l.here.load
87 let h1 ← c.lcode.add e.val.toNat
88 let m ← shl32 1 l.op
89 let here ← h1.add (l.hold &&& (m - 1).toUInt64).toNat
90 -- goto dolen;
91 pure { l with here, againL := true }
92 -- else if (op & 32) { /* end-of-block */
93 else if l.op &&& 32 != 0 then
94 -- state->mode = TYPE; break;
95 let s ← ldInflateState c.state
96 stInflateState c.state { s with mode := TYPE }
97 pure { l with broke := true }
98 else
99 -- strm->msg = "invalid literal/length code"; state->mode = BAD; break;
100 badData c "invalid literal/length code"
101 pure { l with broke := true }) := by rfl
102
103theorem mask0 : ∀ x : UInt8, (x.toUInt32 == 0) = (x == 0) :=
104 u8_forall _ (by decide +kernel)
105
106set_option maxHeartbeats 1000000 in
107/-- One actual length-table pass either follows its one permitted link or
108establishes the reviewed body postcondition. -/
109theorem dolen_pass_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
110 (l : L) (i o s d k : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
111 (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
112 (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
113 (hb15 : 15 ≤ l.bits.toNat + d) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat + d)
114 (hhere : l.here = .ref e.rl k) (hk : k < e.LCA.size)
115 (hEb : (e.LCA.getD k default).bits.toNat ≤ l.bits.toNat)
116 (hEd : (e.LCA.getD k default).bits.toNat + d ≤ 15)
117 (hcl : (LenLink (e.LCA.getD k default) ∧ LinkOK LenLeaf e.LCA e.ol (e.LCA.getD k default)) ∨
118 LenLeaf d (e.LCA.getD k default)) :
119 Wp (dolen c l) (e.heap A msg m) (fun l' h' =>
120 (l'.againL = true ∧ l'.broke = false ∧ h' = e.heap A msg m ∧
121 LenLink (e.LCA.getD k default) ∧
122 ∃ j, j < 2 ^ (e.LCA.getD k default).op.toNat ∧
123 l'.here = .ref e.rl (e.ol + (e.LCA.getD k default).val.toNat + j) ∧
124 LS e l' i o ∧ l'.bits.toNat = l.bits.toNat - (e.LCA.getD k default).bits.toNat) ∨
125 StepPost e A msg m s o l' h') := by
126 have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
127 have hkE : e.LCA[k]'hk = e.LCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
128 have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.LCA.getD k default) := by
129 rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_LCA A msg m) hk
130 have hEbn : (e.LCA.getD k default).bits.toUInt32.toNat = (e.LCA.getD k default).bits.toNat := toNat32 _
131 have hEb64 : (e.LCA.getD k default).bits.toUInt32.toUInt64.toNat = (e.LCA.getD k default).bits.toNat := by simp [toNat32]
132 have hls1 := hls.dropL (e.LCA.getD k default).bits.toUInt32 (by omega) (by omega)
133 rw [dolen_eq_len]
134 dsimp only
135 refine Wp.bindO hld ?_
136 refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
137 refine Wp.bindO hld ?_
138 generalize e.LCA.getD k default = E at *
139 by_cases hz : (E.op.toUInt32 == 0) = true
140 · simp only [hz, ite_true]
141 refine Wp.bindO hld ?_
142 have hst : store8 l.out E.val.toUInt8 (e.heap A msg m) =
143 .ok ((), e.heap (A.set! o E.val.toUInt8) msg m) := by
144 rw [hls.hout, ← e.heap_put A (A.set! o E.val.toUInt8) msg m]
145 exact Ptr.store_ok (e.heap_bytes_ob A msg m) (e.heap_ro_ob A msg m) (by omega)
146 refine Wp.bindE hst ?_
147 refine Wp.bindO (x := Ptr.ref (BRef.blk e.ob) (o + 1)) ?_ ?_
148 · rw [hls.hout]
149 exact Ptr.add_nat_ok (e.heap_bytes_ob _ msg m) (by simp; omega)
150 · refine Wp.pure' (Or.inr ?_)
151 refine ⟨i, o + 1, A.set! o E.val.toUInt8, msg, m, ?_, hsi, by omega, by omega, by omega,
152 by simp, rfl, rfl, ?_, ?_, ?_⟩
153 · exact ⟨hls.hin, rfl, hls.hi0, hls.hi1, by have := hls.ho0; omega, hls1.hb, hls1.hH, hls1.hacc⟩
154 · intro j hj
155 have hne : o ≠ j := by omega
156 simp [Array.set!, hne]
157 · intro _; exact ⟨by omega, rfl, rfl⟩
158 · intro h; simp [hbroke] at h
159 · have hz' : E.op ≠ 0 := by rw [mask0] at hz; simpa using hz
160 by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
161 · simp only [hz, hb16, ite_true, ite_false, Bool.false_eq_true]
162 have hb16' : E.op &&& 16 ≠ 0 := by rw [mask16] at hb16; simpa using hb16
163 have hbase : (E.op &&& 15).toNat ≤ 5 ∧ 3 ≤ E.val.toNat ∧
164 E.val.toNat + 2 ^ (E.op &&& 15).toNat ≤ 259 := by
165 rcases hcl with h | h
166 · exact False.elim (hb16' h.1.2.1)
167 · rcases h.2 with h0 | h | h
168 · exact False.elim (hz' h0)
169 · exact h.2
170 · exact False.elim (hb16' h.1)
171 refine Wp.bindO hld ?_
172 refine Wp.mono (dolenLen_step_wp hc A msg m
173 { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
174 here := l.here, op := E.op.toUInt32 &&& 15, len := E.val.toUInt32, dist := l.dist, from_ := l.from_,
175 broke := l.broke, againL := false, againD := l.againD }
176 i o s (LS.congr hls1 rfl rfl rfl rfl) hAsz ho hbroke rfl
177 (by rw [mask15]; exact hbase.1) (by simpa [mask15] using hbase.2)
178 hs6 hsi hT (by intro hi; have := hbi2 hi; show 1 ≤ (l.bits - E.bits.toUInt32).toNat
179 rw [u32_toNat_sub (by omega), hEbn]; omega)) ?_
180 exact fun _ _ h => Or.inr h
181 · have hb16' : E.op &&& 16 = 0 := by rw [mask16] at hb16; simpa using hb16
182 by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
183 · simp only [hz, hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
184 have hb64' : E.op &&& 64 = 0 := by rw [mask64] at hb64; simpa using hb64
185 have hl : LenLink E := ⟨hz', hb16', hb64'⟩
186 have hlk : LinkOK LenLeaf e.LCA e.ol E := by
187 rcases hcl with h | h
188 · exact h.2
189 · rcases h.2 with h0 | h | h
190 · exact False.elim (hz' h0)
191 · exact False.elim (h.1 hb16')
192 · exact False.elim (h.2 hb64')
193 refine Wp.bindO hld ?_
194 have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
195 have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; have := hlk.2.2.1; omega
196 refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat)) ?_ ?_
197 · rw [hlc]
198 exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol)
199 (n := E.val.toNat) (e.heap_cget_LCA A msg m)
200 (Nat.le_trans (Nat.le_add_right _ _) hlk.2.2.2.1)
201 refine Wp.bindO (shl32_ok hop32) ?_
202 have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
203 have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
204 rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
205 generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
206 refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat + j)) ?_ ?_
207 · rw [hlow]
208 exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol + E.val.toNat)
209 (n := j) (e.heap_cget_LCA A msg m) (by have := hlk.2.2.2.1; omega)
210 refine Wp.pure' (Or.inl ⟨rfl, hbroke, rfl, hl, j, hjlt, rfl,
211 LS.congr hls1 rfl rfl rfl rfl, ?_⟩)
212 rw [u32_toNat_sub (by omega), hEbn]
213 · simp only [hz, hb16, hb64, ite_false, Bool.false_eq_true]
214 by_cases hb32 : (E.op.toUInt32 &&& 32 != 0) = true
215 · simp only [hb32, ite_true]
216 refine Wp.bindE (e.heap_ldstate hc A msg m) ?_
217 refine Wp.bindE (e.heap_stmode hc A msg m TYPE _ rfl) ?_
218 refine Wp.pure' (Or.inr ?_)
219 refine ⟨i, o, A, msg, TYPE, LS.congr hls1 rfl rfl rfl rfl, hsi, by omega, by omega, by omega,
220 rfl, rfl, rfl, (fun _ _ => rfl), ?_, (fun _ => Or.inl rfl)⟩
221 intro h; cases h
222 · simp only [hb32, ite_false, Bool.false_eq_true]
223 obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid literal/length code" (by decide +kernel)
224 refine Wp.bindE hip ?_
225 refine Wp.pure' (Or.inr ?_)
226 refine ⟨i, o, A, .ref (BRef.str ip) 0, BAD, LS.congr hls1 rfl rfl rfl rfl, hsi, by omega, by omega, by omega,
227 rfl, rfl, rfl, (fun _ _ => rfl), ?_, (fun _ => Or.inr rfl)⟩
228 intro h; cases h
229
230theorem StepPost.againL {A : Array UInt8} {msg : BPtr} {m : UInt32} {i o : Nat} {l : L} {h : Heap}
231 (hp : StepPost e A msg m i o l h) : l.againL = false := by
232 obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, hf, _⟩ := hp
233 exact hf
234
235/-- The actual `dolen` root/link loop ends after at most two passes. -/
236theorem dolenLoop_step_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
237 (l : L) (i o s kidx : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
238 (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
239 (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
240 (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat)
241 (hk : kidx < 2 ^ e.s0.lenbits.toNat) (hhere : l.here = .ref e.rl (e.ol + kidx)) :
242 Wp (cdoWhile (dolen c) (fun l => pure (l.againL, l)) l) (e.heap A msg m)
243 (StepPost e A msg m s o) := by
244 have hts := e.hlt
245 obtain ⟨hR, hsz, hall⟩ := hts
246 have hksz : e.ol + kidx < e.LCA.size := by omega
247 have hclass : (LenLink (e.LCA.getD (e.ol + kidx) default) ∧
248 LinkOK LenLeaf e.LCA e.ol (e.LCA.getD (e.ol + kidx) default)) ∨
249 LenLeaf 0 (e.LCA.getD (e.ol + kidx) default) := by
250 have hh := hall kidx hk
251 by_cases hl : LenLink (e.LCA.getD (e.ol + kidx) default)
252 · rw [ite_eq_left hl] at hh; exact Or.inl ⟨hl, hh⟩
253 · rw [ite_eq_right hl] at hh; exact Or.inr hh
254 have hEd0 : (e.LCA.getD (e.ol + kidx) default).bits.toNat + 0 ≤ 15 := by
255 rcases hclass with h | h
256 · exact h.2.1
257 · exact h.1
258 obtain ⟨l1, h1, e1, hq1⟩ := dolen_pass_wp hc A msg m l i o s 0 (e.ol + kidx) hls hAsz ho hbroke
259 hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega) hhere hksz (by omega) hEd0 hclass
260 generalize hE0 : e.LCA.getD (e.ol + kidx) default = E0 at hq1 hclass hEd0
261 rcases hq1 with ⟨hag, hbr, hh, hlink, j, hjlt, hhere1, hls1, hb1⟩ | hend
262 · subst hh
263 have hlk : LinkOK LenLeaf e.LCA e.ol E0 := by
264 rcases hclass with h | h
265 · exact h.2
266 · rcases h.2 with h0 | h | h
267 · exact False.elim (hlink.1 h0)
268 · exact False.elim (h.1 hlink.2.1)
269 · exact False.elim (h.2 hlink.2.2)
270 have hleaf := hlk.2.2.2.2 j hjlt
271 have hk2 : e.ol + E0.val.toNat + j < e.LCA.size := by have := hlk.2.2.2.1; omega
272 obtain ⟨l2, h2, e2, hq2⟩ := dolen_pass_wp hc A msg m l1 i o s E0.bits.toNat (e.ol + E0.val.toNat + j)
273 hls1 hAsz ho hbr hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega)
274 hhere1 hk2 (by have := hleaf.1; omega) hleaf.1 (Or.inr hleaf)
275 rcases hq2 with ⟨_, _, _, hl2, _⟩ | hend2
276 · rcases hleaf.2 with h0 | h | h
277 · exact False.elim (hl2.1 h0)
278 · exact False.elim (h.1 hl2.2.1)
279 · exact False.elim (h.2 hl2.2.2)
280 · have c1 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l1 (e.heap A msg m) =
281 .ok ((true, l1), e.heap A msg m) := by simp [hag]
282 have c2 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l2 h2 =
283 .ok ((false, l2), h2) := by simp [StepPost.againL hend2]
284 exact Wp.of_eq (cdoWhile_two e1 c1 e2 c2) hend2
285 · have c1 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l1 h1 =
286 .ok ((false, l1), h1) := by simp [StepPost.againL hend]
287 exact Wp.of_eq (cdoWhile_one e1 c1) hend
288
289/-- Root-table lookup followed by the actual length root/link loop. -/
290theorem dolenRoot_step_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
291 (l : L) (i o s : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
292 (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
293 (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
294 (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat) :
295 Wp (do
296 let here ← c.lcode.add (l.hold &&& c.lmask.toUInt64).toNat
297 cdoWhile (dolen c) (fun l => pure (l.againL, l)) {l with here})
298 (e.heap A msg m) (StepPost e A msg m s o) := by
299 have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
300 have hR : e.s0.lenbits.toNat < 32 := by have := e.hlt.1; omega
301 have hmask : c.lmask.toUInt64.toNat = 2 ^ e.s0.lenbits.toNat - 1 := by
302 rw [hc.lmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
303 have hidx := u64_and_mask (x := l.hold) hmask
304 have hmod : l.hold.toNat % 2 ^ e.s0.lenbits.toNat < 2 ^ e.s0.lenbits.toNat :=
305 Nat.mod_lt _ (Nat.pow_pos (by omega))
306 refine Wp.bindO (x := Ptr.ref e.rl (e.ol + l.hold.toNat % 2 ^ e.s0.lenbits.toNat)) ?_ ?_
307 · rw [hlc, hidx]
308 exact Ptr.add_nat_ok (e.heap_cget_LCA A msg m) (by have := e.hlt.2.1; omega)
309 · exact dolenLoop_step_wp hc A msg m _ i o s _ (LS.congr hls rfl rfl rfl rfl) hAsz ho hbroke
310 hs6 hsi hT hb15 hbi2 hmod rfl
311
312/-- Safety, frame, exact margins and positive output on continuation for one
313actual translated `inflate_fast_body` execution. This proves the unchanged
314parent-authored `Goal.step_safe`, not a model execution assumption. -/
315theorem inflate_fast_body_step_safe : Goal.step_safe := by
316 intro e c A msg m l i o hp
317 rcases hp with ⟨hc, hls, hAsz, hi6, ho258, hbroke⟩
318 change Wp (inflate_fast_body c l) (e.heap A msg m) (StepPost e A msg m i o)
319 unfold inflate_fast_body
320 by_cases h1 : l.bits < 15
321 · simp only [h1, ite_true]
322 have hb : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
323 have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
324 refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
325 have hl1 := hls.pullL (by omega) hiin
326 have hb1 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
327 have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
328 have hb1' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
329 simp only [pullL] at hb1 ⊢; omega
330 refine Wp.bindO (pull_run e _ _ (i + 1) o hl1 hb1' hi2 (e.heap_bytes_in A msg m)) ?_
331 have hl2 := hl1.pullL hb1' hi2
332 have hb2 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)))
333 (e.IN.getD (i + 1) 0) (.ref (BRef.blk e.ib) (i + 1 + 1)) hl1.hb
334 exact dolenRoot_step_wp hc A msg m _ (i + 1 + 1) o i hl2 hAsz ho258 hbroke hi6 (by omega) (by omega)
335 (by simp only [pullL] at hb1 hb2 ⊢; omega)
336 (by intro _; simp only [pullL] at hb1 hb2 ⊢; omega)
337 · simp only [h1, ite_false]
338 have hb : 15 ≤ l.bits.toNat := by
339 have : ¬ l.bits.toNat < 15 := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
340 omega
341 exact dolenRoot_step_wp hc A msg m l i o i hls hAsz ho258 hbroke hi6 (by omega) (by omega) hb (by omega)
342
343end Zlib.Inffast.Proofs