def mok_inv_o

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

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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

256# over an open all-ones word o (a literal 2^32 - 1 is expanded in unary)
257def mok_inv_o(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +o: U32, +po: {o == U32{WD.mask(32n, 32n)} : U32}, +heq: {U32.is_eq(U32.mul(m, X.minv32(m)), o) == True{} : Bool}) -> {1n+C.low(32n, Nat.mul(1n+bp, v(X.minv32(m)))) == C.shift(32n, one) : Nat}:
258  +mp = X.minv32(m)
259  +w = U32.mul(m, mp)
260  +h = Equal.trans(Bool, Nat.is_eq(v(w), v(o)), U32.is_eq(U32.mul(m, X.minv32(m)), o), True{}, Equal.sym(Bool, U32.is_eq(U32.mul(m, X.minv32(m)), o), Nat.is_eq(v(w), v(o)), LW.eq_nat(w, o)), heq)
261  +e1 = N.eq_from_is_eq(v(w), v(o), h)
262  +e2 = Equal.trans(Nat, C.low(32n, Nat.mul(1n+bp, v(mp))), C.low(32n, Nat.mul(v(m), v(mp))), v(w), Equal.cong(Nat, Nat, z => C.low(32n, Nat.mul(z, v(mp))), 1n+bp, v(m), Equal.sym(Nat, v(m), 1n+bp, hM)), Equal.sym(Nat, v(w), C.low(32n, Nat.mul(v(m), v(mp))), SH.mul_low(m, mp)))
263  +e3 = Equal.trans(Nat, 1n+v(o), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, o, po), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
264  Equal.trans(Nat, 1n+C.low(32n, Nat.mul(1n+bp, v(mp))), 1n+v(o), C.shift(32n, one), Equal.cong(Nat, Nat, z => 1n+z, C.low(32n, Nat.mul(1n+bp, v(mp))), v(o), Equal.trans(Nat, C.low(32n, Nat.mul(1n+bp, v(mp))), v(w), v(o), e2, e1)), e3)