1	import Base
2	import ./proof_nat.bend as N
3	import ./proof_word.bend as W
4	import ./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	
19	law 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	
25	def wlt.m(w, m, hm):
26	  %hm : {Nat.is_lt(Word.to_nat(32n, w), _) == True{} : Bool}
27	  W.wlt(32n, w)
28	
29	law 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	
35	def 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	
39	law 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	
48	def 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	
53	law 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	
59	def 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	
63	law 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	
69	def 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	
73	law 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	
81	def 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	
86	law 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	
94	def 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	
99	law 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	
107	def 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	
115	law 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	
121	def to_nat_lt.m(a, m, hm):
122	  match a:
123	    case U32{+w}:
124	      wlt.m(w, m, hm)
125	
126	law to_nat_lt_p:
127	  for +a: U32
128	  {Nat.is_lt(U32.to_nat(a), Nat.pow(2n, 32n)) == True{} : Bool}
129	
130	def to_nat_lt_p(a):
131	  to_nat_lt.m(a, Nat.pow(2n, 32n), {==})
132	
133	law 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	
139	def 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	
145	law 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	
150	def wrap_small_p(n, h):
151	  N.mod_small(n, Nat.pow(2n, 32n), h)
152	
153	law 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	
159	def 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	
167	law 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	
171	def to_nat_inc_p(a):
172	  to_nat_inc.m(a, Nat.pow(2n, 32n), {==})
173	
174	law 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	
180	def 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	
192	law 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	
196	def to_nat_from_nat_p(n):
197	  to_nat_from_nat.m(n, Nat.pow(2n, 32n), {==})
198	
199	law 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	
205	def 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	
210	law from_nat_to_nat:
211	  for +a: U32
212	  {U32.from_nat(U32.to_nat(a)) == a : U32}
213	
214	def from_nat_to_nat(a):
215	  from_nat_to_nat.m(a, Nat.pow(2n, 32n), {==})
216	
217	# Comparisons
218	# ===========
219	
220	law 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	
225	def cmp_to_nat(a, b):
226	  match a b:
227	    case U32{+x} U32{+y}:
228	      W.wcmp(32n, x, y)
229	
230	law 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	
235	def 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	
238	law 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	
243	def 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	
246	law 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	
251	def 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	
254	law 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	
259	def 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	
262	law 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	
267	def 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	
270	law 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	
275	def 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	
278	law is_zero_to_nat:
279	  for +a: U32
280	  {U32.is_zero(a) == Nat.is_eq(U32.to_nat(a), 0n) : Bool}
281	
282	def is_zero_to_nat(a):
283	  is_eq_to_nat(a, 0)
284	
285	law 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	
291	def 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	
296	law 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	
302	def fin_eq(a, b, t):
303	  match t:
304	    case LT{}:
305	      {==}
306	    case EQ{}:
307	      {==}
308	    case GT{}:
309	      {==}
310	
311	law 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	
316	def 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	
327	law 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	
333	def 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	
355	law 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	
360	def 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	
368	law 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	
375	def 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	
382	law 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	
387	def to_nat_add_p(a, b):
388	  to_nat_add.m(a, b, Nat.pow(2n, 32n), {==})
389	
390	law 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	
397	def 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	
409	law 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	
414	def to_nat_sub_p(a, b):
415	  to_nat_sub.m(a, b, Nat.pow(2n, 32n), {==})
416	
417	law 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	
424	def 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	
429	law 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	
434	def to_nat_mul_p(a, b):
435	  to_nat_mul.m(a, b, Nat.pow(2n, 32n), {==})
436	
437	law 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	
444	def 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	
460	law 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	
465	def from_nat_add(x, y):
466	  from_nat_add.m(x, y, Nat.pow(2n, 32n), {==})
467	
468	law 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	
475	def 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	
491	law 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	
496	def 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	
502	law 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	
510	def 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	
521	law 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	
527	def to_nat_inc_lt(a, b, h):
528	  to_nat_inc_lt.m(a, b, h, Nat.pow(2n, 32n), {==})
529	
530	law 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	
536	def 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	
540	law 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	
546	def 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.
551	law 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	
558	def 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	
564	law sub_le:
565	  for +x: Nat
566	  for +y: Nat
567	  {Nat.is_le(Nat.sub(x, y), x) == True{} : Bool}
568	
569	def 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	
578	law 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	
583	def 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	
589	law 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	
597	def 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	
605	law 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	
611	def 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	
617	law 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	
623	def 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.
637	def 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).
643	law 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	
654	def 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	
667	law 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	
678	def 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	
687	law 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	
694	def 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.
702	law 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	
709	def 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	
715	law ge_le:
716	  for +x: Nat
717	  for +y: Nat
718	  {Nat.is_ge(x, y) == Nat.is_le(y, x) : Bool}
719	
720	def 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.
732	def 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	
783	def 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	
799	law 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	
808	def 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	
815	def 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	
823	def 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	
831	law 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	
836	def 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	
843	def 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	
854	def 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	
865	law 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	
870	def 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	
875	law 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	
880	def 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	
888	law 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	
894	def 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	
903	law 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	
909	def 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	
920	law 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	
926	def 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	
935	law 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	
941	def 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	
952	def 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	
962	def 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	
972	law 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	
977	def 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	
982	law 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	
987	def 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	
995	law to_nat_shr:
996	  for +a: U32
997	  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
998	
999	def to_nat_shr(a):
1000	  match a:
1001	    case U32{+x}:
1002	      W.wshr(32n, x)
1003	
1004	law 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	
1010	def 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	
1018	law 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	
1022	def to_nat_shl_p(a):
1023	  to_nat_shl.m(a, Nat.pow(2n, 32n), {==})
1024	
1025	law 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	
1030	def 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	
1044	law 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	
1051	def 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	
1070	law 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	
1075	def to_nat_shln_p(a, k):
1076	  to_nat_shln.m(a, k, Nat.pow(2n, 32n), {==})
1077	
1078	law 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	
1084	def 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	
1088	def 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	
1111	law 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	
1118	def 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	
1123	law 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	
1128	def to_nat_shln_mod(a, k):
1129	  to_nat_shln_mod.m(a, k, Nat.pow(2n, 32n), {==})
1130	
1131	law 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	
1138	def 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	
1148	law 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	
1153	def 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	
1159	law 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	
1166	def 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	
1171	law 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	
1177	def 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	
1186	law 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	
1190	def to_nat_not_p(a):
1191	  to_nat_not.m(a, Nat.pow(2n, 32n), {==})
1192	
1193	law 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	
1201	def 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	
1206	law 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	
1214	def 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	
1222	law 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	
1229	def 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	
1238	law 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	
1245	def 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	
1255	law bitw:
1256	  for +w: Word(32n)
1257	  for +k: Nat
1258	  {D.bit(U32{w}, k) == W.wbit(32n, w, k) : Bool}
1259	
1260	def bitw(w, k):
1261	  W.wbit_num(32n, w, k)
1262	
1263	law 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	
1269	def 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	
1278	law 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	
1284	def 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	
1293	law 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	
1299	def 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	
1308	law 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	
1313	def 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	
1321	law 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	
1327	def 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	      {==}