crc32.c.views.lean

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

1import ZlibF.Spec.Crc32ByteViews
2
3/-!
4# CRC over all represented byte views
5
6The physical loads and pointer updates use the actual byte-array view.
7Alignment observes its arbitrary stable origin residue. The checksum
8algebra is reused without changing the independent CRC definition.
9-/
10
11namespace Zlib.Crc32.Proofs.ViewsProof
12open C Zlib.Crc32.Proofs
13
14private theorem addrOf_ref_ok (h : Heap) (ref : BRef) (offset : Nat) :
15    OkOn h (addrOf (.ref ref offset)) (UInt64.ofNat (ByteAddress.base h ref + offset)) := by
16  cases ref <;> simp [OkOn, addrOf, ByteAddress.address, ByteAddress.value, ByteAddress.base]
17
18theorem idx8 (h : Heap) (ref : BRef) (off i : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs) (hlt : off + i < bs.size) :
19    OkOn h (index8 (.ref ref off) i) bs[off + i]! := by
20  have := Ptr.index_ok hb hlt
21  rw [getElem!_pos bs (off + i) hlt]; exact this
22
23set_option maxRecDepth 4000 in
24theorem loadWord_ok (h : Heap) (ref : BRef) (off : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
25    (hlt : off + 8 ≤ bs.size) :
26    OkOn h (loadWord (.ref ref off))
27      (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
28  unfold loadWord
29  simp only [forIn, Std.Legacy.Range.forIn'_eq_forIn'_range', Std.Legacy.Range.size]
30  simp only [List.range'_succ, List.range'_zero, List.forIn'_cons, List.forIn'_nil]
31  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 _ _)
32  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
33  try dsimp only
34  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
35  try dsimp only
36  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
37  try dsimp only
38  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
39  try dsimp only
40  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
41  try dsimp only
42  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
43  try dsimp only
44  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
45  try dsimp only
46  refine OkOn.bind (x := ForInStep.yield _) (OkOn.bind (idx8 h ref off _ bs hb (by omega)) (OkOn.pure _ _)) ?_
47  try dsimp only
48  exact OkOn.pure _ _
49
50
51theorem wordAt_ok (h : Heap) (ref : BRef) (ow i : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
52    (hlt : ow + 8 * i + 8 ≤ bs.size) :
53    OkOn h (wordAt (.ref ref ow) i) (WA bs (ow + 8 * i)) := by
54  unfold wordAt
55  have hadd : OkOn h (Ptr.add (Ptr.ref ref ow) (8 * (i : Int))) (Ptr.ref ref (ow + 8 * i)) := by
56    have := Ptr.add_ok (r := ref) (off := ow) (k := 8 * (i : Int)) (a := bs) hb (by omega) (by omega)
57    have e : ((ow : Int) + 8 * (i : Int)).toNat = ow + 8 * i := by omega
58    rwa [e] at this
59  exact OkOn.bind hadd (loadWord_ok h ref (ow + 8 * i) bs hb hlt)
60
61
62theorem blockLittle_ok (h : Heap) (s : BL) (ref : BRef) (ow : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
63    (hlt : ow + 40 ≤ bs.size) (hw : s.words = .ref ref ow) :
64    OkOn h (blockLittle s)
65      { crc0 := bw (s.crc0.toUInt64 ^^^ WA bs ow), crc1 := bw (s.crc1.toUInt64 ^^^ WA bs (ow + 8)),
66        crc2 := bw (s.crc2.toUInt64 ^^^ WA bs (ow + 16)), crc3 := bw (s.crc3.toUInt64 ^^^ WA bs (ow + 24)),
67        crc4 := bw (s.crc4.toUInt64 ^^^ WA bs (ow + 32)), words := .ref ref (ow + 40), blks := s.blks } := by
68  have w0 := wordAt_ok h ref ow 0 bs hb (by omega)
69  have w1 := wordAt_ok h ref ow 1 bs hb (by omega)
70  have w2 := wordAt_ok h ref ow 2 bs hb (by omega)
71  have w3 := wordAt_ok h ref ow 3 bs hb (by omega)
72  have w4 := wordAt_ok h ref ow 4 bs hb (by omega)
73  simp only [Nat.mul_zero, Nat.add_zero] at w0
74  have hadd : OkOn h (Ptr.add s.words 40) (Ptr.ref ref (ow + 40)) := by
75    rw [hw]
76    have := Ptr.add_nat_ok (r := ref) (off := ow) (n := 40) (a := bs) hb hlt
77    simpa using this
78  rw [← hw] at w0 w1 w2 w3 w4
79  unfold blockLittle
80  refine OkOn.bind w0 ?_
81  try dsimp only
82  refine OkOn.bind w1 ?_
83  try dsimp only
84  refine OkOn.bind w2 ?_
85  try dsimp only
86  refine OkOn.bind w3 ?_
87  try dsimp only
88  refine OkOn.bind w4 ?_
89  try dsimp only
90  refine OkOn.bind hadd ?_
91  try dsimp only
92  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
93  try dsimp only
94  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
95  try dsimp only
96  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
97  try dsimp only
98  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
99  try dsimp only
100  refine OkOn.bind (braidTab_ok h 0 (by omega) _) ?_
101  try dsimp only
102  generalize hW0 : s.crc0.toUInt64 ^^^ WA bs (ow + 8 * 0) = W0
103  generalize hW1 : s.crc1.toUInt64 ^^^ WA bs (ow + 8 * 1) = W1
104  generalize hW2 : s.crc2.toUInt64 ^^^ WA bs (ow + 8 * 2) = W2
105  generalize hW3 : s.crc3.toUInt64 ^^^ WA bs (ow + 8 * 3) = W3
106  generalize hW4 : s.crc4.toUInt64 ^^^ WA bs (ow + 8 * 4) = W4
107  refine bind_of (fun s => s = (bw W0, bw W1, bw W2, bw W3, bw W4, Int32.ofNat 8)) ?_ ?_
108  · refine cwhile_ok (fun cnt s => ∃ m, m + cnt = 8 ∧ 1 ≤ m ∧
109        s = (psum W0 m, psum W1 m, psum W2 m, psum W3 m, psum W4 m, Int32.ofNat m))
110      (fun s => s = (bw W0, bw W1, bw W2, bw W3, bw W4, Int32.ofNat 8)) ?_ ?_ (k := 7)
111      (s := (pw (8 * (40 - 0)) (bx W0 0), pw (8 * (40 - 0)) (bx W1 0), pw (8 * (40 - 0)) (bx W2 0),
112        pw (8 * (40 - 0)) (bx W3 0), pw (8 * (40 - 0)) (bx W4 0), 1)) ?_ ?_
113    · intro cnt s hP
114      obtain ⟨m, hm, hm1, rfl⟩ := hP
115      have hc : (Int32.ofNat m < W) = true := by
116        rcases (by omega : m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5 ∨ m = 6 ∨ m = 7) with
117          rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
118      have hk : Int32.ofNat m + 1 = Int32.ofNat (m + 1) := by
119        rcases (by omega : m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5 ∨ m = 6 ∨ m = 7) with
120          rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
121      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),
122        Int32.ofNat (m + 1)), ?_, ?_, ⟨m + 1, by omega, by omega, rfl⟩⟩
123      · show OkOn h (pure _) _
124        simp only [hc]
125        exact OkOn.pure _ _
126      · show OkOn h (do
127          let a0 ← braidTab (Int32.ofNat m) W0
128          let a1 ← braidTab (Int32.ofNat m) W1
129          let a2 ← braidTab (Int32.ofNat m) W2
130          let a3 ← braidTab (Int32.ofNat m) W3
131          let a4 ← braidTab (Int32.ofNat m) W4
132          pure (psum W0 m ^^^ a0, psum W1 m ^^^ a1, psum W2 m ^^^ a2, psum W3 m ^^^ a3, psum W4 m ^^^ a4,
133            Int32.ofNat m + 1)) _
134        rw [hk]
135        exact OkOn.bind (braidTab_ok h m (by omega) _) (OkOn.bind (braidTab_ok h m (by omega) _)
136          (OkOn.bind (braidTab_ok h m (by omega) _) (OkOn.bind (braidTab_ok h m (by omega) _)
137          (OkOn.bind (braidTab_ok h m (by omega) _) (OkOn.pure _ _)))))
138    · intro s hP
139      obtain ⟨m, hm, hm1, rfl⟩ := hP
140      have : m = 8 := by omega
141      subst this
142      have hc : (Int32.ofNat 8 < W) = false := by decide
143      refine ⟨_, ?_, rfl⟩
144      · show OkOn h (pure _) _
145        simp only [hc]
146        exact OkOn.pure _ _
147    · exact ⟨1, by omega, Nat.le_refl _, by simp [psum]⟩
148    · show 7 < 2 ^ 64; omega
149  · intro x hx
150    subst hx
151    exact OkOn.pure _ _
152
153
154theorem crcByte_ok (h : Heap) (hs : StaticsOK h) (ref : BRef) (o : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
155    (ho : o < bs.size) (c : UInt32) :
156    OkOn h (crcByte c.toUInt64 (.ref ref o))
157      ((ZlibF.Spec.crcByte c bs[o]!).toUInt64, Ptr.ref ref (o + 1)) := by
158  unfold crcByte
159  have hl := Ptr.load_ok hb ho
160  have hadd := Ptr.add_nat_ok (r := ref) (off := o) (n := 1) (a := bs) hb (by omega)
161  have ht := crcTab_ok h hs ((c.toUInt64 ^^^ bs[o].toUInt64) &&& 0xff) (and255_lt _)
162  have e : ((c.toUInt64 >>> 8) ^^^ Crc32H.crc_table[((c.toUInt64 ^^^ bs[o].toUInt64) &&& 0xff).toNat]!.toUInt64) =
163      (ZlibF.Spec.crcByte c bs[o]).toUInt64 := by
164    have := wstep_u32 (c ^^^ bs[o].toUInt32)
165    rw [UInt32.toUInt64_xor, u8_u32_u64] at this
166    unfold wstep at this
167    have h8 : bs[o].toUInt64 >>> 8 = 0 := by
168      apply UInt64.toNat_inj.mp
169      rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
170      have := UInt8.toNat_lt bs[o]
171      simp
172      omega
173    rw [UInt64.shiftRight_xor, h8, UInt64.xor_zero] at this
174    rw [crcByte_eq, this]
175  rw [getElem!_pos bs o ho]
176  rw [← e]
177  exact OkOn.bind hl (OkOn.bind hadd (OkOn.bind ht (OkOn.pure _ _)))
178
179
180theorem body1_ok (h : Heap) (hs : StaticsOK h) (ref : BRef) (o : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
181    (ho : o < bs.size) (c : UInt32) (l : UInt64) :
182    OkOn h (body1 (c.toUInt64, .ref ref o, l))
183      ((ZlibF.Spec.crcByte c bs[o]!).toUInt64, Ptr.ref ref (o + 1), l - 1) := by
184  unfold body1
185  exact OkOn.bind (crcByte_ok h hs ref o bs hb ho c) (OkOn.pure _ _)
186
187theorem body8_ok (h : Heap) (hs : StaticsOK h) (ref : BRef) (o : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
188    (ho : o + 8 ≤ bs.size) (c : UInt32) (l : UInt64) :
189    OkOn h (body8 (c.toUInt64, .ref ref o, l))
190      ((rbFrom bs c o 8).toUInt64, Ptr.ref ref (o + 8), l - 8) := by
191  unfold body8
192  refine OkOn.bind (crcByte_ok h hs ref o bs hb (by omega) c) ?_
193  refine OkOn.bind (crcByte_ok h hs ref (o + 1) bs hb (by omega) _) ?_
194  refine OkOn.bind (crcByte_ok h hs ref (o + 1 + 1) bs hb (by omega) _) ?_
195  refine OkOn.bind (crcByte_ok h hs ref (o + 1 + 1 + 1) bs hb (by omega) _) ?_
196  refine OkOn.bind (crcByte_ok h hs ref (o + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
197  refine OkOn.bind (crcByte_ok h hs ref (o + 1 + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
198  refine OkOn.bind (crcByte_ok h hs ref (o + 1 + 1 + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
199  refine OkOn.bind (crcByte_ok h hs ref (o + 1 + 1 + 1 + 1 + 1 + 1 + 1) bs hb (by omega) _) ?_
200  exact OkOn.pure _ _
201
202
203theorem loop1_ok (h : Heap) (hs : StaticsOK h) (ref : BRef) (o L : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
204    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (c : UInt32) :
205    OkOn h (cwhile cond1 body1 (c.toUInt64, .ref ref o, UInt64.ofNat L))
206      ((rbFrom bs c o L).toUInt64, Ptr.ref ref (o + L), 0) := by
207  suffices H : ∃ s, OkOn h (cwhile cond1 body1 (c.toUInt64, .ref ref o, UInt64.ofNat L)) s ∧
208      s = ((rbFrom bs c o L).toUInt64, Ptr.ref ref (o + L), 0) by
209    obtain ⟨s, hs', rfl⟩ := H; exact hs'
210  refine cwhile_ok (fun k s => ∃ j, j + k = L ∧
211      s = ((rbFrom bs c o j).toUInt64, Ptr.ref ref (o + j), UInt64.ofNat (L - j))) _ ?_ ?_ (k := L)
212    (s := (c.toUInt64, .ref ref o, UInt64.ofNat L)) ⟨0, by omega, by simp [rbFrom_zero]⟩ hL
213  · intro k s hP
214    obtain ⟨j, hj, rfl⟩ := hP
215    have hne : (UInt64.ofNat (L - j) != 0) = true := by
216      have : UInt64.ofNat (L - j) ≠ 0 := by
217        intro h0
218        have := congrArg UInt64.toNat h0
219        rw [ofNat_toNat_lt _ (by omega)] at this
220        have h1 : (0 : UInt64).toNat = 0 := rfl
221        omega
222      simpa using this
223    refine ⟨((rbFrom bs c o j).toUInt64, Ptr.ref ref (o + j), UInt64.ofNat (L - j)), ((ZlibF.Spec.crcByte (rbFrom bs c o j) bs[o + j]!).toUInt64, Ptr.ref ref (o + j + 1),
224      UInt64.ofNat (L - j) - 1), ?_, ?_, ?_⟩
225    · show OkOn h (pure _) _
226      simp only [hne]
227      exact OkOn.pure _ _
228    · exact body1_ok h hs ref (o + j) bs hb (by omega) _ _
229    · refine ⟨j + 1, by omega, ?_⟩
230      rw [rbFrom_snoc, show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
231      rw [show L - j - 1 = L - (j + 1) by omega]
232      rfl
233  · intro s hP
234    obtain ⟨j, hj, rfl⟩ := hP
235    have hjL : L = j := by omega
236    subst hjL
237    refine ⟨((rbFrom bs c o L).toUInt64, Ptr.ref ref (o + L), UInt64.ofNat (L - L)), ?_, ?_⟩
238    · show OkOn h (pure _) _
239      simp only [Nat.sub_self]
240      exact OkOn.pure _ _
241    · simp [Nat.sub_self]
242
243theorem loop8_ok (h : Heap) (hs : StaticsOK h) (ref : BRef) (o L : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
244    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (c : UInt32) :
245    OkOn h (cwhile cond8 body8 (c.toUInt64, .ref ref o, UInt64.ofNat L))
246      ((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref ref (o + 8 * (L / 8)),
247        UInt64.ofNat (L - 8 * (L / 8))) := by
248  suffices H : ∃ s, OkOn h (cwhile cond8 body8 (c.toUInt64, .ref ref o, UInt64.ofNat L)) s ∧
249      s = ((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref ref (o + 8 * (L / 8)),
250        UInt64.ofNat (L - 8 * (L / 8))) by
251    obtain ⟨s, hs', rfl⟩ := H; exact hs'
252  refine cwhile_ok (fun k s => ∃ j, j + k = L / 8 ∧
253      s = ((rbFrom bs c o (8 * j)).toUInt64, Ptr.ref ref (o + 8 * j), UInt64.ofNat (L - 8 * j))) _ ?_ ?_
254    (k := L / 8) (s := (c.toUInt64, .ref ref o, UInt64.ofNat L)) ⟨0, by omega, by simp [rbFrom_zero]⟩
255    (by show L / 8 < 2 ^ 64; omega)
256  · intro k s hP
257    obtain ⟨j, hj, rfl⟩ := hP
258    have hge : (decide (UInt64.ofNat (L - 8 * j) ≥ 8)) = true := by
259      simp only [decide_eq_true_eq, ge_iff_le, UInt64.le_iff_toNat_le]
260      rw [ofNat_toNat_lt _ (by omega)]
261      have : (8 : UInt64).toNat = 8 := rfl
262      omega
263    refine ⟨((rbFrom bs c o (8 * j)).toUInt64, Ptr.ref ref (o + 8 * j), UInt64.ofNat (L - 8 * j)),
264      ((rbFrom bs (rbFrom bs c o (8 * j)) (o + 8 * j) 8).toUInt64, Ptr.ref ref (o + 8 * j + 8),
265        UInt64.ofNat (L - 8 * j) - 8), ?_, ?_, ?_⟩
266    · show OkOn h (pure _) _
267      simp only [hge]
268      exact OkOn.pure _ _
269    · exact body8_ok h hs ref (o + 8 * j) bs hb (by omega) _ _
270    · refine ⟨j + 1, by omega, ?_⟩
271      rw [show 8 * (j + 1) = 8 * j + 8 by omega, rbFrom_add,
272        show (8 : UInt64) = UInt64.ofNat 8 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
273      rw [show L - 8 * j - 8 = L - (8 * j + 8) by omega]
274      rfl
275  · intro s hP
276    obtain ⟨j, hj, rfl⟩ := hP
277    have hjq : j = L / 8 := by omega
278    have hlt : (decide (UInt64.ofNat (L - 8 * j) ≥ 8)) = false := by
279      simp only [decide_eq_false_iff_not, ge_iff_le, UInt64.le_iff_toNat_le, Nat.not_le]
280      rw [ofNat_toNat_lt _ (by omega)]
281      have : (8 : UInt64).toNat = 8 := rfl
282      omega
283    subst hjq
284    refine ⟨((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref ref (o + 8 * (L / 8)),
285      UInt64.ofNat (L - 8 * (L / 8))), ?_, rfl⟩
286    show OkOn h (pure _) _
287    simp only [hlt]
288    exact OkOn.pure _ _
289
290theorem tail_ok (h : Heap) (hs : StaticsOK h) (ref : BRef) (o L : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
291    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (c : UInt32) :
292    OkOn h (tailP c.toUInt64 (.ref ref o) (UInt64.ofNat L)) ((rbFrom bs c o L).toUInt64 ^^^ 0xffffffff) := by
293  unfold tailP
294  refine bind_of (fun x => x = ((rbFrom bs c o (8 * (L / 8))).toUInt64, Ptr.ref ref (o + 8 * (L / 8)),
295        UInt64.ofNat (L - 8 * (L / 8)))) ⟨_, loop8_ok h hs ref o L bs hb hle hL c, rfl⟩ ?_
296  intro x hx
297  subst hx
298  show OkOn h (cwhile cond1 body1 _ >>= _) _
299  refine bind_of (fun x => x = ((rbFrom bs (rbFrom bs c o (8 * (L / 8))) (o + 8 * (L / 8)) (L - 8 * (L / 8))).toUInt64,
300      Ptr.ref ref (o + 8 * (L / 8) + (L - 8 * (L / 8))), 0))
301    ⟨_, loop1_ok h hs ref (o + 8 * (L / 8)) (L - 8 * (L / 8)) bs hb (by omega) (by omega) _, rfl⟩ ?_
302  intro x hx
303  subst hx
304  rw [← rbFrom_add]
305  rw [show 8 * (L / 8) + (L - 8 * (L / 8)) = L by omega]
306  exact OkOn.pure _ _
307
308
309theorem loopA_ok (h : Heap) (ref : BRef) (o L : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
310    (hle : o + L ≤ bs.size) (hL : L < 2 ^ 64) (h8 : 8 ≤ L) (hs : StaticsOK h) (c : UInt32) :
311    OkOn h (cwhile condA bodyA (c.toUInt64, .ref ref o, UInt64.ofNat L))
312      ((rbFrom bs c o (alignLen (ByteAddress.base h ref + o))).toUInt64, Ptr.ref ref (o + alignLen (ByteAddress.base h ref + o)),
313        UInt64.ofNat (L - alignLen (ByteAddress.base h ref + o))) := by
314  suffices H : ∃ s, OkOn h (cwhile condA bodyA (c.toUInt64, .ref ref o, UInt64.ofNat L)) s ∧
315      s = ((rbFrom bs c o (alignLen (ByteAddress.base h ref + o))).toUInt64, Ptr.ref ref (o + alignLen (ByteAddress.base h ref + o)),
316        UInt64.ofNat (L - alignLen (ByteAddress.base h ref + o))) by
317    obtain ⟨s, hs', rfl⟩ := H; exact hs'
318  have ha7 : alignLen (ByteAddress.base h ref + o) ≤ 7 := by unfold alignLen; omega
319  have hcondA : ∀ j, j ≤ alignLen (ByteAddress.base h ref + o) →
320      OkOn h (condA ((rbFrom bs c o j).toUInt64, Ptr.ref ref (o + j), UInt64.ofNat (L - j)))
321        (decide (j < alignLen (ByteAddress.base h ref + o)), (rbFrom bs c o j).toUInt64, Ptr.ref ref (o + j), UInt64.ofNat (L - j)) := by
322    intro j hj
323    have hne : (UInt64.ofNat (L - j) == 0) = false := by
324      have : UInt64.ofNat (L - j) ≠ 0 := by
325        intro h0
326        have := congrArg UInt64.toNat h0
327        rw [ofNat_toNat_lt _ (by omega)] at this
328        have h1 : (0 : UInt64).toNat = 0 := rfl
329        omega
330      simpa using this
331    have hmod : decide ((UInt64.ofNat (ByteAddress.base h ref + o + j) &&& 7) ≠ 0) = decide (j < alignLen (ByteAddress.base h ref + o)) := by
332      have h1 : (UInt64.ofNat (ByteAddress.base h ref + o + j) &&& 7).toNat = (ByteAddress.base h ref + o + j) % 8 := and7 _
333      by_cases hj' : j < alignLen (ByteAddress.base h ref + o)
334      · have : (UInt64.ofNat (ByteAddress.base h ref + o + j) &&& 7) ≠ 0 := by
335          intro h0; rw [h0] at h1
336          have h2 : (0 : UInt64).toNat = 0 := rfl
337          unfold alignLen at hj'; omega
338        rw [decide_eq_true this, decide_eq_true hj']
339      · have : (UInt64.ofNat (ByteAddress.base h ref + o + j) &&& 7) = 0 := by
340          apply UInt64.toNat_inj.mp
341          have h2 : (0 : UInt64).toNat = 0 := rfl
342          rw [h1, h2]; unfold alignLen at hj hj'; omega
343        rw [decide_eq_false (by rw [this]; simp), decide_eq_false hj']
344    unfold condA
345    dsimp only
346    rw [ite_eq_right (by simp [hne])]
347    show OkOn h (addrOf (Ptr.ref ref (o + j)) >>= _) _
348    refine OkOn.bind (x := UInt64.ofNat (ByteAddress.base h ref + o + j)) (by simpa only [Nat.add_assoc] using addrOf_ref_ok h ref (o + j)) ?_
349    rw [W_pred]
350    show OkOn h (pure _) _
351    have hb : ((UInt64.ofNat (ByteAddress.base h ref + o + j) &&& 7) != 0) = decide (j < alignLen (ByteAddress.base h ref + o)) := by
352      rw [← hmod]
353      generalize UInt64.ofNat (ByteAddress.base h ref + o + j) &&& 7 = x
354      by_cases hx : x = 0 <;> simp [hx]
355    rw [hb]
356    exact OkOn.pure _ _
357  refine cwhile_ok (fun k s => ∃ j, j + k = alignLen (ByteAddress.base h ref + o) ∧
358      s = ((rbFrom bs c o j).toUInt64, Ptr.ref ref (o + j), UInt64.ofNat (L - j))) _ ?_ ?_
359    (k := alignLen (ByteAddress.base h ref + o)) (s := (c.toUInt64, .ref ref o, UInt64.ofNat L)) ⟨0, by omega, by simp [rbFrom_zero]⟩
360    (by show alignLen (ByteAddress.base h ref + o) < 2 ^ 64; omega)
361  · intro k s hP
362    obtain ⟨j, hj, rfl⟩ := hP
363    refine ⟨((rbFrom bs c o j).toUInt64, Ptr.ref ref (o + j), UInt64.ofNat (L - j)),
364      ((ZlibF.Spec.crcByte (rbFrom bs c o j) bs[o + j]!).toUInt64, Ptr.ref ref (o + j + 1),
365      UInt64.ofNat (L - j) - 1), ?_, ?_, ?_⟩
366    · have := hcondA j (by omega)
367      rwa [show decide (j < alignLen (ByteAddress.base h ref + o)) = true by simp; omega] at this
368    · exact body1_ok h hs ref (o + j) bs hb (by omega) _ _
369    · refine ⟨j + 1, by omega, ?_⟩
370      rw [rbFrom_snoc, show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
371      rw [show L - j - 1 = L - (j + 1) by omega]
372      rfl
373  · intro s hP
374    obtain ⟨j, hj, rfl⟩ := hP
375    have hjL : alignLen (ByteAddress.base h ref + o) = j := by omega
376    subst hjL
377    refine ⟨((rbFrom bs c o (alignLen (ByteAddress.base h ref + o))).toUInt64, Ptr.ref ref (o + alignLen (ByteAddress.base h ref + o)),
378      UInt64.ofNat (L - alignLen (ByteAddress.base h ref + o))), ?_, rfl⟩
379    have := hcondA (alignLen (ByteAddress.base h ref + o)) (Nat.le_refl _)
380    simpa using this
381
382
383theorem loopBlk_ok (h : Heap) (ref : BRef) (o1 B : Nat) (bs : Array UInt8) (hb : Space.get h ref = some bs)
384    (hB : 1 ≤ B) (hle : o1 + 40 * B ≤ bs.size) (hB64 : B < 2 ^ 64) (c : UInt32) :
385    ∃ s : BL, OkOn h (cwhile condBlk blockLittle
386        { crc0 := c, crc1 := 0, crc2 := 0, crc3 := 0, crc4 := 0, words := (.ref ref o1 : BPtr), blks := UInt64.ofNat B }) s ∧
387      Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 = pw 320 (rbFrom bs c o1 (40 * (B - 1))) ∧
388      s.words = .ref ref (o1 + 40 * (B - 1)) := by
389  refine cwhile_ok (cond := condBlk) (body := blockLittle) (fun k s => ∃ j, j + k = B - 1 ∧ s.words = .ref ref (o1 + 40 * j) ∧
390      s.blks = UInt64.ofNat (B - j) ∧
391      Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 = pw 320 (rbFrom bs c o1 (40 * j)))
392    (fun s => Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 = pw 320 (rbFrom bs c o1 (40 * (B - 1))) ∧
393      s.words = .ref ref (o1 + 40 * (B - 1))) ?_ ?_ (k := B - 1)
394    (s := { crc0 := c, crc1 := 0, crc2 := 0, crc3 := 0, crc4 := 0, words := (.ref ref o1 : BPtr), blks := UInt64.ofNat B }) ?_ (by show B - 1 < 2 ^ 64; omega)
395  · intro k s hP
396    obtain ⟨c0, c1, c2, c3, c4, words, blks⟩ := s
397    obtain ⟨j, hj, hw, hbl, hV⟩ := hP
398    simp only at hw hbl hV
399    subst hw hbl
400    have hne : (UInt64.ofNat (B - j) - 1 != 0) = true := by
401      rw [show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
402      have : UInt64.ofNat (B - j - 1) ≠ 0 := by
403        intro h0
404        have := congrArg UInt64.toNat h0
405        rw [ofNat_toNat_lt _ (by omega)] at this
406        have h1 : (0 : UInt64).toNat = 0 := rfl
407        omega
408      simpa using this
409    let s1 : BL := { crc0 := c0, crc1 := c1, crc2 := c2, crc3 := c3, crc4 := c4,
410                     words := (.ref ref (o1 + 40 * j) : BPtr), blks := UInt64.ofNat (B - j) - 1 }
411    have hbk := blockLittle_ok h s1 ref (o1 + 40 * j) bs hb (by omega) rfl
412    refine ⟨s1, _, ?_, hbk, ?_⟩
413    · show OkOn h (pure _) _
414      simp only [hne]
415      exact OkOn.pure _ _
416    · refine ⟨j + 1, by omega, rfl, ?_, ?_⟩
417      · show UInt64.ofNat (B - j) - 1 = UInt64.ofNat (B - (j + 1))
418        rw [show (1 : UInt64) = UInt64.ofNat 1 from rfl, ofNat_sub64 _ _ (by omega) (by omega)]
419        rfl
420      · show Val (bw (c0.toUInt64 ^^^ WA bs (o1 + 40 * j))) (bw (c1.toUInt64 ^^^ WA bs (o1 + 40 * j + 8)))
421          (bw (c2.toUInt64 ^^^ WA bs (o1 + 40 * j + 16))) (bw (c3.toUInt64 ^^^ WA bs (o1 + 40 * j + 24)))
422          (bw (c4.toUInt64 ^^^ WA bs (o1 + 40 * j + 32))) = _
423        rw [bw_Psi, bw_Psi, bw_Psi, bw_Psi, bw_Psi, val_inv bs c0 c1 c2 c3 c4 _ _ hV]
424        rw [show 40 * (j + 1) = 40 * j + 40 by omega, rbFrom_add]
425  · intro s hP
426    obtain ⟨c0, c1, c2, c3, c4, words, blks⟩ := s
427    obtain ⟨j, hj, hw, hbl, hV⟩ := hP
428    simp only at hw hbl hV
429    subst hw hbl
430    have hjB : j = B - 1 := by omega
431    subst hjB
432    have hz : (UInt64.ofNat (B - (B - 1)) - 1 != 0) = false := by
433      rw [show B - (B - 1) = 1 by omega]
434      decide
435    refine ⟨{ crc0 := c0, crc1 := c1, crc2 := c2, crc3 := c3, crc4 := c4,
436              words := (.ref ref (o1 + 40 * (B - 1)) : BPtr), blks := UInt64.ofNat (B - (B - 1)) - 1 }, ?_, hV, rfl⟩
437    show OkOn h (pure _) _
438    simp only [hz]
439    exact OkOn.pure _ _
440  · refine ⟨0, by omega, rfl, rfl, ?_⟩
441    simp [Val, rbFrom_zero, pw_zero]
442
443
444theorem crc32_z_ok (h : Heap) (hs : StaticsOK h) (crc : UInt64) (ref : BRef) (off : Nat) (bs : Array UInt8)
445    (hb : Space.get h ref = some bs) (len : UInt64) (hlen : off + len.toNat ≤ bs.size) :
446    OkOn h (crc32_z crc (.ref ref off) len)
447      ((rbFrom bs (~~~ crc.toUInt32) off len.toNat).toUInt64 ^^^ 0xffffffff) := by
448  have hlen' : len = UInt64.ofNat len.toNat := UInt64.ofNat_toNat.symm
449  have hL : len.toNat < 2 ^ 64 := UInt64.toNat_lt len
450  generalize len.toNat = L at hlen' hlen hL ⊢
451  subst hlen'
452  unfold crc32_z
453  rw [ite_eq_right (by simp)]
454  dsimp only
455  rw [crc_init]
456  by_cases hlong : 47 ≤ L
457  · rw [ite_eq_left (by rw [NWW_val]; exact (ge47 L hL).mpr hlong)]
458    have ha7 : alignLen (ByteAddress.base h ref + off) ≤ 7 := by unfold alignLen; omega
459    refine bind_of (fun x => x = ((rbFrom bs (~~~ crc.toUInt32) off (alignLen (ByteAddress.base h ref + off))).toUInt64,
460      Ptr.ref ref (off + alignLen (ByteAddress.base h ref + off)), UInt64.ofNat (L - alignLen (ByteAddress.base h ref + off))))
461      ⟨_, loopA_ok h ref off L bs hb hlen hL (by omega) hs _, rfl⟩ ?_
462    intro x hx
463    subst hx
464    dsimp only
465    rw [NW_val]
466    rw [ite_eq_left (by decide), u32_roundtrip]
467    have hB1 : 1 ≤ (L - alignLen (ByteAddress.base h ref + off)) / 40 := by omega
468    have hBle : off + alignLen (ByteAddress.base h ref + off) + 40 * ((L - alignLen (ByteAddress.base h ref + off)) / 40) ≤ bs.size := by omega
469    have hdiv : UInt64.ofNat (L - alignLen (ByteAddress.base h ref + off)) / 40 = UInt64.ofNat ((L - alignLen (ByteAddress.base h ref + off)) / 40) := by
470      rw [show (40 : UInt64) = UInt64.ofNat 40 from rfl, ofNat_div64 _ _ (by omega) (by omega) (by omega)]
471    have hrem : UInt64.ofNat (L - alignLen (ByteAddress.base h ref + off)) - UInt64.ofNat ((L - alignLen (ByteAddress.base h ref + off)) / 40) * 40 =
472        UInt64.ofNat (L - alignLen (ByteAddress.base h ref + off) - (L - alignLen (ByteAddress.base h ref + off)) / 40 * 40) := by
473      rw [show (40 : UInt64) = UInt64.ofNat 40 from rfl, ofNat_mul64 _ _ (by omega) (by omega) (by omega),
474        ofNat_sub64 _ _ (by omega) (by omega)]
475    rw [hdiv, hrem]
476    refine bind_of (fun s : BL => Val s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 =
477        pw 320 (rbFrom bs (rbFrom bs (~~~ crc.toUInt32) off (alignLen (ByteAddress.base h ref + off))) (off + alignLen (ByteAddress.base h ref + off))
478          (40 * ((L - alignLen (ByteAddress.base h ref + off)) / 40 - 1))) ∧
479        s.words = .ref ref (off + alignLen (ByteAddress.base h ref + off) + 40 * ((L - alignLen (ByteAddress.base h ref + off)) / 40 - 1)))
480      (loopBlk_ok h ref (off + alignLen (ByteAddress.base h ref + off)) ((L - alignLen (ByteAddress.base h ref + off)) / 40) bs hb hB1 hBle (by omega) _) ?_
481    intro s hR
482    obtain ⟨hV, hw⟩ := hR
483    rw [hw]
484    generalize hA : alignLen (ByteAddress.base h ref + off) = a at ha7 hB1 hBle hdiv hrem hV hw ⊢
485    generalize hB : (L - a) / 40 = B at hB1 hBle hdiv hrem hV hw ⊢
486    generalize hc' : rbFrom bs (~~~crc.toUInt32) off a = c' at hV ⊢
487    generalize how : off + a + 40 * (B - 1) = ow at hV hw ⊢
488    have w0 := wordAt_ok h ref ow 0 bs hb (by omega)
489    have w1 := wordAt_ok h ref ow 1 bs hb (by omega)
490    have w2 := wordAt_ok h ref ow 2 bs hb (by omega)
491    have w3 := wordAt_ok h ref ow 3 bs hb (by omega)
492    have w4 := wordAt_ok h ref ow 4 bs hb (by omega)
493    have hadd : OkOn h (Ptr.add (Ptr.ref ref ow) 40) (Ptr.ref ref (ow + 40)) := by
494      have := Ptr.add_nat_ok (r := ref) (off := ow) (n := 40) (a := bs) hb (by omega)
495      simpa using this
496    have e1 : ∀ (a b : UInt32) (W : UInt64), a.toUInt64 ^^^ W ^^^ b.toUInt64 = (a ^^^ b).toUInt64 ^^^ W := by
497      intro a b W; rw [UInt32.toUInt64_xor]; ac_rfl
498    refine OkOn.bind w0 ?_
499    refine OkOn.bind (crc_word_ok h hs _) ?_
500    rw [Psi_WA]
501    refine OkOn.bind w1 ?_
502    rw [e1]
503    refine OkOn.bind (crc_word_ok h hs _) ?_
504    rw [Psi_WA]
505    refine OkOn.bind w2 ?_
506    rw [e1]
507    refine OkOn.bind (crc_word_ok h hs _) ?_
508    rw [Psi_WA]
509    refine OkOn.bind w3 ?_
510    rw [e1]
511    refine OkOn.bind (crc_word_ok h hs _) ?_
512    rw [Psi_WA]
513    refine OkOn.bind w4 ?_
514    rw [e1]
515    refine OkOn.bind (crc_word_ok h hs _) ?_
516    rw [Psi_WA]
517    refine OkOn.bind hadd ?_
518    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)
519        (ow + 8 * 1) 8) (ow + 8 * 2) 8) (ow + 8 * 3) 8) (ow + 8 * 4) 8 = rbFrom bs c' (off + a) (40 * B) := by
520      have h1 := chain_aff bs s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 ow
521      rw [hV, chain_zero] at h1
522      change chain bs s.crc0 s.crc1 s.crc2 s.crc3 s.crc4 ow = _
523      rw [h1, ← rbFrom_aff bs 40 _ ow, ← how, ← rbFrom_add]
524      congr 1; omega
525    have hall : rbFrom bs c' (off + a) (40 * B + (L - a - B * 40)) = rbFrom bs (~~~crc.toUInt32) off L := by
526      rw [← hc']
527      have := rbFrom_add bs a (L - a) (~~~crc.toUInt32) off
528      rw [show a + (L - a) = L by omega] at this
529      rw [this, hc', show 40 * B + (L - a - B * 40) = L - a by omega]
530    rw [hx4]
531    rw [rbFrom_add, show off + a + 40 * B = ow + 40 by omega] at hall
532    rw [← hall]
533    exact tail_ok h hs ref (ow + 40) (L - a - B * 40) bs hb (by omega) (by omega) _
534  · rw [ite_eq_right (by rw [NWW_val]; exact fun hh => hlong ((ge47 L hL).mp hh))]
535    exact tail_ok h hs ref off L bs hb hlen hL _
536
537
538theorem crc32_z_correct (h : Heap) (hs : StaticsOK h) (crc : UInt64) (ref : BRef) (off : Nat) (bs : Array UInt8)
539    (hb : Space.get h ref = some bs) (len : UInt64) (hlen : off + len.toNat ≤ bs.size) :
540    C.run (crc32_z crc (.ref ref off) len) h =
541      .ok (((ZlibF.Spec.crc32Update crc.toUInt32 ((bs.toList.drop off).take len.toNat))).toUInt64, h) := by
542  have := crc32_z_ok h hs crc ref off bs hb len hlen
543  unfold OkOn at this
544  unfold C.run
545  rw [this, rbFrom_list bs len.toNat _ off hlen]
546  have e1 : ZlibF.Spec.crc32Update crc.toUInt32 ((bs.toList.drop off).take len.toNat) =
547      ~~~ rbl (~~~ crc.toUInt32) ((bs.toList.drop off).take len.toNat) := rfl
548  rw [e1, not32_toUInt64]
549
550
551theorem crc32_correct (h : Heap) (hs : StaticsOK h) (crc : UInt64) (ref : BRef) (off : Nat) (bs : Array UInt8)
552    (hb : Space.get h ref = some bs) (len : UInt32) (hlen : off + len.toNat ≤ bs.size) :
553    C.run (crc32 crc (.ref ref off) len) h =
554      .ok (((ZlibF.Spec.crc32Update crc.toUInt32 ((bs.toList.drop off).take len.toNat))).toUInt64, h) := by
555  have := crc32_z_correct h hs crc ref off bs hb len.toUInt64 (by rwa [UInt32.toNat_toUInt64])
556  rw [UInt32.toNat_toUInt64] at this
557  exact this
558
559end Zlib.Crc32.Proofs.ViewsProof
560
561namespace Zlib.Crc32.Proofs
562open C
563
564/-- `uLong crc32_z(uLong crc, const unsigned char *buf, z_size_t len)`.
565The exact general-view goal includes every represented origin residue and
566leaves all heap fields unchanged. -/
567theorem crc32_z_all_byte_views : Spec.ByteViews.Goal.crc32_z_all_byte_views := by
568  intro h hs crc ref offset bytes hg len readable
569  exact ViewsProof.crc32_z_correct h hs crc ref offset bytes hg len readable
570
571/-- `uLong crc32(uLong crc, const unsigned char *buf, uInt len)`.
572The compatibility entry has the same complete byte-view and layout scope. -/
573theorem crc32_all_byte_views : Spec.ByteViews.Goal.crc32_all_byte_views := by
574  intro h hs crc ref offset bytes hg len readable
575  exact ViewsProof.crc32_correct h hs crc ref offset bytes hg len readable
576
577end Zlib.Crc32.Proofs