adler32.c.public-any.lean

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

1import ZlibF.Proof.«adler32.c.public-block»
2
3/-! Adler execution over every represented byte reference. -/
4namespace Zlib.Adler32.Proofs
5open C Zlib.Adler32 Zlib.Adler32.Spec Zlib.Adler32.Proofs
6
7
8variable {h : Heap} {ref : BRef} {bytes : Array UInt8}
9
10theorem do1_ok_any (hb : Space.get h ref = some bytes) (s : Locals) (p i : Nat)
11    (hbuf : s.buf = .ref ref p) (hlt : p + i < bytes.size) :
12    OkOn h (do1 s i) (upd s bytes[p + i]!) := by
13  obtain ⟨a, s2, buf, len, n⟩ := s
14  simp only at hbuf
15  subst hbuf
16  unfold do1
17  refine OkOn.bind (Ptr.index_ok hb hlt) ?_
18  rw [getElem_eq_bang bytes _ hlt]
19  exact OkOn.pure _ _
20
21theorem upd_buf_any (t : Locals) (b : UInt8) : (upd t b).buf = t.buf := rfl
22
23theorem do16_ok_any (hb : Space.get h ref = some bytes) (s : Locals) (p : Nat)
24    (hbuf : s.buf = .ref ref p) (hlt : p + 16 ≤ bytes.size) :
25    OkOn h (do16 s) (updL s (seg bytes p 16)) := by
26  have st : ∀ (t : Locals) (i : Nat), t.buf = .ref ref p → i < 16 →
27      OkOn h (do1 t i) (upd t bytes[p + i]!) :=
28    fun t i ht hi => do1_ok_any (ref := ref) hb t p i ht (by omega)
29  unfold do16
30  refine OkOn.bind (st _ 0 hbuf (by omega)) ?_
31  refine OkOn.bind (st _ 1 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
32  refine OkOn.bind (st _ 2 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
33  refine OkOn.bind (st _ 3 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
34  refine OkOn.bind (st _ 4 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
35  refine OkOn.bind (st _ 5 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
36  refine OkOn.bind (st _ 6 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
37  refine OkOn.bind (st _ 7 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
38  refine OkOn.bind (st _ 8 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
39  refine OkOn.bind (st _ 9 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
40  refine OkOn.bind (st _ 10 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
41  refine OkOn.bind (st _ 11 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
42  refine OkOn.bind (st _ 12 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
43  refine OkOn.bind (st _ 13 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
44  refine OkOn.bind (st _ 14 (by simp only [upd_buf_any]; exact hbuf) (by omega)) ?_
45  have e : updL s (seg bytes p 16) = upd (upd (upd (upd (upd (upd (upd (upd (upd (upd (upd
46      (upd (upd (upd (upd (upd s bytes[p + 0]!) bytes[p + 1]!) bytes[p + 2]!) bytes[p + 3]!)
47      bytes[p + 4]!) bytes[p + 5]!) bytes[p + 6]!) bytes[p + 7]!) bytes[p + 8]!) bytes[p + 9]!)
48      bytes[p + 10]!) bytes[p + 11]!) bytes[p + 12]!) bytes[p + 13]!) bytes[p + 14]!) bytes[p + 15]! := rfl
49  rw [e]
50  exact st _ 15 (by simp only [upd_buf_any]; exact hbuf) (by omega)
51
52theorem stepByte_ok_any (hb : Space.get h ref = some bytes) (s : Locals) (p : Nat)
53    (hbuf : s.buf = .ref ref p) (hlt : p < bytes.size) :
54    OkOn h (stepByte s) { upd s bytes[p]! with buf := .ref ref (p + 1) } := by
55  obtain ⟨a, s2, buf, len, n⟩ := s
56  simp only at hbuf
57  subst hbuf
58  unfold stepByte
59  refine OkOn.bind (Ptr.load_ok hb hlt) ?_
60  refine OkOn.bind (Ptr.add_ok hb (by omega) (by omega)) ?_
61  rw [getElem_eq_bang bytes _ hlt]
62  have : ((p : Int) + 1).toNat = p + 1 := by omega
63  rw [this]
64  exact OkOn.pure _ _
65
66theorem bufAdd16_ok_any (hb : Space.get h ref = some bytes) (s : Locals) (p : Nat)
67    (hbuf : s.buf = .ref ref p) (hlt : p + 16 ≤ bytes.size) :
68    OkOn h (do pure { s with buf := ← s.buf.add 16 }) { s with buf := .ref ref (p + 16) } := by
69  rw [hbuf]
70  refine OkOn.bind (Ptr.add_ok hb (by omega) (by omega)) ?_
71  have : ((p : Int) + 16).toNat = p + 16 := by omega
72  rw [this]
73  exact OkOn.pure _ _
74
75theorem byteLoop_ok_any (hb : Space.get h ref = some bytes) (s : Locals) (p : Nat)
76    (hbuf : s.buf = .ref ref p) (hfit : p + s.len.toNat ≤ bytes.size) :
77    ∃ s', OkOn h (cwhile lenPostDec stepByte s) s' ∧
78      s'.buf = .ref ref (p + s.len.toNat) ∧ AccFrom s s' (seg bytes p s.len.toNat) := by
79  have hk := fuel_gt s.len
80  generalize hkdef : s.len.toNat = k at hfit hk ⊢
81  let P : Nat → Locals → Prop := fun j t => ∃ i, i + j = k ∧ t.buf = .ref ref (p + i) ∧
82    t.len.toNat = j ∧ AccFrom s t (seg bytes p i)
83  let Q : Locals → Prop := fun t => t.buf = .ref ref (p + k) ∧ AccFrom s t (seg bytes p k)
84  refine cwhile_ok (h := h) P Q ?_ ?_ (k := k) ⟨0, by omega, by simpa using hbuf, hkdef, AccFrom.refl s⟩ hk
85  · intro j t ⟨i, hi, htb, htl, hacc⟩
86    have hne : (t.len != 0) = true := by
87      simp only [bne_iff_ne, ne_eq]; intro h0; rw [h0] at htl; simp at htl
88    refine ⟨{ t with len := t.len - 1 }, { upd { t with len := t.len - 1 } bytes[p + i]! with
89        buf := .ref ref (p + i + 1) }, ?_, stepByte_ok_any (ref := ref) hb _ (p + i) htb (by omega), ?_⟩
90    · show OkOn h (pure (t.len != 0, { t with len := t.len - 1 })) _
91      rw [hne]; exact OkOn.pure _ _
92    · refine ⟨i + 1, by omega, by simp [Nat.add_assoc], ?_, ?_⟩
93      · simp only [Zlib.Adler32.Proofs.upd]
94        rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le]; simp; omega)]
95        simp; omega
96      · rw [seg_add, seg_one]
97        exact (hacc.congr rfl rfl).upd _
98  · intro t ⟨i, hi, htb, htl, hacc⟩
99    have he : (t.len != 0) = false := by
100      simp only [bne_eq_false_iff_eq]; exact UInt64.toNat_inj.mp (by simp [htl])
101    refine ⟨{ t with len := t.len - 1 }, ?_, ?_, ?_⟩
102    · show OkOn h (pure (t.len != 0, { t with len := t.len - 1 })) _
103      rw [he]; exact OkOn.pure _ _
104    · simpa [show i = k by omega] using htb
105    · exact (show i = k by omega) ▸ hacc.congr rfl rfl
106
107/-- `while (len >= 16) { len -= 16; DO16(buf); buf += 16; }` -/
108theorem chunkLoop_ok_any (hb : Space.get h ref = some bytes) (s : Locals) (p : Nat)
109    (hbuf : s.buf = .ref ref p) (hfit : p + s.len.toNat ≤ bytes.size) :
110    ∃ s', OkOn h (cwhile (fun s => pure (decide (s.len ≥ 16), s))
111        (fun s => do
112          let s ← do16 { adler := s.adler, sum2 := s.sum2, buf := s.buf, len := s.len - 16, n := s.n }
113          let __do_lift ← s.buf.add 16
114          pure { adler := s.adler, sum2 := s.sum2, buf := __do_lift, len := s.len, n := s.n }) s) s' ∧
115      s'.buf = .ref ref (p + 16 * (s.len.toNat / 16)) ∧ s'.len.toNat = s.len.toNat % 16 ∧
116      s'.n = s.n ∧ AccFrom s s' (seg bytes p (16 * (s.len.toNat / 16))) := by
117  have hk := fuel_gt s.len
118  generalize hrdef : s.len.toNat = r at hfit hk ⊢
119  let P : Nat → Locals → Prop := fun j t => ∃ i, i + j = r / 16 ∧
120    t.buf = .ref ref (p + 16 * i) ∧
121    t.len.toNat = r - 16 * i ∧ t.n = s.n ∧ AccFrom s t (seg bytes p (16 * i))
122  let Q : Locals → Prop := fun t => t.buf = .ref ref (p + 16 * (r / 16)) ∧
123    t.len.toNat = r % 16 ∧ t.n = s.n ∧ AccFrom s t (seg bytes p (16 * (r / 16)))
124  refine cwhile_ok (h := h) P Q ?_ ?_ (k := r / 16)
125    ⟨0, by omega, by simpa using hbuf, by simp [hrdef], rfl, AccFrom.refl s⟩ (by omega)
126  · intro j t ⟨i, hi, htb, htl, htn, hacc⟩
127    have hge : decide (t.len ≥ 16) = true := by
128      simp only [decide_eq_true_eq, ge_iff_le, UInt64.le_iff_toNat_le]; simp; omega
129    let t1 : Locals := { adler := t.adler, sum2 := t.sum2, buf := t.buf, len := t.len - 16, n := t.n }
130    have ht1 : t1.buf = .ref ref (p + 16 * i) := htb
131    refine ⟨t, { updL t1 (seg bytes (p + 16 * i) 16) with
132        buf := .ref ref (p + 16 * i + 16) }, ?_, ?_, ?_⟩
133    · show OkOn h (pure (decide (t.len ≥ 16), t)) _
134      rw [hge]; exact OkOn.pure _ _
135    · refine OkOn.bind (do16_ok_any (ref := ref) hb t1 (p + 16 * i) ht1 (by omega)) ?_
136      exact bufAdd16_ok_any (ref := ref) hb _ (p + 16 * i) ht1 (by omega)
137    · refine ⟨i + 1, by omega, by simp [Nat.mul_add, Nat.add_assoc], ?_, htn, ?_⟩
138      · show (t.len - 16).toNat = r - 16 * (i + 1)
139        rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le]; simp; omega)]
140        simp; omega
141      · rw [show 16 * (i + 1) = 16 * i + 16 by omega, seg_add]
142        exact ((hacc.congr rfl rfl : AccFrom s t1 _).updL _).congr rfl rfl
143  · intro t ⟨i, hi, htb, htl, htn, hacc⟩
144    have hlt : decide (t.len ≥ 16) = false := by
145      simp only [decide_eq_false_iff_not, ge_iff_le, UInt64.le_iff_toNat_le]; simp; omega
146    refine ⟨t, ?_, ?_, ?_, htn, ?_⟩
147    · show OkOn h (pure (decide (t.len ≥ 16), t)) _
148      rw [hlt]; exact OkOn.pure _ _
149    · simpa [show i = r / 16 by omega] using htb
150    · rw [htl]; omega
151    · exact (show i = r / 16 by omega) ▸ hacc
152
153theorem nmaxBlock_ok_any (hb : Space.get h ref = some bytes) (t : Locals) (p : Nat)
154    (hbuf : t.buf = .ref ref p) (hfit : p + 5552 ≤ bytes.size) (ht : t.n = 347) :
155    ∃ u, OkOn h (cdoWhile
156        (fun s => do
157          let s ← do16 s
158          let __do_lift ← s.buf.add 16
159          pure { adler := s.adler, sum2 := s.sum2, buf := __do_lift, len := s.len, n := s.n })
160        (fun s => pure (s.n - 1 != 0, { adler := s.adler, sum2 := s.sum2, buf := s.buf, len := s.len, n := s.n - 1 }))
161        t) u ∧
162      u.buf = .ref ref (p + 5552) ∧ u.len = t.len ∧ AccFrom t u (seg bytes p 5552) := by
163  let P : Nat → Locals → Prop := fun m u => ∃ i, i + m = 346 ∧ u.n.toNat = m + 1 ∧
164    u.buf = .ref ref (p + 16 * i) ∧ u.len = t.len ∧ AccFrom t u (seg bytes p (16 * i))
165  let Q : Locals → Prop := fun u => u.buf = .ref ref (p + 5552) ∧ u.len = t.len ∧
166    AccFrom t u (seg bytes p 5552)
167  refine cdoWhile_ok (h := h) P Q ?_ ?_ (k := 346)
168    ⟨0, rfl, by rw [ht]; rfl, by simpa using hbuf, rfl, AccFrom.refl t⟩ (by simp [fuel])
169  · intro m u ⟨i, hi, hn, hub, hul, hacc⟩
170    let u1 : Locals := { updL u (seg bytes (p + 16 * i) 16) with buf := .ref ref (p + 16 * i + 16) }
171    have hne : (u1.n - 1 != 0) = true := by
172      have : u1.n = u.n := rfl
173      simp only [bne_iff_ne, ne_eq, this]
174      intro h0
175      have := congrArg UInt32.toNat h0
176      rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)] at this
177      simp at this; omega
178    refine ⟨u1, { u1 with n := u1.n - 1 }, ?_, ?_, ?_⟩
179    · refine OkOn.bind (do16_ok_any (ref := ref) hb u (p + 16 * i) hub (by omega)) ?_
180      exact bufAdd16_ok_any (ref := ref) hb _ (p + 16 * i) hub (by omega)
181    · show OkOn h (pure (u1.n - 1 != 0, { u1 with n := u1.n - 1 })) _
182      rw [hne]; exact OkOn.pure _ _
183    · refine ⟨i + 1, by omega, ?_, ?_, hul, ?_⟩
184      · show (u.n - 1).toNat = m + 1
185        rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
186        simp; omega
187      · show Ptr.ref ref (p + 16 * i + 16) = _
188        rw [show p + 16 * i + 16 = p + 16 * (i + 1) by omega]
189      · rw [show 16 * (i + 1) = 16 * i + 16 by omega, seg_add]
190        exact (hacc.updL _).congr rfl rfl
191  · intro u ⟨i, hi, hn, hub, hul, hacc⟩
192    let u1 : Locals := { updL u (seg bytes (p + 16 * i) 16) with buf := .ref ref (p + 16 * i + 16) }
193    have he : (u1.n - 1 != 0) = false := by
194      have : u1.n = u.n := rfl
195      simp only [bne_eq_false_iff_eq, this]
196      apply UInt32.toNat_inj.mp
197      rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
198      simp; omega
199    refine ⟨u1, { u1 with n := u1.n - 1 }, ?_, ?_, ?_⟩
200    · refine OkOn.bind (do16_ok_any (ref := ref) hb u (p + 16 * i) hub (by omega)) ?_
201      exact bufAdd16_ok_any (ref := ref) hb _ (p + 16 * i) hub (by omega)
202    · show OkOn h (pure (u1.n - 1 != 0, { u1 with n := u1.n - 1 })) _
203      rw [he]; exact OkOn.pure _ _
204    · refine ⟨by simp [u1]; omega, hul, ?_⟩
205      have hi' : i = 346 := by omega
206      subst hi'
207      rw [show 5552 = 16 * 346 + 16 by rfl, seg_add]
208      exact (hacc.updL _).congr rfl rfl
209
210
211theorem adler32_z_long_any (hb : Space.get h ref = some bytes) (a : UInt64) (off L : Nat)
212    (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) (h16 : 16 ≤ L) :
213    ∃ r, OkOn h (adler32_z a (.ref ref off) L.toUInt64) r ∧
214      r.toNat = Spec.adler32 a.toNat (seg bytes off L) := by
215  have hLn : L.toUInt64.toNat = L := by simp; omega
216  have hne1 : (L.toUInt64 == 1) = false := by
217    simp only [beq_eq_false_iff_ne, ne_eq]; intro e; have := congrArg UInt64.toNat e; simp at this; omega
218  have hnull : (Ptr.ref ref off == (Ptr.null : BPtr)) = false := by simp
219  have hn16 : ¬ (L.toUInt64 < 16) := by rw [UInt64.lt_iff_toNat_lt, hLn]; simp; omega
220  unfold adler32_z
221  rw [ite_eq_right_of_eq_false _ _ (by simp [hne1]), ite_eq_right_of_eq_false _ _ (by simp [hnull]),
222    ite_eq_right_of_eq_false _ _ (by simp [hn16])]
223  let lo := (a &&& 65535).toNat % 65521
224  let hi := (a >>> 16 &&& 65535).toNat % 65521
225  let q := L / 5552
226  let r := L % 5552
227  let s0 : Locals := { adler := a &&& 65535, sum2 := a >>> 16 &&& 65535, buf := .ref ref off, len := L.toUInt64, n := 0 }
228  let P : Nat → Locals → Prop := fun k t => ∃ i, i + k = q ∧ t.buf = .ref ref (off + 5552 * i) ∧
229    t.len.toNat = L - 5552 * i ∧
230    Rel 0 t.adler t.sum2 (sums lo hi (seg bytes off (5552 * i))).1 (sums lo hi (seg bytes off (5552 * i))).2 ∧
231    (1 ≤ i → t.adler.toNat < 65521 ∧ t.sum2.toNat < 65521)
232  let Q : Locals → Prop := fun t => t.buf = .ref ref (off + 5552 * q) ∧ t.len.toNat = r ∧
233    Rel 0 t.adler t.sum2 (sums lo hi (seg bytes off (5552 * q))).1 (sums lo hi (seg bytes off (5552 * q))).2 ∧
234    (1 ≤ q → t.adler.toNat < 65521 ∧ t.sum2.toNat < 65521)
235  have hinit : P q s0 := ⟨0, by omega, by simp [s0], by simp [s0, hLn], rel_init a, by omega⟩
236  refine OkOn.bind_ex (cwhile_ok (h := h) P Q ?_ ?_ hinit (by simp [fuel]; omega)) ?_
237  · -- one NMAX block
238    rintro k t ⟨i, hi_, htb, htl, hrel, -⟩
239    have hge : decide (t.len ≥ NMAX) = true := by
240      simp only [decide_eq_true_eq, ge_iff_le, UInt64.le_iff_toNat_le, htl]; simp [NMAX]; omega
241    let t0 : Locals := { adler := t.adler, sum2 := t.sum2, buf := t.buf, len := t.len - NMAX, n := (NMAX / 16).toUInt32 }
242    obtain ⟨u, hu, hub, hul, hacc⟩ := nmaxBlock_ok_any (ref := ref) hb t0 (off + 5552 * i) htb (by omega) nmax_div
243    refine ⟨t, { adler := u.adler % BASE, sum2 := u.sum2 % BASE, buf := u.buf, len := u.len, n := u.n }, ?_, ?_, ?_⟩
244    · show OkOn h (pure (decide (t.len ≥ NMAX), t)) _
245      rw [hge]; exact OkOn.pure _ _
246    · exact OkOn.bind hu (OkOn.pure _ _)
247    · have hacc' := acc_list (seg bytes (off + 5552 * i) 5552) 0 t0.adler t0.sum2 _ _ hrel (by simp [seg_length])
248      rw [seg_length] at hacc'
249      have hmod := rel_mod _ _ _ _ _ hacc'
250      refine ⟨i + 1, by omega, ?_, ?_, ?_, ?_⟩
251      · rw [hub, show off + 5552 * i + 5552 = off + 5552 * (i + 1) by omega]
252      · show u.len.toNat = _
253        rw [hul]; show (t.len - NMAX).toNat = _
254        rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le, htl]; simp [NMAX]; omega), htl]
255        simp [NMAX]; omega
256      · rw [show 5552 * (i + 1) = 5552 * i + 5552 by omega, seg_add, sums_append]
257        obtain ⟨ha, hs⟩ := hacc
258        simp only [updL] at ha hs
259        show Rel 0 (u.adler % 65521) (u.sum2 % 65521) _ _
260        rw [ha, hs]
261        exact hmod
262      · intro _
263        simp only [UInt64.toNat_mod, BASE]
264        exact ⟨Nat.mod_lt _ (by decide), Nat.mod_lt _ (by decide)⟩
265  · -- loop exit
266    rintro t ⟨i, hi_, htb, htl, hrel, hred⟩
267    have hlt : decide (t.len ≥ NMAX) = false := by
268      simp only [decide_eq_false_iff_not, ge_iff_le, UInt64.le_iff_toNat_le, htl]; simp [NMAX]; omega
269    refine ⟨t, ?_, ?_⟩
270    · show OkOn h (pure (decide (t.len ≥ NMAX), t)) _
271      rw [hlt]; exact OkOn.pure _ _
272    · have : i = q := by omega
273      subst this
274      exact ⟨htb, by rw [htl]; omega, hrel, hred⟩
275  · -- remainder
276    rintro t ⟨htb, htl, hrel, hred⟩
277    by_cases hr0 : r = 0
278    · have hz : (t.len != 0) = false := by
279        simp only [bne_eq_false_iff_eq]; exact UInt64.toNat_inj.mp (by simp [htl, hr0])
280      rw [hz]
281      simp only [Bool.false_eq_true, ite_false]
282      have hq : 1 ≤ q := by omega
283      obtain ⟨ha, hs⟩ := hred hq
284      obtain ⟨ea, es⟩ := rel_exact hrel ha hs
285      refine ⟨_, OkOn.bind (OkOn.pure _ _) (OkOn.pure _ _), ?_⟩
286      have hseg : seg bytes off L = seg bytes off (5552 * q) := by
287        rw [show 5552 * q = L by omega]
288      rw [hseg]
289      exact result_value a t.adler t.sum2 _ ea es
290    · have hnz : (t.len != 0) = true := by
291        simp only [bne_iff_ne, ne_eq]; intro e; have := congrArg UInt64.toNat e; simp [htl] at this; omega
292      rw [hnz]
293      simp only [ite_true]
294      obtain ⟨c, hc, hcb, hcl, -, hcacc⟩ := chunkLoop_ok_any (ref := ref) hb t (off + 5552 * q) htb (by rw [htl]; omega)
295      rw [htl] at hcb hcl hcacc
296      obtain ⟨d, hd, hdb, hdacc⟩ := byteLoop_ok_any (ref := ref) hb c _ hcb (by rw [hcl]; omega)
297      rw [hcl] at hdb hdacc
298      have hall := hcacc.trans hdacc
299      have hlen : (seg bytes (off + 5552 * q) (16 * (r / 16)) ++ seg bytes (off + 5552 * q + 16 * (r / 16)) (r % 16)).length = r := by
300        simp [seg_length]; omega
301      have hrel' := acc_list _ 0 t.adler t.sum2 _ _ hrel (by rw [hlen]; omega)
302      rw [hlen] at hrel'
303      obtain ⟨hda, hds⟩ := hall
304      simp only [updL] at hda hds
305      refine ⟨_, OkOn.bind hc (OkOn.bind hd (OkOn.bind (OkOn.pure _ _) (OkOn.pure _ _))), ?_⟩
306      have hseg : seg bytes off L = seg bytes off (5552 * q) ++
307          (seg bytes (off + 5552 * q) (16 * (r / 16)) ++ seg bytes (off + 5552 * q + 16 * (r / 16)) (r % 16)) := by
308        rw [← seg_add, ← seg_add]; congr 1; omega
309      rw [hseg]
310      apply result_value
311      · rw [sums_append, show (d.adler % BASE).toNat = d.adler.toNat % 65521 by simp [BASE], hda]
312        exact hrel'.1
313      · rw [sums_append, show (d.sum2 % BASE).toNat = d.sum2.toNat % 65521 by simp [BASE], hds]
314        exact hrel'.2.1
315
316
317theorem adler32_z_short_any (hb : Space.get h ref = some bytes) (a : UInt64) (off L : Nat)
318    (hfit : off + L ≤ bytes.size) (h16 : L < 16) (h1 : L ≠ 1) :
319    ∃ r, OkOn h (adler32_z a (.ref ref off) L.toUInt64) r ∧
320      r.toNat = Spec.adler32 a.toNat (seg bytes off L) := by
321  have hLn : L.toUInt64.toNat = L := by simp; omega
322  have hne1 : (L.toUInt64 == 1) = false := by
323    simp only [beq_eq_false_iff_ne, ne_eq]; intro e; have := congrArg UInt64.toNat e; simp at this; omega
324  have hnull : (Ptr.ref ref off == (Ptr.null : BPtr)) = false := by simp
325  have hy16 : L.toUInt64 < 16 := by rw [UInt64.lt_iff_toNat_lt, hLn]; simp; omega
326  unfold adler32_z
327  rw [ite_eq_right_of_eq_false _ _ (by simp [hne1]), ite_eq_right_of_eq_false _ _ (by simp [hnull]),
328    ite_eq_left hy16]
329  let s0 : Locals := { adler := a &&& 65535, sum2 := a >>> 16 &&& 65535, buf := .ref ref off, len := L.toUInt64, n := 0 }
330  obtain ⟨d, hd, -, hacc⟩ := byteLoop_ok_any (ref := ref) hb s0 off rfl (by simp [s0, hLn]; omega)
331  have hrel := acc_list (seg bytes off s0.len.toNat) 0 s0.adler s0.sum2 _ _ (rel_init a)
332    (by simp [seg_length, s0, hLn]; omega)
333  obtain ⟨hda, hds⟩ := hacc
334  simp only [updL] at hda hds
335  rw [← hda, ← hds] at hrel
336  obtain ⟨r1, r2, rb1, -⟩ := hrel
337  simp only [seg_length, s0, hLn] at r1 r2 rb1
338  refine OkOn.bind_ex (R := fun x => x = d) ⟨d, hd, rfl⟩ ?_
339  intro x hx
340  rw [hx]
341  dsimp only
342  have hres := result_value a (if d.adler ≥ BASE then d.adler - BASE else d.adler) (d.sum2 % BASE)
343    (seg bytes off L) ?_ ?_
344  · split
345    · next hge => exact ⟨_, OkOn.pure _ _, by simpa [hge] using hres⟩
346    · next hlt => exact ⟨_, OkOn.pure _ _, by simpa [hlt] using hres⟩
347  · split
348    · next hge =>
349      rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat] at hge
350      rw [sub_small _ _ (by rw [base_toNat]; omega), base_toNat, ← r1]; omega
351    · next hlt =>
352      rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat] at hlt
353      rw [← r1]; omega
354  · rw [UInt64.toNat_mod, base_toNat, r2]
355
356
357theorem adler32_z_short_format_any (hb : Space.get h ref = some bytes) (a : UInt64) (off L : Nat)
358    (hfit : off + L ≤ bytes.size) (h16 : L < 16) (h1 : L ≠ 1) :
359    C.run (adler32_z a (.ref ref off) L.toUInt64) h =
360      .ok ((ZlibF.Spec.adler32Update (canonicalStart a) (seg bytes off L)).toUInt64, h) := by
361  obtain ⟨r, hr, hv⟩ := adler32_z_short_any hb a off L hfit h16 h1
362  change C.run (adler32_z a (.ref ref off) L.toUInt64) h = .ok (r, h) at hr
363  rw [hr]
364  congr 2
365  apply UInt64.toNat_inj.mp
366  rw [UInt32.toNat_toUInt64, adler_format_seed, UInt32.toNat_ofNat', hv]
367  have hs := sums_lt (a.toNat % 65536 % 65521) (a.toNat / 65536 % 65536 % 65521)
368    (seg bytes off L) (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))
369  change (sums _ _ _).1 < 65521 ∧ (sums _ _ _).2 < 65521 at hs
370  have he : Zlib.Adler32.Spec.adler32 a.toNat (seg bytes off L) < 2 ^ 32 := by
371    unfold Zlib.Adler32.Spec.adler32
372    simp only [Zlib.Adler32.Spec.BASE]
373    omega
374  exact (Nat.mod_eq_of_lt he).symm
375
376
377theorem adler32_z_any_format (hb : Space.get h ref = some bytes) (a : UInt64) (off L : Nat)
378    (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) (h1 : L ≠ 1) :
379    C.run (adler32_z a (.ref ref off) L.toUInt64) h =
380      .ok ((ZlibF.Spec.adler32Update (canonicalStart a) (seg bytes off L)).toUInt64, h) := by
381  by_cases h16 : L < 16
382  · exact adler32_z_short_format_any hb a off L hfit h16 h1
383  · obtain ⟨r, hr, hv⟩ := adler32_z_long_any hb a off L hfit hL (by omega)
384    change C.run (adler32_z a (.ref ref off) L.toUInt64) h = .ok (r, h) at hr
385    rw [hr]
386    congr 2
387    apply UInt64.toNat_inj.mp
388    rw [UInt32.toNat_toUInt64, adler_format_seed, UInt32.toNat_ofNat', hv]
389    have hs := sums_lt (a.toNat % 65536 % 65521) (a.toNat / 65536 % 65536 % 65521)
390      (seg bytes off L) (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))
391    change (sums _ _ _).1 < 65521 ∧ (sums _ _ _).2 < 65521 at hs
392    have he : Zlib.Adler32.Spec.adler32 a.toNat (seg bytes off L) < 2 ^ 32 := by
393      unfold Zlib.Adler32.Spec.adler32
394      simp only [Zlib.Adler32.Spec.BASE]
395      omega
396    exact (Nat.mod_eq_of_lt he).symm
397
398/-- `uLong adler32(uLong adler, const Bytef *buf, uInt len)`: the
39932-bit entry preserves the full general-reference format result. -/
400theorem adler32_any_format (hb : Space.get h ref = some bytes) (a : UInt64)
401    (off : Nat) (len : UInt32) (hfit : off + len.toNat ≤ bytes.size)
402    (h1 : len.toNat ≠ 1) :
403    C.run (Zlib.Adler32.adler32 a (.ref ref off) len) h =
404      .ok ((ZlibF.Spec.adler32Update (canonicalStart a) (seg bytes off len.toNat)).toUInt64, h) := by
405  simpa [Zlib.Adler32.adler32, UInt32.toNat_toUInt64, UInt64.ofNat_toNat] using
406    (adler32_z_any_format hb a off len.toNat hfit (by have := len.toNat_lt; omega) h1)
407
408#print axioms adler32_z_any_format
409#print axioms adler32_any_format
410end Zlib.Adler32.Proofs