def mul_over_k

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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/typed/u32.bend as U32P
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X

257def mul_over_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {U32.is_zero(X.hi(X.mul32(a, b))) == C.fits(k, Nat.mul(v(a), v(b))) : Bool}:
258  +lo = X.lo(X.mul32(a, b))
259  +hi = X.hi(X.mul32(a, b))
260  +ek = L.subst(Nat, z => {Nat.add(v(lo), WD.sc(z, v(hi))) == Nat.mul(v(a), v(b)) : Nat}, 32n, k, Equal.sym(Nat, k, 32n, hk), prod_limbs(a, b))
261  %ek : {U32.is_zero(hi) == C.fits(k, _) : Bool}
262  %Equal.sym(Bool, C.fits(k, Nat.add(v(lo), WD.sc(k, v(hi)))), Nat.is_eq(v(hi), 0n), fits_split(k, v(lo), v(hi), U32P.val_lt(1n, {==}, k, hk, lo))) : {U32.is_zero(hi) == _ : Bool}
263  zero_nat(hi)