Checksums.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.Calls
2import ZlibF.Spec.Format.Checksum
3
4/-!
5# Public checksum contracts
6
7The buffer domain includes NULL queries and every represented readable byte object, not
8only heap byte blocks. Every result preserves the entire heap. No library callee contract
9is assumed. CRC tables are the library's initialised globals, not caller-selected tables.
10-/
11
12namespace ZlibF.Spec.Public
13open C
14
15/-- The bytes of a readable public buffer. NULL is a documented initial-value query even for
16a nonzero length. A nonnull pointer may be one past its object for a zero-length read. -/
17def BufferBytes (h : Heap) (pointer : BPtr) (length : Nat) (bytes : List UInt8) : Prop :=
18  (pointer = .null ∧ bytes = []) ∨
19  ∃ reference offset data, pointer = .ref reference offset ∧
20    Space.get h reference = some data ∧ offset + length ≤ data.size ∧
21    bytes = (data.toList.drop offset).take length
22
23/-- Adler initialization queries require a NULL pointer and zero length. This is an
24explicit restriction relative to the pinned header's unrestricted NULL wording;
25see `docs/deviations.md`. Nonnull readable objects retain their full length domain. -/
26def AdlerBufferBytes (h : Heap) (pointer : BPtr) (length : Nat) (bytes : List UInt8) : Prop :=
27  BufferBytes h pointer length bytes ∧ (pointer = .null → length = 0)
28
29/-- The fixed CRC globals of the selected build. -/
30def CrcGlobals (h : Heap) : Prop :=
31  h.static.crc_table = Zlib.Crc32H.crc_table ∧
32  h.static.x2n_table = Zlib.Crc32H.x2n_table
33
34/-- Canonicalise the low two component sums of an Adler seed. -/
35def adlerStart (seed : UInt64) : UInt32 :=
36  UInt32.ofNat ((seed.toNat % 65536) % 65521 +
37    65536 * ((seed.toNat / 65536 % 65536) % 65521))
38
39/-- Exact numeric behaviour, including the recorded noncanonical-seed caveat of the
40one-byte fast path. Canonical seeds agree with the RFC checksum recurrence. -/
41def adlerValue (seed : UInt64) (bytes : List UInt8) : UInt64 :=
42  if bytes.length = 1 then
43    let low := (seed.toNat % 65536 + (bytes.headD 0).toNat) % 65521
44    let sum := seed.toNat / 65536 % 65536 + low
45    UInt64.ofNat (low + 65536 * (if 65521 ≤ sum then sum - 65521 else sum))
46  else (ZlibF.Spec.adler32Update (adlerStart seed) bytes).toUInt64
47
48/-- Public update behaviour for either length width. All readable objects and all seeds are
49covered; NULL queries require zero length and return one without reading bytes.
50This explicit domain restriction is recorded in `docs/deviations.md`. The heap is unchanged. -/
51def AdlerUpdate (program : UInt64 → BPtr → UInt64 → M UInt64) : Prop :=
52  ∀ (h : Heap) (seed : UInt64) (pointer : BPtr) (length : UInt64) (bytes : List UInt8),
53    AdlerBufferBytes h pointer length.toNat bytes →
54    C.run (program seed pointer length) h =
55      .ok ((if pointer = .null then 1 else adlerValue seed bytes), h)
56
57/-- `uLong adler32_z(uLong adler, const Bytef *buf, z_size_t len)`.
58NULL queries have zero length; nonnull readable objects cover 64-bit lengths and all seeds.
59See `docs/deviations.md` for the query restriction. Exact value, no fault, termination,
60no allocation and the complete heap frame. -/
61def Goal.adler32_z : Prop := AdlerUpdate Zlib.Adler32.adler32_z
62
63/-- `uLong adler32(uLong adler, const Bytef *buf, uInt len)`.
64The public 32-bit length entry has the same buffer domain and exact result as `_z`.
65NULL queries require zero length, as recorded in `docs/deviations.md`. -/
66def Goal.adler32 : Prop :=
67  ∀ (h : Heap) (seed : UInt64) (pointer : BPtr) (length : UInt32) (bytes : List UInt8),
68    AdlerBufferBytes h pointer length.toNat bytes →
69    C.run (Zlib.Adler32.adler32 seed pointer length) h =
70      .ok ((if pointer = .null then 1 else adlerValue seed bytes), h)
71
72/-- Combine calls never fault or change the heap, even for forged checksums. Negative lengths
73return the documented sentinel. For genuine checksums and the length of the second input,
74the result is the checksum of concatenation. No claim of a meaningful checksum is made for
75a forged pair that does not describe those inputs. -/
76def AdlerCombine (program : UInt64 → UInt64 → Int64 → M UInt64) : Prop :=
77  ∀ (h : Heap) (first second : UInt64) (length : Int64), ∃ result,
78    C.run (program first second length) h = .ok (result, h) ∧
79    (length.toInt < 0 → result = 0xffffffff) ∧
80    (∀ a b : List UInt8,
81      first.toUInt32 = ZlibF.Spec.adler32 a → second.toUInt32 = ZlibF.Spec.adler32 b →
82      length.toInt = (b.length : Int) → result = (ZlibF.Spec.adler32 (a ++ b)).toUInt64)
83
84/-- `uLong adler32_combine(uLong adler1, uLong adler2, z_off_t len2)`.
85Total execution, immutable heap, negative-length rejection and checksum concatenation. -/
86def Goal.adler32_combine : Prop := AdlerCombine Zlib.Adler32.adler32_combine
87
88/-- `uLong adler32_combine64(uLong adler1, uLong adler2, z_off64_t len2)`.
89The LP64 64-bit-length entry has the same complete public combine contract. -/
90def Goal.adler32_combine64 : Prop := AdlerCombine Zlib.Adler32.adler32_combine64
91
92/-- Advancing a reflected CRC register through `bits` zero bits, as polynomial arithmetic.
93This is independent of the implementation's tables and multiplication loop. -/
94def crcAdvance (bits : Nat) (register : UInt32) : UInt32 :=
95  (List.range bits).foldl (fun current _ => ZlibF.Spec.crcBit current) register
96
97/-- The polynomial operator for a signed byte length; a negative length is rejected with zero. -/
98def crcOperator (length : Int64) : UInt64 :=
99  if length.toInt < 0 then 0 else (crcAdvance (8 * length.toInt.toNat) 0x80000000).toUInt64
100
101/-- Mathematical CRC combination, with zero for a rejected negative length. -/
102def crcCombined (first second : UInt64) (length : Int64) : UInt64 :=
103  if length.toInt < 0 then 0
104  else ((crcAdvance (8 * length.toInt.toNat) first.toUInt32) ^^^ second.toUInt32).toUInt64
105
106/-- `uLong crc32_z(uLong crc, const Bytef *buf, z_size_t len)`.
107All readable represented buffers, alignments, seeds and 64-bit lengths. NULL returns zero.
108The exact RFC recurrence is returned and the heap is unchanged. -/
109def Goal.crc32_z : Prop :=
110  ∀ (h : Heap) (seed : UInt64) (pointer : BPtr) (length : UInt64) (bytes : List UInt8),
111    CrcGlobals h → BufferBytes h pointer length.toNat bytes →
112    C.run (Zlib.Crc32.crc32_z seed pointer length) h =
113      .ok ((if pointer = .null then 0 else (ZlibF.Spec.crc32Update seed.toUInt32 bytes).toUInt64), h)
114
115/-- `uLong crc32(uLong crc, const Bytef *buf, uInt len)`.
116The public 32-bit length entry has the same full buffer domain and exact checksum contract. -/
117def Goal.crc32 : Prop :=
118  ∀ (h : Heap) (seed : UInt64) (pointer : BPtr) (length : UInt32) (bytes : List UInt8),
119    CrcGlobals h → BufferBytes h pointer length.toNat bytes →
120    C.run (Zlib.Crc32.crc32 seed pointer length) h =
121      .ok ((if pointer = .null then 0 else (ZlibF.Spec.crc32Update seed.toUInt32 bytes).toUInt64), h)
122
123/-- `const z_crc_t *get_crc_table(void)`.
124The returned table is static and read-only, has 256 entries given by the reflected CRC
125recurrence, and leaves every heap observation unchanged. -/
126def Goal.get_crc_table : Prop :=
127  ∀ h : Heap, CrcGlobals h → ∃ pointer table,
128    C.run Zlib.Crc32.get_crc_table h = .ok (pointer, h) ∧
129    pointer = .ref .st_crc_table 0 ∧ Space.get h URef.st_crc_table = some table ∧
130    Space.ro h URef.st_crc_table = true ∧ table.size = 256 ∧
131    ∀ i : Fin 256, table[i.val]? = some (ZlibF.Spec.crcByte 0 (UInt8.ofNat i.val))
132
133/-- Operator generation is total for every signed argument. Initialised globals are preserved;
134negative lengths return zero and nonnegative lengths give the mathematical polynomial. -/
135def CrcGenerate (program : Int64 → M UInt64) : Prop :=
136  ∀ (h : Heap) (length : Int64), CrcGlobals h →
137    C.run (program length) h = .ok (crcOperator length, h)
138
139/-- `uLong crc32_combine_gen(z_off_t len2)`; complete operator-generation contract. -/
140def Goal.crc32_combine_gen : Prop := CrcGenerate Zlib.Crc32.crc32_combine_gen
141
142/-- `uLong crc32_combine_gen64(z_off64_t len2)`; complete operator-generation contract. -/
143def Goal.crc32_combine_gen64 : Prop := CrcGenerate Zlib.Crc32.crc32_combine_gen64
144
145/-- `uLong crc32_combine_op(uLong crc1, uLong crc2, uLong op)`.
146`zlib.h` requires an operator generated from a length by `crc32_combine_gen`. The domain here
147is exactly those mathematical operators, including its zero rejection result. Arbitrary forged
148operators are not promised termination. Every permitted call has the polynomial result and
149preserves the whole heap. -/
150def Goal.crc32_combine_op : Prop :=
151  ∀ (h : Heap) (first second : UInt64) (length : Int64), CrcGlobals h →
152    C.run (Zlib.Crc32.crc32_combine_op first second (crcOperator length)) h =
153      .ok (crcCombined first second length, h)
154
155/-- Total CRC combination, exact polynomial result and the entire heap frame for every signed
156length and checksum argument. Negative lengths return zero. -/
157def CrcCombine (program : UInt64 → UInt64 → Int64 → M UInt64) : Prop :=
158  ∀ (h : Heap) (first second : UInt64) (length : Int64), CrcGlobals h →
159    C.run (program first second length) h = .ok (crcCombined first second length, h)
160
161/-- `uLong crc32_combine(uLong crc1, uLong crc2, z_off_t len2)`; full combine contract. -/
162def Goal.crc32_combine : Prop := CrcCombine Zlib.Crc32.crc32_combine
163
164/-- `uLong crc32_combine64(uLong crc1, uLong crc2, z_off64_t len2)`; full combine contract. -/
165def Goal.crc32_combine64 : Prop := CrcCombine Zlib.Crc32.crc32_combine64
166
167end ZlibF.Spec.Public