1	# GF(2^8) (gf.bend). For every reduction polynomial (every Gf8Field) and
2	# every input, multiplication is commutative and associative, distributes
3	# over addition, has 1 as its identity and 0 as its zero; addition is
4	# commutative and associative, with 0 as its identity and every element its
5	# own negative; xtime is multiplication by x; and powers add. (These are the
6	# laws of the ring GF(2)[x] modulo the polynomial, which hold whether or not
7	# the polynomial is irreducible.)
8	#
9	# For the named fields (AES's 0x11B and Reed-Solomon's 0x11D, both
10	# irreducible): every nonzero element has an inverse, and is a power of the
11	# field's generator, its logarithm (checked for all 255 nonzero bytes).
12	#
13	# Vectors: FIPS 197's worked products (section 4.2), the AES inverse of
14	# 0x53 (0xCA), and the Reed-Solomon powers of x. The tables (tables.bend),
15	# GF(2^128) (gf128.bend) and GF(2^m) (gfm.bend) laws follow.
16	import Base
17	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18	import ./gf.bend as G
19	import ./tables.bend as T
20	import ./gf128.bend as H
21	import ./gfm.bend as M
22	
23	# Multiplication: a commutative ring with identity, for every polynomial
24	
25	law mul_comm:
26	  for +f: G.Gf8Field
27	  for +a: U32
28	  for +b: U32
29	  {G.Gf8.mul(f, a, b) == G.Gf8.mul(f, b, a) : U32}
30	
31	law mul_assoc:
32	  for +f: G.Gf8Field
33	  for +a: U32
34	  for +b: U32
35	  for +c: U32
36	  {G.Gf8.mul(f, G.Gf8.mul(f, a, b), c) == G.Gf8.mul(f, a, G.Gf8.mul(f, b, c)) : U32}
37	
38	law mul_distrib:
39	  for +f: G.Gf8Field
40	  for +a: U32
41	  for +b: U32
42	  for +c: U32
43	  {G.Gf8.mul(f, a, G.Gf8.add(b, c)) == G.Gf8.add(G.Gf8.mul(f, a, b), G.Gf8.mul(f, a, c)) : U32}
44	
45	law mul_one:
46	  for +f: G.Gf8Field
47	  for +a: U32
48	  {G.Gf8.mul(f, 1, a) == G.Gf8.elt(a) : U32}
49	
50	law mul_zero:
51	  for +f: G.Gf8Field
52	  for +a: U32
53	  {G.Gf8.mul(f, 0, a) == 0 : U32}
54	
55	law xtime_mul_x:
56	  for +f: G.Gf8Field
57	  for +a: U32
58	  {G.Gf8.xtime(f, a) == G.Gf8.mul(f, 2, a) : U32}
59	
60	# Addition: XOR, a group in which every element is its own negative
61	
62	law add_comm:
63	  for +a: U32
64	  for +b: U32
65	  {G.Gf8.add(a, b) == G.Gf8.add(b, a) : U32}
66	
67	law add_assoc:
68	  for +a: U32
69	  for +b: U32
70	  for +c: U32
71	  {G.Gf8.add(G.Gf8.add(a, b), c) == G.Gf8.add(a, G.Gf8.add(b, c)) : U32}
72	
73	law add_zero:
74	  for +a: U32
75	  {G.Gf8.add(a, 0) == G.Gf8.elt(a) : U32}
76	
77	law add_self:
78	  for +a: U32
79	  {G.Gf8.add(a, a) == 0 : U32}
80	
81	# Powers: a^(m + n) = a^m * a^n
82	
83	law pow_add:
84	  for +f: G.Gf8Field
85	  for +a: U32
86	  for +m: Nat
87	  for +n: Nat
88	  {G.Gf8.pow(f, a, Nat.add(m, n)) == G.Gf8.mul(f, G.Gf8.pow(f, a, m), G.Gf8.pow(f, a, n)) : U32}
89	
90	# Inverses and logarithms in the named fields, for every nonzero element
91	
92	law mul_inv_aes:
93	  for +a: U32
94	  for nz: {G.Gf8.is_zero(a) == False{} : Bool}
95	  {G.Gf8.mul(G.Gf8.aes(), a, G.Gf8.inv(G.Gf8.aes(), a)) == 1 : U32}
96	
97	law mul_inv_rs:
98	  for +a: U32
99	  for nz: {G.Gf8.is_zero(a) == False{} : Bool}
100	  {G.Gf8.mul(G.Gf8.rs(), a, G.Gf8.inv(G.Gf8.rs(), a)) == 1 : U32}
101	
102	law exp_log_aes:
103	  for +a: U32
104	  for nz: {G.Gf8.is_zero(a) == False{} : Bool}
105	  {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), a)) == G.Gf8.elt(a) : U32}
106	
107	law exp_log_rs:
108	  for +a: U32
109	  for nz: {G.Gf8.is_zero(a) == False{} : Bool}
110	  {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), a)) == G.Gf8.elt(a) : U32}
111	
112	law inv_zero:
113	  for +f: G.Gf8Field
114	  {G.Gf8.inv(f, 0) == 0 : U32}
115	
116	# Vectors: FIPS 197, section 4.2: {57} * {83} = {c1}, {57} * {13} = {fe},
117	# and xtime: {57} * {02} = {ae}, {57} * {04} = {47}, {57} * {08} = {8e},
118	# {57} * {10} = {07}
119	
120	law v_aes_mul:
121	  {G.Gf8.mul(G.Gf8.aes(), 87, 131) == 193 : U32}
122	
123	law v_aes_mul13:
124	  {G.Gf8.mul(G.Gf8.aes(), 87, 19) == 254 : U32}
125	
126	law v_aes_xtime:
127	  {[G.Gf8.xtime(G.Gf8.aes(), 87), G.Gf8.mul(G.Gf8.aes(), 87, 4), G.Gf8.mul(G.Gf8.aes(), 87, 8), G.Gf8.mul(G.Gf8.aes(), 87, 16)] == [174, 71, 142, 7] : List<&2, U32>}
128	
129	# the inverse of {53} is {ca} (the AES S-box's first step)
130	law v_aes_inv:
131	  {G.Gf8.inv(G.Gf8.aes(), 83) == 202 : U32}
132	
133	# in the Reed-Solomon field x^8 = x^4 + x^3 + x^2 + 1 = 0x1D, and x has
134	# order 255 (x^255 = 1): x generates the field
135	law v_rs_x8:
136	  {G.Gf8.exp(G.Gf8.rs(), 8n) == 29 : U32}
137	
138	law v_rs_order:
139	  {G.Gf8.exp(G.Gf8.rs(), 255n) == 1 : U32}
140	
141	law v_div:
142	  {G.Gf8.mul(G.Gf8.aes(), G.Gf8.div(G.Gf8.aes(), 87, 131), 131) == 87 : U32}
143	
144	# The tables (tables.bend) give the reference's results on these vectors;
145	# they are tied to the reference for every input by the exhaustive runtime
146	# check in check.bend and by ref/run.sh (see the README).
147	
148	law v_tab_mul_aes:
149	  {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.aes()), 87, 131)) == 193 : U32}
150	
151	law v_tab_inv_aes:
152	  {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.inv(T.Gf8Tab.new(G.Gf8.aes()), 83)) == 202 : U32}
153	
154	law v_tab_mul_rs:
155	  {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 200, 77)) == G.Gf8.mul(G.Gf8.rs(), 200, 77) : U32}
156	
157	law v_tab_zero:
158	  {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 0, 77)) == 0 : U32}
159	
160	# GF(2^128) (gf128.bend): vectors only. GCM: Test Case 2 of the GCM
161	# specification (McGrew and Viega; H = AES-128 of the zero block under the
162	# zero key): X1 = C * H, and GHASH(H, C || lengths). CMAC: the subkeys of
163	# SP 800-38B D.1 / RFC 4493 (L = AES-128(K, 0), K1 = 2L, K2 = 4L). The
164	# others pin the bit orders against each other. Laws for every input would
165	# compute on 128 symbolic bits through 128 rounds; ref/run.sh checks every
166	# function against independent implementations instead (see the README).
167	# H = 66e94bd4ef8a2c3b884cfa59ca342b2e, C = 0388dace60b6a392f328c2b971b2fe78,
168	# and a = 0123456789abcdeffedcba9876543210.
169	
170	# 5e2ec746917062882c85b0685353deb7
171	law v_gcm_x1:
172	  {H.Gf128.mul_gcm(H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960), H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)) == H.Gf128.of_words(1580123974, 2440061576, 746958952, 1398005431) : H.Gf128}
173	
174	# f38cbb1ad69223dcc3457ae5b6b0f885 (one block of C, then the lengths: 0 bits
175	# of A, 128 of C)
176	law v_gcm_ghash:
177	  {H.Gf128.ghash(H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558), [H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960), H.Gf128.of_words(0, 0, 0, 128)]) == H.Gf128.of_words(4086086426, 3599901660, 3276110565, 3065051269) : H.Gf128}
178	
179	# L = 7df76b0c1ab899b33e42f047b91b546f, K1 = fbeed618357133667c85e08f7236a8de,
180	# K2 = f7ddac306ae266ccf90bc11ee46d513b
181	law v_cmac_k1:
182	  {H.Gf128.double_be(H.Gf128.of_words(2113366796, 448305587, 1044574279, 3105576047)) == H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798) : H.Gf128}
183	
184	law v_cmac_k2:
185	  {H.Gf128.double_be(H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798)) == H.Gf128.of_words(4158499888, 1793222348, 4178297118, 3832369467) : H.Gf128}
186	
187	# GCM's x is the block 0x40 00 .. 00: mul_x_gcm is multiplication by it
188	law v_gcm_mul_x:
189	  {H.Gf128.mul_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(1073741824, 0, 0, 0)) == H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) : H.Gf128}
190	
191	law v_gcm_mul_x_value:
192	  {H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(9544371, 3302352631, 4285422924, 992614664) : H.Gf128}
193	
194	# in big-endian order x is the number 2: double_be is multiplication by it
195	law v_be_mul_x:
196	  {H.Gf128.mul_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(0, 0, 0, 2)) == H.Gf128.double_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) : H.Gf128}
197	
198	law v_be_mul:
199	  {H.Gf128.mul_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)) == H.Gf128.of_words(780021721, 1580971822, 2568813327, 4049188832) : H.Gf128}
200	
201	# XTS: the top bit of byte 15 wraps round as 0x87 into byte 0
202	law v_xts_wrap:
203	  {H.Gf128.double_le(H.Gf128.of_words(0, 0, 0, 255)) == H.Gf128.of_words(2264924160, 0, 0, 254) : H.Gf128}
204	
205	law v_xts_double:
206	  {H.Gf128.double_le(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(38177486, 307731423, 4256789809, 3987235872) : H.Gf128}
207	
208	law v_gf128_octets:
209	  {H.Gf128.of_octets(H.Gf128.to_octets(H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558))) == Done{H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)} : Result<&2, &2, H.Gf128Error, H.Gf128>}
210	
211	law v_gf128_short:
212	  {H.Gf128.of_octets(B.Octets.zeros(15n)) == Fail{H.Gf128BadLength{15n}} : Result<&2, &2, H.Gf128Error, H.Gf128>}
213	
214	# GF(2^m) (gfm.bend). For every field and input: addition commutes. For
215	# GF(2^4): multiplication commutes (all 256 pairs) and every nonzero element
216	# has an inverse; for GF(2^5), inverses too. Vectors for the BCH fields: x^13
217	# = x^4 + x^3 + x + 1, x has order 8191 (so generates GF(2^13)), a product,
218	# an inverse and a logarithm (x^100 = 1664), from an independent model
219	# (ref/gen.py).
220	
221	law gfm_add_comm:
222	  for +f: M.GfmField
223	  for +a: U32
224	  for +b: U32
225	  {M.Gfm.add(f, a, b) == M.Gfm.add(f, b, a) : U32}
226	
227	law gfm_mul_comm_gf16:
228	  for +a: U32
229	  for +b: U32
230	  {M.Gfm.mul(M.Gfm.gf16(), a, b) == M.Gfm.mul(M.Gfm.gf16(), b, a) : U32}
231	
232	law gfm_mul_inv_gf16:
233	  for +a: U32
234	  for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf16(), a), 0) == False{} : Bool}
235	  {M.Gfm.mul(M.Gfm.gf16(), a, M.Gfm.inv(M.Gfm.gf16(), a)) == 1 : U32}
236	
237	law gfm_mul_inv_gf32:
238	  for +a: U32
239	  for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf32(), a), 0) == False{} : Bool}
240	  {M.Gfm.mul(M.Gfm.gf32(), a, M.Gfm.inv(M.Gfm.gf32(), a)) == 1 : U32}
241	
242	law v_bch13_x13:
243	  {M.Gfm.exp(M.Gfm.bch13(), 13) == 27 : U32}
244	
245	law v_bch13_order:
246	  {M.Gfm.exp(M.Gfm.bch13(), 8191) == 1 : U32}
247	
248	law v_bch13_mul:
249	  {M.Gfm.mul(M.Gfm.bch13(), 1234, 5678) == 4994 : U32}
250	
251	law v_bch13_inv:
252	  {M.Gfm.inv(M.Gfm.bch13(), 1234) == 2297 : U32}
253	
254	law v_bch13_log:
255	  {M.Gfm.log(M.Gfm.bch13(), 1664) == 100 : U32}
256	
257	law v_bch14_mul:
258	  {M.Gfm.mul(M.Gfm.bch14(), 12345, 6789) == 6882 : U32}