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.
16	import Base
17	import bend-osdev-word64@0.1.0.0/word64.bend as W
18	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
19	
20	type Crc32Spec is Data:
21	  Crc32Spec{width: Nat, poly: U32, init: U32, reflected: Bool, xorout: U32}
22	
23	type 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	
28	def 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	
35	def reflect32(x: U32, n: Nat) -> U32:
36	  reflect32.go(n, x, 0)
37	
38	def 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	
45	def 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	
50	def 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	
57	def 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)
65	def 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	
74	def 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	
81	def 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
89	def 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	
100	def 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
108	def 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	
115	def 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	
124	def 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	
131	def 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	
138	def 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	
145	def 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	
152	def 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	
159	def 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
170	def 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
180	def 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	
187	def 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
193	def 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	
200	def Crc32Spec.start(spec: Crc32Spec) -> U32:
201	  match spec:
202	    case Crc32Spec{+width, poly, init, reflected, xorout}:
203	      Crc32Spec.start.go(reflected, init, width)
204	
205	def Crc32Spec.finish(spec: Crc32Spec, c: U32) -> U32:
206	  match spec:
207	    case Crc32Spec{width, poly, init, reflected, xorout}:
208	      U32.xor(c, xorout)
209	
210	def Crc32Spec.compute(+spec: Crc32Spec, xs: B.Octets) -> U32:
211	  Crc32Spec.finish(spec, Crc32Spec.update(spec, Crc32Spec.start(spec), xs))
212	
213	def 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	
220	def 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	
225	def 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	
232	def Crc64Spec.start(spec: Crc64Spec) -> W.W64:
233	  match spec:
234	    case Crc64Spec{poly, init, reflected, xorout}:
235	      Crc64Spec.start.go(reflected, init)
236	
237	def 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	
242	def 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
248	def crc32c.spec() -> Crc32Spec:
249	  Crc32Spec{32n, 517762881, 4294967295, True{}, 4294967295}
250	
251	# CRC-32 (ISO-HDLC, as zlib and Ethernet): poly 0x04C11DB7
252	def crc32.spec() -> Crc32Spec:
253	  Crc32Spec{32n, 79764919, 4294967295, True{}, 4294967295}
254	
255	# CRC-16/ARC (the kernel's crc16): poly 0x8005
256	def crc16.spec() -> Crc32Spec:
257	  Crc32Spec{16n, 32773, 0, True{}, 0}
258	
259	# CRC-16/T10-DIF: poly 0x8BB7
260	def crc_t10dif.spec() -> Crc32Spec:
261	  Crc32Spec{16n, 35767, 0, False{}, 0}
262	
263	# CRC-64/ECMA-182: poly 0x42F0E1EBA9EA3693, most significant bit first
264	def 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
268	def 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
272	def 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
276	def crc4_itu.spec() -> Crc32Spec:
277	  Crc32Spec{4n, 3, 0, True{}, 0}
278	
279	# CRC-7/MMC (SD/MMC commands): poly 0x09
280	def crc7_mmc.spec() -> Crc32Spec:
281	  Crc32Spec{7n, 9, 0, False{}, 0}
282	
283	# CRC-8/SMBUS: poly 0x07
284	def 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
288	def crc8_itu.spec() -> Crc32Spec:
289	  Crc32Spec{8n, 7, 0, False{}, 85}
290	
291	# CRC-8/MAXIM-DOW (Dallas/Maxim 1-Wire): poly 0x31, reflected
292	def crc8_maxim.spec() -> Crc32Spec:
293	  Crc32Spec{8n, 49, 0, True{}, 0}
294	
295	# CRC-8/DVB-S2: poly 0xD5
296	def crc8_dvb_s2.spec() -> Crc32Spec:
297	  Crc32Spec{8n, 213, 0, False{}, 0}
298	
299	# CRC-8/AUTOSAR: poly 0x2F, init 0xFF, xorout 0xFF
300	def 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
304	def 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
308	def 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
312	def crc16_xmodem.spec() -> Crc32Spec:
313	  Crc32Spec{16n, 4129, 0, False{}, 0}
314	
315	def crc32c(xs: B.Octets) -> U32:
316	  Crc32Spec.compute(crc32c.spec(), xs)
317	
318	def crc32(xs: B.Octets) -> U32:
319	  Crc32Spec.compute(crc32.spec(), xs)
320	
321	def crc16(xs: B.Octets) -> U32:
322	  Crc32Spec.compute(crc16.spec(), xs)
323	
324	def crc_t10dif(xs: B.Octets) -> U32:
325	  Crc32Spec.compute(crc_t10dif.spec(), xs)
326	
327	def crc64_ecma(xs: B.Octets) -> W.W64:
328	  Crc64Spec.compute(crc64_ecma.spec(), xs)
329	
330	def crc64_xz(xs: B.Octets) -> W.W64:
331	  Crc64Spec.compute(crc64_xz.spec(), xs)
332	
333	def crc64_nvme(xs: B.Octets) -> W.W64:
334	  Crc64Spec.compute(crc64_nvme.spec(), xs)
335	
336	def crc4_itu(xs: B.Octets) -> U32:
337	  Crc32Spec.compute(crc4_itu.spec(), xs)
338	
339	def crc7_mmc(xs: B.Octets) -> U32:
340	  Crc32Spec.compute(crc7_mmc.spec(), xs)
341	
342	def crc8_smbus(xs: B.Octets) -> U32:
343	  Crc32Spec.compute(crc8_smbus.spec(), xs)
344	
345	def crc8_itu(xs: B.Octets) -> U32:
346	  Crc32Spec.compute(crc8_itu.spec(), xs)
347	
348	def crc8_maxim(xs: B.Octets) -> U32:
349	  Crc32Spec.compute(crc8_maxim.spec(), xs)
350	
351	def crc8_dvb_s2(xs: B.Octets) -> U32:
352	  Crc32Spec.compute(crc8_dvb_s2.spec(), xs)
353	
354	def crc8_autosar(xs: B.Octets) -> U32:
355	  Crc32Spec.compute(crc8_autosar.spec(), xs)
356	
357	def crc16_kermit(xs: B.Octets) -> U32:
358	  Crc32Spec.compute(crc16_kermit.spec(), xs)
359	
360	def crc16_ccitt_false(xs: B.Octets) -> U32:
361	  Crc32Spec.compute(crc16_ccitt_false.spec(), xs)
362	
363	def crc16_xmodem(xs: B.Octets) -> U32:
364	  Crc32Spec.compute(crc16_xmodem.spec(), xs)