LAWS.bend
bend-osdev-word64@0.1.0.0 · 58 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-word64@0.1.0.0/word64.bend as W
6
7law add_wraps:
8 {W.W64.add(W.W64.max(), W.W64.one()) == W.W64.zero() : W.W64}
9
10law sub_wraps:
11 {W.W64.sub(W.W64.zero(), W.W64.one()) == W.W64.max() : W.W64}
12
13law hi_of_parts:
14 {W.W64.hi(W.W64.from_parts(3735928559, 3405691582)) == 3735928559 : U32}
15
16law lo_of_parts:
17 {W.W64.lo(W.W64.from_parts(3735928559, 3405691582)) == 3405691582 : U32}
18
19law shl_crosses_halves:
20 {W.W64.shl(W.W64.one(), 32n) == W.W64.from_parts(1, 0) : W.W64}
21
22law shr_crosses_halves:
23 {W.W64.shr(W.W64.from_parts(1, 0), 1n) == W.W64.from_parts(0, 2147483648) : W.W64}
24
25# (2^32 - 1)^2 = 2^64 - 2^33 + 1
26law mul_of_max_halves:
27 {W.W64.mul(W.W64.from_u32(4294967295), W.W64.from_u32(4294967295)) == W.W64.from_parts(4294967294, 1) : W.W64}
28
29law show_max:
30 {W.W64.show(W.W64.max()) == "18446744073709551615" : String}
31
32law show_hex_parts:
33 {W.W64.show_hex(W.W64.from_parts(3735928559, 3405691582)) == "deadbeefcafebabe" : String}
34
35law show_hex_zero:
36 {W.W64.show_hex(W.W64.zero()) == "0000000000000000" : String}
37
38# For every 32-bit a: from_u32 then lo gives a back.
39law lo_from_u32:
40 for a: U32
41 {W.W64.lo(W.W64.from_u32(a)) == a : U32}
42
43# For every pair of halves: splitting the joined word gives them back.
44law hi_from_parts:
45 for h: U32
46 for l: U32
47 {W.W64.hi(W.W64.from_parts(h, l)) == h : U32}
48
49law lo_from_parts:
50 for h: U32
51 for l: U32
52 {W.W64.lo(W.W64.from_parts(h, l)) == l : U32}
53
54# Interface law: a word is its two halves joined (for every word). Other
55# packages' proofs use this instead of looking inside W64.
56law parts_of:
57 for v: W.W64
58 {W.W64.from_parts(W.W64.hi(v), W.W64.lo(v)) == v : W.W64}