inffast.c.body.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

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