1 import Base 2 import ../../../spec/math/u64.bend as SU 3 import ../../../src/math/u64.bend as U 4 import ../../lib/lemmas/src/wide.bend as W 5 import ../../lib/lemmas/spec/numeric.bend as S 6 import ../../lib/logic.bend as L 7 import ../../lib/nat.bend as N 8 import ../../lib/u32.bend as U3 9 import ../../lib/u32alg.bend as A 10 import ../../lib/lemmas/proofs/numeric.bend as NUM 11 import ../../lib/lemmas/proofs/addition.bend as AD 12 import ../../lib/lemmas/proofs/modular_addition.bend as MA 13 import ../../lib/lemmas/proofs/word_addition.bend as WA 14 import ../../lib/word.bend as WD 15 import ../../lib/u32div.bend as UD 16 17 # src/math/u64.bend against its specification spec/math/u64.bend: a U64 18 # denotes the 64-bit word bits(a) (low limb first). 19 20 def bits(a: U.U64) -> Word(64n): 21 SU.bits(a) 22 23 # ---- comparison ---- 24 25 def order_eq(+c: Cmp) -> {U.order(c, EQ{}) == c : Cmp}: 26 match c: 27 case LT{}: 28 {==} 29 case EQ{}: 30 {==} 31 case GT{}: 32 {==} 33 34 def fin_order(+x: Bool, +y: Bool, +c: Cmp, +d: Cmp) -> {Word.cmp.fin(x, y, U.order(c, d)) == U.order(c, Word.cmp.fin(x, y, d)) : Cmp}: 35 match c: 36 case LT{}: 37 {==} 38 case EQ{}: 39 {==} 40 case GT{}: 41 {==} 42 43 # Comparing two joined words is comparing the high parts, then the low parts. 44 def cmp_join(+n: Nat, +m: Nat, +a1: Word(n), +b1: Word(m), +a2: Word(n), +b2: Word(m)) -> {Word.cmp(Nat.add(n, m), W.join(n, m, a1, b1), W.join(n, m, a2, b2)) == U.order(Word.cmp(m, b1, b2), Word.cmp(n, a1, a2)) : Cmp}: 45 match n a1 a2: 46 case 0n WNil{} WNil{}: 47 Equal.sym(Cmp, U.order(Word.cmp(m, b1, b2), EQ{}), Word.cmp(m, b1, b2), order_eq(Word.cmp(m, b1, b2))) 48 case 1n+p WCon{x, t1} WCon{y, t2}: 49 %Equal.sym(Cmp, Word.cmp(Nat.add(p, m), W.join(p, m, t1, b1), W.join(p, m, t2, b2)), U.order(Word.cmp(m, b1, b2), Word.cmp(p, t1, t2)), cmp_join(p, m, t1, b1, t2, b2)) : {Word.cmp.fin(x, y, _) == U.order(Word.cmp(m, b1, b2), Word.cmp.fin(x, y, Word.cmp(p, t1, t2))) : Cmp} 50 fin_order(x, y, Word.cmp(m, b1, b2), Word.cmp(p, t1, t2)) 51 52 def u32_cmp(+x: Word(32n), +y: Word(32n)) -> {U32.cmp(U32{x}, U32{y}) == Word.cmp(32n, x, y) : Cmp}: 53 {==} 54 55 def cmp_pack(+alo: U32, +ahi: U32, +blo: U32, +bhi: U32) -> {Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi)) == U.order(U32.cmp(ahi, bhi), U32.cmp(alo, blo)) : Cmp}: 56 match alo ahi blo bhi: 57 case U32{a} U32{b} U32{c} U32{d}: 58 cmp_join(32n, 32n, a, b, c, d) 59 60 def ge_fin_zero(+c: Cmp, +x: Bool, +h: {Cmp.is_ge(c) == True{} : Bool}) -> {Cmp.is_ge(Word.cmp.fin(x, False{}, c)) == True{} : Bool}: 61 match c x: 62 case LT{} _: 63 Empty.absurd({Cmp.is_ge(Word.cmp.fin(x, False{}, LT{})) == True{} : Bool}, L.false_true(h)) 64 case EQ{} True{}: 65 {==} 66 case EQ{} False{}: 67 {==} 68 case GT{} _: 69 {==} 70 71 # Nothing compares below zero. 72 def ge_zero(+n: Nat, +w: Word(n)) -> {Cmp.is_ge(Word.cmp(n, w, Word.zero(n))) == True{} : Bool}: 73 match n w: 74 case 0n WNil{}: 75 {==} 76 case 1n+p WCon{x, t}: 77 ge_fin_zero(Word.cmp(p, t, Word.zero(p)), x, ge_zero(p, t)) 78 79 def ge_order(+c: Cmp, +d: Cmp, +h: {Cmp.is_ge(d) == True{} : Bool}) -> {Cmp.is_ge(U.order(c, d)) == Cmp.is_ge(c) : Bool}: 80 match c: 81 case LT{}: 82 {==} 83 case EQ{}: 84 h 85 case GT{}: 86 {==} 87 88 def threshold() -> {S.sign_threshold(63n) == W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n)) : Word(64n)}: 89 {==} 90 91 def threshold_u32() -> {2147483648 == U32{S.sign_threshold(31n)} : U32}: 92 {==} 93 94 # The sign of the 64-bit word is the top bit of the high limb. 95 def negative_pack(+lo: U32, +hi: U32) -> {S.negative(W.pack(lo, hi)) == U32.is_ge(hi, 2147483648) : Bool}: 96 match lo hi: 97 case U32{a} U32{b}: 98 %Equal.sym(Word(64n), W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n)), S.sign_threshold(63n), threshold()) : {Cmp.is_ge(Word.cmp(64n, W.join(32n, 32n, a, b), _)) == U32.is_ge(U32{b}, 2147483648) : Bool} 99 %Equal.sym(Cmp, Word.cmp(64n, W.join(32n, 32n, a, b), W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n))), U.order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n))), cmp_join(32n, 32n, a, b, Word.zero(32n), S.sign_threshold(31n))) : {Cmp.is_ge(_) == U32.is_ge(U32{b}, 2147483648) : Bool} 100 %Equal.sym(U32, U32{S.sign_threshold(31n)}, 2147483648, threshold_u32()) : {Cmp.is_ge(U.order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n)))) == U32.is_ge(U32{b}, _) : Bool} 101 ge_order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n)), ge_zero(32n, a)) 102 103 def le_sign_spec(+alo: U32, +ahi: U32, +blo: U32, +bhi: U32, +na: Bool, +nb: Bool) -> {U.le_sign(alo, ahi, blo, bhi, na, nb) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), na, nb) : Bool}: 104 match na nb: 105 case True{} False{}: 106 {==} 107 case False{} True{}: 108 {==} 109 case True{} True{}: 110 %cmp_pack(alo, ahi, blo, bhi) : {Cmp.is_le(_) == Cmp.is_le(Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi))) : Bool} 111 {==} 112 case False{} False{}: 113 %cmp_pack(alo, ahi, blo, bhi) : {Cmp.is_le(_) == Cmp.is_le(Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi))) : Bool} 114 {==} 115 116 # THEOREM: le_signed is the specification's signed 64-bit order. 117 def le_signed(+a: U.U64, +b: U.U64) -> {U.le_signed(a, b) == S.order(bits(a), bits(b), S.negative(bits(a)), S.negative(bits(b))) : Bool}: 118 match a b: 119 case U.U64{alo, ahi} U.U64{blo, bhi}: 120 %Equal.sym(Bool, S.negative(W.pack(alo, ahi)), U32.is_ge(ahi, 2147483648), negative_pack(alo, ahi)) : {U.le_signed(U.U64{alo, ahi}, U.U64{blo, bhi}) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), _, S.negative(W.pack(blo, bhi))) : Bool} 121 %Equal.sym(Bool, S.negative(W.pack(blo, bhi)), U32.is_ge(bhi, 2147483648), negative_pack(blo, bhi)) : {U.le_signed(U.U64{alo, ahi}, U.U64{blo, bhi}) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), U32.is_ge(ahi, 2147483648), _) : Bool} 122 le_sign_spec(alo, ahi, blo, bhi, U32.is_ge(ahi, 2147483648), U32.is_ge(bhi, 2147483648)) 123 124 # ---- zero test ---- 125 126 def eq_order(+c: Cmp, +d: Cmp) -> {Cmp.is_eq(U.order(c, d)) == Bool.and(Cmp.is_eq(d), Cmp.is_eq(c)) : Bool}: 127 match c d: 128 case LT{} LT{}: 129 {==} 130 case LT{} EQ{}: 131 {==} 132 case LT{} GT{}: 133 {==} 134 case EQ{} LT{}: 135 {==} 136 case EQ{} EQ{}: 137 {==} 138 case EQ{} GT{}: 139 {==} 140 case GT{} LT{}: 141 {==} 142 case GT{} EQ{}: 143 {==} 144 case GT{} GT{}: 145 {==} 146 147 def zero_pack() -> {Word.zero(64n) == W.pack(0, 0) : Word(64n)}: 148 {==} 149 150 # THEOREM: is_zero is the specification's zero test. 151 def is_zero(+a: U.U64) -> {U.is_zero(a) == S.zero(bits(a)) : Bool}: 152 match a: 153 case U.U64{lo, hi}: 154 %Equal.sym(Word(64n), W.pack(0, 0), Word.zero(64n), zero_pack()) : {U.is_zero(U.U64{lo, hi}) == Cmp.is_eq(Word.cmp(64n, W.pack(lo, hi), _)) : Bool} 155 %Equal.sym(Cmp, Word.cmp(64n, W.pack(lo, hi), W.pack(0, 0)), U.order(U32.cmp(hi, 0), U32.cmp(lo, 0)), cmp_pack(lo, hi, 0, 0)) : {U.is_zero(U.U64{lo, hi}) == Cmp.is_eq(_) : Bool} 156 Equal.sym(Bool, Cmp.is_eq(U.order(U32.cmp(hi, 0), U32.cmp(lo, 0))), Bool.and(Cmp.is_eq(U32.cmp(lo, 0)), Cmp.is_eq(U32.cmp(hi, 0))), eq_order(U32.cmp(hi, 0), U32.cmp(lo, 0))) 157 158 # ---- addition ---- 159 160 def val(+a: U.U64) -> Nat: 161 S.unsigned(64n, bits(a)) 162 163 def val_pack(+lo: U32, +hi: U32) -> {S.unsigned(64n, W.pack(lo, hi)) == Nat.add(UD.v(lo), WD.sc(32n, UD.v(hi))) : Nat}: 164 NUM.pack_interpretation(lo, hi) 165 166 def carry32(+x: U32, +y: U32) -> Bool: 167 match x y: 168 case U32{a} U32{b}: 169 AD.carry_out(32n, a, b, False{}) 170 171 def add_cons(+x: U32, +y: U32) -> {Nat.add(UD.v(U32.add(x, y)), WD.sc(32n, S.bit_value(carry32(x, y)))) == Nat.add(UD.v(x), UD.v(y)) : Nat}: 172 match x y: 173 case U32{+a} U32{+b}: 174 %Equal.sym(Nat, UD.v(U32{Word.add(32n, a, b)}), WD.uw(32n, Word.add(32n, a, b)), UD.vw(Word.add(32n, a, b))) : {Nat.add(_, WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(UD.v(U32{a}), UD.v(U32{b})) : Nat} 175 %Equal.sym(Nat, UD.v(U32{a}), WD.uw(32n, a), UD.vw(a)) : {Nat.add(WD.uw(32n, Word.add(32n, a, b)), WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(_, UD.v(U32{b})) : Nat} 176 %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.add(WD.uw(32n, Word.add(32n, a, b)), WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(WD.uw(32n, a), _) : Nat} 177 A.cons(32n, a, b) 178 179 def add_lt1(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}: 180 %Equal.sym(Bool, U32.is_lt(U32.add(x, y), x), Nat.is_lt(UD.v(U32.add(x, y)), UD.v(x)), U3.is_lt_nat(U32.add(x, y), x)) : {_ == carry32(x, y) : Bool} 181 WD.carry_lt(32n, one, h1, UD.v(U32.add(x, y)), UD.v(x), UD.v(y), carry32(x, y), add_cons(x, y), UD.vb(one, h1, y)) 182 183 # the low-limb wrap test is the low-limb carry 184 def add_lt(+x: U32, +y: U32) -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}: 185 add_lt1(1n, {==}, x, y) 186 187 def carry_v(+c: Bool) -> {UD.v(U.carry(c)) == S.bit_value(c) : Nat}: 188 match c: 189 case True{}: 190 {==} 191 case False{}: 192 {==} 193 194 def add_hi(ahi: U32, bhi: U32, c: Bool) -> U32: 195 U32.add(U32.add(ahi, bhi), U.carry(c)) 196 197 def add_over(a: U.U64, b: U.U64) -> Nat: 198 match a b: 199 case U.U64{+alo, +ahi} U.U64{+blo, +bhi}: 200 Nat.add(S.bit_value(carry32(ahi, bhi)), S.bit_value(carry32(U32.add(ahi, bhi), U.carry(U32.is_lt(U32.add(alo, blo), alo))))) 201 202 # the sum loses exactly 2^64 times the high carries 203 def add_value(+a: U.U64, +b: U.U64) -> {Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b))) == Nat.add(val(a), val(b)) : Nat}: 204 match a b: 205 case U.U64{+alo, +ahi} U.U64{+blo, +bhi}: 206 +lo = U32.add(alo, blo) 207 +cb = U32.is_lt(lo, alo) 208 +t = U32.add(ahi, bhi) 209 +h = U32.add(t, U.carry(cb)) 210 +c0 = S.bit_value(carry32(alo, blo)) 211 +c1 = S.bit_value(carry32(ahi, bhi)) 212 +c2 = S.bit_value(carry32(t, U.carry(cb))) 213 +f1 = add_cons(alo, blo) 214 +f2 = add_cons(ahi, bhi) 215 +f3 = Equal.trans(Nat, Nat.add(UD.v(h), WD.sc(32n, c2)), Nat.add(UD.v(t), UD.v(U.carry(cb))), Nat.add(UD.v(t), c0), add_cons(t, U.carry(cb)), 216 Equal.cong(Nat, Nat, z => Nat.add(UD.v(t), z), UD.v(U.carry(cb)), c0, Equal.trans(Nat, UD.v(U.carry(cb)), S.bit_value(cb), c0, carry_v(cb), Equal.cong(Bool, Nat, S.bit_value, cb, carry32(alo, blo), add_lt(alo, blo))))) 217 %Equal.sym(Nat, S.unsigned(64n, W.pack(lo, h)), Nat.add(UD.v(lo), WD.sc(32n, UD.v(h))), val_pack(lo, h)) : {Nat.add(_, WD.sc(64n, Nat.add(c1, c2))) == Nat.add(S.unsigned(64n, W.pack(alo, ahi)), S.unsigned(64n, W.pack(blo, bhi))) : Nat} 218 %Equal.sym(Nat, S.unsigned(64n, W.pack(alo, ahi)), Nat.add(UD.v(alo), WD.sc(32n, UD.v(ahi))), val_pack(alo, ahi)) : {Nat.add(Nat.add(UD.v(lo), WD.sc(32n, UD.v(h))), WD.sc(64n, Nat.add(c1, c2))) == Nat.add(_, S.unsigned(64n, W.pack(blo, bhi))) : Nat} 219 %Equal.sym(Nat, S.unsigned(64n, W.pack(blo, bhi)), Nat.add(UD.v(blo), WD.sc(32n, UD.v(bhi))), val_pack(blo, bhi)) : {Nat.add(Nat.add(UD.v(lo), WD.sc(32n, UD.v(h))), WD.sc(64n, Nat.add(c1, c2))) == Nat.add(Nat.add(UD.v(alo), WD.sc(32n, UD.v(ahi))), _) : Nat} 220 WD.add_alg(32n, UD.v(lo), UD.v(h), UD.v(t), c0, c1, c2, UD.v(alo), UD.v(ahi), UD.v(blo), UD.v(bhi), f1, f2, f3) 221 222 # THEOREM: add is 64-bit wrapping addition. 223 def add(+a: U.U64, +b: U.U64) -> {bits(U.add(a, b)) == Word.add(64n, bits(a), bits(b)) : Word(64n)}: 224 Equal.trans(Word(64n), bits(U.add(a, b)), S.from_nat(64n, Nat.add(val(a), val(b))), Word.add(64n, bits(a), bits(b)), 225 Equal.trans(Word(64n), bits(U.add(a, b)), S.from_nat(64n, Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b)))), S.from_nat(64n, Nat.add(val(a), val(b))), 226 Equal.sym(Word(64n), S.from_nat(64n, Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b)))), bits(U.add(a, b)), MA.reconstruct(64n, bits(U.add(a, b)), add_over(a, b))), 227 Equal.cong(Nat, Word(64n), z => S.from_nat(64n, z), Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b))), Nat.add(val(a), val(b)), add_value(a, b))), 228 Equal.sym(Word(64n), Word.add(64n, bits(a), bits(b)), S.from_nat(64n, Nat.add(val(a), val(b))), WA.refines(64n, bits(a), bits(b)))) 229 230 # ---- negation ---- 231 232 def inc_zero32(+x: Word(32n)) -> {U32.is_zero(U32{Word.inc(32n, x)}) == WD.ones(32n, x) : Bool}: 233 WD.inc_zero(32n, x) 234 235 def add_carry(+xw: Word(32n), +c: Bool) -> {U32.add(U32{xw}, U.carry(c)) == U32{WD.incif(32n, c, xw)} : U32}: 236 match c: 237 case True{}: 238 Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, xw, WD.one_word(31n)), Word.inc(32n, xw), WD.add_one(31n, xw)) 239 case False{}: 240 A.add_zero(U32{xw}) 241 242 # THEOREM: neg is two's-complement negation. 243 def neg(+a: U.U64) -> {bits(U.neg(a)) == Word.inc(64n, Word.not(64n, bits(a))) : Word(64n)}: 244 match a: 245 case U.U64{+lo, +hi}: 246 match lo hi: 247 case U32{+x} U32{+y}: 248 +nx = Word.not(32n, x) 249 +ny = Word.not(32n, y) 250 +j = W.join(32n, 32n, Word.inc(32n, nx), WD.incif(32n, WD.ones(32n, nx), ny)) 251 +p1 = Equal.cong(U32, Word(64n), z => W.pack(U32{Word.inc(32n, nx)}, z), U32.add(U32{ny}, U.carry(U32.is_zero(U32{Word.inc(32n, nx)}))), U32{WD.incif(32n, WD.ones(32n, nx), ny)}, 252 Equal.trans(U32, U32.add(U32{ny}, U.carry(U32.is_zero(U32{Word.inc(32n, nx)}))), U32.add(U32{ny}, U.carry(WD.ones(32n, nx))), U32{WD.incif(32n, WD.ones(32n, nx), ny)}, 253 Equal.cong(Bool, U32, c => U32.add(U32{ny}, U.carry(c)), U32.is_zero(U32{Word.inc(32n, nx)}), WD.ones(32n, nx), inc_zero32(nx)), 254 add_carry(ny, WD.ones(32n, nx)))) 255 +p2 = Equal.trans(Word(64n), Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), Word.inc(64n, W.join(32n, 32n, nx, ny)), j, 256 Equal.cong(Word(64n), Word(64n), w => Word.inc(64n, w), Word.not(64n, W.join(32n, 32n, x, y)), W.join(32n, 32n, nx, ny), WD.not_join(32n, 32n, x, y)), 257 WD.inc_join(32n, 32n, nx, ny)) 258 Equal.trans(Word(64n), bits(U.neg(U.U64{U32{x}, U32{y}})), j, Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), p1, Equal.sym(Word(64n), Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), j, p2))