def mul32_value

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64mul.bend:347

import Base
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

347# Mul32.value: the full product of two U32
348def mul32_value(+a: U32, +b: U32) -> SW.Mul32.value(a, b):
349  %Equal.sym(WU.U64, X.mul32(a, b), mul32g(a, b, 65536, 65535), impl(a, b)) : {SW.value(_) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
350  mulval(1n, {==}, a, b, 65536, {==}, 65535, {==})