def mul_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:355

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

355def mul_value(+a: WU.U64, +b: WU.U64) -> SW.Mul.value(a, b):
356  match a b:
357    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
358      +m1 = U32.mul(al, bh)
359      +m2 = U32.mul(ah, bl)
360      +t = U32.add(m1, m2)
361      +kc = Nat.add(bv(P64.carry32(m1, m2)), Nat.add(W64M.mex(al, bh), W64M.mex(ah, bl)))
362      +A = Nat.mul(v(al), v(bl))
363      +H = Nat.mul(v(ah), v(bh))
364      +mk = WW.mul_k(32n, v(al), v(ah), v(bl), v(bh), v(t), kc, cross_eq(al, ah, bl, bh))
365      +Y = Nat.add(kc, H)
366      +p = X.mul32(al, bl)
367      +q = {WU.U64{0, t} : WU.U64}
368      av = add_value(p, q)
369      +elp = Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(z, C.shift(32n, v(t)))), SW.value(p), A, W64M.mul32_value(al, bl))
370      +em = Equal.trans(Nat, Nat.mul(val(al, ah), val(bl, bh)), Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(32n, C.shift(32n, Y))), Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(64n, Y)), mk, Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(32n, v(t))), z), C.shift(32n, C.shift(32n, Y)), C.shift(64n, Y), Equal.sym(Nat, C.shift(64n, Y), C.shift(32n, C.shift(32n, Y)), WW.shift_comp(32n, 32n, Y))))
371      +elm = Equal.trans(Nat, C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), C.low(64n, Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(64n, Y))), C.low(64n, Nat.add(A, C.shift(32n, v(t)))), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.mul(val(al, ah), val(bl, bh)), Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(64n, Y)), em), WW.low_add_shift(64n, Nat.add(A, C.shift(32n, v(t))), Y))
372      Equal.trans(Nat, SW.value(X.add(p, q)), C.low(64n, Nat.add(SW.value(p), C.shift(32n, v(t)))), C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), av, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(p), C.shift(32n, v(t)))), C.low(64n, Nat.add(A, C.shift(32n, v(t)))), C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), elp, Equal.sym(Nat, C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), C.low(64n, Nat.add(A, C.shift(32n, v(t)))), elm)))