public-adler-combine.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»
2import ZlibF.Spec.Public.Checksums
3
4/-! Bridging the bytewise format checksum to the component-sum proof. -/
5
6namespace Zlib.Adler32.Proofs
7open C Zlib.Adler32 Zlib.Adler32.Spec
8
9private theorem adler_step_components (lo hi : Nat) (b : UInt8)
10    (hl : lo < 65521) (hh : hi < 65521) :
11    ZlibF.Spec.adlerStep (UInt32.ofNat (lo + 65536 * hi)) b =
12      UInt32.ofNat ((step (lo, hi) b).1 + 65536 * (step (lo, hi) b).2) := by
13  have hpack : (UInt32.ofNat (lo + 65536 * hi)).toNat = lo + 65536 * hi := by
14    rw [UInt32.toNat_ofNat', Nat.mod_eq_of_lt (by omega)]
15  have hlow : (lo + 65536 * hi) % 65536 = lo := by omega
16  have hhigh : (lo + 65536 * hi) / 65536 = hi := by omega
17  unfold ZlibF.Spec.adlerStep
18  rw [hpack, hlow, hhigh]
19  simp only [step, Zlib.Adler32.Spec.BASE]
20  congr 1
21  omega
22
23/-- The format Adler recurrence agrees with the component-sum model on canonical states. -/
24theorem adler_fold_components (bs : List UInt8) (lo hi : Nat)
25    (hl : lo < 65521) (hh : hi < 65521) :
26    ZlibF.Spec.adler32Update (UInt32.ofNat (lo + 65536 * hi)) bs =
27      UInt32.ofNat ((sums lo hi bs).1 + 65536 * (sums lo hi bs).2) := by
28  induction bs generalizing lo hi with
29  | nil => rfl
30  | cons b rest ih =>
31    have hs := step_lt (lo, hi) b
32    simp only [ZlibF.Spec.adler32Update, List.foldl_cons, sums, step] at *
33    rw [adler_step_components lo hi b hl hh]
34    exact ih _ _ hs.1 hs.2
35
36/-- The two independent definitions of Adler-32 agree on every byte sequence. -/
37theorem adler32_format_eq (bs : List UInt8) :
38    ZlibF.Spec.adler32 bs = UInt32.ofNat (Zlib.Adler32.Spec.adler32 1 bs) := by
39  have h := adler_fold_components bs 1 0 (by decide) (by decide)
40  simpa [ZlibF.Spec.adler32, Zlib.Adler32.Spec.adler32, Zlib.Adler32.Spec.BASE] using h
41
42private theorem format_halves (a : UInt64) (bs : List UInt8)
43    (ha : a.toUInt32 = ZlibF.Spec.adler32 bs) :
44    (a &&& 65535).toNat = (sums 1 0 bs).1 ∧
45    (a >>> 16 &&& 65535).toNat = (sums 1 0 bs).2 := by
46  have hb := sums_lt 1 0 bs (by decide) (by decide)
47  change (sums 1 0 bs).1 < 65521 ∧ (sums 1 0 bs).2 < 65521 at hb
48  have heq := congrArg UInt32.toNat ha
49  rw [adler32_format_eq] at heq
50  have hp : Zlib.Adler32.Spec.adler32 1 bs =
51      (sums 1 0 bs).1 + 65536 * (sums 1 0 bs).2 := by
52    simp [Zlib.Adler32.Spec.adler32, Zlib.Adler32.Spec.BASE]
53  rw [hp, UInt32.toNat_ofNat', Nat.mod_eq_of_lt (by omega), UInt64.toNat_toUInt32] at heq
54  rw [low16, high16]
55  omega
56
57/-- Both Adler combine entries terminate for all values, reject negative lengths,
58and combine genuine format checksums, even if the arguments carry upper bits. -/
59theorem adler32_combine_public (h : Heap) (a1 a2 : UInt64) (len : Int64) :
60    ∃ result, C.run (adler32_combine a1 a2 len) h = .ok (result, h) ∧
61      (len.toInt < 0 → result = 0xffffffff) ∧
62      (∀ xs ys : List UInt8,
63        a1.toUInt32 = ZlibF.Spec.adler32 xs → a2.toUInt32 = ZlibF.Spec.adler32 ys →
64        len.toInt = (ys.length : Int) → result = (ZlibF.Spec.adler32 (xs ++ ys)).toUInt64) := by
65  obtain ⟨result, hr⟩ := adler32_combine_c_safe (h := h) a1 a2 len
66  change C.run (adler32_combine a1 a2 len) h = .ok (result, h) at hr
67  refine ⟨result, hr, ?_, ?_⟩
68  · intro hn
69    have hneg : len < 0 := Int64.lt_iff_toInt_lt.mpr (by simpa using hn)
70    have hresult : C.run (adler32_combine a1 a2 len) h = .ok (0xffffffff, h) := by
71      simp [C.run, adler32_combine, adler32_combine_, hneg]
72    rw [hresult] at hr
73    cases hr
74    rfl
75  · intro xs ys hxs hys hlen
76    have hx := format_halves a1 xs hxs
77    have hy := format_halves a2 ys hys
78    have bx := sums_lt 1 0 xs (by decide) (by decide)
79    have bys := sums_lt 1 0 ys (by decide) (by decide)
80    change (sums 1 0 xs).1 < 65521 ∧ (sums 1 0 xs).2 < 65521 at bx
81    change (sums 1 0 ys).1 < 65521 ∧ (sums 1 0 ys).2 < 65521 at bys
82    have hpos : 0 ≤ len := Int64.le_iff_toInt_le.mpr (by simp [hlen])
83    obtain ⟨out, hrun, hout⟩ := combine_value (h := h) a1 a2 len hpos
84      (by simpa [hx.1] using bx.1) (by simpa [hx.2] using bx.2)
85      (by simpa [hy.1] using bys.1) (by simpa [hy.2] using bys.2)
86    have heq : out = result := by
87      change C.run (adler32_combine a1 a2 len) h = .ok (out, h) at hrun
88      rw [hr] at hrun
89      cases hrun
90      rfl
91    subst out
92    apply UInt64.toNat_inj.mp
93    rw [hout, hx.1, hx.2, hy.1, hy.2, hlen, Int.toNat_natCast, adler32_format_eq,
94      UInt32.toNat_toUInt64, UInt32.toNat_ofNat']
95    have hab := sums_lt 1 0 (xs ++ ys) (by decide) (by decide)
96    change (sums 1 0 (xs ++ ys)).1 < 65521 ∧ (sums 1 0 (xs ++ ys)).2 < 65521 at hab
97    have e3 : Zlib.Adler32.Spec.adler32 1 (xs ++ ys) =
98        (sums 1 0 (xs ++ ys)).1 + 65536 * (sums 1 0 (xs ++ ys)).2 := rfl
99    have hb32 : (sums 1 0 (xs ++ ys)).1 + 65536 * (sums 1 0 (xs ++ ys)).2 < 2 ^ 32 := by omega
100    rw [e3, Nat.mod_eq_of_lt hb32, sums_combine]
101    rfl
102
103
104/-- The 64-bit length entry has the same LP64 contract. -/
105theorem adler32_combine64_public (h : Heap) (a1 a2 : UInt64) (len : Int64) :
106    ∃ result, C.run (adler32_combine64 a1 a2 len) h = .ok (result, h) ∧
107      (len.toInt < 0 → result = 0xffffffff) ∧
108      (∀ xs ys : List UInt8,
109        a1.toUInt32 = ZlibF.Spec.adler32 xs → a2.toUInt32 = ZlibF.Spec.adler32 ys →
110        len.toInt = (ys.length : Int) → result = (ZlibF.Spec.adler32 (xs ++ ys)).toUInt64) :=
111  adler32_combine_public h a1 a2 len
112
113end Zlib.Adler32.Proofs
114
115namespace ZlibF.Spec.Public.AdlerCombineProof
116
117/-- `uLong adler32_combine(uLong adler1, uLong adler2, z_off_t len2)` combines checksums. -/
118theorem combine_public : Goal.adler32_combine := Zlib.Adler32.Proofs.adler32_combine_public
119
120/-- `uLong adler32_combine64(uLong adler1, uLong adler2, z_off64_t len2)` combines checksums. -/
121theorem combine64_public : Goal.adler32_combine64 := Zlib.Adler32.Proofs.adler32_combine64_public
122
123#print axioms combine_public
124#print axioms combine64_public
125end ZlibF.Spec.Public.AdlerCombineProof