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).
17	import Base
18	
19	type 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)
25	def 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)
29	def Gf8.rs() -> Gf8Field:
30	  Gf8Field{285, 2}
31	
32	def Gf8.raid6() -> Gf8Field:
33	  Gf8.rs()
34	
35	def Gf8.poly(f: Gf8Field) -> U32:
36	  match f:
37	    case Gf8Field{poly, gen}:
38	      poly
39	
40	def 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	
47	type 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
51	def 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	
56	def 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	
61	def Gf8Bits.zero() -> Gf8Bits:
62	  Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}
63	
64	def 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
70	def 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)
79	def 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
85	def 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
89	def 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
97	def 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	
102	def 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
108	def 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)
112	def 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	
117	def Gf8.is_zero(a: U32) -> Bool:
118	  Gf8Bits.is_zero(Gf8Bits.of(a))
119	
120	def 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
124	def Gf8.sub(a: U32, b: U32) -> U32:
125	  Gf8.add(a, b)
126	
127	def 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)
133	def 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)
139	def 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
148	def Gf8.inv(+f: Gf8Field, +a: U32) -> U32:
149	  Gf8.pow(f, a, 254n)
150	
151	# a / b = a * b^-1 (and a / 0 = 0)
152	def 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
158	def 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
163	def 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	
173	def 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)