def MulMod.value

bend-collections-laws-crypto@1.0.0.0 · spec/math/w64.bend:95

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X

95# a, b < m: the product reduced, with no 64-bit overflow on the way
96def MulMod.value(+a: W.U64, +b: W.U64, +m: W.U64, +ha: {Nat.is_lt(value(a), value(m)) == True{} : Bool}, +hb: {Nat.is_lt(value(b), value(m)) == True{} : Bool}) -> Type:
97  {value(X.mulmod(a, b, m)) == Nat.mod(Nat.mul(value(a), value(b)), value(m)) : Nat}