def ops_mul_one

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/u32laws.bend:246

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as NM
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/u32div.bend as UD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
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/math/u64/u64div.bend as PD
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/src/math/w64.bend as X

246def ops_mul_one(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> {v(U32.mul(a, b)) == Nat.mul(v(a), v(b)) : Nat}:
247  +lo = X.lo(X.mul32(a, b))
248  +hi = X.hi(X.mul32(a, b))
249  +e0 = Equal.trans(Nat, v(lo), Nat.add(v(lo), 0n), Nat.add(v(lo), WD.sc(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), 0n), v(lo), N.add_zero(v(lo))), W64M.cong_r(v(lo), 0n, WD.sc(32n, v(hi)), Equal.trans(Nat, 0n, WD.sc(32n, 0n), WD.sc(32n, v(hi)), Equal.sym(Nat, WD.sc(32n, 0n), 0n, A.sc_zero(32n)), W64M.cong_sc(32n, 0n, v(hi), Equal.sym(Nat, v(hi), 0n, hi_zero(a, b, h))))))
250  +ep = Equal.trans(Nat, v(lo), Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.mul(v(a), v(b)), e0, prod_limbs(a, b))
251  +lt = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, v(lo), Nat.mul(v(a), v(b)), ep, UD.vb(one, h1, lo))
252  PD.mul32(one, h1, a, b, lt)