1	import Base
2	import ./defs.bend as D
3	
4	# lawful-words: what Base's U32 operations compute, stated as arithmetic on
5	# natural numbers. 2^32 is written Nat.pow(2n, 32n) in every law: Nat is unary,
6	# and a named constant would be unfolded (and evaluated) by the checker. U32.to_nat(a) is the number a word stands for (0 to 2^32-1).
7	# Each law says what an operation does to that number: modulo 2^32 in general,
8	# and exactly when the result fits. Bytes inside a word (D.byte, D.put_byte,
9	# D.pack4) get get/set laws, and a few facts about Nat that Base lacks come
10	# last. Hypotheses are tests written as in code: {U32.is_lt(a, b) == True{}}.
11	
12	# ==========================================================================
13	# Numbers
14	# ==========================================================================
15	
16	# Every word stands for a number below 2^32.
17	law to_nat_lt:
18	  for a: U32
19	  {Nat.is_lt(U32.to_nat(a), Nat.pow(2n, 32n)) == True{} : Bool}
20	
21	# Two words that stand for the same number are the same word.
22	law to_nat_inj:
23	  for a: U32
24	  for b: U32
25	  for h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
26	  {a == b : U32}
27	
28	law from_nat_to_nat:
29	  for a: U32
30	  {U32.from_nat(U32.to_nat(a)) == a : U32}
31	
32	law to_nat_from_nat:
33	  for n: Nat
34	  {U32.to_nat(U32.from_nat(n)) == Nat.mod(n, Nat.pow(2n, 32n)) : Nat}
35	
36	# A number below 2^32 is unchanged by wrapping.
37	law wrap_small:
38	  for n: Nat
39	  for h: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
40	  {Nat.mod(n, Nat.pow(2n, 32n)) == n : Nat}
41	
42	# ==========================================================================
43	# Comparisons
44	# ==========================================================================
45	
46	# Words compare as their numbers; every U32.is_* test follows from this one.
47	law cmp_to_nat:
48	  for a: U32
49	  for b: U32
50	  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
51	
52	law is_eq_to_nat:
53	  for a: U32
54	  for b: U32
55	  {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
56	
57	law is_lt_to_nat:
58	  for a: U32
59	  for b: U32
60	  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
61	
62	law is_le_to_nat:
63	  for a: U32
64	  for b: U32
65	  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
66	
67	law is_gt_to_nat:
68	  for a: U32
69	  for b: U32
70	  {U32.is_gt(a, b) == Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) : Bool}
71	
72	law is_ge_to_nat:
73	  for a: U32
74	  for b: U32
75	  {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}
76	
77	law is_ne_to_nat:
78	  for a: U32
79	  for b: U32
80	  {U32.is_ne(a, b) == Bool.not(Nat.is_eq(U32.to_nat(a), U32.to_nat(b))) : Bool}
81	
82	law is_zero_to_nat:
83	  for a: U32
84	  {U32.is_zero(a) == Nat.is_eq(U32.to_nat(a), 0n) : Bool}
85	
86	# Two words are equal exactly when their xor is zero.
87	law is_zero_xor:
88	  for a: U32
89	  for b: U32
90	  {U32.is_zero(U32.xor(a, b)) == U32.is_eq(a, b) : Bool}
91	
92	# A passed equality test gives equal words.
93	law is_eq_true:
94	  for a: U32
95	  for b: U32
96	  for h: {U32.is_eq(a, b) == True{} : Bool}
97	  {a == b : U32}
98	
99	# ==========================================================================
100	# Arithmetic modulo 2^32
101	# ==========================================================================
102	
103	law to_nat_inc:
104	  for a: U32
105	  {U32.to_nat(U32.inc(a)) == Nat.mod(Nat.add(U32.to_nat(a), 1n), Nat.pow(2n, 32n)) : Nat}
106	
107	law to_nat_add:
108	  for a: U32
109	  for b: U32
110	  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
111	
112	# a - b wraps: it is a + 2^32 - b, modulo 2^32.
113	law to_nat_sub:
114	  for a: U32
115	  for b: U32
116	  {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}
117	
118	law to_nat_mul:
119	  for a: U32
120	  for b: U32
121	  {U32.to_nat(U32.mul(a, b)) == Nat.mod(Nat.mul(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
122	
123	law from_nat_add:
124	  for x: Nat
125	  for y: Nat
126	  {U32.from_nat(Nat.add(x, y)) == U32.add(U32.from_nat(x), U32.from_nat(y)) : U32}
127	
128	law from_nat_mul:
129	  for x: Nat
130	  for y: Nat
131	  {U32.from_nat(Nat.mul(x, y)) == U32.mul(U32.from_nat(x), U32.from_nat(y)) : U32}
132	
133	# ==========================================================================
134	# Arithmetic when the result fits (counters and indexes)
135	# ==========================================================================
136	
137	# A counter below some word steps up by exactly one.
138	law to_nat_inc_lt:
139	  for a: U32
140	  for b: U32
141	  for h: {U32.is_lt(a, b) == True{} : Bool}
142	  {U32.to_nat(U32.inc(a)) == Nat.add(U32.to_nat(a), 1n) : Nat}
143	
144	law to_nat_add_fits:
145	  for a: U32
146	  for b: U32
147	  for h: {Nat.is_lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == True{} : Bool}
148	  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
149	
150	law to_nat_sub_le:
151	  for a: U32
152	  for b: U32
153	  for h: {U32.is_le(b, a) == True{} : Bool}
154	  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
155	
156	law to_nat_mul_fits:
157	  for a: U32
158	  for b: U32
159	  for h: {Nat.is_lt(Nat.mul(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == True{} : Bool}
160	  {U32.to_nat(U32.mul(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
161	
162	# ==========================================================================
163	# Division, remainder, minimum, maximum
164	# ==========================================================================
165	
166	# As in Base, dividing by 0 gives 0 and the remainder is a; so does Nat.
167	law to_nat_div:
168	  for a: U32
169	  for b: U32
170	  {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}
171	
172	law to_nat_mod:
173	  for a: U32
174	  for b: U32
175	  {U32.to_nat(U32.mod(a, b)) == Nat.mod(U32.to_nat(a), U32.to_nat(b)) : Nat}
176	
177	law to_nat_min:
178	  for a: U32
179	  for b: U32
180	  {U32.to_nat(U32.min(a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}
181	
182	law to_nat_max:
183	  for a: U32
184	  for b: U32
185	  {U32.to_nat(U32.max(a, b)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}
186	
187	# ==========================================================================
188	# Shifts (shifting by 32 or more gives 0)
189	# ==========================================================================
190	
191	law to_nat_shr:
192	  for a: U32
193	  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
194	
195	law to_nat_shl:
196	  for a: U32
197	  {U32.to_nat(U32.shl(a)) == Nat.mod(Nat.mul(U32.to_nat(a), 2n), Nat.pow(2n, 32n)) : Nat}
198	
199	law to_nat_shrn:
200	  for a: U32
201	  for k: Nat
202	  {U32.to_nat(U32.shrn(a, k)) == Nat.div(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
203	
204	law to_nat_shln:
205	  for a: U32
206	  for k: Nat
207	  {U32.to_nat(U32.shln(a, k)) == Nat.mod(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) : Nat}
208	
209	law to_nat_shln_fits:
210	  for a: U32
211	  for k: Nat
212	  for h: {Nat.is_lt(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) == True{} : Bool}
213	  {U32.to_nat(U32.shln(a, k)) == Nat.mul(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
214	
215	# A left shift by k leaves the low k bits zero.
216	law to_nat_shln_mod:
217	  for a: U32
218	  for k: Nat
219	  {Nat.mod(U32.to_nat(U32.shln(a, k)), Nat.pow(2n, k)) == 0n : Nat}
220	
221	# A right shift by k leaves a number below 2^(32-k) (below 1 from k = 32 up).
222	law to_nat_shrn_lt:
223	  for a: U32
224	  for k: Nat
225	  {Nat.is_lt(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, Nat.sub(32n, k))) == True{} : Bool}
226	
227	# ==========================================================================
228	# Indexes: a byte index i is word i >> 2, byte i & 3
229	# ==========================================================================
230	
231	# A word splits into its high part (a >> k) and its low k bits (a & m).
232	law to_nat_split:
233	  for a: U32
234	  for m: U32
235	  for k: Nat
236	  for h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
237	  {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}
238	
239	# An index below 2^k * w words-worth has its word index below w.
240	law shrn_lt_words:
241	  for i: U32
242	  for w: U32
243	  for k: Nat
244	  for h: {Nat.is_lt(U32.to_nat(i), Nat.mul(Nat.pow(2n, k), U32.to_nat(w))) == True{} : Bool}
245	  {U32.is_lt(U32.shrn(i, k), w) == True{} : Bool}
246	
247	# ==========================================================================
248	# Bitwise operations as numbers
249	# ==========================================================================
250	
251	# And with a mask of the low k bits takes the number modulo 2^k. The mask is
252	# any word standing for 2^k - 1, so a literal such as 255 or 3 qualifies. No
253	# word stands for 2^k - 1 when k > 32, so in practice k <= 32 (k = 32 is the
254	# all-ones word).
255	law to_nat_and_mask:
256	  for a: U32
257	  for m: U32
258	  for k: Nat
259	  for h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
260	  {U32.to_nat(U32.and(a, m)) == Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
261	
262	law to_nat_not:
263	  for a: U32
264	  {U32.to_nat(U32.not(a)) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(a)) : Nat}
265	
266	# Or of a word with only bits from k up and a word below 2^k is their sum
267	# (no bit in common). Xor likewise.
268	law to_nat_or_split:
269	  for a: U32
270	  for b: U32
271	  for k: Nat
272	  for ha: {Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) == 0n : Nat}
273	  for hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
274	  {U32.to_nat(U32.or(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
275	
276	law to_nat_xor_split:
277	  for a: U32
278	  for b: U32
279	  for k: Nat
280	  for ha: {Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) == 0n : Nat}
281	  for hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
282	  {U32.to_nat(U32.xor(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
283	
284	# ==========================================================================
285	# Bitwise operations bit by bit
286	# ==========================================================================
287	
288	law bit_and:
289	  for a: U32
290	  for b: U32
291	  for k: Nat
292	  {D.bit(U32.and(a, b), k) == (D.bit(a, k) && D.bit(b, k)) : Bool}
293	
294	law bit_or:
295	  for a: U32
296	  for b: U32
297	  for k: Nat
298	  {D.bit(U32.or(a, b), k) == (D.bit(a, k) || D.bit(b, k)) : Bool}
299	
300	law bit_xor:
301	  for a: U32
302	  for b: U32
303	  for k: Nat
304	  {D.bit(U32.xor(a, b), k) == Bool.xor(D.bit(a, k), D.bit(b, k)) : Bool}
305	
306	# not flips the 32 bits, and only those.
307	law bit_not:
308	  for a: U32
309	  for k: Nat
310	  {D.bit(U32.not(a), k) == (Nat.is_lt(k, 32n) && Bool.not(D.bit(a, k))) : Bool}
311	
312	# Two words with the same bits are the same word.
313	law bit_ext:
314	  for a: U32
315	  for b: U32
316	  for h: @k: Nat -> {D.bit(a, k) == D.bit(b, k) : Bool}
317	  {a == b : U32}
318	
319	# ==========================================================================
320	# Bytes in a word
321	# ==========================================================================
322	
323	law to_nat_byte:
324	  for w: U32
325	  for j: Nat
326	  {U32.to_nat(D.byte(w, j)) == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, Nat.mul(8n, j))), Nat.pow(2n, 8n)) : Nat}
327	
328	# Byte j of a word whose byte j was set to b (below 256) is b.
329	law byte_put_same:
330	  for w: U32
331	  for j: Nat
332	  for b: U32
333	  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
334	  for hb: {U32.is_lt(b, 256) == True{} : Bool}
335	  {D.byte(D.put_byte(w, j, b), j) == b : U32}
336	
337	# Setting byte j leaves every other byte as it was (from j = 4 up,
338	# put_byte changes nothing).
339	law byte_put_other:
340	  for w: U32
341	  for i: Nat
342	  for j: Nat
343	  for b: U32
344	  for hb: {U32.is_lt(b, 256) == True{} : Bool}
345	  for hij: {Nat.is_eq(i, j) == False{} : Bool}
346	  {D.byte(D.put_byte(w, j, b), i) == D.byte(w, i) : U32}
347	
348	# The number a packed word stands for.
349	law to_nat_pack4:
350	  for b0: U32
351	  for b1: U32
352	  for b2: U32
353	  for b3: U32
354	  for h0: {U32.is_lt(b0, 256) == True{} : Bool}
355	  for h1: {U32.is_lt(b1, 256) == True{} : Bool}
356	  for h2: {U32.is_lt(b2, 256) == True{} : Bool}
357	  for h3: {U32.is_lt(b3, 256) == True{} : Bool}
358	  {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), Nat.pow(2n, 16n)), Nat.mul(U32.to_nat(b3), Nat.pow(2n, 24n))))) : Nat}
359	
360	# Unpacking a packed word gives its bytes back. j is any index below 4 (in
361	# code it is i & 3, not a literal).
362	law byte_pack4:
363	  for b0: U32
364	  for b1: U32
365	  for b2: U32
366	  for b3: U32
367	  for j: Nat
368	  for h0: {U32.is_lt(b0, 256) == True{} : Bool}
369	  for h1: {U32.is_lt(b1, 256) == True{} : Bool}
370	  for h2: {U32.is_lt(b2, 256) == True{} : Bool}
371	  for h3: {U32.is_lt(b3, 256) == True{} : Bool}
372	  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
373	  {D.byte(D.pack4(b0, b1, b2, b3), j) == D.nth4(j, b0, b1, b2, b3) : U32}
374	
375	# Packing a word's four bytes gives the word back.
376	law pack4_bytes:
377	  for w: U32
378	  {D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == w : U32}
379	
380	# Two words with the same four bytes are the same word.
381	law byte_ext:
382	  for a: U32
383	  for b: U32
384	  for h0: {D.byte(a, 0n) == D.byte(b, 0n) : U32}
385	  for h1: {D.byte(a, 1n) == D.byte(b, 1n) : U32}
386	  for h2: {D.byte(a, 2n) == D.byte(b, 2n) : U32}
387	  for h3: {D.byte(a, 3n) == D.byte(b, 3n) : U32}
388	  {a == b : U32}
389	
390	# Bitwise operations work byte by byte.
391	law byte_and:
392	  for a: U32
393	  for b: U32
394	  for j: Nat
395	  {D.byte(U32.and(a, b), j) == U32.and(D.byte(a, j), D.byte(b, j)) : U32}
396	
397	law byte_or:
398	  for a: U32
399	  for b: U32
400	  for j: Nat
401	  {D.byte(U32.or(a, b), j) == U32.or(D.byte(a, j), D.byte(b, j)) : U32}
402	
403	law byte_xor:
404	  for a: U32
405	  for b: U32
406	  for j: Nat
407	  {D.byte(U32.xor(a, b), j) == U32.xor(D.byte(a, j), D.byte(b, j)) : U32}
408	
409	law byte_not:
410	  for a: U32
411	  for j: Nat
412	  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
413	  {D.byte(U32.not(a), j) == U32.xor(D.byte(a, j), 255) : U32}
414	
415	# Shifting by whole bytes moves bytes.
416	law byte_shrn:
417	  for w: U32
418	  for s: Nat
419	  for j: Nat
420	  {D.byte(U32.shrn(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.add(j, s)) : U32}
421	
422	law byte_shln_high:
423	  for w: U32
424	  for s: Nat
425	  for j: Nat
426	  for hs: {Nat.is_le(s, j) == True{} : Bool}
427	  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
428	  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.sub(j, s)) : U32}
429	
430	law byte_shln_low:
431	  for w: U32
432	  for s: Nat
433	  for j: Nat
434	  for hj: {Nat.is_lt(j, s) == True{} : Bool}
435	  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == 0 : U32}
436	
437	# A word read r bytes into the pair (lo, hi): bytes r.. of lo, then bytes of hi.
438	law byte_merge_lo:
439	  for lo: U32
440	  for hi: U32
441	  for r: Nat
442	  for j: Nat
443	  for h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}
444	  {D.byte(D.merge(lo, hi, r), j) == D.byte(lo, Nat.add(j, r)) : U32}
445	
446	law byte_merge_hi:
447	  for lo: U32
448	  for hi: U32
449	  for r: Nat
450	  for j: Nat
451	  for hr: {Nat.is_le(r, 4n) == True{} : Bool}
452	  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
453	  for h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}
454	  {D.byte(D.merge(lo, hi, r), j) == D.byte(hi, Nat.sub(Nat.add(j, r), 4n)) : U32}
455	
456	# The zero-byte test: zb(v) is zero exactly when no byte of v is zero. (Only
457	# this whole-word statement holds: a flag above a zero byte can be set even
458	# though that byte is not zero, e.g. v = 0x01010100 flags all four bytes.)
459	law zb_zero:
460	  for v: U32
461	  {U32.is_zero(D.zb(v)) == (U32.is_ne(D.byte(v, 0n), 0) && (U32.is_ne(D.byte(v, 1n), 0) && (U32.is_ne(D.byte(v, 2n), 0) && U32.is_ne(D.byte(v, 3n), 0)))) : Bool}
462	
463	# Every byte is below 256.
464	law byte_lt:
465	  for w: U32
466	  for j: Nat
467	  {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}
468	
469	# ==========================================================================
470	# Facts about Nat that Base does not have
471	# ==========================================================================
472	
473	law nat_mod_lt:
474	  for a: Nat
475	  for b: Nat
476	  for h: {Nat.is_lt(0n, b) == True{} : Bool}
477	  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}
478	
479	law nat_mod_small:
480	  for a: Nat
481	  for b: Nat
482	  for h: {Nat.is_lt(a, b) == True{} : Bool}
483	  {Nat.mod(a, b) == a : Nat}
484	
485	law nat_div_small:
486	  for a: Nat
487	  for b: Nat
488	  for h: {Nat.is_lt(a, b) == True{} : Bool}
489	  {Nat.div(a, b) == 0n : Nat}
490	
491	# a = (a / b) * b + a % b (also for b = 0: a / 0 = 0 and a % 0 = a).
492	law nat_div_mod:
493	  for a: Nat
494	  for b: Nat
495	  {Nat.add(Nat.mul(Nat.div(a, b), b), Nat.mod(a, b)) == a : Nat}
496	
497	law nat_pow_add:
498	  for b: Nat
499	  for j: Nat
500	  for k: Nat
501	  {Nat.pow(b, Nat.add(j, k)) == Nat.mul(Nat.pow(b, j), Nat.pow(b, k)) : Nat}
502	
503	# Dividing by 2^j then by 2^k is dividing by 2^(j+k).
504	law nat_div_div:
505	  for a: Nat
506	  for x: Nat
507	  for y: Nat
508	  {Nat.div(Nat.div(a, x), y) == Nat.div(a, Nat.mul(x, y)) : Nat}
509	
510	law nat_add_comm:
511	  for a: Nat
512	  for b: Nat
513	  {Nat.add(a, b) == Nat.add(b, a) : Nat}
514	
515	law nat_add_assoc:
516	  for a: Nat
517	  for b: Nat
518	  for c: Nat
519	  {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
520	
521	law nat_mul_comm:
522	  for a: Nat
523	  for b: Nat
524	  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
525	
526	law nat_mul_assoc:
527	  for a: Nat
528	  for b: Nat
529	  for c: Nat
530	  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
531	
532	law nat_mul_add:
533	  for a: Nat
534	  for b: Nat
535	  for c: Nat
536	  {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
537	
538	law nat_lt_le_trans:
539	  for a: Nat
540	  for b: Nat
541	  for c: Nat
542	  for h1: {Nat.is_lt(a, b) == True{} : Bool}
543	  for h2: {Nat.is_le(b, c) == True{} : Bool}
544	  {Nat.is_lt(a, c) == True{} : Bool}
545	
546	law nat_le_trans:
547	  for a: Nat
548	  for b: Nat
549	  for c: Nat
550	  for h1: {Nat.is_le(a, b) == True{} : Bool}
551	  for h2: {Nat.is_le(b, c) == True{} : Bool}
552	  {Nat.is_le(a, c) == True{} : Bool}
553	
554	# a < b * c with b > 0 gives a / b < c.
555	law nat_div_lt:
556	  for a: Nat
557	  for b: Nat
558	  for c: Nat
559	  for hb: {Nat.is_lt(0n, b) == True{} : Bool}
560	  for h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool}
561	  {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}
562	
563	# (q * b + r) / b = q and (q * b + r) % b = r, for r < b.
564	law nat_div_mul_add:
565	  for q: Nat
566	  for b: Nat
567	  for r: Nat
568	  for h: {Nat.is_lt(r, b) == True{} : Bool}
569	  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}
570	
571	law nat_mod_mul_add:
572	  for q: Nat
573	  for b: Nat
574	  for r: Nat
575	  for h: {Nat.is_lt(r, b) == True{} : Bool}
576	  {Nat.mod(Nat.add(Nat.mul(q, b), r), b) == r : Nat}
577	
578	law nat_mul_mod:
579	  for a: Nat
580	  for b: Nat
581	  {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}
582	
583	# (a % 2^m) % 2^k = a % 2^k for k <= m.
584	law nat_mod_mod_pow:
585	  for a: Nat
586	  for k: Nat
587	  for m: Nat
588	  for h: {Nat.is_le(k, m) == True{} : Bool}
589	  {Nat.mod(Nat.mod(a, Nat.pow(2n, m)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}