crc.bend

bend-osdev-crc@0.1.0.0 · 364 lines · 68 definitions

1# bend-osdev-crc: cyclic redundancy checks, in the Rocksoft parameter model
2# (Ross Williams, "A Painless Guide to CRC Error Detection Algorithms", 1993;
3# the catalogue of parameters at reveng.sourceforge.io).
4#
5# A CRC is fixed by its width, polynomial (in normal, most-significant-first
6# form), initial register value, bit order, and final XOR. Crc32Spec covers
7# widths 1 to 32 on U32 (below 8, most-significant-first CRCs take their
8# input a bit at a time); Crc64Spec covers width 64 on W64. Every CRC here
9# reads its input bytes in the same order it writes its result (refin =
10# refout), as all the CRCs below do.
11#
12# The kernel's CRCs as named variants: crc32c (iSCSI, ext4, btrfs), crc16 (the
13# ARC variant: ext4's group descriptors), crc_t10dif (SCSI data integrity),
14# crc64_ecma, crc64_xz and crc64_nvme. crc32 (ISO-HDLC) is here as a
15# cross-check against implementations outside this repository.
16import Base
17import bend-osdev-word64@0.1.0.0/word64.bend as W
18import bend-osdev-bytes@0.1.0.0/bytes.bend as B
19
20type Crc32Spec is Data:
21  Crc32Spec{width: Nat, poly: U32, init: U32, reflected: Bool, xorout: U32}
22
23type Crc64Spec is Data:
24  Crc64Spec{poly: W.W64, init: W.W64, reflected: Bool, xorout: W.W64}
25
26# Reflection: the low n bits of a word in reverse order
27
28def reflect32.go(n: Nat, +x: U32, r: U32) -> U32:
29  match n:
30    case 0n:
31      r
32    case 1n+p:
33      reflect32.go(p, U32.shr(x), U32.or(U32.shl(r), U32.and(x, 1)))
34
35def reflect32(x: U32, n: Nat) -> U32:
36  reflect32.go(n, x, 0)
37
38def reflect64.go(n: Nat, +x: W.W64, r: W.W64) -> W.W64:
39  match n:
40    case 0n:
41      r
42    case 1n+p:
43      reflect64.go(p, W.W64.shr(x, 1n), W.W64.or(W.W64.shl(r, 1n), W.W64.and(x, W.W64.one())))
44
45def reflect64(x: W.W64) -> W.W64:
46  reflect64.go(64n, x, W.W64.zero())
47
48# The 32-bit engine, least significant bit first (reflected)
49
50def r32.pick(odd: Bool, +poly: U32, c: U32) -> U32:
51  match odd:
52    case True{}:
53      U32.xor(U32.shr(c), poly)
54    case False{}:
55      U32.shr(c)
56
57def r32.bits(n: Nat, +poly: U32, +c: U32) -> U32:
58  match n:
59    case 0n:
60      c
61    case 1n+p:
62      r32.bits(p, poly, r32.pick(U32.is_eq(U32.and(c, 1), 1), poly, c))
63
64# the register after the bytes xs, from register c (poly reflected)
65def r32.raw(xs: List<&2, U32>, +poly: U32, c: U32) -> U32:
66  match xs:
67    case Nil{}:
68      c
69    case Con{h, t}:
70      r32.raw(t, poly, r32.bits(8n, poly, U32.xor(c, U32.and(h, 255))))
71
72# The 32-bit engine, most significant bit first
73
74def n32.pick(top: Bool, +poly: U32, +mask: U32, c: U32) -> U32:
75  match top:
76    case True{}:
77      U32.and(U32.xor(U32.shl(c), poly), mask)
78    case False{}:
79      U32.and(U32.shl(c), mask)
80
81def n32.bits(n: Nat, +poly: U32, +topbit: U32, +mask: U32, +c: U32) -> U32:
82  match n:
83    case 0n:
84      c
85    case 1n+p:
86      n32.bits(p, poly, topbit, mask, n32.pick(Bool.not(U32.is_eq(U32.and(c, topbit), 0)), poly, mask, c))
87
88# the register after the bytes xs, from register c; shift is width - 8
89def n32.raw(xs: List<&2, U32>, +poly: U32, +shift: Nat, +topbit: U32, +mask: U32, c: U32) -> U32:
90  match xs:
91    case Nil{}:
92      c
93    case Con{h, t}:
94      n32.raw(t, poly, shift, topbit, mask, n32.bits(8n, poly, topbit, mask, U32.xor(c, U32.shln(U32.and(h, 255), shift))))
95
96# The 32-bit engine for widths below 8, most significant bit first: a byte
97# does not fit at the register's top, so its bits enter one at a time (the
98# input bit is added to the bit leaving the top); topsh is width - 1
99
100def s32.pick(top: Bool, +poly: U32, +mask: U32, c: U32) -> U32:
101  match top:
102    case True{}:
103      U32.and(U32.xor(U32.shl(c), poly), mask)
104    case False{}:
105      U32.and(U32.shl(c), mask)
106
107# the bits p - 1 down to 0 of h, into register c
108def s32.bits(+n: Nat, +poly: U32, +topsh: Nat, +mask: U32, +h: U32, +c: U32) -> U32:
109  match n:
110    case 0n:
111      c
112    case 1n+p:
113      s32.bits(p, poly, topsh, mask, h, s32.pick(U32.is_eq(U32.and(U32.xor(U32.shrn(c, topsh), U32.shrn(h, p)), 1), 1), poly, mask, c))
114
115def s32.raw(xs: List<&2, U32>, +poly: U32, +topsh: Nat, +mask: U32, c: U32) -> U32:
116  match xs:
117    case Nil{}:
118      c
119    case Con{h, t}:
120      s32.raw(t, poly, topsh, mask, s32.bits(8n, poly, topsh, mask, U32.and(h, 255), c))
121
122# The 64-bit engines
123
124def r64.pick(odd: Bool, +poly: W.W64, c: W.W64) -> W.W64:
125  match odd:
126    case True{}:
127      W.W64.xor(W.W64.shr(c, 1n), poly)
128    case False{}:
129      W.W64.shr(c, 1n)
130
131def r64.bits(n: Nat, +poly: W.W64, +c: W.W64) -> W.W64:
132  match n:
133    case 0n:
134      c
135    case 1n+p:
136      r64.bits(p, poly, r64.pick(U32.is_eq(U32.and(W.W64.lo(c), 1), 1), poly, c))
137
138def r64.raw(xs: List<&2, U32>, +poly: W.W64, c: W.W64) -> W.W64:
139  match xs:
140    case Nil{}:
141      c
142    case Con{h, t}:
143      r64.raw(t, poly, r64.bits(8n, poly, W.W64.xor(c, W.W64.from_u32(U32.and(h, 255)))))
144
145def n64.pick(top: Bool, +poly: W.W64, c: W.W64) -> W.W64:
146  match top:
147    case True{}:
148      W.W64.xor(W.W64.shl(c, 1n), poly)
149    case False{}:
150      W.W64.shl(c, 1n)
151
152def n64.bits(n: Nat, +poly: W.W64, +c: W.W64) -> W.W64:
153  match n:
154    case 0n:
155      c
156    case 1n+p:
157      n64.bits(p, poly, n64.pick(Bool.not(U32.is_eq(U32.and(W.W64.hi(c), 2147483648), 0)), poly, c))
158
159def n64.raw(xs: List<&2, U32>, +poly: W.W64, c: W.W64) -> W.W64:
160  match xs:
161    case Nil{}:
162      c
163    case Con{h, t}:
164      n64.raw(t, poly, n64.bits(8n, poly, W.W64.xor(c, W.W64.from_parts(U32.shln(U32.and(h, 255), 24n), 0))))
165
166# The generic CRCs
167
168# most significant bit first: the byte engine for widths of 8 and up, the
169# bit engine below
170def Crc32Spec.update.msb(small: Bool, +width: Nat, poly: U32, c: U32, xs: List<&2, U32>) -> U32:
171  match small:
172    case True{}:
173      s32.raw(xs, poly, Nat.sub(width, 1n), U32.sub(U32.shln(1, width), 1), c)
174    case False{}:
175      +shift = Nat.sub(width, 8n)
176      n32.raw(xs, poly, shift, U32.shln(1, Nat.sub(width, 1n)), U32.sub(U32.shln(1, width), 1), c)
177
178# the register after the bytes xs, from register c, without the final XOR:
179# what a caller that computes a CRC in pieces passes from one piece to the next
180def Crc32Spec.update.go(reflected: Bool, +width: Nat, poly: U32, c: U32, xs: List<&2, U32>) -> U32:
181  match reflected:
182    case True{}:
183      r32.raw(xs, reflect32(poly, width), c)
184    case False{}:
185      Crc32Spec.update.msb(Nat.is_lt(width, 8n), width, poly, c, xs)
186
187def Crc32Spec.update(spec: Crc32Spec, c: U32, o: B.Octets) -> U32:
188  match spec:
189    case Crc32Spec{+width, poly, init, reflected, xorout}:
190      Crc32Spec.update.go(reflected, width, poly, c, B.Octets.to_list(o))
191
192# the register a CRC starts from
193def Crc32Spec.start.go(reflected: Bool, init: U32, width: Nat) -> U32:
194  match reflected:
195    case True{}:
196      reflect32(init, width)
197    case False{}:
198      init
199
200def Crc32Spec.start(spec: Crc32Spec) -> U32:
201  match spec:
202    case Crc32Spec{+width, poly, init, reflected, xorout}:
203      Crc32Spec.start.go(reflected, init, width)
204
205def Crc32Spec.finish(spec: Crc32Spec, c: U32) -> U32:
206  match spec:
207    case Crc32Spec{width, poly, init, reflected, xorout}:
208      U32.xor(c, xorout)
209
210def Crc32Spec.compute(+spec: Crc32Spec, xs: B.Octets) -> U32:
211  Crc32Spec.finish(spec, Crc32Spec.update(spec, Crc32Spec.start(spec), xs))
212
213def Crc64Spec.update.go(reflected: Bool, poly: W.W64, c: W.W64, xs: List<&2, U32>) -> W.W64:
214  match reflected:
215    case True{}:
216      r64.raw(xs, reflect64(poly), c)
217    case False{}:
218      n64.raw(xs, poly, c)
219
220def Crc64Spec.update(spec: Crc64Spec, c: W.W64, o: B.Octets) -> W.W64:
221  match spec:
222    case Crc64Spec{poly, init, reflected, xorout}:
223      Crc64Spec.update.go(reflected, poly, c, B.Octets.to_list(o))
224
225def Crc64Spec.start.go(reflected: Bool, init: W.W64) -> W.W64:
226  match reflected:
227    case True{}:
228      reflect64(init)
229    case False{}:
230      init
231
232def Crc64Spec.start(spec: Crc64Spec) -> W.W64:
233  match spec:
234    case Crc64Spec{poly, init, reflected, xorout}:
235      Crc64Spec.start.go(reflected, init)
236
237def Crc64Spec.finish(spec: Crc64Spec, c: W.W64) -> W.W64:
238  match spec:
239    case Crc64Spec{poly, init, reflected, xorout}:
240      W.W64.xor(c, xorout)
241
242def Crc64Spec.compute(+spec: Crc64Spec, xs: B.Octets) -> W.W64:
243  Crc64Spec.finish(spec, Crc64Spec.update(spec, Crc64Spec.start(spec), xs))
244
245# The named CRCs (parameters from the reveng catalogue)
246
247# CRC-32C (Castagnoli): poly 0x1EDC6F41
248def crc32c.spec() -> Crc32Spec:
249  Crc32Spec{32n, 517762881, 4294967295, True{}, 4294967295}
250
251# CRC-32 (ISO-HDLC, as zlib and Ethernet): poly 0x04C11DB7
252def crc32.spec() -> Crc32Spec:
253  Crc32Spec{32n, 79764919, 4294967295, True{}, 4294967295}
254
255# CRC-16/ARC (the kernel's crc16): poly 0x8005
256def crc16.spec() -> Crc32Spec:
257  Crc32Spec{16n, 32773, 0, True{}, 0}
258
259# CRC-16/T10-DIF: poly 0x8BB7
260def crc_t10dif.spec() -> Crc32Spec:
261  Crc32Spec{16n, 35767, 0, False{}, 0}
262
263# CRC-64/ECMA-182: poly 0x42F0E1EBA9EA3693, most significant bit first
264def crc64_ecma.spec() -> Crc64Spec:
265  Crc64Spec{W.W64.from_parts(1123082731, 2850698899), W.W64.zero(), False{}, W.W64.zero()}
266
267# CRC-64/XZ: the same polynomial, reflected, as the XZ format's check
268def crc64_xz.spec() -> Crc64Spec:
269  Crc64Spec{W.W64.from_parts(1123082731, 2850698899), W.W64.max(), True{}, W.W64.max()}
270
271# CRC-64/NVME: poly 0xAD93D23594C93659
272def crc64_nvme.spec() -> Crc64Spec:
273  Crc64Spec{W.W64.from_parts(2912145973, 2496214617), W.W64.max(), True{}, W.W64.max()}
274
275# CRC-4/G-704 (CRC-4/ITU): poly 0x3, reflected
276def crc4_itu.spec() -> Crc32Spec:
277  Crc32Spec{4n, 3, 0, True{}, 0}
278
279# CRC-7/MMC (SD/MMC commands): poly 0x09
280def crc7_mmc.spec() -> Crc32Spec:
281  Crc32Spec{7n, 9, 0, False{}, 0}
282
283# CRC-8/SMBUS: poly 0x07
284def crc8_smbus.spec() -> Crc32Spec:
285  Crc32Spec{8n, 7, 0, False{}, 0}
286
287# CRC-8/I-432-1 (CRC-8/ITU, ATM HEC): poly 0x07, xorout 0x55
288def crc8_itu.spec() -> Crc32Spec:
289  Crc32Spec{8n, 7, 0, False{}, 85}
290
291# CRC-8/MAXIM-DOW (Dallas/Maxim 1-Wire): poly 0x31, reflected
292def crc8_maxim.spec() -> Crc32Spec:
293  Crc32Spec{8n, 49, 0, True{}, 0}
294
295# CRC-8/DVB-S2: poly 0xD5
296def crc8_dvb_s2.spec() -> Crc32Spec:
297  Crc32Spec{8n, 213, 0, False{}, 0}
298
299# CRC-8/AUTOSAR: poly 0x2F, init 0xFF, xorout 0xFF
300def crc8_autosar.spec() -> Crc32Spec:
301  Crc32Spec{8n, 47, 255, False{}, 255}
302
303# CRC-16/KERMIT (CRC-16/CCITT, the kernel's crc_ccitt): poly 0x1021, reflected
304def crc16_kermit.spec() -> Crc32Spec:
305  Crc32Spec{16n, 4129, 0, True{}, 0}
306
307# CRC-16/IBM-3740 (CRC-16/CCITT-FALSE): poly 0x1021, init 0xFFFF
308def crc16_ccitt_false.spec() -> Crc32Spec:
309  Crc32Spec{16n, 4129, 65535, False{}, 0}
310
311# CRC-16/XMODEM (CRC-16/ITU-T, the kernel's crc_itu_t): poly 0x1021
312def crc16_xmodem.spec() -> Crc32Spec:
313  Crc32Spec{16n, 4129, 0, False{}, 0}
314
315def crc32c(xs: B.Octets) -> U32:
316  Crc32Spec.compute(crc32c.spec(), xs)
317
318def crc32(xs: B.Octets) -> U32:
319  Crc32Spec.compute(crc32.spec(), xs)
320
321def crc16(xs: B.Octets) -> U32:
322  Crc32Spec.compute(crc16.spec(), xs)
323
324def crc_t10dif(xs: B.Octets) -> U32:
325  Crc32Spec.compute(crc_t10dif.spec(), xs)
326
327def crc64_ecma(xs: B.Octets) -> W.W64:
328  Crc64Spec.compute(crc64_ecma.spec(), xs)
329
330def crc64_xz(xs: B.Octets) -> W.W64:
331  Crc64Spec.compute(crc64_xz.spec(), xs)
332
333def crc64_nvme(xs: B.Octets) -> W.W64:
334  Crc64Spec.compute(crc64_nvme.spec(), xs)
335
336def crc4_itu(xs: B.Octets) -> U32:
337  Crc32Spec.compute(crc4_itu.spec(), xs)
338
339def crc7_mmc(xs: B.Octets) -> U32:
340  Crc32Spec.compute(crc7_mmc.spec(), xs)
341
342def crc8_smbus(xs: B.Octets) -> U32:
343  Crc32Spec.compute(crc8_smbus.spec(), xs)
344
345def crc8_itu(xs: B.Octets) -> U32:
346  Crc32Spec.compute(crc8_itu.spec(), xs)
347
348def crc8_maxim(xs: B.Octets) -> U32:
349  Crc32Spec.compute(crc8_maxim.spec(), xs)
350
351def crc8_dvb_s2(xs: B.Octets) -> U32:
352  Crc32Spec.compute(crc8_dvb_s2.spec(), xs)
353
354def crc8_autosar(xs: B.Octets) -> U32:
355  Crc32Spec.compute(crc8_autosar.spec(), xs)
356
357def crc16_kermit(xs: B.Octets) -> U32:
358  Crc32Spec.compute(crc16_kermit.spec(), xs)
359
360def crc16_ccitt_false(xs: B.Octets) -> U32:
361  Crc32Spec.compute(crc16_ccitt_false.spec(), xs)
362
363def crc16_xmodem(xs: B.Octets) -> U32:
364  Crc32Spec.compute(crc16_xmodem.spec(), xs)