def mpow_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64mont.bend:313

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/lib/nat.bend as N
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/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/w64add.bend as WA
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/w64dmrem.bend as DR
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

313# the Montgomery pow_mod is pow_mod_go on the values
314def mpow_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +mp: WU.U64, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hodd: {Nat.mod(1n+bp, 2n) == 1n : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}, +b: WU.U64, +hb: {Nat.is_lt(SW.value(b), 1n+bp) == True{} : Bool}, +e: WU.U64) -> {SW.value(X.mpow_m(b, e, WU.U64{ml, mh}, mp)) == M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)) : Nat}:
315  +hh : Nat = 1n+Nat.div(1n+bp, 2n)
316  +hH = MN.odd_hh(bp, hodd)
317  +bt = X.to_mont(b, WU.U64{ml, mh})
318  +eb = to_mont_v(one, h1, bp, ml, mh, hM, hz, b, hb)
319  +hnz = Equal.trans(Bool, X.is_zero(WU.U64{ml, mh}), Nat.is_eq(SW.value(WU.U64{ml, mh}), 0n), False{}, WA.is_zero_value(WU.U64{ml, mh}), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
320  +o1 = X.rem(WU.U64{1, 0}, WU.U64{ml, mh})
321  +eo = Equal.trans(Nat, SW.value(o1), Nat.mod(SW.value(WU.U64{1, 0}), SW.value(WU.U64{ml, mh})), Nat.mod(1n, 1n+bp), DR.divmod_rem(WU.U64{1, 0}, WU.U64{ml, mh}, hnz), Equal.cong(Nat, Nat, z => Nat.mod(1n, z), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
322  +lo1 = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(1n, 1n+bp), SW.value(o1), Equal.sym(Nat, SW.value(o1), Nat.mod(1n, 1n+bp), eo), mlt(bp, 1n))
323  +at = X.to_mont(o1, WU.U64{ml, mh})
324  +ea = Equal.trans(Nat, SW.value(at), Nat.mod(C.shift(64n, SW.value(o1)), 1n+bp), Nat.mod(C.shift(64n, Nat.mod(1n, 1n+bp)), 1n+bp), to_mont_v(one, h1, bp, ml, mh, hM, hz, o1, lo1), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(64n, z), 1n+bp), SW.value(o1), Nat.mod(1n, 1n+bp), eo))
325  +go = X.mpow_go(140n, WU.U64{ml, mh}, mp, bt, at, (e, X.is_zero(e)))
326  +eg = msim(one, h1, bp, WU.U64{ml, mh}, mp, hM, hinv, h63, hh, hH, 140n, bt, at, e, SW.value(b), Nat.mod(1n, 1n+bp), eb, ea, X.is_zero(e), SW.value(e), {==}, {==})
327  +lg = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), SW.value(go), Equal.sym(Nat, SW.value(go), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), mlt(bp, C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)))))
328  +l1 = N.lt_le_trans(1n, 2n, 1n+bp, {==}, L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, SW.value(WU.U64{ml, mh}), 1n+bp, hM, two_le(ml, mh, hz)))
329  +o = SW.value(X.mont(WU.U64{ml, mh}, mp, go, WU.U64{1, 0}))
330  +c1 = Equal.trans(Nat, Nat.mod(C.shift(64n, o), 1n+bp), Nat.mod(Nat.mul(SW.value(go), SW.value(WU.U64{1, 0})), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), mont_cong(one, h1, bp, WU.U64{ml, mh}, mp, hM, hinv, h63, go, WU.U64{1, 0}, lg, l1), Equal.trans(Nat, Nat.mod(Nat.mul(SW.value(go), SW.value(WU.U64{1, 0})), 1n+bp), Nat.mod(Nat.mul(SW.value(go), 1n), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), {==}, Equal.trans(Nat, Nat.mod(Nat.mul(SW.value(go), 1n), 1n+bp), Nat.mod(SW.value(go), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(SW.value(go), 1n), SW.value(go), NA.mul_one(SW.value(go))), Equal.trans(Nat, Nat.mod(SW.value(go), 1n+bp), Nat.mod(Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(go), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), NR.mod_mod(bp, C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))))))))
331  +c2 = MN.cancel(bp, hh, hH, 64n, o, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), c1)
332  +lo = mont_lt(one, h1, bp, WU.U64{ml, mh}, mp, hM, hinv, h63, go, WU.U64{1, 0}, lg, l1)
333  +hP = pm_lt(bp, 140n, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp), mlt(bp, 1n))
334  +z1 = Equal.sym(Nat, Nat.mod(o, 1n+bp), o, NR.mod_of(0n, bp, o, lo))
335  +z2 = NR.mod_of(0n, bp, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), hP)
336  +z3 = Equal.trans(Nat, Nat.mod(o, 1n+bp), Nat.mod(M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), 1n+bp), M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), c2, z2)
337  +z4 = Equal.trans(Nat, o, Nat.mod(o, 1n+bp), M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), z1, z3)
338  z4