def m32v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:52

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/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M

52# the two words of a 32 x 32 product
53def m32v(+a: U32, +b: U32) -> {Nat.add(v(X.lo(X.mul32(a, b))), C.shift(32n, v(X.hi(X.mul32(a, b))))) == Nat.mul(v(a), v(b)) : Nat}:
54  Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(a, b))), C.shift(32n, v(X.hi(X.mul32(a, b))))), SW.value(X.mul32(a, b)), Nat.mul(v(a), v(b)), Equal.sym(Nat, SW.value(X.mul32(a, b)), Nat.add(v(X.lo(X.mul32(a, b))), C.shift(32n, v(X.hi(X.mul32(a, b))))), WA.val_eta(X.mul32(a, b))), W64M.mul32_value(a, b))