1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/crypto/aes/poly.bend as P
5	
6	# Polynomial arithmetic over GF(2), for any modulus m(x) = x^n + low(x):
7	# reducing the product a(x) * b(x) modulo m equals the shift-and-add
8	# evaluation of SP 800-38D's Algorithm 1 (sa below): Z accumulates b(x)*x^i
9	# (mod m) for every set coefficient a_i. With n = 128 and low = R this is
10	# the GHASH product; the implementation computes sa.
11	
12	# ---- one bit ----
13	
14	def bxor_false(+b: Bool) -> {Bool.xor(b, False{}) == b : Bool}:
15	  match b:
16	    case True{}:
17	      {==}
18	    case False{}:
19	      {==}
20	
21	def bxor_comm(+a: Bool, +b: Bool) -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}:
22	  match a b:
23	    case True{} True{}:
24	      {==}
25	    case True{} False{}:
26	      {==}
27	    case False{} True{}:
28	      {==}
29	    case False{} False{}:
30	      {==}
31	
32	def bxor_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}:
33	  match a b c:
34	    case True{} True{} True{}:
35	      {==}
36	    case True{} True{} False{}:
37	      {==}
38	    case True{} False{} True{}:
39	      {==}
40	    case True{} False{} False{}:
41	      {==}
42	    case False{} True{} True{}:
43	      {==}
44	    case False{} True{} False{}:
45	      {==}
46	    case False{} False{} True{}:
47	      {==}
48	    case False{} False{} False{}:
49	      {==}
50	
51	def bxor_self(+a: Bool) -> {Bool.xor(a, a) == False{} : Bool}:
52	  match a:
53	    case True{}:
54	      {==}
55	    case False{}:
56	      {==}
57	
58	def bswap4(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> {Bool.xor(Bool.xor(a, b), Bool.xor(c, d)) == Bool.xor(Bool.xor(a, c), Bool.xor(b, d)) : Bool}:
59	  match a b c d:
60	    case True{} True{} True{} True{}:
61	      {==}
62	    case True{} True{} True{} False{}:
63	      {==}
64	    case True{} True{} False{} True{}:
65	      {==}
66	    case True{} True{} False{} False{}:
67	      {==}
68	    case True{} False{} True{} True{}:
69	      {==}
70	    case True{} False{} True{} False{}:
71	      {==}
72	    case True{} False{} False{} True{}:
73	      {==}
74	    case True{} False{} False{} False{}:
75	      {==}
76	    case False{} True{} True{} True{}:
77	      {==}
78	    case False{} True{} True{} False{}:
79	      {==}
80	    case False{} True{} False{} True{}:
81	      {==}
82	    case False{} True{} False{} False{}:
83	      {==}
84	    case False{} False{} True{} True{}:
85	      {==}
86	    case False{} False{} True{} False{}:
87	      {==}
88	    case False{} False{} False{} True{}:
89	      {==}
90	    case False{} False{} False{} False{}:
91	      {==}
92	
93	# ---- words: XOR is a commutative group, shifts and tops are linear ----
94	
95	def xor_zero_l(+n: Nat, +w: Word(n)) -> {Word.xor(n, Word.zero(n), w) == w : Word(n)}:
96	  match n w:
97	    case 0n WNil{}:
98	      {==}
99	    case 1n+p WCon{b, t}:
100	      %xor_zero_l(p, t) : {WCon{b, Word.xor(p, Word.zero(p), t)} == WCon{b, _} : Word(1n+p)}
101	      {==}
102	
103	def xor_zero_r(+n: Nat, +w: Word(n)) -> {Word.xor(n, w, Word.zero(n)) == w : Word(n)}:
104	  match n w:
105	    case 0n WNil{}:
106	      {==}
107	    case 1n+p WCon{b, t}:
108	      %xor_zero_r(p, t) : {WCon{Bool.xor(b, False{}), Word.xor(p, t, Word.zero(p))} == WCon{b, _} : Word(1n+p)}
109	      %bxor_false(b) : {WCon{Bool.xor(b, False{}), Word.xor(p, t, Word.zero(p))} == WCon{_, Word.xor(p, t, Word.zero(p))} : Word(1n+p)}
110	      {==}
111	
112	def xor_self(+n: Nat, +w: Word(n)) -> {Word.xor(n, w, w) == Word.zero(n) : Word(n)}:
113	  match n w:
114	    case 0n WNil{}:
115	      {==}
116	    case 1n+p WCon{b, t}:
117	      %xor_self(p, t) : {WCon{Bool.xor(b, b), Word.xor(p, t, t)} == WCon{False{}, _} : Word(1n+p)}
118	      %bxor_self(b) : {WCon{Bool.xor(b, b), Word.xor(p, t, t)} == WCon{_, Word.xor(p, t, t)} : Word(1n+p)}
119	      {==}
120	
121	def xor_assoc(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n)) -> {Word.xor(n, Word.xor(n, a, b), c) == Word.xor(n, a, Word.xor(n, b, c)) : Word(n)}:
122	  match n a b c:
123	    case 0n WNil{} WNil{} WNil{}:
124	      {==}
125	    case 1n+p WCon{x, s} WCon{y, t} WCon{z, u}:
126	      %xor_assoc(p, s, t, u) : {WCon{Bool.xor(Bool.xor(x, y), z), Word.xor(p, Word.xor(p, s, t), u)} == WCon{Bool.xor(x, Bool.xor(y, z)), _} : Word(1n+p)}
127	      %bxor_assoc(x, y, z) : {WCon{Bool.xor(Bool.xor(x, y), z), Word.xor(p, Word.xor(p, s, t), u)} == WCon{_, Word.xor(p, Word.xor(p, s, t), u)} : Word(1n+p)}
128	      {==}
129	
130	def xor_swap4(+n: Nat, +a: Word(n), +b: Word(n), +c: Word(n), +d: Word(n)) -> {Word.xor(n, Word.xor(n, a, b), Word.xor(n, c, d)) == Word.xor(n, Word.xor(n, a, c), Word.xor(n, b, d)) : Word(n)}:
131	  match n a b c d:
132	    case 0n WNil{} WNil{} WNil{} WNil{}:
133	      {==}
134	    case 1n+p WCon{x, s} WCon{y, t} WCon{z, u} WCon{w, v}:
135	      %xor_swap4(p, s, t, u, v) : {WCon{Bool.xor(Bool.xor(x, y), Bool.xor(z, w)), Word.xor(p, Word.xor(p, s, t), Word.xor(p, u, v))} == WCon{Bool.xor(Bool.xor(x, z), Bool.xor(y, w)), _} : Word(1n+p)}
136	      %bswap4(x, y, z, w) : {WCon{Bool.xor(Bool.xor(x, y), Bool.xor(z, w)), Word.xor(p, Word.xor(p, s, t), Word.xor(p, u, v))} == WCon{_, Word.xor(p, Word.xor(p, s, t), Word.xor(p, u, v))} : Word(1n+p)}
137	      {==}
138	
139	def put_xor(+p: Nat, +c: Bool, +d: Bool, +s: Word(p), +t: Word(p)) -> {Word.shl.put(p, Bool.xor(c, d), Word.xor(p, s, t)) == Word.xor(p, Word.shl.put(p, c, s), Word.shl.put(p, d, t)) : Word(p)}:
140	  match p s t:
141	    case 0n WNil{} WNil{}:
142	      {==}
143	    case 1n+q WCon{x, s1} WCon{y, t1}:
144	      %put_xor(q, x, y, s1, t1) : {WCon{Bool.xor(c, d), Word.shl.put(q, Bool.xor(x, y), Word.xor(q, s1, t1))} == WCon{Bool.xor(c, d), _} : Word(1n+q)}
145	      {==}
146	
147	def shl_xor(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.shl(n, Word.xor(n, a, b)) == Word.xor(n, Word.shl(n, a), Word.shl(n, b)) : Word(n)}:
148	  match n a b:
149	    case 0n WNil{} WNil{}:
150	      {==}
151	    case 1n+p WCon{x, s} WCon{y, t}:
152	      %put_xor(p, x, y, s, t) : {WCon{False{}, Word.shl.put(p, Bool.xor(x, y), Word.xor(p, s, t))} == WCon{False{}, _} : Word(1n+p)}
153	      {==}
154	
155	def top_xor(+n: Nat, +a: Word(n), +b: Word(n)) -> {P.top(n, Word.xor(n, a, b)) == Bool.xor(P.top(n, a), P.top(n, b)) : Bool}:
156	  match n a b:
157	    case 0n WNil{} WNil{}:
158	      {==}
159	    case 1n WCon{x, s} WCon{y, t}:
160	      {==}
161	    case 2n+p WCon{x, s} WCon{y, t}:
162	      top_xor(1n+p, s, t)
163	
164	def top_zero(+n: Nat) -> {P.top(n, Word.zero(n)) == False{} : Bool}:
165	  match n:
166	    case 0n:
167	      {==}
168	    case 1n:
169	      {==}
170	    case 2n+p:
171	      top_zero(1n+p)
172	
173	def put_zero(+p: Nat) -> {Word.shl.put(p, False{}, Word.zero(p)) == Word.zero(p) : Word(p)}:
174	  match p:
175	    case 0n:
176	      {==}
177	    case 1n+q:
178	      %put_zero(q) : {WCon{False{}, Word.shl.put(q, False{}, Word.zero(q))} == WCon{False{}, _} : Word(1n+q)}
179	      {==}
180	
181	def shl_zero(+n: Nat) -> {Word.shl(n, Word.zero(n)) == Word.zero(n) : Word(n)}:
182	  match n:
183	    case 0n:
184	      {==}
185	    case 1n+p:
186	      %put_zero(p) : {WCon{False{}, Word.shl.put(p, False{}, Word.zero(p))} == WCon{False{}, _} : Word(1n+p)}
187	      {==}
188	
189	def wscale_xor(+n: Nat, +c: Bool, +d: Bool, +w: Word(n)) -> {P.wscale(n, Bool.xor(c, d), w) == Word.xor(n, P.wscale(n, c, w), P.wscale(n, d, w)) : Word(n)}:
190	  match c d:
191	    case True{} True{}:
192	      Equal.sym(Word(n), Word.xor(n, w, w), Word.zero(n), xor_self(n, w))
193	    case True{} False{}:
194	      Equal.sym(Word(n), Word.xor(n, w, Word.zero(n)), w, xor_zero_r(n, w))
195	    case False{} True{}:
196	      Equal.sym(Word(n), Word.xor(n, Word.zero(n), w), w, xor_zero_l(n, w))
197	    case False{} False{}:
198	      Equal.sym(Word(n), Word.xor(n, Word.zero(n), Word.zero(n)), Word.zero(n), xor_zero_l(n, Word.zero(n)))
199	
200	# ---- multiplication by x modulo m ----
201	
202	def tx_xor(+n: Nat, +low: Word(n), +a: Word(n), +b: Word(n)) -> {P.times_x(n, low, Word.xor(n, a, b)) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}:
203	  %Equal.sym(Bool, P.top(n, Word.xor(n, a, b)), Bool.xor(P.top(n, a), P.top(n, b)), top_xor(n, a, b)) : {Word.xor(n, P.wscale(n, _, low), Word.shl(n, Word.xor(n, a, b))) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}
204	  %Equal.sym(Word(n), P.wscale(n, Bool.xor(P.top(n, a), P.top(n, b)), low), Word.xor(n, P.wscale(n, P.top(n, a), low), P.wscale(n, P.top(n, b), low)), wscale_xor(n, P.top(n, a), P.top(n, b), low)) : {Word.xor(n, _, Word.shl(n, Word.xor(n, a, b))) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}
205	  %Equal.sym(Word(n), Word.shl(n, Word.xor(n, a, b)), Word.xor(n, Word.shl(n, a), Word.shl(n, b)), shl_xor(n, a, b)) : {Word.xor(n, Word.xor(n, P.wscale(n, P.top(n, a), low), P.wscale(n, P.top(n, b), low)), _) == Word.xor(n, P.times_x(n, low, a), P.times_x(n, low, b)) : Word(n)}
206	  xor_swap4(n, P.wscale(n, P.top(n, a), low), P.wscale(n, P.top(n, b), low), Word.shl(n, a), Word.shl(n, b))
207	
208	def tx_zero(+n: Nat, +low: Word(n)) -> {P.times_x(n, low, Word.zero(n)) == Word.zero(n) : Word(n)}:
209	  %Equal.sym(Bool, P.top(n, Word.zero(n)), False{}, top_zero(n)) : {Word.xor(n, P.wscale(n, _, low), Word.shl(n, Word.zero(n))) == Word.zero(n) : Word(n)}
210	  %Equal.sym(Word(n), Word.shl(n, Word.zero(n)), Word.zero(n), shl_zero(n)) : {Word.xor(n, Word.zero(n), _) == Word.zero(n) : Word(n)}
211	  xor_zero_l(n, Word.zero(n))
212	
213	def tx_wscale(+n: Nat, +low: Word(n), +c: Bool, +v: Word(n)) -> {P.times_x(n, low, P.wscale(n, c, v)) == P.wscale(n, c, P.times_x(n, low, v)) : Word(n)}:
214	  match c:
215	    case True{}:
216	      {==}
217	    case False{}:
218	      tx_zero(n, low)
219	
220	# ---- reduction modulo m is linear ----
221	
222	def constant_xor(+n: Nat, +c: Bool, +d: Bool) -> {P.constant(n, Bool.xor(c, d)) == Word.xor(n, P.constant(n, c), P.constant(n, d)) : Word(n)}:
223	  match n:
224	    case 0n:
225	      {==}
226	    case 1n+p:
227	      %Equal.sym(Word(p), Word.xor(p, Word.zero(p), Word.zero(p)), Word.zero(p), xor_zero_l(p, Word.zero(p))) : {WCon{Bool.xor(c, d), Word.zero(p)} == WCon{Bool.xor(c, d), _} : Word(1n+p)}
228	      {==}
229	
230	def red_add(+n: Nat, +low: Word(n), +p: List<&2, Bool>, +q: List<&2, Bool>) -> {P.reduce(n, low, P.add(p, q)) == Word.xor(n, P.reduce(n, low, p), P.reduce(n, low, q)) : Word(n)}:
231	  match p q:
232	    case Nil{} _:
233	      Equal.sym(Word(n), Word.xor(n, Word.zero(n), P.reduce(n, low, q)), P.reduce(n, low, q), xor_zero_l(n, P.reduce(n, low, q)))
234	    case x <> xs Nil{}:
235	      Equal.sym(Word(n), Word.xor(n, P.reduce(n, low, x <> xs), Word.zero(n)), P.reduce(n, low, x <> xs), xor_zero_r(n, P.reduce(n, low, x <> xs)))
236	    case x <> xs y <> ys:
237	      %Equal.sym(Word(n), P.reduce(n, low, P.add(xs, ys)), Word.xor(n, P.reduce(n, low, xs), P.reduce(n, low, ys)), red_add(n, low, xs, ys)) : {Word.xor(n, P.constant(n, Bool.xor(x, y)), P.times_x(n, low, _)) == Word.xor(n, P.reduce(n, low, x <> xs), P.reduce(n, low, y <> ys)) : Word(n)}
238	      %Equal.sym(Word(n), P.times_x(n, low, Word.xor(n, P.reduce(n, low, xs), P.reduce(n, low, ys))), Word.xor(n, P.times_x(n, low, P.reduce(n, low, xs)), P.times_x(n, low, P.reduce(n, low, ys))), tx_xor(n, low, P.reduce(n, low, xs), P.reduce(n, low, ys))) : {Word.xor(n, P.constant(n, Bool.xor(x, y)), _) == Word.xor(n, P.reduce(n, low, x <> xs), P.reduce(n, low, y <> ys)) : Word(n)}
239	      %Equal.sym(Word(n), P.constant(n, Bool.xor(x, y)), Word.xor(n, P.constant(n, x), P.constant(n, y)), constant_xor(n, x, y)) : {Word.xor(n, _, Word.xor(n, P.times_x(n, low, P.reduce(n, low, xs)), P.times_x(n, low, P.reduce(n, low, ys)))) == Word.xor(n, P.reduce(n, low, x <> xs), P.reduce(n, low, y <> ys)) : Word(n)}
240	      xor_swap4(n, P.constant(n, x), P.constant(n, y), P.times_x(n, low, P.reduce(n, low, xs)), P.times_x(n, low, P.reduce(n, low, ys)))
241	
242	def scale_true(+b: List<&2, Bool>) -> {P.scale(True{}, b) == b : List<&2, Bool>}:
243	  match b:
244	    case Nil{}:
245	      {==}
246	    case x <> xs:
247	      %scale_true(xs) : {x <> P.scale(True{}, xs) == x <> _ : List<&2, Bool>}
248	      {==}
249	
250	def constant_false_xor(+n: Nat) -> {Word.xor(n, P.constant(n, False{}), Word.zero(n)) == Word.zero(n) : Word(n)}:
251	  match n:
252	    case 0n:
253	      {==}
254	    case 1n+p:
255	      xor_zero_l(1n+p, Word.zero(1n+p))
256	
257	def red_scale_false(+n: Nat, +low: Word(n), +b: List<&2, Bool>) -> {P.reduce(n, low, P.scale(False{}, b)) == Word.zero(n) : Word(n)}:
258	  match b:
259	    case Nil{}:
260	      {==}
261	    case x <> xs:
262	      %Equal.sym(Word(n), P.reduce(n, low, P.scale(False{}, xs)), Word.zero(n), red_scale_false(n, low, xs)) : {Word.xor(n, P.constant(n, False{}), P.times_x(n, low, _)) == Word.zero(n) : Word(n)}
263	      %Equal.sym(Word(n), P.times_x(n, low, Word.zero(n)), Word.zero(n), tx_zero(n, low)) : {Word.xor(n, P.constant(n, False{}), _) == Word.zero(n) : Word(n)}
264	      constant_false_xor(n)
265	
266	def red_scale(+n: Nat, +low: Word(n), +c: Bool, +b: List<&2, Bool>) -> {P.reduce(n, low, P.scale(c, b)) == P.wscale(n, c, P.reduce(n, low, b)) : Word(n)}:
267	  match c:
268	    case True{}:
269	      %scale_true(b) : {P.reduce(n, low, P.scale(True{}, b)) == P.reduce(n, low, _) : Word(n)}
270	      {==}
271	    case False{}:
272	      red_scale_false(n, low, b)
273	
274	def constant_false_l(+n: Nat, +w: Word(n)) -> {Word.xor(n, P.constant(n, False{}), w) == w : Word(n)}:
275	  match n:
276	    case 0n:
277	      match w:
278	        case WNil{}:
279	          {==}
280	    case 1n+p:
281	      xor_zero_l(1n+p, w)
282	
283	def red_shift(+n: Nat, +low: Word(n), +p: List<&2, Bool>) -> {P.reduce(n, low, False{} <> p) == P.times_x(n, low, P.reduce(n, low, p)) : Word(n)}:
284	  constant_false_l(n, P.times_x(n, low, P.reduce(n, low, p)))
285	
286	# ---- the shift-and-add product ----
287	
288	# sum over the set coefficients a_i of v * x^i (mod m)
289	def sm(+n: Nat, +low: Word(n), a: List<&2, Bool>, +v: Word(n)) -> Word(n):
290	  match a:
291	    case Nil{}:
292	      Word.zero(n)
293	    case c <> r:
294	      Word.xor(n, P.wscale(n, c, v), sm(n, low, r, P.times_x(n, low, v)))
295	
296	# Algorithm 1 of SP 800-38D: Z ^= a_i ? V : 0, V = V * x.
297	def sa(+n: Nat, +low: Word(n), a: List<&2, Bool>, z: Word(n), +v: Word(n)) -> Word(n):
298	  match a:
299	    case Nil{}:
300	      z
301	    case c <> r:
302	      sa(n, low, r, Word.xor(n, z, P.wscale(n, c, v)), P.times_x(n, low, v))
303	
304	def tx_sm(+n: Nat, +low: Word(n), +a: List<&2, Bool>, +v: Word(n)) -> {P.times_x(n, low, sm(n, low, a, v)) == sm(n, low, a, P.times_x(n, low, v)) : Word(n)}:
305	  match a:
306	    case Nil{}:
307	      tx_zero(n, low)
308	    case c <> r:
309	      %tx_sm(n, low, r, P.times_x(n, low, v)) : {P.times_x(n, low, Word.xor(n, P.wscale(n, c, v), sm(n, low, r, P.times_x(n, low, v)))) == Word.xor(n, P.wscale(n, c, P.times_x(n, low, v)), _) : Word(n)}
310	      %tx_wscale(n, low, c, v) : {P.times_x(n, low, Word.xor(n, P.wscale(n, c, v), sm(n, low, r, P.times_x(n, low, v)))) == Word.xor(n, _, P.times_x(n, low, sm(n, low, r, P.times_x(n, low, v)))) : Word(n)}
311	      tx_xor(n, low, P.wscale(n, c, v), sm(n, low, r, P.times_x(n, low, v)))
312	
313	def red_mul(+n: Nat, +low: Word(n), +a: List<&2, Bool>, +b: List<&2, Bool>) -> {P.reduce(n, low, P.mul(a, b)) == sm(n, low, a, P.reduce(n, low, b)) : Word(n)}:
314	  match a:
315	    case Nil{}:
316	      {==}
317	    case c <> q:
318	      %tx_sm(n, low, q, P.reduce(n, low, b)) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, P.wscale(n, c, P.reduce(n, low, b)), _) : Word(n)}
319	      %red_mul(n, low, q, b) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, P.wscale(n, c, P.reduce(n, low, b)), P.times_x(n, low, _)) : Word(n)}
320	      %red_shift(n, low, P.mul(q, b)) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, P.wscale(n, c, P.reduce(n, low, b)), _) : Word(n)}
321	      %red_scale(n, low, c, b) : {P.reduce(n, low, P.add(P.scale(c, b), False{} <> P.mul(q, b))) == Word.xor(n, _, P.reduce(n, low, False{} <> P.mul(q, b))) : Word(n)}
322	      red_add(n, low, P.scale(c, b), False{} <> P.mul(q, b))
323	
324	def sa_sm(+n: Nat, +low: Word(n), +a: List<&2, Bool>, +z: Word(n), +v: Word(n)) -> {sa(n, low, a, z, v) == Word.xor(n, z, sm(n, low, a, v)) : Word(n)}:
325	  match a:
326	    case Nil{}:
327	      Equal.sym(Word(n), Word.xor(n, z, Word.zero(n)), z, xor_zero_r(n, z))
328	    case c <> r:
329	      %xor_assoc(n, z, P.wscale(n, c, v), sm(n, low, r, P.times_x(n, low, v))) : {sa(n, low, c <> r, z, v) == _ : Word(n)}
330	      sa_sm(n, low, r, Word.xor(n, z, P.wscale(n, c, v)), P.times_x(n, low, v))
331	
332	# ---- a residue is its own reduction ----
333	
334	# The first n coefficients of a list, zero-filled.
335	def wof(n: Nat, bs: List<&2, Bool>) -> Word(n):
336	  match n bs:
337	    case 0n _:
338	      WNil{}
339	    case 1n+p Nil{}:
340	      WCon{False{}, wof(p, Nil{})}
341	    case 1n+p b <> rest:
342	      WCon{b, wof(p, rest)}
343	
344	def wof_nil(+n: Nat) -> {Word.zero(n) == wof(n, Nil{}) : Word(n)}:
345	  match n:
346	    case 0n:
347	      {==}
348	    case 1n+p:
349	      %wof_nil(p) : {WCon{False{}, Word.zero(p)} == WCon{False{}, _} : Word(1n+p)}
350	      {==}
351	
352	def wof_false_nil(+q: Nat) -> {wof(q, [False{}]) == wof(q, Nil{}) : Word(q)}:
353	  match q:
354	    case 0n:
355	      {==}
356	    case 1n+r:
357	      {==}
358	
359	def put_wof(+p: Nat, +c: Bool, +l: List<&2, Bool>) -> {Word.shl.put(p, c, wof(p, l)) == wof(p, c <> l) : Word(p)}:
360	  match p l:
361	    case 0n _:
362	      {==}
363	    case 1n+q Nil{}:
364	      %Equal.sym(Word(q), Word.shl.put(q, False{}, wof(q, Nil{})), wof(q, [False{}]), put_wof(q, False{}, Nil{})) : {WCon{c, _} == WCon{c, wof(q, Nil{})} : Word(1n+q)}
365	      %wof_false_nil(q) : {WCon{c, wof(q, [False{}])} == WCon{c, _} : Word(1n+q)}
366	      {==}
367	    case 1n+q x <> xs:
368	      %put_wof(q, x, xs) : {WCon{c, Word.shl.put(q, x, wof(q, xs))} == WCon{c, _} : Word(1n+q)}
369	      {==}
370	
371	def shl_wof(+n: Nat, +l: List<&2, Bool>) -> {Word.shl(n, wof(n, l)) == wof(n, False{} <> l) : Word(n)}:
372	  match n l:
373	    case 0n _:
374	      {==}
375	    case 1n+p Nil{}:
376	      %wof_false_nil(p) : {WCon{False{}, Word.shl.put(p, False{}, wof(p, Nil{}))} == WCon{False{}, _} : Word(1n+p)}
377	      %put_wof(p, False{}, Nil{}) : {WCon{False{}, Word.shl.put(p, False{}, wof(p, Nil{}))} == WCon{False{}, _} : Word(1n+p)}
378	      {==}
379	    case 1n+p x <> xs:
380	      %put_wof(p, x, xs) : {WCon{False{}, Word.shl.put(p, x, wof(p, xs))} == WCon{False{}, _} : Word(1n+p)}
381	      {==}
382	
383	def top_short(+p: Nat, +l: List<&2, Bool>, +h: {Nat.is_le(List.length(&2, Bool, l), p) == True{} : Bool}) -> {P.top(1n+p, wof(1n+p, l)) == False{} : Bool}:
384	  match p l:
385	    case 0n Nil{}:
386	      {==}
387	    case 0n x <> xs:
388	      Empty.absurd({P.top(1n, wof(1n, x <> xs)) == False{} : Bool}, L.false_true(h))
389	    case 1n+q Nil{}:
390	      top_short(q, Nil{}, N.zero_le(q))
391	    case 1n+q x <> xs:
392	      top_short(q, xs, h)
393	
394	def red_short(+n: Nat, +low: Word(n), +l: List<&2, Bool>, +h: {Nat.is_le(List.length(&2, Bool, l), n) == True{} : Bool}) -> {P.reduce(n, low, l) == wof(n, l) : Word(n)}:
395	  match n l:
396	    case _ Nil{}:
397	      wof_nil(n)
398	    case 0n x <> xs:
399	      Empty.absurd({P.reduce(0n, low, x <> xs) == wof(0n, x <> xs) : Word(0n)}, L.false_true(h))
400	    case 1n+p x <> xs:
401	      +hp = {h : {Nat.is_le(List.length(&2, Bool, xs), p) == True{} : Bool}}
402	      %Equal.sym(Word(1n+p), P.reduce(1n+p, low, xs), wof(1n+p, xs), red_short(1n+p, low, xs, N.le_trans(List.length(&2, Bool, xs), p, 1n+p, hp, N.le_succ(p)))) : {Word.xor(1n+p, P.constant(1n+p, x), P.times_x(1n+p, low, _)) == wof(1n+p, x <> xs) : Word(1n+p)}
403	      %Equal.sym(Bool, P.top(1n+p, wof(1n+p, xs)), False{}, top_short(p, xs, hp)) : {Word.xor(1n+p, P.constant(1n+p, x), Word.xor(1n+p, P.wscale(1n+p, _, low), Word.shl(1n+p, wof(1n+p, xs)))) == wof(1n+p, x <> xs) : Word(1n+p)}
404	      %Equal.sym(Word(1n+p), Word.xor(1n+p, Word.zero(1n+p), Word.shl(1n+p, wof(1n+p, xs))), Word.shl(1n+p, wof(1n+p, xs)), xor_zero_l(1n+p, Word.shl(1n+p, wof(1n+p, xs)))) : {Word.xor(1n+p, P.constant(1n+p, x), _) == wof(1n+p, x <> xs) : Word(1n+p)}
405	      %Equal.sym(Word(1n+p), Word.shl(1n+p, wof(1n+p, xs)), wof(1n+p, False{} <> xs), shl_wof(1n+p, xs)) : {Word.xor(1n+p, P.constant(1n+p, x), _) == wof(1n+p, x <> xs) : Word(1n+p)}
406	      %Equal.sym(Word(p), Word.xor(p, Word.zero(p), wof(p, xs)), wof(p, xs), xor_zero_l(p, wof(p, xs))) : {WCon{Bool.xor(x, False{}), _} == wof(1n+p, x <> xs) : Word(1n+p)}
407	      %Equal.sym(Bool, Bool.xor(x, False{}), x, bxor_false(x)) : {WCon{_, wof(p, xs)} == wof(1n+p, x <> xs) : Word(1n+p)}
408	      {==}
409	
410	def wof_coefficients(+n: Nat, +w: Word(n)) -> {wof(n, P.coefficients(n, w)) == w : Word(n)}:
411	  match n w:
412	    case 0n WNil{}:
413	      {==}
414	    case 1n+p WCon{b, t}:
415	      %wof_coefficients(p, t) : {WCon{b, wof(p, P.coefficients(p, t))} == WCon{b, _} : Word(1n+p)}
416	      {==}
417	
418	def coefficients_le(+n: Nat, +w: Word(n)) -> {Nat.is_le(List.length(&2, Bool, P.coefficients(n, w)), n) == True{} : Bool}:
419	  match n w:
420	    case 0n WNil{}:
421	      {==}
422	    case 1n+p WCon{b, t}:
423	      coefficients_le(p, t)
424	
425	def red_coefficients(+n: Nat, +low: Word(n), +w: Word(n)) -> {P.reduce(n, low, P.coefficients(n, w)) == w : Word(n)}:
426	  Equal.trans(Word(n), P.reduce(n, low, P.coefficients(n, w)), wof(n, P.coefficients(n, w)), w,
427	    red_short(n, low, P.coefficients(n, w), coefficients_le(n, w)), wof_coefficients(n, w))
428	
429	# The product of two residues, reduced, is Algorithm 1 from Z = 0.
430	def mul_sa(+n: Nat, +low: Word(n), +a: Word(n), +b: Word(n)) -> {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == sa(n, low, P.coefficients(n, a), Word.zero(n), b) : Word(n)}:
431	  %Equal.sym(Word(n), sa(n, low, P.coefficients(n, a), Word.zero(n), b), Word.xor(n, Word.zero(n), sm(n, low, P.coefficients(n, a), b)), sa_sm(n, low, P.coefficients(n, a), Word.zero(n), b)) : {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == _ : Word(n)}
432	  %Equal.sym(Word(n), Word.xor(n, Word.zero(n), sm(n, low, P.coefficients(n, a), b)), sm(n, low, P.coefficients(n, a), b), xor_zero_l(n, sm(n, low, P.coefficients(n, a), b))) : {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == _ : Word(n)}
433	  %red_coefficients(n, low, b) : {P.reduce(n, low, P.mul(P.coefficients(n, a), P.coefficients(n, b))) == sm(n, low, P.coefficients(n, a), _) : Word(n)}
434	  red_mul(n, low, P.coefficients(n, a), P.coefficients(n, b))