LAWS.bend

bend-osdev-word64@0.1.1.0 · 188 lines · 34 definitions

1# The edge cases of 64-bit arithmetic, as vectors: wrapping at 2^64, the two
2# 32-bit halves, shifts across the halves, a multiply that overflows, and the
3# text forms. 0xDEADBEEF = 3735928559, 0xCAFEBABE = 3405691582.
4import Base
5import bend-osdev-u32@0.1.0.0/u32.bend as U
6import bend-osdev-word64@0.1.1.0/word64.bend as W
7
8law add_wraps:
9  {W.W64.add(W.W64.max(), W.W64.one()) == W.W64.zero() : W.W64}
10
11law sub_wraps:
12  {W.W64.sub(W.W64.zero(), W.W64.one()) == W.W64.max() : W.W64}
13
14law hi_of_parts:
15  {W.W64.hi(W.W64.from_parts(3735928559, 3405691582)) == 3735928559 : U32}
16
17law lo_of_parts:
18  {W.W64.lo(W.W64.from_parts(3735928559, 3405691582)) == 3405691582 : U32}
19
20law shl_crosses_halves:
21  {W.W64.shl(W.W64.one(), 32n) == W.W64.from_parts(1, 0) : W.W64}
22
23law shr_crosses_halves:
24  {W.W64.shr(W.W64.from_parts(1, 0), 1n) == W.W64.from_parts(0, 2147483648) : W.W64}
25
26# (2^32 - 1)^2 = 2^64 - 2^33 + 1
27law mul_of_max_halves:
28  {W.W64.mul(W.W64.from_u32(4294967295), W.W64.from_u32(4294967295)) == W.W64.from_parts(4294967294, 1) : W.W64}
29
30law show_max:
31  {W.W64.show(W.W64.max()) == "18446744073709551615" : String}
32
33law show_hex_parts:
34  {W.W64.show_hex(W.W64.from_parts(3735928559, 3405691582)) == "deadbeefcafebabe" : String}
35
36law show_hex_zero:
37  {W.W64.show_hex(W.W64.zero()) == "0000000000000000" : String}
38
39# For every 32-bit a: from_u32 then lo gives a back.
40law lo_from_u32:
41  for a: U32
42  {W.W64.lo(W.W64.from_u32(a)) == a : U32}
43
44# For every pair of halves: splitting the joined word gives them back.
45law hi_from_parts:
46  for h: U32
47  for l: U32
48  {W.W64.hi(W.W64.from_parts(h, l)) == h : U32}
49
50law lo_from_parts:
51  for h: U32
52  for l: U32
53  {W.W64.lo(W.W64.from_parts(h, l)) == l : U32}
54
55# Interface laws: a word whose high half is 0 is the word of its low half,
56# and the word of halves 0 and 0 is zero.
57law from_parts_zero_hi:
58  for a: U32
59  {W.W64.from_parts(0, a) == W.W64.from_u32(a) : W.W64}
60
61law from_parts_zero:
62  {W.W64.from_parts(0, 0) == W.W64.zero() : W.W64}
63
64# Interface law: a word is its two halves joined (for every word). Other
65# packages' proofs use this instead of looking inside W64.
66law parts_of:
67  for v: W.W64
68  {W.W64.from_parts(W.W64.hi(v), W.W64.lo(v)) == v : W.W64}
69
70# The value of a word (for every word): lo + hi * 2^32, the weight 2^32 being
71# 32 doublings (U32Nat.dbl, from bend-osdev-u32).
72law to_nat_parts:
73  for +h: U32
74  for +l: U32
75  {W.W64.to_nat(W.W64.from_parts(h, l)) == Nat.add(U32.to_nat(l), U.U32Nat.dbl(32n, U32.to_nat(h))) : Nat}
76
77# Two words with the same value are the same word.
78law value_eq:
79  for +a: W.W64
80  for +b: W.W64
81  for e: {W.W64.to_nat(a) == W.W64.to_nat(b) : Nat}
82  {a == b : W.W64}
83
84# Comparison is the order of the values (for every pair of words).
85law cmp_value:
86  for +a: W.W64
87  for +b: W.W64
88  {W.W64.cmp(a, b) == Nat.cmp(W.W64.to_nat(a), W.W64.to_nat(b)) : Cmp}
89
90law lt_value:
91  for +a: W.W64
92  for +b: W.W64
93  {W.W64.is_lt(a, b) == Nat.is_lt(W.W64.to_nat(a), W.W64.to_nat(b)) : Bool}
94
95law le_value:
96  for +a: W.W64
97  for +b: W.W64
98  {W.W64.is_le(a, b) == Nat.is_le(W.W64.to_nat(a), W.W64.to_nat(b)) : Bool}
99
100law eq_value:
101  for +a: W.W64
102  for +b: W.W64
103  {W.W64.is_eq(a, b) == Nat.is_eq(W.W64.to_nat(a), W.W64.to_nat(b)) : Bool}
104
105# Comparison is by the high halves, then the low halves (for dependents
106# that order words through W64.hi and W64.lo).
107law cmp_hi_lt:
108  for +a: W.W64
109  for +b: W.W64
110  for h: {U32.cmp(W.W64.hi(a), W.W64.hi(b)) == LT{} : Cmp}
111  {W.W64.cmp(a, b) == LT{} : Cmp}
112
113law cmp_hi_gt:
114  for +a: W.W64
115  for +b: W.W64
116  for h: {U32.cmp(W.W64.hi(a), W.W64.hi(b)) == GT{} : Cmp}
117  {W.W64.cmp(a, b) == GT{} : Cmp}
118
119law cmp_hi_eq:
120  for +a: W.W64
121  for +b: W.W64
122  for h: {U32.cmp(W.W64.hi(a), W.W64.hi(b)) == EQ{} : Cmp}
123  {W.W64.cmp(a, b) == U32.cmp(W.W64.lo(a), W.W64.lo(b)) : Cmp}
124
125# Addition, for every pair of words: the sum of the values, less 2^64 when
126# it wraps, which is exactly when the result is below the first operand;
127# and with the sum no more than a word's value, it does not wrap.
128law add_wrap:
129  for +a: W.W64
130  for +b: W.W64
131  {Nat.add(W.W64.to_nat(W.W64.add(a, b)), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(W.W64.add(a, b), a)))) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
132
133law add_value:
134  for +a: W.W64
135  for +b: W.W64
136  for +c: W.W64
137  for h: {Nat.is_le(Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)), W.W64.to_nat(c)) == True{} : Bool}
138  {W.W64.to_nat(W.W64.add(a, b)) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
139
140# Subtraction, for every pair of words: the difference plus the subtrahend
141# is the minuend, plus 2^64 when the subtrahend is the larger; when it is
142# not, the difference is the Nat difference.
143law sub_wrap:
144  for +a: W.W64
145  for +b: W.W64
146  {Nat.add(W.W64.to_nat(W.W64.sub(a, b)), W.W64.to_nat(b)) == Nat.add(W.W64.to_nat(a), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(a, b)))) : Nat}
147
148law sub_value:
149  for +a: W.W64
150  for +b: W.W64
151  for h: {Nat.is_le(W.W64.to_nat(b), W.W64.to_nat(a)) == True{} : Bool}
152  {W.W64.to_nat(W.W64.sub(a, b)) == Nat.sub(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
153
154# Shifts, as Nat facts. A shift left by k < 64 multiplies the value by 2^k
155# when the result is no more than a word's value; a shift right by k < 64
156# is the floor of the value divided by 2^k (2^k times it is at most the
157# value, and 2^k times one more is above it); by 64 or more, both give 0.
158law shl_value:
159  for +a: W.W64
160  for +k: Nat
161  for +c: W.W64
162  for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
163  for +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(a)), W.W64.to_nat(c)) == True{} : Bool}
164  {W.W64.to_nat(W.W64.shl(a, k)) == U.U32Nat.dbl(k, W.W64.to_nat(a)) : Nat}
165
166law shr_value_le:
167  for +a: W.W64
168  for +k: Nat
169  for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
170  {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr(a, k))), W.W64.to_nat(a)) == True{} : Bool}
171
172law shr_value_lt:
173  for +a: W.W64
174  for +k: Nat
175  for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
176  {Nat.is_lt(W.W64.to_nat(a), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64.shr(a, k)))) == True{} : Bool}
177
178law shl_big:
179  for +a: W.W64
180  for +k: Nat
181  for +h: {Nat.is_le(64n, k) == True{} : Bool}
182  {W.W64.shl(a, k) == W.W64.zero() : W.W64}
183
184law shr_big:
185  for +a: W.W64
186  for +k: Nat
187  for +h: {Nat.is_le(64n, k) == True{} : Bool}
188  {W.W64.shr(a, k) == W.W64.zero() : W.W64}