def mpow_v

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

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/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as MN
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64mont.bend as UM

231def mpow_v(+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}, +b: U32, +hb: {Nat.is_lt(v(b), 1n+bp) == True{} : Bool}, +e: U32, +hodd: {Nat.mod(1n+bp, 2n) == 1n : Nat}) -> {v(X.mpow32_m(b, e, m, mp)) == M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)) : Nat}:
232  +hh : Nat = 1n+Nat.div(1n+bp, 2n)
233  +hH = MN.odd_hh(bp, hodd)
234  +bt = X.mod32(WU.U64{0, b}, m)
235  +eb = to_mont_v(bp, m, hM, b)
236  +o1 = U32.mod(1, m)
237  +eo = Equal.trans(Nat, v(o1), Nat.mod(v(1), v(m)), Nat.mod(1n, 1n+bp), UD.mod_nat(1, m, hdz(bp, m, hM)), Equal.cong(Nat, Nat, z => Nat.mod(1n, z), v(m), 1n+bp, hM))
238  +at = X.mod32(WU.U64{0, o1}, m)
239  +ea = Equal.trans(Nat, v(at), Nat.mod(C.shift(32n, v(o1)), 1n+bp), Nat.mod(C.shift(32n, Nat.mod(1n, 1n+bp)), 1n+bp), to_mont_v(bp, m, hM, o1), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), 1n+bp), v(o1), Nat.mod(1n, 1n+bp), eo))
240  +go = X.mpow32_go(140n, m, mp, bt, at, (e, U32.is_zero(e)))
241  +eg = msim(one, h1, bp, m, mp, hM, hinv, hh, hH, 140n, bt, at, e, v(b), Nat.mod(1n, 1n+bp), eb, ea, U32.is_zero(e), v(e), {==}, {==})
242  +lg = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), v(go), Equal.sym(Nat, v(go), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), mlt(bp, C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)))))
243  +hT1 = g1_lt(bp, v(go), lg)
244  +o = v(X.mont32(m, mp, go, 1))
245  +c1 = Equal.trans(Nat, Nat.mod(C.shift(32n, o), 1n+bp), Nat.mod(Nat.mul(v(go), v(1)), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), mont_cong(one, h1, bp, m, mp, hM, hinv, go, 1, hT1), Equal.trans(Nat, Nat.mod(Nat.mul(v(go), v(1)), 1n+bp), Nat.mod(Nat.mul(v(go), 1n), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), {==}, Equal.trans(Nat, Nat.mod(Nat.mul(v(go), 1n), 1n+bp), Nat.mod(v(go), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(v(go), 1n), v(go), NA.mul_one(v(go))), Equal.trans(Nat, Nat.mod(v(go), 1n+bp), Nat.mod(Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), v(go), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), NR.mod_mod(bp, C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))))))))
246  +c2 = MN.cancel(bp, hh, hH, 32n, o, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), c1)
247  +lo = mont_lt(one, h1, bp, m, mp, hM, hinv, go, 1, hT1)
248  +hP = UM.pm_lt(bp, 140n, v(e), v(b), Nat.mod(1n, 1n+bp), mlt(bp, 1n))
249  Equal.trans(Nat, o, Nat.mod(o, 1n+bp), M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), Equal.sym(Nat, Nat.mod(o, 1n+bp), o, NR.mod_of(0n, bp, o, lo)), Equal.trans(Nat, Nat.mod(o, 1n+bp), Nat.mod(M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), 1n+bp), M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), c2, NR.mod_of(0n, bp, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), hP)))