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. 4 import Base 5 import bend-osdev-u32@0.1.0.0/u32.bend as U 6 import ./word64.bend as W 7 8 law add_wraps: 9 {W.W64.add(W.W64.max(), W.W64.one()) == W.W64.zero() : W.W64} 10 11 law sub_wraps: 12 {W.W64.sub(W.W64.zero(), W.W64.one()) == W.W64.max() : W.W64} 13 14 law hi_of_parts: 15 {W.W64.hi(W.W64.from_parts(3735928559, 3405691582)) == 3735928559 : U32} 16 17 law lo_of_parts: 18 {W.W64.lo(W.W64.from_parts(3735928559, 3405691582)) == 3405691582 : U32} 19 20 law shl_crosses_halves: 21 {W.W64.shl(W.W64.one(), 32n) == W.W64.from_parts(1, 0) : W.W64} 22 23 law 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 27 law 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 30 law show_max: 31 {W.W64.show(W.W64.max()) == "18446744073709551615" : String} 32 33 law show_hex_parts: 34 {W.W64.show_hex(W.W64.from_parts(3735928559, 3405691582)) == "deadbeefcafebabe" : String} 35 36 law 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. 40 law 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. 45 law hi_from_parts: 46 for h: U32 47 for l: U32 48 {W.W64.hi(W.W64.from_parts(h, l)) == h : U32} 49 50 law 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. 57 law from_parts_zero_hi: 58 for a: U32 59 {W.W64.from_parts(0, a) == W.W64.from_u32(a) : W.W64} 60 61 law 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. 66 law 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). 72 law 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. 78 law 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). 85 law 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 90 law 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 95 law 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 100 law 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). 107 law 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 113 law 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 119 law 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. 128 law 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 133 law 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. 143 law 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 148 law 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. 158 law 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 166 law 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 172 law 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 178 law 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 184 law 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}