adler32.c.public-one.lean

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

1import ZlibF.Proof.«adler32.c»
2
3/-! The public Adler-32 one-byte fast path, including noncanonical seeds. -/
4
5namespace Zlib.Adler32.Proofs
6open C Zlib.Adler32 Zlib.Adler32.Spec
7
8/-- One conditional subtraction suffices for the one-byte low component. -/
9private theorem one_low (seed : UInt64) (byte : UInt8) :
10    (csub ((seed &&& 65535) + byte.toUInt64) BASE).toNat =
11      (seed.toNat % 65536 + byte.toNat) % 65521 := by
12  have hlo : (seed &&& 65535).toNat < 65536 := by rw [low16]; omega
13  have hb := byte.toNat_lt
14  have hraw : ((seed &&& 65535) + byte.toUInt64).toNat =
15      seed.toNat % 65536 + byte.toNat := by
16    rw [add_small _ _ (by rw [UInt8.toNat_toUInt64]; omega), low16, UInt8.toNat_toUInt64]
17  rw [csub_toNat, base_toNat, hraw]
18  split <;> omega
19
20/-- The high component uses one conditional subtraction, matching zlib even for
21noncanonical initial checksums. -/
22private theorem one_high (seed : UInt64) (byte : UInt8) :
23    (csub ((seed >>> 16 &&& 65535) + csub ((seed &&& 65535) + byte.toUInt64) BASE) BASE).toNat =
24      let lo := (seed.toNat % 65536 + byte.toNat) % 65521
25      let total := seed.toNat / 65536 % 65536 + lo
26      if 65521 ≤ total then total - 65521 else total := by
27  have hhi : (seed >>> 16 &&& 65535).toNat < 65536 := by rw [high16]; omega
28  have hlo : (csub ((seed &&& 65535) + byte.toUInt64) BASE).toNat < 65521 := by
29    rw [one_low]; exact Nat.mod_lt _ (by decide)
30  have hs : ((seed >>> 16 &&& 65535) + csub ((seed &&& 65535) + byte.toUInt64) BASE).toNat =
31      seed.toNat / 65536 % 65536 + (seed.toNat % 65536 + byte.toNat) % 65521 := by
32    rw [add_small _ _ (by omega), high16, one_low]
33  rw [csub_toNat, base_toNat, hs]
34
35/-- `uLong adler32_z(uLong adler, const Bytef *buf, z_size_t len)` with
36`len = 1`: for every represented readable byte object and every seed, the
37actual result matches the noncanonical-seed fast-path arithmetic. -/
38theorem adler32_z_one_public {h : Heap} {r : BRef} {off : Nat} {bytes : Array UInt8}
39    (hg : Space.get h r = some bytes) (hfit : off + 1 ≤ bytes.size) (seed : UInt64) :
40    C.run (adler32_z seed (.ref r off) 1) h = .ok
41      (UInt64.ofNat (let low := (seed.toNat % 65536 + bytes[off]!.toNat) % 65521
42        let total := seed.toNat / 65536 % 65536 + low
43        low + 65536 * (if 65521 ≤ total then total - 65521 else total)), h) := by
44  have hi : off + 0 < bytes.size := by omega
45  have hindex := Ptr.index_ok (h := h) (r := r) (a := bytes) (off := off) (i := 0) hg hi
46  unfold OkOn at hindex
47  have hindex' : index8 (.ref r off) 0 h = .ok (bytes[off]!, h) := by
48    simpa [getElem_eq_bang bytes off (by omega)] using hindex
49  have hr : (adler32_z seed (.ref r off) 1) h =
50      .ok ((csub ((seed &&& 65535) + bytes[off]!.toUInt64) BASE |||
51        (csub ((seed >>> 16 &&& 65535) + csub ((seed &&& 65535) + bytes[off]!.toUInt64) BASE) BASE <<< 16)), h) := by
52    unfold adler32_z
53    rw [ite_eq_left (by decide)]
54    simp only [bind_app, hindex', csub]
55    by_cases hlow : (seed &&& 65535) + bytes[off]!.toUInt64 ≥ BASE
56    · rw [ite_eq_left hlow]
57      by_cases hhigh : (seed >>> 16 &&& 65535) + ((seed &&& 65535) + bytes[off]!.toUInt64 - BASE) ≥ BASE
58      · simp [hlow, hhigh, pure_app]
59      · simp [hlow, hhigh, pure_app]
60    · rw [ite_eq_right hlow]
61      by_cases hhigh : (seed >>> 16 &&& 65535) + ((seed &&& 65535) + bytes[off]!.toUInt64) ≥ BASE
62      · simp [hlow, hhigh, pure_app]
63      · simp [hlow, hhigh, pure_app]
64  unfold C.run
65  rw [hr]
66  have heq : (csub ((seed &&& 65535) + bytes[off]!.toUInt64) BASE |||
67        (csub ((seed >>> 16 &&& 65535) + csub ((seed &&& 65535) + bytes[off]!.toUInt64) BASE) BASE <<< 16)) =
68      UInt64.ofNat (let low := (seed.toNat % 65536 + bytes[off]!.toNat) % 65521
69        let total := seed.toNat / 65536 % 65536 + low
70        low + 65536 * (if 65521 ≤ total then total - 65521 else total)) := by
71    apply UInt64.toNat_inj.mp
72    have hl : (csub ((seed &&& 65535) + bytes[off]!.toUInt64) BASE).toNat < 65536 := by
73      rw [one_low]; have := Nat.mod_lt (seed.toNat % 65536 + bytes[off]!.toNat) (by decide : 0 < 65521); omega
74    have hh : (csub ((seed >>> 16 &&& 65535) + csub ((seed &&& 65535) + bytes[off]!.toUInt64) BASE) BASE).toNat < 65536 := by
75      rw [one_high]
76      have hlow := Nat.mod_lt (seed.toNat % 65536 + bytes[off]!.toNat) (by decide : 0 < 65521)
77      have hhi : seed.toNat / 65536 % 65536 < 65536 := Nat.mod_lt _ (by decide)
78      dsimp only
79      split <;> omega
80    rw [or_shift _ _ hl hh, one_low, one_high, UInt64.toNat_ofNat']
81    dsimp only
82    symm
83    apply Nat.mod_eq_of_lt
84    have hlow := Nat.mod_lt (seed.toNat % 65536 + bytes[off]!.toNat) (by decide : 0 < 65521)
85    have hhi : seed.toNat / 65536 % 65536 < 65536 := Nat.mod_lt _ (by decide)
86    split <;> omega
87  rw [heq]
88
89end Zlib.Adler32.Proofs