lemmas.bend

bend-kit-lemmas@0.1.1.0 · 746 lines · 45 definitions

1# Proved laws that relate Word and U32 arithmetic to Nat. Source: https://github.com/paymog/bend-kit/tree/main/lemmas
2import Base
3import bend-mathlib@0.7.4.0/nat.bend as MNat
4
5# 2^n, by the doubling that Word.to_nat uses.
6def pow2(n: Nat) -> Nat:
7  match n:
8    case 0n:
9      1n
10    case 1n+p:
11      Nat.double(pow2(p))
12
13# The value of a word whose low bit is x and whose upper bits have value t.
14def bit(x: Bool, t: Nat) -> Nat:
15  match x:
16    case False{}:
17      Nat.double(t)
18    case True{}:
19      1n+Nat.double(t)
20
21law to_nat_con:
22  for -p: Nat
23  for x: Bool
24  for -t: Word(p)
25  {bit(x, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{x, t}) : Nat}
26
27def to_nat_con(p, x, t):
28  match x:
29    case False{}:
30      {==}
31    case True{}:
32      {==}
33
34law cmp_bit:
35  for a: Nat
36  for b: Nat
37  for x: Bool
38  for y: Bool
39  {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(bit(x, a), bit(y, b)) : Cmp}
40
41def cmp_bit(a, b, x, y):
42  match a b:
43    case 0n 0n:
44      match x y:
45        case False{} False{}:
46          {==}
47        case False{} True{}:
48          {==}
49        case True{} False{}:
50          {==}
51        case True{} True{}:
52          {==}
53    case 0n 1n+q:
54      match x y:
55        case False{} False{}:
56          {==}
57        case False{} True{}:
58          {==}
59        case True{} False{}:
60          {==}
61        case True{} True{}:
62          {==}
63    case 1n+p 0n:
64      match x y:
65        case False{} False{}:
66          {==}
67        case False{} True{}:
68          {==}
69        case True{} False{}:
70          {==}
71        case True{} True{}:
72          {==}
73    case 1n+p 1n+q:
74      match x y:
75        case False{} False{}:
76          cmp_bit(p, q, False{}, False{})
77        case False{} True{}:
78          cmp_bit(p, q, False{}, True{})
79        case True{} False{}:
80          cmp_bit(p, q, True{}, False{})
81        case True{} True{}:
82          cmp_bit(p, q, True{}, True{})
83
84# Comparing two words compares their values.
85law word_cmp_nat:
86  for n: Nat
87  for a: Word(n)
88  for b: Word(n)
89  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
90
91def word_cmp_nat(n, a, b):
92  match n:
93    case 0n:
94      {==}
95    case 1n+ +p:
96      match a b:
97        case WCon{+x, +at} WCon{+y, +bt}:
98          %to_nat_con(p, x, at) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) ==
99            Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
100          %to_nat_con(p, y, bt) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) ==
101            Nat.cmp(bit(x, Word.to_nat(p, at)), _) : Cmp}
102          %cmp_bit(Word.to_nat(p, at), Word.to_nat(p, bt), x, y) :
103            {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == _ : Cmp}
104          %word_cmp_nat(p, at, bt) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) ==
105            Word.cmp.fin(x, y, _) : Cmp}
106          {==}
107
108law u32_cmp_nat:
109  for a: U32
110  for b: U32
111  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
112
113def u32_cmp_nat(a, b):
114  match a b:
115    case U32{x} U32{y}:
116      word_cmp_nat(32n, x, y)
117
118law u32_is_lt_nat:
119  for a: U32
120  for b: U32
121  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
122
123def u32_is_lt_nat(a, b):
124  Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), U32.cmp(a, b),
125    Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))
126
127law u32_is_le_nat:
128  for a: U32
129  for b: U32
130  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
131
132def u32_is_le_nat(a, b):
133  Equal.cong(Cmp, Bool, c => Cmp.is_le(c), U32.cmp(a, b),
134    Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))
135
136law u32_is_eq_nat:
137  for a: U32
138  for b: U32
139  {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
140
141def u32_is_eq_nat(a, b):
142  Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b),
143    Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))
144
145law odd_lt_double:
146  for a: Nat
147  for b: Nat
148  for h: MNat.lt(a, b)
149  MNat.lt(1n+Nat.double(a), Nat.double(b))
150
151def odd_lt_double(a, b, h):
152  match a b:
153    case 0n 0n:
154      Empty.absurd(MNat.lt(1n, 0n), MNat.lt_zero(0n)(h))
155    case 0n 1n+q:
156      {==}
157    case 1n+p 0n:
158      Empty.absurd(MNat.lt(1n+Nat.double(1n+p), 0n), MNat.lt_zero(1n+p)(h))
159    case 1n+p 1n+q:
160      odd_lt_double(p, q, h)
161
162# A word of n bits has a value below 2^n.
163law word_to_nat_lt:
164  for n: Nat
165  for w: Word(n)
166  MNat.lt(Word.to_nat(n, w), pow2(n))
167
168def word_to_nat_lt(n, w):
169  match n:
170    case 0n:
171      {==}
172    case 1n+ +p:
173      match w:
174        case WCon{False{}, +t}:
175          MNat.double_lt_double(Word.to_nat(p, t), pow2(p), word_to_nat_lt(p, t))
176        case WCon{True{}, +t}:
177          odd_lt_double(Word.to_nat(p, t), pow2(p), word_to_nat_lt(p, t))
178
179law u32_to_nat_word:
180  for -x: Word(32n)
181  {Word.to_nat(32n, x) == U32.to_nat(U32{x}) : Nat}
182
183def u32_to_nat_word(x):
184  {==}
185
186law u32_to_nat_lt:
187  for a: U32
188  MNat.lt(U32.to_nat(a), pow2(32n))
189
190def u32_to_nat_lt(a):
191  match a:
192    case U32{+x}:
193      # A conversion here expands pow2(32n) and overflows the checker stack (bendlang/bend#1071).
194      %u32_to_nat_word(x) : MNat.lt(_, pow2(32n))
195      word_to_nat_lt(32n, x)
196
197law double_inj:
198  for a: Nat
199  for b: Nat
200  for h: {Nat.double(a) == Nat.double(b) : Nat}
201  {a == b : Nat}
202
203def double_inj(a, b, h):
204  match a b:
205    case 0n 0n:
206      {==}
207    case 0n 1n+q:
208      Empty.absurd({0n == 1n+q : Nat}, MNat.zero_ne_succ(1n+Nat.double(q))(h))
209    case 1n+p 0n:
210      Empty.absurd({1n+p == 0n : Nat}, MNat.succ_ne_zero(1n+Nat.double(p))(h))
211    case 1n+p 1n+q:
212      Equal.cong(Nat, Nat, k => 1n+k, p, q,
213        double_inj(p, q, MNat.succ_inj(Nat.double(p), Nat.double(q),
214          MNat.succ_inj(1n+Nat.double(p), 1n+Nat.double(q), h))))
215
216law double_ne_odd:
217  for a: Nat
218  for b: Nat
219  for h: {Nat.double(a) == 1n+Nat.double(b) : Nat}
220  Empty
221
222def double_ne_odd(a, b, h):
223  match a b:
224    case 0n 0n:
225      MNat.zero_ne_succ(0n)(h)
226    case 0n 1n+q:
227      MNat.zero_ne_succ(2n+Nat.double(q))(h)
228    case 1n+p 0n:
229      MNat.succ_ne_zero(Nat.double(p))(MNat.succ_inj(1n+Nat.double(p), 0n, h))
230    case 1n+p 1n+q:
231      double_ne_odd(p, q, MNat.succ_inj(Nat.double(p), 1n+Nat.double(q),
232        MNat.succ_inj(1n+Nat.double(p), 2n+Nat.double(q), h)))
233
234# Two words with the same value are the same word.
235law word_to_nat_inj:
236  for n: Nat
237  for a: Word(n)
238  for b: Word(n)
239  for h: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
240  {a == b : Word(n)}
241
242def word_to_nat_inj(n, a, b, h):
243  match n:
244    case 0n:
245      match a b:
246        case WNil{} WNil{}:
247          {==}
248    case 1n+ +p:
249      match a b:
250        case WCon{False{}, +at} WCon{False{}, +bt}:
251          Equal.cong(Word(p), Word(1n+p), t => WCon{False{}, t}, at, bt,
252            word_to_nat_inj(p, at, bt, double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), h)))
253        case WCon{True{}, +at} WCon{True{}, +bt}:
254          Equal.cong(Word(p), Word(1n+p), t => WCon{True{}, t}, at, bt,
255            word_to_nat_inj(p, at, bt, double_inj(Word.to_nat(p, at), Word.to_nat(p, bt),
256              MNat.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h))))
257        case WCon{False{}, +at} WCon{True{}, +bt}:
258          Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)},
259            double_ne_odd(Word.to_nat(p, at), Word.to_nat(p, bt), h))
260        case WCon{True{}, +at} WCon{False{}, +bt}:
261          Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)},
262            double_ne_odd(Word.to_nat(p, bt), Word.to_nat(p, at),
263              Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h)))
264
265law u32_to_nat_inj:
266  for a: U32
267  for b: U32
268  for h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
269  {a == b : U32}
270
271def u32_to_nat_inj(a, b, h):
272  match a b:
273    case U32{+x} U32{+y}:
274      Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_to_nat_inj(32n, x, y, h))
275
276def b2n(b: Bool) -> Nat:
277  match b:
278    case False{}:
279      0n
280    case True{}:
281      1n
282
283# m when q is set, else 0.
284def scale(q: Bool, m: Nat) -> Nat:
285  match q:
286    case False{}:
287      0n
288    case True{}:
289      m
290
291# The carry out of a full adder: set when two or three of the bits are set.
292def maj(x: Bool, y: Bool, c: Bool) -> Bool:
293  match x y:
294    case False{} False{}:
295      False{}
296    case True{} True{}:
297      True{}
298    case False{} True{}:
299      c
300    case True{} False{}:
301      c
302
303# The carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.
304def carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
305  match n:
306    case 0n:
307      c
308    case 1n+p:
309      match a b:
310        case WCon{x, at} WCon{y, bt}:
311          carry(p, at, bt, maj(x, y, c))
312
313law scale_double:
314  for q: Bool
315  for -m: Nat
316  {Nat.double(scale(q, m)) == scale(q, Nat.double(m)) : Nat}
317
318def scale_double(q, m):
319  match q:
320    case False{}:
321      {==}
322    case True{}:
323      {==}
324
325# One bit of the adder: s + 2k is the sum c + x + y of the three input bits.
326law adc_step:
327  for +s: Nat
328  for +x: Nat
329  for +y: Nat
330  for +c: Nat
331  for +k: Nat
332  for +r: Nat
333  for +q: Bool
334  for +m: Nat
335  for +a: Nat
336  for +b: Nat
337  for ih: {Nat.add(r, scale(q, m)) == Nat.add(k, Nat.add(a, b)) : Nat}
338  for fa: {Nat.add(c, Nat.add(x, y)) == Nat.add(s, Nat.double(k)) : Nat}
339  {Nat.add(Nat.add(s, Nat.double(r)), scale(q, Nat.double(m))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
340
341def adc_step(s, x, y, c, k, r, q, m, a, b, ih, fa):
342  %scale_double(q, m) : {Nat.add(Nat.add(s, Nat.double(r)), _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
343  %MNat.add_assoc_sym(s, Nat.double(r), Nat.double(scale(q, m))) : {_ == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
344  %MNat.double_add(r, scale(q, m)) : {Nat.add(s, _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
345  %Equal.sym(Nat, Nat.add(r, scale(q, m)), Nat.add(k, Nat.add(a, b)), ih) :
346    {Nat.add(s, Nat.double(_)) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
347  %MNat.double_add_sym(k, Nat.add(a, b)) : {Nat.add(s, _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
348  %MNat.double_add_sym(a, b) : {Nat.add(s, Nat.add(Nat.double(k), _)) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
349  %MNat.add_assoc(s, Nat.double(k), Nat.add(Nat.double(a), Nat.double(b))) : {_ == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
350  %fa : {Nat.add(_, Nat.add(Nat.double(a), Nat.double(b))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
351  %MNat.add_add_add_comm(x, y, Nat.double(a), Nat.double(b)) : {Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(Nat.double(a), Nat.double(b))) == Nat.add(c, _) : Nat}
352  %MNat.add_assoc(c, Nat.add(x, y), Nat.add(Nat.double(a), Nat.double(b))) : {Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(Nat.double(a), Nat.double(b))) == _ : Nat}
353  {==}
354
355# The adder is exact: the word sum plus the carry-out weight 2^n is c + a + b.
356law word_adc_nat:
357  for n: Nat
358  for a: Word(n)
359  for b: Word(n)
360  for c: Bool
361  {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)),
362    scale(carry(n, a, b, c), pow2(n))) ==
363    Nat.add(b2n(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}
364
365def word_adc_nat(n, a, b, c):
366  match n:
367    case 0n:
368      match c:
369        case False{}:
370          {==}
371        case True{}:
372          {==}
373    case 1n+ +p:
374      match a b c:
375        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
376          adc_step(0n, 0n, 0n, 0n, 0n,
377            Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
378            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
379        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
380          adc_step(1n, 0n, 0n, 1n, 0n,
381            Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
382            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
383        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
384          adc_step(1n, 0n, 1n, 0n, 0n,
385            Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
386            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
387        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
388          adc_step(0n, 0n, 1n, 1n, 1n,
389            Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
390            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
391        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
392          adc_step(1n, 1n, 0n, 0n, 0n,
393            Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
394            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
395        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
396          adc_step(0n, 1n, 0n, 1n, 1n,
397            Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
398            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
399        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
400          adc_step(0n, 1n, 1n, 0n, 1n,
401            Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
402            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
403        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
404          adc_step(1n, 1n, 1n, 1n, 1n,
405            Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
406            Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
407
408# Moves a strict upper bound across an equation without a conversion check.
409law lt_rw:
410  for -a: Nat
411  for -b: Nat
412  for -c: Nat
413  for e: {a == b : Nat}
414  for h: MNat.lt(b, c)
415  MNat.lt(a, c)
416
417def lt_rw(a, b, c, e, h):
418  %Equal.sym(Nat, a, b, e) : MNat.lt(_, c)
419  h
420
421law add_no_carry:
422  for q: Bool
423  for +r: Nat
424  for +m: Nat
425  for +s: Nat
426  for e: {Nat.add(r, scale(q, m)) == s : Nat}
427  for h: MNat.lt(s, m)
428  {r == s : Nat}
429
430def add_no_carry(q, r, m, s, e, h):
431  match q:
432    case False{}:
433      Equal.trans(Nat, r, Nat.add(r, 0n), s, MNat.add_zero_sym(r), e)
434    case True{}:
435      Empty.absurd({r == s : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, Nat.add(r, m), m,
436        MNat.le_add_left(m, r), lt_rw(Nat.add(r, m), s, m, e, h))))
437
438law add_mod_carry:
439  for q: Bool
440  for +r: Nat
441  for +m: Nat
442  for +s: Nat
443  for e: {Nat.add(r, scale(q, m)) == s : Nat}
444  for h: MNat.lt(r, m)
445  {r == Nat.mod(s, m) : Nat}
446
447def add_mod_carry(q, r, m, s, e, h):
448  match q:
449    case False{}:
450      %e : {r == Nat.mod(_, m) : Nat}
451      %MNat.add_zero_sym(r) : {r == Nat.mod(_, m) : Nat}
452      Equal.sym(Nat, Nat.mod(r, m), r, MNat.mod_eq_of_lt(r, m, h))
453    case True{}:
454      %e : {r == Nat.mod(_, m) : Nat}
455      %MNat.add_comm(m, r) : {r == Nat.mod(_, m) : Nat}
456      %MNat.add_mod_left_sym(r, m) : {r == _ : Nat}
457      Equal.sym(Nat, Nat.mod(r, m), r, MNat.mod_eq_of_lt(r, m, h))
458
459# Addition without overflow is exact.
460law word_add_nat:
461  for +n: Nat
462  for +a: Word(n)
463  for +b: Word(n)
464  for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n))
465  {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
466
467def word_add_nat(n, a, b, h):
468  add_no_carry(carry(n, a, b, False{}), Word.to_nat(n, Word.adc(n, a, b, False{}, False{})), pow2(n),
469    Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_adc_nat(n, a, b, False{}), h)
470
471# Addition wraps modulo 2^n.
472law word_add_mod:
473  for +n: Nat
474  for +a: Word(n)
475  for +b: Word(n)
476  {Word.to_nat(n, Word.add(n, a, b)) ==
477    Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) : Nat}
478
479def word_add_mod(n, a, b):
480  add_mod_carry(carry(n, a, b, False{}), Word.to_nat(n, Word.adc(n, a, b, False{}, False{})), pow2(n),
481    Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_adc_nat(n, a, b, False{}),
482    word_to_nat_lt(n, Word.adc(n, a, b, False{}, False{})))
483
484law u32_add_word:
485  for -x: Word(32n)
486  for -y: Word(32n)
487  {Word.to_nat(32n, Word.add(32n, x, y)) == U32.to_nat(U32.add(U32{x}, U32{y})) : Nat}
488
489def u32_add_word(x, y):
490  {==}
491
492law u32_add_nat:
493  for a: U32
494  for b: U32
495  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n))
496  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
497
498def u32_add_nat(a, b, h):
499  match a b:
500    case U32{+x} U32{+y}:
501      word_add_nat(32n, x, y, lt_rw(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)),
502        Nat.add(U32.to_nat(U32{x}), U32.to_nat(U32{y})), pow2(32n), {==}, h))
503
504law u32_add_mod:
505  for a: U32
506  for b: U32
507  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) : Nat}
508
509def u32_add_mod(a, b):
510  match a b:
511    case U32{+x} U32{+y}:
512      %u32_add_word(x, y) :
513        {_ == Nat.mod(Nat.add(U32.to_nat(U32{x}), U32.to_nat(U32{y})), pow2(32n)) : Nat}
514      %u32_to_nat_word(x) : {Word.to_nat(32n, Word.add(32n, x, y)) ==
515        Nat.mod(Nat.add(_, U32.to_nat(U32{y})), pow2(32n)) : Nat}
516      %u32_to_nat_word(y) : {Word.to_nat(32n, Word.add(32n, x, y)) ==
517        Nat.mod(Nat.add(Word.to_nat(32n, x), _), pow2(32n)) : Nat}
518      word_add_mod(32n, x, y)
519
520# The bitwise complement of w has value 2^n - 1 - w.
521law word_not_nat:
522  for n: Nat
523  for w: Word(n)
524  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == pow2(n) : Nat}
525
526def word_not_nat(n, w):
527  match n:
528    case 0n:
529      {==}
530    case 1n+ +p:
531      match w:
532        case WCon{False{}, +t}:
533          %word_not_nat(p, t) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == Nat.double(_) : Nat}
534          %MNat.double_add_sym(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == 2n+_ : Nat}
535          {==}
536        case WCon{True{}, +t}:
537          %MNat.add_succ_sym(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) : {1n+_ == pow2(1n+p) : Nat}
538          %word_not_nat(p, t) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == Nat.double(_) : Nat}
539          %MNat.double_add_sym(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == 2n+_ : Nat}
540          {==}
541
542# Subtraction is addition of the complement with a carry in.
543law word_sub_not:
544  for n: Nat
545  for a: Word(n)
546  for b: Word(n)
547  for +c: Bool
548  {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}
549
550def word_sub_not(n, a, b, c):
551  match n:
552    case 0n:
553      {==}
554    case 1n+ +p:
555      match a b:
556        case WCon{False{}, +at} WCon{+y, +bt}:
557          Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.xor(Bool.not(y), c), w},
558            Word.adc(p, at, bt, True{}, Bool.and(Bool.not(y), c)),
559            Word.adc(p, at, Word.not(p, bt), False{}, Bool.and(Bool.not(y), c)),
560            word_sub_not(p, at, bt, Bool.and(Bool.not(y), c)))
561        case WCon{True{}, +at} WCon{+y, +bt}:
562          Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.not(Bool.xor(Bool.not(y), c)), w},
563            Word.adc(p, at, bt, True{}, Bool.or(Bool.not(y), c)),
564            Word.adc(p, at, Word.not(p, bt), False{}, Bool.or(Bool.not(y), c)),
565            word_sub_not(p, at, bt, Bool.or(Bool.not(y), c)))
566
567law sub_arith:
568  for +a: Nat
569  for +b: Nat
570  for +nb: Nat
571  for +m: Nat
572  for h: MNat.le(b, a)
573  for hn: {1n+Nat.add(nb, b) == m : Nat}
574  {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}
575
576def sub_arith(a, b, nb, m, h, hn):
577  %hn : {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), _) : Nat}
578  %MNat.add_succ_sym(Nat.sub(a, b), Nat.add(nb, b)) : {1n+Nat.add(a, nb) == _ : Nat}
579  %MNat.sub_add_cancel(a, b, h) : {1n+Nat.add(_, nb) == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat}
580  %MNat.add_assoc_sym(Nat.sub(a, b), b, nb) : {1n+_ == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat}
581  %MNat.add_comm(nb, b) : {1n+Nat.add(Nat.sub(a, b), _) == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat}
582  {==}
583
584law sub_fin:
585  for q: Bool
586  for +r: Nat
587  for +d: Nat
588  for +m: Nat
589  for e: {Nat.add(r, scale(q, m)) == Nat.add(d, m) : Nat}
590  for h: MNat.lt(r, m)
591  {r == d : Nat}
592
593def sub_fin(q, r, d, m, e, h):
594  match q:
595    case False{}:
596      Empty.absurd({r == d : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, Nat.add(d, m), m,
597        MNat.le_add_left(m, d), lt_rw(Nat.add(d, m), r, m,
598          Equal.sym(Nat, r, Nat.add(d, m),
599            Equal.trans(Nat, r, Nat.add(r, 0n), Nat.add(d, m), MNat.add_zero_sym(r), e)), h))))
600    case True{}:
601      MNat.add_right_cancel(r, m, d, e)
602
603# Subtraction without wrap is exact.
604law word_sub_nat:
605  for +n: Nat
606  for +a: Word(n)
607  for +b: Word(n)
608  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
609  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
610
611def word_sub_nat(n, a, b, h):
612  %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}),
613    Word.adc(n, a, Word.not(n, b), False{}, True{}), word_sub_not(n, a, b, True{})) :
614    {Word.to_nat(n, _) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
615  sub_fin(carry(n, a, Word.not(n, b), True{}),
616    Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})),
617    Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n),
618    Equal.trans(Nat,
619      Nat.add(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})),
620        scale(carry(n, a, Word.not(n, b), True{}), pow2(n))),
621      1n+Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))),
622      Nat.add(Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)),
623      word_adc_nat(n, a, Word.not(n, b), True{}),
624      sub_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), pow2(n), h,
625        word_not_nat(n, b))),
626    word_to_nat_lt(n, Word.adc(n, a, Word.not(n, b), False{}, True{})))
627
628law u32_sub_nat:
629  for a: U32
630  for b: U32
631  for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
632  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
633
634def u32_sub_nat(a, b, h):
635  match a b:
636    case U32{x} U32{y}:
637      word_sub_nat(32n, x, y, h)
638
639law lt_of_double_lt:
640  for a: Nat
641  for b: Nat
642  for h: MNat.lt(Nat.double(a), Nat.double(b))
643  MNat.lt(a, b)
644
645def lt_of_double_lt(a, b, h):
646  match a b:
647    case 0n 0n:
648      Empty.absurd(MNat.lt(0n, 0n), MNat.lt_zero(0n)(h))
649    case 1n+p 0n:
650      Empty.absurd(MNat.lt(1n+p, 0n), MNat.lt_zero(2n+Nat.double(p))(h))
651    case 0n 1n+q:
652      {==}
653    case 1n+p 1n+q:
654      lt_of_double_lt(p, q, h)
655
656# Incrementing without overflow adds one.
657law word_inc_nat:
658  for n: Nat
659  for w: Word(n)
660  for h: MNat.lt(1n+Word.to_nat(n, w), pow2(n))
661  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
662
663def word_inc_nat(n, w, h):
664  match n:
665    case 0n:
666      Empty.absurd({0n == 1n : Nat}, MNat.lt_irrefl(1n)(h))
667    case 1n+ +p:
668      match w:
669        case WCon{False{}, t}:
670          {==}
671        case WCon{True{}, +t}:
672          Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.inc(p, t)),
673            1n+Word.to_nat(p, t),
674            word_inc_nat(p, t, lt_of_double_lt(1n+Word.to_nat(p, t), pow2(p), h)))
675
676law u32_inc_nat:
677  for a: U32
678  for h: MNat.lt(1n+U32.to_nat(a), pow2(32n))
679  {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
680
681def u32_inc_nat(a, h):
682  match a:
683    case U32{+x}:
684      word_inc_nat(32n, x, lt_rw(1n+Word.to_nat(32n, x), 1n+U32.to_nat(U32{x}), pow2(32n), {==}, h))
685
686law u32_to_from_nat:
687  for k: Nat
688  for +h: MNat.lt(k, pow2(32n))
689  {U32.to_nat(U32.from_nat(k)) == k : Nat}
690
691def u32_to_from_nat(k, h):
692  match k:
693    case 0n:
694      {==}
695    case 1n+ +j:
696      +ih = u32_to_from_nat(j, MNat.lt_trans(j, 1n+j, pow2(32n), MNat.lt_succ_self(j), h))
697      Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(j))), 1n+U32.to_nat(U32.from_nat(j)), 1n+j,
698        u32_inc_nat(U32.from_nat(j), lt_rw(1n+U32.to_nat(U32.from_nat(j)), 1n+j, pow2(32n),
699          Equal.cong(Nat, Nat, v => 1n+v, U32.to_nat(U32.from_nat(j)), j, ih), h)),
700        Equal.cong(Nat, Nat, v => 1n+v, U32.to_nat(U32.from_nat(j)), j, ih))
701
702law u32_from_to_nat:
703  for +a: U32
704  {U32.from_nat(U32.to_nat(a)) == a : U32}
705
706def u32_from_to_nat(a):
707  u32_to_nat_inj(U32.from_nat(U32.to_nat(a)), a, u32_to_from_nat(U32.to_nat(a), u32_to_nat_lt(a)))
708
709law and_le_sub:
710  for c: Bool
711  for +a: Nat
712  for +b: Nat
713  for +l: Nat
714  for -s: Nat
715  for +hc: {Nat.is_le(a, l) == c : Bool}
716  for hs: MNat.le(a, l) -> {s == Nat.sub(l, a) : Nat}
717  {Bool.and(c, Nat.is_le(b, s)) == Nat.is_le(Nat.add(a, b), l) : Bool}
718
719def and_le_sub(c, a, b, l, s, hc, hs):
720  match c:
721    case True{}:
722      %Equal.sym(Nat, s, Nat.sub(l, a), hs(hc)) :
723        {Bool.and(True{}, Nat.is_le(b, _)) == Nat.is_le(Nat.add(a, b), l) : Bool}
724      %hc : {Bool.and(_, Nat.is_le(b, Nat.sub(l, a))) == Nat.is_le(Nat.add(a, b), l) : Bool}
725      MNat.le_and_le_sub_iff_add_le(a, b, l)
726    case False{}:
727      %MNat.le_and_le_sub_iff_add_le(a, b, l) : {Bool.and(False{}, Nat.is_le(b, s)) == _ : Bool}
728      %Equal.sym(Bool, Nat.is_le(a, l), False{}, hc) :
729        {Bool.and(False{}, Nat.is_le(b, s)) == Bool.and(_, Nat.is_le(b, Nat.sub(l, a))) : Bool}
730      {==}
731
732# The overflow-safe bounds check n <= len and i <= len - n holds exactly when i + n <= len.
733law u32_fits_nat:
734  for +len: U32
735  for +i: U32
736  for +n: U32
737  {Bool.and(U32.is_le(n, len), U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}
738
739def u32_fits_nat(len, i, n):
740  %Equal.sym(Bool, U32.is_le(n, len), Nat.is_le(U32.to_nat(n), U32.to_nat(len)), u32_is_le_nat(n, len)) :
741    {Bool.and(_, U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}
742  %Equal.sym(Bool, U32.is_le(i, U32.sub(len, n)), Nat.is_le(U32.to_nat(i), U32.to_nat(U32.sub(len, n))), u32_is_le_nat(i, U32.sub(len, n))) :
743    {Bool.and(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), _) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}
744  %MNat.add_comm(U32.to_nat(n), U32.to_nat(i)) :
745    {Bool.and(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), Nat.is_le(U32.to_nat(i), U32.to_nat(U32.sub(len, n)))) == Nat.is_le(_, U32.to_nat(len)) : Bool}
746  and_le_sub(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), U32.to_nat(n), U32.to_nat(i), U32.to_nat(len), U32.to_nat(U32.sub(len, n)), {==}, h => u32_sub_nat(len, n, h))