def to_mont_v

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

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64D

220# x 2^32 mod m by one 64 / 32 reduction
221def to_mont_v(+bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +x: U32) -> {v(X.mod32(WU.U64{0, x}, m)) == Nat.mod(C.shift(32n, v(x)), 1n+bp) : Nat}:
222  Equal.trans(Nat, v(X.mod32(WU.U64{0, x}, m)), Nat.mod(SW.value(WU.U64{0, x}), v(m)), Nat.mod(C.shift(32n, v(x)), 1n+bp), W64D.mod32_value(WU.U64{0, x}, m, hdz(bp, m, hM)), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, v(x)), z), v(m), 1n+bp, hM))