Checksum.lean

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

1/-!
2# Format: Adler-32 and CRC-32
3
4Simple bytewise definitions (no tables). the checksum definitions in `docs/spec/format/README.md`.
5-/
6
7namespace ZlibF.Spec
8
9/-- One byte of Adler-32 (RFC 1950, 8.2): `s1 := (s1 + b) mod 65521`,
10`s2 := (s2 + s1) mod 65521`, with the value `s2 * 65536 + s1`.
11(lean-zip has an equivalent in `Zip.Adler32`.) -/
12def adlerStep (a : UInt32) (b : UInt8) : UInt32 :=
13  let s1 := (a.toNat % 65536 + b.toNat) % 65521
14  let s2 := (a.toNat / 65536 + s1) % 65521
15  UInt32.ofNat (s2 * 65536 + s1)
16
17/-- `adler32Update a data` continues the Adler-32 value `a` over `data`
18(the function `adler32(adler, buf, len)` of `zlib.h`). `F-adler-incremental`. -/
19def adler32Update (a : UInt32) (data : List UInt8) : UInt32 :=
20  data.foldl adlerStep a
21
22/-- Adler-32 of a byte sequence (RFC 1950, 8.2): the start value is 1, so the empty sequence gives 1. -/
23def adler32 (data : List UInt8) : UInt32 :=
24  adler32Update 1 data
25
26/-- The reflected CRC-32 polynomial of RFC 1952, 8.1.1.6.2. -/
27def crcPoly : UInt32 := 0xEDB88320
28
29/-- One bit step of the bit-reflected CRC: shift right, and xor the polynomial
30if the bit shifted out was 1. -/
31def crcBit (c : UInt32) : UInt32 :=
32  if c &&& 1 = 1 then (c >>> 1) ^^^ crcPoly else c >>> 1
33
34/-- One byte of the (already inverted) CRC register: xor the byte in, then 8 bit steps,
35least significant bit first. -/
36def crcByte (c : UInt32) (b : UInt8) : UInt32 :=
37  (List.range 8).foldl (fun c _ => crcBit c) (c ^^^ b.toUInt32)
38
39/-- `crc32Update crc data` continues the CRC-32 value `crc` over `data`
40(the function `crc32(crc, buf, len)` of `zlib.h`): invert, process, invert
41(RFC 1952, 8.1.1.6.2). `F-crc-incremental`. (lean-zip: `Zip.Crc32`.) -/
42def crc32Update (crc : UInt32) (data : List UInt8) : UInt32 :=
43  ~~~ (data.foldl crcByte (~~~ crc))
44
45/-- CRC-32 of a byte sequence: the start value is 0, so the empty sequence gives 0. -/
46def crc32 (data : List UInt8) : UInt32 :=
47  crc32Update 0 data
48
49/-- `F-adler-incremental`: feeding a sequence in pieces equals feeding it at once. -/
50theorem adler32Update_append (a : UInt32) (x y : List UInt8) :
51    adler32Update (adler32Update a x) y = adler32Update a (x ++ y) := by
52  simp [adler32Update, List.foldl_append]
53
54/-- `F-crc-incremental`: feeding a sequence in pieces equals feeding it at once. -/
55theorem crc32Update_append (c : UInt32) (x y : List UInt8) :
56    crc32Update (crc32Update c x) y = crc32Update c (x ++ y) := by
57  simp [crc32Update, List.foldl_append]
58
59end ZlibF.Spec