LAWS.bend

lawful-words@0.1.0.0 · 589 lines · 83 definitions

1import Base
2import lawful-words@0.1.0.0/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.
17law 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.
22law 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
28law from_nat_to_nat:
29  for a: U32
30  {U32.from_nat(U32.to_nat(a)) == a : U32}
31
32law 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.
37law 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.
47law 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
52law 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
57law 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
62law 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
67law 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
72law 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
77law 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
82law 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.
87law 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.
93law 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
103law 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
107law 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.
113law 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
118law 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
123law 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
128law 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.
138law 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
144law 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
150law 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
156law 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.
167law 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
172law 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
177law 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
182law 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
191law to_nat_shr:
192  for a: U32
193  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
194
195law 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
199law 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
204law 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
209law 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.
216law 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).
222law 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).
232law 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.
240law 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).
255law 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
262law 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.
268law 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
276law 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
288law 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
294law 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
300law 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.
307law 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.
313law 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
323law 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.
329law 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).
339law 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.
349law 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).
362law 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.
376law 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.
381law 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.
391law 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
397law 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
403law 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
409law 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.
416law 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
422law 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
430law 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.
438law 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
446law 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.)
459law 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.
464law 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
473law 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
479law 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
485law 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).
492law 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
497law 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).
504law 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
510law nat_add_comm:
511  for a: Nat
512  for b: Nat
513  {Nat.add(a, b) == Nat.add(b, a) : Nat}
514
515law 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
521law nat_mul_comm:
522  for a: Nat
523  for b: Nat
524  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
525
526law 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
532law 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
538law 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
546law 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.
555law 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.
564law 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
571law 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
578law 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.
584law 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}