proofs/crypto/aes/gf.bend

bend-collections-laws-crypto@1.0.0.0 · 434 lines · 44 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/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
14def bxor_false(+b: Bool) -> {Bool.xor(b, False{}) == b : Bool}:
15  match b:
16    case True{}:
17      {==}
18    case False{}:
19      {==}
20
21def 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
32def 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
51def bxor_self(+a: Bool) -> {Bool.xor(a, a) == False{} : Bool}:
52  match a:
53    case True{}:
54      {==}
55    case False{}:
56      {==}
57
58def 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
95def 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
103def 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
112def 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
121def 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
130def 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
139def 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
147def 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
155def 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
164def 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
173def 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
181def 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
189def 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
202def 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
208def 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
213def 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
222def 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
230def 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
242def 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
250def 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
257def 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
266def 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
274def 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
283def 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)
289def 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.
297def 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
304def 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
313def 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
324def 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.
335def 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
344def 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
352def 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
359def 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
371def 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
383def 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
394def 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
410def 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
418def 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
425def 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.
430def 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))