def mul1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:110

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/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A

110def mul1(+x: U32, +c: U32, +b: Nat, +bc: Nat, +hx: {Nat.is_le(v(x), b) == True{} : Bool}, +hc: {Nat.is_le(v(c), bc) == True{} : Bool}, +hf: {C.fits(32n, Nat.mul(b, bc)) == True{} : Bool}) -> {v(U32.mul(x, c)) == Nat.mul(v(x), v(c)) : Nat}:
111  A.tr(v(U32.mul(x, c)), C.low(32n, Nat.mul(v(x), v(c))), Nat.mul(v(x), v(c)), SH.mul_low(x, c),
112    WW.low_fit(32n, Nat.mul(v(x), v(c)), A.fits_le(32n, Nat.mul(v(x), v(c)), Nat.mul(b, bc), A.le_mul2(v(x), v(c), b, bc, hx, hc), hf)))