~/jendhub

def m128_value

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64m128.bend:81

import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend as W64m128
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

81# the 128-bit product: low 64 bits + 2^64 * high 64 bits
82def m128_value(+al: U32, +ah: U32, +bl: U32, +bh: U32) -> {Nat.add(SW.value(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh}))), C.shift(64n, SW.value(X.psnd(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh}))))) == Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}:
83  +ea = Equal.trans(Nat, Nat.mul(v(al), v(bl)), SW.value(X.mul32(al, bl)), Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(X.hi(X.mul32(al, bl))))), Equal.sym(Nat, SW.value(X.mul32(al, bl)), Nat.mul(v(al), v(bl)), W64M.mul32_value(al, bl)), WA.val_eta(X.mul32(al, bl)))
84  +e12 = Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(SW.value(X.mul32(al, bh)), Nat.mul(v(ah), v(bl))), Nat.add(SW.value(X.mul32(al, bh)), SW.value(X.mul32(ah, bl))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(v(ah), v(bl))), Nat.mul(v(al), v(bh)), SW.value(X.mul32(al, bh)), Equal.sym(Nat, SW.value(X.mul32(al, bh)), Nat.mul(v(al), v(bh)), W64M.mul32_value(al, bh))), Equal.cong(Nat, Nat, z => Nat.add(SW.value(X.mul32(al, bh)), z), Nat.mul(v(ah), v(bl)), SW.value(X.mul32(ah, bl)), Equal.sym(Nat, SW.value(X.mul32(ah, bl)), Nat.mul(v(ah), v(bl)), W64M.mul32_value(ah, bl))))
85  +et = Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(SW.value(X.mul32(al, bh)), SW.value(X.mul32(ah, bl))), Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), C.shift(32n, C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), e12, Equal.trans(Nat, Nat.add(SW.value(X.mul32(al, bh)), SW.value(X.mul32(ah, bl))), Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), C.shift(64n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), C.shift(32n, C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), add_split(X.mul32(al, bh), X.mul32(ah, bl)), Equal.cong(Nat, Nat, z => Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), z), C.shift(64n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), WW.shift_comp(32n, 32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))))
86  +em = WA.val_eta(X.add(X.mul32(al, bh), X.mul32(ah, bl)))
87  +es = WA.acons(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))
88  +alg = m128_alg(Nat.mul(v(al), v(bl)), Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl)), Nat.mul(v(ah), v(bh)), v(X.lo(X.mul32(al, bl))), v(X.hi(X.mul32(al, bl))), SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), v(X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))), v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), ea, et, em, es)
89  +eP = Equal.trans(Nat, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(Nat.mul(v(al), v(bl)), C.shift(32n, Nat.mul(v(al), v(bh)))), Nat.add(C.shift(32n, Nat.mul(v(ah), v(bl))), C.shift(32n, C.shift(32n, Nat.mul(v(ah), v(bh)))))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))), WW.expand_k(32n, v(al), v(ah), v(bl), v(bh)), alg)
90  +eP64 = Equal.trans(Nat, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), eP, Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), z), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), Equal.sym(Nat, C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), WW.shift_comp(32n, 32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))))
91  +hpf = WA.prod_fits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh}), fit64(WU.U64{al, ah}), fit64(WU.U64{bl, bh}))
92  +ehT = Equal.trans(Nat, C.high(64n, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), C.high(64n, Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), Equal.cong(Nat, Nat, z => C.high(64n, z), Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), eP64), WW.high_u(64n, Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), fit64(WU.U64{X.lo(X.mul32(al, bl)), U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))})))
93  +hT = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, C.high(64n, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), ehT, fits_hk(64n, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), hpf))
94  +ev1 = Equal.trans(Nat, SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, v(X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), {==}, Equal.cong(Nat, Nat, z => Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, z)), v(X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))), S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))), W64M.b32_v(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))
95  +ein = Equal.trans(Nat, Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(X.mul32(ah, bh)), Nat.mul(v(ah), v(bh)), W64M.mul32_value(ah, bh)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(v(ah), v(bh)), z), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), ev1))
96  +hin = fits_lek(64n, Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), L.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))) == True{} : Bool}, Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Equal.sym(Nat, Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), ein), N.le_add_right(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), hT)
97  +evin = Equal.trans(Nat, SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), add64_exact(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}, hin), ein)
98  +ec2 = Equal.trans(Nat, SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0}), v(X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), val0(X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))))), Equal.trans(Nat, v(X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))))), S.bit_value(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), W64M.b32_v(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), Equal.cong(Bool, Nat, z => S.bit_value(z), U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))), P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), P64.add_lt(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))
99  +eo = Equal.trans(Nat, Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), evin), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), z), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0}), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), ec2))
100  +hout = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Equal.sym(Nat, Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), eo), hT)
101  +ePH = Equal.trans(Nat, SW.value(X.add(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), add64_exact(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0}, hout), eo)
102  Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, SW.value(X.add(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, z)), SW.value(X.add(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), ePH), Equal.sym(Nat, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), eP64))

Uses (46)

Used by (2)