adler32.c.lean

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

1import ZlibF.Runtime.Alloc
2
3/-!
4# adler32.c — faithful translation (draft)
5
6Source: `zlib/adler32.c`, default build (`NO_DIVIDE` undefined, so
7`MOD`/`MOD28` are `a %= BASE`), LP64. Translated statement by statement; the
8`DO1`..`DO16` macros become `do1`/`do16` with the same expansion order.
9
10Types: `uLong`/`unsigned long` = `UInt64`, `z_size_t` = `UInt64`,
11`unsigned` = `UInt32`, `Bytef` = `UInt8`. Byte reads are promoted to `int`
12and then converted to `unsigned long`, which preserves their value.
13
14Status: translated by hand; differentially tested against the real C (`tests/`); the proofs are in
15`ZlibF/Proof/adler32.c.lean`.
16-/
17
18namespace Zlib.Adler32
19open C
20
21def BASE : UInt64 := 65521
22def NMAX : UInt64 := 5552
23
24/-- Loop-carried locals of `adler32_z`. -/
25structure Locals where
26  adler : UInt64
27  sum2 : UInt64
28  buf : BPtr
29  len : UInt64
30  n : UInt32
31
32/-- `DO1(buf,i)`: `{adler += (buf)[i]; sum2 += adler;}` -/
33def do1 (s : Locals) (i : Int) : M Locals := do
34  let b ← index8 s.buf i
35  let adler := s.adler + b.toUInt64
36  pure { s with adler, sum2 := s.sum2 + adler }
37
38/-- `DO16(buf)`: `DO8(buf,0); DO8(buf,8);`, i.e. `DO1(buf,0)` .. `DO1(buf,15)`. -/
39def do16 (s : Locals) : M Locals := do
40  let s ← do1 s 0;  let s ← do1 s 1;  let s ← do1 s 2;  let s ← do1 s 3
41  let s ← do1 s 4;  let s ← do1 s 5;  let s ← do1 s 6;  let s ← do1 s 7
42  let s ← do1 s 8;  let s ← do1 s 9;  let s ← do1 s 10; let s ← do1 s 11
43  let s ← do1 s 12; let s ← do1 s 13; let s ← do1 s 14; do1 s 15
44
45/-- `adler += *buf++; sum2 += adler;` -/
46def stepByte (s : Locals) : M Locals := do
47  let b ← load8 s.buf
48  let buf ← s.buf.add 1
49  let adler := s.adler + b.toUInt64
50  pure { s with adler, buf, sum2 := s.sum2 + adler }
51
52/-- `while (len--)` condition. -/
53def lenPostDec (s : Locals) : M (Bool × Locals) :=
54  pure (s.len != 0, { s with len := s.len - 1 })
55
56/-- `uLong ZEXPORT adler32_z(uLong adler, const Bytef *buf, z_size_t len)` -/
57def adler32_z (adler : UInt64) (buf : BPtr) (len : UInt64) : M UInt64 := do
58  -- sum2 = (adler >> 16) & 0xffff; adler &= 0xffff;
59  let sum2 := (adler >>> 16) &&& 0xffff
60  let adler := adler &&& 0xffff
61  -- if (len == 1) { ... }
62  if len == 1 then
63    let b ← index8 buf 0
64    let mut adler := adler + b.toUInt64
65    if adler >= BASE then adler := adler - BASE
66    let mut sum2 := sum2 + adler
67    if sum2 >= BASE then sum2 := sum2 - BASE
68    return adler ||| (sum2 <<< 16)
69  -- initial Adler-32 value (deferred check for len == 1 speed)
70  if buf == .null then return 1
71  -- if (len < 16) { while (len--) {...} ... }
72  if len < 16 then
73    let s ← cwhile lenPostDec stepByte { adler, sum2, buf, len, n := 0 }
74    let mut adler := s.adler
75    if adler >= BASE then adler := adler - BASE
76    let sum2 := s.sum2 % BASE  -- MOD28(sum2)
77    return adler ||| (sum2 <<< 16)
78  -- while (len >= NMAX) { ... }
79  let s ← cwhile (fun s => pure (s.len >= NMAX, s))
80    (fun s => do
81      let s := { s with len := s.len - NMAX, n := (NMAX / 16).toUInt32 }
82      -- do { DO16(buf); buf += 16; } while (--n);
83      let s ← cdoWhile
84        (fun s => do
85          let s ← do16 s
86          pure { s with buf := ← s.buf.add 16 })
87        (fun s => let n := s.n - 1; pure (n != 0, { s with n }))
88        s
89      -- MOD(adler); MOD(sum2);
90      pure { s with adler := s.adler % BASE, sum2 := s.sum2 % BASE })
91    { adler, sum2, buf, len, n := 0 }
92  -- if (len) { ... }
93  let s ← if s.len != 0 then do
94      let s ← cwhile (fun s => pure (s.len >= 16, s))
95        (fun s => do
96          let s := { s with len := s.len - 16 }
97          let s ← do16 s
98          pure { s with buf := ← s.buf.add 16 })
99        s
100      let s ← cwhile lenPostDec stepByte s
101      pure { s with adler := s.adler % BASE, sum2 := s.sum2 % BASE }
102    else pure s
103  return s.adler ||| (s.sum2 <<< 16)
104
105/-- `uLong ZEXPORT adler32(uLong adler, const Bytef *buf, uInt len)` -/
106def adler32 (adler : UInt64) (buf : BPtr) (len : UInt32) : M UInt64 :=
107  adler32_z adler buf len.toUInt64
108
109/-- `local uLong adler32_combine_(uLong adler1, uLong adler2, z_off64_t len2)`
110(`z_off64_t` = signed 64-bit `long` on LP64 Linux; `MOD63` is `%=` in the
111default build). -/
112def adler32_combine_ (adler1 adler2 : UInt64) (len2 : Int64) : M UInt64 := do
113  -- if (len2 < 0) return 0xffffffffUL;
114  if len2 < 0 then return 0xffffffff
115  -- MOD63(len2);  i.e. len2 %= BASE (signed %, operands nonnegative here)
116  let len2 := len2 % 65521
117  -- rem = (unsigned)len2;
118  -- signed -> unsigned conversion is modulo 2^32, i.e. reinterpret then truncate
119  let rem : UInt32 := len2.toUInt64.toUInt32
120  let sum1 := adler1 &&& (0xffff : UInt64)
121  -- sum2 = rem * sum1;  (rem converted to unsigned long)
122  let sum2 := rem.toUInt64 * sum1
123  let sum2 := sum2 % BASE  -- MOD(sum2)
124  let sum1 := sum1 + ((adler2 &&& (0xffff : UInt64)) + BASE - 1)
125  let sum2 := sum2 + (((adler1 >>> 16) &&& (0xffff : UInt64)) + ((adler2 >>> 16) &&& (0xffff : UInt64)) + BASE - rem.toUInt64)
126  let mut sum1 := sum1
127  if sum1 >= BASE then sum1 := sum1 - BASE
128  if sum1 >= BASE then sum1 := sum1 - BASE
129  let mut sum2 := sum2
130  if sum2 >= (BASE <<< 1) then sum2 := sum2 - (BASE <<< 1)
131  if sum2 >= BASE then sum2 := sum2 - BASE
132  return sum1 ||| (sum2 <<< 16)
133
134/-- `uLong ZEXPORT adler32_combine(uLong adler1, uLong adler2, z_off_t len2)` (`z_off_t` = `long`). -/
135def adler32_combine (adler1 adler2 : UInt64) (len2 : Int64) : M UInt64 :=
136  adler32_combine_ adler1 adler2 len2
137
138/-- `uLong ZEXPORT adler32_combine64(uLong adler1, uLong adler2, z_off64_t len2)` -/
139def adler32_combine64 (adler1 adler2 : UInt64) (len2 : Int64) : M UInt64 :=
140  adler32_combine_ adler1 adler2 len2
141
142end Zlib.Adler32