proof_word.bend

lawful-words@0.1.0.0 · 1,227 lines · 59 definitions

1import Base
2import lawful-words@0.1.0.0/proof_nat.bend as N
3
4# Facts about Word(n), n bits lowest first, as numbers: W(n, w) is
5# Word.to_nat(n, w) and P(n) is 2^n. Proven once for every width by
6# induction on n; proof_u32.bend specializes them to 32.
7
8# Numbers
9# =======
10
11# The value of a word with head bit b and tail t.
12law wcon:
13  for +p: Nat
14  for +b: Bool
15  for +t: Word(p)
16  {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))) : Nat}
17
18def wcon(p, b, t):
19  match b:
20    case False{}:
21      {==}
22    case True{}:
23      {==}
24
25law bn_lt2:
26  for +b: Bool
27  {Nat.is_lt(N.bn(b), 2n) == True{} : Bool}
28
29def bn_lt2(b):
30  match b:
31    case False{}:
32      {==}
33    case True{}:
34      {==}
35
36# The same value as t * 2 + b.
37law wcon2:
38  for +p: Nat
39  for +b: Bool
40  for +t: Word(p)
41  {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)) : Nat}
42
43def wcon2(p, b, t):
44  +x = Word.to_nat(p, t)
45  %Equal.sym(Nat, Nat.mul(x, 2n), Nat.double(x), N.mul2_r(x)) : {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(_, N.bn(b)) : Nat}
46  %N.add_comm(N.bn(b), Nat.double(x)) : {Word.to_nat(1n+p, WCon{b, t}) == _ : Nat}
47  wcon(p, b, t)
48
49# b + 2x < 2y when x < y.
50law lt_dbl_bit:
51  for +x: Nat
52  for +y: Nat
53  for +b: Bool
54  for +h: {Nat.is_lt(x, y) == True{} : Bool}
55  {Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), Nat.double(y)) == True{} : Bool}
56
57def lt_dbl_bit(x, y, b, h):
58  match x y:
59    case _ 0n:
60      Empty.absurd({Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), 0n) == True{} : Bool},
61        N.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(x, 0n), True{}, Equal.sym(Bool, Nat.is_lt(x, 0n), False{}, N.lt_zero(x)), h)))
62    case 0n 1n+q:
63      match b:
64        case False{}:
65          {==}
66        case True{}:
67          {==}
68    case 1n+p 1n+q:
69      match b:
70        case False{}:
71          lt_dbl_bit(p, q, False{}, h)
72        case True{}:
73          lt_dbl_bit(p, q, True{}, h)
74
75# b + 2x < 2y gives x < y.
76law lt_dbl_inv:
77  for +x: Nat
78  for +y: Nat
79  for +b: Bool
80  for +h: {Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), Nat.double(y)) == True{} : Bool}
81  {Nat.is_lt(x, y) == True{} : Bool}
82
83def lt_dbl_inv(x, y, b, h):
84  match x y:
85    case 0n 0n:
86      match b:
87        case False{}:
88          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, N.false_ne_true(h))
89        case True{}:
90          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, N.false_ne_true(h))
91    case 0n 1n+q:
92      {==}
93    case 1n+p 0n:
94      match b:
95        case False{}:
96          Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, N.false_ne_true(h))
97        case True{}:
98          Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, N.false_ne_true(h))
99    case 1n+p 1n+q:
100      match b:
101        case False{}:
102          lt_dbl_inv(p, q, False{}, h)
103        case True{}:
104          lt_dbl_inv(p, q, True{}, h)
105
106# (b + 2x) % 2q = b + 2 (x % q).
107law moddbl:
108  for +b: Bool
109  for +x: Nat
110  for +q: Nat
111  for +hq: {Nat.is_lt(0n, q) == True{} : Bool}
112  {Nat.mod(Nat.add(N.bn(b), Nat.double(x)), Nat.double(q)) == Nat.add(N.bn(b), Nat.double(Nat.mod(x, q))) : Nat}
113
114def moddbl(b, x, q, hq):
115  +d = Nat.div(x, q)
116  +r = Nat.mod(x, q)
117  +dq = Nat.double(q)
118  %N.div_mod(x, q) : {Nat.mod(Nat.add(N.bn(b), Nat.double(_)), dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
119  %Equal.sym(Nat, Nat.double(Nat.add(Nat.mul(d, q), r)), Nat.add(Nat.double(Nat.mul(d, q)), Nat.double(r)), N.dbl_dist(Nat.mul(d, q), r)) :
120    {Nat.mod(Nat.add(N.bn(b), _), dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
121  %N.mul_dbl_r(d, q) : {Nat.mod(Nat.add(N.bn(b), Nat.add(_, Nat.double(r))), dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
122  %N.add_left_comm(Nat.mul(d, dq), N.bn(b), Nat.double(r)) : {Nat.mod(_, dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
123  N.mod_mul_add(d, dq, Nat.add(N.bn(b), Nat.double(r)), lt_dbl_bit(r, q, b, N.mod_lt(x, q, hq)))
124
125# Every word stands for a number below 2^n.
126law wlt:
127  for +n: Nat
128  for +w: Word(n)
129  {Nat.is_lt(Word.to_nat(n, w), Nat.pow(2n, n)) == True{} : Bool}
130
131def wlt(n, w):
132  match n:
133    case 0n:
134      match w:
135        case WNil{}:
136          {==}
137    case 1n+p:
138      match w:
139        case WCon{+b, +t}:
140          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(Nat.pow(2n, p)), N.pow2s(p)) :
141            {Nat.is_lt(Word.to_nat(1n+p, WCon{b, t}), _) == True{} : Bool}
142          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wcon(p, b, t)) :
143            {Nat.is_lt(_, Nat.double(Nat.pow(2n, p))) == True{} : Bool}
144          lt_dbl_bit(Word.to_nat(p, t), Nat.pow(2n, p), b, wlt(p, t))
145
146# r + c * m = x with r < m gives x % m = r.
147law carry_mod:
148  for +r: Nat
149  for +c: Nat
150  for +m: Nat
151  for +x: Nat
152  for +e: {Nat.add(r, Nat.mul(c, m)) == x : Nat}
153  for +h: {Nat.is_lt(r, m) == True{} : Bool}
154  {Nat.mod(x, m) == r : Nat}
155
156def carry_mod(r, c, m, x, e, h):
157  %Equal.trans(Nat, Nat.add(Nat.mul(c, m), r), Nat.add(r, Nat.mul(c, m)), x, N.add_comm(Nat.mul(c, m), r), e) :
158    {Nat.mod(_, m) == r : Nat}
159  N.mod_mul_add(c, m, r, h)
160
161# Comparison
162# ==========
163
164law cmp_dbl:
165  for +x: Nat
166  for +y: Nat
167  for +a: Bool
168  for +b: Bool
169  {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(Nat.add(N.bn(a), Nat.double(x)), Nat.add(N.bn(b), Nat.double(y))) : Cmp}
170
171def cmp_dbl(x, y, a, b):
172  match x y:
173    case 0n 0n:
174      match a b:
175        case False{} False{}:
176          {==}
177        case False{} True{}:
178          {==}
179        case True{} False{}:
180          {==}
181        case True{} True{}:
182          {==}
183    case 0n 1n+q:
184      match a b:
185        case False{} False{}:
186          {==}
187        case False{} True{}:
188          {==}
189        case True{} False{}:
190          {==}
191        case True{} True{}:
192          {==}
193    case 1n+p 0n:
194      match a b:
195        case False{} False{}:
196          {==}
197        case False{} True{}:
198          {==}
199        case True{} False{}:
200          {==}
201        case True{} True{}:
202          {==}
203    case 1n+p 1n+q:
204      match a b:
205        case False{} False{}:
206          cmp_dbl(p, q, False{}, False{})
207        case False{} True{}:
208          cmp_dbl(p, q, False{}, True{})
209        case True{} False{}:
210          cmp_dbl(p, q, True{}, False{})
211        case True{} True{}:
212          cmp_dbl(p, q, True{}, True{})
213
214# Words compare as their numbers.
215law wcmp:
216  for +n: Nat
217  for +a: Word(n)
218  for +b: Word(n)
219  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
220
221def wcmp(n, a, b):
222  match n:
223    case 0n:
224      match a b:
225        case WNil{} WNil{}:
226          {==}
227    case 1n+p:
228      match a b:
229        case WCon{+x, +at} WCon{+y, +bt}:
230          %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), wcmp(p, at, bt)) :
231            {Word.cmp.fin(x, y, _) == Nat.cmp(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
232          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, at}), Nat.add(N.bn(x), Nat.double(Word.to_nat(p, at))), wcon(p, x, at)) :
233            {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))) == Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
234          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, bt}), Nat.add(N.bn(y), Nat.double(Word.to_nat(p, bt))), wcon(p, y, bt)) :
235            {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))) == Nat.cmp(Nat.add(N.bn(x), Nat.double(Word.to_nat(p, at))), _) : Cmp}
236          cmp_dbl(Word.to_nat(p, at), Word.to_nat(p, bt), x, y)
237
238def Cmp.disc_eq(c: Cmp) -> Type:
239  match c:
240    case EQ{}:
241      Empty
242    case o:
243      Unit
244
245def lt_ne_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:
246  %e : Cmp.disc_eq(_)
247  Unit{}
248
249def gt_ne_eq(e: {GT{} == EQ{} : Cmp}) -> Empty:
250  %e : Cmp.disc_eq(_)
251  Unit{}
252
253def bool_cmp_eq(+a: Bool, +b: Bool, e: {Bool.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Bool}:
254  match a b:
255    case False{} False{}:
256      {==}
257    case False{} True{}:
258      Empty.absurd({False{} == True{} : Bool}, lt_ne_eq(e))
259    case True{} False{}:
260      Empty.absurd({True{} == False{} : Bool}, gt_ne_eq(e))
261    case True{} True{}:
262      {==}
263
264def word_fin_t(+ab: Bool, +bb: Bool, +t: Cmp, e: {Word.cmp.fin(ab, bb, t) == EQ{} : Cmp}) -> {t == EQ{} : Cmp}:
265  match t:
266    case LT{}:
267      Empty.absurd({LT{} == EQ{} : Cmp}, lt_ne_eq(e))
268    case EQ{}:
269      {==}
270    case GT{}:
271      Empty.absurd({GT{} == EQ{} : Cmp}, gt_ne_eq(e))
272
273def word_fin_b(+ab: Bool, +bb: Bool, +t: Cmp, e: {Word.cmp.fin(ab, bb, t) == EQ{} : Cmp}) -> {Bool.cmp(ab, bb) == EQ{} : Cmp}:
274  match t:
275    case LT{}:
276      Empty.absurd({Bool.cmp(ab, bb) == EQ{} : Cmp}, lt_ne_eq(e))
277    case EQ{}:
278      e
279    case GT{}:
280      Empty.absurd({Bool.cmp(ab, bb) == EQ{} : Cmp}, gt_ne_eq(e))
281
282def word_cmp_eq(+n: Nat, +a: Word(n), +b: Word(n), +e: {Word.cmp(n, a, b) == EQ{} : Cmp}) -> {a == b : Word(n)}:
283  match n:
284    case 0n:
285      match a b:
286        case WNil{} WNil{}:
287          {==}
288    case 1n+p:
289      match a b:
290        case WCon{+ab, +at} WCon{+bb, +bt}:
291          %bool_cmp_eq(ab, bb, word_fin_b(ab, bb, Word.cmp(p, at, bt), e)) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
292          %word_cmp_eq(p, at, bt, word_fin_t(ab, bb, Word.cmp(p, at, bt), e)) : {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
293          {==}
294
295# Two words that stand for the same number are the same word.
296law winj:
297  for +n: Nat
298  for +a: Word(n)
299  for +b: Word(n)
300  for +e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
301  {a == b : Word(n)}
302
303def winj(n, a, b, e):
304  word_cmp_eq(n, a, b,
305    %Equal.sym(Cmp, Word.cmp(n, a, b), Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)), wcmp(n, a, b)) : {_ == EQ{} : Cmp}
306    %e : {Nat.cmp(Word.to_nat(n, a), _) == EQ{} : Cmp}
307    N.cmp_refl(Word.to_nat(n, a)))
308
309# Increment, addition, subtraction
310# ================================
311
312# The carry out of Word.inc: set when every bit is set.
313def incc(n: Nat, w: Word(n)) -> Bool:
314  match n:
315    case 0n:
316      True{}
317    case 1n+p:
318      match w:
319        case WCon{False{}, t}:
320          False{}
321        case WCon{True{}, t}:
322          incc(p, t)
323
324law winc:
325  for +n: Nat
326  for +w: Word(n)
327  {Nat.add(Word.to_nat(n, Word.inc(n, w)), Nat.mul(N.bn(incc(n, w)), Nat.pow(2n, n))) == 1n+Word.to_nat(n, w) : Nat}
328
329def winc(n, w):
330  match n:
331    case 0n:
332      match w:
333        case WNil{}:
334          {==}
335    case 1n+p:
336      match w:
337        case WCon{False{}, +t}:
338          %Equal.sym(Nat, Nat.add(Nat.double(Word.to_nat(p, t)), 0n), Nat.double(Word.to_nat(p, t)), N.add_zero(Nat.double(Word.to_nat(p, t)))) :
339            {1n+_ == 1n+Nat.double(Word.to_nat(p, t)) : Nat}
340          {==}
341        case WCon{True{}, +t}:
342          +i = Word.to_nat(p, Word.inc(p, t))
343          +c = N.bn(incc(p, t))
344          +pp = Nat.pow(2n, p)
345          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
346            {Nat.add(Nat.double(i), Nat.mul(c, _)) == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
347          %Equal.sym(Nat, Nat.mul(c, Nat.double(pp)), Nat.double(Nat.mul(c, pp)), N.mul_dbl_r(c, pp)) :
348            {Nat.add(Nat.double(i), _) == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
349          %N.dbl_dist(i, Nat.mul(c, pp)) : {_ == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
350          %Equal.sym(Nat, Nat.add(i, Nat.mul(c, pp)), 1n+Word.to_nat(p, t), winc(p, t)) : {Nat.double(_) == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
351          {==}
352
353# The carry out of Word.adc without inversion (f = False).
354def cout(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
355  match n:
356    case 0n:
357      c
358    case 1n+p:
359      match a b:
360        case WCon{False{}, at} WCon{bb, bt}:
361          cout(p, at, bt, Bool.and(bb, c))
362        case WCon{True{}, at} WCon{bb, bt}:
363          cout(p, at, bt, Bool.or(bb, c))
364
365# One bit of the sum, as numbers.
366law adc_step:
367  for +p: Nat
368  for +x: Nat
369  for +y: Nat
370  for +c: Nat
371  for +s: Nat
372  for +k: Nat
373  for +a: Nat
374  for +b: Nat
375  for +r: Nat
376  for +co: Nat
377  for +ih: {Nat.add(r, Nat.mul(co, Nat.pow(2n, p))) == Nat.add(k, Nat.add(a, b)) : Nat}
378  for +bit: {Nat.add(s, Nat.double(k)) == Nat.add(c, Nat.add(x, y)) : Nat}
379  {Nat.add(Nat.add(s, Nat.double(r)), Nat.mul(co, Nat.pow(2n, 1n+p)))
380    == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
381
382def adc_step(p, x, y, c, s, k, a, b, r, co, ih, bit):
383  +pp = Nat.pow(2n, p)
384  +dr = Nat.double(r)
385  +da = Nat.double(a)
386  +db = Nat.double(b)
387  +dk = Nat.double(k)
388  +rhs = Nat.add(c, Nat.add(Nat.add(x, da), Nat.add(y, db)))
389  %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
390    {Nat.add(Nat.add(s, dr), Nat.mul(co, _)) == rhs : Nat}
391  %Equal.sym(Nat, Nat.mul(co, Nat.double(pp)), Nat.double(Nat.mul(co, pp)), N.mul_dbl_r(co, pp)) :
392    {Nat.add(Nat.add(s, dr), _) == rhs : Nat}
393  %Equal.sym(Nat, Nat.add(Nat.add(s, dr), Nat.double(Nat.mul(co, pp))), Nat.add(s, Nat.add(dr, Nat.double(Nat.mul(co, pp)))),
394      N.add_assoc(s, dr, Nat.double(Nat.mul(co, pp)))) :
395    {_ == rhs : Nat}
396  %N.dbl_dist(r, Nat.mul(co, pp)) : {Nat.add(s, _) == rhs : Nat}
397  %Equal.sym(Nat, Nat.add(r, Nat.mul(co, pp)), Nat.add(k, Nat.add(a, b)), ih) : {Nat.add(s, Nat.double(_)) == rhs : Nat}
398  %Equal.sym(Nat, Nat.double(Nat.add(k, Nat.add(a, b))), Nat.add(dk, Nat.double(Nat.add(a, b))), N.dbl_dist(k, Nat.add(a, b))) :
399    {Nat.add(s, _) == rhs : Nat}
400  %Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(da, db), N.dbl_dist(a, b)) :
401    {Nat.add(s, Nat.add(dk, _)) == rhs : Nat}
402  %N.add_assoc(s, dk, Nat.add(da, db)) : {_ == rhs : Nat}
403  %Equal.sym(Nat, Nat.add(s, dk), Nat.add(c, Nat.add(x, y)), bit) : {Nat.add(_, Nat.add(da, db)) == rhs : Nat}
404  %Equal.sym(Nat, Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(da, db)), Nat.add(c, Nat.add(Nat.add(x, y), Nat.add(da, db))),
405      N.add_assoc(c, Nat.add(x, y), Nat.add(da, db))) :
406    {_ == rhs : Nat}
407  %Equal.sym(Nat, Nat.add(Nat.add(x, y), Nat.add(da, db)), Nat.add(Nat.add(x, da), Nat.add(y, db)), N.add_swap(x, y, da, db)) :
408    {Nat.add(c, _) == rhs : Nat}
409  {==}
410
411# The sum with its carry out: r + co * 2^n = c + a + b.
412law wadc:
413  for +n: Nat
414  for +a: Word(n)
415  for +b: Word(n)
416  for +c: Bool
417  {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.mul(N.bn(cout(n, a, b, c)), Nat.pow(2n, n)))
418    == Nat.add(N.bn(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}
419
420def wadc(n, a, b, c):
421  match n:
422    case 0n:
423      match a b c:
424        case WNil{} WNil{} False{}:
425          {==}
426        case WNil{} WNil{} True{}:
427          {==}
428    case 1n+p:
429      match a b c:
430        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
431          adc_step(p, 0n, 0n, 0n, 0n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
432            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
433        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
434          adc_step(p, 0n, 0n, 1n, 1n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
435            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
436        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
437          adc_step(p, 0n, 1n, 0n, 1n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
438            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
439        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
440          adc_step(p, 0n, 1n, 1n, 0n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
441            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
442        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
443          adc_step(p, 1n, 0n, 0n, 1n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
444            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
445        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
446          adc_step(p, 1n, 0n, 1n, 0n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
447            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
448        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
449          adc_step(p, 1n, 1n, 0n, 0n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
450            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
451        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
452          adc_step(p, 1n, 1n, 1n, 1n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
453            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
454
455# Subtraction is addition of the complement with carry in.
456def adc_t.con(-p: Nat, at: Word(p), bt: Word(p), sk: Bool & Bool,
457  ih: @k: Bool -> {Word.adc(p, at, bt, True{}, k) == Word.adc(p, at, Word.not(p, bt), False{}, k) : Word(p)}) ->
458  {Word.adc.con(p, at, bt, True{}, sk) == Word.adc.con(p, at, Word.not(p, bt), False{}, sk) : Word(1n+p)}:
459  match sk:
460    case (s, k):
461      %ih(k) : {WCon{s, Word.adc(p, at, bt, True{}, k)} == WCon{s, _} : Word(1n+p)}
462      {==}
463
464law adc_t:
465  for +n: Nat
466  for +a: Word(n)
467  for +b: Word(n)
468  for +c: Bool
469  {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}
470
471def adc_t(n, a, b, c):
472  match n:
473    case 0n:
474      match a b:
475        case WNil{} WNil{}:
476          {==}
477    case 1n+p:
478      match a b:
479        case WCon{+ab, +at} WCon{+bb, +bt}:
480          adc_t.con(p, at, bt, Bool.full_add(ab, Bool.not(bb), c), k => adc_t(p, at, bt, k))
481
482# not w and w add up to 2^n - 1.
483law wnot:
484  for +n: Nat
485  for +w: Word(n)
486  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}
487
488def wnot(n, w):
489  match n:
490    case 0n:
491      match w:
492        case WNil{}:
493          {==}
494    case 1n+p:
495      match w:
496        case WCon{False{}, +t}:
497          +x = Word.to_nat(p, Word.not(p, t))
498          +y = Word.to_nat(p, t)
499          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(Nat.pow(2n, p)), N.pow2s(p)) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == _ : Nat}
500          %wnot(p, t) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == Nat.double(_) : Nat}
501          %Equal.sym(Nat, Nat.double(Nat.add(x, y)), Nat.add(Nat.double(x), Nat.double(y)), N.dbl_dist(x, y)) :
502            {2n+Nat.add(Nat.double(x), Nat.double(y)) == 2n+_ : Nat}
503          {==}
504        case WCon{True{}, +t}:
505          +x = Word.to_nat(p, Word.not(p, t))
506          +y = Word.to_nat(p, t)
507          %Equal.sym(Nat, Nat.add(Nat.double(x), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(x), Nat.double(y)), N.add_succ(Nat.double(x), Nat.double(y))) :
508            {1n+_ == Nat.pow(2n, 1n+p) : Nat}
509          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(Nat.pow(2n, p)), N.pow2s(p)) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == _ : Nat}
510          %wnot(p, t) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == Nat.double(_) : Nat}
511          %Equal.sym(Nat, Nat.double(Nat.add(x, y)), Nat.add(Nat.double(x), Nat.double(y)), N.dbl_dist(x, y)) :
512            {2n+Nat.add(Nat.double(x), Nat.double(y)) == 2n+_ : Nat}
513          {==}
514
515# (a + 2^n) - b = 1 + a + not b.
516law wsub_val:
517  for +n: Nat
518  for +a: Word(n)
519  for +b: Word(n)
520  {Nat.sub(Nat.add(Word.to_nat(n, a), Nat.pow(2n, n)), Word.to_nat(n, b))
521    == 1n+Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))) : Nat}
522
523def wsub_val(n, a, b):
524  +x = Word.to_nat(n, a)
525  +y = Word.to_nat(n, b)
526  +z = Word.to_nat(n, Word.not(n, b))
527  %wnot(n, b) : {Nat.sub(Nat.add(x, _), y) == 1n+Nat.add(x, z) : Nat}
528  %Equal.sym(Nat, Nat.add(x, 1n+Nat.add(z, y)), 1n+Nat.add(x, Nat.add(z, y)), N.add_succ(x, Nat.add(z, y))) :
529    {Nat.sub(_, y) == 1n+Nat.add(x, z) : Nat}
530  %N.add_assoc(x, z, y) : {Nat.sub(1n+_, y) == 1n+Nat.add(x, z) : Nat}
531  N.sub_add(1n+Nat.add(x, z), y)
532
533# Shifts
534# ======
535
536# The bit shifted out of the top by Word.shl.put.
537def stop(n: Nat, c: Bool, w: Word(n)) -> Bool:
538  match n:
539    case 0n:
540      c
541    case 1n+p:
542      match w:
543        case WCon{b, t}:
544          stop(p, b, t)
545
546law wput:
547  for +n: Nat
548  for +c: Bool
549  for +w: Word(n)
550  {Nat.add(Word.to_nat(n, Word.shl.put(n, c, w)), Nat.mul(N.bn(stop(n, c, w)), Nat.pow(2n, n)))
551    == Nat.add(N.bn(c), Nat.double(Word.to_nat(n, w))) : Nat}
552
553def wput(n, c, w):
554  match n:
555    case 0n:
556      match c w:
557        case False{} WNil{}:
558          {==}
559        case True{} WNil{}:
560          {==}
561    case 1n+p:
562      match w:
563        case WCon{+b, +t}:
564          +s = Word.to_nat(p, Word.shl.put(p, b, t))
565          +o = N.bn(stop(p, b, t))
566          +pp = Nat.pow(2n, p)
567          +rhs = Nat.add(N.bn(c), Nat.double(Word.to_nat(1n+p, WCon{b, t})))
568          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{c, Word.shl.put(p, b, t)}), Nat.add(N.bn(c), Nat.double(s)), wcon(p, c, Word.shl.put(p, b, t))) :
569            {Nat.add(_, Nat.mul(o, Nat.pow(2n, 1n+p))) == rhs : Nat}
570          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
571            {Nat.add(Nat.add(N.bn(c), Nat.double(s)), Nat.mul(o, _)) == rhs : Nat}
572          %Equal.sym(Nat, Nat.mul(o, Nat.double(pp)), Nat.double(Nat.mul(o, pp)), N.mul_dbl_r(o, pp)) :
573            {Nat.add(Nat.add(N.bn(c), Nat.double(s)), _) == rhs : Nat}
574          %Equal.sym(Nat, Nat.add(Nat.add(N.bn(c), Nat.double(s)), Nat.double(Nat.mul(o, pp))), Nat.add(N.bn(c), Nat.add(Nat.double(s), Nat.double(Nat.mul(o, pp)))),
575              N.add_assoc(N.bn(c), Nat.double(s), Nat.double(Nat.mul(o, pp)))) :
576            {_ == rhs : Nat}
577          %N.dbl_dist(s, Nat.mul(o, pp)) : {Nat.add(N.bn(c), _) == rhs : Nat}
578          %Equal.sym(Nat, Nat.add(s, Nat.mul(o, pp)), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wput(p, b, t)) :
579            {Nat.add(N.bn(c), Nat.double(_)) == rhs : Nat}
580          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wcon(p, b, t)) :
581            {Nat.add(N.bn(c), Nat.double(Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))))) == Nat.add(N.bn(c), Nat.double(_)) : Nat}
582          {==}
583
584# The bit shifted out of the top by Word.shl.
585def shtop(n: Nat, w: Word(n)) -> Bool:
586  match n:
587    case 0n:
588      False{}
589    case 1n+p:
590      match w:
591        case WCon{b, t}:
592          stop(p, b, t)
593
594law wshl:
595  for +n: Nat
596  for +w: Word(n)
597  {Nat.add(Word.to_nat(n, Word.shl(n, w)), Nat.mul(N.bn(shtop(n, w)), Nat.pow(2n, n))) == Nat.double(Word.to_nat(n, w)) : Nat}
598
599def wshl(n, w):
600  match n:
601    case 0n:
602      match w:
603        case WNil{}:
604          {==}
605    case 1n+p:
606      match w:
607        case WCon{+b, +t}:
608          +s = Word.to_nat(p, Word.shl.put(p, b, t))
609          +o = N.bn(stop(p, b, t))
610          +pp = Nat.pow(2n, p)
611          +rhs = Nat.double(Word.to_nat(1n+p, WCon{b, t}))
612          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
613            {Nat.add(Nat.double(s), Nat.mul(o, _)) == rhs : Nat}
614          %Equal.sym(Nat, Nat.mul(o, Nat.double(pp)), Nat.double(Nat.mul(o, pp)), N.mul_dbl_r(o, pp)) :
615            {Nat.add(Nat.double(s), _) == rhs : Nat}
616          %N.dbl_dist(s, Nat.mul(o, pp)) : {_ == rhs : Nat}
617          %Equal.sym(Nat, Nat.add(s, Nat.mul(o, pp)), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wput(p, b, t)) :
618            {Nat.double(_) == rhs : Nat}
619          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wcon(p, b, t)) :
620            {Nat.double(Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t)))) == Nat.double(_) : Nat}
621          {==}
622
623law wshl_mod:
624  for +n: Nat
625  for +w: Word(n)
626  {Word.to_nat(n, Word.shl(n, w)) == Nat.mod(Nat.double(Word.to_nat(n, w)), Nat.pow(2n, n)) : Nat}
627
628def wshl_mod(n, w):
629  Equal.sym(Nat, Nat.mod(Nat.double(Word.to_nat(n, w)), Nat.pow(2n, n)), Word.to_nat(n, Word.shl(n, w)),
630    carry_mod(Word.to_nat(n, Word.shl(n, w)), N.bn(shtop(n, w)), Nat.pow(2n, n), Nat.double(Word.to_nat(n, w)),
631      wshl(n, w), wlt(n, Word.shl(n, w))))
632
633law wpad:
634  for +p: Nat
635  for +t: Word(p)
636  {Word.to_nat(1n+p, Word.shr.pad(p, t)) == Word.to_nat(p, t) : Nat}
637
638def wpad(p, t):
639  match p:
640    case 0n:
641      match t:
642        case WNil{}:
643          {==}
644    case 1n+q:
645      match t:
646        case WCon{False{}, +u}:
647          Equal.cong(Nat, Nat, x => Nat.double(x), Word.to_nat(1n+q, Word.shr.pad(q, u)), Word.to_nat(q, u), wpad(q, u))
648        case WCon{True{}, +u}:
649          Equal.cong(Nat, Nat, x => 1n+Nat.double(x), Word.to_nat(1n+q, Word.shr.pad(q, u)), Word.to_nat(q, u), wpad(q, u))
650
651law wdiv2:
652  for +p: Nat
653  for +b: Bool
654  for +t: Word(p)
655  {Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n) == Word.to_nat(p, t) : Nat}
656
657def wdiv2(p, b, t):
658  %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)), wcon2(p, b, t)) :
659    {Nat.div(_, 2n) == Word.to_nat(p, t) : Nat}
660  N.div_mul_add(Word.to_nat(p, t), 2n, N.bn(b), bn_lt2(b))
661
662law wshr:
663  for +n: Nat
664  for +w: Word(n)
665  {Word.to_nat(n, Word.shr(n, w)) == Nat.div(Word.to_nat(n, w), 2n) : Nat}
666
667def wshr(n, w):
668  match n:
669    case 0n:
670      match w:
671        case WNil{}:
672          {==}
673    case 1n+p:
674      match w:
675        case WCon{+b, +t}:
676          Equal.trans(Nat, Word.to_nat(1n+p, Word.shr.pad(p, t)), Word.to_nat(p, t), Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n),
677            wpad(p, t), Equal.sym(Nat, Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n), Word.to_nat(p, t), wdiv2(p, b, t)))
678
679# Addition and multiplication modulo 2^n
680# ======================================
681
682law wadd_mod:
683  for +n: Nat
684  for +a: Word(n)
685  for +b: Word(n)
686  {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) : Nat}
687
688def wadd_mod(n, a, b):
689  +r = Word.to_nat(n, Word.adc(n, a, b, False{}, False{}))
690  Equal.sym(Nat, Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)), r,
691    carry_mod(r, N.bn(cout(n, a, b, False{})), Nat.pow(2n, n), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)),
692      wadc(n, a, b, False{}), wlt(n, Word.adc(n, a, b, False{}, False{}))))
693
694law modmulin:
695  for +x: Nat
696  for +y: Nat
697  for +z: Nat
698  for +m: Nat
699  {Nat.mod(Nat.add(x, Nat.mul(y, Nat.mod(z, m))), m) == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}
700
701def modmulin(x, y, z, m):
702  %N.mod_add_mod_r(x, Nat.mul(y, Nat.mod(z, m)), m) : {_ == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}
703  %Equal.sym(Nat, Nat.mod(Nat.mul(y, Nat.mod(z, m)), m), Nat.mod(Nat.mul(y, z), m), N.mod_mul_mod_r(y, z, m)) :
704    {Nat.mod(Nat.add(x, _), m) == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}
705  N.mod_add_mod_r(x, Nat.mul(y, z), m)
706
707law wmul_go:
708  for +n: Nat
709  for +m: Nat
710  for +a: Word(m)
711  for +b: Word(n)
712  for +acc: Word(n)
713  {Word.to_nat(n, Word.mul.go(n, m, a, b, acc))
714    == Nat.mod(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))), Nat.pow(2n, n)) : Nat}
715
716def wmul_go(n, m, a, b, acc):
717  match m:
718    case 0n:
719      match a:
720        case WNil{}:
721          +c = Word.to_nat(n, acc)
722          %Equal.sym(Nat, Nat.add(c, 0n), c, N.add_zero(c)) : {c == Nat.mod(_, Nat.pow(2n, n)) : Nat}
723          Equal.sym(Nat, Nat.mod(c, Nat.pow(2n, n)), c, N.mod_small(c, Nat.pow(2n, n), wlt(n, acc)))
724    case 1n+mp:
725      match a:
726        case WCon{False{}, +at}:
727          +c = Word.to_nat(n, acc)
728          +x = Word.to_nat(mp, at)
729          +y = Word.to_nat(n, b)
730          +pn = Nat.pow(2n, n)
731          +rhs = Nat.mod(Nat.add(c, Nat.mul(Nat.double(x), y)), pn)
732          Equal.trans(Nat, Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)),
733            Nat.mod(Nat.add(c, Nat.mul(x, Word.to_nat(n, Word.shl(n, b)))), pn), rhs,
734            wmul_go(n, mp, at, Word.shl(n, b), acc),
735            %Equal.sym(Nat, Word.to_nat(n, Word.shl(n, b)), Nat.mod(Nat.double(y), pn), wshl_mod(n, b)) :
736              {Nat.mod(Nat.add(c, Nat.mul(x, _)), pn) == rhs : Nat}
737            %Equal.sym(Nat, Nat.mod(Nat.add(c, Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn), Nat.mod(Nat.add(c, Nat.mul(x, Nat.double(y))), pn),
738                modmulin(c, x, Nat.double(y), pn)) :
739              {_ == rhs : Nat}
740            %Equal.sym(Nat, Nat.mul(x, Nat.double(y)), Nat.double(Nat.mul(x, y)), N.mul_dbl_r(x, y)) :
741              {Nat.mod(Nat.add(c, _), pn) == rhs : Nat}
742            %Equal.sym(Nat, Nat.mul(Nat.double(x), y), Nat.double(Nat.mul(x, y)), N.mul_dbl_l(x, y)) :
743              {Nat.mod(Nat.add(c, Nat.double(Nat.mul(x, y))), pn) == Nat.mod(Nat.add(c, _), pn) : Nat}
744            {==})
745        case WCon{True{}, +at}:
746          +c = Word.to_nat(n, acc)
747          +x = Word.to_nat(mp, at)
748          +y = Word.to_nat(n, b)
749          +pn = Nat.pow(2n, n)
750          +rhs = Nat.mod(Nat.add(c, Nat.add(y, Nat.mul(Nat.double(x), y))), pn)
751          Equal.trans(Nat, Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))),
752            Nat.mod(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(x, Word.to_nat(n, Word.shl(n, b)))), pn), rhs,
753            wmul_go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)),
754            %Equal.sym(Nat, Word.to_nat(n, Word.add(n, acc, b)), Nat.mod(Nat.add(c, y), pn), wadd_mod(n, acc, b)) :
755              {Nat.mod(Nat.add(_, Nat.mul(x, Word.to_nat(n, Word.shl(n, b)))), pn) == rhs : Nat}
756            %Equal.sym(Nat, Word.to_nat(n, Word.shl(n, b)), Nat.mod(Nat.double(y), pn), wshl_mod(n, b)) :
757              {Nat.mod(Nat.add(Nat.mod(Nat.add(c, y), pn), Nat.mul(x, _)), pn) == rhs : Nat}
758            %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mod(Nat.add(c, y), pn), Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn),
759                Nat.mod(Nat.add(Nat.add(c, y), Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn),
760                N.mod_add_mod_l(Nat.add(c, y), Nat.mul(x, Nat.mod(Nat.double(y), pn)), pn)) :
761              {_ == rhs : Nat}
762            %Equal.sym(Nat, Nat.mod(Nat.add(Nat.add(c, y), Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn), Nat.mod(Nat.add(Nat.add(c, y), Nat.mul(x, Nat.double(y))), pn),
763                modmulin(Nat.add(c, y), x, Nat.double(y), pn)) :
764              {_ == rhs : Nat}
765            %Equal.sym(Nat, Nat.mul(x, Nat.double(y)), Nat.double(Nat.mul(x, y)), N.mul_dbl_r(x, y)) :
766              {Nat.mod(Nat.add(Nat.add(c, y), _), pn) == rhs : Nat}
767            %Equal.sym(Nat, Nat.mul(Nat.double(x), y), Nat.double(Nat.mul(x, y)), N.mul_dbl_l(x, y)) :
768              {Nat.mod(Nat.add(Nat.add(c, y), Nat.double(Nat.mul(x, y))), pn) == Nat.mod(Nat.add(c, Nat.add(y, _)), pn) : Nat}
769            %Equal.sym(Nat, Nat.add(Nat.add(c, y), Nat.double(Nat.mul(x, y))), Nat.add(c, Nat.add(y, Nat.double(Nat.mul(x, y)))),
770                N.add_assoc(c, y, Nat.double(Nat.mul(x, y)))) :
771              {Nat.mod(_, pn) == Nat.mod(Nat.add(c, Nat.add(y, Nat.double(Nat.mul(x, y)))), pn) : Nat}
772            {==})
773
774# Bits
775# ====
776
777# Bit k of a word (False from n up).
778def wbit(n: Nat, w: Word(n), k: Nat) -> Bool:
779  match n:
780    case 0n:
781      False{}
782    case 1n+p:
783      match w:
784        case WCon{b, t}:
785          match k:
786            case 0n:
787              b
788            case 1n+j:
789              wbit(p, t, j)
790
791law is_eq_bn:
792  for +b: Bool
793  {Nat.is_eq(N.bn(b), 1n) == b : Bool}
794
795def is_eq_bn(b):
796  match b:
797    case False{}:
798      {==}
799    case True{}:
800      {==}
801
802# The numeric bit (as in D.bit) is the word's bit.
803law wbit_num:
804  for +n: Nat
805  for +w: Word(n)
806  for +k: Nat
807  {Nat.is_eq(Nat.mod(Nat.div(Word.to_nat(n, w), Nat.pow(2n, k)), 2n), 1n) == wbit(n, w, k) : Bool}
808
809def wbit_num(n, w, k):
810  match n:
811    case 0n:
812      match w:
813        case WNil{}:
814          %Equal.sym(Nat, Nat.div(0n, Nat.pow(2n, k)), 0n, N.div_zero_l(Nat.pow(2n, k))) :
815            {Nat.is_eq(Nat.mod(_, 2n), 1n) == False{} : Bool}
816          {==}
817    case 1n+p:
818      match w:
819        case WCon{+b, +t}:
820          match k:
821            case 0n:
822              +x = Word.to_nat(1n+p, WCon{b, t})
823              %Equal.sym(Nat, Nat.div(x, 1n), x, N.div_one(x)) : {Nat.is_eq(Nat.mod(_, 2n), 1n) == b : Bool}
824              %Equal.sym(Nat, x, Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)), wcon2(p, b, t)) : {Nat.is_eq(Nat.mod(_, 2n), 1n) == b : Bool}
825              %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)), 2n), N.bn(b), N.mod_mul_add(Word.to_nat(p, t), 2n, N.bn(b), bn_lt2(b))) :
826                {Nat.is_eq(_, 1n) == b : Bool}
827              is_eq_bn(b)
828            case 1n+j:
829              +x = Word.to_nat(1n+p, WCon{b, t})
830              %N.div_div(x, 2n, Nat.pow(2n, j)) : {Nat.is_eq(Nat.mod(_, 2n), 1n) == wbit(p, t, j) : Bool}
831              %Equal.sym(Nat, Nat.div(x, 2n), Word.to_nat(p, t), wdiv2(p, b, t)) :
832                {Nat.is_eq(Nat.mod(Nat.div(_, Nat.pow(2n, j)), 2n), 1n) == wbit(p, t, j) : Bool}
833              wbit_num(p, t, j)
834
835law wbit_and:
836  for +n: Nat
837  for +a: Word(n)
838  for +b: Word(n)
839  for +k: Nat
840  {wbit(n, Word.and(n, a, b), k) == Bool.and(wbit(n, a, k), wbit(n, b, k)) : Bool}
841
842def wbit_and(n, a, b, k):
843  match n:
844    case 0n:
845      {==}
846    case 1n+p:
847      match a b:
848        case WCon{+x, +at} WCon{+y, +bt}:
849          match k:
850            case 0n:
851              {==}
852            case 1n+j:
853              wbit_and(p, at, bt, j)
854
855law wbit_or:
856  for +n: Nat
857  for +a: Word(n)
858  for +b: Word(n)
859  for +k: Nat
860  {wbit(n, Word.or(n, a, b), k) == Bool.or(wbit(n, a, k), wbit(n, b, k)) : Bool}
861
862def wbit_or(n, a, b, k):
863  match n:
864    case 0n:
865      {==}
866    case 1n+p:
867      match a b:
868        case WCon{+x, +at} WCon{+y, +bt}:
869          match k:
870            case 0n:
871              {==}
872            case 1n+j:
873              wbit_or(p, at, bt, j)
874
875law wbit_xor:
876  for +n: Nat
877  for +a: Word(n)
878  for +b: Word(n)
879  for +k: Nat
880  {wbit(n, Word.xor(n, a, b), k) == Bool.xor(wbit(n, a, k), wbit(n, b, k)) : Bool}
881
882def wbit_xor(n, a, b, k):
883  match n:
884    case 0n:
885      {==}
886    case 1n+p:
887      match a b:
888        case WCon{+x, +at} WCon{+y, +bt}:
889          match k:
890            case 0n:
891              {==}
892            case 1n+j:
893              wbit_xor(p, at, bt, j)
894
895law wbit_not:
896  for +n: Nat
897  for +a: Word(n)
898  for +k: Nat
899  {wbit(n, Word.not(n, a), k) == Bool.and(Nat.is_lt(k, n), Bool.not(wbit(n, a, k))) : Bool}
900
901def wbit_not(n, a, k):
902  match n:
903    case 0n:
904      match k:
905        case 0n:
906          {==}
907        case 1n+j:
908          {==}
909    case 1n+p:
910      match a:
911        case WCon{+x, +at}:
912          match k:
913            case 0n:
914              {==}
915            case 1n+j:
916              wbit_not(p, at, j)
917
918# The lowest bit where two words differ (0 if they are equal).
919def wdiff(n: Nat, a: Word(n), b: Word(n)) -> Nat:
920  match n:
921    case 0n:
922      0n
923    case 1n+p:
924      match a b:
925        case WCon{False{}, at} WCon{False{}, bt}:
926          1n+wdiff(p, at, bt)
927        case WCon{False{}, at} WCon{True{}, bt}:
928          0n
929        case WCon{True{}, at} WCon{False{}, bt}:
930          0n
931        case WCon{True{}, at} WCon{True{}, bt}:
932          1n+wdiff(p, at, bt)
933
934# Two words with the same bit where they would first differ are equal.
935law wext:
936  for +n: Nat
937  for +a: Word(n)
938  for +b: Word(n)
939  for +e: {wbit(n, a, wdiff(n, a, b)) == wbit(n, b, wdiff(n, a, b)) : Bool}
940  {a == b : Word(n)}
941
942def wext(n, a, b, e):
943  match n:
944    case 0n:
945      match a b:
946        case WNil{} WNil{}:
947          {==}
948    case 1n+p:
949      match a b:
950        case WCon{False{}, +at} WCon{False{}, +bt}:
951          %wext(p, at, bt, e) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)}
952          {==}
953        case WCon{False{}, +at} WCon{True{}, +bt}:
954          Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)}, N.false_ne_true(e))
955        case WCon{True{}, +at} WCon{False{}, +bt}:
956          Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)}, N.true_ne_false(e))
957        case WCon{True{}, +at} WCon{True{}, +bt}:
958          %wext(p, at, bt, e) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)}
959          {==}
960
961# Masks and disjoint words
962# ========================
963
964law moddbl_w:
965  for +p: Nat
966  for +x: Bool
967  for +t: Word(p)
968  for +j: Nat
969  {Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}
970
971def moddbl_w(p, x, t, j):
972  %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, t}), Nat.add(N.bn(x), Nat.double(Word.to_nat(p, t))), wcon(p, x, t)) :
973    {Nat.mod(_, Nat.pow(2n, 1n+j)) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}
974  %Equal.sym(Nat, Nat.pow(2n, 1n+j), Nat.double(Nat.pow(2n, j)), N.pow2s(j)) :
975    {Nat.mod(Nat.add(N.bn(x), Nat.double(Word.to_nat(p, t))), _) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}
976  moddbl(x, Word.to_nat(p, t), Nat.pow(2n, j), N.pow_pos(j))
977
978law lt_w:
979  for +p: Nat
980  for +y: Bool
981  for +t: Word(p)
982  for +j: Nat
983  for +h: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, t}), Nat.pow(2n, 1n+j)) == True{} : Bool}
984  {Nat.is_lt(Word.to_nat(p, t), Nat.pow(2n, j)) == True{} : Bool}
985
986def lt_w(p, y, t, j, h):
987  lt_dbl_inv(Word.to_nat(p, t), Nat.pow(2n, j), y,
988    %wcon(p, y, t) : {Nat.is_lt(_, Nat.double(Nat.pow(2n, j))) == True{} : Bool}
989    %N.pow2s(j) : {Nat.is_lt(Word.to_nat(1n+p, WCon{y, t}), _) == True{} : Bool}
990    h)
991
992law mask_step:
993  for +p: Nat
994  for +x: Bool
995  for +t: Word(p)
996  for +j: Nat
997  for +r: Nat
998  for +ih: {r == Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)) : Nat}
999  {Nat.add(N.bn(x), Nat.double(r)) == Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)) : Nat}
1000
1001def mask_step(p, x, t, j, r, ih):
1002  %Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)), Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))), moddbl_w(p, x, t, j)) :
1003    {Nat.add(N.bn(x), Nat.double(r)) == _ : Nat}
1004  %ih : {Nat.add(N.bn(x), Nat.double(r)) == Nat.add(N.bn(x), Nat.double(_)) : Nat}
1005  {==}
1006
1007# And with a word standing for 2^k - 1 keeps the low k bits.
1008law and_mask:
1009  for +n: Nat
1010  for +a: Word(n)
1011  for +m: Word(n)
1012  for +k: Nat
1013  for +h: {Word.to_nat(n, m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1014  {Word.to_nat(n, Word.and(n, a, m)) == Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) : Nat}
1015
1016def and_mask(n, a, m, k, h):
1017  match n:
1018    case 0n:
1019      match a m:
1020        case WNil{} WNil{}:
1021          Equal.sym(Nat, Nat.mod(0n, Nat.pow(2n, k)), 0n, N.mod_zero_l(Nat.pow(2n, k)))
1022    case 1n+p:
1023      match a m k:
1024        case WCon{+x, +at} WCon{False{}, +mt} 0n:
1025          +ih = and_mask(p, at, mt, 0n, N.dbl_zero(Word.to_nat(p, mt), h))
1026          +r = Word.to_nat(p, Word.and(p, at, mt))
1027          %Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{x, at}), 1n), 0n, N.mod_one(Word.to_nat(1n+p, WCon{x, at}))) :
1028            {Word.to_nat(1n+p, WCon{Bool.and(x, False{}), Word.and(p, at, mt)}) == _ : Nat}
1029          %Equal.sym(Bool, Bool.and(x, False{}), False{}, N.and_false_r(x)) :
1030            {Word.to_nat(1n+p, WCon{_, Word.and(p, at, mt)}) == 0n : Nat}
1031          %Equal.sym(Nat, r, Nat.mod(Word.to_nat(p, at), 1n), ih) : {Nat.double(_) == 0n : Nat}
1032          %Equal.sym(Nat, Nat.mod(Word.to_nat(p, at), 1n), 0n, N.mod_one(Word.to_nat(p, at))) : {Nat.double(_) == 0n : Nat}
1033          {==}
1034        case WCon{+x, +at} WCon{True{}, +mt} 0n:
1035          Empty.absurd({Word.to_nat(1n+p, WCon{Bool.and(x, True{}), Word.and(p, at, mt)}) == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), 1n) : Nat},
1036            N.succ_ne_zero(Nat.double(Word.to_nat(p, mt)), h))
1037        case WCon{+x, +at} WCon{False{}, +mt} 1n+j:
1038          Empty.absurd({Word.to_nat(1n+p, WCon{Bool.and(x, False{}), Word.and(p, at, mt)}) == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) : Nat},
1039            N.dbl_ne_odd(Word.to_nat(p, mt), Nat.sub(Nat.pow(2n, j), 1n),
1040              Equal.trans(Nat, Nat.double(Word.to_nat(p, mt)), Nat.sub(Nat.pow(2n, 1n+j), 1n), 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)), h, N.pow_sub1(j))))
1041        case WCon{+x, +at} WCon{True{}, +mt} 1n+j:
1042          +hm = N.dbl_inj(Word.to_nat(p, mt), Nat.sub(Nat.pow(2n, j), 1n),
1043            N.succ_inj(Nat.double(Word.to_nat(p, mt)), Nat.double(Nat.sub(Nat.pow(2n, j), 1n)),
1044              Equal.trans(Nat, 1n+Nat.double(Word.to_nat(p, mt)), Nat.sub(Nat.pow(2n, 1n+j), 1n), 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)), h, N.pow_sub1(j))))
1045          %Equal.sym(Bool, Bool.and(x, True{}), x, N.and_true_r_id(x)) :
1046            {Word.to_nat(1n+p, WCon{_, Word.and(p, at, mt)}) == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) : Nat}
1047          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, Word.and(p, at, mt)}), Nat.add(N.bn(x), Nat.double(Word.to_nat(p, Word.and(p, at, mt)))), wcon(p, x, Word.and(p, at, mt))) :
1048            {_ == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) : Nat}
1049          mask_step(p, x, at, j, Word.to_nat(p, Word.and(p, at, mt)), and_mask(p, at, mt, j, hm))
1050
1051# x < 1 gives x = 0.
1052law lt_one:
1053  for +x: Nat
1054  for +h: {Nat.is_lt(x, 1n) == True{} : Bool}
1055  {x == 0n : Nat}
1056
1057def lt_one(x, h):
1058  match x:
1059    case 0n:
1060      {==}
1061    case 1n+p:
1062      Empty.absurd({1n+p == 0n : Nat}, N.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(p, 0n), True{}, Equal.sym(Bool, Nat.is_lt(p, 0n), False{}, N.lt_zero(p)), h)))
1063
1064law or_zero:
1065  for +n: Nat
1066  for +a: Word(n)
1067  for +b: Word(n)
1068  for +h: {Word.to_nat(n, b) == 0n : Nat}
1069  {Word.to_nat(n, Word.or(n, a, b)) == Word.to_nat(n, a) : Nat}
1070
1071def or_zero(n, a, b, h):
1072  match n:
1073    case 0n:
1074      match a b:
1075        case WNil{} WNil{}:
1076          {==}
1077    case 1n+p:
1078      match a b:
1079        case WCon{False{}, +at} WCon{False{}, +bt}:
1080          Equal.cong(Nat, Nat, z => Nat.double(z), Word.to_nat(p, Word.or(p, at, bt)), Word.to_nat(p, at), or_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1081        case WCon{True{}, +at} WCon{False{}, +bt}:
1082          Equal.cong(Nat, Nat, z => 1n+Nat.double(z), Word.to_nat(p, Word.or(p, at, bt)), Word.to_nat(p, at), or_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1083        case WCon{+x, +at} WCon{True{}, +bt}:
1084          Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{True{}, bt})) == Word.to_nat(1n+p, WCon{x, at}) : Nat},
1085            N.succ_ne_zero(Nat.double(Word.to_nat(p, bt)), h))
1086
1087law xor_zero:
1088  for +n: Nat
1089  for +a: Word(n)
1090  for +b: Word(n)
1091  for +h: {Word.to_nat(n, b) == 0n : Nat}
1092  {Word.to_nat(n, Word.xor(n, a, b)) == Word.to_nat(n, a) : Nat}
1093
1094def xor_zero(n, a, b, h):
1095  match n:
1096    case 0n:
1097      match a b:
1098        case WNil{} WNil{}:
1099          {==}
1100    case 1n+p:
1101      match a b:
1102        case WCon{False{}, +at} WCon{False{}, +bt}:
1103          Equal.cong(Nat, Nat, z => Nat.double(z), Word.to_nat(p, Word.xor(p, at, bt)), Word.to_nat(p, at), xor_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1104        case WCon{True{}, +at} WCon{False{}, +bt}:
1105          Equal.cong(Nat, Nat, z => 1n+Nat.double(z), Word.to_nat(p, Word.xor(p, at, bt)), Word.to_nat(p, at), xor_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1106        case WCon{+x, +at} WCon{True{}, +bt}:
1107          Empty.absurd({Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{True{}, bt})) == Word.to_nat(1n+p, WCon{x, at}) : Nat},
1108            N.succ_ne_zero(Nat.double(Word.to_nat(p, bt)), h))
1109
1110# y + 2r = 2a + (y + 2b) when r = a + b.
1111law split_step:
1112  for +y: Bool
1113  for +a: Nat
1114  for +b: Nat
1115  for +r: Nat
1116  for +ih: {r == Nat.add(a, b) : Nat}
1117  {Nat.add(N.bn(y), Nat.double(r)) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}
1118
1119def split_step(y, a, b, r, ih):
1120  %Equal.sym(Nat, r, Nat.add(a, b), ih) : {Nat.add(N.bn(y), Nat.double(_)) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}
1121  %Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(Nat.double(a), Nat.double(b)), N.dbl_dist(a, b)) :
1122    {Nat.add(N.bn(y), _) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}
1123  N.add_left_comm(N.bn(y), Nat.double(a), Nat.double(b))
1124
1125def or_split.s(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), +j: Nat,
1126  ha: {Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) == 0n : Nat},
1127  hb: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, bt}), Nat.pow(2n, 1n+j)) == True{} : Bool},
1128  ih: {Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)) == 0n : Nat} -> {Nat.is_lt(Word.to_nat(p, bt), Nat.pow(2n, j)) == True{} : Bool} ->
1129    {Word.to_nat(p, Word.or(p, at, bt)) == Nat.add(Word.to_nat(p, at), Word.to_nat(p, bt)) : Nat}) ->
1130  {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat}:
1131  match x y:
1132    case True{} _:
1133      Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat},
1134        N.succ_ne_zero(Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))),
1135          Equal.trans(Nat, 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 0n,
1136            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, True{}, at, j)),
1137            ha)))
1138    case False{} False{}:
1139      split_step(False{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
1140        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1141          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1142            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1143            ha)))(lt_w(p, False{}, bt, j, hb)))
1144    case False{} True{}:
1145      split_step(True{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
1146        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1147          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1148            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1149            ha)))(lt_w(p, True{}, bt, j, hb)))
1150
1151# Or of a word with only bits from k up and a word below 2^k is their sum.
1152law or_split:
1153  for +n: Nat
1154  for +a: Word(n)
1155  for +b: Word(n)
1156  for +k: Nat
1157  for +ha: {Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) == 0n : Nat}
1158  for +hb: {Nat.is_lt(Word.to_nat(n, b), Nat.pow(2n, k)) == True{} : Bool}
1159  {Word.to_nat(n, Word.or(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
1160
1161def or_split(n, a, b, k, ha, hb):
1162  match n:
1163    case 0n:
1164      match a b:
1165        case WNil{} WNil{}:
1166          {==}
1167    case 1n+p:
1168      match a b k:
1169        case WCon{+x, +at} WCon{+y, +bt} 0n:
1170          +ea = Word.to_nat(1n+p, WCon{x, at})
1171          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, bt}), 0n, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb)) : {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(ea, _) : Nat}
1172          %Equal.sym(Nat, Nat.add(ea, 0n), ea, N.add_zero(ea)) : {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == _ : Nat}
1173          or_zero(1n+p, WCon{x, at}, WCon{y, bt}, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb))
1174        case WCon{+x, +at} WCon{+y, +bt} 1n+j:
1175          or_split.s(p, x, y, at, bt, j, ha, hb, ha2 => hb2 => or_split(p, at, bt, j, ha2, hb2))
1176
1177def xor_split.s(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), +j: Nat,
1178  ha: {Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) == 0n : Nat},
1179  hb: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, bt}), Nat.pow(2n, 1n+j)) == True{} : Bool},
1180  ih: {Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)) == 0n : Nat} -> {Nat.is_lt(Word.to_nat(p, bt), Nat.pow(2n, j)) == True{} : Bool} ->
1181    {Word.to_nat(p, Word.xor(p, at, bt)) == Nat.add(Word.to_nat(p, at), Word.to_nat(p, bt)) : Nat}) ->
1182  {Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat}:
1183  match x y:
1184    case True{} _:
1185      Empty.absurd({Word.to_nat(1n+p, Word.xor(1n+p, WCon{True{}, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat},
1186        N.succ_ne_zero(Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))),
1187          Equal.trans(Nat, 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 0n,
1188            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, True{}, at, j)),
1189            ha)))
1190    case False{} False{}:
1191      split_step(False{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.xor(p, at, bt)),
1192        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1193          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1194            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1195            ha)))(lt_w(p, False{}, bt, j, hb)))
1196    case False{} True{}:
1197      split_step(True{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.xor(p, at, bt)),
1198        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1199          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1200            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1201            ha)))(lt_w(p, True{}, bt, j, hb)))
1202
1203# Xor likewise.
1204law xor_split:
1205  for +n: Nat
1206  for +a: Word(n)
1207  for +b: Word(n)
1208  for +k: Nat
1209  for +ha: {Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) == 0n : Nat}
1210  for +hb: {Nat.is_lt(Word.to_nat(n, b), Nat.pow(2n, k)) == True{} : Bool}
1211  {Word.to_nat(n, Word.xor(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
1212
1213def xor_split(n, a, b, k, ha, hb):
1214  match n:
1215    case 0n:
1216      match a b:
1217        case WNil{} WNil{}:
1218          {==}
1219    case 1n+p:
1220      match a b k:
1221        case WCon{+x, +at} WCon{+y, +bt} 0n:
1222          +ea = Word.to_nat(1n+p, WCon{x, at})
1223          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, bt}), 0n, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb)) : {Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(ea, _) : Nat}
1224          %Equal.sym(Nat, Nat.add(ea, 0n), ea, N.add_zero(ea)) : {Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{y, bt})) == _ : Nat}
1225          xor_zero(1n+p, WCon{x, at}, WCon{y, bt}, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb))
1226        case WCon{+x, +at} WCon{+y, +bt} 1n+j:
1227          xor_split.s(p, x, y, at, bt, j, ha, hb, ha2 => hb2 => xor_split(p, at, bt, j, ha2, hb2))