REFERENCE / ZLIB × LEAN
adler32.c.lean
Source snapshot ·
bed861c7849a2cb4 · Source at the matching commit ↗Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.
1import ZlibF.Zlib.«adler32.c»
2
3
4/-!
5# Adler-32 specification (RFC 1950 §8.2)
6
7`spec lo hi bs`: starting from component sums `lo`, `hi` (each < 65521), feed
8bytes `bs`; each byte updates `lo := (lo + b) mod 65521`, then
9`hi := (hi + lo) mod 65521`. The checksum is `lo + 65536 * hi`.
10This file is independent of the C translation.
11-/
12
13namespace Zlib.Adler32.Spec
14
15def BASE : Nat := 65521
16
17def step (st : Nat × Nat) (b : UInt8) : Nat × Nat :=
18 ((st.1 + b.toNat) % BASE, (st.2 + (st.1 + b.toNat) % BASE) % BASE)
19
20def sums (lo hi : Nat) (bs : List UInt8) : Nat × Nat := bs.foldl step (lo, hi)
21
22/-- Adler-32 of `bs` continuing from the checksum value `adler`
23(the conventional initial value is 1). -/
24def adler32 (adler : Nat) (bs : List UInt8) : Nat :=
25 let st := sums (adler % 65536 % BASE) (adler / 65536 % 65536 % BASE) bs
26 st.1 + 65536 * st.2
27
28theorem step_lt (st : Nat × Nat) (b : UInt8) : (step st b).1 < BASE ∧ (step st b).2 < BASE := by
29 simp only [step, BASE]; omega
30
31theorem sums_append (lo hi : Nat) (xs ys : List UInt8) :
32 sums lo hi (xs ++ ys) = sums (sums lo hi xs).1 (sums lo hi xs).2 ys := by
33 simp [sums, List.foldl_append]
34
35theorem sums_lt (lo hi : Nat) (bs : List UInt8) (hlo : lo < BASE) (hhi : hi < BASE) :
36 (sums lo hi bs).1 < BASE ∧ (sums lo hi bs).2 < BASE := by
37 induction bs generalizing lo hi with
38 | nil => exact ⟨hlo, hhi⟩
39 | cons b bs ih =>
40 have := step_lt (lo, hi) b
41 exact ih _ _ this.1 this.2
42
43end Zlib.Adler32.Spec
44
45
46namespace Zlib.Adler32.Spec
47
48/-! ## Combination of two Adler-32 values (RFC 1950 sums are affine in the start) -/
49
50/-- Unreduced sums: `S1 = Σ b`, `S2 = Σ (n - i) b_i` for `bs` of length `n`. -/
51def s1 (bs : List UInt8) : Nat := (bs.map UInt8.toNat).sum
52def s2 : List UInt8 → Nat
53 | [] => 0
54 | b :: bs => (bs.length + 1) * b.toNat + s2 bs
55
56/-- Closed form: feeding `bs` from reduced `(lo, hi)` gives
57`(lo + S1, hi + n * lo + S2)` reduced modulo 65521. -/
58theorem sums_closed (bs : List UInt8) : ∀ lo hi : Nat, lo < BASE → hi < BASE →
59 sums lo hi bs = ((lo + s1 bs) % BASE, (hi + bs.length * lo + s2 bs) % BASE) := by
60 induction bs with
61 | nil =>
62 intro lo hi hlo hhi
63 simp [sums, s1, s2, Nat.mod_eq_of_lt hlo, Nat.mod_eq_of_lt hhi]
64 | cons b bs ih =>
65 intro lo hi hlo hhi
66 have hst := step_lt (lo, hi) b
67 have e : sums lo hi (b :: bs) = sums (step (lo, hi) b).1 (step (lo, hi) b).2 bs := rfl
68 rw [e, ih _ _ hst.1 hst.2]
69 simp only [step, BASE, s1, s2, List.map_cons, List.sum_cons, List.length_cons] at *
70 have hm : bs.length * ((lo + b.toNat) % 65521) % 65521 = bs.length * (lo + b.toNat) % 65521 :=
71 Nat.mul_mod_mod _ _ _
72 rw [Nat.mul_add] at hm
73 rw [Prod.mk.injEq]
74 constructor
75 · omega
76 · rw [Nat.add_mul, Nat.add_mul, Nat.one_mul, Nat.one_mul]
77 omega
78
79/-- The Adler-32 combination identity used by `adler32_combine`: for
80`x = sums 1 0 A`, `y = sums 1 0 B` and `n = |B| mod 65521`,
81`sums 1 0 (A ++ B)` is `(x₁ + y₁ + 65520, (n·x₁ mod 65521) + x₂ + y₂ + 65521 − n)`
82reduced modulo 65521. -/
83theorem sums_combine (A B : List UInt8) :
84 sums 1 0 (A ++ B) =
85 (((sums 1 0 A).1 + (sums 1 0 B).1 + BASE - 1) % BASE,
86 ((B.length % BASE) * (sums 1 0 A).1 % BASE + (sums 1 0 A).2 + (sums 1 0 B).2 + BASE
87 - B.length % BASE) % BASE) := by
88 have hx := sums_lt 1 0 A (by decide) (by decide)
89 rw [sums_append, sums_closed B _ _ hx.1 hx.2, sums_closed B 1 0 (by decide) (by decide)]
90 simp only [BASE] at *
91 have hn : (B.length % 65521) * (sums 1 0 A).1 % 65521 = B.length * (sums 1 0 A).1 % 65521 :=
92 Nat.mod_mul_mod _ _ _
93 have hn' : B.length % 65521 < 65521 := Nat.mod_lt _ (by decide)
94 rw [Prod.mk.injEq]
95 constructor
96 · omega
97 · omega
98
99end Zlib.Adler32.Spec
100
101namespace Zlib.Adler32.Proofs
102open C Zlib.Adler32
103
104/-- Bytes `p .. p+n-1` of a block. -/
105def seg (bytes : Array UInt8) (p n : Nat) : List UInt8 := (List.range n).map (fun i => bytes[p + i]!)
106
107end Zlib.Adler32.Proofs
108
109
110/-!
111# Arithmetic core of the adler32_z proof
112
113Between two `MOD` reductions the C code accumulates at most `NMAX = 5552`
114bytes in 64-bit `unsigned long` without reducing. `Rel j a s lo hi` says the
115machine sums `a`, `s` (after `j` unreduced bytes) are congruent to the spec
116sums `lo`, `hi` and bounded so that nothing wraps.
117-/
118
119namespace Zlib.Adler32.Proofs
120open Zlib.Adler32.Spec
121
122/-- One unreduced machine step: `adler += b; sum2 += adler;`. -/
123def acc (st : UInt64 × UInt64) (b : UInt8) : UInt64 × UInt64 :=
124 (st.1 + b.toUInt64, st.2 + (st.1 + b.toUInt64))
125
126/-- Bound on `sum2` growth per byte while at most NMAX bytes are unreduced. -/
127def C : Nat := 65535 + 255 * 5552
128
129def Rel (j : Nat) (a s : UInt64) (lo hi : Nat) : Prop :=
130 a.toNat % 65521 = lo ∧ s.toNat % 65521 = hi ∧
131 a.toNat ≤ 65535 + 255 * j ∧ s.toNat ≤ 65535 + j * C
132
133theorem acc_one (j : Nat) (a s : UInt64) (lo hi : Nat) (b : UInt8)
134 (hr : Rel j a s lo hi) (hj : j + 1 ≤ 5552) :
135 Rel (j + 1) (acc (a, s) b).1 (acc (a, s) b).2 (step (lo, hi) b).1 (step (lo, hi) b).2 := by
136 obtain ⟨hlo, hhi, ha, hs⟩ := hr
137 have hb : b.toNat < 256 := b.toNat_lt
138 have ha' : (a + b.toUInt64).toNat = a.toNat + b.toNat := by
139 rw [UInt64.toNat_add, UInt8.toNat_toUInt64]
140 exact Nat.mod_eq_of_lt (by omega)
141 have hs' : (s + (a + b.toUInt64)).toNat = s.toNat + (a.toNat + b.toNat) := by
142 rw [UInt64.toNat_add, ha']
143 exact Nat.mod_eq_of_lt (by simp only [C] at hs; omega)
144 simp only [acc, step, Spec.BASE, Rel, ha', hs', C] at *
145 omega
146
147theorem acc_list (bs : List UInt8) : ∀ (j : Nat) (a s : UInt64) (lo hi : Nat),
148 Rel j a s lo hi → j + bs.length ≤ 5552 →
149 Rel (j + bs.length) (bs.foldl acc (a, s)).1 (bs.foldl acc (a, s)).2
150 (sums lo hi bs).1 (sums lo hi bs).2 := by
151 induction bs with
152 | nil => intro j a s lo hi hr _; simpa [sums] using hr
153 | cons b bs ih =>
154 intro j a s lo hi hr hj
155 have h1 := acc_one j a s lo hi b hr (by simp at hj; omega)
156 have := ih (j + 1) _ _ _ _ h1 (by simp at hj; omega)
157 simpa [sums, List.foldl, Nat.add_assoc, Nat.add_comm 1] using this
158
159/-- `MOD(a)`: `a %= BASE` reduces exactly to the spec value and resets the bound. -/
160theorem rel_mod (j : Nat) (a s : UInt64) (lo hi : Nat) (hr : Rel j a s lo hi) :
161 Rel 0 (a % 65521) (s % 65521) lo hi := by
162 obtain ⟨hlo, hhi, -, -⟩ := hr
163 simp only [Rel, UInt64.toNat_mod]
164 refine ⟨?_, ?_, ?_, ?_⟩ <;> simp <;> omega
165
166end Zlib.Adler32.Proofs
167
168/-!
169# Step lemmas for the adler32_z translation
170
171Each lemma gives the exact resulting locals of one macro/statement group,
172assuming the buffer pointer is inside a live block.
173-/
174
175namespace Zlib.Adler32.Proofs
176open C Zlib.Adler32
177
178
179theorem seg_length (bytes : Array UInt8) (p n : Nat) : (seg bytes p n).length = n := by
180 simp [seg]
181
182theorem seg_add (bytes : Array UInt8) (p m n : Nat) :
183 seg bytes p (m + n) = seg bytes p m ++ seg bytes (p + m) n := by
184 simp [seg, List.range_add, Nat.add_assoc]
185
186theorem seg_one (bytes : Array UInt8) (p : Nat) : seg bytes p 1 = [bytes[p]!] := by
187 simp [seg]
188
189/-- Machine sums after one byte. -/
190def upd (s : Locals) (b : UInt8) : Locals :=
191 { s with adler := (acc (s.adler, s.sum2) b).1, sum2 := (acc (s.adler, s.sum2) b).2 }
192
193/-- Machine sums after a list of bytes. -/
194def updL (s : Locals) (bs : List UInt8) : Locals :=
195 { s with adler := (bs.foldl acc (s.adler, s.sum2)).1, sum2 := (bs.foldl acc (s.adler, s.sum2)).2 }
196
197theorem updL_nil (s : Locals) : updL s [] = s := rfl
198
199theorem updL_cons (s : Locals) (b : UInt8) (bs : List UInt8) :
200 updL s (b :: bs) = updL (upd s b) bs := rfl
201
202theorem updL_append (s : Locals) (xs ys : List UInt8) :
203 updL s (xs ++ ys) = updL (updL s xs) ys := by
204 simp [updL, List.foldl_append]
205
206variable {h : Heap} {blk : Nat} {bytes : Array UInt8}
207
208theorem getElem_eq_bang (bytes : Array UInt8) (i : Nat) (hi : i < bytes.size) :
209 bytes[i] = bytes[i]! := by
210 simp [getElem!_pos, hi]
211
212theorem do1_ok (hb : h.bytes blk = some bytes) (s : Locals) (p i : Nat)
213 (hbuf : s.buf = .ref (.blk blk) p) (hlt : p + i < bytes.size) :
214 OkOn h (do1 s i) (upd s bytes[p + i]!) := by
215 obtain ⟨a, s2, buf, len, n⟩ := s
216 simp only at hbuf
217 subst hbuf
218 unfold do1
219 refine OkOn.bind (index8_ok hb hlt) ?_
220 rw [getElem_eq_bang bytes _ hlt]
221 exact OkOn.pure _ _
222
223theorem upd_buf (t : Locals) (b : UInt8) : (upd t b).buf = t.buf := rfl
224
225theorem do16_ok (hb : h.bytes blk = some bytes) (s : Locals) (p : Nat)
226 (hbuf : s.buf = .ref (.blk blk) p) (hlt : p + 16 ≤ bytes.size) :
227 OkOn h (do16 s) (updL s (seg bytes p 16)) := by
228 have st : ∀ (t : Locals) (i : Nat), t.buf = .ref (.blk blk) p → i < 16 →
229 OkOn h (do1 t i) (upd t bytes[p + i]!) :=
230 fun t i ht hi => do1_ok hb t p i ht (by omega)
231 unfold do16
232 refine OkOn.bind (st _ 0 hbuf (by omega)) ?_
233 refine OkOn.bind (st _ 1 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
234 refine OkOn.bind (st _ 2 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
235 refine OkOn.bind (st _ 3 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
236 refine OkOn.bind (st _ 4 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
237 refine OkOn.bind (st _ 5 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
238 refine OkOn.bind (st _ 6 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
239 refine OkOn.bind (st _ 7 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
240 refine OkOn.bind (st _ 8 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
241 refine OkOn.bind (st _ 9 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
242 refine OkOn.bind (st _ 10 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
243 refine OkOn.bind (st _ 11 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
244 refine OkOn.bind (st _ 12 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
245 refine OkOn.bind (st _ 13 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
246 refine OkOn.bind (st _ 14 (by simp only [upd_buf]; exact hbuf) (by omega)) ?_
247 have e : updL s (seg bytes p 16) = upd (upd (upd (upd (upd (upd (upd (upd (upd (upd (upd
248 (upd (upd (upd (upd (upd s bytes[p + 0]!) bytes[p + 1]!) bytes[p + 2]!) bytes[p + 3]!)
249 bytes[p + 4]!) bytes[p + 5]!) bytes[p + 6]!) bytes[p + 7]!) bytes[p + 8]!) bytes[p + 9]!)
250 bytes[p + 10]!) bytes[p + 11]!) bytes[p + 12]!) bytes[p + 13]!) bytes[p + 14]!) bytes[p + 15]! := rfl
251 rw [e]
252 exact st _ 15 (by simp only [upd_buf]; exact hbuf) (by omega)
253
254theorem stepByte_ok (hb : h.bytes blk = some bytes) (s : Locals) (p : Nat)
255 (hbuf : s.buf = .ref (.blk blk) p) (hlt : p < bytes.size) :
256 OkOn h (stepByte s) { upd s bytes[p]! with buf := .ref (.blk blk) (p + 1) } := by
257 obtain ⟨a, s2, buf, len, n⟩ := s
258 simp only at hbuf
259 subst hbuf
260 unfold stepByte
261 refine OkOn.bind (load8_ok hb hlt) ?_
262 refine OkOn.bind (Ptr.add_ok hb (by omega) (by omega)) ?_
263 rw [getElem_eq_bang bytes _ hlt]
264 have : ((p : Int) + 1).toNat = p + 1 := by omega
265 rw [this]
266 exact OkOn.pure _ _
267
268theorem bufAdd16_ok (hb : h.bytes blk = some bytes) (s : Locals) (p : Nat)
269 (hbuf : s.buf = .ref (.blk blk) p) (hlt : p + 16 ≤ bytes.size) :
270 OkOn h (do pure { s with buf := ← s.buf.add 16 }) { s with buf := .ref (.blk blk) (p + 16) } := by
271 rw [hbuf]
272 refine OkOn.bind (Ptr.add_ok hb (by omega) (by omega)) ?_
273 have : ((p : Int) + 16).toNat = p + 16 := by omega
274 rw [this]
275 exact OkOn.pure _ _
276
277end Zlib.Adler32.Proofs
278
279/-!
280# Loop lemmas for the adler32_z translation
281
282`AccFrom s t l`: the machine sums of `t` are those of `s` after accumulating
283bytes `l` without reduction. Each lemma proves a loop terminates within fuel,
284stays in bounds, and computes the expected sums.
285-/
286
287namespace Zlib.Adler32.Proofs
288open C Zlib.Adler32
289
290def AccFrom (s t : Locals) (l : List UInt8) : Prop :=
291 t.adler = (updL s l).adler ∧ t.sum2 = (updL s l).sum2
292
293theorem AccFrom.refl (s : Locals) : AccFrom s s [] := ⟨rfl, rfl⟩
294
295theorem AccFrom.updL {s t : Locals} {l : List UInt8} (hr : AccFrom s t l) (m : List UInt8) :
296 AccFrom s (Proofs.updL t m) (l ++ m) := by
297 obtain ⟨ha, hs⟩ := hr
298 simp only [AccFrom, Proofs.updL, List.foldl_append] at *
299 rw [ha, hs]
300 exact ⟨rfl, rfl⟩
301
302theorem AccFrom.upd {s t : Locals} {l : List UInt8} (hr : AccFrom s t l) (b : UInt8) :
303 AccFrom s (upd t b) (l ++ [b]) := hr.updL [b]
304
305theorem AccFrom.congr {s t t' : Locals} {l : List UInt8} (hr : AccFrom s t l)
306 (ha : t'.adler = t.adler) (hs : t'.sum2 = t.sum2) : AccFrom s t' l := by
307 obtain ⟨h1, h2⟩ := hr; exact ⟨ha.trans h1, hs.trans h2⟩
308
309theorem AccFrom.trans {s t u : Locals} {l m : List UInt8} (h1 : AccFrom s t l) (h2 : AccFrom t u m) :
310 AccFrom s u (l ++ m) := by
311 obtain ⟨a1, s1⟩ := h1
312 obtain ⟨a2, s2⟩ := h2
313 simp only [AccFrom, Proofs.updL, List.foldl_append] at *
314 rw [a2, s2, a1, s1]
315 exact ⟨rfl, rfl⟩
316
317theorem fuel_gt (x : UInt64) : x.toNat < fuel := by
318 have := x.toNat_lt; simp only [fuel]; omega
319
320variable {h : Heap} {blk : Nat} {bytes : Array UInt8}
321
322/-- `while (len--) { adler += *buf++; sum2 += adler; }` -/
323theorem byteLoop_ok (hb : h.bytes blk = some bytes) (s : Locals) (p : Nat)
324 (hbuf : s.buf = .ref (.blk blk) p) (hfit : p + s.len.toNat ≤ bytes.size) :
325 ∃ s', OkOn h (cwhile lenPostDec stepByte s) s' ∧
326 s'.buf = .ref (.blk blk) (p + s.len.toNat) ∧ AccFrom s s' (seg bytes p s.len.toNat) := by
327 have hk := fuel_gt s.len
328 generalize hkdef : s.len.toNat = k at hfit hk ⊢
329 let P : Nat → Locals → Prop := fun j t => ∃ i, i + j = k ∧ t.buf = .ref (.blk blk) (p + i) ∧
330 t.len.toNat = j ∧ AccFrom s t (seg bytes p i)
331 let Q : Locals → Prop := fun t => t.buf = .ref (.blk blk) (p + k) ∧ AccFrom s t (seg bytes p k)
332 refine cwhile_ok (h := h) P Q ?_ ?_ (k := k) ⟨0, by omega, by simpa using hbuf, hkdef, AccFrom.refl s⟩ hk
333 · intro j t ⟨i, hi, htb, htl, hacc⟩
334 have hne : (t.len != 0) = true := by
335 simp only [bne_iff_ne, ne_eq]; intro h0; rw [h0] at htl; simp at htl
336 refine ⟨{ t with len := t.len - 1 }, { upd { t with len := t.len - 1 } bytes[p + i]! with
337 buf := .ref (.blk blk) (p + i + 1) }, ?_, stepByte_ok hb _ (p + i) htb (by omega), ?_⟩
338 · show OkOn h (pure (t.len != 0, { t with len := t.len - 1 })) _
339 rw [hne]; exact OkOn.pure _ _
340 · refine ⟨i + 1, by omega, by simp [Nat.add_assoc], ?_, ?_⟩
341 · simp only [upd]
342 rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le]; simp; omega)]
343 simp; omega
344 · rw [seg_add, seg_one]
345 exact (hacc.congr rfl rfl).upd _
346 · intro t ⟨i, hi, htb, htl, hacc⟩
347 have he : (t.len != 0) = false := by
348 simp only [bne_eq_false_iff_eq]; exact UInt64.toNat_inj.mp (by simp [htl])
349 refine ⟨{ t with len := t.len - 1 }, ?_, ?_, ?_⟩
350 · show OkOn h (pure (t.len != 0, { t with len := t.len - 1 })) _
351 rw [he]; exact OkOn.pure _ _
352 · simpa [show i = k by omega] using htb
353 · exact (show i = k by omega) ▸ hacc.congr rfl rfl
354
355/-- `while (len >= 16) { len -= 16; DO16(buf); buf += 16; }` -/
356theorem chunkLoop_ok (hb : h.bytes blk = some bytes) (s : Locals) (p : Nat)
357 (hbuf : s.buf = .ref (.blk blk) p) (hfit : p + s.len.toNat ≤ bytes.size) :
358 ∃ s', OkOn h (cwhile (fun s => pure (decide (s.len ≥ 16), s))
359 (fun s => do
360 let s ← do16 { adler := s.adler, sum2 := s.sum2, buf := s.buf, len := s.len - 16, n := s.n }
361 let __do_lift ← s.buf.add 16
362 pure { adler := s.adler, sum2 := s.sum2, buf := __do_lift, len := s.len, n := s.n }) s) s' ∧
363 s'.buf = .ref (.blk blk) (p + 16 * (s.len.toNat / 16)) ∧ s'.len.toNat = s.len.toNat % 16 ∧
364 s'.n = s.n ∧ AccFrom s s' (seg bytes p (16 * (s.len.toNat / 16))) := by
365 have hk := fuel_gt s.len
366 generalize hrdef : s.len.toNat = r at hfit hk ⊢
367 let P : Nat → Locals → Prop := fun j t => ∃ i, i + j = r / 16 ∧
368 t.buf = .ref (.blk blk) (p + 16 * i) ∧
369 t.len.toNat = r - 16 * i ∧ t.n = s.n ∧ AccFrom s t (seg bytes p (16 * i))
370 let Q : Locals → Prop := fun t => t.buf = .ref (.blk blk) (p + 16 * (r / 16)) ∧
371 t.len.toNat = r % 16 ∧ t.n = s.n ∧ AccFrom s t (seg bytes p (16 * (r / 16)))
372 refine cwhile_ok (h := h) P Q ?_ ?_ (k := r / 16)
373 ⟨0, by omega, by simpa using hbuf, by simp [hrdef], rfl, AccFrom.refl s⟩ (by omega)
374 · intro j t ⟨i, hi, htb, htl, htn, hacc⟩
375 have hge : decide (t.len ≥ 16) = true := by
376 simp only [decide_eq_true_eq, ge_iff_le, UInt64.le_iff_toNat_le]; simp; omega
377 let t1 : Locals := { adler := t.adler, sum2 := t.sum2, buf := t.buf, len := t.len - 16, n := t.n }
378 have ht1 : t1.buf = .ref (.blk blk) (p + 16 * i) := htb
379 refine ⟨t, { updL t1 (seg bytes (p + 16 * i) 16) with
380 buf := .ref (.blk blk) (p + 16 * i + 16) }, ?_, ?_, ?_⟩
381 · show OkOn h (pure (decide (t.len ≥ 16), t)) _
382 rw [hge]; exact OkOn.pure _ _
383 · refine OkOn.bind (do16_ok hb t1 (p + 16 * i) ht1 (by omega)) ?_
384 exact bufAdd16_ok hb _ (p + 16 * i) ht1 (by omega)
385 · refine ⟨i + 1, by omega, by simp [Nat.mul_add, Nat.add_assoc], ?_, htn, ?_⟩
386 · show (t.len - 16).toNat = r - 16 * (i + 1)
387 rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le]; simp; omega)]
388 simp; omega
389 · rw [show 16 * (i + 1) = 16 * i + 16 by omega, seg_add]
390 exact ((hacc.congr rfl rfl : AccFrom s t1 _).updL _).congr rfl rfl
391 · intro t ⟨i, hi, htb, htl, htn, hacc⟩
392 have hlt : decide (t.len ≥ 16) = false := by
393 simp only [decide_eq_false_iff_not, ge_iff_le, UInt64.le_iff_toNat_le]; simp; omega
394 refine ⟨t, ?_, ?_, ?_, htn, ?_⟩
395 · show OkOn h (pure (decide (t.len ≥ 16), t)) _
396 rw [hlt]; exact OkOn.pure _ _
397 · simpa [show i = r / 16 by omega] using htb
398 · rw [htl]; omega
399 · exact (show i = r / 16 by omega) ▸ hacc
400
401end Zlib.Adler32.Proofs
402
403/-!
404# Block-level lemmas for adler32_z: the NMAX inner loop and the outer loop
405-/
406
407namespace Zlib.Adler32.Proofs
408open C Zlib.Adler32 Zlib.Adler32.Spec
409
410variable {h : Heap} {blk : Nat} {bytes : Array UInt8}
411
412theorem nmax_div : (NMAX / 16).toUInt32 = 347 := by decide
413
414/-- One NMAX block: `n = NMAX / 16; do { DO16(buf); buf += 16; } while (--n);` -/
415theorem nmaxBlock_ok (hb : h.bytes blk = some bytes) (t : Locals) (p : Nat)
416 (hbuf : t.buf = .ref (.blk blk) p) (hfit : p + 5552 ≤ bytes.size) (ht : t.n = 347) :
417 ∃ u, OkOn h (cdoWhile
418 (fun s => do
419 let s ← do16 s
420 let __do_lift ← s.buf.add 16
421 pure { adler := s.adler, sum2 := s.sum2, buf := __do_lift, len := s.len, n := s.n })
422 (fun s => pure (s.n - 1 != 0, { adler := s.adler, sum2 := s.sum2, buf := s.buf, len := s.len, n := s.n - 1 }))
423 t) u ∧
424 u.buf = .ref (.blk blk) (p + 5552) ∧ u.len = t.len ∧ AccFrom t u (seg bytes p 5552) := by
425 let P : Nat → Locals → Prop := fun m u => ∃ i, i + m = 346 ∧ u.n.toNat = m + 1 ∧
426 u.buf = .ref (.blk blk) (p + 16 * i) ∧ u.len = t.len ∧ AccFrom t u (seg bytes p (16 * i))
427 let Q : Locals → Prop := fun u => u.buf = .ref (.blk blk) (p + 5552) ∧ u.len = t.len ∧
428 AccFrom t u (seg bytes p 5552)
429 refine cdoWhile_ok (h := h) P Q ?_ ?_ (k := 346)
430 ⟨0, rfl, by rw [ht]; rfl, by simpa using hbuf, rfl, AccFrom.refl t⟩ (by simp [fuel])
431 · intro m u ⟨i, hi, hn, hub, hul, hacc⟩
432 let u1 : Locals := { updL u (seg bytes (p + 16 * i) 16) with buf := .ref (.blk blk) (p + 16 * i + 16) }
433 have hne : (u1.n - 1 != 0) = true := by
434 have : u1.n = u.n := rfl
435 simp only [bne_iff_ne, ne_eq, this]
436 intro h0
437 have := congrArg UInt32.toNat h0
438 rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)] at this
439 simp at this; omega
440 refine ⟨u1, { u1 with n := u1.n - 1 }, ?_, ?_, ?_⟩
441 · refine OkOn.bind (do16_ok hb u (p + 16 * i) hub (by omega)) ?_
442 exact bufAdd16_ok hb _ (p + 16 * i) hub (by omega)
443 · show OkOn h (pure (u1.n - 1 != 0, { u1 with n := u1.n - 1 })) _
444 rw [hne]; exact OkOn.pure _ _
445 · refine ⟨i + 1, by omega, ?_, ?_, hul, ?_⟩
446 · show (u.n - 1).toNat = m + 1
447 rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
448 simp; omega
449 · show Ptr.ref (BRef.blk blk) (p + 16 * i + 16) = _
450 rw [show p + 16 * i + 16 = p + 16 * (i + 1) by omega]
451 · rw [show 16 * (i + 1) = 16 * i + 16 by omega, seg_add]
452 exact (hacc.updL _).congr rfl rfl
453 · intro u ⟨i, hi, hn, hub, hul, hacc⟩
454 let u1 : Locals := { updL u (seg bytes (p + 16 * i) 16) with buf := .ref (.blk blk) (p + 16 * i + 16) }
455 have he : (u1.n - 1 != 0) = false := by
456 have : u1.n = u.n := rfl
457 simp only [bne_eq_false_iff_eq, this]
458 apply UInt32.toNat_inj.mp
459 rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
460 simp; omega
461 refine ⟨u1, { u1 with n := u1.n - 1 }, ?_, ?_, ?_⟩
462 · refine OkOn.bind (do16_ok hb u (p + 16 * i) hub (by omega)) ?_
463 exact bufAdd16_ok hb _ (p + 16 * i) hub (by omega)
464 · show OkOn h (pure (u1.n - 1 != 0, { u1 with n := u1.n - 1 })) _
465 rw [he]; exact OkOn.pure _ _
466 · refine ⟨by simp [u1]; omega, hul, ?_⟩
467 have hi' : i = 346 := by omega
468 subst hi'
469 rw [show 5552 = 16 * 346 + 16 by rfl, seg_add]
470 exact (hacc.updL _).congr rfl rfl
471
472/-- Low 16 and high 16 bits combine into `lo + 65536 * hi`. -/
473theorem or_shift (x y : UInt64) (hx : x.toNat < 65536) (hy : y.toNat < 65536) :
474 (x ||| (y <<< 16)).toNat = x.toNat + 65536 * y.toNat := by
475 rw [UInt64.toNat_or, UInt64.toNat_shiftLeft]
476 have hs : y.toNat <<< (16 % 64) % 2 ^ 64 = y.toNat * 65536 := by
477 rw [Nat.shiftLeft_eq]; simp; omega
478 rw [show (16 : UInt64).toNat = 16 from rfl, hs, Nat.or_comm,
479 show y.toNat * 65536 = y.toNat <<< 16 by rw [Nat.shiftLeft_eq],
480 ← Nat.shiftLeft_add_eq_or_of_lt (by omega), Nat.shiftLeft_eq]
481 omega
482
483theorem low16 (a : UInt64) : (a &&& 65535).toNat = a.toNat % 65536 := by
484 rw [UInt64.toNat_and]
485 exact Nat.and_two_pow_sub_one_eq_mod a.toNat 16
486
487theorem high16 (a : UInt64) : (a >>> 16 &&& 65535).toNat = a.toNat / 65536 % 65536 := by
488 rw [UInt64.toNat_and, UInt64.toNat_shiftRight]
489 rw [show (65535 : UInt64).toNat = 2 ^ 16 - 1 from rfl, Nat.and_two_pow_sub_one_eq_mod]
490 simp [Nat.shiftRight_eq_div_pow]
491
492end Zlib.Adler32.Proofs
493
494/-!
495# Main theorem for adler32_z
496
497For every initial value `adler`, every live block, offset and length with
498`off + len ≤ size`, the translation of `adler32_z` terminates without
499undefined behavior, leaves the heap unchanged, and returns the RFC 1950
500Adler-32 of the bytes `off .. off+len-1`, continuing from `adler` (whose
501component sums are taken modulo 65521; bits above 32 are ignored, as in C).
502-/
503
504namespace Zlib.Adler32.Proofs
505open C Zlib.Adler32 Zlib.Adler32.Spec
506
507variable {h : Heap} {blk : Nat} {bytes : Array UInt8}
508
509theorem rel_init (a : UInt64) :
510 Rel 0 (a &&& 65535) (a >>> 16 &&& 65535)
511 ((a &&& 65535).toNat % 65521) ((a >>> 16 &&& 65535).toNat % 65521) := by
512 have h1 := low16 a
513 have h2 := high16 a
514 refine ⟨rfl, rfl, ?_, ?_⟩ <;> simp only [Nat.mul_zero, Nat.zero_mul, Nat.add_zero] <;> omega
515
516theorem rel_exact {a s : UInt64} {lo hi : Nat} (hr : Rel 0 a s lo hi)
517 (ha : a.toNat < 65521) (hs : s.toNat < 65521) : a.toNat = lo ∧ s.toNat = hi := by
518 obtain ⟨h1, h2, -, -⟩ := hr
519 exact ⟨by rw [← h1, Nat.mod_eq_of_lt ha], by rw [← h2, Nat.mod_eq_of_lt hs]⟩
520
521/-- Spec value from the final reduced component sums. -/
522theorem result_value (a x y : UInt64) (bs : List UInt8)
523 (hx : x.toNat = (sums ((a &&& 65535).toNat % 65521) ((a >>> 16 &&& 65535).toNat % 65521) bs).1)
524 (hy : y.toNat = (sums ((a &&& 65535).toNat % 65521) ((a >>> 16 &&& 65535).toNat % 65521) bs).2) :
525 (x ||| (y <<< 16)).toNat = Spec.adler32 a.toNat bs := by
526 have hlt := sums_lt ((a &&& 65535).toNat % 65521) ((a >>> 16 &&& 65535).toNat % 65521) bs
527 (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))
528 rw [show Spec.BASE = 65521 from rfl] at hlt
529 rw [or_shift x y (by omega) (by omega), hx, hy, Spec.adler32, low16, high16]
530 rfl
531
532/-- Long inputs (`len ≥ 16`): NMAX blocks, then 16-byte chunks, then bytes. -/
533theorem adler32_z_long (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
534 (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) (h16 : 16 ≤ L) :
535 ∃ r, OkOn h (adler32_z a (.ref (.blk blk) off) L.toUInt64) r ∧
536 r.toNat = Spec.adler32 a.toNat (seg bytes off L) := by
537 have hLn : L.toUInt64.toNat = L := by simp; omega
538 have hne1 : (L.toUInt64 == 1) = false := by
539 simp only [beq_eq_false_iff_ne, ne_eq]; intro e; have := congrArg UInt64.toNat e; simp at this; omega
540 have hnull : (Ptr.ref (BRef.blk blk) off == (Ptr.null : BPtr)) = false := by simp
541 have hn16 : ¬ (L.toUInt64 < 16) := by rw [UInt64.lt_iff_toNat_lt, hLn]; simp; omega
542 unfold adler32_z
543 rw [ite_eq_right_of_eq_false _ _ (by simp [hne1]), ite_eq_right_of_eq_false _ _ (by simp [hnull]),
544 ite_eq_right_of_eq_false _ _ (by simp [hn16])]
545 let lo := (a &&& 65535).toNat % 65521
546 let hi := (a >>> 16 &&& 65535).toNat % 65521
547 let q := L / 5552
548 let r := L % 5552
549 let s0 : Locals := { adler := a &&& 65535, sum2 := a >>> 16 &&& 65535, buf := .ref (.blk blk) off, len := L.toUInt64, n := 0 }
550 let P : Nat → Locals → Prop := fun k t => ∃ i, i + k = q ∧ t.buf = .ref (.blk blk) (off + 5552 * i) ∧
551 t.len.toNat = L - 5552 * i ∧
552 Rel 0 t.adler t.sum2 (sums lo hi (seg bytes off (5552 * i))).1 (sums lo hi (seg bytes off (5552 * i))).2 ∧
553 (1 ≤ i → t.adler.toNat < 65521 ∧ t.sum2.toNat < 65521)
554 let Q : Locals → Prop := fun t => t.buf = .ref (.blk blk) (off + 5552 * q) ∧ t.len.toNat = r ∧
555 Rel 0 t.adler t.sum2 (sums lo hi (seg bytes off (5552 * q))).1 (sums lo hi (seg bytes off (5552 * q))).2 ∧
556 (1 ≤ q → t.adler.toNat < 65521 ∧ t.sum2.toNat < 65521)
557 have hinit : P q s0 := ⟨0, by omega, by simp [s0], by simp [s0, hLn], rel_init a, by omega⟩
558 refine OkOn.bind_ex (cwhile_ok (h := h) P Q ?_ ?_ hinit (by simp [fuel]; omega)) ?_
559 · -- one NMAX block
560 rintro k t ⟨i, hi_, htb, htl, hrel, -⟩
561 have hge : decide (t.len ≥ NMAX) = true := by
562 simp only [decide_eq_true_eq, ge_iff_le, UInt64.le_iff_toNat_le, htl]; simp [NMAX]; omega
563 let t0 : Locals := { adler := t.adler, sum2 := t.sum2, buf := t.buf, len := t.len - NMAX, n := (NMAX / 16).toUInt32 }
564 obtain ⟨u, hu, hub, hul, hacc⟩ := nmaxBlock_ok hb t0 (off + 5552 * i) htb (by omega) nmax_div
565 refine ⟨t, { adler := u.adler % BASE, sum2 := u.sum2 % BASE, buf := u.buf, len := u.len, n := u.n }, ?_, ?_, ?_⟩
566 · show OkOn h (pure (decide (t.len ≥ NMAX), t)) _
567 rw [hge]; exact OkOn.pure _ _
568 · exact OkOn.bind hu (OkOn.pure _ _)
569 · have hacc' := acc_list (seg bytes (off + 5552 * i) 5552) 0 t0.adler t0.sum2 _ _ hrel (by simp [seg_length])
570 rw [seg_length] at hacc'
571 have hmod := rel_mod _ _ _ _ _ hacc'
572 refine ⟨i + 1, by omega, ?_, ?_, ?_, ?_⟩
573 · rw [hub, show off + 5552 * i + 5552 = off + 5552 * (i + 1) by omega]
574 · show u.len.toNat = _
575 rw [hul]; show (t.len - NMAX).toNat = _
576 rw [UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le, htl]; simp [NMAX]; omega), htl]
577 simp [NMAX]; omega
578 · rw [show 5552 * (i + 1) = 5552 * i + 5552 by omega, seg_add, sums_append]
579 obtain ⟨ha, hs⟩ := hacc
580 simp only [updL] at ha hs
581 show Rel 0 (u.adler % 65521) (u.sum2 % 65521) _ _
582 rw [ha, hs]
583 exact hmod
584 · intro _
585 simp only [UInt64.toNat_mod, BASE]
586 exact ⟨Nat.mod_lt _ (by decide), Nat.mod_lt _ (by decide)⟩
587 · -- loop exit
588 rintro t ⟨i, hi_, htb, htl, hrel, hred⟩
589 have hlt : decide (t.len ≥ NMAX) = false := by
590 simp only [decide_eq_false_iff_not, ge_iff_le, UInt64.le_iff_toNat_le, htl]; simp [NMAX]; omega
591 refine ⟨t, ?_, ?_⟩
592 · show OkOn h (pure (decide (t.len ≥ NMAX), t)) _
593 rw [hlt]; exact OkOn.pure _ _
594 · have : i = q := by omega
595 subst this
596 exact ⟨htb, by rw [htl]; omega, hrel, hred⟩
597 · -- remainder
598 rintro t ⟨htb, htl, hrel, hred⟩
599 by_cases hr0 : r = 0
600 · have hz : (t.len != 0) = false := by
601 simp only [bne_eq_false_iff_eq]; exact UInt64.toNat_inj.mp (by simp [htl, hr0])
602 rw [hz]
603 simp only [Bool.false_eq_true, ite_false]
604 have hq : 1 ≤ q := by omega
605 obtain ⟨ha, hs⟩ := hred hq
606 obtain ⟨ea, es⟩ := rel_exact hrel ha hs
607 refine ⟨_, OkOn.bind (OkOn.pure _ _) (OkOn.pure _ _), ?_⟩
608 have hseg : seg bytes off L = seg bytes off (5552 * q) := by
609 rw [show 5552 * q = L by omega]
610 rw [hseg]
611 exact result_value a t.adler t.sum2 _ ea es
612 · have hnz : (t.len != 0) = true := by
613 simp only [bne_iff_ne, ne_eq]; intro e; have := congrArg UInt64.toNat e; simp [htl] at this; omega
614 rw [hnz]
615 simp only [ite_true]
616 obtain ⟨c, hc, hcb, hcl, -, hcacc⟩ := chunkLoop_ok hb t (off + 5552 * q) htb (by rw [htl]; omega)
617 rw [htl] at hcb hcl hcacc
618 obtain ⟨d, hd, hdb, hdacc⟩ := byteLoop_ok hb c _ hcb (by rw [hcl]; omega)
619 rw [hcl] at hdb hdacc
620 have hall := hcacc.trans hdacc
621 have hlen : (seg bytes (off + 5552 * q) (16 * (r / 16)) ++ seg bytes (off + 5552 * q + 16 * (r / 16)) (r % 16)).length = r := by
622 simp [seg_length]; omega
623 have hrel' := acc_list _ 0 t.adler t.sum2 _ _ hrel (by rw [hlen]; omega)
624 rw [hlen] at hrel'
625 obtain ⟨hda, hds⟩ := hall
626 simp only [updL] at hda hds
627 refine ⟨_, OkOn.bind hc (OkOn.bind hd (OkOn.bind (OkOn.pure _ _) (OkOn.pure _ _))), ?_⟩
628 have hseg : seg bytes off L = seg bytes off (5552 * q) ++
629 (seg bytes (off + 5552 * q) (16 * (r / 16)) ++ seg bytes (off + 5552 * q + 16 * (r / 16)) (r % 16)) := by
630 rw [← seg_add, ← seg_add]; congr 1; omega
631 rw [hseg]
632 apply result_value
633 · rw [sums_append, show (d.adler % BASE).toNat = d.adler.toNat % 65521 by simp [BASE], hda]
634 exact hrel'.1
635 · rw [sums_append, show (d.sum2 % BASE).toNat = d.sum2.toNat % 65521 by simp [BASE], hds]
636 exact hrel'.2.1
637
638theorem add_small (x y : UInt64) (hxy : x.toNat + y.toNat < 2 ^ 64) : (x + y).toNat = x.toNat + y.toNat := by
639 rw [UInt64.toNat_add]; exact Nat.mod_eq_of_lt hxy
640
641theorem sub_small (x y : UInt64) (hyx : y.toNat ≤ x.toNat) : (x - y).toNat = x.toNat - y.toNat :=
642 UInt64.toNat_sub_of_le _ _ (by rw [UInt64.le_iff_toNat_le]; exact hyx)
643
644theorem base_toNat : (BASE : UInt64).toNat = 65521 := rfl
645
646/-- Short inputs (`len < 16`, `len ≠ 1`, including `len = 0`). -/
647theorem adler32_z_short (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
648 (hfit : off + L ≤ bytes.size) (h16 : L < 16) (h1 : L ≠ 1) :
649 ∃ r, OkOn h (adler32_z a (.ref (.blk blk) off) L.toUInt64) r ∧
650 r.toNat = Spec.adler32 a.toNat (seg bytes off L) := by
651 have hLn : L.toUInt64.toNat = L := by simp; omega
652 have hne1 : (L.toUInt64 == 1) = false := by
653 simp only [beq_eq_false_iff_ne, ne_eq]; intro e; have := congrArg UInt64.toNat e; simp at this; omega
654 have hnull : (Ptr.ref (BRef.blk blk) off == (Ptr.null : BPtr)) = false := by simp
655 have hy16 : L.toUInt64 < 16 := by rw [UInt64.lt_iff_toNat_lt, hLn]; simp; omega
656 unfold adler32_z
657 rw [ite_eq_right_of_eq_false _ _ (by simp [hne1]), ite_eq_right_of_eq_false _ _ (by simp [hnull]),
658 ite_eq_left hy16]
659 let s0 : Locals := { adler := a &&& 65535, sum2 := a >>> 16 &&& 65535, buf := .ref (.blk blk) off, len := L.toUInt64, n := 0 }
660 obtain ⟨d, hd, -, hacc⟩ := byteLoop_ok hb s0 off rfl (by simp [s0, hLn]; omega)
661 have hrel := acc_list (seg bytes off s0.len.toNat) 0 s0.adler s0.sum2 _ _ (rel_init a)
662 (by simp [seg_length, s0, hLn]; omega)
663 obtain ⟨hda, hds⟩ := hacc
664 simp only [updL] at hda hds
665 rw [← hda, ← hds] at hrel
666 obtain ⟨r1, r2, rb1, -⟩ := hrel
667 simp only [seg_length, s0, hLn] at r1 r2 rb1
668 refine OkOn.bind_ex (R := fun x => x = d) ⟨d, hd, rfl⟩ ?_
669 intro x hx
670 rw [hx]
671 dsimp only
672 have hres := result_value a (if d.adler ≥ BASE then d.adler - BASE else d.adler) (d.sum2 % BASE)
673 (seg bytes off L) ?_ ?_
674 · split
675 · next hge => exact ⟨_, OkOn.pure _ _, by simpa [hge] using hres⟩
676 · next hlt => exact ⟨_, OkOn.pure _ _, by simpa [hlt] using hres⟩
677 · split
678 · next hge =>
679 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat] at hge
680 rw [sub_small _ _ (by rw [base_toNat]; omega), base_toNat, ← r1]; omega
681 · next hlt =>
682 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat] at hlt
683 rw [← r1]; omega
684 · rw [UInt64.toNat_mod, base_toNat, r2]
685
686/-- `len == 1`: one byte with single conditional subtractions. -/
687theorem adler32_z_one (hb : h.bytes blk = some bytes) (a : UInt64) (off : Nat)
688 (hfit : off + 1 ≤ bytes.size) (hvalid : (a >>> 16 &&& 65535).toNat < 65521) :
689 ∃ r, OkOn h (adler32_z a (.ref (.blk blk) off) (1 : Nat).toUInt64) r ∧
690 r.toNat = Spec.adler32 a.toNat (seg bytes off 1) := by
691 unfold adler32_z
692 rw [ite_eq_left (by decide)]
693 refine OkOn.bind_ex ⟨bytes[off + 0]!, ?_, rfl⟩ ?_
694 · have := index8_ok (i := 0) hb (by omega : off + 0 < bytes.size)
695 rwa [getElem_eq_bang bytes _ (by omega)] at this
696 intro b hbv
697 subst hbv
698 have hA := low16 a
699 have hH := high16 a
700 have hb256 : (bytes[off + 0]!).toNat < 256 := UInt8.toNat_lt _
701 have hbn : (bytes[off + 0]!).toUInt64.toNat = (bytes[off + 0]!).toNat := UInt8.toNat_toUInt64 _
702 have hAm : (a &&& 65535).toNat < 65536 := by rw [hA]; omega
703 have hHm : (a >>> 16 &&& 65535).toNat < 65536 := by rw [hH]; omega
704 have hx : ((a &&& 65535) + (bytes[off + 0]!).toUInt64).toNat = (a &&& 65535).toNat + (bytes[off + 0]!).toNat := by
705 rw [add_small _ _ (by omega), hbn]
706 rw [seg_one]
707 simp only [Nat.add_zero] at hx hb256 hbn ⊢
708 split
709 · next hge =>
710 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat, hx] at hge
711 have hx' : ((a &&& 65535) + (bytes[off]!).toUInt64 - BASE).toNat = (a &&& 65535).toNat + (bytes[off]!).toNat - 65521 := by
712 rw [sub_small _ _ (by rw [base_toNat, hx]; omega), hx, base_toNat]
713 have hy : ((a >>> 16 &&& 65535) + ((a &&& 65535) + (bytes[off]!).toUInt64 - BASE)).toNat =
714 (a >>> 16 &&& 65535).toNat + ((a &&& 65535).toNat + (bytes[off]!).toNat - 65521) := by
715 rw [add_small _ _ (by rw [hx']; omega), hx']
716 split
717 · next hge2 =>
718 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat, hy] at hge2
719 refine ⟨_, OkOn.pure _ _, result_value a _ _ _ ?_ ?_⟩
720 · rw [hx']; simp only [sums, List.foldl, step, Spec.BASE]; omega
721 · rw [sub_small _ _ (by rw [base_toNat, hy]; omega), hy, base_toNat]
722 simp only [sums, List.foldl, step, Spec.BASE]; omega
723 · next hlt2 =>
724 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat, hy] at hlt2
725 refine ⟨_, OkOn.pure _ _, result_value a _ _ _ ?_ ?_⟩
726 · rw [hx']; simp only [sums, List.foldl, step, Spec.BASE]; omega
727 · rw [hy]; simp only [sums, List.foldl, step, Spec.BASE]; omega
728 · next hlt =>
729 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat, hx] at hlt
730 have hy : ((a >>> 16 &&& 65535) + ((a &&& 65535) + (bytes[off]!).toUInt64)).toNat =
731 (a >>> 16 &&& 65535).toNat + ((a &&& 65535).toNat + (bytes[off]!).toNat) := by
732 rw [add_small _ _ (by rw [hx]; omega), hx]
733 split
734 · next hge2 =>
735 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat, hy] at hge2
736 refine ⟨_, OkOn.pure _ _, result_value a _ _ _ ?_ ?_⟩
737 · rw [hx]; simp only [sums, List.foldl, step, Spec.BASE]; omega
738 · rw [sub_small _ _ (by rw [base_toNat, hy]; omega), hy, base_toNat]
739 simp only [sums, List.foldl, step, Spec.BASE]; omega
740 · next hlt2 =>
741 rw [ge_iff_le, UInt64.le_iff_toNat_le, base_toNat, hy] at hlt2
742 refine ⟨_, OkOn.pure _ _, result_value a _ _ _ ?_ ?_⟩
743 · rw [hx]; simp only [sums, List.foldl, step, Spec.BASE]; omega
744 · rw [hy]; simp only [sums, List.foldl, step, Spec.BASE]; omega
745
746/-- `len == 1` is safe for every initial value (no validity needed). -/
747theorem adler32_z_one_safe (hb : h.bytes blk = some bytes) (a : UInt64) (off : Nat)
748 (hfit : off + 1 ≤ bytes.size) :
749 ∃ r, OkOn h (adler32_z a (.ref (.blk blk) off) (1 : Nat).toUInt64) r ∧ True := by
750 unfold adler32_z
751 rw [ite_eq_left (by decide)]
752 refine OkOn.bind_ex (index8_ok (i := 0) hb (by omega : off + 0 < bytes.size)).bind_ex_pure ?_
753 intro b _
754 dsimp only
755 split <;> split <;> exact ⟨_, OkOn.pure _ _, trivial⟩
756
757
758end Zlib.Adler32.Proofs
759
760namespace Zlib.Adler32.Proofs
761
762/-- A zero-length NULL query returns the initial checksum for every seed. -/
763theorem adler32_z_null_init (seed : UInt64) :
764 Zlib.Adler32.adler32_z seed (C.Ptr.null : C.BPtr) 0 = (pure 1 : C.M UInt64) := by
765 simp [Zlib.Adler32.adler32_z]
766
767/-- The ordinary-length wrapper preserves the zero-length NULL query. -/
768theorem adler32_null_init (seed : UInt64) :
769 Zlib.Adler32.adler32 seed (C.Ptr.null : C.BPtr) 0 = (pure 1 : C.M UInt64) := by
770 exact adler32_z_null_init seed
771
772end Zlib.Adler32.Proofs
773
774/-! ## Main theorems
775
776They state Theorems A1 (safety) and A2 (correctness) of `docs/proof/adler32.md`. -/
777
778namespace Zlib.Adler32.Proofs
779open C Zlib.Adler32 Zlib.Adler32.Spec
780
781/-- **Main theorem.** For every live block, offset and length that fits in the
782block, and every initial value whose high component sum is canonical
783(`< 65521`, true of any value adler32 itself returns), `adler32_z` runs
784without undefined behavior, terminates, leaves the heap unchanged and returns
785the Adler-32 of the bytes. -/
786theorem adler32_z_correct (h : Heap) (blk : Nat) (bytes : Array UInt8)
787 (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
788 (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) (hvalid : (a >>> 16 &&& 65535).toNat < 65521) :
789 ∃ r, C.run (adler32_z a (.ref (.blk blk) off) L.toUInt64) h = .ok (r, h) ∧
790 r.toNat = Spec.adler32 a.toNat (seg bytes off L) := by
791 by_cases h1 : L = 1
792 · subst h1; exact adler32_z_one hb a off hfit hvalid
793 · by_cases h16 : L < 16
794 · exact adler32_z_short hb a off L hfit h16 h1
795 · exact adler32_z_long hb a off L hfit hL (by omega)
796
797/-- For `len ≠ 1` the result is the Adler-32 for **every** initial value. -/
798theorem adler32_z_correct_ne_one (h : Heap) (blk : Nat) (bytes : Array UInt8)
799 (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
800 (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) (h1 : L ≠ 1) :
801 ∃ r, C.run (adler32_z a (.ref (.blk blk) off) L.toUInt64) h = .ok (r, h) ∧
802 r.toNat = Spec.adler32 a.toNat (seg bytes off L) := by
803 by_cases h16 : L < 16
804 · exact adler32_z_short hb a off L hfit h16 h1
805 · exact adler32_z_long hb a off L hfit hL (by omega)
806
807/-- **Safety.** For every initial value, `adler32_z` on an in-bounds buffer
808terminates without undefined behavior and leaves the heap unchanged. -/
809theorem adler32_z_safe (h : Heap) (blk : Nat) (bytes : Array UInt8)
810 (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
811 (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) :
812 ∃ r, C.run (adler32_z a (.ref (.blk blk) off) L.toUInt64) h = .ok (r, h) := by
813 by_cases h1 : L = 1
814 · subst h1; obtain ⟨r, hr, -⟩ := adler32_z_one_safe hb a off hfit; exact ⟨r, hr⟩
815 · obtain ⟨r, hr, -⟩ := adler32_z_correct_ne_one h blk bytes hb a off L hfit hL h1; exact ⟨r, hr⟩
816
817end Zlib.Adler32.Proofs
818
819namespace Zlib.Adler32.Proofs
820open C Zlib.Adler32 Zlib.Adler32.Spec
821
822variable {h : Heap}
823
824theorem len2_rem (x : Int64) (h0 : 0 ≤ x) :
825 (x % 65521).toUInt64.toUInt32.toUInt64.toNat = x.toInt.toNat % 65521 := by
826 have hx : 0 ≤ x.toInt := Int64.le_iff_toInt_le.mp h0
827 have hm : (x % 65521).toInt = x.toInt.tmod 65521 := Int64.toInt_mod x 65521
828 have hm0 : 0 ≤ x % 65521 := by
829 rw [Int64.le_iff_toInt_le, hm]; simp; exact Int.tmod_nonneg _ hx
830 rw [UInt32.toNat_toUInt64, UInt64.toNat_toUInt32, Int64.toNat_toUInt64_of_le hm0,
831 ← Int64.toNat_toInt, hm, Int.tmod_eq_emod_of_nonneg hx]
832 omega
833
834theorem toNat_sub' (x y : UInt64) : (x - y).toNat = (x.toNat + (2 ^ 64 - y.toNat)) % 2 ^ 64 := by
835 rw [UInt64.toNat_sub]; have := y.toNat_lt; omega
836
837/-- `if (x >= c) x -= c;` -/
838def csub (x c : UInt64) : UInt64 := if x ≥ c then x - c else x
839
840theorem csub_toNat (x c : UInt64) :
841 (csub x c).toNat = if c.toNat ≤ x.toNat then x.toNat - c.toNat else x.toNat := by
842 unfold csub
843 by_cases hc : c.toNat ≤ x.toNat
844 · have : x ≥ c := UInt64.le_iff_toNat_le.mpr hc
845 rw [ite_eq_left this, ite_eq_left hc, sub_small _ _ hc]
846 · have : ¬ x ≥ c := fun h' => hc (UInt64.le_iff_toNat_le.mp h')
847 rw [ite_eq_right this, ite_eq_right hc]
848
849/-- Value of `adler32_combine_` on canonical inputs (all four halves `< 65521`). -/
850theorem combine_value (a1 a2 : UInt64) (len2 : Int64) (h0 : 0 ≤ len2)
851 (hl1 : (a1 &&& 65535).toNat < 65521) (hh1 : (a1 >>> 16 &&& 65535).toNat < 65521)
852 (hl2 : (a2 &&& 65535).toNat < 65521) (hh2 : (a2 >>> 16 &&& 65535).toNat < 65521) :
853 ∃ r, OkOn h (adler32_combine_ a1 a2 len2) r ∧
854 r.toNat = ((a1 &&& 65535).toNat + (a2 &&& 65535).toNat + 65521 - 1) % 65521 +
855 65536 * (((len2.toInt.toNat % 65521) * (a1 &&& 65535).toNat % 65521 +
856 (a1 >>> 16 &&& 65535).toNat + (a2 >>> 16 &&& 65535).toNat + 65521 -
857 len2.toInt.toNat % 65521) % 65521) := by
858 unfold adler32_combine_
859 have hz : (0 : Int64).toInt = 0 := rfl
860 rw [ite_eq_right (by
861 intro hneg
862 have a := Int64.lt_iff_toInt_lt.mp hneg
863 have b := Int64.le_iff_toInt_le.mp h0
864 rw [hz] at a b; omega)]
865 dsimp only
866 have hm := len2_rem len2 h0
867 have hn : len2.toInt.toNat % 65521 < 65521 := Nat.mod_lt _ (by decide)
868 generalize len2.toInt.toNat % 65521 = n at hm hn ⊢
869 generalize (len2 % 65521).toUInt64.toUInt32.toUInt64 = M at hm ⊢
870 generalize hA1 : a1 &&& 65535 = A1 at hl1 ⊢
871 generalize hH1 : a1 >>> 16 &&& 65535 = H1 at hh1 ⊢
872 generalize hA2 : a2 &&& 65535 = A2 at hl2 ⊢
873 generalize hH2 : a2 >>> 16 &&& 65535 = H2 at hh2 ⊢
874 have hprod : n * A1.toNat < 65521 * 65521 := Nat.mul_lt_mul'' hn hl1
875 have hP : (M * A1).toNat = n * A1.toNat := by
876 rw [UInt64.toNat_mul, hm]; exact Nat.mod_eq_of_lt (by omega)
877 generalize M * A1 = P at hP ⊢
878 have hB : (BASE : UInt64).toNat = 65521 := rfl
879 have hB2 : (BASE <<< 1 : UInt64).toNat = 131042 := rfl
880 have hpm : (P % BASE).toNat = n * A1.toNat % 65521 := by rw [UInt64.toNat_mod, hP, hB]
881 generalize P % BASE = Pm at hpm ⊢
882 have hpmlt : Pm.toNat < 65521 := by rw [hpm]; exact Nat.mod_lt _ (by decide)
883 -- The two accumulated sums never wrap: compute them exactly, then abstract.
884 have hS1 : (A1 + (A2 + BASE - 1)).toNat = A1.toNat + A2.toNat + 65520 := by
885 have e1 : (A2 + BASE).toNat = A2.toNat + 65521 := by rw [add_small _ _ (by rw [hB]; omega), hB]
886 have e2 : (A2 + BASE - 1).toNat = A2.toNat + 65520 := by
887 rw [sub_small _ _ (by rw [e1]; simp), e1]; simp
888 rw [add_small _ _ (by rw [e2]; omega), e2]; omega
889 have hS2 : (Pm + (H1 + H2 + BASE - M)).toNat = Pm.toNat + H1.toNat + H2.toNat + 65521 - n := by
890 have e1 : (H1 + H2).toNat = H1.toNat + H2.toNat := add_small _ _ (by omega)
891 have e2 : (H1 + H2 + BASE).toNat = H1.toNat + H2.toNat + 65521 := by
892 rw [add_small _ _ (by rw [e1, hB]; omega), e1, hB]
893 have e3 : (H1 + H2 + BASE - M).toNat = H1.toNat + H2.toNat + 65521 - n := by
894 rw [sub_small _ _ (by rw [e2, hm]; omega), e2, hm]
895 rw [add_small _ _ (by rw [e3]; omega), e3]; omega
896 generalize A1 + (A2 + BASE - 1) = S1 at hS1 ⊢
897 generalize Pm + (H1 + H2 + BASE - M) = S2 at hS2 ⊢
898 have sub' : ∀ x y : UInt64, y.toNat ≤ x.toNat → (x - y).toNat = x.toNat - y.toNat := sub_small
899 have key : ∀ v : UInt64,
900 v = csub (csub S1 BASE) BASE ||| csub (csub S2 (BASE <<< 1)) BASE <<< 16 →
901 ∃ r, OkOn h (pure v) r ∧ r.toNat = (A1.toNat + A2.toNat + 65521 - 1) % 65521 +
902 65536 * ((n * A1.toNat % 65521 + H1.toNat + H2.toNat + 65521 - n) % 65521) := by
903 intro v hv
904 refine ⟨v, OkOn.pure _ _, ?_⟩
905 have c1 : (csub (csub S1 BASE) BASE).toNat = (A1.toNat + A2.toNat + 65521 - 1) % 65521 := by
906 rw [csub_toNat, csub_toNat, hB, hS1]
907 split <;> (try split) <;> omega
908 have c2 : (csub (csub S2 (BASE <<< 1)) BASE).toNat =
909 (n * A1.toNat % 65521 + H1.toNat + H2.toNat + 65521 - n) % 65521 := by
910 rw [csub_toNat, csub_toNat, hB, hB2, hS2, hpm]
911 split <;> (try split) <;> omega
912 rw [hv, or_shift _ _ (by rw [c1]; omega) (by rw [c2]; omega), c1, c2]
913 repeat' split
914 all_goals
915 apply key
916 simp only [csub]
917 repeat' split
918 all_goals first
919 | rfl
920 | (exfalso; simp only [ge_iff_le, UInt64.le_iff_toNat_le, Nat.not_le] at *; omega)
921
922theorem halves (st : Nat × Nat) (h1 : st.1 < 65521) (h2 : st.2 < 65521) :
923 ((st.1 + 65536 * st.2).toUInt64 &&& 65535).toNat = st.1 ∧
924 ((st.1 + 65536 * st.2).toUInt64 >>> 16 &&& 65535).toNat = st.2 := by
925 have hv : (st.1 + 65536 * st.2).toUInt64.toNat = st.1 + 65536 * st.2 := by simp; omega
926 rw [low16, high16, hv]
927 omega
928
929end Zlib.Adler32.Proofs
930
931/-! ## Theorems for `adler32_combine`, `adler32_combine64` and `adler32`
932
933The combination theorem says that `adler32_combine64` of the checksums of `A` and `B`, with `len2` the length of `B`, is the checksum of `A ++ B`. -/
934
935namespace Zlib.Adler32.Proofs
936open C Zlib.Adler32 Zlib.Adler32.Spec
937
938variable {h : Heap}
939
940/-- `adler32_combine_` never faults and leaves the heap unchanged. -/
941theorem adler32_combine_safe (a1 a2 : UInt64) (len2 : Int64) :
942 ∃ r, OkOn h (adler32_combine_ a1 a2 len2) r := by
943 unfold adler32_combine_
944 split
945 · exact ⟨_, OkOn.pure _ _⟩
946 · try dsimp only
947 repeat' split
948 all_goals exact ⟨_, OkOn.pure _ _⟩
949
950/-- **Combination theorem.** For byte strings `A` and `B` (with `|B| < 2^63`),
951`adler32_combine64(adler32(A), adler32(B), |B|) = adler32(A ++ B)`, where
952`adler32` starts from the conventional initial value 1. -/
953theorem adler32_combine_correct (A B : List UInt8) (hB : B.length < 2 ^ 63) :
954 ∃ r, OkOn h (adler32_combine64 (Spec.adler32 1 A).toUInt64 (Spec.adler32 1 B).toUInt64
955 (Int64.ofNat B.length)) r ∧ r.toNat = Spec.adler32 1 (A ++ B) := by
956 have hx := sums_lt 1 0 A (by decide) (by decide)
957 have hy := sums_lt 1 0 B (by decide) (by decide)
958 simp only [Spec.BASE] at hx hy
959 have e1 : Spec.adler32 1 A = (sums 1 0 A).1 + 65536 * (sums 1 0 A).2 := rfl
960 have e2 : Spec.adler32 1 B = (sums 1 0 B).1 + 65536 * (sums 1 0 B).2 := rfl
961 have e3 : Spec.adler32 1 (A ++ B) = (sums 1 0 (A ++ B)).1 + 65536 * (sums 1 0 (A ++ B)).2 := rfl
962 obtain ⟨l1, h1⟩ := halves (sums 1 0 A) hx.1 hx.2
963 obtain ⟨l2, h2⟩ := halves (sums 1 0 B) hy.1 hy.2
964 have hlen0 : (0 : Int64) ≤ Int64.ofNat B.length := by
965 rw [Int64.le_iff_toInt_le, Int64.toInt_ofNat_of_lt (by omega : B.length < 2 ^ 63)]
966 exact Int.natCast_nonneg _
967 have hlen : (Int64.ofNat B.length).toInt.toNat = B.length := by
968 rw [Int64.toInt_ofNat_of_lt (by omega)]; simp
969 rw [e1, e2] at *
970 obtain ⟨r, hr, hv⟩ := combine_value (h := h) _ _ _ hlen0 (by rw [l1]; exact hx.1) (by rw [h1]; exact hx.2)
971 (by rw [l2]; exact hy.1) (by rw [h2]; exact hy.2)
972 refine ⟨r, hr, ?_⟩
973 rw [hv, l1, h1, l2, h2, hlen, e3, sums_combine]
974 simp only [Spec.BASE]
975
976/-- `adler32_combine64` is `adler32_combine_`: it never faults. -/
977theorem adler32_combine64_safe (a1 a2 : UInt64) (len2 : Int64) :
978 ∃ r, OkOn h (adler32_combine64 a1 a2 len2) r := by
979 exact adler32_combine_safe a1 a2 len2
980
981/-- `adler32_combine` is `adler32_combine_`: it never faults. -/
982theorem adler32_combine_c_safe (a1 a2 : UInt64) (len2 : Int64) :
983 ∃ r, OkOn h (adler32_combine a1 a2 len2) r := by
984 exact adler32_combine_safe a1 a2 len2
985
986/-- `adler32` is `adler32_z` with a 32-bit length: it never faults on an in-bounds buffer. -/
987theorem adler32_safe (h : Heap) (blk : Nat) (bytes : Array UInt8)
988 (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
989 (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 32) :
990 ∃ r, C.run (adler32 a (.ref (.blk blk) off) L.toUInt32) h = .ok (r, h) := by
991 have hL' : L < 2 ^ 64 := by omega
992 have e : L.toUInt32.toUInt64 = L.toUInt64 := by
993 apply UInt64.toNat_inj.mp
994 simp [Nat.mod_eq_of_lt hL, Nat.mod_eq_of_lt hL']
995 unfold adler32
996 rw [e]
997 exact adler32_z_safe h blk bytes hb a off L hfit hL'
998
999end Zlib.Adler32.Proofs
1000
1001
1002namespace Zlib.Adler32.Proofs
1003open C Zlib.Adler32
1004
1005/-- Result value of a run, if it returns. -/
1006def resultOf {α} (r : Except Fault (α × Heap)) : Option α :=
1007 match r with
1008 | .ok (x, _) => some x
1009 | .error _ => none
1010
1011/-- The `hvalid` precondition of `adler32_z_correct` is necessary: with initial
1012value `0xFFFFFFF0` (high half 65535, not canonical) and the single byte 0, the
1013C code subtracts BASE only once and returns `sum2 = 65534`, while the Adler-32
1014spec gives 13. -/
1015theorem adler32_z_one_noncanonical :
1016 resultOf (C.run (adler32_z 0xFFFFFFF0 (.ref (.blk 0) 0) 1) { Heap.empty with bytes := C.upd Tbl.empty 0 (some #[0]) }) =
1017 some (65520 + 65536 * 65534) ∧
1018 Spec.adler32 (0xFFFFFFF0 : UInt64).toNat [0] = 65520 + 65536 * 13 := by
1019 constructor <;> decide
1020
1021end Zlib.Adler32.Proofs
1022