1	# bend-osdev-crc, the table-driven fast path: one table lookup per byte
2	# instead of eight bit steps (about 3x faster for CRC32C on native builds).
3	#
4	# The bitwise engines in crc.bend are the reference; these must give the same
5	# results, which the vectors in LAWS.bend and ref/run.sh check (a law for
6	# every input is out of reach: it would need lemmas about Array's internals).
7	# The table is an Array, so it is built once per call and threaded through.
8	import Base
9	import bend-osdev-word64@0.1.0.0/word64.bend as W
10	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
11	import ./crc.bend as C
12	
13	# 32-bit tables: entry i is eight bit steps of the register i (reflected), or
14	# of i placed in the register's top byte (most significant bit first)
15	
16	def t32.fill.r(n: Nat, a: Array<U32>, +poly: U32, +i: U32) -> Array<U32>:
17	  match n:
18	    case 0n:
19	      a
20	    case 1n+p:
21	      t32.fill.r(p, Array.set(U32, a, i, C.r32.bits(8n, poly, i)), poly, U32.add(i, 1))
22	
23	def t32.fill.n(n: Nat, a: Array<U32>, +poly: U32, +shift: Nat, +topbit: U32, +mask: U32, +i: U32) -> Array<U32>:
24	  match n:
25	    case 0n:
26	      a
27	    case 1n+p:
28	      t32.fill.n(p, Array.set(U32, a, i, C.n32.bits(8n, poly, topbit, mask, U32.shln(i, shift))), poly, shift, topbit, mask, U32.add(i, 1))
29	
30	def t32.r.fin(r: Array<U32> & U32, +c: U32) -> Array<U32> & U32:
31	  (t, v) = r
32	  (t, U32.xor(U32.shrn(c, 8n), v))
33	
34	# reflected: c = (c >> 8) ^ T[(c ^ b) & 255]
35	def t32.r.raw(xs: List<&2, U32>, r: Array<U32> & U32) -> Array<U32> & U32:
36	  match xs:
37	    case Nil{}:
38	      r
39	    case Con{h, t}:
40	      (tab, +c) = r
41	      t32.r.raw(t, t32.r.fin(Array.get(U32, tab, U32.and(U32.xor(c, h), 255)), c))
42	
43	def t32.n.fin(r: Array<U32> & U32, +c: U32, +mask: U32) -> Array<U32> & U32:
44	  (t, v) = r
45	  (t, U32.and(U32.xor(U32.shln(c, 8n), v), mask))
46	
47	# most significant bit first: c = ((c << 8) ^ T[((c >> (w - 8)) ^ b) & 255]) & mask
48	def t32.n.raw(xs: List<&2, U32>, +shift: Nat, +mask: U32, r: Array<U32> & U32) -> Array<U32> & U32:
49	  match xs:
50	    case Nil{}:
51	      r
52	    case Con{h, t}:
53	      (tab, +c) = r
54	      t32.n.raw(t, shift, mask, t32.n.fin(Array.get(U32, tab, U32.and(U32.xor(U32.shrn(c, shift), h), 255)), c, mask))
55	
56	def t32.snd(r: Array<U32> & U32) -> U32:
57	  (t, v) = r
58	  v
59	
60	# most significant bit first: a table for widths of 8 and up; below 8 the
61	# input goes in a bit at a time, so the bitwise engine serves
62	def t32.update.msb(small: Bool, +width: Nat, +poly: U32, c: U32, xs: List<&2, U32>) -> U32:
63	  match small:
64	    case True{}:
65	      C.s32.raw(xs, poly, Nat.sub(width, 1n), U32.sub(U32.shln(1, width), 1), c)
66	    case False{}:
67	      +shift = Nat.sub(width, 8n)
68	      +topbit = U32.shln(1, Nat.sub(width, 1n))
69	      +mask = U32.sub(U32.shln(1, width), 1)
70	      t32.snd(t32.n.raw(xs, shift, mask, (t32.fill.n(256n, [0 : U32*256n], poly, shift, topbit, mask, 0), c)))
71	
72	def t32.update.go(reflected: Bool, +width: Nat, +poly: U32, c: U32, xs: List<&2, U32>) -> U32:
73	  match reflected:
74	    case True{}:
75	      +rp = C.reflect32(poly, width)
76	      t32.snd(t32.r.raw(xs, (t32.fill.r(256n, [0 : U32*256n], rp, 0), c)))
77	    case False{}:
78	      t32.update.msb(Nat.is_lt(width, 8n), width, poly, c, xs)
79	
80	# the same as Crc32Spec.update, table-driven
81	def Crc32Spec.update_fast(spec: C.Crc32Spec, c: U32, o: B.Octets) -> U32:
82	  match spec:
83	    case C.Crc32Spec{+width, poly, init, reflected, xorout}:
84	      t32.update.go(reflected, width, poly, c, B.Octets.to_list(o))
85	
86	def Crc32Spec.compute_fast(+spec: C.Crc32Spec, o: B.Octets) -> U32:
87	  C.Crc32Spec.finish(spec, Crc32Spec.update_fast(spec, C.Crc32Spec.start(spec), o))
88	
89	# 64-bit tables
90	
91	def t64.fill.r(n: Nat, a: Array<W.W64>, +poly: W.W64, +i: U32) -> Array<W.W64>:
92	  match n:
93	    case 0n:
94	      a
95	    case 1n+p:
96	      t64.fill.r(p, Array.set(W.W64, a, i, C.r64.bits(8n, poly, W.W64.from_u32(i))), poly, U32.add(i, 1))
97	
98	def t64.fill.n(n: Nat, a: Array<W.W64>, +poly: W.W64, +i: U32) -> Array<W.W64>:
99	  match n:
100	    case 0n:
101	      a
102	    case 1n+p:
103	      t64.fill.n(p, Array.set(W.W64, a, i, C.n64.bits(8n, poly, W.W64.from_parts(U32.shln(i, 24n), 0))), poly, U32.add(i, 1))
104	
105	def t64.r.fin(r: Array<W.W64> & W.W64, +c: W.W64) -> Array<W.W64> & W.W64:
106	  (t, v) = r
107	  (t, W.W64.xor(W.W64.shr(c, 8n), v))
108	
109	def t64.r.raw(xs: List<&2, U32>, r: Array<W.W64> & W.W64) -> Array<W.W64> & W.W64:
110	  match xs:
111	    case Nil{}:
112	      r
113	    case Con{h, t}:
114	      (tab, +c) = r
115	      t64.r.raw(t, t64.r.fin(Array.get(W.W64, tab, U32.and(U32.xor(W.W64.lo(c), h), 255)), c))
116	
117	def t64.n.fin(r: Array<W.W64> & W.W64, +c: W.W64) -> Array<W.W64> & W.W64:
118	  (t, v) = r
119	  (t, W.W64.xor(W.W64.shl(c, 8n), v))
120	
121	def t64.n.raw(xs: List<&2, U32>, r: Array<W.W64> & W.W64) -> Array<W.W64> & W.W64:
122	  match xs:
123	    case Nil{}:
124	      r
125	    case Con{h, t}:
126	      (tab, +c) = r
127	      t64.n.raw(t, t64.n.fin(Array.get(W.W64, tab, U32.and(U32.xor(U32.shrn(W.W64.hi(c), 24n), h), 255)), c))
128	
129	def t64.snd(r: Array<W.W64> & W.W64) -> W.W64:
130	  (t, v) = r
131	  v
132	
133	def t64.update.go(reflected: Bool, poly: W.W64, c: W.W64, xs: List<&2, U32>) -> W.W64:
134	  match reflected:
135	    case True{}:
136	      t64.snd(t64.r.raw(xs, (t64.fill.r(256n, Array.new(W.W64, 8n, W.W64.zero()), C.reflect64(poly), 0), c)))
137	    case False{}:
138	      t64.snd(t64.n.raw(xs, (t64.fill.n(256n, Array.new(W.W64, 8n, W.W64.zero()), poly, 0), c)))
139	
140	def Crc64Spec.update_fast(spec: C.Crc64Spec, c: W.W64, o: B.Octets) -> W.W64:
141	  match spec:
142	    case C.Crc64Spec{poly, init, reflected, xorout}:
143	      t64.update.go(reflected, poly, c, B.Octets.to_list(o))
144	
145	def Crc64Spec.compute_fast(+spec: C.Crc64Spec, o: B.Octets) -> W.W64:
146	  C.Crc64Spec.finish(spec, Crc64Spec.update_fast(spec, C.Crc64Spec.start(spec), o))