gf.bend
bend-osdev-gf@0.1.2.0 · 175 lines · 0 definitions
1# bend-osdev-gf: arithmetic in the finite field GF(2^8), with the reduction
2# polynomial as a parameter.
3#
4# GF(2^8) is GF(2)[x] modulo a polynomial of degree 8. An element is a
5# byte: bit i is the coefficient of x^i. Addition is XOR; multiplication is
6# the product of the polynomials, reduced modulo the field's polynomial
7# (FIPS 197, section 4; any algebra text). A Gf8Field names the polynomial
8# (all nine bits, so 0x11B is 283) and a generator of the multiplicative
9# group, used for the exponential and logarithm.
10#
11# Elements are held in U32; only the low 8 bits of an argument are read, and
12# every result is below 256. Inside, a byte is its eight bits (Gf8Bits), and
13# the product is computed by Horner's rule over the bits of the first factor:
14# acc := x * acc + bit * b, from the top bit down. Computing on bits keeps
15# the code short and branch-free, and lets the laws be proved for every
16# polynomial (see LAWS.bend).
17import Base
18
19type Gf8Field is Data:
20 Gf8Field{poly: U32, gen: U32}
21
22# The named fields
23
24# AES (FIPS 197): x^8 + x^4 + x^3 + x + 1 (0x11B), generator x + 1 (3)
25def Gf8.aes() -> Gf8Field:
26 Gf8Field{283, 3}
27
28# Reed-Solomon and RAID-6: x^8 + x^4 + x^3 + x^2 + 1 (0x11D), generator x (2)
29def Gf8.rs() -> Gf8Field:
30 Gf8Field{285, 2}
31
32def Gf8.raid6() -> Gf8Field:
33 Gf8.rs()
34
35def Gf8.poly(f: Gf8Field) -> U32:
36 match f:
37 case Gf8Field{poly, gen}:
38 poly
39
40def Gf8.gen(f: Gf8Field) -> U32:
41 match f:
42 case Gf8Field{poly, gen}:
43 gen
44
45# A byte as its eight bits, b0 the least significant
46
47type Gf8Bits is Data:
48 Gf8Bits{b0: Bool, b1: Bool, b2: Bool, b3: Bool, b4: Bool, b5: Bool, b6: Bool, b7: Bool}
49
50# the low 8 bits of a
51def Gf8Bits.of(a: U32) -> Gf8Bits:
52 match a:
53 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, r}}}}}}}}}:
54 Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}
55
56def Gf8Bits.to(r: Gf8Bits) -> U32:
57 match r:
58 case Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}:
59 U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, Word.zero(24n)}}}}}}}}}
60
61def Gf8Bits.zero() -> Gf8Bits:
62 Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}
63
64def Gf8Bits.xor(a: Gf8Bits, b: Gf8Bits) -> Gf8Bits:
65 match a b:
66 case Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} Gf8Bits{c0, c1, c2, c3, c4, c5, c6, c7}:
67 Gf8Bits{Bool.xor(a0, c0), Bool.xor(a1, c1), Bool.xor(a2, c2), Bool.xor(a3, c3), Bool.xor(a4, c4), Bool.xor(a5, c5), Bool.xor(a6, c6), Bool.xor(a7, c7)}
68
69# a if t, else zero
70def Gf8Bits.sel(t: Bool, a: Gf8Bits) -> Gf8Bits:
71 match t:
72 case True{}:
73 a
74 case False{}:
75 Gf8Bits.zero()
76
77# a times x, where p holds the low 8 bits of the polynomial: shift up one
78# place, and if the coefficient of x^8 was set, add p (x^8 = p in the field)
79def Gf8Bits.x(a: Gf8Bits, p: Gf8Bits) -> Gf8Bits:
80 match a p:
81 case Gf8Bits{a0, a1, a2, a3, a4, a5, a6, +a7} Gf8Bits{p0, p1, p2, p3, p4, p5, p6, p7}:
82 Gf8Bits{Bool.and(a7, p0), Bool.xor(a0, Bool.and(a7, p1)), Bool.xor(a1, Bool.and(a7, p2)), Bool.xor(a2, Bool.and(a7, p3)), Bool.xor(a3, Bool.and(a7, p4)), Bool.xor(a4, Bool.and(a7, p5)), Bool.xor(a5, Bool.and(a7, p6)), Bool.xor(a6, Bool.and(a7, p7))}
83
84# one step of Horner's rule: x * acc + t * b
85def Gf8Bits.step(t: Bool, acc: Gf8Bits, +b: Gf8Bits, +p: Gf8Bits) -> Gf8Bits:
86 Gf8Bits.xor(Gf8Bits.x(acc, p), Gf8Bits.sel(t, b))
87
88# Horner's rule over the bits ts, most significant first
89def Gf8Bits.horner(ts: List<&2, Bool>, acc: Gf8Bits, +b: Gf8Bits, +p: Gf8Bits) -> Gf8Bits:
90 match ts:
91 case Nil{}:
92 acc
93 case Con{t, rest}:
94 Gf8Bits.horner(rest, Gf8Bits.step(t, acc, b, p), b, p)
95
96# the bits of a, most significant first
97def Gf8Bits.top(a: Gf8Bits) -> List<&2, Bool>:
98 match a:
99 case Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}:
100 [b7, b6, b5, b4, b3, b2, b1, b0]
101
102def Gf8Bits.mul(a: Gf8Bits, +b: Gf8Bits, +p: Gf8Bits) -> Gf8Bits:
103 Gf8Bits.horner(Gf8Bits.top(a), Gf8Bits.zero(), b, p)
104
105# The field operations, on bytes held in U32
106
107# the element a: its low 8 bits
108def Gf8.elt(a: U32) -> U32:
109 Gf8Bits.to(Gf8Bits.of(a))
110
111# whether a is the zero element (its low 8 bits are all 0)
112def Gf8Bits.is_zero(a: Gf8Bits) -> Bool:
113 match a:
114 case Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}:
115 Bool.not(Bool.or(b0, Bool.or(b1, Bool.or(b2, Bool.or(b3, Bool.or(b4, Bool.or(b5, Bool.or(b6, b7))))))))
116
117def Gf8.is_zero(a: U32) -> Bool:
118 Gf8Bits.is_zero(Gf8Bits.of(a))
119
120def Gf8.add(a: U32, b: U32) -> U32:
121 Gf8Bits.to(Gf8Bits.xor(Gf8Bits.of(a), Gf8Bits.of(b)))
122
123# subtraction is addition in characteristic 2
124def Gf8.sub(a: U32, b: U32) -> U32:
125 Gf8.add(a, b)
126
127def Gf8.mul(f: Gf8Field, a: U32, b: U32) -> U32:
128 match f:
129 case Gf8Field{poly, gen}:
130 Gf8Bits.to(Gf8Bits.mul(Gf8Bits.of(a), Gf8Bits.of(b), Gf8Bits.of(poly)))
131
132# a times x (FIPS 197's xtime)
133def Gf8.xtime(f: Gf8Field, a: U32) -> U32:
134 match f:
135 case Gf8Field{poly, gen}:
136 Gf8Bits.to(Gf8Bits.x(Gf8Bits.of(a), Gf8Bits.of(poly)))
137
138# a^n, with a^0 = 1 (also for a = 0)
139def Gf8.pow(+f: Gf8Field, +a: U32, n: Nat) -> U32:
140 match n:
141 case 0n:
142 1
143 case 1n+k:
144 Gf8.mul(f, a, Gf8.pow(f, a, k))
145
146# the inverse a^254 (a^255 = 1 for a nonzero); the inverse of 0 is 0, as in
147# the AES S-box
148def Gf8.inv(+f: Gf8Field, +a: U32) -> U32:
149 Gf8.pow(f, a, 254n)
150
151# a / b = a * b^-1 (and a / 0 = 0)
152def Gf8.div(+f: Gf8Field, a: U32, +b: U32) -> U32:
153 Gf8.mul(f, a, Gf8.inv(f, b))
154
155# The exponential and logarithm to the field's generator
156
157# gen^i
158def Gf8.exp(+f: Gf8Field, i: Nat) -> U32:
159 Gf8.pow(f, Gf8.gen(f), i)
160
161# the least i with gen^i = a (searching i = 0 to 254); 0 for a = 0, or when
162# gen does not generate a
163def Gf8.log.go(n: Nat, hit: Bool, +f: Gf8Field, +a: U32, +cur: U32, +i: Nat) -> Nat:
164 match n hit:
165 case _ True{}:
166 i
167 case 0n False{}:
168 0n
169 case 1n+k False{}:
170 +nxt = Gf8.mul(f, Gf8.gen(f), cur)
171 Gf8.log.go(k, U32.is_eq(nxt, a), f, a, nxt, 1n+i)
172
173def Gf8.log(+f: Gf8Field, a: U32) -> Nat:
174 +e = Gf8.elt(a)
175 Gf8.log.go(254n, U32.is_eq(1, e), f, e, 1, 0n)