u32.bend

bend-mathlib@0.8.1.0 · 1,268 lines · 118 definitions

1# bend-mathlib/u32.bend: machine words as naturals; Word(n) and U32 operations agree with Nat arithmetic
2# (compare, add, sub, inc, not, min, max, div, from_nat).
3import Base
4import bend-mathlib@0.8.1.0/nat.bend as MNat
5
6def internal_succ_double_lt(a: Nat, b: Nat, h: MNat.lt(a, b)) -> MNat.lt(1n+Nat.double(a), Nat.double(b)):
7  match a b:
8    case 0n 0n:
9      Empty.absurd(MNat.lt(1n, 0n), MNat.internal_false_ne_true(h))
10    case 0n 1n+q:
11      {==}
12    case 1n+p 0n:
13      Empty.absurd(MNat.lt(3n+Nat.double(p), 0n), MNat.internal_false_ne_true(h))
14    case 1n+p 1n+q:
15      internal_succ_double_lt(p, q, h)
16
17# A word's value is below two to the width: to_nat w < 2^n.
18law word_to_nat_lt:
19  for n: Nat
20  for w: Word(n)
21  MNat.lt(Word.to_nat(n, w), Nat.pow(2n, n))
22
23def word_to_nat_lt(n, w):
24  match n:
25    case 0n:
26      {==}
27    case 1n++p:
28      match w:
29        case WCon{False{}, t}:
30          +t = t
31          %MNat.two_pow_succ_sym(p) : MNat.lt(Nat.double(Word.to_nat(p, t)), _)
32          MNat.double_lt_double(Word.to_nat(p, t), Nat.pow(2n, p), word_to_nat_lt(p, t))
33        case WCon{True{}, t}:
34          +t = t
35          %MNat.two_pow_succ_sym(p) : MNat.lt(1n+Nat.double(Word.to_nat(p, t)), _)
36          internal_succ_double_lt(Word.to_nat(p, t), Nat.pow(2n, p), word_to_nat_lt(p, t))
37
38# The zero word is the natural zero: to_nat (zero n) = 0.
39law word_to_nat_zero:
40  for n: Nat
41  {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
42
43def word_to_nat_zero(n):
44  match n:
45    case 0n:
46      {==}
47    case 1n++p:
48      Equal.cong(Nat, Nat, x => Nat.double(x), Word.to_nat(p, Word.zero(p)), 0n, word_to_nat_zero(p))
49
50# Distinct words have distinct values: to_nat a = to_nat b implies a = b.
51law word_to_nat_inj:
52  for n: Nat
53  for a: Word(n)
54  for b: Word(n)
55  for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
56  {a == b : Word(n)}
57
58def word_to_nat_inj(n, a, b, e):
59  match n:
60    case 0n:
61      match a b:
62        case WNil{} WNil{}:
63          {==}
64    case 1n++p:
65      match a b:
66        case WCon{False{}, +at} WCon{False{}, +bt}:
67          Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, at, bt, word_to_nat_inj(p, at, bt, MNat.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), e)))
68        case WCon{True{}, +at} WCon{True{}, +bt}:
69          Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, at, bt, word_to_nat_inj(p, at, bt, MNat.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), MNat.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), e))))
70        case WCon{False{}, +at} WCon{True{}, +bt}:
71          Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)}, MNat.double_ne_succ_double(Word.to_nat(p, at), Word.to_nat(p, bt))(e))
72        case WCon{True{}, +at} WCon{False{}, +bt}:
73          Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)}, MNat.double_ne_succ_double(Word.to_nat(p, bt), Word.to_nat(p, at))(Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), e)))
74
75def internal_bv(b: Bool) -> Nat:
76  Bool.pick(Nat, b, 1n, 0n)
77
78def internal_to_nat_con(-p: Nat, b: Bool, -t: Word(p)) -> {Nat.add(internal_bv(b), Nat.double(Word.to_nat(p, t))) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
79  match b:
80    case False{}:
81      {==}
82    case True{}:
83      {==}
84
85def internal_cmp_bits(x: Nat, y: Nat, ab: Bool, bb: Bool) -> {Word.cmp.fin(ab, bb, Nat.cmp(x, y)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(x)), Nat.add(internal_bv(bb), Nat.double(y))) : Cmp}:
86  match x y:
87    case 0n 0n:
88      match ab bb:
89        case False{} False{}:
90          {==}
91        case False{} True{}:
92          {==}
93        case True{} False{}:
94          {==}
95        case True{} True{}:
96          {==}
97    case 0n 1n+q:
98      match ab bb:
99        case False{} False{}:
100          {==}
101        case False{} True{}:
102          {==}
103        case True{} False{}:
104          {==}
105        case True{} True{}:
106          {==}
107    case 1n+p 0n:
108      match ab bb:
109        case False{} False{}:
110          {==}
111        case False{} True{}:
112          {==}
113        case True{} False{}:
114          {==}
115        case True{} True{}:
116          {==}
117    case 1n+p 1n+q:
118      match ab bb:
119        case False{} False{}:
120          internal_cmp_bits(p, q, False{}, False{})
121        case False{} True{}:
122          internal_cmp_bits(p, q, False{}, True{})
123        case True{} False{}:
124          internal_cmp_bits(p, q, True{}, False{})
125        case True{} True{}:
126          internal_cmp_bits(p, q, True{}, True{})
127
128# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b).
129law word_cmp_to_nat:
130  for n: Nat
131  for a: Word(n)
132  for b: Word(n)
133  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
134
135def word_cmp_to_nat(n, a, b):
136  match n:
137    case 0n:
138      {==}
139    case 1n++p:
140      match a b:
141        case WCon{+ab, +at} WCon{+bb, +bt}:
142          %internal_to_nat_con(p, ab, at) : {Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) == Nat.cmp(_, Word.to_nat(1n+p, WCon{bb, bt})) : Cmp}
143          %internal_to_nat_con(p, bb, bt) : {Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(Word.to_nat(p, at))), _) : Cmp}
144          %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), word_cmp_to_nat(p, at, bt)) : {Word.cmp.fin(ab, bb, _) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(Word.to_nat(p, at))), Nat.add(internal_bv(bb), Nat.double(Word.to_nat(p, bt)))) : Cmp}
145          internal_cmp_bits(Word.to_nat(p, at), Word.to_nat(p, bt), ab, bb)
146
147# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n.
148law word_not_add:
149  for n: Nat
150  for w: Word(n)
151  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}
152
153def word_not_add(n, w):
154  match n:
155    case 0n:
156      {==}
157    case 1n++p:
158      match w:
159        case WCon{False{}, +t}:
160          -u = Word.to_nat(p, Word.not(p, t))
161          -x = Word.to_nat(p, t)
162          %MNat.two_pow_succ_sym(p) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == _ : Nat}
163          %word_not_add(p, t) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == Nat.double(_) : Nat}
164          %MNat.double_add(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+_ == 2n+Nat.double(Nat.add(u, x)) : Nat}
165          {==}
166        case WCon{True{}, +t}:
167          -u = Word.to_nat(p, Word.not(p, t))
168          -x = Word.to_nat(p, t)
169          %MNat.add_succ_sym(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) : {1n+_ == Nat.pow(2n, 1n+p) : Nat}
170          %MNat.two_pow_succ_sym(p) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == _ : Nat}
171          %word_not_add(p, t) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == Nat.double(_) : Nat}
172          %MNat.double_add(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+_ == 2n+Nat.double(Nat.add(u, x)) : Nat}
173          {==}
174
175def internal_pick_pow(o: Bool, p: Nat) -> {Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)) == Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n) : Nat}:
176  match o:
177    case False{}:
178      {==}
179    case True{}:
180      MNat.two_pow_succ_sym(p)
181
182def internal_carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
183  match n:
184    case 0n:
185      c
186    case 1n+p:
187      match a b:
188        case WCon{False{}, at} WCon{+bb, bt}:
189          internal_carry(p, at, bt, Bool.and(bb, c))
190        case WCon{True{}, at} WCon{+bb, bt}:
191          internal_carry(p, at, bt, Bool.or(bb, c))
192
193def internal_full_add(a: Bool, b: Bool, c: Bool) -> {Nat.add(Nat.add(internal_bv(a), internal_bv(b)), internal_bv(c)) == Nat.add(internal_bv(Pair.fst(Bool, Bool, Bool.full_add(a, b, c))), Nat.double(internal_bv(Pair.snd(Bool, Bool, Bool.full_add(a, b, c))))) : Nat}:
194  match a b c:
195    case False{} False{} False{}:
196      {==}
197    case False{} False{} True{}:
198      {==}
199    case False{} True{} False{}:
200      {==}
201    case False{} True{} True{}:
202      {==}
203    case True{} False{} False{}:
204      {==}
205    case True{} False{} True{}:
206      {==}
207    case True{} True{} False{}:
208      {==}
209    case True{} True{} True{}:
210      {==}
211
212def internal_adc_nat(+s: Nat, +k: Nat, +a: Nat, +b: Nat, +c: Nat, +e: Nat, +q: Nat, +x: Nat, +y: Nat,
213  ih: {Nat.add(e, q) == Nat.add(Nat.add(x, y), k) : Nat},
214  fa: {Nat.add(Nat.add(a, b), c) == Nat.add(s, Nat.double(k)) : Nat})
215  -> {Nat.add(Nat.add(s, Nat.double(e)), Nat.double(q)) == Nat.add(Nat.add(Nat.add(a, Nat.double(x)), Nat.add(b, Nat.double(y))), c) : Nat}:
216  -d = Nat.double(Nat.add(x, y))
217  -r = Nat.add(Nat.add(Nat.add(a, Nat.double(x)), Nat.add(b, Nat.double(y))), c)
218  %MNat.add_assoc_sym(s, Nat.double(e), Nat.double(q)) : {_ == r : Nat}
219  %MNat.double_add(e, q) : {Nat.add(s, _) == r : Nat}
220  %Equal.sym(Nat, Nat.add(e, q), Nat.add(Nat.add(x, y), k), ih) : {Nat.add(s, Nat.double(_)) == r : Nat}
221  %MNat.double_add_sym(Nat.add(x, y), k) : {Nat.add(s, _) == r : Nat}
222  -l = Nat.add(s, Nat.add(d, Nat.double(k)))
223  %MNat.add_add_add_comm(a, b, Nat.double(x), Nat.double(y)) : {l == Nat.add(_, c) : Nat}
224  %MNat.double_add(x, y) : {l == Nat.add(Nat.add(Nat.add(a, b), _), c) : Nat}
225  %MNat.add_right_comm_sym(Nat.add(a, b), Nat.double(Nat.add(x, y)), c) : {l == _ : Nat}
226  %Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(s, Nat.double(k)), fa) : {l == Nat.add(_, d) : Nat}
227  %MNat.add_assoc_sym(s, Nat.double(k), Nat.double(Nat.add(x, y))) : {l == _ : Nat}
228  %MNat.add_comm(Nat.double(Nat.add(x, y)), Nat.double(k)) : {l == Nat.add(s, _) : Nat}
229  {==}
230
231def internal_adc_core(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Bool.pick(Nat, internal_carry(n, a, b, c), Nat.pow(2n, n), 0n)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), internal_bv(c)) : Nat}:
232  match n:
233    case 0n:
234      match c:
235        case False{}:
236          {==}
237        case True{}:
238          {==}
239    case 1n++p:
240      match a b:
241        case WCon{False{}, +at} WCon{+bb, +bt}:
242          +c = c
243          -e = Word.adc(p, at, bt, False{}, Bool.and(bb, c))
244          -o = internal_carry(p, at, bt, Bool.and(bb, c))
245          -r = Nat.add(Nat.add(Word.to_nat(1n+p, WCon{False{}, at}), Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c))
246          %internal_to_nat_con(p, Bool.xor(bb, c), Word.adc(p, at, bt, False{}, Bool.and(bb, c))) : {Nat.add(_, Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n)) == r : Nat}
247          %internal_pick_pow(internal_carry(p, at, bt, Bool.and(bb, c)), p) : {Nat.add(Nat.add(internal_bv(Bool.xor(bb, c)), Nat.double(Word.to_nat(p, e))), _) == r : Nat}
248          -l = Nat.add(Nat.add(internal_bv(Bool.xor(bb, c)), Nat.double(Word.to_nat(p, e))), Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)))
249          %internal_to_nat_con(p, False{}, at) : {l == Nat.add(Nat.add(_, Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c)) : Nat}
250          %internal_to_nat_con(p, bb, bt) : {l == Nat.add(Nat.add(Nat.add(internal_bv(False{}), Nat.double(Word.to_nat(p, at))), _), internal_bv(c)) : Nat}
251          internal_adc_nat(internal_bv(Bool.xor(bb, c)), internal_bv(Bool.and(bb, c)), internal_bv(False{}), internal_bv(bb), internal_bv(c), Word.to_nat(p, Word.adc(p, at, bt, False{}, Bool.and(bb, c))), Bool.pick(Nat, internal_carry(p, at, bt, Bool.and(bb, c)), Nat.pow(2n, p), 0n), Word.to_nat(p, at), Word.to_nat(p, bt), internal_adc_core(p, at, bt, Bool.and(bb, c)), internal_full_add(False{}, bb, c))
252        case WCon{True{}, +at} WCon{+bb, +bt}:
253          +c = c
254          -e = Word.adc(p, at, bt, False{}, Bool.or(bb, c))
255          -o = internal_carry(p, at, bt, Bool.or(bb, c))
256          -r = Nat.add(Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c))
257          %internal_to_nat_con(p, Bool.not(Bool.xor(bb, c)), Word.adc(p, at, bt, False{}, Bool.or(bb, c))) : {Nat.add(_, Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n)) == r : Nat}
258          %internal_pick_pow(internal_carry(p, at, bt, Bool.or(bb, c)), p) : {Nat.add(Nat.add(internal_bv(Bool.not(Bool.xor(bb, c))), Nat.double(Word.to_nat(p, e))), _) == r : Nat}
259          -l = Nat.add(Nat.add(internal_bv(Bool.not(Bool.xor(bb, c))), Nat.double(Word.to_nat(p, e))), Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)))
260          %internal_to_nat_con(p, True{}, at) : {l == Nat.add(Nat.add(_, Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c)) : Nat}
261          %internal_to_nat_con(p, bb, bt) : {l == Nat.add(Nat.add(Nat.add(internal_bv(True{}), Nat.double(Word.to_nat(p, at))), _), internal_bv(c)) : Nat}
262          internal_adc_nat(internal_bv(Bool.not(Bool.xor(bb, c))), internal_bv(Bool.or(bb, c)), internal_bv(True{}), internal_bv(bb), internal_bv(c), Word.to_nat(p, Word.adc(p, at, bt, False{}, Bool.or(bb, c))), Bool.pick(Nat, internal_carry(p, at, bt, Bool.or(bb, c)), Nat.pow(2n, p), 0n), Word.to_nat(p, at), Word.to_nat(p, bt), internal_adc_core(p, at, bt, Bool.or(bb, c)), internal_full_add(True{}, bb, c))
263
264def internal_lt_congl(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: MNat.lt(x, m)) -> MNat.lt(y, m):
265  %e : MNat.lt(_, m)
266  h
267
268def internal_le_congr(-m: Nat, -x: Nat, -y: Nat, e: {y == x : Nat}, h: MNat.le(m, y)) -> MNat.le(m, x):
269  %e : MNat.le(m, _)
270  h
271
272def internal_fin_exact(+e: Nat, +s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(s, m)) -> {e == s : Nat}:
273  match o:
274    case False{}:
275      Equal.trans(Nat, e, Nat.add(e, 0n), s, MNat.add_zero_sym(e), eq)
276    case True{}:
277      +le = MNat.le_of_add_eq(m, e, s, Equal.trans(Nat, Nat.add(m, e), Nat.add(e, m), s, MNat.add_comm(m, e), eq))
278      Empty.absurd({e == s : Nat}, MNat.lt_irrefl(s)(MNat.lt_of_lt_of_le(s, m, s, h, le)))
279
280def internal_fin_wrap(+e: Nat, -s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m)) -> {e == Nat.mod(s, m) : Nat}:
281  match o:
282    case False{}:
283      %eq : {e == Nat.mod(_, m) : Nat}
284      %MNat.add_zero_sym(e) : {e == Nat.mod(_, m) : Nat}
285      Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
286    case True{}:
287      %eq : {e == Nat.mod(_, m) : Nat}
288      %MNat.add_comm(m, e) : {e == Nat.mod(_, m) : Nat}
289      %MNat.add_mod_left_sym(e, m) : {e == _ : Nat}
290      Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
291
292def internal_fin_over(+e: Nat, +s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m), le: MNat.le(m, s)) -> {Nat.add(e, m) == s : Nat}:
293  match o:
294    case False{}:
295      +es = Equal.trans(Nat, e, Nat.add(e, 0n), s, MNat.add_zero_sym(e), eq)
296      Empty.absurd({Nat.add(e, m) == s : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, s, m, le, internal_lt_congl(e, s, m, es, h))))
297    case True{}:
298      eq
299
300# The adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in.
301law word_adc_exact:
302  for n: Nat
303  for a: Word(n)
304  for b: Word(n)
305  for c: Bool
306  for h: MNat.lt(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n))
307  {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) : Nat}
308
309def word_adc_exact(n, a, b, c, h):
310  +n = n
311  +a = a
312  +b = b
313  +c = c
314  internal_fin_exact(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), h)
315
316# The adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in.
317law word_adc_overflow:
318  for n: Nat
319  for a: Word(n)
320  for b: Word(n)
321  for c: Bool
322  for h: MNat.le(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)))
323  {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) : Nat}
324
325def word_adc_overflow(n, a, b, c, h):
326  +n = n
327  +a = a
328  +b = b
329  +c = c
330  internal_fin_over(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), word_to_nat_lt(n, Word.adc(n, a, b, False{}, c)), h)
331
332# The adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n.
333law word_adc_wrap:
334  for n: Nat
335  for a: Word(n)
336  for b: Word(n)
337  for c: Bool
338  {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)) : Nat}
339
340def word_adc_wrap(n, a, b, c):
341  +n = n
342  +a = a
343  +b = b
344  +c = c
345  internal_fin_wrap(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), word_to_nat_lt(n, Word.adc(n, a, b, False{}, c)))
346
347# Word addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b.
348law word_add_exact:
349  for n: Nat
350  for a: Word(n)
351  for b: Word(n)
352  for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
353  {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
354
355def word_add_exact(n, a, b, h):
356  +n = n
357  +a = a
358  +b = b
359  %MNat.add_zero(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : {Word.to_nat(n, Word.add(n, a, b)) == _ : Nat}
360  word_adc_exact(n, a, b, False{}, internal_lt_congl(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), 0n), Nat.pow(2n, n), MNat.add_zero_sym(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), h))
361
362# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n.
363law word_add_wrap:
364  for n: Nat
365  for a: Word(n)
366  for b: Word(n)
367  {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}
368
369def word_add_wrap(n, a, b):
370  +n = n
371  +a = a
372  +b = b
373  %MNat.add_zero(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(_, Nat.pow(2n, n)) : Nat}
374  word_adc_wrap(n, a, b, False{})
375
376def internal_inc_carry(n: Nat, w: Word(n)) -> Bool:
377  match n:
378    case 0n:
379      True{}
380    case 1n+p:
381      match w:
382        case WCon{False{}, t}:
383          False{}
384        case WCon{True{}, t}:
385          internal_inc_carry(p, t)
386
387def internal_inc_core(n: Nat, w: Word(n)) -> {Nat.add(Word.to_nat(n, Word.inc(n, w)), Bool.pick(Nat, internal_inc_carry(n, w), Nat.pow(2n, n), 0n)) == 1n+Word.to_nat(n, w) : Nat}:
388  match n:
389    case 0n:
390      {==}
391    case 1n++p:
392      match w:
393        case WCon{False{}, t}:
394          MNat.add_zero(1n+Nat.double(Word.to_nat(p, t)))
395        case WCon{True{}, +t}:
396          -x = Word.to_nat(p, t)
397          %internal_pick_pow(internal_inc_carry(p, t), p) : {Nat.add(Nat.double(Word.to_nat(p, Word.inc(p, t))), _) == 2n+Nat.double(x) : Nat}
398          %MNat.double_add(Word.to_nat(p, Word.inc(p, t)), Bool.pick(Nat, internal_inc_carry(p, t), Nat.pow(2n, p), 0n)) : {_ == 2n+Nat.double(x) : Nat}
399          Equal.cong(Nat, Nat, z => Nat.double(z), Nat.add(Word.to_nat(p, Word.inc(p, t)), Bool.pick(Nat, internal_inc_carry(p, t), Nat.pow(2n, p), 0n)), 1n+Word.to_nat(p, t), internal_inc_core(p, t))
400
401# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w.
402law word_inc_exact:
403  for n: Nat
404  for w: Word(n)
405  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
406  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
407
408def word_inc_exact(n, w, h):
409  +n = n
410  +w = w
411  internal_fin_exact(Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), Nat.pow(2n, n), internal_inc_carry(n, w), internal_inc_core(n, w), h)
412
413# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n.
414law word_inc_wrap:
415  for n: Nat
416  for w: Word(n)
417  {Word.to_nat(n, Word.inc(n, w)) == Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) : Nat}
418
419def word_inc_wrap(n, w):
420  +n = n
421  +w = w
422  internal_fin_wrap(Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), Nat.pow(2n, n), internal_inc_carry(n, w), internal_inc_core(n, w), word_to_nat_lt(n, Word.inc(n, w)))
423
424def internal_adc_not(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}:
425  match n:
426    case 0n:
427      {==}
428    case 1n++p:
429      match a b:
430        case WCon{False{}, +at} WCon{+bb, +bt}:
431          +c = c
432          Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.xor(Bool.not(bb), c), w}, Word.adc(p, at, bt, True{}, Bool.and(Bool.not(bb), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.and(Bool.not(bb), c)), internal_adc_not(p, at, bt, Bool.and(Bool.not(bb), c)))
433        case WCon{True{}, +at} WCon{+bb, +bt}:
434          +c = c
435          Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.not(Bool.xor(Bool.not(bb), c)), w}, Word.adc(p, at, bt, True{}, Bool.or(Bool.not(bb), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.or(Bool.not(bb), c)), internal_adc_not(p, at, bt, Bool.or(Bool.not(bb), c)))
436
437def internal_sub_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, h: MNat.le(y, x), c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(Nat.sub(x, y), m) : Nat}:
438  -d = Nat.sub(x, y)
439  %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(d, _) : Nat}
440  %MNat.add_sub_of_le(y, x, h) : {Nat.add(Nat.add(_, u), 1n) == Nat.add(d, 1n+Nat.add(u, y)) : Nat}
441  -l = Nat.add(Nat.add(Nat.add(y, d), u), 1n)
442  %MNat.add_succ_sym(Nat.sub(x, y), Nat.add(u, y)) : {l == _ : Nat}
443  %MNat.add_comm(1n, Nat.add(Nat.add(y, Nat.sub(x, y)), u)) : {_ == 1n+Nat.add(d, Nat.add(u, y)) : Nat}
444  -l2 = Nat.add(1n, Nat.add(Nat.add(y, d), u))
445  %MNat.add_comm(y, u) : {l2 == 1n+Nat.add(d, _) : Nat}
446  %MNat.add_left_comm(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
447  %MNat.add_assoc(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
448  {==}
449
450# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b.
451law word_sub_exact:
452  for n: Nat
453  for a: Word(n)
454  for b: Word(n)
455  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
456  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
457
458def word_sub_exact(n, a, b, h):
459  +n = n
460  +a = a
461  +b = b
462  -x = Word.to_nat(n, a)
463  -y = Word.to_nat(n, b)
464  -nb = Word.not(n, b)
465  -e = Word.to_nat(n, Word.adc(n, a, nb, False{}, True{}))
466  -s = Nat.add(Nat.add(x, Word.to_nat(n, nb)), 1n)
467  -m = Nat.pow(2n, n)
468  %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), internal_adc_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.sub(x, y) : Nat}
469  +ar = internal_sub_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), Nat.pow(2n, n), h, word_not_add(n, b))
470  +le = internal_le_congr(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), 1n), Nat.add(Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)), Equal.sym(Nat, s, Nat.add(Nat.sub(x, y), m), ar), MNat.le_add_left(Nat.pow(2n, n), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b))))
471  +ov = internal_fin_over(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), 1n), Nat.pow(2n, n), internal_carry(n, a, Word.not(n, b), True{}), internal_adc_core(n, a, Word.not(n, b), True{}), word_to_nat_lt(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), le)
472  MNat.add_right_cancel(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.pow(2n, n), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), Equal.trans(Nat, Nat.add(e, m), s, Nat.add(Nat.sub(x, y), m), ov, ar))
473
474def internal_sub_wrap_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(m, y)) : Nat}:
475  %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(_, y)) : Nat}
476  %MNat.add_sub_cancel_sym(1n+u, y) : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, _) : Nat}
477  %MNat.add_succ_sym(x, u) : {Nat.add(Nat.add(x, u), 1n) == _ : Nat}
478  MNat.add_comm(Nat.add(x, u), 1n)
479
480# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n.
481law word_sub_wrap:
482  for n: Nat
483  for a: Word(n)
484  for b: Word(n)
485  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)) : Nat}
486
487def word_sub_wrap(n, a, b):
488  +n = n
489  +a = a
490  +b = b
491  -x = Word.to_nat(n, a)
492  -y = Word.to_nat(n, b)
493  -u = Word.to_nat(n, Word.not(n, b))
494  -m = Nat.pow(2n, n)
495  %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), internal_adc_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.mod(Nat.add(x, Nat.sub(m, y)), m) : Nat}
496  %internal_sub_wrap_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), Nat.pow(2n, n), word_not_add(n, b)) : {Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})) == Nat.mod(_, m) : Nat}
497  word_adc_wrap(n, a, Word.not(n, b), True{})
498
499def internal_bound(-s: Nat, -m: Nat, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(s, m)) -> MNat.lt(s, Nat.pow(2n, 32n)):
500  %Equal.sym(Nat, Nat.pow(2n, 32n), m, e) : MNat.lt(s, _)
501  h
502
503def internal_u32_to_nat_lt(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> MNat.lt(U32.to_nat(a), m):
504  match a:
505    case U32{w}:
506      %e : MNat.lt(Word.to_nat(32n, w), _)
507      word_to_nat_lt(32n, w)
508
509# A U32's value is below 2^32.
510law u32_to_nat_lt:
511  for a: U32
512  MNat.lt(U32.to_nat(a), Nat.pow(2n, 32n))
513
514def u32_to_nat_lt(a):
515  internal_u32_to_nat_lt(Nat.pow(2n, 32n), a, {==})
516
517# Distinct U32s have distinct values: to_nat a = to_nat b implies a = b.
518law u32_to_nat_inj:
519  for a: U32
520  for b: U32
521  for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
522  {a == b : U32}
523
524def u32_to_nat_inj(a, b, e):
525  match a b:
526    case U32{+x} U32{+y}:
527      Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_to_nat_inj(32n, x, y, e))
528
529# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b).
530law u32_cmp_to_nat:
531  for a: U32
532  for b: U32
533  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
534
535def u32_cmp_to_nat(a, b):
536  match a b:
537    case U32{x} U32{y}:
538      word_cmp_to_nat(32n, x, y)
539
540# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b).
541law u32_is_eq_to_nat:
542  for a: U32
543  for b: U32
544  {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
545
546def u32_is_eq_to_nat(a, b):
547  +a = a
548  +b = b
549  Equal.cong(Cmp, Bool, k => Cmp.is_eq(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
550
551# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b).
552law u32_is_ne_to_nat:
553  for a: U32
554  for b: U32
555  {U32.is_ne(a, b) == Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) : Bool}
556
557def u32_is_ne_to_nat(a, b):
558  +a = a
559  +b = b
560  Equal.cong(Cmp, Bool, k => Bool.not(Cmp.is_eq(k)), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
561
562# The U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b).
563law u32_is_lt_to_nat:
564  for a: U32
565  for b: U32
566  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
567
568def u32_is_lt_to_nat(a, b):
569  +a = a
570  +b = b
571  Equal.cong(Cmp, Bool, k => Cmp.is_lt(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
572
573# The U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b).
574law u32_is_le_to_nat:
575  for a: U32
576  for b: U32
577  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
578
579def u32_is_le_to_nat(a, b):
580  +a = a
581  +b = b
582  Equal.cong(Cmp, Bool, k => Cmp.is_le(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
583
584# The reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b).
585law u32_is_gt_to_nat:
586  for a: U32
587  for b: U32
588  {U32.is_gt(a, b) == Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) : Bool}
589
590def u32_is_gt_to_nat(a, b):
591  +a = a
592  +b = b
593  Equal.cong(Cmp, Bool, k => Cmp.is_gt(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
594
595# The reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b).
596law u32_is_ge_to_nat:
597  for a: U32
598  for b: U32
599  {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}
600
601def u32_is_ge_to_nat(a, b):
602  +a = a
603  +b = b
604  Equal.cong(Cmp, Bool, k => Cmp.is_ge(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
605
606def internal_u32_add_exact(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), m)) -> {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}:
607  match a b:
608    case U32{+x} U32{+y}:
609      word_add_exact(32n, x, y, internal_bound(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), m, e, h))
610
611# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b.
612law u32_add_exact:
613  for a: U32
614  for b: U32
615  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
616  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
617
618def u32_add_exact(a, b, h):
619  internal_u32_add_exact(Nat.pow(2n, 32n), a, b, {==}, h)
620
621def internal_u32_add_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), m) : Nat}:
622  match a b:
623    case U32{+x} U32{+y}:
624      %e : {Word.to_nat(32n, Word.add(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), _) : Nat}
625      word_add_wrap(32n, x, y)
626
627# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32.
628law u32_add_wrap:
629  for a: U32
630  for b: U32
631  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
632
633def u32_add_wrap(a, b):
634  internal_u32_add_wrap(Nat.pow(2n, 32n), a, b, {==})
635
636# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b.
637law u32_sub_exact:
638  for a: U32
639  for b: U32
640  for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
641  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
642
643def u32_sub_exact(a, b, h):
644  match a b:
645    case U32{x} U32{y}:
646      word_sub_exact(32n, x, y, h)
647
648def internal_u32_sub_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(m, U32.to_nat(b))), m) : Nat}:
649  match a b:
650    case U32{+x} U32{+y}:
651      %e : {Word.to_nat(32n, Word.sub(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Nat.sub(_, Word.to_nat(32n, y))), _) : Nat}
652      word_sub_wrap(32n, x, y)
653
654# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32.
655law u32_sub_wrap:
656  for a: U32
657  for b: U32
658  {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)) : Nat}
659
660def u32_sub_wrap(a, b):
661  internal_u32_sub_wrap(Nat.pow(2n, 32n), a, b, {==})
662
663def internal_u32_inc_exact(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(1n+U32.to_nat(a), m)) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
664  match a:
665    case U32{+w}:
666      word_inc_exact(32n, w, internal_bound(1n+Word.to_nat(32n, w), m, e, h))
667
668# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a.
669law u32_inc_exact:
670  for a: U32
671  for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
672  {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
673
674def u32_inc_exact(a, h):
675  internal_u32_inc_exact(Nat.pow(2n, 32n), a, {==}, h)
676
677def internal_u32_inc_wrap(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.inc(a)) == Nat.mod(1n+U32.to_nat(a), m) : Nat}:
678  match a:
679    case U32{+w}:
680      %e : {Word.to_nat(32n, Word.inc(32n, w)) == Nat.mod(1n+Word.to_nat(32n, w), _) : Nat}
681      word_inc_wrap(32n, w)
682
683# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32.
684law u32_inc_wrap:
685  for a: U32
686  {U32.to_nat(U32.inc(a)) == Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) : Nat}
687
688def u32_inc_wrap(a):
689  internal_u32_inc_wrap(Nat.pow(2n, 32n), a, {==})
690
691def internal_u32_to_nat_from_nat(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat, h: MNat.lt(k, m)) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}:
692  match k:
693    case 0n:
694      {==}
695    case 1n++p:
696      +h = h
697      +ih = internal_u32_to_nat_from_nat(m, e, p, MNat.lt_trans(p, 1n+p, m, MNat.lt_succ_self(p), h))
698      +hu = internal_lt_congl(1n+p, 1n+U32.to_nat(U32.from_nat(p)), m, Equal.cong(Nat, Nat, z => 1n+z, p, U32.to_nat(U32.from_nat(p)), Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ih)), h)
699      Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p, internal_u32_inc_exact(m, U32.from_nat(p), e, hu), Equal.cong(Nat, Nat, z => 1n+z, U32.to_nat(U32.from_nat(p)), p, ih))
700
701# Converting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k.
702law u32_to_nat_from_nat:
703  for k: Nat
704  for h: MNat.lt(k, Nat.pow(2n, 32n))
705  {U32.to_nat(U32.from_nat(k)) == k : Nat}
706
707def u32_to_nat_from_nat(k, h):
708  internal_u32_to_nat_from_nat(Nat.pow(2n, 32n), {==}, k, h)
709
710# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a.
711law u32_from_nat_to_nat:
712  for a: U32
713  {U32.from_nat(U32.to_nat(a)) == a : U32}
714
715def u32_from_nat_to_nat(a):
716  +a = a
717  u32_to_nat_inj(U32.from_nat(U32.to_nat(a)), a, u32_to_nat_from_nat(U32.to_nat(a), u32_to_nat_lt(a)))
718
719def internal_mod_succ_mod(+p: Nat, +m: Nat) -> {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+p, m) : Nat}:
720  %MNat.mod_add_div(p, m) : {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+_, m) : Nat}
721  Equal.sym(Nat, Nat.mod(Nat.add(1n+Nat.mod(p, m), Nat.mul(m, Nat.div(p, m))), m), Nat.mod(1n+Nat.mod(p, m), m), MNat.add_mul_mod_self_left(1n+Nat.mod(p, m), m, Nat.div(p, m)))
722
723def internal_u32_to_nat_from_nat_mod(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat) -> {U32.to_nat(U32.from_nat(k)) == Nat.mod(k, m) : Nat}:
724  match k:
725    case 0n:
726      Equal.sym(Nat, Nat.mod(0n, m), 0n, MNat.zero_mod(m))
727    case 1n++p:
728      -u = U32.from_nat(p)
729      Equal.trans(Nat, U32.to_nat(U32.inc(u)), Nat.mod(1n+U32.to_nat(u), m), Nat.mod(1n+p, m), internal_u32_inc_wrap(m, U32.from_nat(p), e), Equal.trans(Nat, Nat.mod(1n+U32.to_nat(u), m), Nat.mod(1n+Nat.mod(p, m), m), Nat.mod(1n+p, m), Equal.cong(Nat, Nat, z => Nat.mod(1n+z, m), U32.to_nat(u), Nat.mod(p, m), internal_u32_to_nat_from_nat_mod(m, e, p)), internal_mod_succ_mod(p, m)))
730
731# Converting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32.
732law u32_to_nat_from_nat_mod:
733  for k: Nat
734  {U32.to_nat(U32.from_nat(k)) == Nat.mod(k, Nat.pow(2n, 32n)) : Nat}
735
736def u32_to_nat_from_nat_mod(k):
737  internal_u32_to_nat_from_nat_mod(Nat.pow(2n, 32n), {==}, k)
738
739def internal_min_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, u, v)) == Nat.min(U32.to_nat(u), U32.to_nat(v)) : Nat}:
740  match c:
741    case True{}:
742      Equal.sym(Nat, Nat.min(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.min_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
743    case False{}:
744      Equal.sym(Nat, Nat.min(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.min_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))
745
746# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b).
747law u32_min_to_nat:
748  for a: U32
749  for b: U32
750  {U32.to_nat(U32.min(a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}
751
752def u32_min_to_nat(a, b):
753  match a b:
754    case U32{+x} U32{+y}:
755      internal_min_fin(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), Nat.is_lt(U32.to_nat(U32{x}), U32.to_nat(U32{y})), u32_is_lt_to_nat(U32{x}, U32{y})))
756
757def internal_max_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, v, u)) == Nat.max(U32.to_nat(u), U32.to_nat(v)) : Nat}:
758  match c:
759    case True{}:
760      Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.max_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
761    case False{}:
762      Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.max_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))
763
764# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b).
765law u32_max_to_nat:
766  for a: U32
767  for b: U32
768  {U32.to_nat(U32.max(a, b)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}
769
770def u32_max_to_nat(a, b):
771  match a b:
772    case U32{+x} U32{+y}:
773      internal_max_fin(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), Nat.is_lt(U32.to_nat(U32{x}), U32.to_nat(U32{y})), u32_is_lt_to_nat(U32{x}, U32{y})))
774
775def internal_shl_val(n: Nat, md: Nat, ts: Bool & Word(n)) -> Nat:
776  match ts:
777    case (t, s):
778      Nat.add(Word.to_nat(n, s), Bool.pick(Nat, t, md, 0n))
779
780def internal_shl_con(+p: Nat, +c: Bool, r: Bool & Word(p), -x: Nat, ih: {internal_shl_val(p, Nat.pow(2n, p), r) == x : Nat}) -> {internal_shl_val(1n+p, Nat.pow(2n, 1n+p), Word.shl.out.con(p, c, r)) == Nat.add(internal_bv(c), Nat.double(x)) : Nat}:
781  match r:
782    case (+hi, +t2):
783      +u = Word.to_nat(p, t2)
784      +v = Bool.pick(Nat, hi, Nat.pow(2n, p), 0n)
785      %ih : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), Bool.pick(Nat, hi, Nat.pow(2n, 1n+p), 0n)) == Nat.add(internal_bv(c), Nat.double(_)) : Nat}
786      %MNat.double_add_sym(u, v) : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), Bool.pick(Nat, hi, Nat.pow(2n, 1n+p), 0n)) == Nat.add(internal_bv(c), _) : Nat}
787      %internal_pick_pow(hi, p) : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), _) == Nat.add(internal_bv(c), Nat.add(Nat.double(u), Nat.double(v))) : Nat}
788      %internal_to_nat_con(p, c, t2) : {Nat.add(_, Nat.double(v)) == Nat.add(internal_bv(c), Nat.add(Nat.double(u), Nat.double(v))) : Nat}
789      MNat.add_assoc(internal_bv(c), Nat.double(u), Nat.double(v))
790
791def internal_shl_out(n: Nat, c: Bool, w: Word(n)) -> {internal_shl_val(n, Nat.pow(2n, n), Word.shl.out(n, c, w)) == Nat.add(internal_bv(c), Nat.double(Word.to_nat(n, w))) : Nat}:
792  match n:
793    case 0n:
794      match c:
795        case False{}:
796          match w:
797            case WNil{}:
798              {==}
799        case True{}:
800          match w:
801            case WNil{}:
802              {==}
803    case 1n++p:
804      match w:
805        case WCon{+b, +t}:
806          %internal_to_nat_con(p, b, t) : {internal_shl_val(1n+p, Nat.pow(2n, 1n+p), Word.shl.out(1n+p, c, WCon{b, t})) == Nat.add(internal_bv(c), Nat.double(_)) : Nat}
807          internal_shl_con(p, c, Word.shl.out(p, b, t), Nat.add(internal_bv(b), Nat.double(Word.to_nat(p, t))), internal_shl_out(p, b, t))
808
809def internal_shl_out32(-md: Nat, em: {Nat.pow(2n, 32n) == md : Nat}, x: Bool, rw: Word(32n)) -> {internal_shl_val(32n, md, Word.shl.out(32n, x, rw)) == Nat.add(internal_bv(x), Nat.double(Word.to_nat(32n, rw))) : Nat}:
810  %em : {internal_shl_val(32n, _, Word.shl.out(32n, x, rw)) == Nat.add(internal_bv(x), Nat.double(Word.to_nat(32n, rw))) : Nat}
811  internal_shl_out(32n, x, rw)
812
813def internal_div_step(+k: Nat, +q: Nat, +b: Nat, +r2: Nat, +x: Nat, +r: Nat, -a: Nat, ek: {Nat.add(Nat.mul(k, b), r2) == Nat.add(x, Nat.double(r)) : Nat}, ea: {Nat.add(Nat.mul(q, b), r) == a : Nat}) -> {Nat.add(Nat.mul(Nat.add(k, Nat.double(q)), b), r2) == Nat.add(x, Nat.double(a)) : Nat}:
814  -l = Nat.add(Nat.mul(Nat.add(k, Nat.double(q)), b), r2)
815  %ea : {l == Nat.add(x, Nat.double(_)) : Nat}
816  %MNat.double_add_sym(Nat.mul(q, b), r) : {l == Nat.add(x, _) : Nat}
817  %MNat.double_mul_sym(q, b) : {l == Nat.add(x, Nat.add(_, Nat.double(r))) : Nat}
818  %MNat.add_mul_sym(k, Nat.double(q), b) : {Nat.add(_, r2) == Nat.add(x, Nat.add(Nat.mul(Nat.double(q), b), Nat.double(r))) : Nat}
819  %MNat.add_left_comm(Nat.mul(Nat.double(q), b), x, Nat.double(r)) : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == _ : Nat}
820  %ek : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == Nat.add(Nat.mul(Nat.double(q), b), _) : Nat}
821  %MNat.add_left_comm(Nat.mul(k, b), Nat.mul(Nat.double(q), b), r2) : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == _ : Nat}
822  MNat.add_assoc(Nat.mul(k, b), Nat.mul(Nat.double(q), b), r2)
823
824def internal_bit_double_lt(x: Bool, +r: Nat, +b: Nat, h: MNat.lt(r, b)) -> MNat.lt(Nat.add(internal_bv(x), Nat.double(r)), Nat.double(b)):
825  match x:
826    case False{}:
827      MNat.double_lt_double(r, b, h)
828    case True{}:
829      %Equal.sym(Bool, Nat.is_lt(1n+Nat.double(r), Nat.double(b)), Nat.is_le(2n+Nat.double(r), Nat.double(b)), MNat.is_lt_eq_succ_le(1n+Nat.double(r), Nat.double(b))) : {_ == True{} : Bool}
830      MNat.double_le_double(1n+r, b, MNat.succ_le_of_lt(r, b, h))
831
832def internal_rem_lt_add(+b: Nat, +r2: Nat, -v: Nat, e: {Nat.add(b, r2) == v : Nat}, h: MNat.lt(v, Nat.double(b))) -> MNat.lt(Nat.add(b, r2), Nat.add(b, b)):
833  %Equal.sym(Nat, Nat.add(b, r2), v, e) : MNat.lt(_, Nat.add(b, b))
834  %MNat.double_eq_add(b) : MNat.lt(v, _)
835  h
836
837def internal_rem_lt(+b: Nat, +r2: Nat, -v: Nat, e: {Nat.add(b, r2) == v : Nat}, h: MNat.lt(v, Nat.double(b))) -> MNat.lt(r2, b):
838  MNat.lt_of_add_lt_add_left(b, r2, b, internal_rem_lt_add(b, r2, v, e, h))
839
840def internal_wrap_sum(+b: Nat, +s: Nat, +m: Nat, -v: Nat, hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}) -> {Nat.add(b, Nat.add(s, Nat.sub(m, b))) == v : Nat}:
841  %MNat.add_left_comm(s, b, Nat.sub(m, b)) : {_ == v : Nat}
842  %Equal.sym(Nat, Nat.add(b, Nat.sub(m, b)), m, MNat.add_sub_of_le(b, m, MNat.le_of_lt(b, m, hb))) : {Nat.add(s, _) == v : Nat}
843  es
844
845def internal_wrap_rem(+b: Nat, +s: Nat, +m: Nat, +v: Nat, +hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}, hv: MNat.lt(v, Nat.double(b))) -> {Nat.add(b, Nat.mod(Nat.add(s, Nat.sub(m, b)), m)) == v : Nat}:
846  +y = Nat.add(s, Nat.sub(m, b))
847  +ey = internal_wrap_sum(b, s, m, v, hb, es)
848  +hy = internal_rem_lt(b, y, v, ey, hv)
849  %Equal.sym(Nat, Nat.mod(y, m), y, MNat.mod_eq_of_lt(y, m, MNat.lt_trans(y, b, m, hy, hb))) : {Nat.add(b, _) == v : Nat}
850  ey
851
852def internal_dm_inv(m: Nat, b: Nat, a: Nat, qr: Word(m) & U32) -> Type:
853  match qr:
854    case (q, r):
855      {Nat.add(Nat.mul(Word.to_nat(m, q), b), U32.to_nat(r)) == a : Nat} & MNat.lt(U32.to_nat(r), b)
856
857def internal_dm_take(+p: Nat, +q: Word(p), +b: Nat, +r2: Nat, +x: Bool, +r: Nat, -a: Nat, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), b), r) == a : Nat}, hr: MNat.lt(r, b), +e2: {Nat.add(b, r2) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), b), r2) == Nat.add(internal_bv(x), Nat.double(a)) : Nat} & MNat.lt(r2, b):
858  +ek = Equal.trans(Nat, Nat.add(Nat.mul(1n, b), r2), Nat.add(b, r2), Nat.add(internal_bv(x), Nat.double(r)), Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(1n, b), b, MNat.one_mul(b)), e2)
859  (internal_div_step(1n, Word.to_nat(p, q), b, r2, internal_bv(x), r, a, ek, ea), internal_rem_lt(b, r2, Nat.add(internal_bv(x), Nat.double(r)), e2, internal_bit_double_lt(x, r, b, hr)))
860
861def internal_dm_wrap(+b: U32, +s: Word(32n), +x: Bool, +r: Nat, +m: Nat, +em: {Nat.pow(2n, 32n) == m : Nat}, hr: MNat.lt(r, U32.to_nat(b)), es: {Nat.add(Word.to_nat(32n, s), m) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> {Nat.add(U32.to_nat(b), U32.to_nat(U32.sub(U32{s}, b))) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}:
862  +bn = U32.to_nat(b)
863  +sn = Word.to_nat(32n, s)
864  +v = Nat.add(internal_bv(x), Nat.double(r))
865  %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.add(sn, Nat.sub(m, bn)), m), internal_u32_sub_wrap(m, U32{s}, b, em)) : {Nat.add(bn, _) == v : Nat}
866  internal_wrap_rem(bn, sn, m, v, internal_u32_to_nat_lt(m, b, em), es, internal_bit_double_lt(x, r, bn, hr))
867
868def internal_dm_fin(+p: Nat, +q: Word(p), +s: Word(32n), +b: U32, +x: Bool, +r: Nat, -a: Nat, +m: Nat, +em: {Nat.pow(2n, 32n) == m : Nat}, t: Bool, g: Bool, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == a : Nat}, +hr: MNat.lt(r, U32.to_nat(b)), es: {Nat.add(Word.to_nat(32n, s), Bool.pick(Nat, t, m, 0n)) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}, eg: {Bool.or(t, U32.is_ge(U32{s}, b)) == g : Bool}) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.fin(p, q, U32{s}, b, g)):
869  match t g:
870    case True{} True{}:
871      internal_dm_take(p, q, U32.to_nat(b), U32.to_nat(U32.sub(U32{s}, b)), x, r, a, ea, hr, internal_dm_wrap(b, s, x, r, m, em, hr, es))
872    case True{} False{}:
873      Empty.absurd(internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.fin(p, q, U32{s}, b, False{})), MNat.internal_div_true_ne_false(eg))
874    case False{} True{}:
875      +bn = U32.to_nat(b)
876      +sn = Word.to_nat(32n, s)
877      +hle = Equal.trans(Bool, Nat.is_le(bn, sn), U32.is_ge(U32{s}, b), True{}, Equal.trans(Bool, Nat.is_le(bn, sn), Nat.is_ge(sn, bn), U32.is_ge(U32{s}, b), MNat.is_ge_eq_is_le_sym(sn, bn), Equal.sym(Bool, U32.is_ge(U32{s}, b), Nat.is_ge(sn, bn), u32_is_ge_to_nat(U32{s}, b))), eg)
878      +e2 = Equal.trans(Nat, Nat.add(bn, U32.to_nat(U32.sub(U32{s}, b))), Nat.add(bn, Nat.sub(sn, bn)), Nat.add(internal_bv(x), Nat.double(r)), Equal.cong(Nat, Nat, z => Nat.add(bn, z), U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(sn, bn), u32_sub_exact(U32{s}, b, hle)), Equal.trans(Nat, Nat.add(bn, Nat.sub(sn, bn)), sn, Nat.add(internal_bv(x), Nat.double(r)), MNat.add_sub_of_le(bn, sn, hle), Equal.trans(Nat, sn, Nat.add(sn, 0n), Nat.add(internal_bv(x), Nat.double(r)), MNat.add_zero_sym(sn), es)))
879      internal_dm_take(p, q, bn, U32.to_nat(U32.sub(U32{s}, b)), x, r, a, ea, hr, e2)
880    case False{} False{}:
881      +bn = U32.to_nat(b)
882      +sn = Word.to_nat(32n, s)
883      +hnle = Equal.trans(Bool, Nat.is_le(bn, sn), U32.is_ge(U32{s}, b), False{}, Equal.trans(Bool, Nat.is_le(bn, sn), Nat.is_ge(sn, bn), U32.is_ge(U32{s}, b), MNat.is_ge_eq_is_le_sym(sn, bn), Equal.sym(Bool, U32.is_ge(U32{s}, b), Nat.is_ge(sn, bn), u32_is_ge_to_nat(U32{s}, b))), eg)
884      +ek = Equal.trans(Nat, sn, Nat.add(sn, 0n), Nat.add(internal_bv(x), Nat.double(r)), MNat.add_zero_sym(sn), es)
885      (internal_div_step(0n, Word.to_nat(p, q), bn, sn, internal_bv(x), r, a, ek, ea), MNat.lt_of_not_le(bn, sn, hnle))
886
887def internal_dm_shl(+p: Nat, +q: Word(p), +b: U32, +x: Bool, +r: Nat, -a: Nat, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == a : Nat}, +hr: MNat.lt(r, U32.to_nat(b)), +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, ts: Bool & Word(32n), es: {internal_shl_val(32n, md, ts) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.shl(p, q, b, ts)):
888  match ts:
889    case (+t, +s):
890      internal_dm_fin(p, q, s, b, x, r, a, md, em, t, Bool.or(t, U32.is_ge(U32{s}, b)), ea, hr, es, {==})
891
892def internal_dm_rec(+p: Nat, +x: Bool, +b: U32, +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, -a: Nat, qr: Word(p) & U32, ih: internal_dm_inv(p, U32.to_nat(b), a, qr)) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.rec(p, x, b, qr)):
893  match qr:
894    case (+q, r):
895      match r:
896        case U32{+rw}:
897          match ih:
898            case (ea, +hr):
899              internal_dm_shl(p, q, b, x, Word.to_nat(32n, rw), a, ea, hr, md, em, Word.shl.out(32n, x, rw), internal_shl_out32(md, em, x, rw))
900
901def internal_dm_go(m: Nat, w: Word(m), +b: U32, +hb: MNat.lt(0n, U32.to_nat(b)), +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}) -> internal_dm_inv(m, U32.to_nat(b), Word.to_nat(m, w), U32.divmod.go(m, w, b)):
902  match m:
903    case 0n:
904      match w:
905        case WNil{}:
906          ({==}, hb)
907    case 1n++p:
908      match w:
909        case WCon{+x, +hi}:
910          %internal_to_nat_con(p, x, hi) : internal_dm_inv(1n+p, U32.to_nat(b), _, U32.divmod.go(1n+p, WCon{x, hi}, b))
911          internal_dm_rec(p, x, b, md, em, Word.to_nat(p, hi), U32.divmod.go(p, hi, b), internal_dm_go(p, hi, b, hb, md, em))
912
913def internal_div_unique(+q: Nat, b: Nat, +r: Nat, -a: Nat, hb: MNat.lt(0n, b), e: {Nat.add(Nat.mul(q, b), r) == a : Nat}, h: MNat.lt(r, b)) -> {q == Nat.div(a, b) : Nat}:
914  match b:
915    case 0n:
916      Empty.absurd({q == Nat.div(a, 0n) : Nat}, MNat.internal_false_ne_true(hb))
917    case 1n++bp:
918      %e : {q == Nat.div(_, 1n+bp) : Nat}
919      %MNat.add_comm(r, Nat.mul(q, 1n+bp)) : {q == Nat.div(_, 1n+bp) : Nat}
920      %MNat.add_mul_div_right_sym(r, q, bp) : {q == _ : Nat}
921      %Equal.sym(Nat, Nat.div(r, 1n+bp), 0n, MNat.div_eq_zero_of_le(r, bp, MNat.le_of_lt_succ(r, bp, h))) : {q == Nat.add(_, q) : Nat}
922      {==}
923
924def internal_div_fin(+b: U32, -a: Nat, hb: MNat.lt(0n, U32.to_nat(b)), qr: Word(32n) & U32, inv: internal_dm_inv(32n, U32.to_nat(b), a, qr)) -> {U32.to_nat(U32.div.fin(qr)) == Nat.div(a, U32.to_nat(b)) : Nat}:
925  match qr:
926    case (q, r):
927      match inv:
928        case (e, h):
929          internal_div_unique(Word.to_nat(32n, q), U32.to_nat(b), U32.to_nat(r), a, hb, e, h)
930
931def internal_div_if(+md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, +aw: Word(32n), +bw: Word(32n), z: Bool, ez: {U32.is_zero(U32{bw}) == z : Bool}) -> {U32.to_nat(U32.div.if(aw, U32{bw}, z)) == Nat.div(Word.to_nat(32n, aw), Word.to_nat(32n, bw)) : Nat}:
932  match z:
933    case True{}:
934      +bn = Word.to_nat(32n, bw)
935      +ee = Equal.trans(Bool, Nat.is_eq(bn, 0n), U32.is_zero(U32{bw}), True{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(bn, 0n), u32_is_eq_to_nat(U32{bw}, 0)), ez)
936      %Equal.sym(Nat, bn, 0n, MNat.eq_of_is_eq(bn, 0n, ee)) : {0n == Nat.div(Word.to_nat(32n, aw), _) : Nat}
937      {==}
938    case False{}:
939      +bn = Word.to_nat(32n, bw)
940      +ee = Equal.trans(Bool, Nat.is_eq(bn, 0n), U32.is_zero(U32{bw}), False{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(bn, 0n), u32_is_eq_to_nat(U32{bw}, 0)), ez)
941      +hb = MNat.pos_of_ne_zero(bn, ee)
942      internal_div_fin(U32{bw}, Word.to_nat(32n, aw), hb, U32.divmod.go(32n, aw, U32{bw}), internal_dm_go(32n, aw, U32{bw}, hb, md, em))
943
944# U32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b.
945law u32_div_to_nat:
946  for a: U32
947  for b: U32
948  {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}
949
950def u32_div_to_nat(a, b):
951  match a b:
952    case U32{aw} U32{+bw}:
953      internal_div_if(Nat.pow(2n, 32n), {==}, aw, bw, U32.is_zero(U32{bw}), {==})
954
955# U32 division is antitone in a positive divisor: 0 < s and s <= t imply a / t <= a / s.
956law u32_div_le_div_left:
957  for a: U32
958  for s: U32
959  for t: U32
960  for hs: {U32.is_lt(0, s) == True{} : Bool}
961  for h: {U32.is_le(s, t) == True{} : Bool}
962  {U32.is_le(U32.div(a, t), U32.div(a, s)) == True{} : Bool}
963
964def u32_div_le_div_left(a, s, t, hs, h):
965  +a = a
966  +s = s
967  +t = t
968  %Equal.sym(Bool, U32.is_le(U32.div(a, t), U32.div(a, s)), Nat.is_le(U32.to_nat(U32.div(a, t)), U32.to_nat(U32.div(a, s))), u32_is_le_to_nat(U32.div(a, t), U32.div(a, s))) : {_ == True{} : Bool}
969  %Equal.sym(Nat, U32.to_nat(U32.div(a, t)), Nat.div(U32.to_nat(a), U32.to_nat(t)), u32_div_to_nat(a, t)) : {Nat.is_le(_, U32.to_nat(U32.div(a, s))) == True{} : Bool}
970  %Equal.sym(Nat, U32.to_nat(U32.div(a, s)), Nat.div(U32.to_nat(a), U32.to_nat(s)), u32_div_to_nat(a, s)) : {Nat.is_le(Nat.div(U32.to_nat(a), U32.to_nat(t)), _) == True{} : Bool}
971  +hs2 = Equal.trans(Bool, Nat.is_lt(U32.to_nat(0), U32.to_nat(s)), U32.is_lt(0, s), True{}, Equal.sym(Bool, U32.is_lt(0, s), Nat.is_lt(U32.to_nat(0), U32.to_nat(s)), u32_is_lt_to_nat(0, s)), hs)
972  +h2 = Equal.trans(Bool, Nat.is_le(U32.to_nat(s), U32.to_nat(t)), U32.is_le(s, t), True{}, Equal.sym(Bool, U32.is_le(s, t), Nat.is_le(U32.to_nat(s), U32.to_nat(t)), u32_is_le_to_nat(s, t)), h)
973  MNat.div_le_div_left(U32.to_nat(a), U32.to_nat(s), U32.to_nat(t), hs2, h2)
974
975# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
976
977# The zero word is the natural zero: to_nat (zero n) = 0, reversed to rewrite toward the simple side.
978law word_to_nat_zero_sym:
979  for n: Nat
980  {0n == Word.to_nat(n, Word.zero(n)) : Nat}
981
982def word_to_nat_zero_sym(n):
983  Equal.sym(Nat, Word.to_nat(n, Word.zero(n)), 0n, word_to_nat_zero(n))
984
985# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
986law word_cmp_to_nat_sym:
987  for n: Nat
988  for a: Word(n)
989  for b: Word(n)
990  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}
991
992def word_cmp_to_nat_sym(n, a, b):
993  Equal.sym(Cmp, Word.cmp(n, a, b), Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)), word_cmp_to_nat(n, a, b))
994
995# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n, reversed to rewrite toward the simple side.
996law word_not_add_sym:
997  for n: Nat
998  for w: Word(n)
999  {Nat.pow(2n, n) == 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) : Nat}
1000
1001def word_not_add_sym(n, w):
1002  Equal.sym(Nat, 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)), Nat.pow(2n, n), word_not_add(n, w))
1003
1004# The adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in, reversed to rewrite toward the simple side.
1005law word_adc_exact_sym:
1006  for n: Nat
1007  for a: Word(n)
1008  for b: Word(n)
1009  for c: Bool
1010  for h: MNat.lt(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n))
1011  {Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) == Word.to_nat(n, Word.adc(n, a, b, False{}, c)) : Nat}
1012
1013def word_adc_exact_sym(n, a, b, c, h):
1014  Equal.sym(Nat, Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), word_adc_exact(n, a, b, c, h))
1015
1016# The adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in, reversed to rewrite toward the simple side.
1017law word_adc_overflow_sym:
1018  for n: Nat
1019  for a: Word(n)
1020  for b: Word(n)
1021  for c: Bool
1022  for h: MNat.le(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)))
1023  {Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)) : Nat}
1024
1025def word_adc_overflow_sym(n, a, b, c, h):
1026  Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), word_adc_overflow(n, a, b, c, h))
1027
1028# The adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n, reversed to rewrite toward the simple side.
1029law word_adc_wrap_sym:
1030  for n: Nat
1031  for a: Word(n)
1032  for b: Word(n)
1033  for c: Bool
1034  {Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)) == Word.to_nat(n, Word.adc(n, a, b, False{}, c)) : Nat}
1035
1036def word_adc_wrap_sym(n, a, b, c):
1037  Equal.sym(Nat, Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)), word_adc_wrap(n, a, b, c))
1038
1039# Word addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b, reversed to rewrite toward the simple side.
1040law word_add_exact_sym:
1041  for n: Nat
1042  for a: Word(n)
1043  for b: Word(n)
1044  for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
1045  {Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
1046
1047def word_add_exact_sym(n, a, b, h):
1048  Equal.sym(Nat, Word.to_nat(n, Word.add(n, a, b)), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_add_exact(n, a, b, h))
1049
1050# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n, reversed to rewrite toward the simple side.
1051law word_add_wrap_sym:
1052  for n: Nat
1053  for a: Word(n)
1054  for b: Word(n)
1055  {Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
1056
1057def word_add_wrap_sym(n, a, b):
1058  Equal.sym(Nat, 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)), word_add_wrap(n, a, b))
1059
1060# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w, reversed to rewrite toward the simple side.
1061law word_inc_exact_sym:
1062  for n: Nat
1063  for w: Word(n)
1064  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
1065  {1n+Word.to_nat(n, w) == Word.to_nat(n, Word.inc(n, w)) : Nat}
1066
1067def word_inc_exact_sym(n, w, h):
1068  Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), word_inc_exact(n, w, h))
1069
1070# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n, reversed to rewrite toward the simple side.
1071law word_inc_wrap_sym:
1072  for n: Nat
1073  for w: Word(n)
1074  {Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) == Word.to_nat(n, Word.inc(n, w)) : Nat}
1075
1076def word_inc_wrap_sym(n, w):
1077  Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)), word_inc_wrap(n, w))
1078
1079# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b, reversed to rewrite toward the simple side.
1080law word_sub_exact_sym:
1081  for n: Nat
1082  for a: Word(n)
1083  for b: Word(n)
1084  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
1085  {Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
1086
1087def word_sub_exact_sym(n, a, b, h):
1088  Equal.sym(Nat, Word.to_nat(n, Word.sub(n, a, b)), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), word_sub_exact(n, a, b, h))
1089
1090# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n, reversed to rewrite toward the simple side.
1091law word_sub_wrap_sym:
1092  for n: Nat
1093  for a: Word(n)
1094  for b: Word(n)
1095  {Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
1096
1097def word_sub_wrap_sym(n, a, b):
1098  Equal.sym(Nat, Word.to_nat(n, Word.sub(n, a, b)), Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)), word_sub_wrap(n, a, b))
1099
1100# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1101law u32_cmp_to_nat_sym:
1102  for a: U32
1103  for b: U32
1104  {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}
1105
1106def u32_cmp_to_nat_sym(a, b):
1107  Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
1108
1109# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1110law u32_is_eq_to_nat_sym:
1111  for a: U32
1112  for b: U32
1113  {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == U32.is_eq(a, b) : Bool}
1114
1115def u32_is_eq_to_nat_sym(a, b):
1116  Equal.sym(Bool, U32.is_eq(a, b), Nat.is_eq(U32.to_nat(a), U32.to_nat(b)), u32_is_eq_to_nat(a, b))
1117
1118# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1119law u32_is_ne_to_nat_sym:
1120  for a: U32
1121  for b: U32
1122  {Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) == U32.is_ne(a, b) : Bool}
1123
1124def u32_is_ne_to_nat_sym(a, b):
1125  Equal.sym(Bool, U32.is_ne(a, b), Nat.is_ne(U32.to_nat(a), U32.to_nat(b)), u32_is_ne_to_nat(a, b))
1126
1127# The U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1128law u32_is_lt_to_nat_sym:
1129  for a: U32
1130  for b: U32
1131  {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}
1132
1133def u32_is_lt_to_nat_sym(a, b):
1134  Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), u32_is_lt_to_nat(a, b))
1135
1136# The U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1137law u32_is_le_to_nat_sym:
1138  for a: U32
1139  for b: U32
1140  {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}
1141
1142def u32_is_le_to_nat_sym(a, b):
1143  Equal.sym(Bool, U32.is_le(a, b), Nat.is_le(U32.to_nat(a), U32.to_nat(b)), u32_is_le_to_nat(a, b))
1144
1145# The reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1146law u32_is_gt_to_nat_sym:
1147  for a: U32
1148  for b: U32
1149  {Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) == U32.is_gt(a, b) : Bool}
1150
1151def u32_is_gt_to_nat_sym(a, b):
1152  Equal.sym(Bool, U32.is_gt(a, b), Nat.is_gt(U32.to_nat(a), U32.to_nat(b)), u32_is_gt_to_nat(a, b))
1153
1154# The reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1155law u32_is_ge_to_nat_sym:
1156  for a: U32
1157  for b: U32
1158  {Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) == U32.is_ge(a, b) : Bool}
1159
1160def u32_is_ge_to_nat_sym(a, b):
1161  Equal.sym(Bool, U32.is_ge(a, b), Nat.is_ge(U32.to_nat(a), U32.to_nat(b)), u32_is_ge_to_nat(a, b))
1162
1163# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b, reversed to rewrite toward the simple side.
1164law u32_add_exact_sym:
1165  for a: U32
1166  for b: U32
1167  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
1168  {Nat.add(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.add(a, b)) : Nat}
1169
1170def u32_add_exact_sym(a, b, h):
1171  Equal.sym(Nat, U32.to_nat(U32.add(a, b)), Nat.add(U32.to_nat(a), U32.to_nat(b)), u32_add_exact(a, b, h))
1172
1173# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32, reversed to rewrite toward the simple side.
1174law u32_add_wrap_sym:
1175  for a: U32
1176  for b: U32
1177  {Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == U32.to_nat(U32.add(a, b)) : Nat}
1178
1179def u32_add_wrap_sym(a, b):
1180  Equal.sym(Nat, U32.to_nat(U32.add(a, b)), Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)), u32_add_wrap(a, b))
1181
1182# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b, reversed to rewrite toward the simple side.
1183law u32_sub_exact_sym:
1184  for a: U32
1185  for b: U32
1186  for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
1187  {Nat.sub(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.sub(a, b)) : Nat}
1188
1189def u32_sub_exact_sym(a, b, h):
1190  Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.sub(U32.to_nat(a), U32.to_nat(b)), u32_sub_exact(a, b, h))
1191
1192# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32, reversed to rewrite toward the simple side.
1193law u32_sub_wrap_sym:
1194  for a: U32
1195  for b: U32
1196  {Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)) == U32.to_nat(U32.sub(a, b)) : Nat}
1197
1198def u32_sub_wrap_sym(a, b):
1199  Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)), u32_sub_wrap(a, b))
1200
1201# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a, reversed to rewrite toward the simple side.
1202law u32_inc_exact_sym:
1203  for a: U32
1204  for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
1205  {1n+U32.to_nat(a) == U32.to_nat(U32.inc(a)) : Nat}
1206
1207def u32_inc_exact_sym(a, h):
1208  Equal.sym(Nat, U32.to_nat(U32.inc(a)), 1n+U32.to_nat(a), u32_inc_exact(a, h))
1209
1210# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32, reversed to rewrite toward the simple side.
1211law u32_inc_wrap_sym:
1212  for a: U32
1213  {Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) == U32.to_nat(U32.inc(a)) : Nat}
1214
1215def u32_inc_wrap_sym(a):
1216  Equal.sym(Nat, U32.to_nat(U32.inc(a)), Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)), u32_inc_wrap(a))
1217
1218# Converting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k, reversed to rewrite toward the simple side.
1219law u32_to_nat_from_nat_sym:
1220  for k: Nat
1221  for h: MNat.lt(k, Nat.pow(2n, 32n))
1222  {k == U32.to_nat(U32.from_nat(k)) : Nat}
1223
1224def u32_to_nat_from_nat_sym(k, h):
1225  Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), k, u32_to_nat_from_nat(k, h))
1226
1227# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a, reversed to rewrite toward the simple side.
1228law u32_from_nat_to_nat_sym:
1229  for a: U32
1230  {a == U32.from_nat(U32.to_nat(a)) : U32}
1231
1232def u32_from_nat_to_nat_sym(a):
1233  Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, u32_from_nat_to_nat(a))
1234
1235# Converting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32, reversed to rewrite toward the simple side.
1236law u32_to_nat_from_nat_mod_sym:
1237  for k: Nat
1238  {Nat.mod(k, Nat.pow(2n, 32n)) == U32.to_nat(U32.from_nat(k)) : Nat}
1239
1240def u32_to_nat_from_nat_mod_sym(k):
1241  Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), Nat.mod(k, Nat.pow(2n, 32n)), u32_to_nat_from_nat_mod(k))
1242
1243# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1244law u32_min_to_nat_sym:
1245  for a: U32
1246  for b: U32
1247  {Nat.min(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.min(a, b)) : Nat}
1248
1249def u32_min_to_nat_sym(a, b):
1250  Equal.sym(Nat, U32.to_nat(U32.min(a, b)), Nat.min(U32.to_nat(a), U32.to_nat(b)), u32_min_to_nat(a, b))
1251
1252# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1253law u32_max_to_nat_sym:
1254  for a: U32
1255  for b: U32
1256  {Nat.max(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.max(a, b)) : Nat}
1257
1258def u32_max_to_nat_sym(a, b):
1259  Equal.sym(Nat, U32.to_nat(U32.max(a, b)), Nat.max(U32.to_nat(a), U32.to_nat(b)), u32_max_to_nat(a, b))
1260
1261# U32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b, reversed to rewrite toward the simple side.
1262law u32_div_to_nat_sym:
1263  for a: U32
1264  for b: U32
1265  {Nat.div(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.div(a, b)) : Nat}
1266
1267def u32_div_to_nat_sym(a, b):
1268  Equal.sym(Nat, U32.to_nat(U32.div(a, b)), Nat.div(U32.to_nat(a), U32.to_nat(b)), u32_div_to_nat(a, b))