def cross_eq

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

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/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
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

342# the cross terms: al bh + ah bl == t + 2^32 kc, t their wrapped sum
343def cross_eq(+al: U32, +ah: U32, +bl: U32, +bh: U32) -> {Nat.add(v(U32.add(U32.mul(al, bh), U32.mul(ah, bl))), C.shift(32n, Nat.add(bv(P64.carry32(U32.mul(al, bh), U32.mul(ah, bl))), Nat.add(W64M.mex(al, bh), W64M.mex(ah, bl))))) == Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))) : Nat}:
344  +m1 = U32.mul(al, bh)
345  +m2 = U32.mul(ah, bl)
346  +t = U32.add(m1, m2)
347  +c = P64.carry32(m1, m2)
348  +x1 = W64M.mex(al, bh)
349  +x2 = W64M.mex(ah, bl)
350  +e1 = mcons(al, bh)
351  +e2 = mcons(ah, bl)
352  +et = acons(m1, m2)
353  Equal.sym(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.add(v(m2), C.shift(32n, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.mul(v(ah), v(bl))), Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.add(v(m2), C.shift(32n, x2))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(v(ah), v(bl))), Nat.mul(v(al), v(bh)), Nat.add(v(m1), C.shift(32n, x1)), Equal.sym(Nat, Nat.add(v(m1), C.shift(32n, x1)), Nat.mul(v(al), v(bh)), e1)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(m1), C.shift(32n, x1)), z), Nat.mul(v(ah), v(bl)), Nat.add(v(m2), C.shift(32n, x2)), Equal.sym(Nat, Nat.add(v(m2), C.shift(32n, x2)), Nat.mul(v(ah), v(bl)), e2))), Equal.trans(Nat, Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.add(v(m2), C.shift(32n, x2))), Nat.add(Nat.add(v(m1), v(m2)), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), W64M.add4(v(m1), C.shift(32n, x1), v(m2), C.shift(32n, x2)), Equal.trans(Nat, Nat.add(Nat.add(v(m1), v(m2)), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(v(m1), v(m2)), Nat.add(v(t), C.shift(32n, bv(c))), Equal.sym(Nat, Nat.add(v(t), C.shift(32n, bv(c))), Nat.add(v(m1), v(m2)), et)), Equal.trans(Nat, Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), C.shift(32n, Nat.add(x1, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), z), Nat.add(C.shift(32n, x1), C.shift(32n, x2)), C.shift(32n, Nat.add(x1, x2)), Equal.sym(Nat, C.shift(32n, Nat.add(x1, x2)), Nat.add(C.shift(32n, x1), C.shift(32n, x2)), WW.shift_add(32n, x1, x2))), Equal.trans(Nat, Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), C.shift(32n, Nat.add(x1, x2))), Nat.add(v(t), Nat.add(C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2)))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), NA.add_assoc(v(t), C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2))), Equal.cong(Nat, Nat, z => Nat.add(v(t), z), Nat.add(C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2))), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2))), Equal.sym(Nat, C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2))), Nat.add(C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2))), WW.shift_add(32n, bv(c), Nat.add(x1, x2))))))))))