1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/instances.bend as SI 4 import ../../../spec/math/generic.bend as SG 5 import ../../../src/math/instances.bend as I 6 import ../../../src/math/num.bend as NM 7 import ../../../src/math/w64.bend as X 8 import ../../../src/math/u64.bend as WU 9 import ../../lib/nat.bend as N 10 import ../../lib/logic.bend as L 11 import ./width.bend as WW 12 import ./u32laws.bend as LW 13 import ./w64add.bend as WA 14 import ./w64dmtop.bend as DT 15 import ./w64dmrem.bend as DR 16 import ./w64mmtop.bend as MMT 17 import ./w64isq.bend as ISQ 18 import ./w64sh.bend as SH 19 20 # The seventeen instance laws of spec/math/instances.bend at U64, from the 21 # proved clauses of spec/math/w64.bend, and the value model (every U64 is 22 # of_nat of its value, values below 2^64 round-trip). 23 24 def v(+x: WU.U64) -> Nat: 25 SG.u64_val(x) 26 27 def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty: 28 LW.true_ne_false(h) 29 30 def vb(+x: WU.U64) -> {C.fits(64n, v(x)) == True{} : Bool}: 31 match x: 32 case WU.U64{+l, +h}: 33 WW.limbs_fit(32n, 32n, LW.v(l), LW.v(h), LW.vb(l), LW.vb(h)) 34 35 def val_lt(+K: Nat, +hK: {K == 64n : Nat}, +x: WU.U64) -> {Nat.is_lt(v(x), C.pow2(K)) == True{} : Bool}: 36 WW.lt_of_fits(K, v(x), L.subst(Nat, z => {C.fits(z, v(x)) == True{} : Bool}, 64n, K, Equal.sym(Nat, K, 64n, hK), vb(x))) 37 38 def rt(+x: WU.U64) -> {SG.u64_of(v(x)) == x : WU.U64}: 39 match x: 40 case WU.U64{+l, +h}: 41 +el = WW.low_u(32n, LW.v(l), LW.v(h), LW.vb(l)) 42 +eh = WW.high_u(32n, LW.v(l), LW.v(h), LW.vb(l)) 43 +e1 = Equal.trans(U32, U32.from_nat(C.low(32n, v(WU.U64{l, h}))), U32.from_nat(LW.v(l)), l, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, v(WU.U64{l, h})), LW.v(l), el), LW.rt(l)) 44 +e2 = Equal.trans(U32, U32.from_nat(C.high(32n, v(WU.U64{l, h}))), U32.from_nat(LW.v(h)), h, Equal.cong(Nat, U32, z => U32.from_nat(z), C.high(32n, v(WU.U64{l, h})), LW.v(h), eh), LW.rt(h)) 45 Equal.trans(WU.U64, WU.U64{U32.from_nat(C.low(32n, v(WU.U64{l, h}))), U32.from_nat(C.high(32n, v(WU.U64{l, h})))}, WU.U64{l, U32.from_nat(C.high(32n, v(WU.U64{l, h})))}, WU.U64{l, h}, Equal.cong(U32, WU.U64, z => WU.U64{z, U32.from_nat(C.high(32n, v(WU.U64{l, h})))}, U32.from_nat(C.low(32n, v(WU.U64{l, h}))), l, e1), Equal.cong(U32, WU.U64, z => WU.U64{l, z}, U32.from_nat(C.high(32n, v(WU.U64{l, h}))), h, e2)) 46 47 def vo(+n: Nat, +h: {C.fits(64n, n) == True{} : Bool}) -> {v(SG.u64_of(n)) == n : Nat}: 48 +hl = WW.low_fits(32n, n) 49 +hh = SH.fits_high(32n, 32n, n, h) 50 +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, U32.to_nat(U32.from_nat(C.high(32n, n))))), U32.to_nat(U32.from_nat(C.low(32n, n))), C.low(32n, n), LW.vo(C.low(32n, n), hl)) 51 +e2 = Equal.cong(Nat, Nat, z => Nat.add(C.low(32n, n), C.shift(32n, z)), U32.to_nat(U32.from_nat(C.high(32n, n))), C.high(32n, n), LW.vo(C.high(32n, n), hh)) 52 Equal.trans(Nat, Nat.add(U32.to_nat(U32.from_nat(C.low(32n, n))), C.shift(32n, U32.to_nat(U32.from_nat(C.high(32n, n))))), Nat.add(C.low(32n, n), C.shift(32n, U32.to_nat(U32.from_nat(C.high(32n, n))))), n, e1, Equal.trans(Nat, Nat.add(C.low(32n, n), C.shift(32n, U32.to_nat(U32.from_nat(C.high(32n, n))))), Nat.add(C.low(32n, n), C.shift(32n, C.high(32n, n))), n, e2, Equal.sym(Nat, n, Nat.add(C.low(32n, n), C.shift(32n, C.high(32n, n))), WW.low_high(32n, n)))) 53 54 # ---- the laws ---- 55 56 def ops_zero() -> SI.Ops.zero(~WU.U64, ~I.u64_op, ~SG.u64_val): 57 SH.val0(0) 58 59 def ops_one() -> SI.Ops.one(~WU.U64, ~I.u64_op, ~SG.u64_val): 60 SH.val0(1) 61 62 def ops_abs(+x: WU.U64) -> SI.Ops.abs(~WU.U64, ~I.u64_op, x): 63 {==} 64 65 def tests_lt(+a: WU.U64, +b: WU.U64) -> SI.Tests.lt(~WU.U64, ~I.u64_is, ~SG.u64_val, a, b): 66 WA.lt_value(a, b) 67 68 def tests_is_zero(+a: WU.U64) -> SI.Tests.is_zero(~WU.U64, ~I.u64_is, ~SG.u64_val, a): 69 WA.is_zero_value(a) 70 71 def tests_odd(+a: WU.U64) -> SI.Tests.odd(~WU.U64, ~I.u64_is, ~SG.u64_val, a): 72 WA.odd_value(a) 73 74 def tests_add_over(+a: WU.U64, +b: WU.U64) -> SI.Tests.add_over(~WU.U64, ~I.u64_is, ~SG.u64_val, 64n, a, b): 75 WA.add_over_value(a, b) 76 77 def tests_mul_over(+a: WU.U64, +b: WU.U64) -> SI.Tests.mul_over(~WU.U64, ~I.u64_is, ~SG.u64_val, 64n, a, b): 78 WA.mul_over_value(a, b) 79 80 def ops_sub(+a: WU.U64, +b: WU.U64, +h: {Nat.is_le(SG.u64_val(b), SG.u64_val(a)) == True{} : Bool}) -> SI.Ops.sub(~WU.U64, ~I.u64_op, ~SG.u64_val, a, b, h): 81 WA.sub_value(a, b, h) 82 83 def ops_half(+a: WU.U64) -> SI.Ops.half(~WU.U64, ~I.u64_op, ~SG.u64_val, a): 84 WA.half_value(a) 85 86 def nzb(+b: WU.U64, +h: {Nat.is_eq(SG.u64_val(b), 0n) == False{} : Bool}) -> {X.is_zero(b) == False{} : Bool}: 87 Equal.trans(Bool, X.is_zero(b), Nat.is_eq(v(b), 0n), False{}, WA.is_zero_value(b), h) 88 89 def ops_quot(+a: WU.U64, +b: WU.U64, +h: {Nat.is_eq(SG.u64_val(b), 0n) == False{} : Bool}) -> SI.Ops.quot(~WU.U64, ~I.u64_op, ~SG.u64_val, a, b, h): 90 DT.divmod_quot(a, b, nzb(b, h)) 91 92 def ops_rem(+a: WU.U64, +b: WU.U64, +h: {Nat.is_eq(SG.u64_val(b), 0n) == False{} : Bool}) -> SI.Ops.rem(~WU.U64, ~I.u64_op, ~SG.u64_val, a, b, h): 93 DR.divmod_rem(a, b, nzb(b, h)) 94 95 def not_f(+x: Bool, +h: {Bool.not(x) == False{} : Bool}) -> {x == True{} : Bool}: 96 match x: 97 case True{}: 98 {==} 99 case False{}: 100 Empty.absurd({False{} == True{} : Bool}, true_ne_false(h)) 101 102 def ops_add(+a: WU.U64, +b: WU.U64, +h: {I.u64_is(NM.AddOver{a, b}) == False{} : Bool}) -> SI.Ops.add(~WU.U64, ~I.u64_op, ~I.u64_is, ~SG.u64_val, a, b, h): 103 +hf = not_f(C.fits(64n, Nat.add(v(a), v(b))), Equal.trans(Bool, Bool.not(C.fits(64n, Nat.add(v(a), v(b)))), X.add_over(a, b), False{}, Equal.sym(Bool, X.add_over(a, b), Bool.not(C.fits(64n, Nat.add(v(a), v(b)))), WA.add_over_value(a, b)), h)) 104 Equal.trans(Nat, v(X.add(a, b)), C.low(64n, Nat.add(v(a), v(b))), Nat.add(v(a), v(b)), WA.add_value(a, b), WW.low_fit(64n, Nat.add(v(a), v(b)), hf)) 105 106 def ops_mul(+a: WU.U64, +b: WU.U64, +h: {I.u64_is(NM.MulOver{a, b}) == False{} : Bool}) -> SI.Ops.mul(~WU.U64, ~I.u64_op, ~I.u64_is, ~SG.u64_val, a, b, h): 107 +hf = not_f(C.fits(64n, Nat.mul(v(a), v(b))), Equal.trans(Bool, Bool.not(C.fits(64n, Nat.mul(v(a), v(b)))), X.mul_over(a, b), False{}, Equal.sym(Bool, X.mul_over(a, b), Bool.not(C.fits(64n, Nat.mul(v(a), v(b)))), WA.mul_over_value(a, b)), h)) 108 Equal.trans(Nat, v(X.mul(a, b)), C.low(64n, Nat.mul(v(a), v(b))), Nat.mul(v(a), v(b)), WA.mul_value(a, b), WW.low_fit(64n, Nat.mul(v(a), v(b)), hf)) 109 110 def ops_mulmod(+a: WU.U64, +b: WU.U64, +m: WU.U64, +ha: {Nat.is_lt(SG.u64_val(a), SG.u64_val(m)) == True{} : Bool}, +hb: {Nat.is_lt(SG.u64_val(b), SG.u64_val(m)) == True{} : Bool}) -> SI.Ops.mulmod(~WU.U64, ~I.u64_op, ~SG.u64_val, a, b, m, ha, hb): 111 MMT.mulmod_value(a, b, m, ha, hb) 112 113 def ops_sqrt(+a: WU.U64) -> SI.Ops.sqrt(~WU.U64, ~I.u64_op, ~SG.u64_val, a): 114 ISQ.isqrt_value(a) 115 116 def pow2_c(+k: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(k, 32n) == c : Bool}) -> {v(X.w_pow2(k, c)) == C.pow2(k) : Nat}: 117 match c: 118 case True{}: 119 Equal.trans(Nat, v(WU.U64{X.pow2(k), 0}), U32.to_nat(X.pow2(k)), C.pow2(k), SH.val0(X.pow2(k)), SH.p2v(k, hc)) 120 case False{}: 121 +hge = N.not_lt_le(k, 32n, hc) 122 +d = Nat.sub(k, 32n) 123 +ek = N.sub_add(k, 32n, hge) 124 +hd = L.subst(Nat, z => {Nat.is_lt(d, z) == True{} : Bool}, Nat.sub(64n, 32n), 32n, {==}, WW.sub_lt_sub(k, 64n, 32n, hk, hge)) 125 Equal.trans(Nat, C.shift(32n, U32.to_nat(X.pow2(d))), C.shift(32n, C.pow2(d)), C.pow2(k), Equal.cong(Nat, Nat, z => C.shift(32n, z), U32.to_nat(X.pow2(d)), C.pow2(d), SH.p2v(d, hd)), Equal.trans(Nat, C.shift(32n, C.pow2(d)), C.pow2(Nat.add(32n, d)), C.pow2(k), WW.shift_pow2(32n, d), Equal.cong(Nat, Nat, z => C.pow2(z), Nat.add(32n, d), k, ek))) 126 127 def ops_pow2(+k: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> SI.Ops.pow2(~WU.U64, ~I.u64_op, ~SG.u64_val, 64n, k, hk): 128 pow2_c(k, hk, Nat.is_lt(k, 32n), {==})