LAWS.bend
bend-osdev-word64@0.1.1.0 · 188 lines · 0 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}