infback.c.stored.lean

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

1import ZlibF.Proof.«infback.c.pull»
2import ZlibF.Proof.«infback.c.pure»
3import ZlibF.Proof.«infback.c.wf»
4import ZlibF.Proof.«inflate.c.main.stored»
5import ZlibF.Proof.«inflate.c.main.stored2»
6
7/-!
8# infback.c: `ROOM()` on the loop invariant, and `case STORED`
9-/
10
11namespace Zlib.Infback.Proofs
12open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
13
14/-- Registers with the same input fields describe the same chunk. -/
15theorem BIn.regs_eq {ownI : Nat → Prop} {h : Heap} {l l' : IL} {bs : List UInt8} (B : BIn ownI h l bs)
16    (hn : l'.next = l.next) (hh : l'.have_ = l.have_) (hho : l'.hold = l.hold) (hb : l'.bits = l.bits) :
17    BIn ownI h l' bs := by
18  obtain ⟨⟨he, hn', hl⟩, ho⟩ := B
19  refine ⟨⟨by rw [hh]; exact he, by rw [hn]; exact hn', by rw [hho, hb]; exact hl⟩, by rw [hn]; exact ho⟩
20
21/-- Like `LInv.cb`, but the window position may move (`ROOM()` restarts at the window). -/
22theorem LInv.cb' {c : BCtx} {win : Nat} {ownI own : Nat → Prop} {R : Heap → Prop} {r : ZStreamRef} {zs : Nat}
23    {h h' : Heap} {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8} (I : LInv c win ownI R r zs h l z s bs)
24    (F : CbFrame own h h') (hw : ¬ own win) (hR' : R h') {l' : IL} {bs' : List UInt8}
25    (hp : ∃ off, s.window = .ref (.blk win) off ∧ l'.put = .ref (.blk win) (off + (s.wsize.toNat - l'.left.toNat)) ∧
26      l'.left.toNat ≤ s.wsize.toNat) (B' : BIn ownI h' l' bs') (hb : l'.bits.toNat ≤ 39) :
27    LInv c win ownI R r zs h' l' z s bs' := by
28  obtain ⟨hcs, hct, hz, hs, wf, ⟨o1, a, w1, ba, ro, le⟩, pt, B, hR, hb0⟩ := I
29  exact ⟨hcs, hct, by rw [CbFrame.zget F]; exact hz, by rw [F.istates]; exact hs, wf,
30    ⟨o1, a, w1, by rw [F.bytes win hw]; exact ba, by rw [F.ro]; exact ro, le⟩, hp, B', hR', hb⟩
31
32/-- **`ROOM()` on the invariant.** The window is the caller's, so `out` is called on `wsize` readable bytes. Afterwards the
33invariant holds with the state `{ s with whave := w }` (only `whave` changes); on `ok` there is room (`left /= 0`, using
34`wsize /= 0`) and the input registers are as before; on a leave the result is `Z_BUF_ERROR`. -/
35theorem ROOM_inv (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
36    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
37    {r : ZStreamRef} {zs : Nat} {h : Heap} {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8}
38    (I : LInv c win ownI R r zs h l z s bs) (hw0 : 0 < s.wsize.toNat) :
39    ∃ res l' h' w, runX (ROOM c) l h = .ok ((res, l'), h') ∧
40      LInv c win ownI R r zs h' l' z { s with whave := w } bs ∧ phi μ h' l' = phi μ h l ∧
41      l'.next = l.next ∧ l'.have_ = l.have_ ∧ l'.hold = l.hold ∧ l'.bits = l.bits ∧ l'.copy = l.copy ∧
42      (res = .ok () → l'.left ≠ 0) ∧ (∀ e, res = .error e → e = Ex.leave ∧ l'.ret = Z_BUF_ERROR) := by
43  by_cases hl : l.left = 0
44  · obtain ⟨o1, a, w1, ba, ro, le⟩ := I.wnd
45    have hRd : ReadableAt h s.window s.wsize.toNat := ⟨win, o1, a, w1, ba, le⟩
46    obtain ⟨res, l', h', hrun, F, hR', hres⟩ := ROOM_run c hK I.cst I.hs hl I.hR hRd
47    have I1 := Zlib.Infback.Proofs.LInv.setS I { s with whave := s.wsize } rfl rfl rfl rfl rfl (LInv.R_setI hK I.hR zs _)
48    have hsame : ∀ b, ownI b → h'.bytes b = (roomHeap h zs s).bytes b := fun b hb => F.bytes b (hK.disj.2.2 b hb)
49    have Bh : BIn ownI h' l bs := @BIn.congr ownI h h' l bs (fun b hb => hsame b hb) I.bin
50    have Bn : BIn ownI h' l' bs := by
51      rcases hres with ⟨-, e⟩ | ⟨-, e⟩ <;> exact BIn.regs_eq Bh (by rw [e]) (by rw [e]) (by rw [e]) (by rw [e])
52    have hp : ∃ off, ({ s with whave := s.wsize } : InflateState).window = .ref (.blk win) off ∧
53        l'.put = .ref (.blk win) (off + (({ s with whave := s.wsize } : InflateState).wsize.toNat - l'.left.toNat)) ∧
54        l'.left.toNat ≤ ({ s with whave := s.wsize } : InflateState).wsize.toNat := by
55      obtain ⟨off, hw, -, -⟩ := I.put
56      rcases hres with ⟨-, e⟩ | ⟨-, e⟩ <;> rw [e] <;> refine ⟨off, hw, ?_, by simp⟩ <;> simp [hw]
57    have hb39 : l'.bits.toNat ≤ 39 := by
58      have := I.bits; rcases hres with ⟨-, e⟩ | ⟨-, e⟩ <;> rw [e] <;> simpa using this
59    refine ⟨res, l', h', s.wsize, hrun, Zlib.Infback.Proofs.LInv.cb' I1 F hK.disj.2.1 hR' hp Bn hb39, ?_, ?_⟩
60    · simp only [phi]
61      rw [hF.local_ h h' (fun b hb => (hsame b hb))]
62      rcases hres with ⟨-, e⟩ | ⟨-, e⟩ <;> rw [e] <;> rfl
63    · rcases hres with ⟨h1, e⟩ | ⟨h1, e⟩ <;> rw [e]
64      · refine ⟨rfl, rfl, rfl, rfl, rfl, fun _ => ?_, fun e he => ?_⟩
65        · intro hh
66          have hz : s.wsize.toNat = 0 := by rw [show s.wsize = 0 from hh]; rfl
67          omega
68        · rw [h1] at he; cases he
69      · refine ⟨rfl, rfl, rfl, rfl, rfl, fun hh => ?_, fun e he => ?_⟩
70        · rw [h1] at hh; cases hh
71        · rw [h1] at he; cases he; exact ⟨rfl, rfl⟩
72  · refine ⟨.ok (), l, h, s.whave, ROOM_have c hl, ?_, rfl, rfl, rfl, rfl, rfl, rfl, fun _ => hl, fun e he => by cases he⟩
73    · have : ({ s with whave := s.whave } : InflateState) = s := rfl
74      rw [this]; exact I
75
76/-! ## `case STORED` -/
77
78/-- The copy count of `case STORED`: `min(length, have, left)`, written with the two `if`s of the C. -/
79def clampCopy (len hv lf : UInt32) : UInt32 :=
80  let c1 := if len > hv then hv else len
81  if c1 > lf then lf else c1
82
83theorem clampCopy_le (len hv lf : UInt32) : (clampCopy len hv lf).toNat ≤ len.toNat ∧
84    (clampCopy len hv lf).toNat ≤ hv.toNat ∧ (clampCopy len hv lf).toNat ≤ lf.toNat := by
85  unfold clampCopy
86  simp only [GT.gt, UInt32.lt_iff_toNat_lt]
87  split <;> split <;> omega
88
89theorem clampCopy_pos (len hv lf : UInt32) (h1 : len ≠ 0) (h2 : hv ≠ 0) (h3 : lf ≠ 0) : clampCopy len hv lf ≠ 0 := by
90  have e1 : 0 < len.toNat := by
91    apply Nat.pos_of_ne_zero; intro e; exact h1 (UInt32.toNat_inj.mp (by simpa using e))
92  have e2 : 0 < hv.toNat := by
93    apply Nat.pos_of_ne_zero; intro e; exact h2 (UInt32.toNat_inj.mp (by simpa using e))
94  have e3 : 0 < lf.toNat := by
95    apply Nat.pos_of_ne_zero; intro e; exact h3 (UInt32.toNat_inj.mp (by simpa using e))
96  intro e
97  have := congrArg UInt32.toNat e
98  unfold clampCopy at this
99  simp only [GT.gt, UInt32.lt_iff_toNat_lt] at this
100  split at this <;> split at this <;> simp at this <;> omega
101
102/-- The part of the copy loop after `ROOM()`. -/
103def storedTail (c : BCtx) : X Unit := do
104  let l ← get
105  let mut copy := l.copy
106  if copy > l.have_ then copy := l.have_
107  if copy > l.left then copy := l.left
108  memcpyB l.put l.next copy.toNat
109  let nx ← l.next.add (copy.toNat : Int)
110  let pt ← l.put.add (copy.toNat : Int)
111  set { l with copy := copy, have_ := l.have_ - copy, next := nx, left := l.left - copy, put := pt }
112  wrS c.st fun s => { s with length := s.length - copy }
113
114/-- The heap after the copy: `n` bytes written into the window block, and `state->length` set to `L`. -/
115def copiedHeap (h : Heap) (zs win : Nat) (s : InflateState) (da sa : Array UInt8) (od off2 n : Nat) (L : UInt32) : Heap :=
116  setI { h with bytes := upd h.bytes win (some (copyRange da sa od off2 n)) } zs { s with length := L }
117
118/-- The registers after the copy of `n` bytes. -/
119def storedRegs (l : IL) (n : UInt32) (bb off2 win od : Nat) : IL :=
120  { l with copy := n, have_ := l.have_ - n, next := .ref (.blk bb) (off2 + n.toNat), left := l.left - n, put := .ref (.blk win) (od + n.toNat) }
121
122/-- **The copy of one piece.** `n = min(length, have, left)` bytes move from the input chunk (block `bb`) to the window (block
123`win`); the two blocks differ, both ranges are inside their blocks. The heap changes in the window block and in
124`state->length`. -/
125theorem storedTail_run (c : BCtx) {h : Heap} {l : IL} {zs : Nat} {s : InflateState} {bb off2 win od : Nat}
126    {da sa : Array UInt8} (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s)
127    (hput : l.put = .ref (.blk win) od) (hnext : l.next = .ref (.blk bb) off2)
128    (hd : h.bytes win = some da) (hsa : h.bytes bb = some sa) (hro : h.ro win = false) (hne : win ≠ bb)
129    (hhave : l.have_ ≠ 0) (hleft : l.left ≠ 0) (hcopy : l.copy ≠ 0)
130    (h1 : od + l.left.toNat ≤ da.size) (h2 : off2 + l.have_.toNat ≤ sa.size) :
131    runX (storedTail c) l h = .ok ((.ok (), storedRegs l (clampCopy l.copy l.have_ l.left) bb off2 win od),
132      copiedHeap h zs win s da sa od off2 (clampCopy l.copy l.have_ l.left).toNat (s.length - clampCopy l.copy l.have_ l.left)) := by
133  obtain ⟨hn1, hn2, hn3⟩ := clampCopy_le l.copy l.have_ l.left
134  obtain ⟨n, hn⟩ : ∃ n, n = clampCopy l.copy l.have_ l.left := ⟨_, rfl⟩
135  rw [← hn] at hn1 hn2 hn3 ⊢
136  have hmc : memcpyB l.put l.next n.toNat h = .ok ((), { h with bytes := upd h.bytes win (some (copyRange da sa od off2 n.toNat)) }) := by
137    rw [hput, hnext]; exact memcpyB_blk_ok hd hsa hro hne (by omega) (by omega)
138  have hsz : (copyRange da sa od off2 n.toNat).size = da.size := size_copyRange _ _ _ _ _
139  have hdg : (Space.get h (BRef.blk win) : Option (Array UInt8)) = some da := hd
140  have hsg : (Space.get h (BRef.blk bb) : Option (Array UInt8)) = some sa := hsa
141  obtain ⟨a2, ha2, hs2⟩ := get_after_put hd hsz hsg
142  obtain ⟨a3, ha3, hs3⟩ := get_after_put hd hsz hdg
143  have hadd1 : OkOn { h with bytes := upd h.bytes win (some (copyRange da sa od off2 n.toNat)) } (l.next.add (n.toNat : Int))
144      (.ref (.blk bb) (off2 + n.toNat)) := by
145    rw [hnext]; exact Ptr.add_nat_ok ha2 (by omega)
146  have hadd2 : OkOn { h with bytes := upd h.bytes win (some (copyRange da sa od off2 n.toNat)) } (l.put.add (n.toNat : Int))
147      (.ref (.blk win) (od + n.toNat)) := by
148    rw [hput]; exact Ptr.add_nat_ok ha3 (by omega)
149  have hs' : ({ h with bytes := upd h.bytes win (some (copyRange da sa od off2 n.toNat)) } : Heap).istates zs = some s := hs
150  have hw : wrS c.st (fun s => { s with length := s.length - n })
151      { h with bytes := upd h.bytes win (some (copyRange da sa od off2 n.toNat)) } =
152      .ok ((), setI { h with bytes := upd h.bytes win (some (copyRange da sa od off2 n.toNat)) } zs
153        { s with length := s.length - n }) := wrS_ok hc hs' _
154  unfold storedTail storedRegs copiedHeap
155  rw [runX_bind, runX_get]
156  by_cases e1 : l.copy > l.have_
157  · by_cases e2 : l.have_ > l.left
158    · have hv : n = l.left := by rw [hn]; simp only [clampCopy, e1, e2, ↓reduceIte]
159      subst hv
160      simp only [e1, e2, ↓reduceIte, runX_bind, runX_lift_ok hmc, runX_lift_ok hadd1, runX_lift_ok hadd2, runX_set,
161        runX_lift_ok hw]
162    · have hv : n = l.have_ := by rw [hn]; simp only [clampCopy, e1, e2, ↓reduceIte]
163      subst hv
164      simp only [e1, e2, ↓reduceIte, runX_bind, runX_lift_ok hmc, runX_lift_ok hadd1, runX_lift_ok hadd2, runX_set,
165        runX_lift_ok hw]
166  · by_cases e2 : l.copy > l.left
167    · have hv : n = l.left := by rw [hn]; simp only [clampCopy, e1, e2, ↓reduceIte]
168      subst hv
169      simp only [e1, e2, ↓reduceIte, runX_bind, runX_lift_ok hmc, runX_lift_ok hadd1, runX_lift_ok hadd2, runX_set,
170        runX_lift_ok hw]
171    · have hv : n = l.copy := by rw [hn]; simp only [clampCopy, e1, e2, ↓reduceIte]
172      subst hv
173      simp only [e1, e2, ↓reduceIte, runX_bind, runX_lift_ok hmc, runX_lift_ok hadd1, runX_lift_ok hadd2, runX_set,
174        runX_lift_ok hw]
175
176/-- The loop body of `case STORED`. -/
177def storedBody (c : BCtx) : X Unit := do
178  let s ← ldInflateState c.st
179  modify fun l => { l with copy := s.length }
180  PULL c
181  ROOM c
182  storedTail c
183
184/-- The condition of the copy loop. -/
185def storedCond (c : BCtx) : X Bool := do return (← rdS c.st (·.length)) != 0
186
187/-- `case STORED` as the function `back_STORED`, with the loop split into `storedCond` and `storedBody`. -/
188theorem back_STORED_eq (c : BCtx) : back_STORED c = (do
189    BYTEBITS
190    NEEDBITS c 32
191    let l ← get
192    if (l.hold &&& (0xffff : UInt64)) != ((l.hold >>> 16) ^^^ (0xffff : UInt64)) then
193      badMode c "invalid stored block lengths"
194      return
195    wrS c.st fun s => { s with length := l.hold.toUInt32 &&& 0xffff }
196    INITBITS
197    xwhile (storedCond c) (storedBody c)
198    setMode c.st TYPE) := rfl
199
200theorem drop_take_drop (a : List UInt8) (o k n : Nat) :
201    ((a.drop o).take k).drop n = (a.drop (o + n)).take (k - n) := by
202  rw [List.drop_take, List.drop_drop]
203  all_goals (try (congr 2; omega))
204
205/-- The invariant after `storedTail`: `n` bytes of the chunk were copied into the window. -/
206theorem LInv.copied {c : BCtx} {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
207    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {r : ZStreamRef} {zs : Nat} {h : Heap} {l : IL}
208    {z : ZStream} {s : InflateState} {bs : List UInt8} (I : LInv c win ownI R r zs h l z s bs) {bb off2 od : Nat}
209    {da sa : Array UInt8} (hnext : l.next = .ref (.blk bb) off2) (hown : ownI bb) (hsa : h.bytes bb = some sa)
210    (hd : h.bytes win = some da) (hne : win ≠ bb)
211    (hput : l.put = .ref (.blk win) od) (hodl : ∃ off, s.window = .ref (.blk win) off ∧
212      od = off + (s.wsize.toNat - l.left.toNat))
213    (n : UInt32) (hn1 : n.toNat ≤ l.have_.toNat) (hn2 : n.toNat ≤ l.left.toNat) (L : UInt32) :
214    LInv c win ownI R r zs (copiedHeap h zs win s da sa od off2 n.toNat L)
215      (storedRegs l n bb off2 win od) z { s with length := L } (bs.drop n.toNat) := by
216  unfold storedRegs copiedHeap
217  obtain ⟨hcs, hct, hz, hs, wf, ⟨o1, a, w1, ba, ro, le⟩, ⟨o2, w2, pp, pl⟩, B, hR, hb⟩ := I
218  obtain ⟨o3, w3, hod⟩ := hodl
219  have ho12 : o3 = o1 := (Ptr.ref.inj (w3.symm.trans w1)).2
220  have hda : a = da := by rw [hd] at ba; exact (Option.some.inj ba).symm
221  subst hda
222  have hsz : (copyRange a sa od off2 n.toNat).size = a.size := size_copyRange _ _ _ _ _
223  have hbn : h.bytes bb = some sa := hsa
224  have hL : (l.left - n).toNat = l.left.toNat - n.toNat := UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr hn2)
225  have hH : (l.have_ - n).toNat = l.have_.toNat - n.toNat := UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr hn1)
226  have hbb : ∀ b, b ≠ win → (upd h.bytes win (some (copyRange a sa od off2 n.toNat))) b = h.bytes b :=
227    fun b hb => upd_ne _ _ _ _ hb
228  refine ⟨hcs, hct, by cases r <;> simpa [ZStreamRef.get] using hz, by simp, wf_with wf _ rfl rfl rfl, ⟨o1, copyRange a sa od off2 n.toNat, w1, ?_, ?_, ?_⟩,
229    ⟨o2, w2, ?_, ?_⟩, ?_, ?_, hb⟩
230  · show (upd h.bytes win (some (copyRange a sa od off2 n.toNat))) win = _
231    simp
232  · simpa using ro
233  · rw [hsz]; exact le
234  · rw [hL, hod, ho12]; simp only []
235    have := pl
236    have e : o1 + (s.wsize.toNat - l.left.toNat) + n.toNat = o2 + (s.wsize.toNat - (l.left.toNat - n.toNat)) := by
237      have : o2 = o1 := (Ptr.ref.inj (w2.symm.trans w1)).2
238      omega
239    rw [e]
240  · simp only []; omega
241  · -- the chunk
242    refine ⟨?_, ?_⟩
243    · rcases B.bit.next with e0 | ⟨r', a', off', hn', hg', hsz', hbs'⟩
244      · have e1 : bs = [] := e0
245        subst e1
246        refine ⟨by simp only [List.drop_nil, List.length_nil, hH]; have := B.bit.have_eq; simp at this; omega, Or.inl (by simp), B.bit.hold_lt⟩
247      · rw [hnext] at hn'
248        obtain ⟨h1, h2⟩ := Ptr.ref.inj hn'
249        subst h1; subst h2
250        have hsa' : a' = sa := by have : h.bytes bb = some a' := hg'; rw [hsa] at this; exact (Option.some.inj this).symm
251        rw [hsa'] at hsz' hbs'
252        refine ⟨?_, ?_, B.bit.hold_lt⟩
253        · simp only [List.length_drop, hH]; have := B.bit.have_eq; omega
254        · by_cases hz0 : (bs.drop n.toNat) = []
255          · exact Or.inl hz0
256          · right
257            refine ⟨.blk bb, sa, off2 + n.toNat, rfl, ?_, ?_, ?_⟩
258            · show (upd h.bytes win (some (copyRange a sa od off2 n.toNat))) bb = _
259              rw [hbb bb (fun e => hne e.symm)]; exact hsa
260            · simp only [List.length_drop]; have := B.bit.have_eq; omega
261            · have e2 : bs.drop n.toNat = (sa.toList.drop (off2 + n.toNat)).take (bs.length - n.toNat) := by
262                have := drop_take_drop sa.toList off2 bs.length n.toNat
263                rw [← hbs'] at this; exact this
264              simp only [List.length_drop]
265              exact e2
266    · rcases B.own with e0 | ⟨b', o', hb', hob'⟩
267      · left; subst e0; simp
268      · right
269        rw [hnext] at hb'
270        obtain ⟨h1, h2⟩ := Ptr.ref.inj hb'
271        exact ⟨bb, off2 + n.toNat, rfl, hown⟩
272  · apply (hK.local_ h _ _).1 hR
273    intro b hb'
274    have hbw : b ≠ win := by
275      rcases hb' with hb' | hb'
276      · intro e; subst e; exact hK.disj.1 hb'
277      · intro e; subst e; exact hK.disj.2.1 hb'
278    show (upd h.bytes win (some (copyRange a sa od off2 n.toNat))) b = h.bytes b
279    exact hbb b hbw
280
281/-- **One trip of the copy loop of `case STORED`.** A stored block with `length /= 0` bytes left: `PULL()`, `ROOM()`, then
282`min(length, have, left) >= 1` bytes move from the chunk to the window. Either the call ends at `PULL`/`ROOM` with `Z_BUF_ERROR`
283(`in` ended, or `out` failed), or the invariant holds again with a smaller `length` and less input to read. Only `whave` and
284`length` of the state change; the bit buffer is untouched. -/
285theorem stored_body_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
286    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
287    {r : ZStreamRef} {zs : Nat} {h : Heap} {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8}
288    (I : LInv c win ownI R r zs h l z s bs) (hw0 : 0 < s.wsize.toNat) (hlen : s.length ≠ 0) :
289    ∃ res l' h' s' bs', runX (storedBody c) l h = .ok ((res, l'), h') ∧ LInv c win ownI R r zs h' l' z s' bs' ∧
290      (∃ w n, s' = { s with whave := w, length := n }) ∧ l'.bits = l.bits ∧ l'.hold = l.hold ∧
291      (res = .ok () → s'.length.toNat < s.length.toNat ∧ phi μ h' l' < phi μ h l) ∧
292      (∀ e, res = .error e → e = Ex.leave ∧ l'.ret = Z_BUF_ERROR ∧ phi μ h' l' ≤ phi μ h l) := by
293  have hld : ldInflateState c.st h = .ok (s, h) := by rw [I.cst]; exact ldInflateState_tab I.hs
294  have I0 : LInv c win ownI R r zs h { l with copy := s.length } z s bs :=
295    Zlib.Infback.Proofs.LInv.regs I rfl rfl (BIn.regs_eq I.bin rfl rfl rfl rfl) I.bits
296  obtain ⟨r1, l1, h1, bs1, hp, F1, R1, B1, Hok1, Hl1, He1, Hbh1, Ph1⟩ := PULL_run c hK hF I0.bin I.hR
297  have hphi0 : phi μ h { l with copy := s.length } = phi μ h l := rfl
298  cases r1 with
299  | error e =>
300    have he := He1 e rfl
301    subst he
302    have hE := Hl1 rfl
303    have I1 := Zlib.Infback.Proofs.LInv.cb I0 F1 hK.disj.1 R1 (l' := l1) (by rw [hE]; rfl) (by rw [hE]; rfl) B1
304      (by rw [hE]; exact I.bits)
305    refine ⟨.error Ex.leave, l1, h1, s, bs1, ?_, I1, ⟨s.whave, s.length, rfl⟩, by rw [hE]; rfl, by rw [hE]; rfl,
306      (fun h0 => by cases h0), fun e he => ?_⟩
307    · unfold storedBody
308      rw [runX_bind, runX_lift_ok hld]; simp only []
309      rw [runX_bind, runX_modify]; simp only []
310      rw [runX_bind, hp]
311    · cases he
312      exact ⟨rfl, by rw [hE]; rfl, by rw [hphi0] at Ph1; exact Ph1⟩
313  | ok u =>
314    cases u
315    obtain ⟨hh1, hS1⟩ := Hok1 rfl
316    have hp1 : l1.put = l.put := by rw [hS1]
317    have hl1 : l1.left = l.left := by rw [hS1]
318    have hc1 : l1.copy = s.length := by rw [hS1]
319    have hbits1 : l1.bits = l.bits := Hbh1.1
320    have hhold1 : l1.hold = l.hold := Hbh1.2
321    have I1 := Zlib.Infback.Proofs.LInv.cb I0 F1 hK.disj.1 R1 (l' := l1) hp1 hl1 B1 (by rw [hbits1]; exact I.bits)
322    obtain ⟨res2, l2, h2, w, hr2, I2, Phi2, hn2, hh2, hho2, hbi2, hco2, hlf2, he2⟩ := ROOM_inv c hK hF I1 hw0
323    have hrun_pre : runX (storedBody c) l h = runX (ROOM c >>= fun _ => storedTail c) l1 h1 := by
324      unfold storedBody
325      rw [runX_bind, runX_lift_ok hld]; simp only []
326      rw [runX_bind, runX_modify]; simp only []
327      rw [runX_bind, hp]
328    have hphi01 : phi μ h1 l1 ≤ phi μ h l := Ph1
329    cases res2 with
330    | error e =>
331      have he := (he2 e rfl).1
332      subst he
333      refine ⟨.error Ex.leave, l2, h2, { s with whave := w }, bs1, ?_, I2, ⟨w, s.length, rfl⟩, by rw [hbi2, hbits1],
334        by rw [hho2, hhold1], (fun h0 => by cases h0), fun e he => ?_⟩
335      · rw [hrun_pre, runX_bind, hr2]
336      · cases he
337        exact ⟨rfl, (he2 _ rfl).2, by omega⟩
338    | ok u2 =>
339      cases u2
340      have hleft2 := hlf2 rfl
341      obtain ⟨hcs2, hct2, hz2, hs2, wf2, ⟨o1, da, w1, ba, ro, le⟩, ⟨o2, w2, pp, pl⟩, B2, hR2, hb2⟩ := I2
342      have hhave2 : l2.have_ ≠ 0 := by rw [hh2]; exact hh1
343      have hbs1 : bs1 ≠ [] := by
344        intro e
345        have := B2.bit.have_eq
346        rw [e] at this
347        exact hhave2 (UInt32.toNat_inj.mp (by simpa using this))
348      obtain ⟨bb, off2, hnx2, hown⟩ := B2.own.resolve_left hbs1
349      obtain ⟨r', sa, off', hn', hg', hsz', hbs'⟩ := B2.bit.next.resolve_left hbs1
350      rw [hnx2] at hn'
351      obtain ⟨h1', h2'⟩ := Ptr.ref.inj hn'
352      subst h1'; subst h2'
353      have hsa : h2.bytes bb = some sa := hg'
354      have hne : win ≠ bb := fun e => hK.disj.1 (e ▸ hown)
355      have hcopy2 : l2.copy ≠ 0 := by rw [hco2, hc1]; exact hlen
356      have ho21 : o2 = o1 := (Ptr.ref.inj (w2.symm.trans w1)).2
357      have hhv : l2.have_.toNat = bs1.length := B2.bit.have_eq
358      have Ihold : LInv c win ownI R r zs h2 l2 z { s with whave := w } bs1 :=
359        ⟨hcs2, hct2, hz2, hs2, wf2, ⟨o1, da, w1, ba, ro, le⟩, ⟨o2, w2, pp, pl⟩, B2, hR2, hb2⟩
360      have hle' : o1 + s.wsize.toNat ≤ da.size := le
361      have hpl' : l2.left.toNat ≤ s.wsize.toNat := pl
362      have hodsz : o2 + (s.wsize.toNat - l2.left.toNat) + l2.left.toNat ≤ da.size := by omega
363      have hrt := storedTail_run c (h := h2) (l := l2) (zs := zs) (s := { s with whave := w }) (bb := bb) (off2 := off2)
364        (win := win) (od := o2 + (s.wsize.toNat - l2.left.toNat)) (da := da) (sa := sa) hct2 hs2 pp hnx2 ba hsa ro hne
365        hhave2 hleft2 hcopy2 hodsz (by omega)
366      obtain ⟨n1, n2, n3⟩ := clampCopy_le l2.copy l2.have_ l2.left
367      have hnpos : clampCopy l2.copy l2.have_ l2.left ≠ 0 := clampCopy_pos _ _ _ hcopy2 hhave2 hleft2
368      have hnpos' : 0 < (clampCopy l2.copy l2.have_ l2.left).toNat := by
369        apply Nat.pos_of_ne_zero; intro e; exact hnpos (UInt32.toNat_inj.mp (by simpa using e))
370      have Ifin := LInv.copied hK Ihold hnx2 hown hsa ba hne pp ⟨o2, w2, rfl⟩ (clampCopy l2.copy l2.have_ l2.left) (by omega)
371        (by omega) ({ s with whave := w }.length - clampCopy l2.copy l2.have_ l2.left)
372      refine ⟨.ok (), _, _, { s with whave := w, length := s.length - clampCopy l2.copy l2.have_ l2.left },
373        _, ?_, Ifin, ⟨w, _, rfl⟩, (by show l2.bits = l.bits; rw [hbi2, hbits1]), (by show l2.hold = l.hold; rw [hho2, hhold1]),
374        fun _ => ⟨?_, ?_⟩, fun e he => by cases he⟩
375      · rw [hrun_pre, runX_bind, hr2]; exact hrt
376      · have : (s.length - clampCopy l2.copy l2.have_ l2.left).toNat = s.length.toNat - (clampCopy l2.copy l2.have_ l2.left).toNat :=
377          UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr (Nat.le_trans n1 (Nat.le_of_eq (by rw [hco2, hc1]))))
378        have hsl : 0 < s.length.toNat := by
379          apply Nat.pos_of_ne_zero; intro e; exact hlen (UInt32.toNat_inj.mp (by simpa using e))
380        simp only [this]; omega
381      · have hmu : μ (copiedHeap h2 zs win { s with whave := w } da sa (o2 + (s.wsize.toNat - l2.left.toNat)) off2 (clampCopy l2.copy l2.have_ l2.left).toNat ({ s with whave := w }.length - clampCopy l2.copy l2.have_ l2.left)) = μ h2 := by
382          apply hF.local_
383          intro b hb'
384          have hbw : b ≠ win := by
385            intro e; subst e; exact hK.disj.1 hb'
386          show (upd h2.bytes win (some (copyRange da sa (o2 + (s.wsize.toNat - l2.left.toNat)) off2 (clampCopy l2.copy l2.have_ l2.left).toNat))) b = h2.bytes b
387          exact upd_ne _ _ _ _ hbw
388        have hH : (l2.have_ - clampCopy l2.copy l2.have_ l2.left).toNat = l2.have_.toNat - (clampCopy l2.copy l2.have_ l2.left).toNat :=
389          UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr n2)
390        simp only [phi, storedRegs] at Phi2 hphi01 ⊢
391        rw [hmu]
392        simp only [hH]
393        omega
394
395/-- The length of the state record in the heap (0 if there is none): the measure of the copy loop. -/
396def stLen (zs : Nat) (h : Heap) : Nat := match h.istates zs with
397  | some s => s.length.toNat
398  | none => 0
399
400theorem stLen_of {zs : Nat} {h : Heap} {s : InflateState} (hs : h.istates zs = some s) : stLen zs h = s.length.toNat := by
401  simp [stLen, hs]
402
403/-- **The copy loop of `case STORED`.** From the registers `l` (no bits held), with `s.length` bytes to go: either `in`/`out`
404ended the call (`Z_BUF_ERROR`), or all `length` bytes were copied and the state's `length` is 0. Only `whave` and `length`
405change in the state. -/
406theorem stored_loop_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
407    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
408    {r : ZStreamRef} {zs : Nat} {h : Heap} {l : IL} {z : ZStream} {s0 : InflateState} {bs : List UInt8}
409    (hw0 : 0 < s0.wsize.toNat) (I : LInv c win ownI R r zs h l z s0 bs) :
410    ∃ res l' h' s' bs', runX (xwhile (storedCond c) (storedBody c)) l h = .ok ((res, l'), h') ∧
411      LInv c win ownI R r zs h' l' z s' bs' ∧ (∃ w n, s' = { s0 with whave := w, length := n }) ∧
412      l'.bits = l.bits ∧ l'.hold = l.hold ∧ phi μ h' l' ≤ phi μ h l ∧
413      (res = .ok () → s'.length = 0) ∧ (∀ e, res = .error e → e = Ex.leave ∧ l'.ret = Z_BUF_ERROR) := by
414  have key := xwhileBrk_wf (cond := storedCond c) (body := (do storedBody c; pure false : X Bool))
415    (fun l1 h1 => ∃ s1 bs1, LInv c win ownI R r zs h1 l1 z s1 bs1 ∧ (∃ w n, s1 = { s0 with whave := w, length := n }) ∧
416      l1.bits = l.bits ∧ l1.hold = l.hold ∧ phi μ h1 l1 ≤ phi μ h l)
417    (fun res l1 h1 => ∃ s1 bs1, LInv c win ownI R r zs h1 l1 z s1 bs1 ∧ (∃ w n, s1 = { s0 with whave := w, length := n }) ∧
418      l1.bits = l.bits ∧ l1.hold = l.hold ∧ phi μ h1 l1 ≤ phi μ h l ∧
419      (res = .ok () → s1.length = 0) ∧ (∀ e, res = .error e → e = Ex.leave ∧ l1.ret = Z_BUF_ERROR))
420    (fun _ h1 => stLen zs h1)
421    (fun l1 h1 hI => by
422      obtain ⟨s1, bs1, I1, ⟨w, n, hs1⟩, hb1, hh1, hp1⟩ := hI
423      have hwsz : s1.wsize = s0.wsize := by rw [hs1]
424      have hw1 : 0 < s1.wsize.toNat := by rw [hwsz]; exact hw0
425      have hcond : runX (storedCond c) l1 h1 = .ok ((.ok (s1.length != 0), l1), h1) := by
426        unfold storedCond
427        rw [runX_bind, runX_lift_ok (rdS_ok I1.cst I1.hs _)]; rfl
428      refine ⟨l1, h1, s1.length != 0, hcond, fun hT => ?_, fun hF' => ?_⟩
429      · have hne : s1.length ≠ 0 := by simpa using hT
430        obtain ⟨res, l2, h2, s2, bs2, hrun, I2, ⟨w2, n2, hs2⟩, hb2, hh2, hok, herr⟩ :=
431          stored_body_run c hK hF I1 hw1 hne
432        cases res with
433        | ok u =>
434          cases u
435          obtain ⟨hlt, hph⟩ := hok rfl
436          refine ⟨.ok false, l2, h2, ?_, ?_⟩
437          · rw [runX_bind, hrun]; rfl
438          · refine ⟨⟨s2, bs2, I2, ⟨w2, n2, by rw [hs2, hs1]⟩, by rw [hb2, hb1], by rw [hh2, hh1], by omega⟩, ?_⟩
439            rw [stLen_of I2.hs, stLen_of I1.hs]; exact hlt
440        | error e =>
441          obtain ⟨he, hret, hph⟩ := herr e rfl
442          subst he
443          refine ⟨.error Ex.leave, l2, h2, ?_, ?_⟩
444          · rw [runX_bind, hrun]
445          · exact ⟨s2, bs2, I2, ⟨w2, n2, by rw [hs2, hs1]⟩, by rw [hb2, hb1], by rw [hh2, hh1], by omega, (fun h0 => by cases h0),
446              (fun e he => by cases he; exact ⟨rfl, hret⟩)⟩
447      · have h0 : s1.length = 0 := by simpa using hF'
448        exact ⟨s1, bs1, I1, ⟨w, n, hs1⟩, hb1, hh1, hp1, fun _ => h0, fun e he => by cases he⟩)
449    (l := l) (h := h)
450    ⟨s0, bs, I, ⟨s0.whave, s0.length, rfl⟩, rfl, rfl, Nat.le_refl _⟩
451    (by rw [stLen_of I.hs]; have := UInt32.toNat_lt s0.length; unfold fuel; omega)
452  obtain ⟨res, l', h', hr, s', bs', I', hs', hb', hh', hp', hz, he⟩ := key
453  exact ⟨res, l', h', s', bs', by unfold xwhile; exact hr, I', hs', hb', hh', hp', hz, he⟩
454
455/-- **`case STORED`** (stored block): `BYTEBITS`, `NEEDBITS(32)`, the length check, then the copy loop. The result is one of:
456`Z_BUF_ERROR` (`in` ended or `out` failed); the lengths do not match ("invalid stored block lengths", mode `BAD`, no input
457consumed beyond the alignment bits); or all `length` bytes were copied and the mode is `TYPE`, with at least 32 input bits
458consumed. The invariant holds in every case; `wsize` is untouched. -/
459theorem stored_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
460    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
461    {r : ZStreamRef} {zs : Nat} {h : Heap} {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8}
462    (I : LInv c win ownI R r zs h l z s bs) (hw0 : 0 < s.wsize.toNat) :
463    ∃ res l' h' z' s' bs', runX (back_STORED c) l h = .ok ((res, l'), h') ∧ LInv c win ownI R r zs h' l' z' s' bs' ∧
464      s'.wsize = s.wsize ∧
465      (∀ e, res = .error e → e = Ex.leave ∧ l'.ret = Z_BUF_ERROR ∧ phi μ h' l' ≤ phi μ h l) ∧
466      (res = .ok () → (s'.mode = BAD ∧ phi μ h' l' ≤ phi μ h l) ∨ (s'.mode = TYPE ∧ phi μ h' l' + 32 ≤ phi μ h l)) := by
467  obtain ⟨B1b, -, hb1b⟩ := BYTEBITS_inv I.bin.bit
468  have hbl : (bytebits l).bits.toNat ≤ l.bits.toNat := by
469    show (l.bits - (l.bits &&& 7)).toNat ≤ _
470    rw [UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr (and7_le l))]; omega
471  have Ib : LInv c win ownI R r zs h (bytebits l) z s bs :=
472    Zlib.Infback.Proofs.LInv.regs I rfl rfl ⟨B1b, I.bin.own⟩ (by have := I.bits; omega)
473  have hphib : phi μ h (bytebits l) ≤ phi μ h l := by
474    simp only [phi]; have : (bytebits l).have_ = l.have_ := rfl
475    rw [this]; omega
476  obtain ⟨res0, l1, h1, bs1, hr1, F1, R1, B1, M1, Z1, Hok, Hleave, Herr, Ph1⟩ :=
477    NEEDBITS_run c hK hF Ib.bin I.hR 32 (by decide)
478  have h32 : (32 : UInt32).toNat = 32 := rfl
479  have hb39 : l1.bits.toNat ≤ 39 := by
480    have := Ib.bits; rw [h32] at M1; omega
481  cases res0 with
482  | error e =>
483    have he := Herr e rfl
484    subst he
485    have hE := Hleave rfl
486    have hp : l1.put = (bytebits l).put := by rw [hE]
487    have hlf : l1.left = (bytebits l).left := by rw [hE]
488    have I1 := Zlib.Infback.Proofs.LInv.cb Ib F1 hK.disj.1 R1 hp hlf B1 hb39
489    refine ⟨.error Ex.leave, l1, h1, z, s, bs1, ?_, I1, rfl, ?_, fun h0 => by cases h0⟩
490    · rw [back_STORED_eq]
491      simp only [runX_bind, BYTEBITS_run, hr1]
492    · intro e he
493      cases he
494      exact ⟨rfl, by rw [hE], by omega⟩
495  | ok u =>
496    cases u
497    obtain ⟨h32', hS⟩ := Hok rfl
498    have hp : l1.put = (bytebits l).put := by rw [hS]
499    have hlf : l1.left = (bytebits l).left := by rw [hS]
500    have I1 := Zlib.Infback.Proofs.LInv.cb Ib F1 hK.disj.1 R1 hp hlf B1 hb39
501    by_cases hcond : ((l1.hold &&& (0xffff : UInt64)) != ((l1.hold >>> 16) ^^^ (0xffff : UInt64))) = true
502    · -- the lengths do not match
503      obtain ⟨i, hbad⟩ := badMode_run c I1.cstrm I1.cst I1.hz I1.hs "invalid stored block lengths"
504        Zlib.Inflate.Proofs.lit_invalid_stored
505      have hRm : R (r.put h1 { z with msg := .ref (.str i) 0 }) :=
506        (hK.local_ h1 _ (fun b _ => by simp)).1 I1.hR
507      have Iz := Zlib.Infback.Proofs.LInv.putMsg I1 (.ref (.str i) 0) hRm
508      have I2 := Zlib.Infback.Proofs.LInv.setS Iz { s with mode := BAD } rfl rfl rfl rfl rfl (LInv.R_setI hK Iz.hR zs _)
509      have hbad' : badMode c "invalid stored block lengths" h1 =
510          .ok ((), setI (r.put h1 { z with msg := .ref (.str i) 0 }) zs { s with mode := BAD }) := hbad
511      refine ⟨.ok (), l1, setI (r.put h1 { z with msg := .ref (.str i) 0 }) zs { s with mode := BAD },
512        { z with msg := .ref (.str i) 0 }, { s with mode := BAD }, bs1, ?_, I2, rfl, (fun e he => by cases he),
513        fun _ => Or.inl ⟨rfl, ?_⟩⟩
514      · rw [back_STORED_eq]
515        simp only [runX_bind, BYTEBITS_run, hr1, runX_get, hcond, ↓reduceIte, runX_lift_ok hbad']
516        rfl
517      · have hmu : μ (setI (r.put h1 { z with msg := .ref (.str i) 0 }) zs { s with mode := BAD }) = μ h1 :=
518          hF.local_ _ _ (fun b _ => by simp)
519        simp only [phi] at Ph1 hphib ⊢
520        rw [hmu]; omega
521    · -- the lengths match: copy
522      have hcond' : ((l1.hold &&& (0xffff : UInt64)) != ((l1.hold >>> 16) ^^^ (0xffff : UInt64))) = false := by simpa using hcond
523      obtain ⟨sL, hsLd⟩ : ∃ sL : InflateState, sL = { s with length := l1.hold.toUInt32 &&& 0xffff } := ⟨_, rfl⟩
524      have hI2 := Zlib.Infback.Proofs.LInv.setS I1 sL (by rw [hsLd]) (by rw [hsLd]) (by rw [hsLd]) (by rw [hsLd])
525        (by rw [hsLd]) (LInv.R_setI hK I1.hR zs _)
526      obtain ⟨Bi, hsi⟩ := INITBITS_inv I1.bin.bit
527      have hwL : 0 < sL.wsize.toNat := by rw [hsLd]; exact hw0
528      have hIL : LInv c win ownI R r zs (setI h1 zs sL) { l1 with hold := 0, bits := 0 } z sL bs1 :=
529        Zlib.Infback.Proofs.LInv.regs hI2 rfl rfl
530          (@BIn.congr ownI h1 (setI h1 zs sL) _ bs1 (fun _ _ => rfl) ⟨Bi, I1.bin.own⟩) (by simp)
531      obtain ⟨res3, l3, h3, s3, bs3, hr3, I3, ⟨w, n, hs3⟩, hb3, hh3, hp3, hz3, he3⟩ := stored_loop_run c hK hF hwL hIL
532      have hmu2 : μ (setI h1 zs sL) = μ h1 := hF.local_ _ _ (fun b _ => rfl)
533      have hld : wrS c.st (fun s => { s with length := l1.hold.toUInt32 &&& 0xffff }) h1 = .ok ((), setI h1 zs sL) := by
534        rw [wrS_ok I1.cst I1.hs, hsLd]
535      have hpre : runX (back_STORED c) l h = runX (xwhile (storedCond c) (storedBody c) >>= fun _ => setMode c.st TYPE)
536          { l1 with hold := 0, bits := 0 } (setI h1 zs sL) := by
537        rw [back_STORED_eq]
538        simp only [runX_bind, BYTEBITS_run, hr1, runX_get, hcond', Bool.false_eq_true, ↓reduceIte, runX_lift_ok hld,
539          runX_INITBITS]
540      cases res3 with
541      | error e =>
542        have he := (he3 e rfl).1
543        subst he
544        refine ⟨.error Ex.leave, l3, h3, z, s3, bs3, ?_, I3, ?_, ?_, fun h0 => by cases h0⟩
545        · rw [hpre, runX_bind, hr3]
546        · rw [hs3, hsLd]
547        · intro e he'
548          cases he'
549          refine ⟨rfl, (he3 _ rfl).2, ?_⟩
550          have : l3.bits = 0 := by rw [hb3]
551          simp only [phi] at Ph1 hphib hp3 ⊢
552          rw [hmu2] at hp3
553          try dsimp only at hp3 ⊢
554          have hbb : (l1 : IL).bits.toNat ≥ 32 := h32'
555          have hl3b : l3.bits.toNat = 0 := by have := congrArg UInt32.toNat hb3; simpa using this
556          have e1' : ({ l1 with hold := 0, bits := 0 } : IL).have_.toNat = l1.have_.toNat := rfl
557          have e2' : ({ l1 with hold := 0, bits := 0 } : IL).bits.toNat = 0 := rfl
558          have e3' : (bytebits l).have_.toNat = l.have_.toNat := rfl
559          have e4' : (bytebits l).bits.toNat ≤ l.bits.toNat := hbl
560          have e0 : (0 : UInt32).toNat = 0 := rfl
561          omega
562      | ok u3 =>
563        cases u3
564        have hlen3 := hz3 rfl
565        have I4 := Zlib.Infback.Proofs.LInv.setS I3 { s3 with mode := TYPE } rfl rfl rfl rfl rfl (LInv.R_setI hK I3.hR zs _)
566        have hs3' : ((setI h3 zs { s3 with mode := TYPE }).istates zs) = some { s3 with mode := TYPE } := by simp
567        have hst : setMode c.st TYPE h3 = .ok ((), setI h3 zs { s3 with mode := TYPE }) := setMode_ok I3.cst I3.hs TYPE
568        refine ⟨.ok (), l3, setI h3 zs { s3 with mode := TYPE }, z, { s3 with mode := TYPE }, bs3, ?_, I4, ?_,
569          (fun e he => by cases he), fun _ => Or.inr ⟨rfl, ?_⟩⟩
570        · rw [hpre, runX_bind, hr3]
571          simp only []
572          rw [runX_lift_ok hst]
573        · rw [hs3, hsLd]
574        · have hmu3 : μ (setI h3 zs { s3 with mode := TYPE }) = μ h3 := hF.local_ _ _ (fun b _ => rfl)
575          simp only [phi] at Ph1 hphib hp3 ⊢
576          rw [hmu3]
577          rw [hmu2] at hp3
578          try dsimp only at hp3 ⊢
579          have hbb : l1.bits.toNat ≥ 32 := h32'
580          have hl3b : l3.bits.toNat = 0 := by have := congrArg UInt32.toNat hb3; simpa using this
581          have e1' : ({ l1 with hold := 0, bits := 0 } : IL).have_.toNat = l1.have_.toNat := rfl
582          have e2' : ({ l1 with hold := 0, bits := 0 } : IL).bits.toNat = 0 := rfl
583          have e3' : (bytebits l).have_.toNat = l.have_.toNat := rfl
584          have e4' : (bytebits l).bits.toNat ≤ l.bits.toNat := hbl
585          have e0 : (0 : UInt32).toNat = 0 := rfl
586          omega
587
588end Zlib.Infback.Proofs