public-adler-update.lean

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

1import ZlibF.Spec.Public.Checksums
2import ZlibF.Proof.«adler32.c.public-any»
3
4open C Zlib.Adler32 Zlib.Adler32.Spec Zlib.Adler32.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.AdlerUpdateProof
7
8theorem adler_z_any_public {h : Heap} {ref : BRef} {data : Array UInt8}
9    (hg : Space.get h ref = some data) (seed : UInt64) (off : Nat) (len : UInt64)
10    (hf : off + len.toNat ≤ data.size) :
11    C.run (adler32_z seed (.ref ref off) len) h =
12      .ok (adlerValue seed ((data.toList.drop off).take len.toNat), h) := by
13  have he : UInt64.ofNat len.toNat = len := UInt64.ofNat_toNat
14  by_cases h1 : len.toNat = 1
15  · have hlen : len = 1 := by apply UInt64.toNat_inj.mp; simpa using h1
16    subst len
17    have hr := adler32_z_one_public (h := h) (r := ref) (off := off) (bytes := data) hg (by simpa using hf) seed
18    have hs := seg_eq_slice data off 1 (by simpa using hf)
19    rw [seg_one] at hs
20    have hout : (data.toList.drop off).take 1 = [data[off]!] := hs.symm
21    simpa [adlerValue, hout] using hr
22  · have hr := adler32_z_any_format hg seed off len.toNat hf len.toNat_lt h1
23    rw [seg_eq_slice data off len.toNat hf] at hr
24    have hl : ((data.toList.drop off).take len.toNat).length = len.toNat := by
25      simp only [List.length_take, List.length_drop, Array.length_toList]
26      apply Nat.min_eq_left
27      omega
28    have hn : ((data.toList.drop off).take len.toNat).length ≠ 1 := by omega
29    unfold adlerValue
30    rw [ite_eq_right hn]
31    change C.run (adler32_z seed (.ref ref off) len) h =
32      .ok ((ZlibF.Spec.adler32Update (canonicalStart seed) ((data.toList.drop off).take len.toNat)).toUInt64, h)
33    simpa only [he] using hr
34
35/-- `uLong adler32_z(uLong adler, const Bytef *buf, z_size_t len)` updates the checksum. -/
36theorem adler_z_public : Goal.adler32_z := by
37  intro h seed pointer len bytes hb
38  obtain ⟨hbuf, hnull⟩ := hb
39  rcases hbuf with ⟨rfl, rfl⟩ | ⟨ref, off, data, rfl, hg, hf, rfl⟩
40  · have hlen : len = 0 := UInt64.toNat_inj.mp (by simpa using hnull rfl)
41    subst len
42    rfl
43  · simpa using adler_z_any_public hg seed off len hf
44
45/-- `uLong adler32(uLong adler, const Bytef *buf, uInt len)` has the same update contract. -/
46theorem adler_public : Goal.adler32 := by
47  intro h seed pointer len bytes hb
48  have hr := adler_z_public h seed pointer len.toUInt64 bytes (by simpa [AdlerBufferBytes] using hb)
49  simpa [Zlib.Adler32.adler32] using hr
50
51#print axioms adler_z_public
52#print axioms adler_public
53end ZlibF.Spec.Public.AdlerUpdateProof