crc32.c.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Runtime.Alloc
2import ZlibF.Runtime.Address
3import ZlibF.Zlib.«crc32.h»
4
5/-!
6# crc32.c — faithful translation
7
8Source: `crc32.c` and `crc32.h`, default x86_64 Linux build. Preprocessor decisions: `DYNAMIC_CRC_TABLE`, `MAKECRCH`,
9`Z_TESTN`, `Z_TESTW`, `ARMCRC32` (`__aarch64__` only) and `HAVE_S390X_VX` are undefined, so the static tables of
10`crc32.h` are used and `make_crc_table`, `braid`, `write_table*` and `z_once` are dead. `N = 5`, `W = 8`
11(`__x86_64__`), `z_word_t` is `unsigned long`, `z_crc_t` is `unsigned`. The `#if N > 5` parts are dead.
12
13Decisions on the model:
14
15* **Tables.** `crc_table` and `x2n_table` are the `Statics` fields of the same name (read through `UPtr`;
16  `initStatics` sets them from `crc32.h.lean`). `crc_big_table`, `crc_braid_table`, `crc_braid_big_table` are only
17  indexed, so they are Lean constants, indexed with a bounds check.
18* **Alignment.** `((z_size_t)buf & (W - 1))` observes the low three address bits. Raw byte blocks retain the
19  aligned-origin convention, so their offsets supply these bits. Static and embedded byte arrays use arbitrary
20  stable origin residues from the heap. Proofs must hold for every residue, including nonzero field alignment.
21  This abstraction is only for the low-bit test; it does not supply a general ABI address or aliasing model.
22* **Words.** `words[i]` reads the byte buffer as `unsigned long`; the translation reads the 8 bytes in order and
23  assembles them little endian (`loadWord`). The formal strict-aliasing issue of this cast is not modelled; it is
24  inside the object either way.
25* **Endianness.** `*(unsigned char *)&endian` with `endian = 1` is the low byte of `endian` on the little-endian
26  target, so the big-endian branch is dead at run time; it is translated for completeness and is not reached
27  (the differential test cannot cover it).
28* `multmodp` loops forever when `a` has no bit set among bits 0..31 (`a != 0` is not enough); the C then never
29  ends, and here the loop runs out of fuel. `crc32_combine_op(crc1, crc2, op)` reaches it for `op` with zero low
30  32 bits.
31-/
32
33namespace Zlib.Crc32
34open C
35
36/-- `Z_BATCH` etc. are `ARMCRC32` only. `N` and `W`: -/
37def N : Int32 := 5
38def W : Int32 := 8
39
40/-- `#define POLY 0xedb88320` (an `unsigned int` constant). -/
41def POLY : UInt64 := 0xedb88320
42
43/-- The `Statics` with the contents that `crc32.c` fixes: `crc_table` and `x2n_table` (from `crc32.h`). -/
44def initStatics (s : Statics) : Statics :=
45  { s with crc_table := Zlib.Crc32H.crc_table, x2n_table := Zlib.Crc32H.x2n_table }
46
47/-- `x >> n` for `unsigned long`: undefined if `n >= 64`. -/
48def shr64 (x n : UInt64) : M UInt64 :=
49  if n < 64 then pure (x >>> n) else ub "shift count out of range"
50
51/-- `crc_table[i]` -/
52def crcTab (i : UInt64) : M UInt32 := Ptr.index (Ptr.ref URef.st_crc_table 0) i.toNat
53
54/-- `x2n_table[i]` -/
55def x2nTab (i : UInt32) : M UInt32 := Ptr.index (Ptr.ref URef.st_x2n_table 0) i.toNat
56
57/-- `t[k][i]` for a constant two-dimensional table. -/
58def idx2 {α : Type} (t : Array (Array α)) (k i : Nat) : M α :=
59  match t[k]? with
60  | some r => match r[i]? with
61    | some v => pure v
62    | none => ub "table index outside its array"
63  | none => ub "table index outside its array"
64
65/-- `t[i]` for a constant table. -/
66def idx1 {α : Type} (t : Array α) (i : Nat) : M α :=
67  match t[i]? with
68  | some v => pure v
69  | none => ub "table index outside its array"
70
71/-- `(z_size_t)buf`, represented up to the low bits observed by the CRC alignment test. -/
72def addrOf (p : BPtr) : M UInt64 :=
73  C.ByteAddress.address p
74
75/-- `words[i]` for `z_word_t const *words` over the byte buffer at `p` (little-endian target). -/
76def loadWord (p : BPtr) : M UInt64 := do
77  let mut w : UInt64 := 0
78  for i in [0:8] do
79    let b ← index8 p i
80    w := w ||| (b.toUInt64 <<< (8 * i).toUInt64)
81  pure w
82
83/-! ### Byte swaps and the word CRCs -/
84
85/-- `local z_word_t byte_swap(z_word_t word)` (`W == 8`) -/
86def byte_swap (word : UInt64) : UInt64 :=
87  (word &&& 0xff00000000000000) >>> 56 |||
88  (word &&& 0xff000000000000) >>> 40 |||
89  (word &&& 0xff0000000000) >>> 24 |||
90  (word &&& 0xff00000000) >>> 8 |||
91  (word &&& 0xff000000) <<< 8 |||
92  (word &&& 0xff0000) <<< 24 |||
93  (word &&& 0xff00) <<< 40 |||
94  (word &&& 0xff) <<< 56
95
96/-- `local z_crc_t crc_word(z_word_t data)` -/
97def crc_word (data : UInt64) : M UInt32 := do
98  -- for (k = 0; k < W; k++) data = (data >> 8) ^ crc_table[data & 0xff];
99  let (data, _) ← cwhile (fun (data, k) => pure (k < W, (data, k)))
100    (fun (data, k) => do
101      let t ← crcTab (data &&& 0xff)
102      pure ((data >>> 8) ^^^ t.toUInt64, k + 1)) (data, (0 : Int32))
103  -- return (z_crc_t)data;
104  pure data.toUInt32
105
106/-- `local z_word_t crc_word_big(z_word_t data)` -/
107def crc_word_big (data : UInt64) : M UInt64 := do
108  -- for (k = 0; k < W; k++) data = (data << 8) ^ crc_big_table[(data >> ((W - 1) << 3)) & 0xff];
109  let (data, _) ← cwhile (fun (data, k) => pure (k < W, (data, k)))
110    (fun (data, k) => do
111      let t ← idx1 Zlib.Crc32H.crc_big_table (((data >>> 56) &&& 0xff).toNat)
112      pure ((data <<< 8) ^^^ t, k + 1)) (data, (0 : Int32))
113  pure data
114
115/-! ### Polynomial arithmetic -/
116
117/-- `local uLong multmodp(uLong a, uLong b)` -/
118def multmodp (a b : UInt64) : M UInt64 := do
119  -- m = (uLong)1 << 31; p = 0;
120  -- for (;;) { if (a & m) { p ^= b; if ((a & (m - 1)) == 0) break; }
121  --            m >>= 1; b = b & 1 ? (b >> 1) ^ POLY : b >> 1; }
122  let (_, p, _, _) ← cwhile (fun (m, p, b, brk) => pure (!brk, (m, p, b, brk)))
123    (fun (m, p, b, brk) => do
124      let mut p := p
125      if a &&& m != 0 then
126        p := p ^^^ b
127        if a &&& (m - 1) == 0 then return (m, p, b, true)
128      let m := m >>> 1
129      let b := if b &&& 1 != 0 then (b >>> 1) ^^^ POLY else b >>> 1
130      pure (m, p, b, brk)) (((1 : UInt64) <<< 31, (0 : UInt64), b, false) : UInt64 × UInt64 × UInt64 × Bool)
131  pure p
132
133/-- `local uLong x2nmodp(z_off64_t n, unsigned k)` -/
134def x2nmodp (n : Int64) (k : UInt32) : M UInt64 := do
135  -- p = (uLong)1 << 31;             /* x^0 == 1 */
136  -- while (n) { if (n & 1) p = multmodp(x2n_table[k & 31], p); n >>= 1; k++; }
137  let (p, _, _) ← cwhile (fun (p, n, k) => pure (n != 0, (p, n, k)))
138    (fun (p, n, k) => do
139      let mut p := p
140      if n &&& 1 != 0 then
141        let t ← x2nTab (k &&& 31)
142        p ← multmodp t.toUInt64 p
143      pure (p, n >>> 1, k + 1)) (((1 : UInt64) <<< 31, n, k) : UInt64 × Int64 × UInt32)
144  pure p
145
146/-- `const z_crc_t FAR * ZEXPORT get_crc_table(void)` -/
147def get_crc_table : M UPtr :=
148  -- return (const z_crc_t FAR *)crc_table;
149  pure (Ptr.ref URef.st_crc_table 0)
150
151/-! ### `crc32_z` -/
152
153/-- The little-endian braids: `crc0 .. crc4` (`z_crc_t`), `words`, `blks`. -/
154structure BL where
155  crc0 : UInt32
156  crc1 : UInt32
157  crc2 : UInt32
158  crc3 : UInt32
159  crc4 : UInt32
160  words : BPtr
161  blks : UInt64
162
163/-- The big-endian braids: `crc0 .. crc4` (`z_word_t`). -/
164structure BB where
165  crc0 : UInt64
166  crc1 : UInt64
167  crc2 : UInt64
168  crc3 : UInt64
169  crc4 : UInt64
170  words : BPtr
171  blks : UInt64
172
173/-- `words[i]` for `i < N`. -/
174def wordAt (words : BPtr) (i : Nat) : M UInt64 := do
175  loadWord (← words.add (8 * i))
176
177/-- `crcK ^= crc_braid_table[k][(wordK >> (k << 3)) & 0xff];` -/
178def braidTab (k : Int32) (word : UInt64) : M UInt32 := do
179  let sh ← shr64 word (k <<< 3).toInt.toNat.toUInt64
180  idx2 Zlib.Crc32H.crc_braid_table k.toInt.toNat (sh &&& 0xff).toNat
181
182/-- `crcK ^= crc_braid_big_table[k][(wordK >> (k << 3)) & 0xff];` -/
183def braidBigTab (k : Int32) (word : UInt64) : M UInt64 := do
184  let sh ← shr64 word (k <<< 3).toInt.toNat.toUInt64
185  idx2 Zlib.Crc32H.crc_braid_big_table k.toInt.toNat (sh &&& 0xff).toNat
186
187/-- The body of `while (--blks)` in the little-endian branch. -/
188def blockLittle (s : BL) : M BL := do
189  -- word0 = crc0 ^ words[0]; ... word4 = crc4 ^ words[4];
190  let word0 := s.crc0.toUInt64 ^^^ (← wordAt s.words 0)
191  let word1 := s.crc1.toUInt64 ^^^ (← wordAt s.words 1)
192  let word2 := s.crc2.toUInt64 ^^^ (← wordAt s.words 2)
193  let word3 := s.crc3.toUInt64 ^^^ (← wordAt s.words 3)
194  let word4 := s.crc4.toUInt64 ^^^ (← wordAt s.words 4)
195  -- words += N;
196  let words ← s.words.add 40
197  -- crc0 = crc_braid_table[0][word0 & 0xff]; ... crc4 = ...
198  let crc0 ← braidTab 0 word0
199  let crc1 ← braidTab 0 word1
200  let crc2 ← braidTab 0 word2
201  let crc3 ← braidTab 0 word3
202  let crc4 ← braidTab 0 word4
203  -- for (k = 1; k < W; k++) { crc0 ^= ...; crc1 ^= ...; ... crc4 ^= ...; }
204  let (crc0, crc1, crc2, crc3, crc4, _) ← cwhile (fun (c0, c1, c2, c3, c4, k) => pure (k < W, (c0, c1, c2, c3, c4, k)))
205    (fun (c0, c1, c2, c3, c4, k) => do
206      let c0 := c0 ^^^ (← braidTab k word0)
207      let c1 := c1 ^^^ (← braidTab k word1)
208      let c2 := c2 ^^^ (← braidTab k word2)
209      let c3 := c3 ^^^ (← braidTab k word3)
210      let c4 := c4 ^^^ (← braidTab k word4)
211      pure (c0, c1, c2, c3, c4, k + 1)) (crc0, crc1, crc2, crc3, crc4, (1 : Int32))
212  pure { s with crc0, crc1, crc2, crc3, crc4, words }
213
214/-- The body of `while (--blks)` in the big-endian branch. -/
215def blockBig (s : BB) : M BB := do
216  let word0 := s.crc0 ^^^ (← wordAt s.words 0)
217  let word1 := s.crc1 ^^^ (← wordAt s.words 1)
218  let word2 := s.crc2 ^^^ (← wordAt s.words 2)
219  let word3 := s.crc3 ^^^ (← wordAt s.words 3)
220  let word4 := s.crc4 ^^^ (← wordAt s.words 4)
221  let words ← s.words.add 40
222  let crc0 ← (do let sh ← shr64 word0 0; idx2 Zlib.Crc32H.crc_braid_big_table 0 (sh &&& 0xff).toNat)
223  let crc1 ← (do let sh ← shr64 word1 0; idx2 Zlib.Crc32H.crc_braid_big_table 0 (sh &&& 0xff).toNat)
224  let crc2 ← (do let sh ← shr64 word2 0; idx2 Zlib.Crc32H.crc_braid_big_table 0 (sh &&& 0xff).toNat)
225  let crc3 ← (do let sh ← shr64 word3 0; idx2 Zlib.Crc32H.crc_braid_big_table 0 (sh &&& 0xff).toNat)
226  let crc4 ← (do let sh ← shr64 word4 0; idx2 Zlib.Crc32H.crc_braid_big_table 0 (sh &&& 0xff).toNat)
227  let (crc0, crc1, crc2, crc3, crc4, _) ← cwhile (fun (c0, c1, c2, c3, c4, k) => pure (k < W, (c0, c1, c2, c3, c4, k)))
228    (fun (c0, c1, c2, c3, c4, k) => do
229      let c0 := c0 ^^^ (← braidBigTab k word0)
230      let c1 := c1 ^^^ (← braidBigTab k word1)
231      let c2 := c2 ^^^ (← braidBigTab k word2)
232      let c3 := c3 ^^^ (← braidBigTab k word3)
233      let c4 := c4 ^^^ (← braidBigTab k word4)
234      pure (c0, c1, c2, c3, c4, k + 1)) (crc0, crc1, crc2, crc3, crc4, (1 : Int32))
235  pure { s with crc0, crc1, crc2, crc3, crc4, words }
236
237/-- `crc = (crc >> 8) ^ crc_table[(crc ^ *buf++) & 0xff];` -/
238def crcByte (crc : UInt64) (buf : BPtr) : M (UInt64 × BPtr) := do
239  let b ← load8 buf
240  let buf ← buf.add 1
241  let t ← crcTab ((crc ^^^ b.toUInt64) &&& 0xff)
242  pure ((crc >>> 8) ^^^ t.toUInt64, buf)
243
244/-- `uLong ZEXPORT crc32_z(uLong crc, const unsigned char FAR *buf, z_size_t len)` -/
245def crc32_z (crc : UInt64) (buf : BPtr) (len : UInt64) : M UInt64 := do
246  -- if (buf == Z_NULL) return 0;
247  if buf == .null then return 0
248  -- crc = (~crc) & 0xffffffff;
249  let mut crc := (~~~crc) &&& 0xffffffff
250  let mut buf := buf
251  let mut len := len
252  -- if (len >= N * W + W - 1) {
253  if len ≥ (N * W + W - 1).toInt.toNat.toUInt64 then
254    -- while (len && ((z_size_t)buf & (W - 1)) != 0) { len--; crc = (crc >> 8) ^ crc_table[(crc ^ *buf++) & 0xff]; }
255    let (c, b, l) ← cwhile
256      (fun (c, b, l) => do
257        if l == 0 then pure (false, (c, b, l))
258        else pure ((← addrOf b) &&& (W - 1).toInt.toNat.toUInt64 != 0, (c, b, l)))
259      (fun (c, b, l) => do
260        let l := l - 1
261        let (c, b) ← crcByte c b
262        pure (c, b, l)) (crc, buf, len)
263    crc := c; buf := b; len := l
264    -- blks = len / (N * W); len -= blks * N * W; words = (z_word_t const *)buf;
265    let nw : UInt64 := (N * W).toInt.toNat.toUInt64
266    let blks := len / nw
267    len := len - blks * nw
268    let words := buf
269    -- endian = 1;
270    let endian : UInt32 := 1
271    -- if (*(unsigned char *)&endian) {   /* Little endian. */
272    if endian.toUInt8 != 0 then
273      -- crc0 = (z_crc_t)crc; crc1 = 0; ... crc4 = 0;
274      let s : BL := { crc0 := crc.toUInt32, crc1 := 0, crc2 := 0, crc3 := 0, crc4 := 0, words, blks }
275      -- while (--blks) { ... }
276      let s ← cwhile (fun s => let blks := s.blks - 1; pure (blks != 0, { s with blks })) blockLittle s
277      -- crc = crc_word(crc0 ^ words[0]);
278      crc := (← crc_word (s.crc0.toUInt64 ^^^ (← wordAt s.words 0))).toUInt64
279      -- crc = crc_word(crc1 ^ words[1] ^ crc); ... crc4
280      crc := (← crc_word (s.crc1.toUInt64 ^^^ (← wordAt s.words 1) ^^^ crc)).toUInt64
281      crc := (← crc_word (s.crc2.toUInt64 ^^^ (← wordAt s.words 2) ^^^ crc)).toUInt64
282      crc := (← crc_word (s.crc3.toUInt64 ^^^ (← wordAt s.words 3) ^^^ crc)).toUInt64
283      crc := (← crc_word (s.crc4.toUInt64 ^^^ (← wordAt s.words 4) ^^^ crc)).toUInt64
284      -- words += N;
285      buf := ← s.words.add 40
286    else
287      -- /* Big endian. */ crc0 = byte_swap(crc); crc1 = 0; ... crc4 = 0;
288      let s : BB := { crc0 := byte_swap crc, crc1 := 0, crc2 := 0, crc3 := 0, crc4 := 0, words, blks }
289      let s ← cwhile (fun s => let blks := s.blks - 1; pure (blks != 0, { s with blks })) blockBig s
290      -- comb = crc_word_big(crc0 ^ words[0]); comb = crc_word_big(crc1 ^ words[1] ^ comb); ...
291      let comb ← crc_word_big (s.crc0 ^^^ (← wordAt s.words 0))
292      let comb ← crc_word_big (s.crc1 ^^^ (← wordAt s.words 1) ^^^ comb)
293      let comb ← crc_word_big (s.crc2 ^^^ (← wordAt s.words 2) ^^^ comb)
294      let comb ← crc_word_big (s.crc3 ^^^ (← wordAt s.words 3) ^^^ comb)
295      let comb ← crc_word_big (s.crc4 ^^^ (← wordAt s.words 4) ^^^ comb)
296      -- words += N; crc = byte_swap(comb);
297      let words ← s.words.add 40
298      crc := byte_swap comb
299      -- buf = (unsigned char const *)words;
300      buf := words
301    -- (little endian: buf = (unsigned char const *)words;  done above)
302  -- while (len >= 8) { len -= 8; eight times: crc = (crc >> 8) ^ crc_table[(crc ^ *buf++) & 0xff]; }
303  let (c, b, l) ← cwhile (fun (c, b, l) => pure (l ≥ 8, (c, b, l)))
304    (fun (c, b, l) => do
305      let l := l - 8
306      let (c, b) ← crcByte c b
307      let (c, b) ← crcByte c b
308      let (c, b) ← crcByte c b
309      let (c, b) ← crcByte c b
310      let (c, b) ← crcByte c b
311      let (c, b) ← crcByte c b
312      let (c, b) ← crcByte c b
313      let (c, b) ← crcByte c b
314      pure (c, b, l)) (crc, buf, len)
315  crc := c; buf := b; len := l
316  -- while (len) { len--; crc = (crc >> 8) ^ crc_table[(crc ^ *buf++) & 0xff]; }
317  let (c, _, _) ← cwhile (fun (c, b, l) => pure (l != 0, (c, b, l)))
318    (fun (c, b, l) => do
319      let l := l - 1
320      let (c, b) ← crcByte c b
321      pure (c, b, l)) (crc, buf, len)
322  -- return crc ^ 0xffffffff;
323  pure (c ^^^ 0xffffffff)
324
325/-- `uLong ZEXPORT crc32(uLong crc, const unsigned char FAR *buf, uInt len)` -/
326def crc32 (crc : UInt64) (buf : BPtr) (len : UInt32) : M UInt64 :=
327  -- return crc32_z(crc, buf, len);
328  crc32_z crc buf len.toUInt64
329
330/-- `uLong ZEXPORT crc32_combine_gen64(z_off64_t len2)` -/
331def crc32_combine_gen64 (len2 : Int64) : M UInt64 := do
332  -- if (len2 < 0) return 0;
333  if len2 < 0 then return 0
334  -- return x2nmodp(len2, 3);
335  x2nmodp len2 3
336
337/-- `uLong ZEXPORT crc32_combine_gen(z_off_t len2)` -/
338def crc32_combine_gen (len2 : Int64) : M UInt64 :=
339  -- return crc32_combine_gen64((z_off64_t)len2);
340  crc32_combine_gen64 len2
341
342/-- `uLong ZEXPORT crc32_combine_op(uLong crc1, uLong crc2, uLong op)` -/
343def crc32_combine_op (crc1 crc2 op : UInt64) : M UInt64 := do
344  -- if (op == 0) return 0;
345  if op == 0 then return 0
346  -- return multmodp(op, crc1 & 0xffffffff) ^ (crc2 & 0xffffffff);
347  let m ← multmodp op (crc1 &&& 0xffffffff)
348  pure (m ^^^ (crc2 &&& 0xffffffff))
349
350/-- `uLong ZEXPORT crc32_combine64(uLong crc1, uLong crc2, z_off64_t len2)` -/
351def crc32_combine64 (crc1 crc2 : UInt64) (len2 : Int64) : M UInt64 := do
352  -- return crc32_combine_op(crc1, crc2, crc32_combine_gen64(len2));
353  crc32_combine_op crc1 crc2 (← crc32_combine_gen64 len2)
354
355/-- `uLong ZEXPORT crc32_combine(uLong crc1, uLong crc2, z_off_t len2)` -/
356def crc32_combine (crc1 crc2 : UInt64) (len2 : Int64) : M UInt64 :=
357  -- return crc32_combine64(crc1, crc2, (z_off64_t)len2);
358  crc32_combine64 crc1 crc2 len2
359
360end Zlib.Crc32