crc32.c.lean

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

1import ZlibF.Zlib.«crc32.c»
2import ZlibF.Spec.Format.Checksum
3
4/-!
5# crc32.c: safety and correctness
6
7Every function of `crc32.c.lean` has a safety theorem (`*_safe`: no fault, the heap is unchanged, so every heap
8invariant and frame is preserved; preconditions explicit) and a correctness theorem (`*_correct`: the value, against
9`ZlibF.Spec.crc32Update` / `ZlibF.Spec.crc32` and `ZlibF.Spec.crcBit`, which do not mention the translation).
10
11The heap hypothesis `StaticsOK` says that the static tables `crc_table` and `x2n_table` hold the contents `crc32.h`
12fixes (`Zlib.Crc32.initStatics`). The other tables (`crc_braid_table`, `crc_big_table`, `crc_braid_big_table`) are
13constants of the translation.
14
15Method. A CRC register step is linear over GF(2) (`crcBit_xor`). `pw m` is `m` steps of `ZlibF.Spec.crcBit`
16(multiplication by `x^m`). From the table contents (checked by kernel evaluation, `decide +kernel`, no axioms):
17`crc_table[n] = pw 8 n` (`crc_table_eq`), `crc_braid_table[j][n] = pw (8 * (40 - j)) n` (`braid_eq`), and the
18squaring chain of `x2n_table` with `x^(2^32) = x` (`Xt_sq`, `Xt_wrap`). The word step of `crc_word` is a linear map of
1964-bit words that agrees with the closed form `Psi` on the 64 unit vectors (`Phi_eq_Psi`), hence everywhere. The braided
20loop keeps the invariant `Val c0 .. c4 = pw 320 R` where `R` is the register of the bytes consumed so far
21(`loopBlk_ok`); the final chain of `crc_word` calls then equals `rbFrom R ow 40` (`chain_aff`, `chain_zero`,
22`val_step`). `multmodp` is multiplication in the algebra of registers (`mulp`): bilinear, associative
23(`mulp_assoc`), with `mulp (x^m) v = pw m v` (`mulp_pw_left'`).
24
25Not covered: the big-endian helpers (`byte_swap`, `blockBig`, `crc_word_big`, dead at run time on the target): only
26`crc_word_big_safe`; `byte_swap` is a total pure function with no correctness theorem; `blockBig` has none.
27-/
28
29namespace Zlib.Crc32.Proofs
30open C
31open ZlibF.Spec (crcBit crcPoly)
32
33/-! ### Bit lemmas -/
34
35theorem u32_ext {x y : UInt32} (h : ∀ i, i < 32 → x.toBitVec.getLsbD i = y.toBitVec.getLsbD i) : x = y :=
36  UInt32.eq_of_toBitVec_eq (BitVec.eq_of_getLsbD_eq h)
37
38theorem u64_ext {x y : UInt64} (h : ∀ i, i < 64 → x.toBitVec.getLsbD i = y.toBitVec.getLsbD i) : x = y :=
39  UInt64.eq_of_toBitVec_eq (BitVec.eq_of_getLsbD_eq h)
40
41theorem and_xor32 (a b m : UInt32) : (a ^^^ b) &&& m = (a &&& m) ^^^ (b &&& m) := by
42  apply u32_ext; intro i _
43  simp only [UInt32.toBitVec_and, UInt32.toBitVec_xor, BitVec.getLsbD_and, BitVec.getLsbD_xor]
44  cases a.toBitVec.getLsbD i <;> cases b.toBitVec.getLsbD i <;> cases m.toBitVec.getLsbD i <;> rfl
45
46theorem and_xor64 (a b m : UInt64) : (a ^^^ b) &&& m = (a &&& m) ^^^ (b &&& m) := by
47  apply u64_ext; intro i _
48  simp only [UInt64.toBitVec_and, UInt64.toBitVec_xor, BitVec.getLsbD_and, BitVec.getLsbD_xor]
49  cases a.toBitVec.getLsbD i <;> cases b.toBitVec.getLsbD i <;> cases m.toBitVec.getLsbD i <;> rfl
50
51theorem and1_cases (x : UInt32) : x &&& 1 = 0 ∨ x &&& 1 = 1 := by
52  have h : (x &&& 1).toNat = x.toNat % 2 := by
53    rw [UInt32.toNat_and]; exact Nat.and_one_is_mod _
54  rcases (by omega : x.toNat % 2 = 0 ∨ x.toNat % 2 = 1) with h0 | h0
55  · left; apply UInt32.toNat_inj.mp; simp [h, h0]
56  · right; apply UInt32.toNat_inj.mp; simp [h, h0]
57
58theorem xor_cancel32 (a b : UInt32) : a ^^^ (a ^^^ b) = b := by
59  rw [← UInt32.xor_assoc, UInt32.xor_self, UInt32.zero_xor]
60theorem xor_cancel64 (a b : UInt64) : a ^^^ (a ^^^ b) = b := by
61  rw [← UInt64.xor_assoc, UInt64.xor_self, UInt64.zero_xor]
62theorem xor_pp32 (a b p : UInt32) : (a ^^^ p) ^^^ (b ^^^ p) = a ^^^ b := by
63  apply u32_ext; intro i _
64  simp only [UInt32.toBitVec_xor, BitVec.getLsbD_xor]
65  cases a.toBitVec.getLsbD i <;> cases b.toBitVec.getLsbD i <;> cases p.toBitVec.getLsbD i <;> rfl
66
67theorem crcBit_xor (x y : UInt32) : crcBit (x ^^^ y) = crcBit x ^^^ crcBit y := by
68  unfold crcBit
69  have e : (x ^^^ y) &&& 1 = (x &&& 1) ^^^ (y &&& 1) := and_xor32 _ _ _
70  rcases and1_cases x with hx | hx <;> rcases and1_cases y with hy | hy <;>
71    simp [e, hx, hy, UInt32.shiftRight_xor, xor_pp32, xor_cancel32]
72  · ac_rfl
73  · ac_rfl
74
75theorem crcBit_zero : crcBit 0 = 0 := by decide
76
77/-- `m` register steps of the CRC (multiplication by `x^m` in the bit-reflected representation). -/
78def pw : Nat → UInt32 → UInt32
79  | 0, v => v
80  | m + 1, v => pw m (ZlibF.Spec.crcBit v)
81
82theorem pw_zero_n (v : UInt32) : pw 0 v = v := rfl
83theorem pw_succ (m : Nat) (v : UInt32) : pw (m + 1) v = pw m (ZlibF.Spec.crcBit v) := rfl
84theorem pw_succ' (m : Nat) (v : UInt32) : pw (m + 1) v = ZlibF.Spec.crcBit (pw m v) := by
85  induction m generalizing v with
86  | zero => rfl
87  | succ m ih => rw [pw_succ, ih, pw_succ]
88theorem pw_add (m n : Nat) (v : UInt32) : pw (m + n) v = pw m (pw n v) := by
89  induction n generalizing v with
90  | zero => rfl
91  | succ n ih => rw [← Nat.add_assoc, pw_succ, ih, pw_succ]
92theorem pw_xor (m : Nat) (x y : UInt32) : pw m (x ^^^ y) = pw m x ^^^ pw m y := by
93  induction m generalizing x y with
94  | zero => rfl
95  | succ m ih => rw [pw_succ, pw_succ, pw_succ, crcBit_xor, ih]
96theorem pw_zero (m : Nat) : pw m 0 = 0 := by
97  induction m with
98  | zero => rfl
99  | succ m ih => rw [pw_succ, crcBit_zero, ih]
100
101theorem crcByte_eq (c : UInt32) (b : UInt8) : ZlibF.Spec.crcByte c b = pw 8 (c ^^^ b.toUInt32) := by
102  unfold ZlibF.Spec.crcByte
103  generalize c ^^^ b.toUInt32 = v
104  have : ∀ n, (List.range n).foldl (fun c _ => ZlibF.Spec.crcBit c) v = pw n v := by
105    intro n
106    induction n with
107    | zero => rfl
108    | succ n ih => rw [List.range_succ, List.foldl_append, ih, pw_succ']; rfl
109  exact this 8
110
111
112/-! ### Tables -/
113
114theorem crc_table_size : Crc32H.crc_table.size = 256 := by decide +kernel
115
116set_option maxRecDepth 100000 in
117theorem crc_table_eq : ∀ n : Fin 256, Crc32H.crc_table[n.val]! = pw 8 (UInt32.ofNat n.val) := by decide +kernel
118
119
120theorem braid_size : Crc32H.crc_braid_table.size = 8 ∧ ∀ j : Fin 8, Crc32H.crc_braid_table[j.val]!.size = 256 := by
121  decide +kernel
122
123set_option maxRecDepth 100000 in
124theorem braid_eq : ∀ j : Fin 8, ∀ n : Fin 256,
125    Crc32H.crc_braid_table[j.val]![n.val]! = pw (8 * (40 - j.val)) (UInt32.ofNat n.val) := by decide +kernel
126
127/-! ### Linear maps are determined by their values on the unit vectors -/
128
129theorem lin_ext_nat (w : Nat) (F G : Nat → Nat)
130    (hF : ∀ x y, F (x ^^^ y) = F x ^^^ F y) (hG : ∀ x y, G (x ^^^ y) = G x ^^^ G y)
131    (hb : ∀ t, t < w → F (2 ^ t) = G (2 ^ t)) : ∀ n, n ≤ w → ∀ x, x < 2 ^ n → F x = G x := by
132  have F0 : F 0 = 0 := by have := hF 0 0; simpa [Nat.xor_self] using this
133  have G0 : G 0 = 0 := by have := hG 0 0; simpa [Nat.xor_self] using this
134  intro n
135  induction n with
136  | zero => intro _ x hx; have : x = 0 := by simpa using hx
137            subst this; rw [F0, G0]
138  | succ n ih =>
139    intro hn x hx
140    by_cases hbit : x.testBit n
141    · have hy : (x ^^^ 2 ^ n) < 2 ^ n := by
142        apply Nat.lt_pow_two_of_testBit
143        intro i hi
144        rw [Nat.testBit_xor, Nat.testBit_two_pow]
145        rcases Nat.eq_or_lt_of_le hi with rfl | hlt
146        · simp [hbit]
147        · have : x.testBit i = false := Nat.testBit_lt_two_pow (by
148            exact Nat.lt_of_lt_of_le hx (Nat.pow_le_pow_right (by omega) (by omega)))
149          simp [this]; omega
150      have hx' : x = (x ^^^ 2 ^ n) ^^^ 2 ^ n := by
151        rw [Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
152      rw [hx', hF, hG, ih (by omega) _ hy, hb n (by omega)]
153    · have : x < 2 ^ n := by
154        apply Nat.lt_pow_two_of_testBit
155        intro i hi
156        rcases Nat.eq_or_lt_of_le hi with rfl | hlt
157        · simpa using hbit
158        · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hx (Nat.pow_le_pow_right (by omega) (by omega)))
159      exact ih (by omega) x this
160
161def Lin32 (f : UInt32 → UInt32) : Prop := ∀ x y, f (x ^^^ y) = f x ^^^ f y
162
163/-- The unit vector with bit `s` set. -/
164def e (s : Nat) : UInt32 := UInt32.ofNat (2 ^ s)
165
166theorem lin32_ext {f g : UInt32 → UInt32} (hf : Lin32 f) (hg : Lin32 g)
167    (hb : ∀ t, t < 32 → f (e t) = g (e t)) : ∀ x, f x = g x := by
168  intro x
169  have hf' : ∀ x y, f (x ^^^ y) = f x ^^^ f y := hf
170  have hg' : ∀ x y, g (x ^^^ y) = g x ^^^ g y := hg
171  have key := lin_ext_nat 32 (fun n => (f (UInt32.ofNat n)).toNat) (fun n => (g (UInt32.ofNat n)).toNat)
172    (by intro a b; simp only [UInt32.ofNat_xor, hf', UInt32.toNat_xor])
173    (by intro a b; simp only [UInt32.ofNat_xor, hg', UInt32.toNat_xor])
174    (by intro t ht; simp only [e] at hb; rw [hb t ht]) 32 (Nat.le_refl _) x.toNat (by simpa using UInt32.toNat_lt x)
175  simp only [UInt32.ofNat_toNat] at key
176  exact UInt32.toNat_inj.mp key
177
178theorem lin32_zero {f : UInt32 → UInt32} (hf : Lin32 f) : f 0 = 0 := by
179  have := hf 0 0
180  simpa using this
181
182/-! ### Multiplication in the bit-reflected representation -/
183
184/-- coefficient of `x^j` in `a` (bit `31 - j`) -/
185def bitAt (a : UInt32) (j : Nat) : Bool := decide (j < 32) && a.toNat.testBit (31 - j)
186
187def mulpAux (a b : UInt32) : Nat → UInt32
188  | 0 => 0
189  | n + 1 => mulpAux a b n ^^^ (if bitAt a n then pw n b else 0)
190
191/-- the product of `multmodp`: `a * b` modulo the CRC polynomial -/
192def mulp (a b : UInt32) : UInt32 := mulpAux a b 32
193
194theorem bitAt_xor (a b : UInt32) (j : Nat) : bitAt (a ^^^ b) j = (bitAt a j ^^ bitAt b j) := by
195  unfold bitAt; rw [UInt32.toNat_xor, Nat.testBit_xor]
196  by_cases h : j < 32 <;> simp [h]
197
198theorem ite_xor (p q : Bool) (t : UInt32) :
199    (if (p ^^ q) = true then t else 0) = (if p = true then t else 0) ^^^ (if q = true then t else 0) := by
200  cases p <;> cases q <;> simp [UInt32.xor_self]
201
202theorem mulpAux_xor_left (a a' b : UInt32) (n : Nat) :
203    mulpAux (a ^^^ a') b n = mulpAux a b n ^^^ mulpAux a' b n := by
204  induction n with
205  | zero => simp [mulpAux]
206  | succ n ih =>
207    simp only [mulpAux, ih, bitAt_xor, ite_xor]; ac_rfl
208
209theorem mulpAux_xor_right (a b b' : UInt32) (n : Nat) :
210    mulpAux a (b ^^^ b') n = mulpAux a b n ^^^ mulpAux a b' n := by
211  induction n with
212  | zero => simp [mulpAux]
213  | succ n ih =>
214    simp only [mulpAux, ih, pw_xor]
215    cases bitAt a n <;> simp <;> ac_rfl
216
217theorem mulp_xor_left (a a' b : UInt32) : mulp (a ^^^ a') b = mulp a b ^^^ mulp a' b := mulpAux_xor_left ..
218theorem mulp_xor_right (a b b' : UInt32) : mulp a (b ^^^ b') = mulp a b ^^^ mulp a b' := mulpAux_xor_right ..
219
220theorem mulpAux_zero_left (b : UInt32) (n : Nat) : mulpAux 0 b n = 0 := by
221  induction n with
222  | zero => rfl
223  | succ n ih => simp [mulpAux, ih, bitAt]
224theorem mulp_zero_left (b : UInt32) : mulp 0 b = 0 := mulpAux_zero_left b 32
225
226theorem tb_e (s i : Nat) (hs : s < 32) : (e s).toNat.testBit i = decide (s = i) := by
227  simp only [e, UInt32.toNat_ofNat']
228  rw [Nat.mod_eq_of_lt (Nat.pow_lt_pow_right (by omega) hs), Nat.testBit_two_pow]
229
230theorem bitAt_e (s : Nat) (hs : s < 32) (j : Nat) : bitAt (e s) j = decide (j < 32 ∧ 31 - j = s) := by
231  unfold bitAt; rw [tb_e s _ hs]
232  by_cases h : j < 32
233  · simp [h]; omega
234  · simp [h]
235
236theorem mulpAux_e (s : Nat) (hs : s < 32) (b : UInt32) (n : Nat) (hn : n ≤ 32) :
237    mulpAux (e s) b n = if 31 - s < n then pw (31 - s) b else 0 := by
238  induction n with
239  | zero => simp [mulpAux]
240  | succ n ih =>
241    simp only [mulpAux, ih (by omega), bitAt_e s hs]
242    by_cases h2 : 31 - s = n
243    · have h3 : n < 32 := by omega
244      have h5 : 31 - n = s := by omega
245      simp [h2, h3, h5]
246    · have h3 : ¬ (n < 32 ∧ 31 - n = s) := by omega
247      simp [h3]
248      by_cases h4 : 31 - s < n
249      · simp [h4, show 31 - s < n + 1 by omega]
250      · simp [h4, show ¬ 31 - s < n + 1 by omega]
251
252theorem mulp_e (s : Nat) (hs : s < 32) (b : UInt32) : mulp (e s) b = pw (31 - s) b := by
253  unfold mulp; rw [mulpAux_e s hs b 32 (Nat.le_refl _)]; simp; omega
254
255set_option maxRecDepth 100000 in
256theorem crcBit_e : ∀ s : Fin 32, crcBit (e s.val) = if s.val = 0 then crcPoly else e (s.val - 1) := by
257  decide +kernel
258
259set_option maxRecDepth 100000 in
260theorem mulp_poly_basis : ∀ t : Fin 32, mulp crcPoly (e t.val) = pw 32 (e t.val) := by decide +kernel
261
262theorem mulp_lin_right (a : UInt32) : Lin32 (mulp a) := fun x y => mulp_xor_right a x y
263theorem pw_lin (m : Nat) : Lin32 (pw m) := fun x y => pw_xor m x y
264
265theorem mulp_poly (v : UInt32) : mulp crcPoly v = pw 32 v :=
266  lin32_ext (mulp_lin_right crcPoly) (pw_lin 32) (fun t ht => mulp_poly_basis ⟨t, ht⟩) v
267
268theorem mulp_crcBit_left (a v : UInt32) : mulp (crcBit a) v = crcBit (mulp a v) := by
269  refine lin32_ext (f := fun a => mulp (crcBit a) v) (g := fun a => crcBit (mulp a v)) ?_ ?_ ?_ a
270  · intro x y; simp only [crcBit_xor, mulp_xor_left]
271  · intro x y; simp only [mulp_xor_left, crcBit_xor]
272  · intro t ht
273    have h := crcBit_e ⟨t, ht⟩
274    simp only at h
275    show mulp (crcBit (e t)) v = crcBit (mulp (e t) v)
276    rw [h, mulp_e t ht]
277    by_cases h0 : t = 0
278    · subst h0
279      simp only [ite_true]
280      rw [mulp_poly]
281      show pw 32 v = crcBit (pw 31 v)
282      rw [← pw_succ']
283    · simp only [h0, ite_false]
284      rw [mulp_e (t - 1) (by omega)]
285      rw [show 31 - (t - 1) = (31 - t) + 1 by omega, pw_succ']
286
287theorem mulp_pw_left' (j : Nat) (a v : UInt32) : mulp (pw j a) v = pw j (mulp a v) := by
288  induction j generalizing a with
289  | zero => rfl
290  | succ j ih => rw [pw_succ', pw_succ', mulp_crcBit_left, ih]
291
292theorem mulp_one (v : UInt32) : mulp (e 31) v = v := by
293  rw [mulp_e 31 (by omega)]; rfl
294
295theorem mulpAux_assoc (a b v : UInt32) (n : Nat) : mulp (mulpAux a b n) v = mulpAux a (mulp b v) n := by
296  induction n with
297  | zero => simp [mulpAux, mulp_zero_left]
298  | succ n ih =>
299    simp only [mulpAux, mulp_xor_left, ih]
300    cases bitAt a n
301    · simp [mulp_zero_left]
302    · simp [mulp_pw_left']
303
304theorem mulp_assoc (a b v : UInt32) : mulp (mulp a b) v = mulp a (mulp b v) := mulpAux_assoc a b v 32
305
306/-! ### The table `x2n_table` -/
307
308def Xt (i : Nat) : UInt32 := Crc32H.x2n_table[i]!
309
310theorem x2n_size : Crc32H.x2n_table.size = 32 := by decide +kernel
311set_option maxRecDepth 100000 in
312theorem Xt_zero : Xt 0 = pw 1 (e 31) := by decide +kernel
313set_option maxRecDepth 100000 in
314theorem Xt_sq : ∀ i : Fin 31, Xt (i.val + 1) = mulp (Xt i.val) (Xt i.val) := by decide +kernel
315set_option maxRecDepth 100000 in
316theorem Xt_wrap : mulp (Xt 31) (Xt 31) = Xt 0 := by decide +kernel
317set_option maxRecDepth 100000 in
318theorem Xt_ne : ∀ i : Fin 32, Xt i.val ≠ 0 := by decide +kernel
319
320theorem Xt_pw : ∀ i, i < 32 → ∀ v, mulp (Xt i) v = pw (2 ^ i) v := by
321  intro i
322  induction i with
323  | zero =>
324    intro _ v
325    rw [Xt_zero, mulp_pw_left', mulp_one]
326  | succ i ih =>
327    intro hi v
328    rw [Xt_sq ⟨i, by omega⟩]
329    simp only []
330    rw [mulp_assoc, ih (by omega), ih (by omega), ← pw_add, Nat.pow_succ, Nat.mul_two]
331
332theorem pw_period_one (v : UInt32) : pw (2 ^ 32) v = pw 1 v := by
333  have h := mulp_assoc (Xt 31) (Xt 31) v
334  have h1 : mulp (Xt 31) v = pw (2 ^ 31) v := Xt_pw 31 (by omega) v
335  have h2 : mulp (Xt 31) (pw (2 ^ 31) v) = pw (2 ^ 31) (pw (2 ^ 31) v) := Xt_pw 31 (by omega) _
336  have h3 : mulp (Xt 0) v = pw 1 v := Xt_pw 0 (by omega) v
337  rw [Xt_wrap, h3, h1, h2, ← pw_add] at h
338  rw [show 2 ^ 32 = 2 ^ 31 + 2 ^ 31 by omega]
339  exact h.symm
340
341theorem pw_period (a : Nat) (v : UInt32) : pw (2 ^ 32 * a) v = pw a v := by
342  induction a with
343  | zero => rfl
344  | succ a ih =>
345    rw [Nat.mul_succ, Nat.add_comm, pw_add, ih, pw_period_one, ← pw_add, Nat.add_comm]
346
347theorem Xt_mod (k : Nat) (v : UInt32) : mulp (Xt (k % 32)) v = pw (2 ^ k) v := by
348  induction k using Nat.strongRecOn with
349  | _ k ih =>
350    by_cases hk : k < 32
351    · rw [Nat.mod_eq_of_lt hk]; exact Xt_pw k hk v
352    · obtain ⟨m, rfl⟩ : ∃ m, k = m + 32 := ⟨k - 32, by omega⟩
353      have := ih m (by omega)
354      rw [show (m + 32) % 32 = m % 32 by omega, this, Nat.pow_add, Nat.mul_comm, pw_period]
355
356/-- `StaticsOK h`: the static tables `crc_table` and `x2n_table` of the heap hold the contents `crc32.h` gives them
357(`Zlib.Crc32.initStatics`). -/
358def StaticsOK (h : Heap) : Prop :=
359  h.static.crc_table = Crc32H.crc_table ∧ h.static.x2n_table = Crc32H.x2n_table
360
361/-! ### Bits of 64-bit values -/
362
363theorem lowbit_aux (x : Nat) : ∀ n, x.testBit n = true →
364    ∃ t, x.testBit t = true ∧ ∀ s, s < t → x.testBit s = false := by
365  intro n
366  induction n using Nat.strongRecOn with
367  | _ n ih =>
368    intro hn
369    by_cases h : ∃ s, s < n ∧ x.testBit s = true
370    · obtain ⟨s, hs, hs2⟩ := h
371      exact ih s hs hs2
372    · refine ⟨n, hn, ?_⟩
373      intro s hs
374      cases hb : x.testBit s
375      · rfl
376      · exact absurd ⟨s, hs, hb⟩ h
377
378theorem lowbit_exists (x : Nat) (hx : x ≠ 0) : ∃ t, x.testBit t = true ∧ ∀ s, s < t → x.testBit s = false := by
379  obtain ⟨i, hi⟩ := Nat.exists_testBit_of_ne_zero hx
380  exact lowbit_aux x i hi
381
382theorem mod_pow_zero_iff (x t i : Nat) (ht : x.testBit t = true) (hlow : ∀ s, s < t → x.testBit s = false) :
383    x % 2 ^ i = 0 ↔ i ≤ t := by
384  constructor
385  · intro h
386    apply Classical.byContradiction
387    intro hlt
388    have h1 : (x % 2 ^ i).testBit t = true := by
389      rw [Nat.testBit_mod_two_pow]; simp [ht]; omega
390    rw [h] at h1; simp at h1
391  · intro h
392    apply Nat.eq_of_testBit_eq
393    intro k
394    rw [Nat.testBit_mod_two_pow, Nat.zero_testBit]
395    by_cases hk : k < i
396    · simp [hlow k (by omega)]
397    · simp [hk]
398
399def mm (j : Nat) : UInt64 := UInt64.ofNat (2 ^ (31 - j))
400
401theorem mm_toNat (j : Nat) : (mm j).toNat = 2 ^ (31 - j) := by
402  unfold mm; rw [UInt64.toNat_ofNat']
403  exact Nat.mod_eq_of_lt (Nat.pow_lt_pow_right (by omega) (by omega))
404
405theorem and_pow_ne (n i : Nat) : (n &&& 2 ^ i ≠ 0) ↔ n.testBit i = true := by
406  constructor
407  · intro h
408    apply Classical.byContradiction
409    intro hb
410    apply h
411    apply Nat.eq_of_testBit_eq
412    intro k
413    rw [Nat.testBit_and, Nat.testBit_two_pow, Nat.zero_testBit]
414    by_cases hk : i = k
415    · subst hk; simp at hb; simp [hb]
416    · simp [hk]
417  · intro h h0
418    have := congrArg (fun z => z.testBit i) h0
419    simp [Nat.testBit_and, Nat.testBit_two_pow, h] at this
420
421theorem and_mm_ne (a : UInt64) (j : Nat) (hj : j ≤ 31) :
422    (a &&& mm j != 0) = decide (a.toUInt32.toNat.testBit (31 - j) = true) := by
423  have h1 : (a &&& mm j ≠ 0) ↔ a.toNat.testBit (31 - j) = true := by
424    rw [← and_pow_ne, ← mm_toNat j, ← UInt64.toNat_and]
425    constructor
426    · intro h h0; apply h; apply UInt64.toNat_inj.mp; simpa using h0
427    · intro h h0; apply h; rw [h0]; rfl
428  have h2 : a.toUInt32.toNat.testBit (31 - j) = a.toNat.testBit (31 - j) := by
429    rw [UInt64.toNat_toUInt32, Nat.testBit_mod_two_pow]; simp; omega
430  rw [h2]
431  by_cases h : a.toNat.testBit (31 - j) = true
432  · simp [h, h1.mpr h]
433  · have : ¬ (a &&& mm j ≠ 0) := fun hh => h (h1.mp hh)
434    simp [h]; simpa using this
435
436theorem and_mm_pred_eq (a : UInt64) (j : Nat) (hj : j ≤ 31) :
437    (a &&& (mm j - 1) == 0) = decide (a.toNat % 2 ^ (31 - j) = 0) := by
438  have h1 : (mm j - 1).toNat = 2 ^ (31 - j) - 1 := by
439    rw [UInt64.toNat_sub_of_le, mm_toNat]; rfl
440    rw [UInt64.le_iff_toNat_le, mm_toNat]; simp
441    exact Nat.one_le_two_pow
442  have h2 : (a &&& (mm j - 1)).toNat = a.toNat % 2 ^ (31 - j) := by
443    rw [UInt64.toNat_and, h1, Nat.and_two_pow_sub_one_eq_mod]
444  by_cases h : a.toNat % 2 ^ (31 - j) = 0
445  · have : a &&& (mm j - 1) = 0 := by apply UInt64.toNat_inj.mp; rw [h2, h]; rfl
446    simp [this, h]
447  · have : ¬ a &&& (mm j - 1) = 0 := by
448      intro hh; apply h; rw [← h2, hh]; rfl
449    simp [this, h]
450
451theorem mod_32 (a : UInt64) (i : Nat) (hi : i ≤ 32) : a.toUInt32.toNat % 2 ^ i = a.toNat % 2 ^ i := by
452  rw [UInt64.toNat_toUInt32]
453  exact Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 hi)
454
455theorem mm_shr (j : Nat) (hj : j < 31) : mm j >>> 1 = mm (j + 1) := by
456  apply UInt64.toNat_inj.mp
457  rw [UInt64.toNat_shiftRight, mm_toNat, mm_toNat]
458  have h1 : (1 : UInt64).toNat % 64 = 1 := by decide
459  rw [h1, Nat.shiftRight_eq_div_pow]
460  have : 31 - j = (31 - (j + 1)) + 1 := by omega
461  rw [this, Nat.pow_succ]; simp
462
463theorem POLY_eq : Zlib.Crc32.POLY = crcPoly.toUInt64 := by decide
464
465theorem b_step (v : UInt32) :
466    (if (v.toUInt64 &&& 1 != 0) = true then v.toUInt64 >>> 1 ^^^ Zlib.Crc32.POLY else v.toUInt64 >>> 1)
467      = (crcBit v).toUInt64 := by
468  unfold crcBit
469  have h1 : (v.toUInt64 &&& 1) = (v &&& 1).toUInt64 := (UInt32.toUInt64_and v 1).symm
470  have hs : v.toUInt64 >>> 1 = (v >>> 1).toUInt64 := by rw [UInt32.toUInt64_shiftRight]; rfl
471  rcases and1_cases v with h0 | h0
472  · have hz : (v.toUInt64 &&& 1 != 0) = false := by rw [h1, h0]; decide
473    have hz2 : ¬ (v &&& 1 = 1) := by rw [h0]; decide
474    rw [hz, ite_eq_right hz2, ite_eq_right (by decide), hs]
475  · have hz : (v.toUInt64 &&& 1 != 0) = true := by rw [h1, h0]; decide
476    rw [hz, ite_eq_left h0, ite_eq_left rfl, UInt32.toUInt64_xor, POLY_eq, hs]
477
478/-! ### `multmodp` -/
479
480abbrev MS := UInt64 × UInt64 × UInt64 × Bool
481
482/-- the body of the loop of `multmodp` as a pure function -/
483def mmStep (a : UInt64) (s : MS) : MS :=
484  match s with
485  | (m, p, b, brk) =>
486    if (a &&& m != 0) = true then
487      if (a &&& (m - 1) == 0) = true then (m, p ^^^ b, b, true)
488      else (m >>> 1, p ^^^ b, (if (b &&& 1 != 0) = true then b >>> 1 ^^^ Zlib.Crc32.POLY else b >>> 1), brk)
489    else (m >>> 1, p, (if (b &&& 1 != 0) = true then b >>> 1 ^^^ Zlib.Crc32.POLY else b >>> 1), brk)
490
491theorem mulpAux_stable (a b : UInt32) (t : Nat) (ht : t < 32) (hlow : ∀ s, s < t → a.toNat.testBit s = false) :
492    ∀ n, 31 - t + 1 ≤ n → n ≤ 32 → mulpAux a b n = mulpAux a b (31 - t + 1) := by
493  intro n
494  induction n with
495  | zero => intro h; omega
496  | succ n ih =>
497    intro h1 h2
498    by_cases h : 31 - t + 1 ≤ n
499    · rw [mulpAux, ih h (by omega)]
500      have : bitAt a n = false := by
501        unfold bitAt
502        have := hlow (31 - n) (by omega)
503        simp [this]
504      simp [this]
505    · have : n + 1 = 31 - t + 1 := by omega
506      rw [this]
507
508def Pmm (a32 b32 : UInt32) (J : Nat) : Nat → MS → Prop
509  | 0, s => s.2.2.2 = true ∧ s.2.1 = (mulp a32 b32).toUInt64
510  | k + 1, s => ∃ j, j + k = J ∧ s = (mm j, (mulpAux a32 b32 j).toUInt64, (pw j b32).toUInt64, false)
511
512theorem multmodp_ok (h : Heap) (a b : UInt64) (ha : a.toUInt32 ≠ 0) (hb : b.toNat < 2 ^ 32) :
513    OkOn h (multmodp a b) (mulp a.toUInt32 b.toUInt32).toUInt64 := by
514  have ha' : a.toUInt32.toNat ≠ 0 := fun h0 => ha (UInt32.toNat_inj.mp (by simpa using h0))
515  obtain ⟨t, ht, hlow⟩ := lowbit_exists _ ha'
516  have ht32 : t < 32 := by
517    apply Classical.byContradiction; intro hh
518    have := Nat.testBit_lt_two_pow (x := a.toUInt32.toNat) (i := t)
519      (Nat.lt_of_lt_of_le (UInt32.toNat_lt _) (Nat.pow_le_pow_right (by omega) (by omega)))
520    rw [ht] at this; simp at this
521  have hb64 : b.toUInt32.toUInt64 = b := by
522    apply UInt64.toNat_inj.mp
523    rw [UInt32.toNat_toUInt64, UInt64.toNat_toUInt32, Nat.mod_eq_of_lt hb]
524  generalize hJ : 31 - t = J
525  suffices H : ∃ y, OkOn h (multmodp a b) y ∧ y = (mulp a.toUInt32 b.toUInt32).toUInt64 by
526    obtain ⟨y, hy, rfl⟩ := H; exact hy
527  unfold multmodp
528  refine OkOn.bind_ex (R := fun x : MS => x.2.1 = (mulp a.toUInt32 b.toUInt32).toUInt64) ?_ ?_
529  · refine cwhile_ok (Pmm a.toUInt32 b.toUInt32 J) (fun x : MS => x.2.1 = (mulp a.toUInt32 b.toUInt32).toUInt64)
530      ?_ ?_ (k := J + 1) (s := ((1 : UInt64) <<< 31, 0, b, false)) ?_ ?_
531    · intro k s hP
532      obtain ⟨j, hjk, rfl⟩ := hP
533      have hj31 : j ≤ 31 := by omega
534      have e1 : (a &&& mm j != 0) = bitAt a.toUInt32 j := by
535        rw [and_mm_ne a j hj31]; unfold bitAt; simp [show j < 32 by omega]
536      have e2 : (a &&& (mm j - 1) == 0) = decide (31 - j ≤ t) := by
537        rw [and_mm_pred_eq a j hj31, ← mod_32 a (31 - j) (by omega)]
538        simp only [mod_pow_zero_iff _ t _ ht hlow]
539      refine ⟨(mm j, (mulpAux a.toUInt32 b.toUInt32 j).toUInt64, (pw j b.toUInt32).toUInt64, false),
540        mmStep a (mm j, (mulpAux a.toUInt32 b.toUInt32 j).toUInt64, (pw j b.toUInt32).toUInt64, false), rfl, ?_, ?_⟩
541      · by_cases c1 : (a &&& mm j != 0) = true <;> by_cases c2 : (a &&& mm j - 1 == 0) = true <;>
542          simp [mmStep, c1, c2, OkOn]
543      simp only [mmStep, e1, e2]
544      cases k with
545      | zero =>
546        have hj : j = J := by omega
547        have hbit : bitAt a.toUInt32 j = true := by
548          unfold bitAt; rw [show 31 - j = t by omega, ht]; simp [show j < 32 by omega]
549        have hst : decide (31 - j ≤ t) = true := by simp; omega
550        rw [ite_eq_left hbit, ite_eq_left hst]
551        refine ⟨rfl, ?_⟩
552        have : mulpAux a.toUInt32 b.toUInt32 (j + 1) = mulpAux a.toUInt32 b.toUInt32 j ^^^ pw j b.toUInt32 := by
553          simp [mulpAux, hbit]
554        have hst2 := mulpAux_stable a.toUInt32 b.toUInt32 t ht32 hlow 32 (by omega) (by omega)
555        show _ = (mulpAux a.toUInt32 b.toUInt32 32).toUInt64
556        rw [hst2, show 31 - t + 1 = j + 1 by omega, this, UInt32.toUInt64_xor]
557      | succ k =>
558        have hst : decide (31 - j ≤ t) = false := by simp; omega
559        have hst' : ¬ (decide (31 - j ≤ t) = true) := by rw [hst]; decide
560        refine ⟨j + 1, by omega, ?_⟩
561        have hb' := b_step (pw j b.toUInt32)
562        rw [← pw_succ'] at hb'
563        have hm : mm j >>> 1 = mm (j + 1) := mm_shr j (by omega)
564        cases hbit : bitAt a.toUInt32 j
565        · rw [ite_eq_right (by simp [hbit]), hm, hb']; simp [mulpAux, hbit]
566        · rw [ite_eq_left (by simp [hbit]), ite_eq_right hst', hm, hb']; simp [mulpAux, hbit, UInt32.toUInt64_xor]
567    · intro s hP
568      obtain ⟨m, p, bb, brk⟩ := s
569      obtain ⟨h1, h2⟩ := hP
570      simp only at h1 h2
571      subst h1
572      exact ⟨_, rfl, h2⟩
573    · refine ⟨0, by omega, ?_⟩
574      simp only [mulpAux, pw]
575      rw [hb64]; rfl
576    · show J + 1 < 2 ^ 64
577      omega
578  · intro x hx
579    obtain ⟨m, p, bb, brk⟩ := x
580    exact ⟨p, rfl, hx⟩
581
582theorem int64_shr (nn : Nat) (h : nn < 2 ^ 63) : (Int64.ofNat nn) >>> 1 = Int64.ofNat (nn / 2) := by
583  apply Int64.toBitVec_inj.mp
584  rw [Int64.toBitVec_shiftRight]
585  simp [Int64.toBitVec_ofNat']
586  rw [BitVec.sshiftRight_eq_of_msb_false]
587  · apply BitVec.eq_of_toNat_eq
588    rw [BitVec.toNat_ushiftRight, BitVec.toNat_ofNat, BitVec.toNat_ofNat,
589      Nat.mod_eq_of_lt (by omega : nn < 2 ^ 64), Nat.mod_eq_of_lt (by omega : nn / 2 < 2 ^ 64),
590      Nat.shiftRight_eq_div_pow]
591  · rw [BitVec.msb_eq_false_iff_two_mul_lt, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega : nn < 2 ^ 64)]
592    omega
593
594
595theorem int64_and1 (nn : Nat) (h : nn < 2 ^ 63) : ((Int64.ofNat nn) &&& 1 != 0) = decide (nn % 2 = 1) := by
596  have h1 : ((Int64.ofNat nn) &&& 1).toBitVec.toNat = nn % 2 := by
597    rw [Int64.toBitVec_and, BitVec.toNat_and, Int64.toBitVec_ofNat', BitVec.toNat_ofNat,
598      Nat.mod_eq_of_lt (by omega : nn < 2 ^ 64)]
599    have : (Int64.toBitVec 1).toNat = 1 := by decide
600    rw [this, Nat.and_one_is_mod]
601  by_cases h2 : nn % 2 = 1
602  · have : ((Int64.ofNat nn) &&& 1) ≠ 0 := by
603      intro h0
604      rw [h0] at h1
605      have : (Int64.toBitVec 0).toNat = 0 := by decide
606      omega
607    simp [this, h2]
608  · have : ((Int64.ofNat nn) &&& 1) = 0 := by
609      apply Int64.toBitVec_inj.mp
610      apply BitVec.eq_of_toNat_eq
611      rw [h1]; have : (Int64.toBitVec 0).toNat = 0 := by decide
612      rw [this]; omega
613    simp [this, h2]
614
615theorem int64_ne0 (nn : Nat) (h : nn < 2 ^ 63) : ((Int64.ofNat nn) != 0) = decide (nn ≠ 0) := by
616  by_cases h2 : nn = 0
617  · subst h2; decide
618  · have : Int64.ofNat nn ≠ 0 := by
619      intro h0
620      have := congrArg (fun x => x.toBitVec.toNat) h0
621      simp only [Int64.toBitVec_ofNat', BitVec.toNat_ofNat] at this
622      have h3 : (Int64.toBitVec 0).toNat = 0 := by decide
623      rw [h3, Nat.mod_eq_of_lt (by omega : nn < 2 ^ 64)] at this
624      exact h2 this
625    simp [this, h2]
626
627/-! ### `x2nmodp` -/
628
629/-- the number of loop iterations of `x2nmodp` for `n`: its bit length -/
630def bl (n : Nat) : Nat := if n = 0 then 0 else bl (n / 2) + 1
631termination_by n
632decreasing_by omega
633
634theorem bl_zero : bl 0 = 0 := by rw [bl]; simp
635theorem bl_pos (n : Nat) (h : n ≠ 0) : bl n = bl (n / 2) + 1 := by rw [bl]; simp [h]
636
637theorem bl_div (n i : Nat) : bl (n / 2 ^ i / 2) = bl (n / 2 ^ (i + 1)) := by
638  rw [Nat.pow_succ, Nat.div_div_eq_div_mul]
639
640theorem bl_le (n : Nat) : bl n ≤ n := by
641  induction n using Nat.strongRecOn with
642  | _ n ih =>
643    by_cases h : n = 0
644    · subst h; rw [bl_zero]; exact Nat.le_refl _
645    · rw [bl_pos n h]
646      have := ih (n / 2) (by omega)
647      omega
648
649theorem lt_pow_bl (n : Nat) : n < 2 ^ bl n := by
650  induction n using Nat.strongRecOn with
651  | _ n ih =>
652    by_cases h : n = 0
653    · subst h; rw [bl_zero]; simp
654    · rw [bl_pos n h, Nat.pow_succ]
655      have := ih (n / 2) (by omega)
656      omega
657
658
659theorem u32_roundtrip (x : UInt32) : x.toUInt64.toUInt32 = x := by
660  apply UInt32.toNat_inj.mp
661  rw [UInt64.toNat_toUInt32, UInt32.toNat_toUInt64, Nat.mod_eq_of_lt (UInt32.toNat_lt _)]
662
663theorem x2nTab_ok (h : Heap) (hs : StaticsOK h) (i : UInt32) (hi : i.toNat < 32) :
664    OkOn h (x2nTab i) (Xt i.toNat) := by
665  unfold x2nTab
666  have hg : Space.get h URef.st_x2n_table = some Crc32H.x2n_table := by rw [URef.get_st_x2n_table, hs.2]
667  have hlt : 0 + i.toNat < Crc32H.x2n_table.size := by rw [x2n_size]; omega
668  have := Ptr.index_ok (r := URef.st_x2n_table) (off := 0) (i := i.toNat) hg hlt
669  have e : Xt i.toNat = Crc32H.x2n_table[0 + i.toNat] := by
670    simp only [Xt, Nat.zero_add]; exact getElem!_pos _ _ (by omega)
671  rw [e]; exact this
672
673theorem crcTab_ok (h : Heap) (hs : StaticsOK h) (i : UInt64) (hi : i.toNat < 256) :
674    OkOn h (crcTab i) Crc32H.crc_table[i.toNat]! := by
675  unfold crcTab
676  have hg : Space.get h URef.st_crc_table = some Crc32H.crc_table := by rw [URef.get_st_crc_table, hs.1]
677  have hlt : 0 + i.toNat < Crc32H.crc_table.size := by rw [crc_table_size]; omega
678  have := Ptr.index_ok (r := URef.st_crc_table) (off := 0) (i := i.toNat) hg hlt
679  have e : Crc32H.crc_table[i.toNat]! = Crc32H.crc_table[0 + i.toNat] := by
680    simp only [Nat.zero_add]; exact getElem!_pos _ _ (by omega)
681  rw [e]; exact this
682
683theorem and31 (x : UInt32) : (x &&& 31).toNat = x.toNat % 32 := by
684  rw [UInt32.toNat_and]
685  exact Nat.and_two_pow_sub_one_eq_mod x.toNat 5
686
687def Px (n0 k0 : Nat) (cnt : Nat) (s : UInt64 × Int64 × UInt32) : Prop :=
688  ∃ i, cnt = bl (n0 / 2 ^ i) ∧ s.1.toNat < 2 ^ 32 ∧ s.2.1 = Int64.ofNat (n0 / 2 ^ i) ∧
689    s.2.2 = UInt32.ofNat (k0 + i) ∧ ∀ v, mulp s.1.toUInt32 v = pw ((n0 % 2 ^ i) * 2 ^ k0) v
690
691theorem int64_nat_lt (n : Int64) (hn : 0 ≤ n.toInt) : n.toInt.toNat < 2 ^ 63 := by
692  have h1 : n.toInt < 2 ^ 63 := by
693    have := Int64.toInt_lt n  
694    omega
695  omega
696
697theorem x2nmodp_ok (h : Heap) (hs : StaticsOK h) (n : Int64) (hn : 0 ≤ n.toInt) (k : UInt32) :
698    ∃ p, OkOn h (x2nmodp n k) p ∧ p.toNat < 2 ^ 32 ∧
699      ∀ v, mulp p.toUInt32 v = pw (n.toInt.toNat * 2 ^ k.toNat) v := by
700  have hn63 := int64_nat_lt n hn
701  generalize hn0 : n.toInt.toNat = n0 at hn63 ⊢
702  have hnn : n = Int64.ofNat n0 := by
703    rw [← hn0]
704    have := Int64.ofNat_toNatClampNeg n (by simpa [Int64.le_iff_toInt_le] using hn)
705    simpa using this.symm
706  generalize hk0 : k.toNat = k0
707  have hkk : k = UInt32.ofNat k0 := by rw [← hk0]; simp
708  subst hnn hkk
709  suffices H : ∃ y, OkOn h (x2nmodp (Int64.ofNat n0) (UInt32.ofNat k0)) y ∧
710      (y.toNat < 2 ^ 32 ∧ ∀ v, mulp y.toUInt32 v = pw (n0 * 2 ^ k0) v) by
711    obtain ⟨y, hy, h2⟩ := H; exact ⟨y, hy, h2⟩
712  unfold x2nmodp
713  refine OkOn.bind_ex (R := fun x : UInt64 × Int64 × UInt32 =>
714    x.1.toNat < 2 ^ 32 ∧ ∀ v, mulp x.1.toUInt32 v = pw (n0 * 2 ^ k0) v) ?_ ?_
715  · refine cwhile_ok (Px n0 k0) _ ?_ ?_ (k := bl n0) (s := ((1 : UInt64) <<< 31, Int64.ofNat n0, UInt32.ofNat k0)) ?_ ?_
716    · intro cnt s hP
717      obtain ⟨p, n, kk⟩ := s
718      obtain ⟨i, hcnt, hp32, hn', hk', hm⟩ := hP
719      simp only at hp32 hn' hk' hm
720      subst hn' hk'
721      have hne : n0 / 2 ^ i ≠ 0 := by
722        intro h0; rw [h0, bl_zero] at hcnt; omega
723      have hlt63 : n0 / 2 ^ i < 2 ^ 63 := Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hn63
724      have hc : OkOn h (pure ((Int64.ofNat (n0 / 2 ^ i) != 0), p, Int64.ofNat (n0 / 2 ^ i), UInt32.ofNat (k0 + i)) :
725          M (Bool × UInt64 × Int64 × UInt32)) (true, p, Int64.ofNat (n0 / 2 ^ i), UInt32.ofNat (k0 + i)) := by
726        rw [int64_ne0 _ hlt63]; simp [hne]; exact OkOn.pure _ _
727      have hbit : (Int64.ofNat (n0 / 2 ^ i) &&& 1 != 0) = decide ((n0 / 2 ^ i) % 2 = 1) := int64_and1 _ hlt63
728      have hnext : Int64.ofNat (n0 / 2 ^ i) >>> 1 = Int64.ofNat (n0 / 2 ^ (i + 1)) := by
729        rw [int64_shr _ hlt63, Nat.pow_succ, Nat.div_div_eq_div_mul]
730      have hknext : UInt32.ofNat (k0 + i) + 1 = UInt32.ofNat (k0 + (i + 1)) := by
731        apply UInt32.toNat_inj.mp
732        simp [UInt32.toNat_add, UInt32.toNat_ofNat']
733        omega
734      have hcnt' : cnt = bl (n0 / 2 ^ (i + 1)) := by
735        rw [bl_pos _ hne, bl_div] at hcnt; omega
736      have hkt : (UInt32.ofNat (k0 + i) &&& 31).toNat = (k0 + i) % 32 := by
737        rw [and31, UInt32.toNat_ofNat']
738        exact Nat.mod_mod_of_dvd _ (by decide : 32 ∣ 2 ^ 32)
739      by_cases hb : (n0 / 2 ^ i) % 2 = 1
740      · have hX := x2nTab_ok h hs (UInt32.ofNat (k0 + i) &&& 31) (by rw [hkt]; omega)
741        rw [hkt] at hX
742        have hXne : (Xt ((k0 + i) % 32)).toUInt64.toUInt32 ≠ 0 := by
743          have : (Xt ((k0 + i) % 32)).toUInt64.toUInt32 = Xt ((k0 + i) % 32) := by
744            apply UInt32.toNat_inj.mp
745            rw [UInt64.toNat_toUInt32, UInt32.toNat_toUInt64, Nat.mod_eq_of_lt (UInt32.toNat_lt _)]
746          rw [this]; exact Xt_ne ⟨(k0 + i) % 32, by omega⟩
747        have hM := multmodp_ok h (Xt ((k0 + i) % 32)).toUInt64 p hXne (by omega)
748        refine ⟨(p, Int64.ofNat (n0 / 2 ^ i), UInt32.ofNat (k0 + i)),
749          ((mulp (Xt ((k0 + i) % 32)).toUInt64.toUInt32 p.toUInt32).toUInt64,
750          Int64.ofNat (n0 / 2 ^ (i + 1)), UInt32.ofNat (k0 + (i + 1))), hc, ?_, ?_⟩
751        · simp only [hbit, hb, decide_true, ite_true]
752          exact OkOn.bind hX (OkOn.bind hM (by rw [hnext, hknext]; exact OkOn.pure _ _))
753        · refine ⟨i + 1, hcnt', ?_, rfl, rfl, ?_⟩
754          · simp only [UInt32.toNat_toUInt64]; exact UInt32.toNat_lt _
755          · intro v
756            rw [u32_roundtrip, u32_roundtrip, mulp_assoc, Xt_mod, hm v, ← pw_add]
757            rw [Nat.mod_pow_succ, hb]
758            congr 1
759            rw [Nat.mul_one, Nat.add_mul, Nat.pow_add, Nat.mul_comm (2 ^ k0)]
760            omega
761      · have hb' : ¬ (n0 / 2 ^ i % 2 = 1) := hb
762        refine ⟨(p, Int64.ofNat (n0 / 2 ^ i), UInt32.ofNat (k0 + i)),
763          (p, Int64.ofNat (n0 / 2 ^ (i + 1)), UInt32.ofNat (k0 + (i + 1))), hc, ?_, ?_⟩
764        · simp only [hbit, hb', decide_false]
765          rw [ite_eq_right (by decide)]
766          rw [hnext, hknext]; exact OkOn.pure _ _
767        · refine ⟨i + 1, hcnt', hp32, rfl, rfl, ?_⟩
768          intro v
769          rw [hm v]
770          congr 1
771          rw [Nat.mod_pow_succ]
772          have : n0 / 2 ^ i % 2 = 0 := by omega
773          rw [this]; simp
774    · intro s hP
775      obtain ⟨p, n, kk⟩ := s
776      obtain ⟨i, hcnt, hp32, hn', hk', hm⟩ := hP
777      simp only at hp32 hn' hk' hm
778      subst hn' hk'
779      have h0 : n0 / 2 ^ i = 0 := by
780        apply Classical.byContradiction; intro hne
781        rw [bl_pos _ hne] at hcnt; omega
782      have hlt63 : n0 / 2 ^ i < 2 ^ 63 := Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hn63
783      refine ⟨(p, Int64.ofNat (n0 / 2 ^ i), UInt32.ofNat (k0 + i)), ?_, hp32, ?_⟩
784      · show OkOn h (pure _) _
785        rw [int64_ne0 _ hlt63]; simp [h0]; exact OkOn.pure _ _
786      · have hmod : n0 % 2 ^ i = n0 := Nat.mod_eq_of_lt (by
787          rcases Nat.div_eq_zero_iff.mp h0 with h1 | h1
788          · have := Nat.two_pow_pos i; omega
789          · exact h1)
790        intro v; rw [hm v, hmod]
791    · refine ⟨0, by simp, by show ((1 : UInt64) <<< 31).toNat < 2 ^ 32; decide, by simp, by simp, ?_⟩
792      intro v
793      have : ((1 : UInt64) <<< 31).toUInt32 = e 31 := by decide
794      simp only [this, Nat.pow_zero, Nat.mod_one, Nat.zero_mul]
795      exact mulp_one v
796    · show bl n0 < 2 ^ 64
797      have := bl_le n0
798      have : 2 ^ 63 < 2 ^ 64 := by decide
799      omega
800  · intro x hx
801    obtain ⟨p, n, kk⟩ := x
802    exact ⟨p, rfl, hx⟩
803
804/-! ### `crcBit` is injective, so a power of `x` times a nonzero register is nonzero -/
805
806theorem crcBit_eq_zero (c : UInt32) (h : crcBit c = 0) : c = 0 := by
807  have e1 : (1 : UInt32).toNat = 1 := rfl
808  have e0 : (0 : UInt32).toNat = 0 := rfl
809  have hb : c &&& 1 = 0 := by
810    apply Classical.byContradiction; intro hne
811    rcases and1_cases c with h0 | h0
812    · exact hne h0
813    · unfold ZlibF.Spec.crcBit at h
814      rw [ite_eq_left h0] at h
815      have h1 := congrArg (fun x => x.toNat.testBit 31) h
816      simp only [UInt32.toNat_xor, Nat.testBit_xor, UInt32.toNat_shiftRight, e1, e0] at h1
817      have h2 : (c.toNat >>> (1 % 32)).testBit 31 = false := by
818        rw [Nat.testBit_shiftRight]
819        exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le (UInt32.toNat_lt c) (by decide))
820      have h3 : crcPoly.toNat.testBit 31 = true := by decide
821      rw [h2, h3] at h1
822      simp at h1
823  unfold ZlibF.Spec.crcBit at h
824  rw [ite_eq_right (by rw [hb]; decide)] at h
825  have h1 : c.toNat >>> 1 = 0 := by
826    have := congrArg UInt32.toNat h
827    rw [UInt32.toNat_shiftRight, e1, e0] at this
828    simpa using this
829  have h2 : c.toNat < 2 := by
830    rw [Nat.shiftRight_eq_div_pow] at h1
831    have := Nat.div_eq_zero_iff.mp h1
832    omega
833  have h3 : (c &&& 1).toNat = 0 := by rw [hb]; rfl
834  rw [UInt32.toNat_and, e1, Nat.and_one_is_mod] at h3
835  apply UInt32.toNat_inj.mp
836  rw [e0]; omega
837
838theorem pw_eq_zero (m : Nat) (c : UInt32) (h : pw m c = 0) : c = 0 := by
839  induction m generalizing c with
840  | zero => exact h
841  | succ m ih => exact crcBit_eq_zero c (ih _ (by rw [← pw_succ]; exact h))
842
843theorem e_ne_zero (s : Nat) (hs : s < 32) : e s ≠ 0 := by
844  intro h
845  have := congrArg (fun x => x.toNat) h
846  simp only [e, UInt32.toNat_ofNat'] at this
847  rw [Nat.mod_eq_of_lt (Nat.pow_lt_pow_right (by omega) hs)] at this
848  have h0 : (0 : UInt32).toNat = 0 := rfl
849  rw [h0] at this
850  exact absurd this (Nat.pos_iff_ne_zero.mp (Nat.two_pow_pos s))
851
852
853/-! ### The specification side: the CRC register is affine in its start value -/
854
855/-- the register after processing `l` from the start value `c` -/
856def rbl (c : UInt32) (l : List UInt8) : UInt32 := l.foldl ZlibF.Spec.crcByte c
857
858theorem rbl_nil (c : UInt32) : rbl c [] = c := rfl
859theorem rbl_cons (c : UInt32) (b : UInt8) (l : List UInt8) : rbl c (b :: l) = rbl (ZlibF.Spec.crcByte c b) l := rfl
860
861theorem rbl_affine (l : List UInt8) : ∀ c : UInt32, rbl c l = pw (8 * l.length) c ^^^ rbl 0 l := by
862  induction l with
863  | nil => intro c; simp [rbl_nil, pw]
864  | cons b l ih =>
865    intro c
866    rw [rbl_cons, rbl_cons, ih, ih (ZlibF.Spec.crcByte 0 b)]
867    simp only [crcByte_eq, UInt32.zero_xor, pw_xor, List.length_cons]
868    rw [show 8 * (l.length + 1) = 8 * l.length + 8 by omega, pw_add]
869    ac_rfl
870
871theorem not32_eq (x : UInt32) : ~~~ x = x ^^^ 0xffffffff := by
872  apply UInt32.eq_of_toBitVec_eq
873  have : (0xffffffff : UInt32).toBitVec = BitVec.allOnes 32 := by decide
874  rw [UInt32.toBitVec_xor, this, BitVec.xor_allOnes]
875  rfl
876
877theorem crc32Update_affine (c : UInt32) (l : List UInt8) :
878    ZlibF.Spec.crc32Update c l = pw (8 * l.length) c ^^^ ZlibF.Spec.crc32 l := by
879  unfold ZlibF.Spec.crc32 ZlibF.Spec.crc32Update
880  change ~~~ rbl (~~~ c) l = pw (8 * l.length) c ^^^ ~~~ rbl (~~~ 0) l
881  rw [rbl_affine l (~~~ c), rbl_affine l (~~~ 0), not32_eq, not32_eq c, not32_eq 0, not32_eq]
882  simp only [pw_xor]
883  rw [pw_zero, UInt32.zero_xor]
884  ac_rfl
885
886/-- `op` is the operator for `n` bytes: a 32-bit value with a bit set among the low 32 (so `multmodp` terminates
887on it) that multiplies a CRC register by `x^(8n)` (the advance over `n` zero bytes). -/
888def IsOp (op : UInt64) (n : Nat) : Prop :=
889  op.toNat < 2 ^ 32 ∧ op.toUInt32 ≠ 0 ∧ ∀ v, mulp op.toUInt32 v = pw (8 * n) v
890
891theorem and_ffffffff (x : UInt64) : x &&& 0xffffffff = x.toUInt32.toUInt64 := by
892  apply UInt64.toNat_inj.mp
893  rw [UInt64.toNat_and, UInt32.toNat_toUInt64, UInt64.toNat_toUInt32]
894  have : (0xffffffff : UInt64).toNat = 2 ^ 32 - 1 := by decide
895  rw [this, Nat.and_two_pow_sub_one_eq_mod]
896
897theorem gen64_neg (h : Heap) (len2 : Int64) (hneg : len2.toInt < 0) :
898    OkOn h (crc32_combine_gen64 len2) 0 := by
899  unfold crc32_combine_gen64
900  have : len2 < 0 := by rw [Int64.lt_iff_toInt_lt]; simpa using hneg
901  rw [ite_eq_left this]; exact OkOn.pure _ _
902
903theorem gen64_op (h : Heap) (hs : StaticsOK h) (len2 : Int64) (hpos : 0 ≤ len2.toInt) :
904    ∃ op, OkOn h (crc32_combine_gen64 len2) op ∧ IsOp op len2.toInt.toNat := by
905  obtain ⟨p, hp, hp32, hpv⟩ := x2nmodp_ok h hs len2 hpos 3
906  have hlt : ¬ (len2 < 0) := by rw [Int64.lt_iff_toInt_lt]; simpa using hpos
907  have h3 : (3 : UInt32).toNat = 3 := rfl
908  have hpv' : ∀ v, mulp p.toUInt32 v = pw (8 * len2.toInt.toNat) v := by
909    intro v; rw [hpv v, h3, Nat.mul_comm]
910  refine ⟨p, ?_, hp32, ?_, hpv'⟩
911  · unfold crc32_combine_gen64; rw [ite_eq_right hlt]; exact hp
912  · intro h0
913    have := hpv' (e 31)
914    rw [h0, mulp_zero_left] at this
915    exact e_ne_zero 31 (by omega) (pw_eq_zero _ _ this.symm)
916
917theorem combine_op_ok (h : Heap) (crc1 crc2 op : UInt64) (hop : op.toUInt32 ≠ 0) :
918    OkOn h (crc32_combine_op crc1 crc2 op) (mulp op.toUInt32 crc1.toUInt32 ^^^ crc2.toUInt32).toUInt64 := by
919  have hne : ¬ (op == 0) = true := by
920    intro hh
921    have : op = 0 := by simpa using hh
922    exact hop (by rw [this]; rfl)
923  have hb : (crc1 &&& 0xffffffff).toNat < 2 ^ 32 := by
924    rw [and_ffffffff, UInt32.toNat_toUInt64]; exact UInt32.toNat_lt _
925  have hm := multmodp_ok h op (crc1 &&& 0xffffffff) hop hb
926  rw [and_ffffffff] at hm
927  rw [u32_roundtrip] at hm
928  unfold crc32_combine_op
929  rw [ite_eq_right hne, and_ffffffff crc1, and_ffffffff crc2, UInt32.toUInt64_xor]
930  exact OkOn.bind hm (OkOn.pure _ _)
931
932theorem combine64_ok (h : Heap) (hs : StaticsOK h) (crc1 crc2 : UInt64) (len2 : Int64) :
933    OkOn h (crc32_combine64 crc1 crc2 len2)
934      (if len2.toInt < 0 then 0 else (pw (8 * len2.toInt.toNat) crc1.toUInt32 ^^^ crc2.toUInt32).toUInt64) := by
935  unfold crc32_combine64
936  by_cases hneg : len2.toInt < 0
937  · rw [ite_eq_left hneg]
938    refine OkOn.bind (gen64_neg h len2 hneg) ?_
939    unfold crc32_combine_op
940    rw [ite_eq_left (by decide)]; exact OkOn.pure _ _
941  · rw [ite_eq_right hneg]
942    obtain ⟨op, hop, hnz, hlt, hv⟩ := gen64_op h hs len2 (by omega)
943    refine OkOn.bind hop ?_
944    have := combine_op_ok h crc1 crc2 op hlt
945    rw [hv] at this
946    exact this
947
948
949/-! ### `multmodp` does not terminate when the low 32 bits of `a` are zero -/
950
951theorem go_diverges {σ : Type} (cond : σ → M (Bool × σ)) (body : σ → M σ) (Inv : σ → Prop)
952    (hstep : ∀ s, Inv s → ∀ h, cond s h = .ok ((true, s), h) ∧ ∃ s2, body s h = .ok (s2, h) ∧ Inv s2) :
953    ∀ n s h, Inv s → cwhile.go cond body n s h = .error .outOfFuel := by
954  intro n
955  induction n with
956  | zero => intro s h _; simp [cwhile.go]
957  | succ n ih =>
958    intro s h hI
959    obtain ⟨hc, s2, hb, hI2⟩ := hstep s hI h
960    simp [cwhile.go, hc, hb, ih s2 h hI2]
961
962theorem and_low_zero (a m : UInt64) (ha : a.toUInt32 = 0) (hm : m.toNat < 2 ^ 32) : a &&& m = 0 := by
963  apply UInt64.toNat_inj.mp
964  rw [UInt64.toNat_and]
965  have e0 : (0 : UInt64).toNat = 0 := rfl
966  rw [e0]
967  apply Nat.eq_of_testBit_eq
968  intro k
969  rw [Nat.testBit_and, Nat.zero_testBit]
970  by_cases hk : k < 32
971  · have h0 : a.toNat % 2 ^ 32 = 0 := by
972      have := congrArg UInt32.toNat ha
973      rwa [UInt64.toNat_toUInt32] at this
974    have : a.toNat.testBit k = false := by
975      have h1 := Nat.testBit_mod_two_pow a.toNat 32 k
976      rw [h0, Nat.zero_testBit] at h1
977      simpa [hk] using h1.symm
978    simp [this]
979  · have : m.toNat.testBit k = false :=
980      Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hm (Nat.pow_le_pow_right (by omega) (by omega)))
981    simp [this]
982
983/-- **multmodp, non-termination.** If the low 32 bits of `a` are zero, the loop of `multmodp` never finds a set bit
984(`a & m` is 0 for every `m <= 2^31`, `m` then becomes 0): the translation runs out of fuel for every `b` and every heap.
985The real C (zlib `develop`) hangs on `crc32_combine_op(1, 2, 1UL << 32)`. -/
986theorem multmodp_diverges (a b : UInt64) (ha : a.toUInt32 = 0) (h : Heap) :
987    multmodp a b h = .error .outOfFuel := by
988  unfold multmodp
989  rw [bind_app]
990  have key : cwhile (fun x : MS => match x with | (m, p, b, brk) => pure (!brk, m, p, b, brk))
991      (fun x : MS => match x with
992        | (m, p, b, brk) =>
993          have p := p;
994          have __do_jp := fun __r p =>
995            have m := m >>> 1;
996            have b := if (b &&& 1 != 0) = true then b >>> 1 ^^^ POLY else b >>> 1;
997            pure (m, p, b, brk);
998          if (a &&& m != 0) = true then
999            have p := p ^^^ b;
1000            if (a &&& m - 1 == 0) = true then pure (m, p, b, true) else __do_jp () p
1001          else __do_jp () p)
1002      ((1 : UInt64) <<< 31, 0, b, false) h = .error .outOfFuel := by
1003    refine go_diverges _ _ (fun s : MS => s.2.2.2 = false ∧ s.1.toNat < 2 ^ 32) ?_ fuel _ h ⟨rfl, ?_⟩
1004    · intro s hI h
1005      obtain ⟨m, p, bb, brk⟩ := s
1006      obtain ⟨h1, h2⟩ := hI
1007      simp only at h1 h2
1008      subst h1
1009      have hz : (a &&& m != 0) = false := by rw [and_low_zero a m ha h2]; rfl
1010      refine ⟨rfl, (m >>> 1, p, (if (bb &&& 1 != 0) = true then bb >>> 1 ^^^ POLY else bb >>> 1), false), ?_, ?_⟩
1011      · simp [hz]
1012      · refine ⟨rfl, ?_⟩
1013        show (m >>> 1).toNat < 2 ^ 32
1014        rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
1015        exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h2
1016    · show ((1 : UInt64) <<< 31).toNat < 2 ^ 32
1017      decide
1018  rw [key]
1019
1020theorem combine_op_diverges (h : Heap) (crc1 crc2 op : UInt64) (hop : op ≠ 0) (hlow : op.toUInt32 = 0) :
1021    crc32_combine_op crc1 crc2 op h = .error .outOfFuel := by
1022  unfold crc32_combine_op
1023  have hne : ¬ (op == 0) = true := by simpa using hop
1024  rw [ite_eq_right hne, bind_app, multmodp_diverges _ _ hlow]
1025
1026/-! ### Linear maps on 64-bit words -/
1027
1028def Lin64 (f : UInt64 → UInt32) : Prop := ∀ x y, f (x ^^^ y) = f x ^^^ f y
1029
1030theorem lin64_ext {f g : UInt64 → UInt32} (hf : Lin64 f) (hg : Lin64 g)
1031    (hb : ∀ t, t < 64 → f (UInt64.ofNat (2 ^ t)) = g (UInt64.ofNat (2 ^ t))) : ∀ x, f x = g x := by
1032  intro x
1033  have hf' : ∀ x y, f (x ^^^ y) = f x ^^^ f y := hf
1034  have hg' : ∀ x y, g (x ^^^ y) = g x ^^^ g y := hg
1035  have key := lin_ext_nat 64 (fun n => (f (UInt64.ofNat n)).toNat) (fun n => (g (UInt64.ofNat n)).toNat)
1036    (by intro a b; simp only [UInt64.ofNat_xor, hf', UInt32.toNat_xor])
1037    (by intro a b; simp only [UInt64.ofNat_xor, hg', UInt32.toNat_xor])
1038    (by intro t ht; rw [hb t ht]) 64 (Nat.le_refl _) x.toNat (by simpa using UInt64.toNat_lt x)
1039  simp only [UInt64.ofNat_toNat] at key
1040  exact UInt32.toNat_inj.mp key
1041
1042/-! ### The word recurrence of `crc_word` -/
1043
1044/-- one step of the loop of `crc_word` -/
1045def wstep (d : UInt64) : UInt64 := (d >>> 8) ^^^ (Crc32H.crc_table[(d &&& 0xff).toNat]!).toUInt64
1046
1047def wsteps : Nat → UInt64 → UInt64
1048  | 0, d => d
1049  | n + 1, d => wstep (wsteps n d)
1050
1051theorem toUInt32_ofNat_eq (x : UInt64) (h : x.toNat < 256) : UInt32.ofNat x.toNat = x.toUInt32 := by
1052  apply UInt32.toNat_inj.mp
1053  rw [UInt32.toNat_ofNat', UInt64.toNat_toUInt32]
1054
1055theorem and255_lt (d : UInt64) : (d &&& 0xff).toNat < 256 := by
1056  rw [UInt64.toNat_and]
1057  have : (0xff : UInt64).toNat = 2 ^ 8 - 1 := by decide
1058  rw [this, Nat.and_two_pow_sub_one_eq_mod]
1059  exact Nat.mod_lt _ (by decide)
1060
1061theorem tab_lookup (d : UInt64) : Crc32H.crc_table[(d &&& 0xff).toNat]! = pw 8 (d &&& 0xff).toUInt32 := by
1062  have := crc_table_eq ⟨(d &&& 0xff).toNat, and255_lt d⟩
1063  simp only at this
1064  rw [this, toUInt32_ofNat_eq _ (and255_lt d)]
1065
1066theorem wstep_xor (a b : UInt64) : wstep (a ^^^ b) = wstep a ^^^ wstep b := by
1067  unfold wstep
1068  rw [UInt64.shiftRight_xor, tab_lookup, tab_lookup, tab_lookup, and_xor64, UInt64.toUInt32_xor, pw_xor,
1069    UInt32.toUInt64_xor]
1070  ac_rfl
1071
1072theorem wsteps_xor (n : Nat) (a b : UInt64) : wsteps n (a ^^^ b) = wsteps n a ^^^ wsteps n b := by
1073  induction n generalizing a b with
1074  | zero => rfl
1075  | succ n ih => simp only [wsteps, ih, wstep_xor]
1076
1077/-- the byte `j` of `d`, as a register value -/
1078def bx (d : UInt64) (j : Nat) : UInt32 := ((d >>> (8 * j).toUInt64) &&& 0xff).toUInt32
1079
1080theorem bx_xor (a b : UInt64) (j : Nat) : bx (a ^^^ b) j = bx a j ^^^ bx b j := by
1081  unfold bx
1082  rw [UInt64.shiftRight_xor, and_xor64, UInt64.toUInt32_xor]
1083
1084/-- the closed form of `crc_word`: byte `j` advanced over `8 - j` bytes -/
1085def psiW (d : UInt64) : Nat → UInt32
1086  | 0 => 0
1087  | m + 1 => psiW d m ^^^ pw (8 * (8 - m)) (bx d m)
1088
1089def Psi (d : UInt64) : UInt32 := psiW d 8
1090
1091theorem psiW_xor (a b : UInt64) (m : Nat) : psiW (a ^^^ b) m = psiW a m ^^^ psiW b m := by
1092  induction m with
1093  | zero => simp [psiW]
1094  | succ m ih => simp only [psiW, ih, bx_xor, pw_xor]; ac_rfl
1095
1096theorem Psi_xor (a b : UInt64) : Psi (a ^^^ b) = Psi a ^^^ Psi b := psiW_xor a b 8
1097
1098theorem Phi_xor (a b : UInt64) : (wsteps 8 (a ^^^ b)).toUInt32 = (wsteps 8 a).toUInt32 ^^^ (wsteps 8 b).toUInt32 := by
1099  rw [wsteps_xor, UInt64.toUInt32_xor]
1100
1101set_option maxRecDepth 100000 in
1102theorem Phi_basis : ∀ t : Fin 64, (wsteps 8 (UInt64.ofNat (2 ^ t.val))).toUInt32 = Psi (UInt64.ofNat (2 ^ t.val)) := by
1103  decide +kernel
1104
1105theorem Phi_eq_Psi (d : UInt64) : (wsteps 8 d).toUInt32 = Psi d :=
1106  lin64_ext (f := fun d => (wsteps 8 d).toUInt32) (g := Psi) Phi_xor Psi_xor (fun t ht => Phi_basis ⟨t, ht⟩) d
1107
1108
1109/-- the 64-bit word that `loadWord` assembles from eight bytes (little endian) -/
1110def wob (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : UInt64 :=
1111  (0 : UInt64) ||| b0.toUInt64 <<< (8 * 0).toUInt64 ||| b1.toUInt64 <<< (8 * 1).toUInt64 ||| b2.toUInt64 <<< (8 * 2).toUInt64 |||
1112  b3.toUInt64 <<< (8 * 3).toUInt64 ||| b4.toUInt64 <<< (8 * 4).toUInt64 ||| b5.toUInt64 <<< (8 * 5).toUInt64 |||
1113  b6.toUInt64 <<< (8 * 6).toUInt64 ||| b7.toUInt64 <<< (8 * 7).toUInt64
1114
1115theorem getLsbD_255 (i : Nat) (h : 8 ≤ i) : (255#32).getLsbD i = false := by
1116  rw [BitVec.getLsbD_ofNat]
1117  simp
1118  intro _
1119  exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le (by decide) (Nat.pow_le_pow_right (by omega) h))
1120
1121theorem bx_wob_0 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 0 = b0.toUInt32 := by
1122  unfold bx
1123  apply u32_ext
1124  intro i hi
1125  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1126  by_cases h8 : i < 8
1127  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1128      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1129  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1130    simp [this]
1131    intro _
1132    exact BitVec.getLsbD_of_ge _ _ (by omega)
1133
1134theorem bx_wob_1 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 1 = b1.toUInt32 := by
1135  unfold bx
1136  apply u32_ext
1137  intro i hi
1138  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1139  by_cases h8 : i < 8
1140  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1141      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1142  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1143    simp [this]
1144    intro _
1145    exact BitVec.getLsbD_of_ge _ _ (by omega)
1146
1147theorem bx_wob_2 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 2 = b2.toUInt32 := by
1148  unfold bx
1149  apply u32_ext
1150  intro i hi
1151  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1152  by_cases h8 : i < 8
1153  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1154      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1155  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1156    simp [this]
1157    intro _
1158    exact BitVec.getLsbD_of_ge _ _ (by omega)
1159
1160theorem bx_wob_3 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 3 = b3.toUInt32 := by
1161  unfold bx
1162  apply u32_ext
1163  intro i hi
1164  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1165  by_cases h8 : i < 8
1166  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1167      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1168  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1169    simp [this]
1170    intro _
1171    exact BitVec.getLsbD_of_ge _ _ (by omega)
1172
1173theorem bx_wob_4 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 4 = b4.toUInt32 := by
1174  unfold bx
1175  apply u32_ext
1176  intro i hi
1177  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1178  by_cases h8 : i < 8
1179  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1180      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1181  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1182    simp [this]
1183    intro _
1184    exact BitVec.getLsbD_of_ge _ _ (by omega)
1185
1186theorem bx_wob_5 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 5 = b5.toUInt32 := by
1187  unfold bx
1188  apply u32_ext
1189  intro i hi
1190  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1191  by_cases h8 : i < 8
1192  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1193      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1194  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1195    simp [this]
1196    intro _
1197    exact BitVec.getLsbD_of_ge _ _ (by omega)
1198
1199theorem bx_wob_6 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 6 = b6.toUInt32 := by
1200  unfold bx
1201  apply u32_ext
1202  intro i hi
1203  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1204  by_cases h8 : i < 8
1205  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1206      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1207  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1208    simp [this]
1209    intro _
1210    exact BitVec.getLsbD_of_ge _ _ (by omega)
1211
1212theorem bx_wob_7 (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) : bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 7 = b7.toUInt32 := by
1213  unfold bx
1214  apply u32_ext
1215  intro i hi
1216  simp [wob, UInt64.toBitVec_or, UInt64.toBitVec_shiftRight, UInt64.toBitVec_shiftLeft]
1217  by_cases h8 : i < 8
1218  · rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1219      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [BitVec.getLsbD_of_ge]
1220  · have : ¬ (255#32).getLsbD i = true := by rw [getLsbD_255 i (by omega)]; decide
1221    simp [this]
1222    intro _
1223    exact BitVec.getLsbD_of_ge _ _ (by omega)
1224
1225set_option maxRecDepth 100000 in
1226theorem Psi_basis : ∀ t : Fin 32, Psi (e t.val).toUInt64 = pw 64 (e t.val) := by decide +kernel
1227
1228theorem Psi_reg (c : UInt32) : Psi c.toUInt64 = pw 64 c :=
1229  lin32_ext (f := fun c => Psi c.toUInt64) (g := pw 64)
1230    (by intro x y; simp only [UInt32.toUInt64_xor, Psi_xor]) (pw_lin 64) (fun t ht => Psi_basis ⟨t, ht⟩) c
1231
1232theorem Psi_wob (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) :
1233    Psi (wob b0 b1 b2 b3 b4 b5 b6 b7) =
1234      pw 64 b0.toUInt32 ^^^ pw 56 b1.toUInt32 ^^^ pw 48 b2.toUInt32 ^^^ pw 40 b3.toUInt32 ^^^
1235      pw 32 b4.toUInt32 ^^^ pw 24 b5.toUInt32 ^^^ pw 16 b6.toUInt32 ^^^ pw 8 b7.toUInt32 := by
1236  have : Psi (wob b0 b1 b2 b3 b4 b5 b6 b7) =
1237      (((((((0 ^^^ pw (8 * (8 - 0)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 0)) ^^^
1238        pw (8 * (8 - 1)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 1)) ^^^
1239        pw (8 * (8 - 2)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 2)) ^^^
1240        pw (8 * (8 - 3)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 3)) ^^^
1241        pw (8 * (8 - 4)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 4)) ^^^
1242        pw (8 * (8 - 5)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 5)) ^^^
1243        pw (8 * (8 - 6)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 6)) ^^^
1244        pw (8 * (8 - 7)) (bx (wob b0 b1 b2 b3 b4 b5 b6 b7) 7) := rfl
1245  rw [this, bx_wob_0, bx_wob_1, bx_wob_2, bx_wob_3, bx_wob_4, bx_wob_5, bx_wob_6, bx_wob_7, UInt32.zero_xor]
1246
1247theorem rbl_bytes (c : UInt32) (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) :
1248    rbl c [b0, b1, b2, b3, b4, b5, b6, b7] =
1249      pw 64 c ^^^ (pw 64 b0.toUInt32 ^^^ pw 56 b1.toUInt32 ^^^ pw 48 b2.toUInt32 ^^^ pw 40 b3.toUInt32 ^^^
1250      pw 32 b4.toUInt32 ^^^ pw 24 b5.toUInt32 ^^^ pw 16 b6.toUInt32 ^^^ pw 8 b7.toUInt32) := by
1251  rw [rbl_affine]
1252  simp only [List.length_cons, List.length_nil]
1253  have : rbl 0 [b0, b1, b2, b3, b4, b5, b6, b7] =
1254      pw 64 b0.toUInt32 ^^^ pw 56 b1.toUInt32 ^^^ pw 48 b2.toUInt32 ^^^ pw 40 b3.toUInt32 ^^^
1255      pw 32 b4.toUInt32 ^^^ pw 24 b5.toUInt32 ^^^ pw 16 b6.toUInt32 ^^^ pw 8 b7.toUInt32 := by
1256    simp only [rbl_cons, rbl_nil, crcByte_eq, UInt32.zero_xor, pw_xor, ← pw_add]
1257  rw [this]
1258
1259/-- the word that `crc_word` is applied to, for the register `c` and the eight bytes: its result is the register after
1260the eight bytes. -/
1261theorem Psi_word (c : UInt32) (b0 b1 b2 b3 b4 b5 b6 b7 : UInt8) :
1262    Psi (c.toUInt64 ^^^ wob b0 b1 b2 b3 b4 b5 b6 b7) = rbl c [b0, b1, b2, b3, b4, b5, b6, b7] := by
1263  rw [Psi_xor, Psi_reg, Psi_wob, rbl_bytes]
1264
1265theorem crc_word_ok (h : Heap) (hs : StaticsOK h) (data : UInt64) : OkOn h (crc_word data) (Psi data) := by
1266  suffices H : ∃ y, OkOn h (crc_word data) y ∧ y = Psi data by obtain ⟨y, hy, rfl⟩ := H; exact hy
1267  unfold crc_word
1268  refine OkOn.bind_ex (R := fun x : UInt64 × Int32 => x.1.toUInt32 = Psi data) ?_ ?_
1269  · refine cwhile_ok (fun cnt s => ∃ i, i + cnt = 8 ∧ s = (wsteps i data, Int32.ofNat i))
1270      (fun x : UInt64 × Int32 => x.1.toUInt32 = Psi data) ?_ ?_ (k := 8) (s := (data, (0 : Int32))) ?_ ?_
1271    · intro cnt s hP
1272      obtain ⟨i, hi, rfl⟩ := hP
1273      have hc : (Int32.ofNat i < (8 : Int32)) = true := by
1274        rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1275          rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1276      have hk : Int32.ofNat i + 1 = Int32.ofNat (i + 1) := by
1277        rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
1278          rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1279      have ht := crcTab_ok h hs (wsteps i data &&& 0xff) (and255_lt _)
1280      refine ⟨(wsteps i data, Int32.ofNat i), (wsteps (i + 1) data, Int32.ofNat (i + 1)), ?_, ?_, ⟨i + 1, by omega, rfl⟩⟩
1281      · show OkOn h (pure _) _
1282        simp only [W, hc]
1283        exact OkOn.pure _ _
1284      · show OkOn h (do let t ← crcTab (wsteps i data &&& 0xff); pure ((wsteps i data >>> 8) ^^^ t.toUInt64, Int32.ofNat i + 1)) _
1285        rw [hk]
1286        exact OkOn.bind ht (OkOn.pure _ _)
1287    · intro s hP
1288      obtain ⟨i, hi, rfl⟩ := hP
1289      have : i = 8 := by omega
1290      subst this
1291      have hc : (Int32.ofNat 8 < (8 : Int32)) = false := by decide
1292      refine ⟨(wsteps 8 data, Int32.ofNat 8), ?_, ?_⟩
1293      · show OkOn h (pure _) _
1294        simp only [W, hc]
1295        exact OkOn.pure _ _
1296      · exact Phi_eq_Psi data
1297    · exact ⟨0, rfl, rfl⟩
1298    · show 8 < 2 ^ 64; omega
1299  · intro x hx
1300    obtain ⟨d, k⟩ := x
1301    exact ⟨d.toUInt32, OkOn.pure _ _, hx⟩
1302
1303/-! ### Loading a word -/
1304
1305theorem idx8 (h : Heap) (blk off i : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs) (hlt : off + i < bs.size) :
1306    OkOn h (index8 (.ref (.blk blk) off) i) bs[off + i]! := by
1307  have := index8_ok hb hlt
1308  rw [getElem!_pos bs (off + i) hlt]; exact this
1309
1310set_option maxRecDepth 4000 in
1311theorem loadWord_ok (h : Heap) (blk off : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1312    (hlt : off + 8 ≤ bs.size) :
1313    OkOn h (loadWord (.ref (.blk blk) off))
1314      (wob bs[off + 0]! bs[off + 1]! bs[off + 2]! bs[off + 3]! bs[off + 4]! bs[off + 5]! bs[off + 6]! bs[off + 7]!) := by
1315  unfold loadWord
1316  simp only [forIn, Std.Legacy.Range.forIn'_eq_forIn'_range', Std.Legacy.Range.size]
1317  simp only [List.range'_succ, List.range'_zero, List.forIn'_cons, List.forIn'_nil]
1318  refine OkOn.bind (x := wob bs[off + 0]! bs[off + 1]! bs[off + 2]! bs[off + 3]! bs[off + 4]! bs[off + 5]! bs[off + 6]! bs[off + 7]!) ?_ (OkOn.pure _ _)
1319  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1320  try dsimp only
1321  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1322  try dsimp only
1323  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1324  try dsimp only
1325  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1326  try dsimp only
1327  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1328  try dsimp only
1329  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1330  try dsimp only
1331  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1332  try dsimp only
1333  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h blk off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
1334  try dsimp only
1335  exact OkOn.pure _ _
1336
1337/-! ### The braid tables -/
1338
1339def psum (d : UInt64) : Nat → UInt32
1340  | 0 => 0
1341  | m + 1 => psum d m ^^^ pw (8 * (40 - m)) (bx d m)
1342
1343/-- the effect of the eight table lookups on a 64-bit word -/
1344def bw (d : UInt64) : UInt32 := psum d 8
1345
1346theorem idx2_ok (h : Heap) (kn i : Nat) (hk : kn < 8) (hi : i < 256) :
1347    OkOn h (idx2 Crc32H.crc_braid_table kn i) Crc32H.crc_braid_table[kn]![i]! := by
1348  have hs := braid_size
1349  have hrow : Crc32H.crc_braid_table[kn]? = some Crc32H.crc_braid_table[kn]! := by
1350    rw [getElem!_pos Crc32H.crc_braid_table kn (by omega)]; simp
1351  have hrs := hs.2 ⟨kn, hk⟩
1352  have hcol : Crc32H.crc_braid_table[kn]![i]? = some Crc32H.crc_braid_table[kn]![i]! := by
1353    rw [getElem!_pos Crc32H.crc_braid_table[kn]! i (by simp only at hrs; omega)]; simp
1354  unfold idx2
1355  rw [hrow]
1356  simp only
1357  rw [hcol]
1358  exact OkOn.pure _ _
1359
1360theorem braidTab_ok (h : Heap) (kn : Nat) (hk : kn < 8) (word : UInt64) :
1361    OkOn h (braidTab (Int32.ofNat kn) word) (pw (8 * (40 - kn)) (bx word kn)) := by
1362  have h3 : (Int32.ofNat kn <<< 3).toInt.toNat.toUInt64 = (8 * kn).toUInt64 := by
1363    rcases (by omega : kn = 0 ∨ kn = 1 ∨ kn = 2 ∨ kn = 3 ∨ kn = 4 ∨ kn = 5 ∨ kn = 6 ∨ kn = 7) with
1364      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1365  have hk' : (Int32.ofNat kn).toInt.toNat = kn := by
1366    rcases (by omega : kn = 0 ∨ kn = 1 ∨ kn = 2 ∨ kn = 3 ∨ kn = 4 ∨ kn = 5 ∨ kn = 6 ∨ kn = 7) with
1367      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1368  have h64 : (8 * kn).toUInt64 < 64 := by
1369    rcases (by omega : kn = 0 ∨ kn = 1 ∨ kn = 2 ∨ kn = 3 ∨ kn = 4 ∨ kn = 5 ∨ kn = 6 ∨ kn = 7) with
1370      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1371  have hsh : OkOn h (shr64 word (8 * kn).toUInt64) (word >>> (8 * kn).toUInt64) := by
1372    unfold shr64; rw [ite_eq_left h64]; exact OkOn.pure _ _
1373  have hid := idx2_ok h kn ((word >>> (8 * kn).toUInt64) &&& 0xff).toNat hk (and255_lt _)
1374  have hv : Crc32H.crc_braid_table[kn]![((word >>> (8 * kn).toUInt64) &&& 0xff).toNat]! =
1375      pw (8 * (40 - kn)) (bx word kn) := by
1376    have := braid_eq ⟨kn, hk⟩ ⟨_, and255_lt (word >>> (8 * kn).toUInt64)⟩
1377    simp only at this
1378    rw [this, toUInt32_ofNat_eq _ (and255_lt _)]; rfl
1379  unfold braidTab
1380  rw [h3, hk']
1381  rw [hv] at hid
1382  exact OkOn.bind hsh hid
1383
1384theorem psum_eq (d : UInt64) : ∀ m, m ≤ 8 → psum d m = pw 256 (psiW d m) := by
1385  intro m
1386  induction m with
1387  | zero => intro _; simp [psum, psiW, pw_zero]
1388  | succ m ih =>
1389    intro hm
1390    simp only [psum, psiW, ih (by omega), pw_xor, ← pw_add]
1391    congr 2; omega
1392
1393theorem bw_eq (d : UInt64) : bw d = pw 256 (Psi d) := psum_eq d 8 (Nat.le_refl _)
1394
1395/-- the word at byte offset `o` of `bs` -/
1396def WA (bs : Array UInt8) (o : Nat) : UInt64 :=
1397  wob bs[o + 0]! bs[o + 1]! bs[o + 2]! bs[o + 3]! bs[o + 4]! bs[o + 5]! bs[o + 6]! bs[o + 7]!
1398
1399theorem wordAt_ok (h : Heap) (blk ow i : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1400    (hlt : ow + 8 * i + 8 ≤ bs.size) :
1401    OkOn h (wordAt (.ref (.blk blk) ow) i) (WA bs (ow + 8 * i)) := by
1402  unfold wordAt
1403  have hadd : OkOn h (Ptr.add (Ptr.ref (BRef.blk blk) ow) (8 * (i : Int))) (Ptr.ref (BRef.blk blk) (ow + 8 * i)) := by
1404    have := Ptr.add_ok (r := BRef.blk blk) (off := ow) (k := 8 * (i : Int)) (a := bs) hb (by omega) (by omega)
1405    have e : ((ow : Int) + 8 * (i : Int)).toNat = ow + 8 * i := by omega
1406    rwa [e] at this
1407  exact OkOn.bind hadd (loadWord_ok h blk (ow + 8 * i) bs hb hlt)
1408
1409theorem bind_of {α β : Type} {h : Heap} {m : M α} {f : α → M β} {y : β} (R : α → Prop)
1410    (hm : ∃ x, OkOn h m x ∧ R x) (hf : ∀ x, R x → OkOn h (f x) y) : OkOn h (m >>= f) y := by
1411  obtain ⟨x, hx, hR⟩ := hm
1412  exact OkOn.bind hx (hf x hR)
1413
1414theorem blockLittle_ok (h : Heap) (s : BL) (blk ow : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1415    (hlt : ow + 40 ≤ bs.size) (hw : s.words = .ref (.blk blk) ow) :
1416    OkOn h (blockLittle s)
1417      { crc0 := bw (s.crc0.toUInt64 ^^^ WA bs ow), crc1 := bw (s.crc1.toUInt64 ^^^ WA bs (ow + 8)),
1418        crc2 := bw (s.crc2.toUInt64 ^^^ WA bs (ow + 16)), crc3 := bw (s.crc3.toUInt64 ^^^ WA bs (ow + 24)),
1419        crc4 := bw (s.crc4.toUInt64 ^^^ WA bs (ow + 32)), words := .ref (.blk blk) (ow + 40), blks := s.blks } := by
1420  have w0 := wordAt_ok h blk ow 0 bs hb (by omega)
1421  have w1 := wordAt_ok h blk ow 1 bs hb (by omega)
1422  have w2 := wordAt_ok h blk ow 2 bs hb (by omega)
1423  have w3 := wordAt_ok h blk ow 3 bs hb (by omega)
1424  have w4 := wordAt_ok h blk ow 4 bs hb (by omega)
1425  simp only [Nat.mul_zero, Nat.add_zero] at w0
1426  have hadd : OkOn h (Ptr.add s.words 40) (Ptr.ref (BRef.blk blk) (ow + 40)) := by
1427    rw [hw]
1428    have := Ptr.add_nat_ok (r := BRef.blk blk) (off := ow) (n := 40) (a := bs) hb hlt
1429    simpa using this
1430  rw [← hw] at w0 w1 w2 w3 w4
1431  unfold blockLittle
1432  refine OkOn.bind w0 ?_
1433  try dsimp only
1434  refine OkOn.bind w1 ?_
1435  try dsimp only
1436  refine OkOn.bind w2 ?_
1437  try dsimp only
1438  refine OkOn.bind w3 ?_
1439  try dsimp only
1440  refine OkOn.bind w4 ?_
1441  try dsimp only
1442  refine OkOn.bind hadd ?_
1443  try dsimp only
1444  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
1445  try dsimp only
1446  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
1447  try dsimp only
1448  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
1449  try dsimp only
1450  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
1451  try dsimp only
1452  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
1453  try dsimp only
1454  generalize hW0 : s.crc0.toUInt64 ^^^ WA bs (ow + 8 * 0) = W0
1455  generalize hW1 : s.crc1.toUInt64 ^^^ WA bs (ow + 8 * 1) = W1
1456  generalize hW2 : s.crc2.toUInt64 ^^^ WA bs (ow + 8 * 2) = W2
1457  generalize hW3 : s.crc3.toUInt64 ^^^ WA bs (ow + 8 * 3) = W3
1458  generalize hW4 : s.crc4.toUInt64 ^^^ WA bs (ow + 8 * 4) = W4
1459  refine bind_of (fun s => s = (bw W0, bw W1, bw W2, bw W3, bw W4, Int32.ofNat 8)) ?_ ?_
1460  · refine cwhile_ok (fun cnt s => ∃ m, m + cnt = 8 ∧ 1 ≤ m ∧
1461        s = (psum W0 m, psum W1 m, psum W2 m, psum W3 m, psum W4 m, Int32.ofNat m))
1462      (fun s => s = (bw W0, bw W1, bw W2, bw W3, bw W4, Int32.ofNat 8)) ?_ ?_ (k := 7)
1463      (s := (pw (8 * (40 - 0)) (bx W0 0), pw (8 * (40 - 0)) (bx W1 0), pw (8 * (40 - 0)) (bx W2 0),
1464        pw (8 * (40 - 0)) (bx W3 0), pw (8 * (40 - 0)) (bx W4 0), 1)) ?_ ?_
1465    · intro cnt s hP
1466      obtain ⟨m, hm, hm1, rfl⟩ := hP
1467      have hc : (Int32.ofNat m < W) = true := by
1468        rcases (by omega : m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5 ∨ m = 6 ∨ m = 7) with
1469          rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1470      have hk : Int32.ofNat m + 1 = Int32.ofNat (m + 1) := by
1471        rcases (by omega : m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5 ∨ m = 6 ∨ m = 7) with
1472          rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
1473      refine ⟨(psum W0 m, psum W1 m, psum W2 m, psum W3 m, psum W4 m, Int32.ofNat m), (psum W0 (m + 1), psum W1 (m + 1), psum W2 (m + 1), psum W3 (m + 1), psum W4 (m + 1),
1474        Int32.ofNat (m + 1)), ?_, ?_, ⟨m + 1, by omega, by omega, rfl⟩⟩
1475      · show OkOn h (pure _) _
1476        simp only [hc]
1477        exact OkOn.pure _ _
1478      · show OkOn h (do
1479          let a0 ← braidTab (Int32.ofNat m) W0
1480          let a1 ← braidTab (Int32.ofNat m) W1
1481          let a2 ← braidTab (Int32.ofNat m) W2
1482          let a3 ← braidTab (Int32.ofNat m) W3
1483          let a4 ← braidTab (Int32.ofNat m) W4
1484          pure (psum W0 m ^^^ a0, psum W1 m ^^^ a1, psum W2 m ^^^ a2, psum W3 m ^^^ a3, psum W4 m ^^^ a4,
1485            Int32.ofNat m + 1)) _
1486        rw [hk]
1487        exact OkOn.bind (braidTab_ok h m (by omega) _) (OkOn.bind (braidTab_ok h m (by omega) _)
1488          (OkOn.bind (braidTab_ok h m (by omega) _) (OkOn.bind (braidTab_ok h m (by omega) _)
1489          (OkOn.bind (braidTab_ok h m (by omega) _) (OkOn.pure _ _)))))
1490    · intro s hP
1491      obtain ⟨m, hm, hm1, rfl⟩ := hP
1492      have : m = 8 := by omega
1493      subst this
1494      have hc : (Int32.ofNat 8 < W) = false := by decide
1495      refine ⟨_, ?_, rfl⟩
1496      · show OkOn h (pure _) _
1497        simp only [hc]
1498        exact OkOn.pure _ _
1499    · exact ⟨1, by omega, Nat.le_refl _, by simp [psum]⟩
1500    · show 7 < 2 ^ 64; omega
1501  · intro x hx
1502    subst hx
1503    exact OkOn.pure _ _
1504
1505/-! ### The register over a range of a byte array -/
1506
1507/-- the register after `n` bytes of `bs` from index `o`, starting from `c` -/
1508def rbFrom (bs : Array UInt8) : UInt32 → Nat → Nat → UInt32
1509  | c, _, 0 => c
1510  | c, o, n + 1 => rbFrom bs (ZlibF.Spec.crcByte c bs[o]!) (o + 1) n
1511
1512theorem rbFrom_zero (bs : Array UInt8) (c : UInt32) (o : Nat) : rbFrom bs c o 0 = c := rfl
1513theorem rbFrom_succ (bs : Array UInt8) (c : UInt32) (o n : Nat) :
1514    rbFrom bs c o (n + 1) = rbFrom bs (ZlibF.Spec.crcByte c bs[o]!) (o + 1) n := rfl
1515
1516theorem rbFrom_add (bs : Array UInt8) (n m : Nat) : ∀ (c : UInt32) (o : Nat),
1517    rbFrom bs c o (n + m) = rbFrom bs (rbFrom bs c o n) (o + n) m := by
1518  induction n with
1519  | zero => intro c o; simp [rbFrom_zero]
1520  | succ n ih =>
1521    intro c o
1522    rw [Nat.succ_add, rbFrom_succ, ih, rbFrom_succ]
1523    rw [show o + 1 + n = o + (n + 1) by omega]
1524
1525theorem rbFrom_aff (bs : Array UInt8) (n : Nat) : ∀ (c : UInt32) (o : Nat),
1526    rbFrom bs c o n = pw (8 * n) c ^^^ rbFrom bs 0 o n := by
1527  induction n with
1528  | zero => intro c o; simp [rbFrom_zero, pw]
1529  | succ n ih =>
1530    intro c o
1531    rw [rbFrom_succ, rbFrom_succ, ih, ih (ZlibF.Spec.crcByte 0 bs[o]!)]
1532    simp only [crcByte_eq, UInt32.zero_xor, pw_xor]
1533    rw [show 8 * (n + 1) = 8 * n + 8 by omega, pw_add]
1534    ac_rfl
1535
1536theorem rbFrom_list (bs : Array UInt8) (n : Nat) : ∀ (c : UInt32) (o : Nat), o + n ≤ bs.size →
1537    rbFrom bs c o n = rbl c ((bs.toList.drop o).take n) := by
1538  induction n with
1539  | zero => intro c o _; simp [rbFrom_zero, rbl_nil]
1540  | succ n ih =>
1541    intro c o h
1542    have ho : o < bs.size := by omega
1543    have : (bs.toList.drop o) = bs[o] :: bs.toList.drop (o + 1) := by
1544      rw [List.drop_eq_getElem_cons (by simpa using ho)]; simp
1545    rw [rbFrom_succ, ih _ _ (by omega), this, List.take_succ_cons, rbl_cons]
1546    rw [getElem!_pos bs o ho]
1547
1548theorem rbFrom8 (bs : Array UInt8) (c : UInt32) (o : Nat) :
1549    rbFrom bs c o 8 = rbl c [bs[o + 0]!, bs[o + 1]!, bs[o + 2]!, bs[o + 3]!, bs[o + 4]!, bs[o + 5]!, bs[o + 6]!, bs[o + 7]!] := rfl
1550
1551theorem Psi_WA (c : UInt32) (bs : Array UInt8) (o : Nat) : Psi (c.toUInt64 ^^^ WA bs o) = rbFrom bs c o 8 := by
1552  rw [rbFrom8]; exact Psi_word c _ _ _ _ _ _ _ _
1553
1554theorem rbFrom8_xor (bs : Array UInt8) (a b : UInt32) (o : Nat) :
1555    rbFrom bs (a ^^^ b) o 8 = rbFrom bs a o 8 ^^^ pw 64 b := by
1556  rw [rbFrom_aff bs 8 (a ^^^ b), rbFrom_aff bs 8 a, pw_xor]
1557  simp only [Nat.reduceMul]
1558  ac_rfl
1559
1560/-! ### The five-word chain at the end of the braided loop -/
1561
1562def Val (c0 c1 c2 c3 c4 : UInt32) : UInt32 :=
1563  pw 320 c0 ^^^ pw 256 c1 ^^^ pw 192 c2 ^^^ pw 128 c3 ^^^ pw 64 c4
1564
1565def chain (bs : Array UInt8) (c0 c1 c2 c3 c4 : UInt32) (o : Nat) : UInt32 :=
1566  rbFrom bs (c4 ^^^ rbFrom bs (c3 ^^^ rbFrom bs (c2 ^^^ rbFrom bs (c1 ^^^ rbFrom bs c0 o 8) (o + 8) 8) (o + 16) 8)
1567    (o + 24) 8) (o + 32) 8
1568
1569theorem chain_aff (bs : Array UInt8) (c0 c1 c2 c3 c4 : UInt32) (o : Nat) :
1570    chain bs c0 c1 c2 c3 c4 o = Val c0 c1 c2 c3 c4 ^^^ chain bs 0 0 0 0 0 o := by
1571  unfold chain Val
1572  simp only [rbFrom8_xor]
1573  rw [rbFrom_aff bs 8 c0 o, rbFrom_aff bs 8 c1 (o + 8), rbFrom_aff bs 8 c2 (o + 16), rbFrom_aff bs 8 c3 (o + 24),
1574    rbFrom_aff bs 8 c4 (o + 32)]
1575  simp only [pw_xor, Nat.reduceMul, ← pw_add, Nat.reduceAdd]
1576  ac_rfl
1577
1578theorem chain_zero (bs : Array UInt8) (o : Nat) : chain bs 0 0 0 0 0 o = rbFrom bs 0 o 40 := by
1579  unfold chain
1580  simp only [UInt32.zero_xor]
1581  have e1 : ∀ c o, rbFrom bs c o 40 = rbFrom bs (rbFrom bs c o 8) (o + 8) 32 := fun c o => rbFrom_add bs 8 32 c o
1582  have e2 : ∀ c o, rbFrom bs c o 32 = rbFrom bs (rbFrom bs c o 8) (o + 8) 24 := fun c o => rbFrom_add bs 8 24 c o
1583  have e3 : ∀ c o, rbFrom bs c o 24 = rbFrom bs (rbFrom bs c o 8) (o + 8) 16 := fun c o => rbFrom_add bs 8 16 c o
1584  have e4 : ∀ c o, rbFrom bs c o 16 = rbFrom bs (rbFrom bs c o 8) (o + 8) 8 := fun c o => rbFrom_add bs 8 8 c o
1585  rw [e1, e2, e3, e4]
1586
1587set_option maxRecDepth 100000 in
1588/-- `Val` after one pass of the braids: `pw 320` of the chain result -/
1589theorem val_step (bs : Array UInt8) (c0 c1 c2 c3 c4 : UInt32) (o : Nat) :
1590    Val (pw 256 (rbFrom bs c0 o 8)) (pw 256 (rbFrom bs c1 (o + 8) 8)) (pw 256 (rbFrom bs c2 (o + 16) 8))
1591      (pw 256 (rbFrom bs c3 (o + 24) 8)) (pw 256 (rbFrom bs c4 (o + 32) 8)) = pw 320 (chain bs c0 c1 c2 c3 c4 o) := by
1592  unfold chain Val
1593  simp only [rbFrom8_xor, pw_xor, Nat.reduceMul, ← pw_add, Nat.reduceAdd]
1594  ac_rfl
1595
1596/-! ### One byte of the table-driven CRC -/
1597
1598set_option maxRecDepth 100000 in
1599theorem pw8_basis : ∀ t : Fin 32,
1600    pw 8 (e t.val) = (e t.val >>> 8) ^^^ pw 8 (e t.val &&& 0xff) := by decide +kernel
1601
1602theorem pw8_split (v : UInt32) : pw 8 v = (v >>> 8) ^^^ pw 8 (v &&& 0xff) :=
1603  lin32_ext (f := pw 8) (g := fun v => (v >>> 8) ^^^ pw 8 (v &&& 0xff)) (pw_lin 8)
1604    (by intro x y; simp only [UInt32.shiftRight_xor, and_xor32, pw_xor]; ac_rfl)
1605    (fun t ht => pw8_basis ⟨t, ht⟩) v
1606
1607theorem wstep_u32 (v : UInt32) : wstep v.toUInt64 = (pw 8 v).toUInt64 := by
1608  unfold wstep
1609  rw [tab_lookup, pw8_split v]
1610  have h1 : (v.toUInt64 &&& 0xff).toUInt32 = v &&& 0xff := by
1611    apply UInt32.toNat_inj.mp
1612    rw [UInt64.toNat_toUInt32, UInt64.toNat_and, UInt32.toNat_and, UInt32.toNat_toUInt64]
1613    have : (0xff : UInt64).toNat = 255 := by decide
1614    have h2 : (0xff : UInt32).toNat = 255 := by decide
1615    rw [this, h2]
1616    exact Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt Nat.and_le_right (by decide))
1617  have h2 : v.toUInt64 >>> 8 = (v >>> 8).toUInt64 := by
1618    apply UInt64.toNat_inj.mp
1619    rw [UInt64.toNat_shiftRight, UInt32.toNat_toUInt64, UInt32.toNat_toUInt64, UInt32.toNat_shiftRight]
1620    rfl
1621  rw [h1, h2, UInt32.toUInt64_xor]
1622
1623theorem u8_u32_u64 (b : UInt8) : b.toUInt32.toUInt64 = b.toUInt64 := by
1624  apply UInt64.toNat_inj.mp
1625  simp
1626
1627theorem crcByte_ok (h : Heap) (hs : StaticsOK h) (blk o : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1628    (ho : o < bs.size) (c : UInt32) :
1629    OkOn h (crcByte c.toUInt64 (.ref (.blk blk) o))
1630      ((ZlibF.Spec.crcByte c bs[o]!).toUInt64, Ptr.ref (BRef.blk blk) (o + 1)) := by
1631  unfold crcByte
1632  have hl := load8_ok hb ho
1633  have hadd := Ptr.add_nat_ok (r := BRef.blk blk) (off := o) (n := 1) (a := bs) hb (by omega)
1634  have ht := crcTab_ok h hs ((c.toUInt64 ^^^ bs[o].toUInt64) &&& 0xff) (and255_lt _)
1635  have e : ((c.toUInt64 >>> 8) ^^^ Crc32H.crc_table[((c.toUInt64 ^^^ bs[o].toUInt64) &&& 0xff).toNat]!.toUInt64) =
1636      (ZlibF.Spec.crcByte c bs[o]).toUInt64 := by
1637    have := wstep_u32 (c ^^^ bs[o].toUInt32)
1638    rw [UInt32.toUInt64_xor, u8_u32_u64] at this
1639    unfold wstep at this
1640    have h8 : bs[o].toUInt64 >>> 8 = 0 := by
1641      apply UInt64.toNat_inj.mp
1642      rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
1643      have := UInt8.toNat_lt bs[o]
1644      simp
1645      omega
1646    rw [UInt64.shiftRight_xor, h8, UInt64.xor_zero] at this
1647    rw [crcByte_eq, this]
1648  rw [getElem!_pos bs o ho]
1649  rw [← e]
1650  exact OkOn.bind hl (OkOn.bind hadd (OkOn.bind ht (OkOn.pure _ _)))
1651
1652/-! ### The tail of `crc32_z`: the loops over eight bytes and over single bytes -/
1653
1654def cond8 (x : UInt64 × BPtr × UInt64) : M (Bool × UInt64 × BPtr × UInt64) :=
1655  match x with
1656  | (c, b, l) => pure (decide (l ≥ 8), c, b, l)
1657
1658def body8 (x : UInt64 × BPtr × UInt64) : M (UInt64 × BPtr × UInt64) :=
1659  match x with
1660  | (c, b, l) =>
1661    have l := l - 8
1662    do
1663    let __x ← crcByte c b
1664    match __x with
1665    | (c, b) => do
1666    let __x ← crcByte c b
1667    match __x with
1668    | (c, b) => do
1669    let __x ← crcByte c b
1670    match __x with
1671    | (c, b) => do
1672    let __x ← crcByte c b
1673    match __x with
1674    | (c, b) => do
1675    let __x ← crcByte c b
1676    match __x with
1677    | (c, b) => do
1678    let __x ← crcByte c b
1679    match __x with
1680    | (c, b) => do
1681    let __x ← crcByte c b
1682    match __x with
1683    | (c, b) => do
1684    let __x ← crcByte c b
1685    match __x with
1686    | (c, b) => pure (c, b, l)
1687
1688def cond1 (x : UInt64 × BPtr × UInt64) : M (Bool × UInt64 × BPtr × UInt64) :=
1689  match x with
1690  | (c, b, l) => pure (l != 0, c, b, l)
1691
1692def body1 (x : UInt64 × BPtr × UInt64) : M (UInt64 × BPtr × UInt64) :=
1693  match x with
1694  | (c, b, l) =>
1695    have l := l - 1
1696    do
1697    let __x ← crcByte c b
1698    match __x with
1699    | (c, b) => pure (c, b, l)
1700
1701/-- the end of `crc32_z` (the local join point of the translation) -/
1702def tailP (crc : UInt64) (buf : BPtr) (len : UInt64) : M UInt64 := do
1703  let __x ← cwhile cond8 body8 (crc, buf, len)
1704  match __x with
1705  | (c, b, l) => do
1706    let __x ← cwhile cond1 body1 (c, b, l)
1707    match __x with
1708    | (c, _, _) => pure (c ^^^ 4294967295)
1709
1710theorem body1_ok (h : Heap) (hs : StaticsOK h) (blk o : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1711    (ho : o < bs.size) (c : UInt32) (l : UInt64) :
1712    OkOn h (body1 (c.toUInt64, .ref (.blk blk) o, l))
1713      ((ZlibF.Spec.crcByte c bs[o]!).toUInt64, Ptr.ref (BRef.blk blk) (o + 1), l - 1) := by
1714  unfold body1
1715  exact OkOn.bind (crcByte_ok h hs blk o bs hb ho c) (OkOn.pure _ _)
1716
1717theorem body8_ok (h : Heap) (hs : StaticsOK h) (blk o : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1718    (ho : o + 8 ≤ bs.size) (c : UInt32) (l : UInt64) :
1719    OkOn h (body8 (c.toUInt64, .ref (.blk blk) o, l))
1720      ((rbFrom bs c o 8).toUInt64, Ptr.ref (BRef.blk blk) (o + 8), l - 8) := by
1721  unfold body8
1722  refine OkOn.bind (crcByte_ok h hs blk o bs hb (by omega) c) ?_
1723  refine OkOn.bind (crcByte_ok h hs blk (o + 1) bs hb (by omega) _) ?_
1724  refine OkOn.bind (crcByte_ok h hs blk (o + 1 + 1) bs hb (by omega) _) ?_
1725  refine OkOn.bind (crcByte_ok h hs blk (o + 1 + 1 + 1) bs hb (by omega) _) ?_
1726  refine OkOn.bind (crcByte_ok h hs blk (o + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
1727  refine OkOn.bind (crcByte_ok h hs blk (o + 1 + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
1728  refine OkOn.bind (crcByte_ok h hs blk (o + 1 + 1 + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
1729  refine OkOn.bind (crcByte_ok h hs blk (o + 1 + 1 + 1 + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
1730  exact OkOn.pure _ _
1731
1732theorem rbFrom_snoc (bs : Array UInt8) (c : UInt32) (o j : Nat) :
1733    rbFrom bs c o (j + 1) = ZlibF.Spec.crcByte (rbFrom bs c o j) bs[o + j]! := by
1734  have := rbFrom_add bs j 1 c o
1735  rw [this]; rfl
1736
1737theorem ofNat_sub64 (n k : Nat) (hk : k ≤ n) (hn : n < 2 ^ 64) :
1738    UInt64.ofNat n - UInt64.ofNat k = UInt64.ofNat (n - k) := by
1739  apply UInt64.toNat_inj.mp
1740  rw [UInt64.toNat_sub_of_le, UInt64.toNat_ofNat', UInt64.toNat_ofNat', UInt64.toNat_ofNat',
1741    Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)]
1742  rw [UInt64.le_iff_toNat_le, UInt64.toNat_ofNat', UInt64.toNat_ofNat', Nat.mod_eq_of_lt hn,
1743    Nat.mod_eq_of_lt (by omega)]
1744  exact hk
1745
1746theorem ofNat_toNat_lt (n : Nat) (hn : n < 2 ^ 64) : (UInt64.ofNat n).toNat = n := by
1747  rw [UInt64.toNat_ofNat', Nat.mod_eq_of_lt hn]
1748
1749theorem loop1_ok (h : Heap) (hs : StaticsOK h) (blk o L : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1750    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (c : UInt32) :
1751    OkOn h (cwhile cond1 body1 (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L))
1752      ((rbFrom bs c o L).toUInt64, Ptr.ref (BRef.blk blk) (o + L), 0) := by
1753  suffices H : ∃ s, OkOn h (cwhile cond1 body1 (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L)) s ∧
1754      s = ((rbFrom bs c o L).toUInt64, Ptr.ref (BRef.blk blk) (o + L), 0) by
1755    obtain ⟨s, hs', rfl⟩ := H; exact hs'
1756  refine cwhile_ok (fun k s => ∃ j, j + k = L ∧
1757      s = ((rbFrom bs c o j).toUInt64, Ptr.ref (BRef.blk blk) (o + j), UInt64.ofNat (L - j))) _ ?_ ?_ (k := L)
1758    (s := (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L)) ⟨0, by omega, by simp [rbFrom_zero]⟩ hL
1759  · intro k s hP
1760    obtain ⟨j, hj, rfl⟩ := hP
1761    have hne : (UInt64.ofNat (L - j) != 0) = true := by
1762      have : UInt64.ofNat (L - j) ≠ 0 := by
1763        intro h0
1764        have := congrArg UInt64.toNat h0
1765        rw [ofNat_toNat_lt _ (by omega)] at this
1766        have h1 : (0 : UInt64).toNat = 0 := rfl
1767        omega
1768      simpa using this
1769    refine ⟨((rbFrom bs c o j).toUInt64, Ptr.ref (BRef.blk blk) (o + j), UInt64.ofNat (L - j)), ((ZlibF.Spec.crcByte (rbFrom bs c o j) bs[o + j]!).toUInt64, Ptr.ref (BRef.blk blk) (o + j + 1),
1770      UInt64.ofNat (L - j) - 1), ?_, ?_, ?_⟩
1771    · show OkOn h (pure _) _
1772      simp only [hne]
1773      exact OkOn.pure _ _
1774    · exact body1_ok h hs blk (o + j) bs hb (by omega) _ _
1775    · refine ⟨j + 1, by omega, ?_⟩
1776      rw [rbFrom_snoc, show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
1777      rw [show L - j - 1 = L - (j + 1) by omega]
1778      rfl
1779  · intro s hP
1780    obtain ⟨j, hj, rfl⟩ := hP
1781    have hjL : L = j := by omega
1782    subst hjL
1783    refine ⟨((rbFrom bs c o L).toUInt64, Ptr.ref (BRef.blk blk) (o + L), UInt64.ofNat (L - L)), ?_, ?_⟩
1784    · show OkOn h (pure _) _
1785      simp only [Nat.sub_self]
1786      exact OkOn.pure _ _
1787    · simp [Nat.sub_self]
1788
1789theorem loop8_ok (h : Heap) (hs : StaticsOK h) (blk o L : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1790    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (c : UInt32) :
1791    OkOn h (cwhile cond8 body8 (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L))
1792      ((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * (L / 8)),
1793        UInt64.ofNat (L - 8 * (L / 8))) := by
1794  suffices H : ∃ s, OkOn h (cwhile cond8 body8 (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L)) s ∧
1795      s = ((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * (L / 8)),
1796        UInt64.ofNat (L - 8 * (L / 8))) by
1797    obtain ⟨s, hs', rfl⟩ := H; exact hs'
1798  refine cwhile_ok (fun k s => ∃ j, j + k = L / 8 ∧
1799      s = ((rbFrom bs c o (8 * j)).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * j), UInt64.ofNat (L - 8 * j))) _ ?_ ?_
1800    (k := L / 8) (s := (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L)) ⟨0, by omega, by simp [rbFrom_zero]⟩
1801    (by show L / 8 < 2 ^ 64; omega)
1802  · intro k s hP
1803    obtain ⟨j, hj, rfl⟩ := hP
1804    have hge : (decide (UInt64.ofNat (L - 8 * j) ≥ 8)) = true := by
1805      simp only [decide_eq_true_eq, ge_iff_le, UInt64.le_iff_toNat_le]
1806      rw [ofNat_toNat_lt _ (by omega)]
1807      have : (8 : UInt64).toNat = 8 := rfl
1808      omega
1809    refine ⟨((rbFrom bs c o (8 * j)).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * j), UInt64.ofNat (L - 8 * j)),
1810      ((rbFrom bs (rbFrom bs c o (8 * j)) (o + 8 * j) 8).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * j + 8),
1811        UInt64.ofNat (L - 8 * j) - 8), ?_, ?_, ?_⟩
1812    · show OkOn h (pure _) _
1813      simp only [hge]
1814      exact OkOn.pure _ _
1815    · exact body8_ok h hs blk (o + 8 * j) bs hb (by omega) _ _
1816    · refine ⟨j + 1, by omega, ?_⟩
1817      rw [show 8 * (j + 1) = 8 * j + 8 by omega, rbFrom_add,
1818        show (8 : UInt64) = UInt64.ofNat 8 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
1819      rw [show L - 8 * j - 8 = L - (8 * j + 8) by omega]
1820      rfl
1821  · intro s hP
1822    obtain ⟨j, hj, rfl⟩ := hP
1823    have hjq : j = L / 8 := by omega
1824    have hlt : (decide (UInt64.ofNat (L - 8 * j) ≥ 8)) = false := by
1825      simp only [decide_eq_false_iff_not, ge_iff_le, UInt64.le_iff_toNat_le, Nat.not_le]
1826      rw [ofNat_toNat_lt _ (by omega)]
1827      have : (8 : UInt64).toNat = 8 := rfl
1828      omega
1829    subst hjq
1830    refine ⟨((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * (L / 8)),
1831      UInt64.ofNat (L - 8 * (L / 8))), ?_, rfl⟩
1832    show OkOn h (pure _) _
1833    simp only [hlt]
1834    exact OkOn.pure _ _
1835
1836theorem tail_ok (h : Heap) (hs : StaticsOK h) (blk o L : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1837    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (c : UInt32) :
1838    OkOn h (tailP c.toUInt64 (.ref (.blk blk) o) (UInt64.ofNat L)) ((rbFrom bs c o L).toUInt64 ^^^ 0xffffffff) := by
1839  unfold tailP
1840  refine bind_of (fun x => x = ((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref (BRef.blk blk) (o + 8 * (L / 8)),
1841        UInt64.ofNat (L - 8 * (L / 8)))) ⟨_, loop8_ok h hs blk o L bs hb hle hL c, rfl⟩ ?_
1842  intro x hx
1843  subst hx
1844  show OkOn h (cwhile cond1 body1 _ >>= _) _
1845  refine bind_of (fun x => x = ((rbFrom bs (rbFrom bs c o (8 * (L / 8))) (o + 8 * (L / 8)) (L - 8 * (L / 8))).toUInt64,
1846      Ptr.ref (BRef.blk blk) (o + 8 * (L / 8) + (L - 8 * (L / 8))), 0))
1847    ⟨_, loop1_ok h hs blk (o + 8 * (L / 8)) (L - 8 * (L / 8)) bs hb (by omega) (by omega) _, rfl⟩ ?_
1848  intro x hx
1849  subst hx
1850  rw [← rbFrom_add]
1851  rw [show 8 * (L / 8) + (L - 8 * (L / 8)) = L by omega]
1852  exact OkOn.pure _ _
1853
1854/-! ### The alignment loop -/
1855
1856def condA (x : UInt64 × BPtr × UInt64) : M (Bool × UInt64 × BPtr × UInt64) :=
1857  match x with
1858  | (c, b, l) =>
1859    if (l == 0) = true then pure (false, c, b, l)
1860    else do
1861      let __do_lift ← addrOf b
1862      pure (__do_lift &&& (W - 1).toInt.toNat.toUInt64 != 0, c, b, l)
1863
1864def bodyA (x : UInt64 × BPtr × UInt64) : M (UInt64 × BPtr × UInt64) :=
1865  match x with
1866  | (c, b, l) =>
1867    have l := l - 1
1868    do
1869    let __x ← crcByte c b
1870    match __x with
1871    | (c, b) => pure (c, b, l)
1872
1873theorem W_pred : (W - 1).toInt.toNat.toUInt64 = 7 := by decide
1874
1875theorem and7 (n : Nat) : (UInt64.ofNat n &&& 7).toNat = n % 8 := by
1876  rw [UInt64.toNat_and, UInt64.toNat_ofNat']
1877  have : (7 : UInt64).toNat = 2 ^ 3 - 1 := by decide
1878  rw [this, Nat.and_two_pow_sub_one_eq_mod]
1879  have : (n % 2 ^ 64) % 2 ^ 3 = n % 2 ^ 3 := Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 (by decide))
1880  rw [this]
1881
1882def alignLen (o : Nat) : Nat := (8 - o % 8) % 8
1883
1884theorem loopA_ok (h : Heap) (blk o L : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1885    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (h8 : 8 ≤ L) (hs : StaticsOK h) (c : UInt32) :
1886    OkOn h (cwhile condA bodyA (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L))
1887      ((rbFrom bs c o (alignLen o)).toUInt64, Ptr.ref (BRef.blk blk) (o + alignLen o),
1888        UInt64.ofNat (L - alignLen o)) := by
1889  suffices H : ∃ s, OkOn h (cwhile condA bodyA (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L)) s ∧
1890      s = ((rbFrom bs c o (alignLen o)).toUInt64, Ptr.ref (BRef.blk blk) (o + alignLen o),
1891        UInt64.ofNat (L - alignLen o)) by
1892    obtain ⟨s, hs', rfl⟩ := H; exact hs'
1893  have ha7 : alignLen o ≤ 7 := by unfold alignLen; omega
1894  have hcondA : ∀ j, j ≤ alignLen o →
1895      OkOn h (condA ((rbFrom bs c o j).toUInt64, Ptr.ref (BRef.blk blk) (o + j), UInt64.ofNat (L - j)))
1896        (decide (j < alignLen o), (rbFrom bs c o j).toUInt64, Ptr.ref (BRef.blk blk) (o + j), UInt64.ofNat (L - j)) := by
1897    intro j hj
1898    have hne : (UInt64.ofNat (L - j) == 0) = false := by
1899      have : UInt64.ofNat (L - j) ≠ 0 := by
1900        intro h0
1901        have := congrArg UInt64.toNat h0
1902        rw [ofNat_toNat_lt _ (by omega)] at this
1903        have h1 : (0 : UInt64).toNat = 0 := rfl
1904        omega
1905      simpa using this
1906    have hmod : decide ((UInt64.ofNat (o + j) &&& 7) ≠ 0) = decide (j < alignLen o) := by
1907      have h1 : (UInt64.ofNat (o + j) &&& 7).toNat = (o + j) % 8 := and7 _
1908      by_cases hj' : j < alignLen o
1909      · have : (UInt64.ofNat (o + j) &&& 7) ≠ 0 := by
1910          intro h0; rw [h0] at h1
1911          have h2 : (0 : UInt64).toNat = 0 := rfl
1912          unfold alignLen at hj'; omega
1913        rw [decide_eq_true this, decide_eq_true hj']
1914      · have : (UInt64.ofNat (o + j) &&& 7) = 0 := by
1915          apply UInt64.toNat_inj.mp
1916          have h2 : (0 : UInt64).toNat = 0 := rfl
1917          rw [h1, h2]; unfold alignLen at hj hj'; omega
1918        rw [decide_eq_false (by rw [this]; simp), decide_eq_false hj']
1919    unfold condA
1920    dsimp only
1921    rw [ite_eq_right (by simp [hne])]
1922    show OkOn h (addrOf (Ptr.ref (BRef.blk blk) (o + j)) >>= _) _
1923    refine OkOn.bind (x := UInt64.ofNat (o + j)) (OkOn.pure _ _) ?_
1924    rw [W_pred]
1925    show OkOn h (pure _) _
1926    have hb : ((UInt64.ofNat (o + j) &&& 7) != 0) = decide (j < alignLen o) := by
1927      rw [← hmod]
1928      generalize UInt64.ofNat (o + j) &&& 7 = x
1929      by_cases hx : x = 0 <;> simp [hx]
1930    rw [hb]
1931    exact OkOn.pure _ _
1932  refine cwhile_ok (fun k s => ∃ j, j + k = alignLen o ∧
1933      s = ((rbFrom bs c o j).toUInt64, Ptr.ref (BRef.blk blk) (o + j), UInt64.ofNat (L - j))) _ ?_ ?_
1934    (k := alignLen o) (s := (c.toUInt64, .ref (.blk blk) o, UInt64.ofNat L)) ⟨0, by omega, by simp [rbFrom_zero]⟩
1935    (by show alignLen o < 2 ^ 64; omega)
1936  · intro k s hP
1937    obtain ⟨j, hj, rfl⟩ := hP
1938    refine ⟨((rbFrom bs c o j).toUInt64, Ptr.ref (BRef.blk blk) (o + j), UInt64.ofNat (L - j)),
1939      ((ZlibF.Spec.crcByte (rbFrom bs c o j) bs[o + j]!).toUInt64, Ptr.ref (BRef.blk blk) (o + j + 1),
1940      UInt64.ofNat (L - j) - 1), ?_, ?_, ?_⟩
1941    · have := hcondA j (by omega)
1942      rwa [show decide (j < alignLen o) = true by simp; omega] at this
1943    · exact body1_ok h hs blk (o + j) bs hb (by omega) _ _
1944    · refine ⟨j + 1, by omega, ?_⟩
1945      rw [rbFrom_snoc, show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
1946      rw [show L - j - 1 = L - (j + 1) by omega]
1947      rfl
1948  · intro s hP
1949    obtain ⟨j, hj, rfl⟩ := hP
1950    have hjL : alignLen o = j := by omega
1951    subst hjL
1952    refine ⟨((rbFrom bs c o (alignLen o)).toUInt64, Ptr.ref (BRef.blk blk) (o + alignLen o),
1953      UInt64.ofNat (L - alignLen o)), ?_, rfl⟩
1954    have := hcondA (alignLen o) (Nat.le_refl _)
1955    simpa using this
1956
1957/-! ### The braided loop -/
1958
1959def condBlk (s : BL) : M (Bool × BL) :=
1960  have blks := s.blks - 1
1961  pure (blks != 0, { crc0 := s.crc0, crc1 := s.crc1, crc2 := s.crc2, crc3 := s.crc3, crc4 := s.crc4,
1962                     words := s.words, blks := blks })
1963
1964theorem bw_Psi (c : UInt32) (bs : Array UInt8) (o : Nat) :
1965    bw (c.toUInt64 ^^^ WA bs o) = pw 256 (rbFrom bs c o 8) := by
1966  rw [bw_eq, Psi_WA]
1967
1968theorem val_inv (bs : Array UInt8) (c0 c1 c2 c3 c4 R : UInt32) (ow : Nat)
1969    (hV : Val c0 c1 c2 c3 c4 = pw 320 R) :
1970    Val (pw 256 (rbFrom bs c0 ow 8)) (pw 256 (rbFrom bs c1 (ow + 8) 8)) (pw 256 (rbFrom bs c2 (ow + 16) 8))
1971      (pw 256 (rbFrom bs c3 (ow + 24) 8)) (pw 256 (rbFrom bs c4 (ow + 32) 8)) = pw 320 (rbFrom bs R ow 40) := by
1972  rw [val_step, chain_aff, hV, chain_zero, rbFrom_aff bs 40 R ow]
1973
1974theorem loopBlk_ok (h : Heap) (blk o1 B : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
1975    (hB : 1 ≤ B) (hle : o1 + 40 * B ≤ bs.size) (hB64 : B < 2 ^ 64) (c : UInt32) :
1976    ∃ s : BL, OkOn h (cwhile condBlk blockLittle
1977        { crc0 := c, crc1 := 0, crc2 := 0, crc3 := 0, crc4 := 0, words := (.ref (.blk blk) o1 : BPtr), blks := UInt64.ofNat B }) s ∧
1978      Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 = pw 320 (rbFrom bs c o1 (40 * (B - 1))) ∧
1979      s.words = .ref (.blk blk) (o1 + 40 * (B - 1)) := by
1980  refine cwhile_ok (cond := condBlk) (body := blockLittle) (fun k s => ∃ j, j + k = B - 1 ∧ s.words = .ref (.blk blk) (o1 + 40 * j) ∧
1981      s.blks = UInt64.ofNat (B - j) ∧
1982      Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 = pw 320 (rbFrom bs c o1 (40 * j)))
1983    (fun s => Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 = pw 320 (rbFrom bs c o1 (40 * (B - 1))) ∧
1984      s.words = .ref (.blk blk) (o1 + 40 * (B - 1))) ?_ ?_ (k := B - 1)
1985    (s := { crc0 := c, crc1 := 0, crc2 := 0, crc3 := 0, crc4 := 0, words := (.ref (.blk blk) o1 : BPtr), blks := UInt64.ofNat B }) ?_ (by show B - 1 < 2 ^ 64; omega)
1986  · intro k s hP
1987    obtain ⟨c0, c1, c2, c3, c4, words, blks⟩ := s
1988    obtain ⟨j, hj, hw, hbl, hV⟩ := hP
1989    simp only at hw hbl hV
1990    subst hw hbl
1991    have hne : (UInt64.ofNat (B - j) - 1 != 0) = true := by
1992      rw [show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
1993      have : UInt64.ofNat (B - j - 1) ≠ 0 := by
1994        intro h0
1995        have := congrArg UInt64.toNat h0
1996        rw [ofNat_toNat_lt _ (by omega)] at this
1997        have h1 : (0 : UInt64).toNat = 0 := rfl
1998        omega
1999      simpa using this
2000    let s1 : BL := { crc0 := c0, crc1 := c1, crc2 := c2, crc3 := c3, crc4 := c4,
2001                     words := (.ref (.blk blk) (o1 + 40 * j) : BPtr), blks := UInt64.ofNat (B - j) - 1 }
2002    have hbk := blockLittle_ok h s1 blk (o1 + 40 * j) bs hb (by omega) rfl
2003    refine ⟨s1, _, ?_, hbk, ?_⟩
2004    · show OkOn h (pure _) _
2005      simp only [hne]
2006      exact OkOn.pure _ _
2007    · refine ⟨j + 1, by omega, rfl, ?_, ?_⟩
2008      · show UInt64.ofNat (B - j) - 1 = UInt64.ofNat (B - (j + 1))
2009        rw [show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
2010        rfl
2011      · show Val (bw (c0.toUInt64 ^^^ WA bs (o1 + 40 * j))) (bw (c1.toUInt64 ^^^ WA bs (o1 + 40 * j + 8)))
2012          (bw (c2.toUInt64 ^^^ WA bs (o1 + 40 * j + 16))) (bw (c3.toUInt64 ^^^ WA bs (o1 + 40 * j + 24)))
2013          (bw (c4.toUInt64 ^^^ WA bs (o1 + 40 * j + 32))) = _
2014        rw [bw_Psi, bw_Psi, bw_Psi, bw_Psi, bw_Psi, val_inv bs c0 c1 c2 c3 c4 _ _ hV]
2015        rw [show 40 * (j + 1) = 40 * j + 40 by omega, rbFrom_add]
2016  · intro s hP
2017    obtain ⟨c0, c1, c2, c3, c4, words, blks⟩ := s
2018    obtain ⟨j, hj, hw, hbl, hV⟩ := hP
2019    simp only at hw hbl hV
2020    subst hw hbl
2021    have hjB : j = B - 1 := by omega
2022    subst hjB
2023    have hz : (UInt64.ofNat (B - (B - 1)) - 1 != 0) = false := by
2024      rw [show B - (B - 1) = 1 by omega]
2025      decide
2026    refine ⟨{ crc0 := c0, crc1 := c1, crc2 := c2, crc3 := c3, crc4 := c4,
2027              words := (.ref (.blk blk) (o1 + 40 * (B - 1)) : BPtr), blks := UInt64.ofNat (B - (B - 1)) - 1 }, ?_, hV, rfl⟩
2028    show OkOn h (pure _) _
2029    simp only [hz]
2030    exact OkOn.pure _ _
2031  · refine ⟨0, by omega, rfl, rfl, ?_⟩
2032    simp [Val, rbFrom_zero, pw_zero]
2033
2034theorem ofNat_div64 (n k : Nat) (hn : n < 2 ^ 64) (hk : 0 < k) (hk64 : k < 2 ^ 64) :
2035    UInt64.ofNat n / UInt64.ofNat k = UInt64.ofNat (n / k) := by
2036  apply UInt64.toNat_inj.mp
2037  rw [UInt64.toNat_div, UInt64.toNat_ofNat', UInt64.toNat_ofNat', UInt64.toNat_ofNat',
2038    Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt hk64, Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hn)]
2039
2040theorem ofNat_mul64 (a b : Nat) (h : a * b < 2 ^ 64) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) :
2041    UInt64.ofNat a * UInt64.ofNat b = UInt64.ofNat (a * b) := by
2042  apply UInt64.toNat_inj.mp
2043  rw [UInt64.toNat_mul, UInt64.toNat_ofNat', UInt64.toNat_ofNat', UInt64.toNat_ofNat',
2044    Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt h]
2045
2046theorem crc_init (crc : UInt64) : (~~~crc &&& 4294967295) = (~~~ crc.toUInt32).toUInt64 := by
2047  apply UInt64.toNat_inj.mp
2048  have h1 : (4294967295 : UInt64).toNat = 2 ^ 32 - 1 := by decide
2049  rw [UInt64.toNat_and, h1, Nat.and_two_pow_sub_one_eq_mod, UInt32.toNat_toUInt64]
2050  rw [UInt64.toNat_not, UInt32.toNat_not, UInt64.toNat_toUInt32]
2051  have := UInt64.toNat_lt crc
2052  have e1 : UInt64.size = 2 ^ 64 := rfl
2053  have e2 : UInt32.size = 2 ^ 32 := rfl
2054  simp only [e1, e2] at *
2055  omega
2056
2057theorem ge47 (L : Nat) (hL : L < 2 ^ 64) : (UInt64.ofNat L ≥ 47) ↔ 47 ≤ L := by
2058  have : (47 : UInt64).toNat = 47 := rfl
2059  rw [ge_iff_le, UInt64.le_iff_toNat_le, this, ofNat_toNat_lt _ hL]
2060
2061theorem NW_val : (N * W).toInt.toNat.toUInt64 = 40 := by decide
2062theorem NWW_val : (N * W + W - 1).toInt.toNat.toUInt64 = 47 := by decide
2063
2064theorem crc32_z_ok (h : Heap) (hs : StaticsOK h) (crc : UInt64) (blk off : Nat) (bs : Array UInt8)
2065    (hb : h.bytes blk = some bs) (len : UInt64) (hlen : off + len.toNat ≤ bs.size) :
2066    OkOn h (crc32_z crc (.ref (.blk blk) off) len)
2067      ((rbFrom bs (~~~ crc.toUInt32) off len.toNat).toUInt64 ^^^ 0xffffffff) := by
2068  have hlen' : len = UInt64.ofNat len.toNat := UInt64.ofNat_toNat.symm
2069  have hL : len.toNat < 2 ^ 64 := UInt64.toNat_lt len
2070  generalize len.toNat = L at hlen' hlen hL ⊢
2071  subst hlen'
2072  unfold crc32_z
2073  rw [ite_eq_right (by simp)]
2074  dsimp only
2075  rw [crc_init]
2076  by_cases hlong : 47 ≤ L
2077  · rw [ite_eq_left (by rw [NWW_val]; exact (ge47 L hL).mpr hlong)]
2078    have ha7 : alignLen off ≤ 7 := by unfold alignLen; omega
2079    refine bind_of (fun x => x = ((rbFrom bs (~~~ crc.toUInt32) off (alignLen off)).toUInt64,
2080      Ptr.ref (BRef.blk blk) (off + alignLen off), UInt64.ofNat (L - alignLen off)))
2081      ⟨_, loopA_ok h blk off L bs hb hlen hL (by omega) hs _, rfl⟩ ?_
2082    intro x hx
2083    subst hx
2084    dsimp only
2085    rw [NW_val]
2086    rw [ite_eq_left (by decide), u32_roundtrip]
2087    have hB1 : 1 ≤ (L - alignLen off) / 40 := by omega
2088    have hBle : off + alignLen off + 40 * ((L - alignLen off) / 40) ≤ bs.size := by omega
2089    have hdiv : UInt64.ofNat (L - alignLen off) / 40 = UInt64.ofNat ((L - alignLen off) / 40) := by
2090      rw [show (40 : UInt64) = UInt64.ofNat 40 from rfl, ofNat_div64 _ _ (by omega) (by omega) (by omega)]
2091    have hrem : UInt64.ofNat (L - alignLen off) - UInt64.ofNat ((L - alignLen off) / 40) * 40 =
2092        UInt64.ofNat (L - alignLen off - (L - alignLen off) / 40 * 40) := by
2093      rw [show (40 : UInt64) = UInt64.ofNat 40 from rfl, ofNat_mul64 _ _ (by omega) (by omega) (by omega),
2094        ofNat_sub64 _ _ (by omega) (by omega)]
2095    rw [hdiv, hrem]
2096    refine bind_of (fun s : BL => Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 =
2097        pw 320 (rbFrom bs (rbFrom bs (~~~ crc.toUInt32) off (alignLen off)) (off + alignLen off)
2098          (40 * ((L - alignLen off) / 40 - 1))) ∧
2099        s.words = .ref (.blk blk) (off + alignLen off + 40 * ((L - alignLen off) / 40 - 1)))
2100      (loopBlk_ok h blk (off + alignLen off) ((L - alignLen off) / 40) bs hb hB1 hBle (by omega) _) ?_
2101    intro s hR
2102    obtain ⟨hV, hw⟩ := hR
2103    rw [hw]
2104    generalize hA : alignLen off = a at ha7 hB1 hBle hdiv hrem hV hw ⊢
2105    generalize hB : (L - a) / 40 = B at hB1 hBle hdiv hrem hV hw ⊢
2106    generalize hc' : rbFrom bs (~~~crc.toUInt32) off a = c' at hV ⊢
2107    generalize how : off + a + 40 * (B - 1) = ow at hV hw ⊢
2108    have w0 := wordAt_ok h blk ow 0 bs hb (by omega)
2109    have w1 := wordAt_ok h blk ow 1 bs hb (by omega)
2110    have w2 := wordAt_ok h blk ow 2 bs hb (by omega)
2111    have w3 := wordAt_ok h blk ow 3 bs hb (by omega)
2112    have w4 := wordAt_ok h blk ow 4 bs hb (by omega)
2113    have hadd : OkOn h (Ptr.add (Ptr.ref (BRef.blk blk) ow) 40) (Ptr.ref (BRef.blk blk) (ow + 40)) := by
2114      have := Ptr.add_nat_ok (r := BRef.blk blk) (off := ow) (n := 40) (a := bs) hb (by omega)
2115      simpa using this
2116    have e1 : ∀ (a b : UInt32) (W : UInt64), a.toUInt64 ^^^ W ^^^ b.toUInt64 = (a ^^^ b).toUInt64 ^^^ W := by
2117      intro a b W; rw [UInt32.toUInt64_xor]; ac_rfl
2118    refine OkOn.bind w0 ?_
2119    refine OkOn.bind (crc_word_ok h hs _) ?_
2120    rw [Psi_WA]
2121    refine OkOn.bind w1 ?_
2122    rw [e1]
2123    refine OkOn.bind (crc_word_ok h hs _) ?_
2124    rw [Psi_WA]
2125    refine OkOn.bind w2 ?_
2126    rw [e1]
2127    refine OkOn.bind (crc_word_ok h hs _) ?_
2128    rw [Psi_WA]
2129    refine OkOn.bind w3 ?_
2130    rw [e1]
2131    refine OkOn.bind (crc_word_ok h hs _) ?_
2132    rw [Psi_WA]
2133    refine OkOn.bind w4 ?_
2134    rw [e1]
2135    refine OkOn.bind (crc_word_ok h hs _) ?_
2136    rw [Psi_WA]
2137    refine OkOn.bind hadd ?_
2138    have hx4 : rbFrom bs (s.crc4 ^^^ rbFrom bs (s.crc3 ^^^ rbFrom bs (s.crc2 ^^^ rbFrom bs (s.crc1 ^^^ rbFrom bs s.crc0 (ow + 8 * 0) 8)
2139        (ow + 8 * 1) 8) (ow + 8 * 2) 8) (ow + 8 * 3) 8) (ow + 8 * 4) 8 = rbFrom bs c' (off + a) (40 * B) := by
2140      have h1 := chain_aff bs s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 ow
2141      rw [hV, chain_zero] at h1
2142      change chain bs s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 ow = _
2143      rw [h1, ← rbFrom_aff bs 40 _ ow, ← how, ← rbFrom_add]
2144      congr 1; omega
2145    have hall : rbFrom bs c' (off + a) (40 * B + (L - a - B * 40)) = rbFrom bs (~~~crc.toUInt32) off L := by
2146      rw [← hc']
2147      have := rbFrom_add bs a (L - a) (~~~crc.toUInt32) off
2148      rw [show a + (L - a) = L by omega] at this
2149      rw [this, hc', show 40 * B + (L - a - B * 40) = L - a by omega]
2150    rw [hx4]
2151    rw [rbFrom_add, show off + a + 40 * B = ow + 40 by omega] at hall
2152    rw [← hall]
2153    exact tail_ok h hs blk (ow + 40) (L - a - B * 40) bs hb (by omega) (by omega) _
2154  · rw [ite_eq_right (by rw [NWW_val]; exact fun hh => hlong ((ge47 L hL).mp hh))]
2155    exact tail_ok h hs blk off L bs hb hlen hL _
2156
2157/-! ### Statement helpers -/
2158
2159theorem pw_foldl (m : Nat) (v : UInt32) : (List.range m).foldl (fun c _ => crcBit c) v = pw m v := by
2160  induction m generalizing v with
2161  | zero => rfl
2162  | succ m ih => rw [List.range_succ, List.foldl_append, ih, pw_succ']; rfl
2163
2164theorem e31_eq : (0x80000000 : UInt32) = e 31 := by decide
2165
2166set_option maxRecDepth 100000 in
2167theorem mulp_one_basis : ∀ t : Fin 32, mulp (e t.val) (e 31) = e t.val := by decide +kernel
2168
2169theorem mulp_one_right (a : UInt32) : mulp a (e 31) = a :=
2170  lin32_ext (f := fun a => mulp a (e 31)) (g := fun a => a)
2171    (by intro x y; exact mulp_xor_left x y _) (by intro x y; rfl) (fun t ht => mulp_one_basis ⟨t, ht⟩) a
2172
2173theorem not32_toUInt64 (x : UInt32) : (~~~ x).toUInt64 = x.toUInt64 ^^^ 0xffffffff := by
2174  rw [not32_eq, UInt32.toUInt64_xor]; rfl
2175
2176theorem u64_roundtrip (x : UInt64) (h : x.toNat < 2 ^ 32) : x.toUInt32.toUInt64 = x := by
2177  apply UInt64.toNat_inj.mp
2178  rw [UInt32.toNat_toUInt64, UInt64.toNat_toUInt32, Nat.mod_eq_of_lt h]
2179
2180theorem crc32_append (A B : List UInt8) :
2181    ZlibF.Spec.crc32 (A ++ B) = pw (8 * B.length) (ZlibF.Spec.crc32 A) ^^^ ZlibF.Spec.crc32 B := by
2182  unfold ZlibF.Spec.crc32
2183  rw [← ZlibF.Spec.crc32Update_append, crc32Update_affine]
2184  rfl
2185
2186/-! ## Theorems -/
2187
2188/-- **crc32_z, `buf == NULL`.** For every heap and every `crc`, `len`: `crc32_z(crc, Z_NULL, len)` returns `0` (the
2189initial value of `zlib.h`) and does not touch the heap. -/
2190theorem crc32_z_null (h : Heap) (crc len : UInt64) :
2191    C.run (crc32_z crc .null len) h = .ok (0, h) := by
2192  unfold C.run crc32_z
2193  rw [ite_eq_left (by decide)]
2194  rfl
2195
2196/-- **crc32_z, correctness.** For every heap whose static tables are the ones of `crc32.h` (`StaticsOK`), every `crc`
2197(only its low 32 bits matter, as in C), and every buffer in a heap block (`off + len ≤ size` of the block; the model
2198resolves the alignment test `(z_size_t)buf & 7` through the offset in the block, see `crc32.c.lean`): `crc32_z` returns the
2199CRC-32 of the `len` bytes at `buf` continuing `crc`, that is `ZlibF.Spec.crc32Update` of the byte list, and leaves the
2200heap unchanged. This covers every length (the byte loop, the 8-byte loop, the braided word loop of 5 words of 8 bytes)
2201and every alignment of `off`. This statement covers only heap byte blocks. Static and embedded arrays require
2202the general byte-view result, including their symbolic origin residues. -/
2203theorem crc32_z_correct (h : Heap) (hs : StaticsOK h) (crc : UInt64) (blk off : Nat) (bs : Array UInt8)
2204    (hb : h.bytes blk = some bs) (len : UInt64) (hlen : off + len.toNat ≤ bs.size) :
2205    C.run (crc32_z crc (.ref (.blk blk) off) len) h =
2206      .ok (((ZlibF.Spec.crc32Update crc.toUInt32 ((bs.toList.drop off).take len.toNat))).toUInt64, h) := by
2207  have := crc32_z_ok h hs crc blk off bs hb len hlen
2208  unfold OkOn at this
2209  unfold C.run
2210  rw [this, rbFrom_list bs len.toNat _ off hlen]
2211  have e1 : ZlibF.Spec.crc32Update crc.toUInt32 ((bs.toList.drop off).take len.toNat) =
2212      ~~~ rbl (~~~ crc.toUInt32) ((bs.toList.drop off).take len.toNat) := rfl
2213  rw [e1, not32_toUInt64]
2214
2215/-- **crc32_z, safety.** Same hypotheses as `crc32_z_correct`: no fault (no out-of-bounds read, no bad table index, no
2216shift overflow, no fuel exhaustion), the heap is unchanged (so every heap invariant and every block is preserved). -/
2217theorem crc32_z_safe (h : Heap) (hs : StaticsOK h) (crc : UInt64) (blk off : Nat) (bs : Array UInt8)
2218    (hb : h.bytes blk = some bs) (len : UInt64) (hlen : off + len.toNat ≤ bs.size) :
2219    ∃ r, C.run (crc32_z crc (.ref (.blk blk) off) len) h = .ok (r, h) :=
2220  ⟨_, crc32_z_correct h hs crc blk off bs hb len hlen⟩
2221
2222/-- **crc32, `buf == NULL`.** Returns `0` for every `crc` and `len`; heap unchanged. -/
2223theorem crc32_null (h : Heap) (crc : UInt64) (len : UInt32) :
2224    C.run (crc32 crc .null len) h = .ok (0, h) := crc32_z_null h crc len.toUInt64
2225
2226/-- **crc32, correctness.** As `crc32_z_correct` with `len : uInt` (32 bits). -/
2227theorem crc32_correct (h : Heap) (hs : StaticsOK h) (crc : UInt64) (blk off : Nat) (bs : Array UInt8)
2228    (hb : h.bytes blk = some bs) (len : UInt32) (hlen : off + len.toNat ≤ bs.size) :
2229    C.run (crc32 crc (.ref (.blk blk) off) len) h =
2230      .ok (((ZlibF.Spec.crc32Update crc.toUInt32 ((bs.toList.drop off).take len.toNat))).toUInt64, h) := by
2231  have := crc32_z_correct h hs crc blk off bs hb len.toUInt64 (by rwa [UInt32.toNat_toUInt64])
2232  rw [UInt32.toNat_toUInt64] at this
2233  exact this
2234
2235/-- **crc32, safety.** Same hypotheses as `crc32_correct`; no fault, heap unchanged. -/
2236theorem crc32_safe (h : Heap) (hs : StaticsOK h) (crc : UInt64) (blk off : Nat) (bs : Array UInt8)
2237    (hb : h.bytes blk = some bs) (len : UInt32) (hlen : off + len.toNat ≤ bs.size) :
2238    ∃ r, C.run (crc32 crc (.ref (.blk blk) off) len) h = .ok (r, h) :=
2239  ⟨_, crc32_correct h hs crc blk off bs hb len hlen⟩
2240
2241/-! ### `get_crc_table` -/
2242
2243/-- **get_crc_table, safety.** Returns the pointer to the static table (index 0); no fault; heap unchanged. -/
2244theorem get_crc_table_safe (h : Heap) :
2245    C.run get_crc_table h = .ok (Ptr.ref URef.st_crc_table 0, h) := rfl
2246
2247/-- **get_crc_table, correctness.** With the static tables of `crc32.h`, entry `i < 256` of the returned table is the
2248CRC register after the single byte `i` from the zero register (`ZlibF.Spec.crcByte 0 i`), and reading it does not fault. -/
2249theorem get_crc_table_correct (h : Heap) (hs : StaticsOK h) (i : Nat) (hi : i < 256) :
2250    ∃ p, C.run get_crc_table h = .ok (p, h) ∧
2251      C.run (Ptr.index p (i : Int)) h = .ok (ZlibF.Spec.crcByte 0 (UInt8.ofNat i), h) := by
2252  refine ⟨Ptr.ref URef.st_crc_table 0, rfl, ?_⟩
2253  have hg : Space.get h URef.st_crc_table = some Crc32H.crc_table := by rw [URef.get_st_crc_table, hs.1]
2254  have hlt : 0 + i < Crc32H.crc_table.size := by rw [crc_table_size]; omega
2255  have := Ptr.index_ok (r := URef.st_crc_table) (off := 0) (i := i) hg hlt
2256  unfold OkOn at this
2257  unfold C.run
2258  rw [this]
2259  have e : Crc32H.crc_table[0 + i] = ZlibF.Spec.crcByte 0 (UInt8.ofNat i) := by
2260    have h1 := crc_table_eq ⟨i, hi⟩
2261    simp only at h1
2262    rw [getElem!_pos _ _ (by omega)] at h1
2263    simp only [Nat.zero_add]
2264    rw [h1, crcByte_eq, UInt32.zero_xor]
2265    congr 1
2266    apply UInt32.toNat_inj.mp
2267    simp [UInt8.toNat_ofNat, UInt32.toNat_ofNat']
2268    omega
2269  rw [e]
2270
2271/-! ### `multmodp`, `x2nmodp` -/
2272
2273/-- **multmodp, safety.** If the low 32 bits of `a` are not all zero and `b < 2^32`, `multmodp(a, b)` terminates
2274without fault, returns a value below `2^32` and leaves the heap unchanged. (If the low 32 bits of `a` are zero, the C
2275function loops forever: `multmodp_diverges`.) This is wider than the callers need (`zlib.h` has no `multmodp`). -/
2276theorem multmodp_safe (h : Heap) (a b : UInt64) (ha : a.toUInt32 ≠ 0) (hb : b.toNat < 2 ^ 32) :
2277    ∃ r, C.run (multmodp a b) h = .ok (r, h) ∧ r.toNat < 2 ^ 32 :=
2278  ⟨_, multmodp_ok h a b ha hb, by rw [UInt32.toNat_toUInt64]; exact UInt32.toNat_lt _⟩
2279
2280/-- **multmodp, correctness.** `multmodp(x^n, b)` for the register `x^n` (the register `0x80000000`, which is `x^0`,
2281advanced by `n` steps of the bit-reflected CRC polynomial division `ZlibF.Spec.crcBit`) is `b` advanced by `n` steps:
2282multiplication by `x^n` modulo the CRC polynomial. For every `n` and every `b < 2^32`. -/
2283theorem multmodp_correct (h : Heap) (n : Nat) (b : UInt64) (hb : b.toNat < 2 ^ 32) :
2284    C.run (multmodp ((((List.range n).foldl (fun c _ => crcBit c) (0x80000000 : UInt32))).toUInt64) b) h =
2285      .ok (((List.range n).foldl (fun c _ => crcBit c) b.toUInt32).toUInt64, h) := by
2286  rw [pw_foldl, pw_foldl, e31_eq]
2287  have hne : (pw n (e 31)).toUInt64.toUInt32 ≠ 0 := by
2288    rw [u32_roundtrip]
2289    intro h0
2290    exact e_ne_zero 31 (by omega) (pw_eq_zero _ _ h0)
2291  have := multmodp_ok h (pw n (e 31)).toUInt64 b hne hb
2292  unfold OkOn at this
2293  unfold C.run
2294  rw [this, u32_roundtrip, mulp_pw_left', mulp_one]
2295
2296/-- **x2nmodp, safety.** With the static tables of `crc32.h`, for every `n >= 0` (`z_off64_t`) and every `k`:
2297`x2nmodp(n, k)` terminates without fault, returns a value below `2^32` and leaves the heap unchanged. (`n < 0` is
2298excluded by the callers; the loop `while (n)` would run on the arithmetic shift.) -/
2299theorem x2nmodp_safe (h : Heap) (hs : StaticsOK h) (n : Int64) (hn : 0 ≤ n.toInt) (k : UInt32) :
2300    ∃ r, C.run (x2nmodp n k) h = .ok (r, h) ∧ r.toNat < 2 ^ 32 := by
2301  obtain ⟨p, hp, hp32, _⟩ := x2nmodp_ok h hs n hn k
2302  exact ⟨p, hp, hp32⟩
2303
2304/-- **x2nmodp, correctness.** `x2nmodp(n, k)` is `x^(n * 2^k) mod p(x)`: the register `0x80000000` (`x^0`) advanced by
2305`n * 2^k` steps of `ZlibF.Spec.crcBit`, for `n >= 0` and every `k` (the table index `k & 31` is justified by
2306`x^(2^32) = x`, checked on the table). -/
2307theorem x2nmodp_correct (h : Heap) (hs : StaticsOK h) (n : Int64) (hn : 0 ≤ n.toInt) (k : UInt32) :
2308    C.run (x2nmodp n k) h =
2309      .ok ((((List.range (n.toInt.toNat * 2 ^ k.toNat)).foldl (fun c _ => crcBit c) (0x80000000 : UInt32))).toUInt64, h) := by
2310  obtain ⟨p, hp, hp32, hv⟩ := x2nmodp_ok h hs n hn k
2311  rw [pw_foldl, e31_eq]
2312  have h1 : p.toUInt32 = pw (n.toInt.toNat * 2 ^ k.toNat) (e 31) := by
2313    have := hv (e 31)
2314    rwa [mulp_one_right] at this
2315  unfold OkOn at hp
2316  unfold C.run
2317  rw [hp, ← h1, u64_roundtrip p hp32]
2318
2319/-! ### `crc32_combine` and friends -/
2320
2321/-- **crc32_combine_gen64, safety.** With the static tables of `crc32.h`, no fault and heap unchanged for every
2322`len2`. For `len2 < 0` the result is `0`; for `len2 >= 0` it is below `2^32` and nonzero (so `crc32_combine_op`
2323terminates on it). -/
2324theorem crc32_combine_gen64_safe (h : Heap) (hs : StaticsOK h) (len2 : Int64) :
2325    ∃ op, C.run (crc32_combine_gen64 len2) h = .ok (op, h) ∧ (len2.toInt < 0 → op = 0) ∧
2326      (0 ≤ len2.toInt → op.toNat < 2 ^ 32 ∧ op.toUInt32 ≠ 0) := by
2327  by_cases hneg : len2.toInt < 0
2328  · exact ⟨0, gen64_neg h len2 hneg, fun _ => rfl, fun hh => absurd hh (by omega)⟩
2329  · obtain ⟨op, hop, hlt, hnz, _⟩ := gen64_op h hs len2 (by omega)
2330    exact ⟨op, hop, fun hh => absurd hh hneg, fun _ => ⟨hlt, hnz⟩⟩
2331
2332/-- **crc32_combine_gen64, correctness.** For `len2 >= 0`, the operator is `x^(8 * len2) mod p(x)`: the register
2333`0x80000000` advanced by `8 * len2` steps of `ZlibF.Spec.crcBit` (the effect of `len2` zero bytes on a CRC register). -/
2334theorem crc32_combine_gen64_correct (h : Heap) (hs : StaticsOK h) (len2 : Int64) (hpos : 0 ≤ len2.toInt) :
2335    C.run (crc32_combine_gen64 len2) h =
2336      .ok ((((List.range (8 * len2.toInt.toNat)).foldl (fun c _ => crcBit c) (0x80000000 : UInt32))).toUInt64, h) := by
2337  obtain ⟨op, hop, hlt, hnz, hv⟩ := gen64_op h hs len2 hpos
2338  rw [pw_foldl, e31_eq]
2339  have h1 : op.toUInt32 = pw (8 * len2.toInt.toNat) (e 31) := by
2340    have := hv (e 31)
2341    rwa [mulp_one_right] at this
2342  unfold OkOn at hop
2343  unfold C.run
2344  rw [hop, ← h1, u64_roundtrip op hlt]
2345
2346/-- **crc32_combine_gen, safety.** `z_off_t` is `long` (64 bits): same as `crc32_combine_gen64`. -/
2347theorem crc32_combine_gen_safe (h : Heap) (hs : StaticsOK h) (len2 : Int64) :
2348    ∃ op, C.run (crc32_combine_gen len2) h = .ok (op, h) ∧ (len2.toInt < 0 → op = 0) ∧
2349      (0 ≤ len2.toInt → op.toNat < 2 ^ 32 ∧ op.toUInt32 ≠ 0) :=
2350  crc32_combine_gen64_safe h hs len2
2351
2352/-- **crc32_combine_gen, correctness.** As `crc32_combine_gen64_correct`. -/
2353theorem crc32_combine_gen_correct (h : Heap) (hs : StaticsOK h) (len2 : Int64) (hpos : 0 ≤ len2.toInt) :
2354    C.run (crc32_combine_gen len2) h =
2355      .ok ((((List.range (8 * len2.toInt.toNat)).foldl (fun c _ => crcBit c) (0x80000000 : UInt32))).toUInt64, h) :=
2356  crc32_combine_gen64_correct h hs len2 hpos
2357
2358/-- **crc32_combine_op, safety.** For every `crc1`, `crc2`, and every `op` that is `0` or has a bit set among its low
235932 bits (in particular every value `crc32_combine_gen` returns, and every `op < 2^32`): no fault, heap unchanged.
2360Narrower than the C signature: for `op` nonzero with zero low 32 bits the C function never terminates
2361(`crc32_combine_op_diverges`; reproduced on the real zlib: `crc32_combine_op(1, 2, 1UL << 32)` does not return). -/
2362theorem crc32_combine_op_safe (h : Heap) (crc1 crc2 op : UInt64) (hop : op = 0 ∨ op.toUInt32 ≠ 0) :
2363    ∃ r, C.run (crc32_combine_op crc1 crc2 op) h = .ok (r, h) := by
2364  rcases hop with rfl | hop
2365  · exact ⟨0, by unfold C.run crc32_combine_op; rw [ite_eq_left (by decide)]; rfl⟩
2366  · exact ⟨_, combine_op_ok h crc1 crc2 op hop⟩
2367
2368/-- **crc32_combine_op, the candidate hang.** If `op != 0` and the low 32 bits of `op` are zero (for example
2369`op = 1UL << 32`), the translation of `crc32_combine_op` runs out of fuel (the C loop in `multmodp` does not end):
2370`multmodp` finds no set bit among bits 0..31 of `a`, so `(a & (m - 1)) == 0` is never reached. -/
2371theorem crc32_combine_op_diverges (h : Heap) (crc1 crc2 op : UInt64) (hop : op ≠ 0) (hlow : op.toUInt32 = 0) :
2372    C.run (crc32_combine_op crc1 crc2 op) h = .error .outOfFuel :=
2373  combine_op_diverges h crc1 crc2 op hop hlow
2374
2375/-- **crc32_combine64, safety.** With the static tables of `crc32.h`: every `crc1`, `crc2`, `len2`: no fault, heap
2376unchanged; the result is `0` for `len2 < 0`. -/
2377theorem crc32_combine64_safe (h : Heap) (hs : StaticsOK h) (crc1 crc2 : UInt64) (len2 : Int64) :
2378    ∃ r, C.run (crc32_combine64 crc1 crc2 len2) h = .ok (r, h) ∧ (len2.toInt < 0 → r = 0) :=
2379  ⟨_, combine64_ok h hs crc1 crc2 len2, fun hh => by rw [ite_eq_left hh]⟩
2380
2381/-- **crc32_combine64, correctness.** For two byte sequences `A`, `B` with `len2 = B.length` and the CRC values
2382`crc1 = crc32 A`, `crc2 = crc32 B` (`ZlibF.Spec.crc32`), the result is `crc32 (A ++ B)`. -/
2383theorem crc32_combine64_correct (h : Heap) (hs : StaticsOK h) (A B : List UInt8) (len2 : Int64)
2384    (hlen : len2.toInt = B.length) :
2385    C.run (crc32_combine64 (ZlibF.Spec.crc32 A).toUInt64 (ZlibF.Spec.crc32 B).toUInt64 len2) h =
2386      .ok ((ZlibF.Spec.crc32 (A ++ B)).toUInt64, h) := by
2387  have := combine64_ok h hs (ZlibF.Spec.crc32 A).toUInt64 (ZlibF.Spec.crc32 B).toUInt64 len2
2388  unfold OkOn at this
2389  unfold C.run
2390  rw [this, ite_eq_right (by omega), u32_roundtrip, u32_roundtrip, hlen, Int.toNat_natCast, crc32_append]
2391
2392/-- **crc32_combine, safety.** `z_off_t` is `long`: the same as `crc32_combine64`. -/
2393theorem crc32_combine_safe (h : Heap) (hs : StaticsOK h) (crc1 crc2 : UInt64) (len2 : Int64) :
2394    ∃ r, C.run (crc32_combine crc1 crc2 len2) h = .ok (r, h) ∧ (len2.toInt < 0 → r = 0) :=
2395  crc32_combine64_safe h hs crc1 crc2 len2
2396
2397/-- **crc32_combine, correctness.** As `crc32_combine64_correct`: `crc32_combine(crc32 A, crc32 B, |B|) = crc32 (A ++ B)`. -/
2398theorem crc32_combine_correct (h : Heap) (hs : StaticsOK h) (A B : List UInt8) (len2 : Int64)
2399    (hlen : len2.toInt = B.length) :
2400    C.run (crc32_combine (ZlibF.Spec.crc32 A).toUInt64 (ZlibF.Spec.crc32 B).toUInt64 len2) h =
2401      .ok ((ZlibF.Spec.crc32 (A ++ B)).toUInt64, h) :=
2402  crc32_combine64_correct h hs A B len2 hlen
2403
2404/-- **crc32_combine_op, correctness (with the generator).** For `A`, `B` and `len2 = |B|`: running
2405`crc32_combine_gen(len2)` and then `crc32_combine_op(crc32 A, crc32 B, op)` returns `crc32 (A ++ B)`. -/
2406theorem crc32_combine_op_correct (h : Heap) (hs : StaticsOK h) (A B : List UInt8) (len2 : Int64)
2407    (hlen : len2.toInt = B.length) :
2408    C.run (crc32_combine_gen len2 >>= fun op =>
2409        crc32_combine_op (ZlibF.Spec.crc32 A).toUInt64 (ZlibF.Spec.crc32 B).toUInt64 op) h =
2410      .ok ((ZlibF.Spec.crc32 (A ++ B)).toUInt64, h) :=
2411  crc32_combine64_correct h hs A B len2 hlen
2412
2413/-! ### `crc_word` and the helpers -/
2414
2415/-- **crc_word, safety.** With the static tables of `crc32.h`, `crc_word(data)` does not fault for any 64-bit `data`;
2416heap unchanged. -/
2417theorem crc_word_safe (h : Heap) (hs : StaticsOK h) (data : UInt64) :
2418    ∃ r, C.run (crc_word data) h = .ok (r, h) := ⟨_, crc_word_ok h hs data⟩
2419
2420/-- **crc_word, correctness.** For a register `c` and the eight bytes at `off` of a heap block (read by `loadWord`, little
2421endian), `crc_word(c ^ word)` is the register after those eight bytes: the left fold of `ZlibF.Spec.crcByte`. -/
2422theorem crc_word_correct (h : Heap) (hs : StaticsOK h) (c : UInt32) (blk off : Nat) (bs : Array UInt8)
2423    (hb : h.bytes blk = some bs) (hlen : off + 8 ≤ bs.size) :
2424    C.run (loadWord (.ref (.blk blk) off) >>= fun w => crc_word (c.toUInt64 ^^^ w)) h =
2425      .ok ((((bs.toList.drop off).take 8).foldl ZlibF.Spec.crcByte c), h) := by
2426  have h1 := OkOn.bind (f := fun w => crc_word (c.toUInt64 ^^^ w)) (loadWord_ok h blk off bs hb hlen) (crc_word_ok h hs (c.toUInt64 ^^^
2427    wob bs[off + 0]! bs[off + 1]! bs[off + 2]! bs[off + 3]! bs[off + 4]! bs[off + 5]! bs[off + 6]! bs[off + 7]!))
2428  have h2 : Psi (c.toUInt64 ^^^ wob bs[off + 0]! bs[off + 1]! bs[off + 2]! bs[off + 3]! bs[off + 4]! bs[off + 5]!
2429      bs[off + 6]! bs[off + 7]!) = rbFrom bs c off 8 := Psi_WA c bs off
2430  rw [h2, rbFrom_list bs 8 c off hlen] at h1
2431  exact h1
2432
2433/-- **loadWord, safety.** Reading eight bytes inside a block never faults and leaves the heap unchanged. -/
2434theorem loadWord_safe (h : Heap) (blk off : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
2435    (hlen : off + 8 ≤ bs.size) : ∃ w, C.run (loadWord (.ref (.blk blk) off)) h = .ok (w, h) :=
2436  ⟨_, loadWord_ok h blk off bs hb hlen⟩
2437
2438/-- **crcTab / x2nTab, safety.** Table reads with an index below the table size (256, 32) do not fault. -/
2439theorem crcTab_safe (h : Heap) (hs : StaticsOK h) (i : UInt64) (hi : i.toNat < 256) :
2440    ∃ t, C.run (crcTab i) h = .ok (t, h) := ⟨_, crcTab_ok h hs i hi⟩
2441
2442/-- **x2nTab, safety.** A read of `x2n_table[i]` with `i < 32` does not fault; heap unchanged. -/
2443theorem x2nTab_safe (h : Heap) (hs : StaticsOK h) (i : UInt32) (hi : i.toNat < 32) :
2444    ∃ t, C.run (x2nTab i) h = .ok (t, h) := ⟨_, x2nTab_ok h hs i hi⟩
2445
2446/-- **crcByte, safety.** One table-driven byte step inside a block does not fault, and returns the next register and
2447pointer (`ZlibF.Spec.crcByte`). -/
2448theorem crcByte_safe (h : Heap) (hs : StaticsOK h) (blk o : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
2449    (ho : o < bs.size) (c : UInt32) :
2450    C.run (crcByte c.toUInt64 (.ref (.blk blk) o)) h =
2451      .ok (((ZlibF.Spec.crcByte c bs[o]!).toUInt64, Ptr.ref (BRef.blk blk) (o + 1)), h) :=
2452  crcByte_ok h hs blk o bs hb ho c
2453
2454/-- **wordAt, safety.** Word `i` of a word array inside a block: no fault. -/
2455theorem wordAt_safe (h : Heap) (blk ow i : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
2456    (hlt : ow + 8 * i + 8 ≤ bs.size) : ∃ w, C.run (wordAt (.ref (.blk blk) ow) i) h = .ok (w, h) :=
2457  ⟨_, wordAt_ok h blk ow i bs hb hlt⟩
2458
2459/-- **braidTab, safety.** The braid table lookup for `k < 8` and any word: no fault. -/
2460theorem braidTab_safe (h : Heap) (kn : Nat) (hk : kn < 8) (word : UInt64) :
2461    ∃ t, C.run (braidTab (Int32.ofNat kn) word) h = .ok (t, h) := ⟨_, braidTab_ok h kn hk word⟩
2462
2463/-- **blockLittle, safety.** One block of 5 words (40 bytes) of the braided loop inside a block: no fault. -/
2464theorem blockLittle_safe (h : Heap) (s : BL) (blk ow : Nat) (bs : Array UInt8) (hb : h.bytes blk = some bs)
2465    (hlt : ow + 40 ≤ bs.size) (hw : s.words = .ref (.blk blk) ow) :
2466    ∃ s', C.run (blockLittle s) h = .ok (s', h) := ⟨_, blockLittle_ok h s blk ow bs hb hlt hw⟩
2467
2468/-- **addrOf, raw block case.** The aligned-origin convention retains the offset as its address representative.
2469Static and embedded origins use separate symbolic residues. -/
2470theorem addrOf_safe (h : Heap) (blk off : Nat) :
2471    C.run (addrOf (.ref (.blk blk) off)) h = .ok (UInt64.ofNat off, h) := rfl
2472
2473/-- **shr64, safety.** A shift count below 64 does not fault. -/
2474theorem shr64_safe (h : Heap) (x n : UInt64) (hn : n < 64) : C.run (shr64 x n) h = .ok (x >>> n, h) := by
2475  unfold C.run shr64; rw [ite_eq_left hn]; rfl
2476
2477theorem crc_big_table_size : Crc32H.crc_big_table.size = 256 := by decide +kernel
2478
2479theorem idx1_ok {α : Type} [Inhabited α] (h : Heap) (t : Array α) (i : Nat) (hi : i < t.size) :
2480    OkOn h (idx1 t i) t[i]! := by
2481  unfold idx1
2482  have : t[i]? = some t[i]! := by rw [getElem!_pos t i hi]; simp [hi]
2483  rw [this]
2484  exact OkOn.pure _ _
2485
2486/-- **crc_word_big, safety.** The big-endian word step (dead on the little-endian target, translated for
2487completeness) does not fault for any `data`; heap unchanged. Its correctness is not proved. -/
2488theorem crc_word_big_safe (h : Heap) (data : UInt64) :
2489    ∃ r, C.run (crc_word_big data) h = .ok (r, h) := by
2490  have key : ∃ y, OkOn h (crc_word_big data) y ∧ True := by
2491    unfold crc_word_big
2492    refine OkOn.bind_ex (R := fun _ : UInt64 × Int32 => True) ?_ (fun x _ => ⟨x.1, OkOn.pure _ _, trivial⟩)
2493    refine cwhile_ok (fun cnt s => ∃ i, i + cnt = 8 ∧ s.2 = Int32.ofNat i) (fun _ => True) ?_ ?_ (k := 8)
2494      (s := (data, (0 : Int32))) ⟨0, rfl, rfl⟩ (by show 8 < 2 ^ 64; omega)
2495    · intro cnt s hP
2496      obtain ⟨d, k⟩ := s
2497      obtain ⟨i, hi, hk⟩ := hP
2498      simp only at hk
2499      subst hk
2500      have hc : (Int32.ofNat i < (8 : Int32)) = true := by
2501        rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
2502          rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
2503      have hk : Int32.ofNat i + 1 = Int32.ofNat (i + 1) := by
2504        rcases (by omega : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7) with
2505          rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
2506      have ht := idx1_ok h Crc32H.crc_big_table ((d >>> 56) &&& 0xff).toNat (by
2507        rw [crc_big_table_size]; exact and255_lt _)
2508      refine ⟨(d, Int32.ofNat i), ((d <<< 8) ^^^ Crc32H.crc_big_table[((d >>> 56) &&& 0xff).toNat]!, Int32.ofNat (i + 1)),
2509        ?_, ?_, ⟨i + 1, by omega, rfl⟩⟩
2510      · show OkOn h (pure _) _
2511        simp only [W, hc]
2512        exact OkOn.pure _ _
2513      · show OkOn h (do let t ← idx1 Crc32H.crc_big_table (((d >>> 56) &&& 0xff).toNat); pure ((d <<< 8) ^^^ t, Int32.ofNat i + 1)) _
2514        rw [hk]
2515        exact OkOn.bind ht (OkOn.pure _ _)
2516    · intro s hP
2517      obtain ⟨d, k⟩ := s
2518      obtain ⟨i, hi, hk⟩ := hP
2519      simp only at hk
2520      subst hk
2521      have : i = 8 := by omega
2522      subst this
2523      have hc : (Int32.ofNat 8 < (8 : Int32)) = false := by decide
2524      refine ⟨(d, Int32.ofNat 8), ?_, trivial⟩
2525      show OkOn h (pure _) _
2526      simp only [W, hc]
2527      exact OkOn.pure _ _
2528  obtain ⟨y, hy, _⟩ := key
2529  unfold OkOn at hy
2530  refine ⟨y, ?_⟩
2531  unfold C.run
2532  exact hy
2533
2534/-! ### Non-vacuity: concrete heaps built by `allocBytes`
2535
2536The heap `h0` has the static tables `crc32.c` fixes (`initStatics`); `allocBytes` (the runtime function) puts a buffer in
2537a fresh block; the hypotheses of the theorems hold there and the translated functions run on it. -/
2538
2539/-- the empty heap with the static tables of `crc32.h` -/
2540def h0 : Heap := { Heap.empty with static := Zlib.Crc32.initStatics Heap.empty.static }
2541
2542/-- 100 bytes, enough for the braided path at an unaligned offset -/
2543def buf100 : Array UInt8 := (Array.range 100).map (fun i => UInt8.ofNat (i * 7 + 3))
2544
2545example : StaticsOK h0 := ⟨rfl, rfl⟩
2546
2547/-- `allocBytes` gives a pointer into block 0, in a heap where the hypotheses hold. -/
2548example : ∃ p h1, C.allocBytes buf100 h0 = .ok (p, h1) ∧ p = .ref (.blk 0) 0 ∧ StaticsOK h1 ∧
2549    h1.bytes 0 = some buf100 ∧ 3 + (90 : UInt64).toNat ≤ buf100.size :=
2550  ⟨_, _, rfl, rfl, ⟨rfl, rfl⟩, rfl, by decide +kernel⟩
2551
2552/-- `crc32_z_correct` on a concrete heap: 90 bytes from the unaligned offset 3 (alignment loop, braided loop,
2553tails), value as in the specification. -/
2554example : ∃ p h1, C.allocBytes buf100 h0 = .ok (p, h1) ∧
2555    C.run (crc32_z 0 (.ref (.blk 0) 3) 90) h1 =
2556      .ok ((ZlibF.Spec.crc32Update 0 ((buf100.toList.drop 3).take 90)).toUInt64, h1) :=
2557  ⟨_, _, rfl, crc32_z_correct _ ⟨rfl, rfl⟩ 0 0 3 buf100 rfl 90 (by decide +kernel)⟩
2558
2559/-- the heap after `allocBytes arr` on `h0` -/
2560def heapOf (arr : Array UInt8) : Heap := match C.allocBytes arr h0 with | .ok (_, h1) => h1 | .error _ => h0
2561
2562/-- the value of a run, `0` on a fault -/
2563def valOf (r : Except Fault (UInt64 × Heap)) : UInt64 := match r with | .ok (v, _) => v | .error _ => 0
2564
2565/-- the value computed by running the translation on the 90 bytes from offset 3 equals the specification (an
2566independent check of the theorem on this instance) -/
2567example : valOf (C.run (crc32_z 0 (.ref (.blk 0) 3) 90) (heapOf buf100)) =
2568    (ZlibF.Spec.crc32Update 0 ((buf100.toList.drop 3).take 90)).toUInt64 := by decide +kernel
2569
2570/-- `crc32("123456789") = 0xCBF43926`, by running the translation on a block made by `allocBytes` -/
2571example : valOf (C.run (crc32_z 0 (.ref (.blk 0) 0) 9) (heapOf "123456789".toUTF8.data)) = 0xCBF43926 := by
2572  decide +kernel
2573
2574/-- the same through the theorem: hypotheses hold, the result is the specification's -/
2575example : ∃ p h1, C.allocBytes "123456789".toUTF8.data h0 = .ok (p, h1) ∧
2576    C.run (crc32_z 0 p 9) h1 =
2577      .ok ((ZlibF.Spec.crc32Update 0 (("123456789".toUTF8.data.toList.drop 0).take 9)).toUInt64, h1) :=
2578  ⟨_, _, rfl, crc32_z_correct _ ⟨rfl, rfl⟩ 0 0 0 _ rfl 9 (by decide +kernel)⟩
2579
2580/-- the combine functions on a concrete instance -/
2581example : ∃ h1, StaticsOK h1 ∧
2582    C.run (crc32_combine64 (ZlibF.Spec.crc32 [1, 2, 3]).toUInt64 (ZlibF.Spec.crc32 [4, 5, 6, 7]).toUInt64 4) h1 =
2583      .ok ((ZlibF.Spec.crc32 [1, 2, 3, 4, 5, 6, 7]).toUInt64, h1) :=
2584  ⟨h0, ⟨rfl, rfl⟩, crc32_combine64_correct h0 ⟨rfl, rfl⟩ [1, 2, 3] [4, 5, 6, 7] 4 (by decide)⟩
2585
2586/-- the hang, on the translation -/
2587example : C.run (crc32_combine_op 1 2 ((1 : UInt64) <<< 32)) h0 = .error .outOfFuel :=
2588  crc32_combine_op_diverges h0 1 2 _ (by decide) (by decide)
2589
2590end Zlib.Crc32.Proofs