inffast.c.advance.lean

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

1import ZlibF.Spec.InflateFast
2
3/-!
4# inffast.c: exact input advancement in the distance and length branches
5
6These proofs retain the single-pull consequence of the existing bit bounds.
7No new semantic definition or caller contract is introduced.
8-/
9
10namespace Zlib.Inffast.Proofs
11open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
12
13theorem Wp.at_run {α : Type} {m : M α} {h h' : Heap} {a : α}
14    {Q : α → Heap → Prop} (hw : Wp m h Q) (hr : m h = .ok (a, h')) : Q a h' := by
15  obtain ⟨a1, h1, hr1, hq⟩ := hw
16  have he := Except.ok.inj (hr1.symm.trans hr)
17  rcases Prod.mk.inj he with ⟨rfl, rfl⟩
18  exact hq
19
20variable {e : Env} {c : Ctx}
21
22theorem dodistBase_tight_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
23    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
24    (hAb : A.size < 2 ^ 63) (hx : l.op.toNat ≤ 13) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
25    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false)
26    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 5 ≤ l.bits.toNat)) :
27    Wp (dodistBase c l) (e.heap A msg m) (fun l' h' =>
28      ∃ i' xv rest, i ≤ i' ∧ i' ≤ i + 2 ∧ (5 ≤ l.bits.toNat → i' ≤ i + 1) ∧ readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (xv, rest) ∧
29        l'.againD = l.againD ∧
30        ((l'.broke = false ∧ LS e l' i' (o + l.len.toNat) ∧ Sg e l'.hold.toNat l'.bits.toNat i' = rest ∧
31            h' = e.heap (matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o (l.dist.toNat + xv) l.len.toNat A) msg m) ∨
32         (l'.broke = true ∧ LS e l' i' o ∧ ∃ p, h' = e.heap A p BAD))) := by
33  unfold dodistBase
34  by_cases h1 : l.bits < l.op
35  · simp only [h1, ite_true]
36    have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
37    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
38    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
39    have hl3 := hls.pullL (by omega) hiin
40    have hs3 := Sg_pullL hls (by omega) hiin
41    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
42    by_cases h2 : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits <
43        (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op
44    · simp only [h2, ite_true]
45      have h2' : l.bits.toNat + 8 < l.op.toNat := by
46        have := UInt32.lt_iff_toNat_lt.mp h2
47        simp only [pullL] at this hb3 ⊢
48        omega
49      have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
50      have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by omega
51      refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
52      have hl4 := hl3.pullL hb3' hi2
53      have hs4 := Sg_pullL hl3 hb3' hi2
54      have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
55        (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
56      refine Wp.mono (distCont_wp hc A msg m _ (i + 1 + 1) o hl4 hA ho hAb (by simp only [pullL]; omega)
57        (by simp only [pullL] at hb3 hb4 ⊢; omega) (by simp only [pullL]; omega) (by simp only [pullL]; omega)
58        (by simp only [pullL]; omega) (by simp only [pullL]; omega)) ?_
59      intro l' h' hq
60      obtain ⟨xv, rest, hr, hin, hagD, hres⟩ := hq
61      refine ⟨i + 1 + 1, xv, rest, by omega, by omega, (by intro h; omega), ?_, hagD, ?_⟩
62      · simp only [pullL] at hr hs4 hs3 ⊢
63        rw [hs4, hs3] at hr
64        exact hr
65      · simp only [pullL] at hres ⊢
66        exact Or.imp id (fun h => ⟨h.1, h.2.1, h.2.2.2⟩) hres
67    · simp only [h2, ite_false]
68      have h2n : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op.toNat ≤
69          (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat := by
70        have : ¬ ((pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat <
71            (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op.toNat) :=
72          fun h => h2 (UInt32.lt_iff_toNat_lt.mpr h)
73        omega
74      refine Wp.mono (distCont_wp hc A msg m _ (i + 1) o hl3 hA ho hAb (by simp only [pullL]; omega)
75        h2n (by simp only [pullL]; omega) (by simp only [pullL]; omega)
76        (by simp only [pullL]; omega) (by simp only [pullL]; omega)) ?_
77      intro l' h' hq
78      obtain ⟨xv, rest, hr, hin, hagD, hres⟩ := hq
79      refine ⟨i + 1, xv, rest, by omega, by omega, (by intro h; omega), ?_, hagD, ?_⟩
80      · simp only [pullL] at hr hs3 ⊢
81        rw [hs3] at hr
82        exact hr
83      · simp only [pullL] at hres ⊢
84        exact Or.imp id (fun h => ⟨h.1, h.2.1, h.2.2.2⟩) hres
85  · simp only [h1, ite_false]
86    have h1' : l.op.toNat ≤ l.bits.toNat := by
87      have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
88      omega
89    refine Wp.mono (distCont_wp hc A msg m l i o hls hA ho hAb hx h1' hd1 hd2 hlen hbroke) ?_
90    intro l' h' hq
91    obtain ⟨xv, rest, hr, hin, hagD, hres⟩ := hq
92    exact ⟨i, xv, rest, by omega, by omega, (by intro h; omega), hr, hagD, Or.imp id (fun h => ⟨h.1, h.2.1, h.2.2.2⟩) hres⟩
93
94
95set_option maxHeartbeats 1000000 in
96/-- One pass of the block at `dodist:`. Either it follows a link (`againD`), or it ends the distance block. -/
97theorem dodist_advance_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o d k : Nat)
98    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
99    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
100    (hhere : l.here = .ref e.rd k) (hk : k < e.DCA.size)
101    (hEb : (e.DCA.getD k default).bits.toNat ≤ l.bits.toNat)
102    (hEd : (e.DCA.getD k default).bits.toNat + d ≤ 15)
103    (hcl : DistClass e (e.DCA.getD k default))
104    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat + d)) :
105    Wp (dodist c l) (e.heap A msg m) (fun l' _ =>
106      ∃ i', i ≤ i' ∧ i' ≤ i + 2 ∧ (20 ≤ l.bits.toNat + d → i' ≤ i + 1) ∧
107        l'.in_ = .ref (BRef.blk e.ib) i') := by
108  have hkE : e.DCA[k]'hk = e.DCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
109  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.DCA.getD k default) := by
110    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_DCA A msg m) hk
111  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
112    simp [toNat32]
113  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
114  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
115    hls.dropL _ (by omega) (by omega)
116  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
117    simp [toNat32]
118  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
119  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
120    hls.dropL _ (by omega) (by omega)
121  have hsg1 := Sg_dropL (e := e) l (e.DCA.getD k default).bits.toUInt32 i (by omega) (by omega)
122  have hlow64 : ∀ x : UInt32, x.toNat < 32 → (l.hold >>> (e.DCA.getD k default).bits.toUInt32.toUInt64).toNat = l.hold.toNat / 2 ^ (e.DCA.getD k default).bits.toNat := by
123    intro x _; rw [u64_shr (by omega), hEbn]
124  unfold dodist
125  dsimp only
126  refine Wp.bindO hld ?_
127  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
128  refine Wp.bindO hld ?_
129  generalize e.DCA.getD k default = E at *
130  have hsg1' : Sg e (l.hold >>> E.bits.toUInt32.toUInt64).toNat (l.bits - E.bits.toUInt32).toNat i =
131      (Sg e l.hold.toNat l.bits.toNat i).drop E.bits.toNat := by
132    have := hsg1; rw [hEbn] at this; exact this
133  by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
134  · simp only [hb16, ite_true]
135    have hb16' : E.op &&& 16 ≠ 0 := by
136      rw [mask16] at hb16; simpa using hb16
137    have hbase : E.op &&& 16 ≠ 0 ∧ ((E.op &&& 15).toNat ≤ 13) ∧ 1 ≤ E.val.toNat := by
138      rcases hcl with h | h | h
139      · exact h
140      · exact absurd h.1 hb16'
141      · exact absurd h.1 hb16'
142    refine Wp.bindO hld ?_
143    have hv : E.val.toUInt32.toNat = E.val.toNat := by simp
144    have hv2 := UInt16.toNat_lt E.val
145    have hbn := dropL_bits l E.bits.toUInt32 (by omega)
146    have key := (dodistBase_tight_wp hc A msg m
147      { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
148        here := l.here, op := E.op.toUInt32 &&& 15, len := l.len, dist := E.val.toUInt32, from_ := l.from_,
149        broke := l.broke, againL := l.againL, againD := false } i o (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb
150      (by rw [mask15]; exact hbase.2.1) (by rw [hv]; exact hbase.2.2) (by rw [hv]; omega) hlen hbroke
151      (by rcases hpull with h | h
152          · exact Or.inl h
153          · refine Or.inr ⟨h.1, ?_⟩
154            show 5 ≤ (l.bits - E.bits.toUInt32).toNat
155            have hbn' : (l.bits - E.bits.toUInt32).toNat = l.bits.toNat - E.bits.toNat := by
156              rw [u32_toNat_sub (by omega), hEbn]
157            omega))
158    unfold dodistBase distCont at key
159    dsimp only at key
160    refine Wp.mono key ?_
161    intro l' h' hq
162    obtain ⟨i', xv, rest, hi1, hi2, htight, _, _, hres⟩ := hq
163    have hbound : 20 ≤ l.bits.toNat + d → i' ≤ i + 1 := by
164      intro hh
165      apply htight
166      show 5 ≤ (l.bits - E.bits.toUInt32).toNat
167      rw [u32_toNat_sub (by omega), hEbn]
168      omega
169    rcases hres with ⟨_, hls', _, _⟩ | ⟨_, hls', _⟩
170    · exact ⟨i', hi1, hi2, hbound, hls'.hin⟩
171    · exact ⟨i', hi1, hi2, hbound, hls'.hin⟩
172  · -- not a base: a link or an invalid code
173    have hb16' : E.op &&& 16 = 0 := by
174      rw [mask16] at hb16; simpa using hb16
175    by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
176    · simp only [hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
177      have hb64' : E.op &&& 64 = 0 := by
178        rw [mask64] at hb64; simpa using hb64
179      have hlink : 1 ≤ E.op.toNat ∧ E.op.toNat ≤ 15 ∧ e.od + E.val.toNat + 2 ^ E.op.toNat ≤ e.DCA.size := by
180        rcases hcl with h | h | h
181        · exact absurd hb16' h.1
182        · exact ⟨h.2.2.1, h.2.2.2.1, h.2.2.2.2⟩
183        · exact absurd hb64' h.2
184      refine Wp.bindO hld ?_
185      have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
186      have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; omega
187      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat)) ?_ ?_
188      · rw [hdc]
189        exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (Nat.le_trans (Nat.le_add_right _ _) hlink.2.2)
190      refine Wp.bindO (shl32_ok hop32) ?_
191      have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
192      have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
193        rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
194      generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
195      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat + j)) ?_ ?_
196      · rw [hlow]
197        exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rd) (a := e.DCA) (off := e.od + E.val.toNat)
198          (n := j) (e.heap_cget_DCA A msg m) (by have := hlink.2.2; omega)
199      refine Wp.pure' ⟨i, by omega, by omega, by omega, hls.hin⟩
200    · simp only [hb16, hb64, ite_false, Bool.false_eq_true]
201      obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid distance code" (by decide +kernel)
202      refine Wp.bindE hip ?_
203      exact Wp.pure' ⟨i, by omega, by omega, by omega, hls.hin⟩
204
205
206theorem dodistLoop_advance_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o kidx : Nat)
207    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat) (hk : kidx < 2 ^ e.s0.distbits.toNat)
208    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
209    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
210    (hhere : l.here = .ref e.rd (e.od + kidx)) (hb15 : 15 ≤ l.bits.toNat)
211    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) :
212    Wp (cdoWhile (dodist c) (fun l => pure (l.againD, l)) l) (e.heap A msg m) (fun l' _ =>
213      ∃ i', i ≤ i' ∧ i' ≤ i + 2 ∧ (20 ≤ l.bits.toNat → i' ≤ i + 1) ∧
214        l'.in_ = .ref (BRef.blk e.ib) i') := by
215  obtain ⟨hksz, hlk, hnl⟩ := distRoot hts kidx hk
216  have hcl0 := distClass_of (e := e) _ hlk hnl
217  have hEd0 : (e.DCA.getD (e.od + kidx) default).bits.toNat + 0 ≤ 15 := by
218    by_cases hl : DistLink (e.DCA.getD (e.od + kidx) default)
219    · have := (hlk hl).1; omega
220    · have := (hnl hl).1; omega
221  obtain ⟨l1, h1, e1, hq1⟩ := dodist_pass hc A msg m l i o 0 (e.od + kidx) hls hA ho hAb hbroke hlen hhere hksz
222    (by omega) hEd0 hcl0 (by simpa using hpull)
223  have hadv1 := Wp.at_run (dodist_advance_wp hc A msg m l i o 0 (e.od + kidx) hls hA ho hAb hbroke hlen hhere hksz
224    (by omega) hEd0 hcl0 (by simpa using hpull)) e1
225  obtain ⟨E0, hE0⟩ : ∃ E0, e.DCA.getD (e.od + kidx) default = E0 := ⟨_, rfl⟩
226  rw [hE0] at hq1 hlk hnl hcl0 hEd0
227  rcases hq1 with ⟨hag, hbr, hh, ⟨hl16, hl64⟩, j, hjlt, hjd, hhere1, hls1, hsg1, hb1, hlen1, hout1, hdist1, hagL1⟩ | ⟨hNL, hag, hend⟩
228  · -- a link: the second pass ends the block
229    subst hh
230    have hlink : DistLink E0 := ⟨hl16, hl64⟩
231    have hlk' := hlk hlink
232    have hleaf := hlk'.2.2.2.2 j hjlt
233    have hk2 : e.od + E0.val.toNat + j < e.DCA.size := by
234      have := hlk'.2.2.2.1; omega
235    have hcl1 : DistClass e (e.DCA.getD (e.od + E0.val.toNat + j) default) := by
236      rcases hleaf.2 with h | h
237      · exact Or.inl h
238      · exact Or.inr (Or.inr h)
239    have hb15' : E0.bits.toNat ≤ 15 := hlk'.1
240    obtain ⟨l2, h2, e2, hq2⟩ := dodist_pass hc A msg m l1 i o E0.bits.toNat (e.od + E0.val.toNat + j) hls1 hA ho hAb hbr
241      (by rw [hlen1]; exact hlen) hhere1 hk2 (by have := hleaf.1; omega) (by omega) hcl1 (by
242        rcases hpull with h | h
243        · exact Or.inl h
244        · exact Or.inr ⟨h.1, by omega⟩)
245    have hadv2 := Wp.at_run (dodist_advance_wp hc A msg m l1 i o E0.bits.toNat (e.od + E0.val.toNat + j) hls1 hA ho hAb hbr
246      (by rw [hlen1]; exact hlen) hhere1 hk2 (by have := hleaf.1; omega) (by omega) hcl1 (by
247        rcases hpull with h | h
248        · exact Or.inl h
249        · exact Or.inr ⟨h.1, by omega⟩)) e2
250    rcases hq2 with ⟨hag2, -, -, ⟨hl16', hl64'⟩, -⟩ | hend2
251    · rcases hleaf.2 with h | h
252      · exact absurd hl16' h.1
253      · exact absurd hl64' h.2
254    · have c1 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l1 (e.heap A msg m) = .ok ((true, l1), e.heap A msg m) := by simp [hag]
255      have c2 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l2 h2 = .ok ((false, l2), h2) := by simp [hend2.2.1]
256      have e1' : dodist c l (e.heap A msg m) = .ok (l1, e.heap A msg m) := e1
257      refine Wp.of_eq (cdoWhile_two e1' c1 e2 c2) ?_
258      obtain ⟨i', hi1, hi2, htight, hin⟩ := hadv2
259      exact ⟨i', hi1, hi2, (by intro h; apply htight; omega), hin⟩
260  · -- the first pass ended the block
261    have c1 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l1 h1 = .ok ((false, l1), h1) := by simp [hag]
262    refine Wp.of_eq (cdoWhile_one e1 c1) ?_
263    obtain ⟨i', hi1, hi2, htight, hin⟩ := hadv1
264    exact ⟨i', hi1, hi2, (by intro h; apply htight; omega), hin⟩
265
266
267theorem dolenDist_advance_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
268    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
269    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
270    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
271    (hb15 : 15 ≤ l.bits.toNat)
272    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) :
273    Wp (dolenDist c l) (e.heap A msg m) (fun l' _ =>
274      ∃ i', i ≤ i' ∧ i' ≤ i + 2 ∧ (20 ≤ l.bits.toNat → i' ≤ i + 1) ∧
275        l'.in_ = .ref (BRef.blk e.ib) i') := by
276  unfold dolenDist
277  have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
278  have hR : e.s0.distbits.toNat < 32 := by have := hts.1; omega
279  have hmask : c.dmask.toUInt64.toNat = 2 ^ e.s0.distbits.toNat - 1 := by
280    rw [hc.dmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
281  have hidx := u64_and_mask (x := l.hold) hmask
282  have hmod : l.hold.toNat % 2 ^ e.s0.distbits.toNat < 2 ^ e.s0.distbits.toNat :=
283    Nat.mod_lt _ (Nat.pow_pos (by omega))
284  refine Wp.bindO (x := Ptr.ref e.rd (e.od + l.hold.toNat % 2 ^ e.s0.distbits.toNat)) ?_ ?_
285  · rw [hdc, hidx]
286    exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (by have := hts.2.1; omega)
287  · exact Wp.mono (dodistLoop_advance_wp hc A msg m { l with here := Ptr.ref e.rd (e.od + l.hold.toNat % 2 ^ e.s0.distbits.toNat) }
288      i o _ hts hmod (LS.congr hls rfl rfl rfl rfl) hA ho hAb hbroke hlen rfl hb15 hpull) (fun _ _ h => h)
289
290theorem dolenRefill_advance_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
291    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
292    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
293    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
294    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3) (hT3 : i = s + 3 → 4 ≤ l.bits.toNat) :
295    Wp (dolenRefill c l) (e.heap A msg m) (fun l' _ =>
296      ∃ i', i ≤ i' ∧ i' ≤ s + 6 ∧ l'.in_ = .ref (BRef.blk e.ib) i') := by
297  unfold dolenRefill
298  by_cases h1 : l.bits < 15
299  · simp only [h1, ite_true]
300    have h1' : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
301    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
302    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
303    have hl3 := hls.pullL (by omega) hiin
304    have hs3 := Sg_pullL hls (by omega) hiin
305    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
306    have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
307    have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
308      simp only [pullL] at hb3 ⊢; omega
309    refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
310    have hl4 := hl3.pullL hb3' hi2
311    have hs4 := Sg_pullL hl3 hb3' hi2
312    have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
313      (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
314    simp only [pullL] at hb3 hb4
315    refine Wp.mono (dolenDist_advance_wp hc A msg m _ (i + 1 + 1) o hts hl4 hA ho hAb hbroke hlen (by simp only [pullL]; omega) ?_) ?_
316    · by_cases hc3 : i = s + 3
317      · right; have := hT3 hc3; simp only [pullL]; omega
318      · left; omega
319    · intro l' h' hq
320      obtain ⟨i', hi1, hi2, htight, hin⟩ := hq
321      refine ⟨i', by omega, ?_, hin⟩
322      by_cases hc3 : i = s + 3
323      · have hb : 20 ≤ (pullL (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)))
324          (e.IN.getD (i + 1) 0) (.ref (BRef.blk e.ib) (i + 1 + 1))).bits.toNat := by
325          have := hT3 hc3
326          simp only [pullL] at hb3 hb4 ⊢
327          omega
328        have := htight hb
329        omega
330      · omega
331  · simp only [h1, ite_false]
332    have h1' : 15 ≤ l.bits.toNat := by
333      have : ¬ (l.bits.toNat < 15) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
334      omega
335    refine Wp.mono (dolenDist_advance_wp hc A msg m l i o hts hls hA ho hAb hbroke hlen h1' (Or.inl (by omega))) ?_
336    intro l' h' hq
337    obtain ⟨i', hi1, hi2, _, hin⟩ := hq
338    exact ⟨i', hi1, by omega, hin⟩
339
340
341theorem dolenExt_advance_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
342    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
343    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
344    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5) (hxb : l.op.toNat ≤ l.bits.toNat)
345    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
346    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3)
347    (hT3 : i = s + 3 → 4 + l.op.toNat ≤ l.bits.toNat) :
348    Wp (dolenExt c l) (e.heap A msg m) (fun l' _ =>
349      ∃ i', i ≤ i' ∧ i' ≤ s + 6 ∧ l'.in_ = .ref (BRef.blk e.ib) i') := by
350  unfold dolenExt
351  have hxs : l.op.toNat < 32 := by omega
352  refine Wp.bindO (shl32_ok hxs) ?_
353  dsimp only
354  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
355  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
356  have hpow : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
357  have hlen' : (l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.len.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
358    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
359  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
360  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
361  have hbn := dropL_bits l l.op hxb
362  have hrb := readBits_bitsOfNat l.op.toNat l.bits.toNat l.hold.toNat (inBits e i) hxb
363  have hsg := Sg_dropL (e := e) l l.op i hxb (by omega)
364  refine Wp.mono (dolenRefill_advance_wp hc A msg m
365    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits - l.op, here := l.here, op := l.op,
366      len := l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1), dist := l.dist, from_ := l.from_, broke := l.broke,
367      againL := l.againL, againD := l.againD } i o s hts (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
368    (by rw [hlen']; omega) hs6 hT (by intro h3; have := hT3 h3; show 4 ≤ (l.bits - l.op).toNat; simp only [dropL] at hbn; omega)) ?_
369  exact fun _ _ hq => hq
370
371
372theorem dolenLen_advance_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
373    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
374    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
375    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5)
376    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
377    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 2) (hb2 : i = s + 2 → 1 ≤ l.bits.toNat) :
378    Wp (dolenLen c l) (e.heap A msg m) (fun l' _ =>
379      ∃ i', i ≤ i' ∧ i' ≤ s + 6 ∧ l'.in_ = .ref (BRef.blk e.ib) i') := by
380  unfold dolenLen
381  by_cases h0 : l.op != 0
382  · simp only [h0, ite_true]
383    have h0' : l.op.toNat ≠ 0 := by
384      intro h; apply (by simpa using h0 : l.op ≠ 0); exact UInt32.toNat_inj.mp (by simpa using h)
385    by_cases h1 : l.bits < l.op
386    · simp only [h1, ite_true]
387      have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
388      have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
389      refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
390      have hl3 := hls.pullL (by omega) hiin
391      have hs3 := Sg_pullL hls (by omega) hiin
392      have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
393      refine Wp.mono (dolenExt_advance_wp hc A msg m _ (i + 1) o s hts hl3 hA ho hAb hbroke (by simp only [pullL]; omega)
394        (by simp only [pullL] at hb3 ⊢; omega) (by simp only [pullL]; omega) hs6 (by omega)
395        (by intro h3; simp only [pullL] at hb3 ⊢; have := hb2 (by omega); omega)) ?_
396      intro l' h' hq
397      obtain ⟨i', hi1, hi2, hin⟩ := hq
398      exact ⟨i', by omega, hi2, hin⟩
399    · simp only [h1, ite_false]
400      have h1' : l.op.toNat ≤ l.bits.toNat := by
401        have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
402        omega
403      refine Wp.mono (dolenExt_advance_wp hc A msg m l i o s hts hls hA ho hAb hbroke hx h1' hlen hs6 (by omega)
404        (by intro h3; omega)) ?_
405      exact fun _ _ hq => hq
406  · simp only [h0, ite_false]
407    have h0' : l.op.toNat = 0 := by
408      have : l.op = 0 := by simpa using h0
409      rw [this]; rfl
410    refine Wp.mono (dolenRefill_advance_wp hc A msg m l i o s hts hls hA ho hAb hbroke ⟨hlen.1, by
411      have : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
412      omega⟩ hs6 (by omega) (by intro h3; omega)) ?_
413    exact fun _ _ hq => hq
414
415
416theorem readBits_value_lt {n : Nat} {inp rest : List Bool} {v : Nat}
417    (hr : readBits n inp = some (v, rest)) : v < 2 ^ n := by
418  induction n generalizing inp v rest with
419  | zero => simp only [readBits, Option.some.injEq, Prod.mk.injEq] at hr; omega
420  | succ n ih =>
421    cases inp with
422    | nil => cases hr
423    | cons b r =>
424      cases hread : readBits n r with
425      | none => simp [readBits, hread] at hr
426      | some vr =>
427        rcases vr with ⟨v1, r1⟩
428        have hv := ih hread
429        simp only [readBits, hread, Option.some.injEq, Prod.mk.injEq] at hr
430        rcases hr with ⟨rfl, rfl⟩
431        rw [Nat.pow_succ]
432        cases b <;> simp only [Bool.false_eq_true, ite_false, ite_true] <;> omega
433
434end Zlib.Inffast.Proofs