def mont_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:155

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X

155# 32-bit Montgomery multiplication: mont32(a, b) < m and mont32(a, b) 2^32 == a b (mod m)
156def mont_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +a: U32, +b: U32, +hT: {Nat.is_lt(Nat.mul(v(a), v(b)), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}) -> {Nat.is_lt(v(X.mont32(m, mp, a, b)), 1n+bp) == True{} : Bool}:
157  rp_lt_m(one, h1, bp, m, mp, hM, hinv, X.mul32(a, b), X.mul32(U32.mul(X.lo(X.mul32(a, b)), mp), m), Nat.mul(v(a), v(b)), m32v(a, b), hT, ep_m(bp, m, hM, U32.mul(X.lo(X.mul32(a, b)), mp)))