def mok_inv

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

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S

266def mok_inv(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}) -> {1n+C.low(32n, Nat.mul(1n+bp, v(X.minv32(m)))) == C.shift(32n, one) : Nat}:
267  mok_inv_o(one, h1, bp, m, hM, 4294967295, {==}, W64S.and_r(U32.is_eq(U32.and(m, 1), 1), U32.is_eq(U32.mul(m, X.minv32(m)), 4294967295), hok))