LAWS.bend

bend-osdev-u32@0.1.0.0 · 734 lines · 108 definitions

1# The arithmetic of Base's Word(n) and U32 as Nat arithmetic, for every
2# width n and every word:
3#
4# * a word's value (Word.to_nat) is below 2^n, and two words with the same
5#   value are the same word;
6# * Word.cmp and U32.cmp are the order of the values (so are U32.is_lt,
7#   is_le, is_eq);
8# * addition is the sum of the values, less 2^n when it wraps, and it wraps
9#   exactly when the result is below the first operand; with a bound on the
10#   sum (no more than another word's value), it does not wrap;
11# * subtraction plus the subtrahend is the minuend, plus 2^n when the
12#   subtrahend is the larger; when it is not, it is the Nat difference;
13# * increment, and a shift left by one bit (or by k bits, for U32), are the
14#   successor and the doubling when the result is bounded by a word's value;
15#   a shift right by one bit halves, rounding down;
16# * the complement of w is 2^n - 1 - w.
17#
18# And laws of the Nat functions they are stated with (u32.bend): 2^n is
19# U32Nat.dbl(n, 1n), and dbl(n, x) = x * 2^n is additive, composes, and
20# keeps the order.
21#
22# A bound is stated as "no more than a word's value" (Nat.is_le(x,
23# U32.to_nat(c))) rather than "below 2^32", because a closed 2^32 is a unary
24# Nat in the checkers (see README.md).
25import Base
26import bend-osdev-u32@0.1.0.0/u32.bend as U
27
28# The Nat functions
29
30law dbl_zero:
31  for +n: Nat
32  {U.U32Nat.dbl(n, 0n) == 0n : Nat}
33
34law dbl_add:
35  for +n: Nat
36  for +x: Nat
37  for +y: Nat
38  {U.U32Nat.dbl(n, Nat.add(x, y)) == Nat.add(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) : Nat}
39
40law dbl_dbl:
41  for +m: Nat
42  for +k: Nat
43  for +x: Nat
44  {U.U32Nat.dbl(m, U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(Nat.add(m, k), x) : Nat}
45
46law dbl_lt:
47  for +n: Nat
48  for +x: Nat
49  for +y: Nat
50  {Nat.is_lt(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) == Nat.is_lt(x, y) : Bool}
51
52law dbl_le:
53  for +n: Nat
54  for +x: Nat
55  for +y: Nat
56  {Nat.is_le(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) == Nat.is_le(x, y) : Bool}
57
58law half_double:
59  for +x: Nat
60  {U.U32Nat.half(Nat.double(x)) == x : Nat}
61
62law half_double_one:
63  for +x: Nat
64  {U.U32Nat.half(1n+Nat.double(x)) == x : Nat}
65
66# Words of any width n
67
68law word_zero_value:
69  for +n: Nat
70  {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
71
72law word_value_lt:
73  for +n: Nat
74  for +w: Word(n)
75  {Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(n, 1n)) == True{} : Bool}
76
77law word_value_eq:
78  for +n: Nat
79  for +a: Word(n)
80  for +b: Word(n)
81  for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
82  {a == b : Word(n)}
83
84law word_cmp_value:
85  for +n: Nat
86  for +a: Word(n)
87  for +b: Word(n)
88  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
89
90law word_not_value:
91  for +n: Nat
92  for +w: Word(n)
93  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == U.U32Nat.dbl(n, 1n) : Nat}
94
95law word_add_wrap:
96  for +n: Nat
97  for +a: Word(n)
98  for +b: Word(n)
99  {Nat.add(Word.to_nat(n, Word.add(n, a, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, a, b), a))))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
100
101law word_add_value:
102  for +n: Nat
103  for +a: Word(n)
104  for +b: Word(n)
105  for +z: Word(n)
106  for h: {Nat.is_le(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Word.to_nat(n, z)) == True{} : Bool}
107  {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
108
109law word_sub_wrap:
110  for +n: Nat
111  for +a: Word(n)
112  for +b: Word(n)
113  {Nat.add(Word.to_nat(n, Word.sub(n, a, b)), Word.to_nat(n, b)) == Nat.add(Word.to_nat(n, a), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, a, b))))) : Nat}
114
115law word_sub_value:
116  for +n: Nat
117  for +a: Word(n)
118  for +b: Word(n)
119  for h: {Nat.is_le(Word.to_nat(n, b), Word.to_nat(n, a)) == True{} : Bool}
120  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
121
122law word_inc_value:
123  for +n: Nat
124  for +w: Word(n)
125  for +z: Word(n)
126  for h: {Nat.is_le(1n+Word.to_nat(n, w), Word.to_nat(n, z)) == True{} : Bool}
127  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
128
129law word_shl_value:
130  for +n: Nat
131  for +w: Word(n)
132  for +z: Word(n)
133  for h: {Nat.is_le(Nat.double(Word.to_nat(n, w)), Word.to_nat(n, z)) == True{} : Bool}
134  {Word.to_nat(n, Word.shl(n, w)) == Nat.double(Word.to_nat(n, w)) : Nat}
135
136law word_shr_value:
137  for +n: Nat
138  for +w: Word(n)
139  {Word.to_nat(n, Word.shr(n, w)) == U.U32Nat.half(Word.to_nat(n, w)) : Nat}
140
141# U32
142
143law u32_cmp_value:
144  for +a: U32
145  for +b: U32
146  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
147
148law u32_lt_value:
149  for +a: U32
150  for +b: U32
151  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
152
153law u32_le_value:
154  for +a: U32
155  for +b: U32
156  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
157
158law u32_eq_value:
159  for +a: U32
160  for +b: U32
161  {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
162
163law u32_value_eq:
164  for +a: U32
165  for +b: U32
166  for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
167  {a == b : U32}
168
169law u32_add_wrap:
170  for +a: U32
171  for +b: U32
172  {Nat.add(U32.to_nat(U32.add(a, b)), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(a, b), a)))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
173
174law u32_add_value:
175  for +a: U32
176  for +b: U32
177  for +c: U32
178  for h: {Nat.is_le(Nat.add(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(c)) == True{} : Bool}
179  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
180
181law u32_sub_wrap:
182  for +a: U32
183  for +b: U32
184  {Nat.add(U32.to_nat(U32.sub(a, b)), U32.to_nat(b)) == Nat.add(U32.to_nat(a), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(a, b)))) : Nat}
185
186law u32_sub_value:
187  for +a: U32
188  for +b: U32
189  for h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}
190  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
191
192law u32_inc_value:
193  for +a: U32
194  for +c: U32
195  for h: {Nat.is_le(1n+U32.to_nat(a), U32.to_nat(c)) == True{} : Bool}
196  {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
197
198law u32_shl_value:
199  for +a: U32
200  for +c: U32
201  for h: {Nat.is_le(Nat.double(U32.to_nat(a)), U32.to_nat(c)) == True{} : Bool}
202  {U32.to_nat(U32.shl(a)) == Nat.double(U32.to_nat(a)) : Nat}
203
204law u32_shln_value:
205  for +a: U32
206  for +k: Nat
207  for +c: U32
208  for +h: {Nat.is_le(U.U32Nat.dbl(k, U32.to_nat(a)), U32.to_nat(c)) == True{} : Bool}
209  {U32.to_nat(U32.shln(a, k)) == U.U32Nat.dbl(k, U32.to_nat(a)) : Nat}
210
211law u32_shr_value:
212  for +a: U32
213  {U32.to_nat(U32.shr(a)) == U.U32Nat.half(U32.to_nat(a)) : Nat}
214
215# Witnesses and vectors
216
217# the bounds can hold, and the wrapping cases happen: 2^32 - 1 + 1 wraps to
218# 0, below the first operand; 0 - 1 borrows
219law u32_wit:
220  {(Nat.is_le(Nat.add(U32.to_nat(3), U32.to_nat(4)), U32.to_nat(7)), U32.is_lt(U32.add(4294967295, 1), 4294967295), U32.is_lt(0, 1), U32.add(4294967295, 1), U32.sub(0, 1)) == (True{}, True{}, True{}, 0, 4294967295) : Bool & Bool & Bool & U32 & U32}
221
222law dbl_vec:
223  {(U.U32Nat.dbl(3n, 5n), U.U32Nat.bit(True{}), U.U32Nat.half(7n)) == (40n, 1n, 3n) : Nat & Nat & Nat}
224
225# Nat arithmetic: the semiring laws, the order as witnesses, the uniqueness
226# of a quotient and remainder, and a sum that cannot wrap. They are what the
227# word laws below are proved from, and what other packages' proofs use for
228# their own Nat arithmetic (scripts/natproof.py writes ring identities from
229# them).
230
231law nat_add_zero:
232  for +x: Nat
233  {Nat.add(x, 0n) == x : Nat}
234
235law nat_add_succ:
236  for +x: Nat
237  for +y: Nat
238  {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}
239
240law nat_add_comm:
241  for +x: Nat
242  for +y: Nat
243  {Nat.add(x, y) == Nat.add(y, x) : Nat}
244
245law nat_add_assoc:
246  for +x: Nat
247  for +y: Nat
248  for +z: Nat
249  {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}
250
251law nat_add_left_comm:
252  for +x: Nat
253  for +y: Nat
254  for +z: Nat
255  {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}
256
257law nat_add_cancel:
258  for +k: Nat
259  for +x: Nat
260  for +y: Nat
261  for e: {Nat.add(k, x) == Nat.add(k, y) : Nat}
262  {x == y : Nat}
263
264law nat_mul_zero:
265  for +x: Nat
266  {Nat.mul(x, 0n) == 0n : Nat}
267
268law nat_mul_one:
269  for +x: Nat
270  {Nat.mul(x, 1n) == x : Nat}
271
272law nat_one_mul:
273  for +x: Nat
274  {Nat.mul(1n, x) == x : Nat}
275
276law nat_mul_succ:
277  for +x: Nat
278  for +y: Nat
279  {Nat.mul(x, 1n+y) == Nat.add(x, Nat.mul(x, y)) : Nat}
280
281law nat_mul_comm:
282  for +x: Nat
283  for +y: Nat
284  {Nat.mul(x, y) == Nat.mul(y, x) : Nat}
285
286law nat_mul_assoc:
287  for +x: Nat
288  for +y: Nat
289  for +z: Nat
290  {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}
291
292law nat_mul_left_comm:
293  for +x: Nat
294  for +y: Nat
295  for +z: Nat
296  {Nat.mul(x, Nat.mul(y, z)) == Nat.mul(y, Nat.mul(x, z)) : Nat}
297
298law nat_mul_add:
299  for +x: Nat
300  for +y: Nat
301  for +z: Nat
302  {Nat.mul(x, Nat.add(y, z)) == Nat.add(Nat.mul(x, y), Nat.mul(x, z)) : Nat}
303
304law nat_add_mul:
305  for +x: Nat
306  for +y: Nat
307  for +z: Nat
308  {Nat.mul(Nat.add(x, y), z) == Nat.add(Nat.mul(x, z), Nat.mul(y, z)) : Nat}
309
310law nat_double:
311  for +x: Nat
312  {Nat.double(x) == Nat.add(x, x) : Nat}
313
314law dbl_comm:
315  for +j: Nat
316  for +k: Nat
317  for +x: Nat
318  {U.U32Nat.dbl(j, U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(k, U.U32Nat.dbl(j, x)) : Nat}
319
320law dbl_mul_l:
321  for +k: Nat
322  for +x: Nat
323  for +y: Nat
324  {Nat.mul(U.U32Nat.dbl(k, x), y) == U.U32Nat.dbl(k, Nat.mul(x, y)) : Nat}
325
326law dbl_mul_r:
327  for +k: Nat
328  for +x: Nat
329  for +y: Nat
330  {Nat.mul(x, U.U32Nat.dbl(k, y)) == U.U32Nat.dbl(k, Nat.mul(x, y)) : Nat}
331
332# the order: x <= y exactly when (y - x) + x = y, and x < y when
333# (y - (1 + x)) + 1 + x = y; and w + 1 + x is never x
334
335law nat_le_refl:
336  for +x: Nat
337  {Nat.is_le(x, x) == True{} : Bool}
338
339law nat_le_add:
340  for +x: Nat
341  for +w: Nat
342  {Nat.is_le(x, Nat.add(w, x)) == True{} : Bool}
343
344law nat_lt_add:
345  for +x: Nat
346  for +w: Nat
347  {Nat.is_lt(x, Nat.add(w, 1n+x)) == True{} : Bool}
348
349law nat_le_witness:
350  for +x: Nat
351  for +y: Nat
352  for h: {Nat.is_le(x, y) == True{} : Bool}
353  {Nat.add(Nat.sub(y, x), x) == y : Nat}
354
355law nat_lt_witness:
356  for +x: Nat
357  for +y: Nat
358  for h: {Nat.is_lt(x, y) == True{} : Bool}
359  {Nat.add(Nat.sub(y, 1n+x), 1n+x) == y : Nat}
360
361law nat_succ_add_absurd:
362  for +w: Nat
363  for +x: Nat
364  for e: {Nat.add(w, 1n+x) == x : Nat}
365  Empty
366
367# a quotient and remainder are unique: q b + r with r < b determines q and r
368
369law nat_div_unique:
370  for +b: Nat
371  for +q1: Nat
372  for +r1: Nat
373  for +q2: Nat
374  for +r2: Nat
375  for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
376  for h1: {Nat.is_lt(r1, b) == True{} : Bool}
377  for h2: {Nat.is_lt(r2, b) == True{} : Bool}
378  {q1 == q2 : Nat}
379
380law nat_mod_unique:
381  for +b: Nat
382  for +q1: Nat
383  for +r1: Nat
384  for +q2: Nat
385  for +r2: Nat
386  for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
387  for h1: {Nat.is_lt(r1, b) == True{} : Bool}
388  for h2: {Nat.is_lt(r2, b) == True{} : Bool}
389  {r1 == r2 : Nat}
390
391# r + 2^n k = p, with p no more than z and z below 2^n: k is 0, and r = p
392# (a sum below 2^n did not wrap)
393
394law dbl_nowrap:
395  for +n: Nat
396  for +k: Nat
397  for +r: Nat
398  for +p: Nat
399  for +z: Nat
400  for e: {Nat.add(r, U.U32Nat.dbl(n, k)) == p : Nat}
401  for h: {Nat.is_le(p, z) == True{} : Bool}
402  for hz: {Nat.is_lt(z, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
403  {r == p : Nat}
404
405# The low k bits of x and the rest (u32.bend): x = low(k, x) + 2^k high(k, x)
406# with low(k, x) below 2^k, and these are the only such pair
407
408law nat_odd_half:
409  for +x: Nat
410  {Nat.add(U.U32Nat.odd(x), Nat.double(U.U32Nat.half(x))) == x : Nat}
411
412law nat_odd_le:
413  for +x: Nat
414  {Nat.is_le(U.U32Nat.odd(x), 1n) == True{} : Bool}
415
416law low_high:
417  for +k: Nat
418  for +x: Nat
419  {Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x))) == x : Nat}
420
421law low_lt:
422  for +k: Nat
423  for +x: Nat
424  {Nat.is_lt(U.U32Nat.low(k, x), U.U32Nat.dbl(k, 1n)) == True{} : Bool}
425
426law low_unique:
427  for +k: Nat
428  for +x: Nat
429  for +r: Nat
430  for +q: Nat
431  for e: {Nat.add(r, U.U32Nat.dbl(k, q)) == x : Nat}
432  for h: {Nat.is_lt(r, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
433  {r == U.U32Nat.low(k, x) : Nat}
434
435law high_unique:
436  for +k: Nat
437  for +x: Nat
438  for +r: Nat
439  for +q: Nat
440  for e: {Nat.add(r, U.U32Nat.dbl(k, q)) == x : Nat}
441  for h: {Nat.is_lt(r, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
442  {q == U.U32Nat.high(k, x) : Nat}
443
444law low_add_dbl:
445  for +k: Nat
446  for +x: Nat
447  for +q: Nat
448  {U.U32Nat.low(k, Nat.add(x, U.U32Nat.dbl(k, q))) == U.U32Nat.low(k, x) : Nat}
449
450law low_small:
451  for +k: Nat
452  for +x: Nat
453  for h: {Nat.is_lt(x, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
454  {U.U32Nat.low(k, x) == x : Nat}
455
456# Multiplication: the product's value is the low n bits of the product of
457# the values; what wraps is 2^n times the rest; with the product no more
458# than a word's value, nothing wraps
459
460law word_mul_wrap:
461  for +n: Nat
462  for +a: Word(n)
463  for +b: Word(n)
464  {Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))))) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
465
466law word_mul_low:
467  for +n: Nat
468  for +a: Word(n)
469  for +b: Word(n)
470  {Word.to_nat(n, Word.mul(n, a, b)) == U.U32Nat.low(n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}
471
472law word_mul_value:
473  for +n: Nat
474  for +a: Word(n)
475  for +b: Word(n)
476  for +z: Word(n)
477  for h: {Nat.is_le(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), Word.to_nat(n, z)) == True{} : Bool}
478  {Word.to_nat(n, Word.mul(n, a, b)) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
479
480law u32_mul_wrap:
481  for +a: U32
482  for +b: U32
483  {Nat.add(U32.to_nat(U32.mul(a, b)), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))))) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
484
485law u32_mul_low:
486  for +a: U32
487  for +b: U32
488  {U32.to_nat(U32.mul(a, b)) == U.U32Nat.low(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))) : Nat}
489
490law u32_mul_value:
491  for +a: U32
492  for +b: U32
493  for +c: U32
494  for h: {Nat.is_le(Nat.mul(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(c)) == True{} : Bool}
495  {U32.to_nat(U32.mul(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
496
497# Division: for b not 0, the quotient and remainder are the Nat ones,
498# a = q b + r with r < b; by 0, the quotient is 0 and the remainder a
499
500law u32_divmod:
501  for +a: U32
502  for +b: U32
503  for h: {U32.is_zero(b) == False{} : Bool}
504  {Nat.add(Nat.mul(U32.to_nat(U32.div(a, b)), U32.to_nat(b)), U32.to_nat(U32.mod(a, b))) == U32.to_nat(a) : Nat}
505
506law u32_mod_lt:
507  for +a: U32
508  for +b: U32
509  for h: {U32.is_zero(b) == False{} : Bool}
510  {Nat.is_lt(U32.to_nat(U32.mod(a, b)), U32.to_nat(b)) == True{} : Bool}
511
512law u32_div_zero:
513  for +a: U32
514  {U32.div(a, 0) == 0 : U32}
515
516law u32_mod_zero:
517  for +a: U32
518  {U32.mod(a, 0) == a : U32}
519
520# The bitwise operations: and, or and xor commute; and + or is the sum of
521# the values, and so is xor + 2 and; an or of a multiple of 2^k and a value
522# below 2^k is their sum; an and with the mask of the low k bits is the low
523# k bits; not is the subtraction from the mask of all n bits
524
525law word_and_comm:
526  for +n: Nat
527  for +a: Word(n)
528  for +b: Word(n)
529  {Word.and(n, a, b) == Word.and(n, b, a) : Word(n)}
530
531law word_or_comm:
532  for +n: Nat
533  for +a: Word(n)
534  for +b: Word(n)
535  {Word.or(n, a, b) == Word.or(n, b, a) : Word(n)}
536
537law word_xor_comm:
538  for +n: Nat
539  for +a: Word(n)
540  for +b: Word(n)
541  {Word.xor(n, a, b) == Word.xor(n, b, a) : Word(n)}
542
543law word_and_or:
544  for +n: Nat
545  for +a: Word(n)
546  for +b: Word(n)
547  {Nat.add(Word.to_nat(n, Word.and(n, a, b)), Word.to_nat(n, Word.or(n, a, b))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
548
549law word_xor_and:
550  for +n: Nat
551  for +a: Word(n)
552  for +b: Word(n)
553  {Nat.add(Word.to_nat(n, Word.xor(n, a, b)), Nat.double(Word.to_nat(n, Word.and(n, a, b)))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
554
555law word_or_split:
556  for +n: Nat
557  for +a: Word(n)
558  for +b: Word(n)
559  for +k: Nat
560  for +q: Nat
561  for e: {Word.to_nat(n, a) == U.U32Nat.dbl(k, q) : Nat}
562  for h: {Nat.is_lt(Word.to_nat(n, b), U.U32Nat.dbl(k, 1n)) == True{} : Bool}
563  {Word.to_nat(n, Word.or(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
564
565law word_mask_value:
566  for +n: Nat
567  for +k: Nat
568  for h: {Nat.is_le(k, n) == True{} : Bool}
569  {1n+Word.to_nat(n, U.U32Word.mask(n, k)) == U.U32Nat.dbl(k, 1n) : Nat}
570
571law word_and_mask:
572  for +n: Nat
573  for +w: Word(n)
574  for +m: Word(n)
575  for +k: Nat
576  for h: {1n+Word.to_nat(n, m) == U.U32Nat.dbl(k, 1n) : Nat}
577  {Word.to_nat(n, Word.and(n, w, m)) == U.U32Nat.low(k, Word.to_nat(n, w)) : Nat}
578
579law word_not_sub:
580  for +n: Nat
581  for +w: Word(n)
582  {Word.not(n, w) == Word.sub(n, U.U32Word.mask(n, n), w) : Word(n)}
583
584law u32_and_comm:
585  for +a: U32
586  for +b: U32
587  {U32.and(a, b) == U32.and(b, a) : U32}
588
589law u32_or_comm:
590  for +a: U32
591  for +b: U32
592  {U32.or(a, b) == U32.or(b, a) : U32}
593
594law u32_xor_comm:
595  for +a: U32
596  for +b: U32
597  {U32.xor(a, b) == U32.xor(b, a) : U32}
598
599law u32_and_or:
600  for +a: U32
601  for +b: U32
602  {Nat.add(U32.to_nat(U32.and(a, b)), U32.to_nat(U32.or(a, b))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
603
604law u32_xor_and:
605  for +a: U32
606  for +b: U32
607  {Nat.add(U32.to_nat(U32.xor(a, b)), Nat.double(U32.to_nat(U32.and(a, b)))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
608
609law u32_or_split:
610  for +a: U32
611  for +b: U32
612  for +k: Nat
613  for +q: Nat
614  for e: {U32.to_nat(a) == U.U32Nat.dbl(k, q) : Nat}
615  for h: {Nat.is_lt(U32.to_nat(b), U.U32Nat.dbl(k, 1n)) == True{} : Bool}
616  {U32.to_nat(U32.or(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
617
618law u32_and_mask:
619  for +a: U32
620  for +m: U32
621  for +k: Nat
622  for h: {1n+U32.to_nat(m) == U.U32Nat.dbl(k, 1n) : Nat}
623  {U32.to_nat(U32.and(a, m)) == U.U32Nat.low(k, U32.to_nat(a)) : Nat}
624
625# the 16-bit mask, written as Base reads it (65535 = U32Word.mask(32, 16))
626law u32_and_65535:
627  for +a: U32
628  {U32.to_nat(U32.and(a, 65535)) == U.U32Nat.low(16n, U32.to_nat(a)) : Nat}
629
630law u32_not_sub:
631  for +a: U32
632  {U32.not(a) == U32.sub(4294967295, a) : U32}
633
634# Shifts by k bits: right, the rest of the value past its low k bits; left,
635# the low 32 bits of the value times 2^k
636
637law u32_shrn_value:
638  for +a: U32
639  for +k: Nat
640  {U32.to_nat(U32.shrn(a, k)) == U.U32Nat.high(k, U32.to_nat(a)) : Nat}
641
642law u32_shln_low:
643  for +a: U32
644  for +k: Nat
645  {U32.to_nat(U32.shln(a, k)) == U.U32Nat.low(32n, U.U32Nat.dbl(k, U32.to_nat(a))) : Nat}
646
647# More of the Nat library: doubling and the low bits, a bound on the rest,
648# order of products and of powers of two
649
650law low_double:
651  for +k: Nat
652  for +x: Nat
653  {U.U32Nat.low(1n+k, Nat.double(x)) == Nat.double(U.U32Nat.low(k, x)) : Nat}
654
655law high_double:
656  for +k: Nat
657  for +x: Nat
658  {U.U32Nat.high(1n+k, Nat.double(x)) == U.U32Nat.high(k, x) : Nat}
659
660# x below 2^(k + j): high(k, x) below 2^j
661law high_lt:
662  for +k: Nat
663  for +j: Nat
664  for +m: Nat
665  for +x: Nat
666  for e: {Nat.add(k, j) == m : Nat}
667  for h: {Nat.is_lt(x, U.U32Nat.dbl(m, 1n)) == True{} : Bool}
668  {Nat.is_lt(U.U32Nat.high(k, x), U.U32Nat.dbl(j, 1n)) == True{} : Bool}
669
670law nat_mul_lt:
671  for +a: Nat
672  for +b: Nat
673  for +c: Nat
674  for +d: Nat
675  for h1: {Nat.is_lt(a, c) == True{} : Bool}
676  for h2: {Nat.is_lt(b, d) == True{} : Bool}
677  {Nat.is_lt(Nat.mul(a, b), Nat.mul(c, d)) == True{} : Bool}
678
679law nat_le_dbl:
680  for +k: Nat
681  for +x: Nat
682  {Nat.is_le(x, U.U32Nat.dbl(k, x)) == True{} : Bool}
683
684law dbl_le_exp:
685  for +j: Nat
686  for +k: Nat
687  for +x: Nat
688  for h: {Nat.is_le(j, k) == True{} : Bool}
689  {Nat.is_le(U.U32Nat.dbl(j, x), U.U32Nat.dbl(k, x)) == True{} : Bool}
690
691# One step of restoring division on n-bit registers (as Base's U32.divmod
692# and bend-osdev-word64's W64.div do it): the remainder r below b < 2^n is
693# shifted left with a bit a coming in, s keeping the low n bits and t the bit
694# going out; if t, or if s is not below b (l false), b is subtracted (g),
695# giving r1 (er: r1 + b = s + 2^n [s < b] when g, r1 = s when not). Then
696# r1 + g b = 2 r + a, and r1 is below b.
697
698law divstep_value:
699  for +n: Nat
700  for +s: Nat
701  for +b: Nat
702  for +r: Nat
703  for +a: Nat
704  for +r1: Nat
705  for +t: Bool
706  for +l: Bool
707  for +g: Bool
708  for e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(t))) == Nat.add(a, Nat.double(r)) : Nat}
709  for el: {Nat.is_lt(s, b) == l : Bool}
710  for eg: {Bool.or(t, Bool.not(l)) == g : Bool}
711  for er: {Nat.add(r1, Nat.mul(U.U32Nat.bit(g), b)) == Nat.add(s, U.U32Nat.dbl(n, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(l)))) : Nat}
712  for ha: {Nat.is_le(a, 1n) == True{} : Bool}
713  for hr: {Nat.is_lt(r, b) == True{} : Bool}
714  for hb: {Nat.is_lt(b, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
715  {Nat.add(r1, Nat.mul(U.U32Nat.bit(g), b)) == Nat.add(a, Nat.double(r)) : Nat}
716
717law divstep_lt:
718  for +n: Nat
719  for +s: Nat
720  for +b: Nat
721  for +r: Nat
722  for +a: Nat
723  for +r1: Nat
724  for +t: Bool
725  for +l: Bool
726  for +g: Bool
727  for e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(t))) == Nat.add(a, Nat.double(r)) : Nat}
728  for el: {Nat.is_lt(s, b) == l : Bool}
729  for eg: {Bool.or(t, Bool.not(l)) == g : Bool}
730  for er: {Nat.add(r1, Nat.mul(U.U32Nat.bit(g), b)) == Nat.add(s, U.U32Nat.dbl(n, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(l)))) : Nat}
731  for ha: {Nat.is_le(a, 1n) == True{} : Bool}
732  for hr: {Nat.is_lt(r, b) == True{} : Bool}
733  for hb: {Nat.is_lt(b, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
734  {Nat.is_lt(r1, b) == True{} : Bool}