proof_words.bend

lawful-arrays@0.1.0.0 · 96 lines · 10 definitions

1import Base
2import lawful-words@0.1.0.0/proof_nat.bend as WN
3import lawful-words@0.1.0.0/proof_u32.bend as WU
4
5# The U32 and Nat facts the index proofs need, from lawful-words (BendHub), where
6# they are laws (proof_u32.bend and proof_nat.bend restate them with every
7# variable reusable). w_shln_fits is to_nat_shln_fits with 2^32 written as
8# Nat.pow(2n, 32n): the law's D.two32() cannot be checked (lawful-words
9# notes/proof.md).
10
11law w_shr:
12  for +a: U32
13  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}
14
15def w_shr(a):
16  WU.to_nat_shr(a)
17
18law w_lt:
19  for +a: U32
20  for +b: U32
21  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
22
23def w_lt(a, b):
24  WU.is_lt_to_nat(a, b)
25
26law w_le:
27  for +a: U32
28  for +b: U32
29  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
30
31def w_le(a, b):
32  WU.is_le_to_nat(a, b)
33
34law w_sub_le:
35  for +a: U32
36  for +b: U32
37  for +h: {U32.is_le(b, a) == True{} : Bool}
38  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
39
40def w_sub_le(a, b, h):
41  WU.to_nat_sub_le(a, b, h)
42
43law w_and_mask:
44  for +a: U32
45  for +m: U32
46  for +k: Nat
47  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
48  {U32.to_nat(U32.and(a, m)) == Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
49
50def w_and_mask(a, m, k, h):
51  WU.to_nat_and_mask(a, m, k, h)
52
53law w_shln_fits:
54  for +a: U32
55  for +k: Nat
56  for +h: {Nat.is_lt(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) == True{} : Bool}
57  {U32.to_nat(U32.shln(a, k)) == Nat.mul(U32.to_nat(a), Nat.pow(2n, k)) : Nat}
58
59def w_shln_fits(a, k, h):
60  WU.to_nat_shln_fits_p(a, k, h)
61
62law n_mod_lt:
63  for +a: Nat
64  for +b: Nat
65  for +h: {Nat.is_lt(0n, b) == True{} : Bool}
66  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}
67
68def n_mod_lt(a, b, h):
69  WN.mod_lt(a, b, h)
70
71law n_mod_small:
72  for +a: Nat
73  for +b: Nat
74  for +h: {Nat.is_lt(a, b) == True{} : Bool}
75  {Nat.mod(a, b) == a : Nat}
76
77def n_mod_small(a, b, h):
78  WN.mod_small(a, b, h)
79
80law n_div_mul_add:
81  for +q: Nat
82  for +b: Nat
83  for +r: Nat
84  for +h: {Nat.is_lt(r, b) == True{} : Bool}
85  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}
86
87def n_div_mul_add(q, b, r, h):
88  WN.div_mul_add(q, b, r, h)
89
90law n_mul_comm:
91  for +a: Nat
92  for +b: Nat
93  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
94
95def n_mul_comm(a, b):
96  WN.mul_comm(a, b)