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