table.bend

bend-osdev-crc@0.1.0.0 · 146 lines · 21 definitions

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.
8import Base
9import bend-osdev-word64@0.1.0.0/word64.bend as W
10import bend-osdev-bytes@0.1.0.0/bytes.bend as B
11import bend-osdev-crc@0.1.0.0/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
16def 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
23def 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
30def 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]
35def 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
43def 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
48def 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
56def 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
62def 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
72def 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
81def 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
86def 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
91def 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
98def 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
105def 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
109def 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
117def 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
121def 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
129def t64.snd(r: Array<W.W64> & W.W64) -> W.W64:
130  (t, v) = r
131  v
132
133def 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
140def 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
145def 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))