proof_u32.bend

lawful-words@0.1.0.0 · 1,335 lines · 100 definitions

1import Base
2import lawful-words@0.1.0.0/proof_nat.bend as N
3import lawful-words@0.1.0.0/proof_word.bend as W
4import lawful-words@0.1.0.0/defs.bend as D
5
6# The U32 laws, restated with every variable reusable. Most are the Word(n)
7# lemmas of proof_word.bend at n = 32.
8#
9# 2^32 is a closed Nat, and the checker compares two different terms that
10# contain it by unfolding it in unary, which overflows. So a lemma whose proof
11# needs 2^32 is first proven as `name.m`, for any m with Nat.pow(2n, 32n) == m
12# (hm), where conversions are cheap; Nat.pow(2n, 32n) only appears where hm
13# rewrites m into it right before a Word lemma of exactly that type. The
14# statement itself then takes m = Nat.pow(2n, 32n) and hm = {==}.
15
16# The Word lemmas at n = 32, with m for 2^32
17# ==========================================
18
19law wlt.m:
20  for +w: Word(32n)
21  for +m: Nat
22  for +hm: {Nat.pow(2n, 32n) == m : Nat}
23  {Nat.is_lt(Word.to_nat(32n, w), m) == True{} : Bool}
24
25def wlt.m(w, m, hm):
26  %hm : {Nat.is_lt(Word.to_nat(32n, w), _) == True{} : Bool}
27  W.wlt(32n, w)
28
29law winc.m:
30  for +w: Word(32n)
31  for +m: Nat
32  for +hm: {Nat.pow(2n, 32n) == m : Nat}
33  {Nat.add(Word.to_nat(32n, Word.inc(32n, w)), Nat.mul(N.bn(W.incc(32n, w)), m)) == 1n+Word.to_nat(32n, w) : Nat}
34
35def winc.m(w, m, hm):
36  %hm : {Nat.add(Word.to_nat(32n, Word.inc(32n, w)), Nat.mul(N.bn(W.incc(32n, w)), _)) == 1n+Word.to_nat(32n, w) : Nat}
37  W.winc(32n, w)
38
39law wadc.m:
40  for +x: Word(32n)
41  for +y: Word(32n)
42  for +c: Bool
43  for +m: Nat
44  for +hm: {Nat.pow(2n, 32n) == m : Nat}
45  {Nat.add(Word.to_nat(32n, Word.adc(32n, x, y, False{}, c)), Nat.mul(N.bn(W.cout(32n, x, y, c)), m))
46    == Nat.add(N.bn(c), Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y))) : Nat}
47
48def wadc.m(x, y, c, m, hm):
49  %hm : {Nat.add(Word.to_nat(32n, Word.adc(32n, x, y, False{}, c)), Nat.mul(N.bn(W.cout(32n, x, y, c)), _))
50    == Nat.add(N.bn(c), Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y))) : Nat}
51  W.wadc(32n, x, y, c)
52
53law wnot.m:
54  for +w: Word(32n)
55  for +m: Nat
56  for +hm: {Nat.pow(2n, 32n) == m : Nat}
57  {1n+Nat.add(Word.to_nat(32n, Word.not(32n, w)), Word.to_nat(32n, w)) == m : Nat}
58
59def wnot.m(w, m, hm):
60  %hm : {1n+Nat.add(Word.to_nat(32n, Word.not(32n, w)), Word.to_nat(32n, w)) == _ : Nat}
61  W.wnot(32n, w)
62
63law wshl.m:
64  for +w: Word(32n)
65  for +m: Nat
66  for +hm: {Nat.pow(2n, 32n) == m : Nat}
67  {Nat.add(Word.to_nat(32n, Word.shl(32n, w)), Nat.mul(N.bn(W.shtop(32n, w)), m)) == Nat.double(Word.to_nat(32n, w)) : Nat}
68
69def wshl.m(w, m, hm):
70  %hm : {Nat.add(Word.to_nat(32n, Word.shl(32n, w)), Nat.mul(N.bn(W.shtop(32n, w)), _)) == Nat.double(Word.to_nat(32n, w)) : Nat}
71  W.wshl(32n, w)
72
73law wput.m:
74  for +c: Bool
75  for +w: Word(32n)
76  for +m: Nat
77  for +hm: {Nat.pow(2n, 32n) == m : Nat}
78  {Nat.add(Word.to_nat(32n, Word.shl.put(32n, c, w)), Nat.mul(N.bn(W.stop(32n, c, w)), m))
79    == Nat.add(N.bn(c), Nat.double(Word.to_nat(32n, w))) : Nat}
80
81def wput.m(c, w, m, hm):
82  %hm : {Nat.add(Word.to_nat(32n, Word.shl.put(32n, c, w)), Nat.mul(N.bn(W.stop(32n, c, w)), _))
83    == Nat.add(N.bn(c), Nat.double(Word.to_nat(32n, w))) : Nat}
84  W.wput(32n, c, w)
85
86law wmul.m:
87  for +x: Word(32n)
88  for +y: Word(32n)
89  for +m: Nat
90  for +hm: {Nat.pow(2n, 32n) == m : Nat}
91  {Word.to_nat(32n, Word.mul.go(32n, 32n, x, y, Word.zero(32n)))
92    == Nat.mod(Nat.add(Word.to_nat(32n, Word.zero(32n)), Nat.mul(Word.to_nat(32n, x), Word.to_nat(32n, y))), m) : Nat}
93
94def wmul.m(x, y, m, hm):
95  %hm : {Word.to_nat(32n, Word.mul.go(32n, 32n, x, y, Word.zero(32n)))
96    == Nat.mod(Nat.add(Word.to_nat(32n, Word.zero(32n)), Nat.mul(Word.to_nat(32n, x), Word.to_nat(32n, y))), _) : Nat}
97  W.wmul_go(32n, 32n, x, y, Word.zero(32n))
98
99law wsub_val.m:
100  for +x: Word(32n)
101  for +y: Word(32n)
102  for +m: Nat
103  for +hm: {Nat.pow(2n, 32n) == m : Nat}
104  {Nat.sub(Nat.add(Word.to_nat(32n, x), m), Word.to_nat(32n, y))
105    == 1n+Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, Word.not(32n, y))) : Nat}
106
107def wsub_val.m(x, y, m, hm):
108  %hm : {Nat.sub(Nat.add(Word.to_nat(32n, x), _), Word.to_nat(32n, y))
109    == 1n+Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, Word.not(32n, y))) : Nat}
110  W.wsub_val(32n, x, y)
111
112# Numbers
113# =======
114
115law to_nat_lt.m:
116  for +a: U32
117  for +m: Nat
118  for +hm: {Nat.pow(2n, 32n) == m : Nat}
119  {Nat.is_lt(U32.to_nat(a), m) == True{} : Bool}
120
121def to_nat_lt.m(a, m, hm):
122  match a:
123    case U32{+w}:
124      wlt.m(w, m, hm)
125
126law to_nat_lt_p:
127  for +a: U32
128  {Nat.is_lt(U32.to_nat(a), Nat.pow(2n, 32n)) == True{} : Bool}
129
130def to_nat_lt_p(a):
131  to_nat_lt.m(a, Nat.pow(2n, 32n), {==})
132
133law to_nat_inj:
134  for +a: U32
135  for +b: U32
136  for +h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
137  {a == b : U32}
138
139def to_nat_inj(a, b, h):
140  match a b:
141    case U32{+x} U32{+y}:
142      %W.winj(32n, x, y, h) : {U32{x} == U32{_} : U32}
143      {==}
144
145law wrap_small_p:
146  for +n: Nat
147  for +h: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
148  {Nat.mod(n, Nat.pow(2n, 32n)) == n : Nat}
149
150def wrap_small_p(n, h):
151  N.mod_small(n, Nat.pow(2n, 32n), h)
152
153law to_nat_inc.m:
154  for +a: U32
155  for +m: Nat
156  for +hm: {Nat.pow(2n, 32n) == m : Nat}
157  {U32.to_nat(U32.inc(a)) == Nat.mod(Nat.add(U32.to_nat(a), 1n), m) : Nat}
158
159def to_nat_inc.m(a, m, hm):
160  match a:
161    case U32{+w}:
162      %Equal.sym(Nat, Nat.add(Word.to_nat(32n, w), 1n), 1n+Word.to_nat(32n, w), N.add_one(Word.to_nat(32n, w))) :
163        {Word.to_nat(32n, Word.inc(32n, w)) == Nat.mod(_, m) : Nat}
164      Equal.sym(Nat, Nat.mod(1n+Word.to_nat(32n, w), m), Word.to_nat(32n, Word.inc(32n, w)),
165        W.carry_mod(Word.to_nat(32n, Word.inc(32n, w)), N.bn(W.incc(32n, w)), m, 1n+Word.to_nat(32n, w), winc.m(w, m, hm), wlt.m(Word.inc(32n, w), m, hm)))
166
167law to_nat_inc_p:
168  for +a: U32
169  {U32.to_nat(U32.inc(a)) == Nat.mod(Nat.add(U32.to_nat(a), 1n), Nat.pow(2n, 32n)) : Nat}
170
171def to_nat_inc_p(a):
172  to_nat_inc.m(a, Nat.pow(2n, 32n), {==})
173
174law to_nat_from_nat.m:
175  for +n: Nat
176  for +m: Nat
177  for +hm: {Nat.pow(2n, 32n) == m : Nat}
178  {U32.to_nat(U32.from_nat(n)) == Nat.mod(n, m) : Nat}
179
180def to_nat_from_nat.m(n, m, hm):
181  match n:
182    case 0n:
183      Equal.sym(Nat, Nat.mod(0n, m), 0n, N.mod_zero_l(m))
184    case 1n+p:
185      %Equal.sym(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), Nat.mod(Nat.add(U32.to_nat(U32.from_nat(p)), 1n), m), to_nat_inc.m(U32.from_nat(p), m, hm)) :
186        {_ == Nat.mod(1n+p, m) : Nat}
187      %Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), Nat.mod(p, m), to_nat_from_nat.m(p, m, hm)) : {Nat.mod(Nat.add(_, 1n), m) == Nat.mod(1n+p, m) : Nat}
188      %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mod(p, m), 1n), m), Nat.mod(Nat.add(p, 1n), m), N.mod_add_mod_l(p, 1n, m)) : {_ == Nat.mod(1n+p, m) : Nat}
189      %Equal.sym(Nat, Nat.add(p, 1n), 1n+p, N.add_one(p)) : {Nat.mod(_, m) == Nat.mod(1n+p, m) : Nat}
190      {==}
191
192law to_nat_from_nat_p:
193  for +n: Nat
194  {U32.to_nat(U32.from_nat(n)) == Nat.mod(n, Nat.pow(2n, 32n)) : Nat}
195
196def to_nat_from_nat_p(n):
197  to_nat_from_nat.m(n, Nat.pow(2n, 32n), {==})
198
199law from_nat_to_nat.m:
200  for +a: U32
201  for +m: Nat
202  for +hm: {Nat.pow(2n, 32n) == m : Nat}
203  {U32.from_nat(U32.to_nat(a)) == a : U32}
204
205def from_nat_to_nat.m(a, m, hm):
206  to_nat_inj(U32.from_nat(U32.to_nat(a)), a,
207    Equal.trans(Nat, U32.to_nat(U32.from_nat(U32.to_nat(a))), Nat.mod(U32.to_nat(a), m), U32.to_nat(a),
208      to_nat_from_nat.m(U32.to_nat(a), m, hm), N.mod_small(U32.to_nat(a), m, to_nat_lt.m(a, m, hm))))
209
210law from_nat_to_nat:
211  for +a: U32
212  {U32.from_nat(U32.to_nat(a)) == a : U32}
213
214def from_nat_to_nat(a):
215  from_nat_to_nat.m(a, Nat.pow(2n, 32n), {==})
216
217# Comparisons
218# ===========
219
220law cmp_to_nat:
221  for +a: U32
222  for +b: U32
223  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
224
225def cmp_to_nat(a, b):
226  match a b:
227    case U32{+x} U32{+y}:
228      W.wcmp(32n, x, y)
229
230law is_eq_to_nat:
231  for +a: U32
232  for +b: U32
233  {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
234
235def is_eq_to_nat(a, b):
236  Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), cmp_to_nat(a, b))
237
238law is_lt_to_nat:
239  for +a: U32
240  for +b: U32
241  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
242
243def is_lt_to_nat(a, b):
244  Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), cmp_to_nat(a, b))
245
246law is_le_to_nat:
247  for +a: U32
248  for +b: U32
249  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
250
251def is_le_to_nat(a, b):
252  Equal.cong(Cmp, Bool, c => Cmp.is_le(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), cmp_to_nat(a, b))
253
254law is_gt_to_nat:
255  for +a: U32
256  for +b: U32
257  {U32.is_gt(a, b) == Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) : Bool}
258
259def is_gt_to_nat(a, b):
260  Equal.cong(Cmp, Bool, c => Cmp.is_gt(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), cmp_to_nat(a, b))
261
262law is_ge_to_nat:
263  for +a: U32
264  for +b: U32
265  {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}
266
267def is_ge_to_nat(a, b):
268  Equal.cong(Cmp, Bool, c => Cmp.is_ge(c), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), cmp_to_nat(a, b))
269
270law is_ne_to_nat:
271  for +a: U32
272  for +b: U32
273  {U32.is_ne(a, b) == Bool.not(Nat.is_eq(U32.to_nat(a), U32.to_nat(b))) : Bool}
274
275def is_ne_to_nat(a, b):
276  Equal.cong(Cmp, Bool, c => Bool.not(Cmp.is_eq(c)), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), cmp_to_nat(a, b))
277
278law is_zero_to_nat:
279  for +a: U32
280  {U32.is_zero(a) == Nat.is_eq(U32.to_nat(a), 0n) : Bool}
281
282def is_zero_to_nat(a):
283  is_eq_to_nat(a, 0)
284
285law is_eq_true:
286  for +a: U32
287  for +b: U32
288  for +h: {U32.is_eq(a, b) == True{} : Bool}
289  {a == b : U32}
290
291def is_eq_true(a, b, h):
292  to_nat_inj(a, b, N.eq_sound(U32.to_nat(a), U32.to_nat(b),
293    %is_eq_to_nat(a, b) : {_ == True{} : Bool}
294    h))
295
296law fin_eq:
297  for +a: Bool
298  for +b: Bool
299  for +t: Cmp
300  {Cmp.is_eq(Word.cmp.fin(a, b, t)) == Bool.and(Cmp.is_eq(t), Cmp.is_eq(Bool.cmp(a, b))) : Bool}
301
302def fin_eq(a, b, t):
303  match t:
304    case LT{}:
305      {==}
306    case EQ{}:
307      {==}
308    case GT{}:
309      {==}
310
311law xor_bit_eq:
312  for +x: Bool
313  for +y: Bool
314  {Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{})) == Cmp.is_eq(Bool.cmp(x, y)) : Bool}
315
316def xor_bit_eq(x, y):
317  match x y:
318    case False{} False{}:
319      {==}
320    case False{} True{}:
321      {==}
322    case True{} False{}:
323      {==}
324    case True{} True{}:
325      {==}
326
327law wxor_zero:
328  for +n: Nat
329  for +a: Word(n)
330  for +b: Word(n)
331  {Cmp.is_eq(Word.cmp(n, Word.xor(n, a, b), Word.zero(n))) == Cmp.is_eq(Word.cmp(n, a, b)) : Bool}
332
333def wxor_zero(n, a, b):
334  match n:
335    case 0n:
336      match a b:
337        case WNil{} WNil{}:
338          {==}
339    case 1n+p:
340      match a b:
341        case WCon{+x, +at} WCon{+y, +bt}:
342          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(Bool.xor(x, y), False{}, Word.cmp(p, Word.xor(p, at, bt), Word.zero(p)))),
343              Bool.and(Cmp.is_eq(Word.cmp(p, Word.xor(p, at, bt), Word.zero(p))), Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{}))),
344              fin_eq(Bool.xor(x, y), False{}, Word.cmp(p, Word.xor(p, at, bt), Word.zero(p)))) :
345            {_ == Cmp.is_eq(Word.cmp.fin(x, y, Word.cmp(p, at, bt))) : Bool}
346          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(x, y, Word.cmp(p, at, bt))), Bool.and(Cmp.is_eq(Word.cmp(p, at, bt)), Cmp.is_eq(Bool.cmp(x, y))),
347              fin_eq(x, y, Word.cmp(p, at, bt))) :
348            {Bool.and(Cmp.is_eq(Word.cmp(p, Word.xor(p, at, bt), Word.zero(p))), Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{}))) == _ : Bool}
349          %Equal.sym(Bool, Cmp.is_eq(Word.cmp(p, Word.xor(p, at, bt), Word.zero(p))), Cmp.is_eq(Word.cmp(p, at, bt)), wxor_zero(p, at, bt)) :
350            {Bool.and(_, Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{}))) == Bool.and(Cmp.is_eq(Word.cmp(p, at, bt)), Cmp.is_eq(Bool.cmp(x, y))) : Bool}
351          %Equal.sym(Bool, Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{})), Cmp.is_eq(Bool.cmp(x, y)), xor_bit_eq(x, y)) :
352            {Bool.and(Cmp.is_eq(Word.cmp(p, at, bt)), _) == Bool.and(Cmp.is_eq(Word.cmp(p, at, bt)), Cmp.is_eq(Bool.cmp(x, y))) : Bool}
353          {==}
354
355law is_zero_xor:
356  for +a: U32
357  for +b: U32
358  {U32.is_zero(U32.xor(a, b)) == U32.is_eq(a, b) : Bool}
359
360def is_zero_xor(a, b):
361  match a b:
362    case U32{+x} U32{+y}:
363      wxor_zero(32n, x, y)
364
365# Arithmetic modulo 2^32
366# ======================
367
368law to_nat_add.m:
369  for +a: U32
370  for +b: U32
371  for +m: Nat
372  for +hm: {Nat.pow(2n, 32n) == m : Nat}
373  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), m) : Nat}
374
375def to_nat_add.m(a, b, m, hm):
376  match a b:
377    case U32{+x} U32{+y}:
378      Equal.sym(Nat, Nat.mod(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), m), Word.to_nat(32n, Word.adc(32n, x, y, False{}, False{})),
379        W.carry_mod(Word.to_nat(32n, Word.adc(32n, x, y, False{}, False{})), N.bn(W.cout(32n, x, y, False{})), m,
380          Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), wadc.m(x, y, False{}, m, hm), wlt.m(Word.adc(32n, x, y, False{}, False{}), m, hm)))
381
382law to_nat_add_p:
383  for +a: U32
384  for +b: U32
385  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
386
387def to_nat_add_p(a, b):
388  to_nat_add.m(a, b, Nat.pow(2n, 32n), {==})
389
390law to_nat_sub.m:
391  for +a: U32
392  for +b: U32
393  for +m: Nat
394  for +hm: {Nat.pow(2n, 32n) == m : Nat}
395  {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.sub(Nat.add(U32.to_nat(a), m), U32.to_nat(b)), m) : Nat}
396
397def to_nat_sub.m(a, b, m, hm):
398  match a b:
399    case U32{+x} U32{+y}:
400      %Equal.sym(Word(32n), Word.adc(32n, x, y, True{}, True{}), Word.adc(32n, x, Word.not(32n, y), False{}, True{}), W.adc_t(32n, x, y, True{})) :
401        {Word.to_nat(32n, _) == Nat.mod(Nat.sub(Nat.add(Word.to_nat(32n, x), m), Word.to_nat(32n, y)), m) : Nat}
402      %Equal.sym(Nat, Nat.sub(Nat.add(Word.to_nat(32n, x), m), Word.to_nat(32n, y)), 1n+Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, Word.not(32n, y))), wsub_val.m(x, y, m, hm)) :
403        {Word.to_nat(32n, Word.adc(32n, x, Word.not(32n, y), False{}, True{})) == Nat.mod(_, m) : Nat}
404      Equal.sym(Nat, Nat.mod(1n+Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, Word.not(32n, y))), m), Word.to_nat(32n, Word.adc(32n, x, Word.not(32n, y), False{}, True{})),
405        W.carry_mod(Word.to_nat(32n, Word.adc(32n, x, Word.not(32n, y), False{}, True{})), N.bn(W.cout(32n, x, Word.not(32n, y), True{})), m,
406          1n+Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, Word.not(32n, y))),
407          wadc.m(x, Word.not(32n, y), True{}, m, hm), wlt.m(Word.adc(32n, x, Word.not(32n, y), False{}, True{}), m, hm)))
408
409law to_nat_sub_p:
410  for +a: U32
411  for +b: U32
412  {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.sub(Nat.add(U32.to_nat(a), Nat.pow(2n, 32n)), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
413
414def to_nat_sub_p(a, b):
415  to_nat_sub.m(a, b, Nat.pow(2n, 32n), {==})
416
417law to_nat_mul.m:
418  for +a: U32
419  for +b: U32
420  for +m: Nat
421  for +hm: {Nat.pow(2n, 32n) == m : Nat}
422  {U32.to_nat(U32.mul(a, b)) == Nat.mod(Nat.mul(U32.to_nat(a), U32.to_nat(b)), m) : Nat}
423
424def to_nat_mul.m(a, b, m, hm):
425  match a b:
426    case U32{+x} U32{+y}:
427      wmul.m(x, y, m, hm)
428
429law to_nat_mul_p:
430  for +a: U32
431  for +b: U32
432  {U32.to_nat(U32.mul(a, b)) == Nat.mod(Nat.mul(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
433
434def to_nat_mul_p(a, b):
435  to_nat_mul.m(a, b, Nat.pow(2n, 32n), {==})
436
437law from_nat_add.m:
438  for +x: Nat
439  for +y: Nat
440  for +m: Nat
441  for +hm: {Nat.pow(2n, 32n) == m : Nat}
442  {U32.from_nat(Nat.add(x, y)) == U32.add(U32.from_nat(x), U32.from_nat(y)) : U32}
443
444def from_nat_add.m(x, y, m, hm):
445  to_nat_inj(U32.from_nat(Nat.add(x, y)), U32.add(U32.from_nat(x), U32.from_nat(y)),
446    %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.add(x, y))), Nat.mod(Nat.add(x, y), m), to_nat_from_nat.m(Nat.add(x, y), m, hm)) :
447      {_ == U32.to_nat(U32.add(U32.from_nat(x), U32.from_nat(y))) : Nat}
448    %Equal.sym(Nat, U32.to_nat(U32.add(U32.from_nat(x), U32.from_nat(y))), Nat.mod(Nat.add(U32.to_nat(U32.from_nat(x)), U32.to_nat(U32.from_nat(y))), m),
449        to_nat_add.m(U32.from_nat(x), U32.from_nat(y), m, hm)) : {Nat.mod(Nat.add(x, y), m) == _ : Nat}
450    %Equal.sym(Nat, U32.to_nat(U32.from_nat(x)), Nat.mod(x, m), to_nat_from_nat.m(x, m, hm)) :
451      {Nat.mod(Nat.add(x, y), m) == Nat.mod(Nat.add(_, U32.to_nat(U32.from_nat(y))), m) : Nat}
452    %Equal.sym(Nat, U32.to_nat(U32.from_nat(y)), Nat.mod(y, m), to_nat_from_nat.m(y, m, hm)) :
453      {Nat.mod(Nat.add(x, y), m) == Nat.mod(Nat.add(Nat.mod(x, m), _), m) : Nat}
454    %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mod(x, m), Nat.mod(y, m)), m), Nat.mod(Nat.add(x, Nat.mod(y, m)), m), N.mod_add_mod_l(x, Nat.mod(y, m), m)) :
455      {Nat.mod(Nat.add(x, y), m) == _ : Nat}
456    %Equal.sym(Nat, Nat.mod(Nat.add(x, Nat.mod(y, m)), m), Nat.mod(Nat.add(x, y), m), N.mod_add_mod_r(x, y, m)) :
457      {Nat.mod(Nat.add(x, y), m) == _ : Nat}
458    {==})
459
460law from_nat_add:
461  for +x: Nat
462  for +y: Nat
463  {U32.from_nat(Nat.add(x, y)) == U32.add(U32.from_nat(x), U32.from_nat(y)) : U32}
464
465def from_nat_add(x, y):
466  from_nat_add.m(x, y, Nat.pow(2n, 32n), {==})
467
468law from_nat_mul.m:
469  for +x: Nat
470  for +y: Nat
471  for +m: Nat
472  for +hm: {Nat.pow(2n, 32n) == m : Nat}
473  {U32.from_nat(Nat.mul(x, y)) == U32.mul(U32.from_nat(x), U32.from_nat(y)) : U32}
474
475def from_nat_mul.m(x, y, m, hm):
476  to_nat_inj(U32.from_nat(Nat.mul(x, y)), U32.mul(U32.from_nat(x), U32.from_nat(y)),
477    %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mul(x, y))), Nat.mod(Nat.mul(x, y), m), to_nat_from_nat.m(Nat.mul(x, y), m, hm)) :
478      {_ == U32.to_nat(U32.mul(U32.from_nat(x), U32.from_nat(y))) : Nat}
479    %Equal.sym(Nat, U32.to_nat(U32.mul(U32.from_nat(x), U32.from_nat(y))), Nat.mod(Nat.mul(U32.to_nat(U32.from_nat(x)), U32.to_nat(U32.from_nat(y))), m),
480        to_nat_mul.m(U32.from_nat(x), U32.from_nat(y), m, hm)) : {Nat.mod(Nat.mul(x, y), m) == _ : Nat}
481    %Equal.sym(Nat, U32.to_nat(U32.from_nat(x)), Nat.mod(x, m), to_nat_from_nat.m(x, m, hm)) :
482      {Nat.mod(Nat.mul(x, y), m) == Nat.mod(Nat.mul(_, U32.to_nat(U32.from_nat(y))), m) : Nat}
483    %Equal.sym(Nat, U32.to_nat(U32.from_nat(y)), Nat.mod(y, m), to_nat_from_nat.m(y, m, hm)) :
484      {Nat.mod(Nat.mul(x, y), m) == Nat.mod(Nat.mul(Nat.mod(x, m), _), m) : Nat}
485    %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(x, m), Nat.mod(y, m)), m), Nat.mod(Nat.mul(x, Nat.mod(y, m)), m), N.mod_mul_mod_l(x, Nat.mod(y, m), m)) :
486      {Nat.mod(Nat.mul(x, y), m) == _ : Nat}
487    %Equal.sym(Nat, Nat.mod(Nat.mul(x, Nat.mod(y, m)), m), Nat.mod(Nat.mul(x, y), m), N.mod_mul_mod_r(x, y, m)) :
488      {Nat.mod(Nat.mul(x, y), m) == _ : Nat}
489    {==})
490
491law from_nat_mul:
492  for +x: Nat
493  for +y: Nat
494  {U32.from_nat(Nat.mul(x, y)) == U32.mul(U32.from_nat(x), U32.from_nat(y)) : U32}
495
496def from_nat_mul(x, y):
497  from_nat_mul.m(x, y, Nat.pow(2n, 32n), {==})
498
499# Arithmetic when the result fits
500# ===============================
501
502law to_nat_inc_lt.m:
503  for +a: U32
504  for +b: U32
505  for +h: {U32.is_lt(a, b) == True{} : Bool}
506  for +m: Nat
507  for +hm: {Nat.pow(2n, 32n) == m : Nat}
508  {U32.to_nat(U32.inc(a)) == Nat.add(U32.to_nat(a), 1n) : Nat}
509
510def to_nat_inc_lt.m(a, b, h, m, hm):
511  Equal.trans(Nat, U32.to_nat(U32.inc(a)), Nat.mod(Nat.add(U32.to_nat(a), 1n), m), Nat.add(U32.to_nat(a), 1n),
512    to_nat_inc.m(a, m, hm),
513    N.mod_small(Nat.add(U32.to_nat(a), 1n), m,
514      %Equal.sym(Nat, Nat.add(U32.to_nat(a), 1n), 1n+U32.to_nat(a), N.add_one(U32.to_nat(a))) : {Nat.is_lt(_, m) == True{} : Bool}
515      N.le_lt_trans(1n+U32.to_nat(a), U32.to_nat(b), m,
516        %Equal.sym(Bool, Nat.is_le(1n+U32.to_nat(a), U32.to_nat(b)), Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), N.le_succ_lt(U32.to_nat(a), U32.to_nat(b))) : {_ == True{} : Bool}
517        %is_lt_to_nat(a, b) : {_ == True{} : Bool}
518        h,
519        to_nat_lt.m(b, m, hm))))
520
521law to_nat_inc_lt:
522  for +a: U32
523  for +b: U32
524  for +h: {U32.is_lt(a, b) == True{} : Bool}
525  {U32.to_nat(U32.inc(a)) == Nat.add(U32.to_nat(a), 1n) : Nat}
526
527def to_nat_inc_lt(a, b, h):
528  to_nat_inc_lt.m(a, b, h, Nat.pow(2n, 32n), {==})
529
530law to_nat_add_fits_p:
531  for +a: U32
532  for +b: U32
533  for +h: {Nat.is_lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == True{} : Bool}
534  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
535
536def to_nat_add_fits_p(a, b, h):
537  Equal.trans(Nat, U32.to_nat(U32.add(a, b)), Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)), Nat.add(U32.to_nat(a), U32.to_nat(b)),
538    to_nat_add_p(a, b), N.mod_small(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n), h))
539
540law to_nat_mul_fits_p:
541  for +a: U32
542  for +b: U32
543  for +h: {Nat.is_lt(Nat.mul(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == True{} : Bool}
544  {U32.to_nat(U32.mul(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
545
546def to_nat_mul_fits_p(a, b, h):
547  Equal.trans(Nat, U32.to_nat(U32.mul(a, b)), Nat.mod(Nat.mul(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)), Nat.mul(U32.to_nat(a), U32.to_nat(b)),
548    to_nat_mul_p(a, b), N.mod_small(Nat.mul(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n), h))
549
550# (x + m) - y = (x - y) + m for y <= x.
551law sub_add_comm:
552  for +x: Nat
553  for +m: Nat
554  for +y: Nat
555  for +h: {Nat.is_le(y, x) == True{} : Bool}
556  {Nat.sub(Nat.add(x, m), y) == Nat.add(Nat.sub(x, y), m) : Nat}
557
558def sub_add_comm(x, m, y, h):
559  %N.le_sub_add(y, x, h) : {Nat.sub(Nat.add(_, m), y) == Nat.add(Nat.sub(x, y), m) : Nat}
560  %Equal.sym(Nat, Nat.add(Nat.add(y, Nat.sub(x, y)), m), Nat.add(y, Nat.add(Nat.sub(x, y), m)), N.add_assoc(y, Nat.sub(x, y), m)) :
561    {Nat.sub(_, y) == Nat.add(Nat.sub(x, y), m) : Nat}
562  N.sub_add_l(y, Nat.add(Nat.sub(x, y), m))
563
564law sub_le:
565  for +x: Nat
566  for +y: Nat
567  {Nat.is_le(Nat.sub(x, y), x) == True{} : Bool}
568
569def sub_le(x, y):
570  match x y:
571    case 0n _:
572      {==}
573    case 1n+p 0n:
574      N.le_refl(1n+p)
575    case 1n+p 1n+q:
576      N.le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), N.lt_to_le(p, 1n+p, %Equal.sym(Bool, Nat.is_lt(p, 1n+p), Nat.is_le(p, p), N.lt_succ_iff(p, p)) : {_ == True{} : Bool}; N.le_refl(p)))
577
578law mod_add_self:
579  for +d: Nat
580  for +m: Nat
581  {Nat.mod(Nat.add(d, m), m) == Nat.mod(d, m) : Nat}
582
583def mod_add_self(d, m):
584  %Equal.trans(Nat, Nat.add(Nat.mul(1n, m), d), Nat.add(m, d), Nat.add(d, m),
585      Equal.cong(Nat, Nat, t => Nat.add(t, d), Nat.mul(1n, m), m, N.add_zero(m)), N.add_comm(m, d)) :
586    {Nat.mod(_, m) == Nat.mod(d, m) : Nat}
587  N.mod_add_mul(1n, m, d)
588
589law to_nat_sub_le.m:
590  for +a: U32
591  for +b: U32
592  for +h: {U32.is_le(b, a) == True{} : Bool}
593  for +m: Nat
594  for +hm: {Nat.pow(2n, 32n) == m : Nat}
595  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
596
597def to_nat_sub_le.m(a, b, h, m, hm):
598  +x = U32.to_nat(a)
599  +y = U32.to_nat(b)
600  %Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.mod(Nat.sub(Nat.add(x, m), y), m), to_nat_sub.m(a, b, m, hm)) : {_ == Nat.sub(x, y) : Nat}
601  %Equal.sym(Nat, Nat.sub(Nat.add(x, m), y), Nat.add(Nat.sub(x, y), m), sub_add_comm(x, m, y, %is_le_to_nat(b, a) : {_ == True{} : Bool}; h)) : {Nat.mod(_, m) == Nat.sub(x, y) : Nat}
602  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.sub(x, y), m), m), Nat.mod(Nat.sub(x, y), m), mod_add_self(Nat.sub(x, y), m)) : {_ == Nat.sub(x, y) : Nat}
603  N.mod_small(Nat.sub(x, y), m, N.le_lt_trans(Nat.sub(x, y), x, m, sub_le(x, y), to_nat_lt.m(a, m, hm)))
604
605law to_nat_sub_le:
606  for +a: U32
607  for +b: U32
608  for +h: {U32.is_le(b, a) == True{} : Bool}
609  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
610
611def to_nat_sub_le(a, b, h):
612  to_nat_sub_le.m(a, b, h, Nat.pow(2n, 32n), {==})
613
614# Division and remainder
615# ======================
616
617law shl_out:
618  for +n: Nat
619  for +c: Bool
620  for +w: Word(n)
621  {Word.shl.out(n, c, w) == (W.stop(n, c, w), Word.shl.put(n, c, w)) : Bool & Word(n)}
622
623def shl_out(n, c, w):
624  match n:
625    case 0n:
626      match w:
627        case WNil{}:
628          {==}
629    case 1n+p:
630      match w:
631        case WCon{+b, +t}:
632          %Equal.sym(Bool & Word(p), Word.shl.out(p, b, t), (W.stop(p, b, t), Word.shl.put(p, b, t)), shl_out(p, b, t)) :
633            {Word.shl.out.con(p, c, _) == (W.stop(p, b, t), WCon{c, Word.shl.put(p, b, t)}) : Bool & Word(1n+p)}
634          {==}
635
636# What U32.divmod.go(k, a, b) returns: q * b + r = a and r < b.
637def DMOK(k: Nat, A: Nat, B: Nat, qr: Word(k) & U32) -> Type:
638  match qr:
639    case (q, r):
640      Pair({Nat.add(Nat.mul(Word.to_nat(k, q), B), U32.to_nat(r)) == A : Nat}, {Nat.is_lt(U32.to_nat(r), B) == True{} : Bool})
641
642# One step of long division, as numbers (quotient bit 1, then 0).
643law divstep1:
644  for +q: Nat
645  for +b: Nat
646  for +r: Nat
647  for +h: Nat
648  for +a0: Bool
649  for +r2: Nat
650  for +e1: {Nat.add(Nat.mul(q, b), r) == h : Nat}
651  for +e: {Nat.add(b, r2) == Nat.add(N.bn(a0), Nat.double(r)) : Nat}
652  {Nat.add(Nat.mul(1n+Nat.double(q), b), r2) == Nat.add(N.bn(a0), Nat.double(h)) : Nat}
653
654def divstep1(q, b, r, h, a0, r2, e1, e):
655  +x = Nat.mul(Nat.double(q), b)
656  %Equal.trans(Nat, Nat.add(x, Nat.add(b, r2)), Nat.add(b, Nat.add(x, r2)), Nat.add(Nat.add(b, x), r2),
657      Equal.sym(Nat, Nat.add(b, Nat.add(x, r2)), Nat.add(x, Nat.add(b, r2)), N.add_left_comm(b, x, r2)),
658      Equal.sym(Nat, Nat.add(Nat.add(b, x), r2), Nat.add(b, Nat.add(x, r2)), N.add_assoc(b, x, r2))) :
659    {_ == Nat.add(N.bn(a0), Nat.double(h)) : Nat}
660  %Equal.sym(Nat, Nat.add(b, r2), Nat.add(N.bn(a0), Nat.double(r)), e) : {Nat.add(x, _) == Nat.add(N.bn(a0), Nat.double(h)) : Nat}
661  %e1 : {Nat.add(x, Nat.add(N.bn(a0), Nat.double(r))) == Nat.add(N.bn(a0), Nat.double(_)) : Nat}
662  %Equal.sym(Nat, Nat.double(Nat.add(Nat.mul(q, b), r)), Nat.add(Nat.double(Nat.mul(q, b)), Nat.double(r)), N.dbl_dist(Nat.mul(q, b), r)) :
663    {Nat.add(x, Nat.add(N.bn(a0), Nat.double(r))) == Nat.add(N.bn(a0), _) : Nat}
664  %N.mul_dbl_l(q, b) : {Nat.add(x, Nat.add(N.bn(a0), Nat.double(r))) == Nat.add(N.bn(a0), Nat.add(_, Nat.double(r))) : Nat}
665  N.add_left_comm(x, N.bn(a0), Nat.double(r))
666
667law divstep0:
668  for +q: Nat
669  for +b: Nat
670  for +r: Nat
671  for +h: Nat
672  for +a0: Bool
673  for +s: Nat
674  for +e1: {Nat.add(Nat.mul(q, b), r) == h : Nat}
675  for +e: {s == Nat.add(N.bn(a0), Nat.double(r)) : Nat}
676  {Nat.add(Nat.mul(Nat.double(q), b), s) == Nat.add(N.bn(a0), Nat.double(h)) : Nat}
677
678def divstep0(q, b, r, h, a0, s, e1, e):
679  +x = Nat.mul(Nat.double(q), b)
680  %Equal.sym(Nat, s, Nat.add(N.bn(a0), Nat.double(r)), e) : {Nat.add(x, _) == Nat.add(N.bn(a0), Nat.double(h)) : Nat}
681  %e1 : {Nat.add(x, Nat.add(N.bn(a0), Nat.double(r))) == Nat.add(N.bn(a0), Nat.double(_)) : Nat}
682  %Equal.sym(Nat, Nat.double(Nat.add(Nat.mul(q, b), r)), Nat.add(Nat.double(Nat.mul(q, b)), Nat.double(r)), N.dbl_dist(Nat.mul(q, b), r)) :
683    {Nat.add(x, Nat.add(N.bn(a0), Nat.double(r))) == Nat.add(N.bn(a0), _) : Nat}
684  %N.mul_dbl_l(q, b) : {Nat.add(x, Nat.add(N.bn(a0), Nat.double(r))) == Nat.add(N.bn(a0), Nat.add(_, Nat.double(r))) : Nat}
685  N.add_left_comm(x, N.bn(a0), Nat.double(r))
686
687law lt_add_cancel_l:
688  for +c: Nat
689  for +a: Nat
690  for +b: Nat
691  for +h: {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
692  {Nat.is_lt(a, b) == True{} : Bool}
693
694def lt_add_cancel_l(c, a, b, h):
695  match c:
696    case 0n:
697      h
698    case 1n+p:
699      lt_add_cancel_l(p, a, b, h)
700
701# x < 2b and b <= x give x - b < b.
702law sub_lt_dbl:
703  for +x: Nat
704  for +b: Nat
705  for +h1: {Nat.is_lt(x, Nat.double(b)) == True{} : Bool}
706  for +h2: {Nat.is_le(b, x) == True{} : Bool}
707  {Nat.is_lt(Nat.sub(x, b), b) == True{} : Bool}
708
709def sub_lt_dbl(x, b, h1, h2):
710  lt_add_cancel_l(b, Nat.sub(x, b), b,
711    %Equal.sym(Nat, Nat.add(b, Nat.sub(x, b)), x, N.le_sub_add(b, x, h2)) : {Nat.is_lt(_, Nat.add(b, b)) == True{} : Bool}
712    %N.dbl_add(b) : {Nat.is_lt(x, _) == True{} : Bool}
713    h1)
714
715law ge_le:
716  for +x: Nat
717  for +y: Nat
718  {Nat.is_ge(x, y) == Nat.is_le(y, x) : Bool}
719
720def ge_le(x, y):
721  match x y:
722    case 0n 0n:
723      {==}
724    case 0n 1n+q:
725      {==}
726    case 1n+p 0n:
727      {==}
728    case 1n+p 1n+q:
729      ge_le(p, q)
730
731# The quotient bit is 1: the remainder becomes 2r + a0 - b.
732def dm_fin.t(+p: Nat, +q: Word(p), +s: Word(32n), +t: Bool, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +m: Nat,
733  +hm: {Nat.pow(2n, 32n) == m : Nat}, +g: Bool,
734  +eg: {Bool.or(t, U32.is_ge(U32{s}, b)) == g : Bool},
735  +e1: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == Word.to_nat(p, hi) : Nat},
736  +e2: {Nat.is_lt(r, U32.to_nat(b)) == True{} : Bool},
737  +ep: {Nat.add(Word.to_nat(32n, s), Nat.mul(N.bn(t), m)) == Nat.add(N.bn(a0), Nat.double(r)) : Nat}) ->
738  DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), U32.divmod.go.fin(p, q, U32{s}, b, g)):
739  match t g:
740    case True{} True{}:
741      +bb = U32.to_nat(b)
742      +sv = Word.to_nat(32n, s)
743      +rr = Nat.add(N.bn(a0), Nat.double(r))
744      # 2r + a0 = s + m
745      +er = Equal.trans(Nat, rr, Nat.add(sv, Nat.mul(1n, m)), Nat.add(sv, m), Equal.sym(Nat, Nat.add(sv, Nat.mul(1n, m)), rr, ep),
746        Equal.cong(Nat, Nat, z => Nat.add(sv, z), Nat.mul(1n, m), m, N.add_zero(m)))
747      +hle = N.lt_to_le(bb, rr, %Equal.sym(Nat, rr, Nat.add(sv, m), er) : {Nat.is_lt(bb, _) == True{} : Bool}; N.lt_le_trans(bb, m, Nat.add(sv, m), to_nat_lt.m(b, m, hm), N.le_add_l(m, sv)))
748      +hlt = sub_lt_dbl(rr, bb, W.lt_dbl_bit(r, bb, a0, e2), hle)
749      +ev = Equal.trans(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.sub(Nat.add(sv, m), bb), m), Nat.sub(rr, bb),
750        to_nat_sub.m(U32{s}, b, m, hm),
751        %er : {Nat.mod(Nat.sub(_, bb), m) == Nat.sub(rr, bb) : Nat}
752        N.mod_small(Nat.sub(rr, bb), m, N.lt_trans(Nat.sub(rr, bb), bb, m, hlt, to_nat_lt.m(b, m, hm))))
753      (%Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), bb), _) == Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))) : Nat}
754        divstep1(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, Nat.sub(rr, bb), e1, N.le_sub_add(bb, rr, hle)),
755       %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.is_lt(_, bb) == True{} : Bool}; hlt)
756    case True{} False{}:
757      Empty.absurd(DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), (WCon{False{}, q}, U32{s})), N.true_ne_false(eg))
758    case False{} True{}:
759      +bb = U32.to_nat(b)
760      +sv = Word.to_nat(32n, s)
761      +rr = Nat.add(N.bn(a0), Nat.double(r))
762      +er = Equal.trans(Nat, rr, Nat.add(sv, 0n), sv, Equal.sym(Nat, Nat.add(sv, 0n), rr, ep), N.add_zero(sv))
763      +hle = {%Equal.sym(Nat, rr, sv, er) : {Nat.is_le(bb, _) == True{} : Bool}; %ge_le(sv, bb) : {_ == True{} : Bool}; %is_ge_to_nat(U32{s}, b) : {_ == True{} : Bool}; eg :
764        {Nat.is_le(bb, rr) == True{} : Bool}}
765      +hlt = sub_lt_dbl(rr, bb, W.lt_dbl_bit(r, bb, a0, e2), hle)
766      +ev = Equal.trans(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.sub(Nat.add(sv, m), bb), m), Nat.sub(rr, bb),
767        to_nat_sub.m(U32{s}, b, m, hm),
768        %Equal.sym(Nat, rr, sv, er) : {Nat.mod(Nat.sub(Nat.add(sv, m), bb), m) == Nat.sub(_, bb) : Nat}
769        %Equal.sym(Nat, Nat.sub(Nat.add(sv, m), bb), Nat.add(Nat.sub(sv, bb), m), sub_add_comm(sv, m, bb, %er : {Nat.is_le(bb, _) == True{} : Bool}; hle)) :
770          {Nat.mod(_, m) == Nat.sub(sv, bb) : Nat}
771        %Equal.sym(Nat, Nat.mod(Nat.add(Nat.sub(sv, bb), m), m), Nat.mod(Nat.sub(sv, bb), m), mod_add_self(Nat.sub(sv, bb), m)) : {_ == Nat.sub(sv, bb) : Nat}
772        N.mod_small(Nat.sub(sv, bb), m, N.le_lt_trans(Nat.sub(sv, bb), sv, m, sub_le(sv, bb), wlt.m(s, m, hm))))
773      (%Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), bb), _) == Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))) : Nat}
774        divstep1(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, Nat.sub(rr, bb), e1, N.le_sub_add(bb, rr, hle)),
775       %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.is_lt(_, bb) == True{} : Bool}; hlt)
776    case False{} False{}:
777      +bb = U32.to_nat(b)
778      +sv = Word.to_nat(32n, s)
779      +er = Equal.trans(Nat, sv, Nat.add(sv, 0n), Nat.add(N.bn(a0), Nat.double(r)), Equal.sym(Nat, Nat.add(sv, 0n), sv, N.add_zero(sv)), ep)
780      +hlt = N.not_le_lt(bb, sv, %ge_le(sv, bb) : {_ == False{} : Bool}; %is_ge_to_nat(U32{s}, b) : {_ == False{} : Bool}; eg)
781      (divstep0(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, sv, e1, er), hlt)
782
783def dm_rec(+p: Nat, +a0: Bool, +hi: Word(p), +b: U32, +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat},
784  qr: Word(p) & U32, ih: DMOK(p, Word.to_nat(p, hi), U32.to_nat(b), qr)) ->
785  DMOK(1n+p, Word.to_nat(1n+p, WCon{a0, hi}), U32.to_nat(b), U32.divmod.go.rec(p, a0, b, qr)):
786  match qr:
787    case (+q, +r):
788      match r:
789        case U32{+rw}:
790          match ih:
791            case (+e1, +e2):
792              %Equal.sym(Nat, Word.to_nat(1n+p, WCon{a0, hi}), Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), W.wcon(p, a0, hi)) :
793                DMOK(1n+p, _, U32.to_nat(b), U32.divmod.go.rec(p, a0, b, (q, U32{rw})))
794              %Equal.sym(Bool & Word(32n), Word.shl.out(32n, a0, rw), (W.stop(32n, a0, rw), Word.shl.put(32n, a0, rw)), shl_out(32n, a0, rw)) :
795                DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), U32.divmod.go.shl(p, q, b, _))
796              dm_fin.t(p, q, Word.shl.put(32n, a0, rw), W.stop(32n, a0, rw), b, a0, hi, Word.to_nat(32n, rw), m, hm,
797                Bool.or(W.stop(32n, a0, rw), U32.is_ge(U32{Word.shl.put(32n, a0, rw)}, b)), {==}, e1, e2, wput.m(a0, rw, m, hm))
798
799law dm_ok:
800  for +k: Nat
801  for +a: Word(k)
802  for +b: U32
803  for +hb: {Nat.is_lt(0n, U32.to_nat(b)) == True{} : Bool}
804  for +m: Nat
805  for +hm: {Nat.pow(2n, 32n) == m : Nat}
806  DMOK(k, Word.to_nat(k, a), U32.to_nat(b), U32.divmod.go(k, a, b))
807
808def dm_ok(k, a, b, hb, m, hm):
809  match k a:
810    case 0n WNil{}:
811      ({==}, hb)
812    case 1n+p WCon{+a0, +hi}:
813      dm_rec(p, a0, hi, b, m, hm, U32.divmod.go(p, hi, b), dm_ok(p, hi, b, hb, m, hm))
814
815def div_fin_ok(+x: Nat, +y: Nat, qr: Word(32n) & U32, d: DMOK(32n, x, y, qr)) -> {U32.to_nat(U32.div.fin(qr)) == Nat.div(x, y) : Nat}:
816  match qr:
817    case (+q, +r):
818      match d:
819        case (+e1, +e2):
820          %e1 : {Word.to_nat(32n, q) == Nat.div(_, y) : Nat}
821          Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(Word.to_nat(32n, q), y), U32.to_nat(r)), y), Word.to_nat(32n, q), N.div_mul_add(Word.to_nat(32n, q), y, U32.to_nat(r), e2))
822
823def mod_fin_ok(+x: Nat, +y: Nat, qr: Word(32n) & U32, d: DMOK(32n, x, y, qr)) -> {U32.to_nat(U32.mod.fin(qr)) == Nat.mod(x, y) : Nat}:
824  match qr:
825    case (+q, +r):
826      match d:
827        case (+e1, +e2):
828          %e1 : {U32.to_nat(r) == Nat.mod(_, y) : Nat}
829          Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Word.to_nat(32n, q), y), U32.to_nat(r)), y), U32.to_nat(r), N.mod_mul_add(Word.to_nat(32n, q), y, U32.to_nat(r), e2))
830
831law ne_zero_pos:
832  for +y: Nat
833  for +h: {Nat.is_eq(y, 0n) == False{} : Bool}
834  {Nat.is_lt(0n, y) == True{} : Bool}
835
836def ne_zero_pos(y, h):
837  match y:
838    case 0n:
839      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, N.true_ne_false(h))
840    case 1n+p:
841      {==}
842
843def div_if_ok(+x: Word(32n), +y: Word(32n), +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {U32.is_zero(U32{y}) == z : Bool}) ->
844  {U32.to_nat(U32.div.if(x, U32{y}, z)) == Nat.div(Word.to_nat(32n, x), Word.to_nat(32n, y)) : Nat}:
845  match z:
846    case True{}:
847      %Equal.sym(Nat, Word.to_nat(32n, y), 0n, N.eq_sound(Word.to_nat(32n, y), 0n, %is_zero_to_nat(U32{y}) : {_ == True{} : Bool}; ez)) :
848        {0n == Nat.div(Word.to_nat(32n, x), _) : Nat}
849      {==}
850    case False{}:
851      div_fin_ok(Word.to_nat(32n, x), Word.to_nat(32n, y), U32.divmod.go(32n, x, U32{y}),
852        dm_ok(32n, x, U32{y}, ne_zero_pos(Word.to_nat(32n, y), %is_zero_to_nat(U32{y}) : {_ == False{} : Bool}; ez), m, hm))
853
854def mod_if_ok(+x: Word(32n), +y: Word(32n), +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {U32.is_zero(U32{y}) == z : Bool}) ->
855  {U32.to_nat(U32.mod.if(x, U32{y}, z)) == Nat.mod(Word.to_nat(32n, x), Word.to_nat(32n, y)) : Nat}:
856  match z:
857    case True{}:
858      %Equal.sym(Nat, Word.to_nat(32n, y), 0n, N.eq_sound(Word.to_nat(32n, y), 0n, %is_zero_to_nat(U32{y}) : {_ == True{} : Bool}; ez)) :
859        {Word.to_nat(32n, x) == Nat.mod(Word.to_nat(32n, x), _) : Nat}
860      {==}
861    case False{}:
862      mod_fin_ok(Word.to_nat(32n, x), Word.to_nat(32n, y), U32.divmod.go(32n, x, U32{y}),
863        dm_ok(32n, x, U32{y}, ne_zero_pos(Word.to_nat(32n, y), %is_zero_to_nat(U32{y}) : {_ == False{} : Bool}; ez), m, hm))
864
865law to_nat_div:
866  for +a: U32
867  for +b: U32
868  {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}
869
870def to_nat_div(a, b):
871  match a b:
872    case U32{+x} U32{+y}:
873      div_if_ok(x, y, Nat.pow(2n, 32n), {==}, U32.is_zero(U32{y}), {==})
874
875law to_nat_mod:
876  for +a: U32
877  for +b: U32
878  {U32.to_nat(U32.mod(a, b)) == Nat.mod(U32.to_nat(a), U32.to_nat(b)) : Nat}
879
880def to_nat_mod(a, b):
881  match a b:
882    case U32{+x} U32{+y}:
883      mod_if_ok(x, y, Nat.pow(2n, 32n), {==}, U32.is_zero(U32{y}), {==})
884
885# Minimum and maximum
886# ===================
887
888law min_lt:
889  for +x: Nat
890  for +y: Nat
891  for +h: {Nat.is_lt(x, y) == True{} : Bool}
892  {Nat.min(x, y) == x : Nat}
893
894def min_lt(x, y, h):
895  match x y:
896    case 0n _:
897      {==}
898    case 1n+p 0n:
899      Empty.absurd({Nat.min(1n+p, 0n) == 1n+p : Nat}, N.false_ne_true(h))
900    case 1n+p 1n+q:
901      Equal.cong(Nat, Nat, z => 1n+z, Nat.min(p, q), p, min_lt(p, q, h))
902
903law min_nlt:
904  for +x: Nat
905  for +y: Nat
906  for +h: {Nat.is_lt(x, y) == False{} : Bool}
907  {Nat.min(x, y) == y : Nat}
908
909def min_nlt(x, y, h):
910  match x y:
911    case 0n 0n:
912      {==}
913    case 0n 1n+q:
914      Empty.absurd({Nat.min(0n, 1n+q) == 1n+q : Nat}, N.true_ne_false(h))
915    case 1n+p 0n:
916      {==}
917    case 1n+p 1n+q:
918      Equal.cong(Nat, Nat, z => 1n+z, Nat.min(p, q), q, min_nlt(p, q, h))
919
920law max_lt:
921  for +x: Nat
922  for +y: Nat
923  for +h: {Nat.is_lt(x, y) == True{} : Bool}
924  {Nat.max(x, y) == y : Nat}
925
926def max_lt(x, y, h):
927  match x y:
928    case 0n _:
929      {==}
930    case 1n+p 0n:
931      Empty.absurd({Nat.max(1n+p, 0n) == 0n : Nat}, N.false_ne_true(h))
932    case 1n+p 1n+q:
933      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(p, q), q, max_lt(p, q, h))
934
935law max_nlt:
936  for +x: Nat
937  for +y: Nat
938  for +h: {Nat.is_lt(x, y) == False{} : Bool}
939  {Nat.max(x, y) == x : Nat}
940
941def max_nlt(x, y, h):
942  match x y:
943    case 0n 0n:
944      {==}
945    case 0n 1n+q:
946      Empty.absurd({Nat.max(0n, 1n+q) == 0n : Nat}, N.true_ne_false(h))
947    case 1n+p 0n:
948      {==}
949    case 1n+p 1n+q:
950      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(p, q), p, max_nlt(p, q, h))
951
952def min_ok(+a: U32, +b: U32, z: Bool, +ez: {U32.is_lt(a, b) == z : Bool}) ->
953  {U32.to_nat(Bool.pick(U32, z, a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}:
954  match z:
955    case True{}:
956      Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a),
957        min_lt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == True{} : Bool}; ez))
958    case False{}:
959      Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b),
960        min_nlt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == False{} : Bool}; ez))
961
962def max_ok(+a: U32, +b: U32, z: Bool, +ez: {U32.is_lt(a, b) == z : Bool}) ->
963  {U32.to_nat(Bool.pick(U32, z, b, a)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}:
964  match z:
965    case True{}:
966      Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b),
967        max_lt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == True{} : Bool}; ez))
968    case False{}:
969      Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a),
970        max_nlt(U32.to_nat(a), U32.to_nat(b), %is_lt_to_nat(a, b) : {_ == False{} : Bool}; ez))
971
972law to_nat_min:
973  for +a: U32
974  for +b: U32
975  {U32.to_nat(U32.min(a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}
976
977def to_nat_min(a, b):
978  match a b:
979    case U32{+x} U32{+y}:
980      min_ok(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), {==})
981
982law to_nat_max:
983  for +a: U32
984  for +b: U32
985  {U32.to_nat(U32.max(a, b)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}
986
987def to_nat_max(a, b):
988  match a b:
989    case U32{+x} U32{+y}:
990      max_ok(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), {==})
991
992# Shifts
993# ======
994
995law to_nat_shr:
996  for +a: U32
997  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
998
999def to_nat_shr(a):
1000  match a:
1001    case U32{+x}:
1002      W.wshr(32n, x)
1003
1004law to_nat_shl.m:
1005  for +a: U32
1006  for +m: Nat
1007  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1008  {U32.to_nat(U32.shl(a)) == Nat.mod(Nat.mul(U32.to_nat(a), 2n), m) : Nat}
1009
1010def to_nat_shl.m(a, m, hm):
1011  match a:
1012    case U32{+w}:
1013      %Equal.sym(Nat, Nat.mul(Word.to_nat(32n, w), 2n), Nat.double(Word.to_nat(32n, w)), N.mul2_r(Word.to_nat(32n, w))) :
1014        {Word.to_nat(32n, Word.shl(32n, w)) == Nat.mod(_, m) : Nat}
1015      Equal.sym(Nat, Nat.mod(Nat.double(Word.to_nat(32n, w)), m), Word.to_nat(32n, Word.shl(32n, w)),
1016        W.carry_mod(Word.to_nat(32n, Word.shl(32n, w)), N.bn(W.shtop(32n, w)), m, Nat.double(Word.to_nat(32n, w)), wshl.m(w, m, hm), wlt.m(Word.shl(32n, w), m, hm)))
1017
1018law to_nat_shl_p:
1019  for +a: U32
1020  {U32.to_nat(U32.shl(a)) == Nat.mod(Nat.mul(U32.to_nat(a), 2n), Nat.pow(2n, 32n)) : Nat}
1021
1022def to_nat_shl_p(a):
1023  to_nat_shl.m(a, Nat.pow(2n, 32n), {==})
1024
1025law to_nat_shrn:
1026  for +a: U32
1027  for +k: Nat
1028  {U32.to_nat(U32.shrn(a, k)) == Nat.div(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
1029
1030def to_nat_shrn(a, k):
1031  match k:
1032    case 0n:
1033      Equal.sym(Nat, Nat.div(U32.to_nat(a), 1n), U32.to_nat(a), N.div_one(U32.to_nat(a)))
1034    case 1n+p:
1035      +x = U32.to_nat(a)
1036      +pp = Nat.pow(2n, p)
1037      %Equal.sym(Nat, U32.to_nat(U32.shr(U32.shrn(a, p))), Nat.div(U32.to_nat(U32.shrn(a, p)), 2n), to_nat_shr(U32.shrn(a, p))) :
1038        {_ == Nat.div(x, Nat.mul(2n, pp)) : Nat}
1039      %Equal.sym(Nat, U32.to_nat(U32.shrn(a, p)), Nat.div(x, pp), to_nat_shrn(a, p)) : {Nat.div(_, 2n) == Nat.div(x, Nat.mul(2n, pp)) : Nat}
1040      %Equal.sym(Nat, Nat.div(Nat.div(x, pp), 2n), Nat.div(x, Nat.mul(pp, 2n)), N.div_div(x, pp, 2n)) : {_ == Nat.div(x, Nat.mul(2n, pp)) : Nat}
1041      %N.mul_comm(2n, pp) : {Nat.div(x, _) == Nat.div(x, Nat.mul(2n, pp)) : Nat}
1042      {==}
1043
1044law to_nat_shln.m:
1045  for +a: U32
1046  for +k: Nat
1047  for +m: Nat
1048  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1049  {U32.to_nat(U32.shln(a, k)) == Nat.mod(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), m) : Nat}
1050
1051def to_nat_shln.m(a, k, m, hm):
1052  match k:
1053    case 0n:
1054      %Equal.sym(Nat, Nat.mul(U32.to_nat(a), 1n), U32.to_nat(a), N.mul_one(U32.to_nat(a))) : {U32.to_nat(a) == Nat.mod(_, m) : Nat}
1055      Equal.sym(Nat, Nat.mod(U32.to_nat(a), m), U32.to_nat(a), N.mod_small(U32.to_nat(a), m, to_nat_lt.m(a, m, hm)))
1056    case 1n+p:
1057      +x = U32.to_nat(a)
1058      +pp = Nat.pow(2n, p)
1059      %Equal.sym(Nat, U32.to_nat(U32.shl(U32.shln(a, p))), Nat.mod(Nat.mul(U32.to_nat(U32.shln(a, p)), 2n), m), to_nat_shl.m(U32.shln(a, p), m, hm)) :
1060        {_ == Nat.mod(Nat.mul(x, Nat.mul(2n, pp)), m) : Nat}
1061      %Equal.sym(Nat, U32.to_nat(U32.shln(a, p)), Nat.mod(Nat.mul(x, pp), m), to_nat_shln.m(a, p, m, hm)) :
1062        {Nat.mod(Nat.mul(_, 2n), m) == Nat.mod(Nat.mul(x, Nat.mul(2n, pp)), m) : Nat}
1063      %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.mul(x, pp), m), 2n), m), Nat.mod(Nat.mul(Nat.mul(x, pp), 2n), m), N.mod_mul_mod_l(Nat.mul(x, pp), 2n, m)) :
1064        {_ == Nat.mod(Nat.mul(x, Nat.mul(2n, pp)), m) : Nat}
1065      %Equal.sym(Nat, Nat.mul(Nat.mul(x, pp), 2n), Nat.mul(x, Nat.mul(pp, 2n)), N.mul_assoc(x, pp, 2n)) :
1066        {Nat.mod(_, m) == Nat.mod(Nat.mul(x, Nat.mul(2n, pp)), m) : Nat}
1067      %N.mul_comm(2n, pp) : {Nat.mod(Nat.mul(x, _), m) == Nat.mod(Nat.mul(x, Nat.mul(2n, pp)), m) : Nat}
1068      {==}
1069
1070law to_nat_shln_p:
1071  for +a: U32
1072  for +k: Nat
1073  {U32.to_nat(U32.shln(a, k)) == Nat.mod(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) : Nat}
1074
1075def to_nat_shln_p(a, k):
1076  to_nat_shln.m(a, k, Nat.pow(2n, 32n), {==})
1077
1078law to_nat_shln_fits_p:
1079  for +a: U32
1080  for +k: Nat
1081  for +h: {Nat.is_lt(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) == True{} : Bool}
1082  {U32.to_nat(U32.shln(a, k)) == Nat.mul(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
1083
1084def to_nat_shln_fits_p(a, k, h):
1085  Equal.trans(Nat, U32.to_nat(U32.shln(a, k)), Nat.mod(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)), Nat.mul(U32.to_nat(a), Nat.pow(2n, k)),
1086    to_nat_shln_p(a, k), N.mod_small(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n), h))
1087
1088def shln_mod.go(+x: Nat, +k: Nat, +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {Nat.is_le(k, 32n) == z : Bool}) ->
1089  {Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m), Nat.pow(2n, k)) == 0n : Nat}:
1090  match z:
1091    case True{}:
1092      %hm : {Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), _), Nat.pow(2n, k)) == 0n : Nat}
1093      %Equal.sym(Nat, Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), Nat.pow(2n, 32n)), Nat.pow(2n, k)), Nat.mod(Nat.mul(x, Nat.pow(2n, k)), Nat.pow(2n, k)),
1094          N.mod_mod_pow(Nat.mul(x, Nat.pow(2n, k)), k, 32n, ez)) :
1095        {_ == 0n : Nat}
1096      N.mul_mod(x, Nat.pow(2n, k))
1097    case False{}:
1098      +d = Nat.sub(k, 32n)
1099      +pd = Nat.pow(2n, d)
1100      +inner = {
1101        %N.le_sub_add(32n, k, N.lt_to_le(32n, k, N.not_le_lt(k, 32n, ez))) : {Nat.mod(Nat.mul(x, Nat.pow(2n, _)), m) == 0n : Nat}
1102        %Equal.sym(Nat, Nat.pow(2n, Nat.add(32n, d)), Nat.mul(Nat.pow(2n, 32n), pd), N.pow_add(2n, 32n, d)) :
1103          {Nat.mod(Nat.mul(x, _), m) == 0n : Nat}
1104        %Equal.sym(Nat, Nat.pow(2n, 32n), m, hm) : {Nat.mod(Nat.mul(x, Nat.mul(_, pd)), m) == 0n : Nat}
1105        %N.mul_comm(pd, m) : {Nat.mod(Nat.mul(x, _), m) == 0n : Nat}
1106        %N.mul_assoc(x, pd, m) : {Nat.mod(_, m) == 0n : Nat}
1107        N.mul_mod(Nat.mul(x, pd), m) : {Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m) == 0n : Nat}}
1108      %Equal.sym(Nat, Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m), 0n, inner) : {Nat.mod(_, Nat.pow(2n, k)) == 0n : Nat}
1109      N.mod_zero_l(Nat.pow(2n, k))
1110
1111law to_nat_shln_mod.m:
1112  for +a: U32
1113  for +k: Nat
1114  for +m: Nat
1115  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1116  {Nat.mod(U32.to_nat(U32.shln(a, k)), Nat.pow(2n, k)) == 0n : Nat}
1117
1118def to_nat_shln_mod.m(a, k, m, hm):
1119  %Equal.sym(Nat, U32.to_nat(U32.shln(a, k)), Nat.mod(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), m), to_nat_shln.m(a, k, m, hm)) :
1120    {Nat.mod(_, Nat.pow(2n, k)) == 0n : Nat}
1121  shln_mod.go(U32.to_nat(a), k, m, hm, Nat.is_le(k, 32n), {==})
1122
1123law to_nat_shln_mod:
1124  for +a: U32
1125  for +k: Nat
1126  {Nat.mod(U32.to_nat(U32.shln(a, k)), Nat.pow(2n, k)) == 0n : Nat}
1127
1128def to_nat_shln_mod(a, k):
1129  to_nat_shln_mod.m(a, k, Nat.pow(2n, 32n), {==})
1130
1131law to_nat_shrn_lt.m:
1132  for +a: U32
1133  for +k: Nat
1134  for +m: Nat
1135  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1136  {Nat.is_lt(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, Nat.sub(32n, k))) == True{} : Bool}
1137
1138def to_nat_shrn_lt.m(a, k, m, hm):
1139  +x = U32.to_nat(a)
1140  +e = Nat.sub(32n, k)
1141  %Equal.sym(Nat, U32.to_nat(U32.shrn(a, k)), Nat.div(x, Nat.pow(2n, k)), to_nat_shrn(a, k)) : {Nat.is_lt(_, Nat.pow(2n, e)) == True{} : Bool}
1142  N.div_lt(x, Nat.pow(2n, k), Nat.pow(2n, e), N.pow_pos(k),
1143    %N.pow_add(2n, k, e) : {Nat.is_lt(x, _) == True{} : Bool}
1144    N.lt_le_trans(x, m, Nat.pow(2n, Nat.add(k, e)), to_nat_lt.m(a, m, hm),
1145      %hm : {Nat.is_le(_, Nat.pow(2n, Nat.add(k, Nat.sub(32n, k)))) == True{} : Bool}
1146      N.pow_le(32n, Nat.add(k, Nat.sub(32n, k)), N.le_add_sub(32n, k))))
1147
1148law to_nat_shrn_lt:
1149  for +a: U32
1150  for +k: Nat
1151  {Nat.is_lt(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, Nat.sub(32n, k))) == True{} : Bool}
1152
1153def to_nat_shrn_lt(a, k):
1154  to_nat_shrn_lt.m(a, k, Nat.pow(2n, 32n), {==})
1155
1156# Bitwise operations as numbers
1157# =============================
1158
1159law to_nat_and_mask:
1160  for +a: U32
1161  for +m: U32
1162  for +k: Nat
1163  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1164  {U32.to_nat(U32.and(a, m)) == Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
1165
1166def to_nat_and_mask(a, m, k, h):
1167  match a m:
1168    case U32{+x} U32{+y}:
1169      W.and_mask(32n, x, y, k, h)
1170
1171law to_nat_not.m:
1172  for +a: U32
1173  for +m: Nat
1174  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1175  {U32.to_nat(U32.not(a)) == Nat.sub(Nat.sub(m, 1n), U32.to_nat(a)) : Nat}
1176
1177def to_nat_not.m(a, m, hm):
1178  match a:
1179    case U32{+w}:
1180      +x = Word.to_nat(32n, w)
1181      +y = Word.to_nat(32n, Word.not(32n, w))
1182      %wnot.m(w, m, hm) : {y == Nat.sub(Nat.sub(_, 1n), x) : Nat}
1183      %Equal.sym(Nat, Nat.sub(Nat.add(y, x), 0n), Nat.add(y, x), N.sub_zero(Nat.add(y, x))) : {y == Nat.sub(_, x) : Nat}
1184      Equal.sym(Nat, Nat.sub(Nat.add(y, x), x), y, N.sub_add(y, x))
1185
1186law to_nat_not_p:
1187  for +a: U32
1188  {U32.to_nat(U32.not(a)) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(a)) : Nat}
1189
1190def to_nat_not_p(a):
1191  to_nat_not.m(a, Nat.pow(2n, 32n), {==})
1192
1193law to_nat_or_split:
1194  for +a: U32
1195  for +b: U32
1196  for +k: Nat
1197  for +ha: {Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) == 0n : Nat}
1198  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
1199  {U32.to_nat(U32.or(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
1200
1201def to_nat_or_split(a, b, k, ha, hb):
1202  match a b:
1203    case U32{+x} U32{+y}:
1204      W.or_split(32n, x, y, k, ha, hb)
1205
1206law to_nat_xor_split:
1207  for +a: U32
1208  for +b: U32
1209  for +k: Nat
1210  for +ha: {Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) == 0n : Nat}
1211  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
1212  {U32.to_nat(U32.xor(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
1213
1214def to_nat_xor_split(a, b, k, ha, hb):
1215  match a b:
1216    case U32{+x} U32{+y}:
1217      W.xor_split(32n, x, y, k, ha, hb)
1218
1219# Indexes
1220# =======
1221
1222law to_nat_split:
1223  for +a: U32
1224  for +m: U32
1225  for +k: Nat
1226  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1227  {U32.to_nat(a) == Nat.add(Nat.mul(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, k)), U32.to_nat(U32.and(a, m))) : Nat}
1228
1229def to_nat_split(a, m, k, h):
1230  +x = U32.to_nat(a)
1231  +pk = Nat.pow(2n, k)
1232  %Equal.sym(Nat, U32.to_nat(U32.shrn(a, k)), Nat.div(x, pk), to_nat_shrn(a, k)) :
1233    {x == Nat.add(Nat.mul(_, pk), U32.to_nat(U32.and(a, m))) : Nat}
1234  %Equal.sym(Nat, U32.to_nat(U32.and(a, m)), Nat.mod(x, pk), to_nat_and_mask(a, m, k, h)) :
1235    {x == Nat.add(Nat.mul(Nat.div(x, pk), pk), _) : Nat}
1236  Equal.sym(Nat, Nat.add(Nat.mul(Nat.div(x, pk), pk), Nat.mod(x, pk)), x, N.div_mod(x, pk))
1237
1238law shrn_lt_words:
1239  for +i: U32
1240  for +w: U32
1241  for +k: Nat
1242  for +h: {Nat.is_lt(U32.to_nat(i), Nat.mul(Nat.pow(2n, k), U32.to_nat(w))) == True{} : Bool}
1243  {U32.is_lt(U32.shrn(i, k), w) == True{} : Bool}
1244
1245def shrn_lt_words(i, w, k, h):
1246  %Equal.sym(Bool, U32.is_lt(U32.shrn(i, k), w), Nat.is_lt(U32.to_nat(U32.shrn(i, k)), U32.to_nat(w)), is_lt_to_nat(U32.shrn(i, k), w)) :
1247    {_ == True{} : Bool}
1248  %Equal.sym(Nat, U32.to_nat(U32.shrn(i, k)), Nat.div(U32.to_nat(i), Nat.pow(2n, k)), to_nat_shrn(i, k)) :
1249    {Nat.is_lt(_, U32.to_nat(w)) == True{} : Bool}
1250  N.div_lt(U32.to_nat(i), Nat.pow(2n, k), U32.to_nat(w), N.pow_pos(k), h)
1251
1252# Bits
1253# ====
1254
1255law bitw:
1256  for +w: Word(32n)
1257  for +k: Nat
1258  {D.bit(U32{w}, k) == W.wbit(32n, w, k) : Bool}
1259
1260def bitw(w, k):
1261  W.wbit_num(32n, w, k)
1262
1263law bit_and:
1264  for +a: U32
1265  for +b: U32
1266  for +k: Nat
1267  {D.bit(U32.and(a, b), k) == (D.bit(a, k) && D.bit(b, k)) : Bool}
1268
1269def bit_and(a, b, k):
1270  match a b:
1271    case U32{+x} U32{+y}:
1272      %Equal.sym(Bool, D.bit(U32{Word.and(32n, x, y)}, k), W.wbit(32n, Word.and(32n, x, y), k), bitw(Word.and(32n, x, y), k)) :
1273        {_ == Bool.and(D.bit(U32{x}, k), D.bit(U32{y}, k)) : Bool}
1274      %Equal.sym(Bool, D.bit(U32{x}, k), W.wbit(32n, x, k), bitw(x, k)) : {W.wbit(32n, Word.and(32n, x, y), k) == Bool.and(_, D.bit(U32{y}, k)) : Bool}
1275      %Equal.sym(Bool, D.bit(U32{y}, k), W.wbit(32n, y, k), bitw(y, k)) : {W.wbit(32n, Word.and(32n, x, y), k) == Bool.and(W.wbit(32n, x, k), _) : Bool}
1276      W.wbit_and(32n, x, y, k)
1277
1278law bit_or:
1279  for +a: U32
1280  for +b: U32
1281  for +k: Nat
1282  {D.bit(U32.or(a, b), k) == (D.bit(a, k) || D.bit(b, k)) : Bool}
1283
1284def bit_or(a, b, k):
1285  match a b:
1286    case U32{+x} U32{+y}:
1287      %Equal.sym(Bool, D.bit(U32{Word.or(32n, x, y)}, k), W.wbit(32n, Word.or(32n, x, y), k), bitw(Word.or(32n, x, y), k)) :
1288        {_ == Bool.or(D.bit(U32{x}, k), D.bit(U32{y}, k)) : Bool}
1289      %Equal.sym(Bool, D.bit(U32{x}, k), W.wbit(32n, x, k), bitw(x, k)) : {W.wbit(32n, Word.or(32n, x, y), k) == Bool.or(_, D.bit(U32{y}, k)) : Bool}
1290      %Equal.sym(Bool, D.bit(U32{y}, k), W.wbit(32n, y, k), bitw(y, k)) : {W.wbit(32n, Word.or(32n, x, y), k) == Bool.or(W.wbit(32n, x, k), _) : Bool}
1291      W.wbit_or(32n, x, y, k)
1292
1293law bit_xor:
1294  for +a: U32
1295  for +b: U32
1296  for +k: Nat
1297  {D.bit(U32.xor(a, b), k) == Bool.xor(D.bit(a, k), D.bit(b, k)) : Bool}
1298
1299def bit_xor(a, b, k):
1300  match a b:
1301    case U32{+x} U32{+y}:
1302      %Equal.sym(Bool, D.bit(U32{Word.xor(32n, x, y)}, k), W.wbit(32n, Word.xor(32n, x, y), k), bitw(Word.xor(32n, x, y), k)) :
1303        {_ == Bool.xor(D.bit(U32{x}, k), D.bit(U32{y}, k)) : Bool}
1304      %Equal.sym(Bool, D.bit(U32{x}, k), W.wbit(32n, x, k), bitw(x, k)) : {W.wbit(32n, Word.xor(32n, x, y), k) == Bool.xor(_, D.bit(U32{y}, k)) : Bool}
1305      %Equal.sym(Bool, D.bit(U32{y}, k), W.wbit(32n, y, k), bitw(y, k)) : {W.wbit(32n, Word.xor(32n, x, y), k) == Bool.xor(W.wbit(32n, x, k), _) : Bool}
1306      W.wbit_xor(32n, x, y, k)
1307
1308law bit_not:
1309  for +a: U32
1310  for +k: Nat
1311  {D.bit(U32.not(a), k) == (Nat.is_lt(k, 32n) && Bool.not(D.bit(a, k))) : Bool}
1312
1313def bit_not(a, k):
1314  match a:
1315    case U32{+x}:
1316      %Equal.sym(Bool, D.bit(U32{Word.not(32n, x)}, k), W.wbit(32n, Word.not(32n, x), k), bitw(Word.not(32n, x), k)) :
1317        {_ == Bool.and(Nat.is_lt(k, 32n), Bool.not(D.bit(U32{x}, k))) : Bool}
1318      %Equal.sym(Bool, D.bit(U32{x}, k), W.wbit(32n, x, k), bitw(x, k)) : {W.wbit(32n, Word.not(32n, x), k) == Bool.and(Nat.is_lt(k, 32n), Bool.not(_)) : Bool}
1319      W.wbit_not(32n, x, k)
1320
1321law bit_ext:
1322  for +a: U32
1323  for +b: U32
1324  for h: @k: Nat -> {D.bit(a, k) == D.bit(b, k) : Bool}
1325  {a == b : U32}
1326
1327def bit_ext(a, b, h):
1328  match a b:
1329    case U32{+x} U32{+y}:
1330      +d = W.wdiff(32n, x, y)
1331      %W.wext(32n, x, y, Equal.trans(Bool, W.wbit(32n, x, d), D.bit(U32{x}, d), W.wbit(32n, y, d),
1332          Equal.sym(Bool, D.bit(U32{x}, d), W.wbit(32n, x, d), bitw(x, d)),
1333          Equal.trans(Bool, D.bit(U32{x}, d), D.bit(U32{y}, d), W.wbit(32n, y, d), h(d), bitw(y, d)))) :
1334        {U32{x} == U32{_} : U32}
1335      {==}