1	import Base
2	
3	# The AES S-box and the GF(2^8) doublings MixColumns needs, computed with
4	# U32 bit operations only: no table and no branch reads a secret byte.
5	#
6	# The S-box is the depth-16, 113-gate (+ 4 NOT) circuit of Boyar and Peralta
7	# ("A depth-16 circuit for the AES S-box", 2011; the gate list BearSSL's
8	# aes_ct uses), evaluated on one byte with one bit per U32 (values 0 or 1).
9	# Its input x0..x7 is the byte's bit 7..0 and its output s0..s7 the result's
10	# bit 7..0. proofs/crypto/aes/sbox.bend proves it equal, on every input, to
11	# FIPS 197's S-box (the inverse in GF(2^8) followed by the affine map).
12	# Every mask is the first operand of U32.and, so the bits above the low
13	# eight of an input never reach the result.
14	def sbox_word(+x: U32) -> U32:
15	  +x0 = U32.and(1, U32.shrn(x, 7n))
16	  +x1 = U32.and(1, U32.shrn(x, 6n))
17	  +x2 = U32.and(1, U32.shrn(x, 5n))
18	  +x3 = U32.and(1, U32.shrn(x, 4n))
19	  +x4 = U32.and(1, U32.shrn(x, 3n))
20	  +x5 = U32.and(1, U32.shrn(x, 2n))
21	  +x6 = U32.and(1, U32.shrn(x, 1n))
22	  +x7 = U32.and(1, U32.shrn(x, 0n))
23	  +y14 = U32.xor(x3, x5)
24	  +y13 = U32.xor(x0, x6)
25	  +y9 = U32.xor(x0, x3)
26	  +y8 = U32.xor(x0, x5)
27	  +t0 = U32.xor(x1, x2)
28	  +y1 = U32.xor(t0, x7)
29	  +y4 = U32.xor(y1, x3)
30	  +y12 = U32.xor(y13, y14)
31	  +y2 = U32.xor(y1, x0)
32	  +y5 = U32.xor(y1, x6)
33	  +y3 = U32.xor(y5, y8)
34	  +t1 = U32.xor(x4, y12)
35	  +y15 = U32.xor(t1, x5)
36	  +y20 = U32.xor(t1, x1)
37	  +y6 = U32.xor(y15, x7)
38	  +y10 = U32.xor(y15, t0)
39	  +y11 = U32.xor(y20, y9)
40	  +y7 = U32.xor(x7, y11)
41	  +y17 = U32.xor(y10, y11)
42	  +y19 = U32.xor(y10, y8)
43	  +y16 = U32.xor(t0, y11)
44	  +y21 = U32.xor(y13, y16)
45	  +y18 = U32.xor(x0, y16)
46	  +t2 = U32.and(y12, y15)
47	  +t3 = U32.and(y3, y6)
48	  +t4 = U32.xor(t3, t2)
49	  +t5 = U32.and(y4, x7)
50	  +t6 = U32.xor(t5, t2)
51	  +t7 = U32.and(y13, y16)
52	  +t8 = U32.and(y5, y1)
53	  +t9 = U32.xor(t8, t7)
54	  +t10 = U32.and(y2, y7)
55	  +t11 = U32.xor(t10, t7)
56	  +t12 = U32.and(y9, y11)
57	  +t13 = U32.and(y14, y17)
58	  +t14 = U32.xor(t13, t12)
59	  +t15 = U32.and(y8, y10)
60	  +t16 = U32.xor(t15, t12)
61	  +t17 = U32.xor(t4, t14)
62	  +t18 = U32.xor(t6, t16)
63	  +t19 = U32.xor(t9, t14)
64	  +t20 = U32.xor(t11, t16)
65	  +t21 = U32.xor(t17, y20)
66	  +t22 = U32.xor(t18, y19)
67	  +t23 = U32.xor(t19, y21)
68	  +t24 = U32.xor(t20, y18)
69	  +t25 = U32.xor(t21, t22)
70	  +t26 = U32.and(t21, t23)
71	  +t27 = U32.xor(t24, t26)
72	  +t28 = U32.and(t25, t27)
73	  +t29 = U32.xor(t28, t22)
74	  +t30 = U32.xor(t23, t24)
75	  +t31 = U32.xor(t22, t26)
76	  +t32 = U32.and(t31, t30)
77	  +t33 = U32.xor(t32, t24)
78	  +t34 = U32.xor(t23, t33)
79	  +t35 = U32.xor(t27, t33)
80	  +t36 = U32.and(t24, t35)
81	  +t37 = U32.xor(t36, t34)
82	  +t38 = U32.xor(t27, t36)
83	  +t39 = U32.and(t29, t38)
84	  +t40 = U32.xor(t25, t39)
85	  +t41 = U32.xor(t40, t37)
86	  +t42 = U32.xor(t29, t33)
87	  +t43 = U32.xor(t29, t40)
88	  +t44 = U32.xor(t33, t37)
89	  +t45 = U32.xor(t42, t41)
90	  +z0 = U32.and(t44, y15)
91	  +z1 = U32.and(t37, y6)
92	  +z2 = U32.and(t33, x7)
93	  +z3 = U32.and(t43, y16)
94	  +z4 = U32.and(t40, y1)
95	  +z5 = U32.and(t29, y7)
96	  +z6 = U32.and(t42, y11)
97	  +z7 = U32.and(t45, y17)
98	  +z8 = U32.and(t41, y10)
99	  +z9 = U32.and(t44, y12)
100	  +z10 = U32.and(t37, y3)
101	  +z11 = U32.and(t33, y4)
102	  +z12 = U32.and(t43, y13)
103	  +z13 = U32.and(t40, y5)
104	  +z14 = U32.and(t29, y2)
105	  +z15 = U32.and(t42, y9)
106	  +z16 = U32.and(t45, y14)
107	  +z17 = U32.and(t41, y8)
108	  +t46 = U32.xor(z15, z16)
109	  +t47 = U32.xor(z10, z11)
110	  +t48 = U32.xor(z5, z13)
111	  +t49 = U32.xor(z9, z10)
112	  +t50 = U32.xor(z2, z12)
113	  +t51 = U32.xor(z2, z5)
114	  +t52 = U32.xor(z7, z8)
115	  +t53 = U32.xor(z0, z3)
116	  +t54 = U32.xor(z6, z7)
117	  +t55 = U32.xor(z16, z17)
118	  +t56 = U32.xor(z12, t48)
119	  +t57 = U32.xor(t50, t53)
120	  +t58 = U32.xor(z4, t46)
121	  +t59 = U32.xor(z3, t54)
122	  +t60 = U32.xor(t46, t57)
123	  +t61 = U32.xor(z14, t57)
124	  +t62 = U32.xor(t52, t58)
125	  +t63 = U32.xor(t49, t58)
126	  +t64 = U32.xor(z4, t59)
127	  +t65 = U32.xor(t61, t62)
128	  +t66 = U32.xor(z1, t63)
129	  +s0 = U32.xor(t59, t63)
130	  +s6 = U32.xor(t56, U32.xor(1, t62))
131	  +s7 = U32.xor(t48, U32.xor(1, t60))
132	  +t67 = U32.xor(t64, t65)
133	  +s3 = U32.xor(t53, t66)
134	  +s4 = U32.xor(t51, t66)
135	  +s5 = U32.xor(t47, t65)
136	  +s1 = U32.xor(t64, U32.xor(1, s3))
137	  +s2 = U32.xor(t55, U32.xor(1, t67))
138	  U32.or(U32.shln(s0, 7n), U32.or(U32.shln(s1, 6n), U32.or(U32.shln(s2, 5n), U32.or(U32.shln(s3, 4n), U32.or(U32.shln(s4, 3n), U32.or(U32.shln(s5, 2n), U32.or(U32.shln(s6, 1n), s7)))))))
139	
140	# The S-box. (The one-constructor match only opens the U32, no branch: it
141	# keeps a proof about an unknown word from expanding the 117 gates.)
142	def sbox(x: U32) -> U32:
143	  match x:
144	    case U32{w}: sbox_word(U32{w})
145	
146	# {02} * x in GF(2^8) (FIPS 197 section 4.2.1, xtime): shift left and, when
147	# bit 7 was set, add x^8 = {1b}; the reduction mask is 0 - bit7, not a branch.
148	def xtime_word(+x: U32) -> U32:
149	  U32.xor(U32.and(254, U32.shln(x, 1n)), U32.and(27, U32.sub(0, U32.and(1, U32.shrn(x, 7n)))))
150	
151	def xtime(x: U32) -> U32:
152	  match x:
153	    case U32{w}: xtime_word(U32{w})
154	
155	# {03} * x = {02} * x + x.
156	def mul3_word(+x: U32) -> U32:
157	  U32.xor(xtime(x), U32.and(255, x))
158	
159	def mul3(x: U32) -> U32:
160	  match x:
161	    case U32{w}: mul3_word(U32{w})