def pow_mod_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/modpow.bend:93

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as LC

93# pow_mod(b, e, m) == Done{b^e mod m}   (Mathlib Nat.pow_mod; Python pow(b, e, m))
94def pow_mod_ok(+b: Nat, +e: Nat, +mp: Nat) -> {M.pow_mod(b, e, 1n+mp) == Done{Nat.mod(Nat.pow(b, e), 1n+mp)} : Result<&2, &2, M.MathError, Nat>}:
95  +m = {1n+mp : Nat}
96  +v = Equal.trans(Nat, M.pow_mod_go(e, m, e, Nat.mod(b, m), Nat.mod(1n, m)), Nat.mod(Nat.mul(Nat.mod(1n, m), Nat.pow(Nat.mod(b, m), e)), m), Nat.mod(Nat.pow(b, e), m), pm_go(e, mp, e, Nat.mod(b, m), Nat.mod(1n, m), N.le_refl(e), R.dm_lt(mp, 1n)),
97    Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(1n, m), Nat.pow(Nat.mod(b, m), e)), m), Nat.mod(Nat.mul(1n, Nat.pow(Nat.mod(b, m), e)), m), Nat.mod(Nat.pow(b, e), m), R.mod_mul_l(mp, 1n, Nat.pow(Nat.mod(b, m), e)),
98      Equal.trans(Nat, Nat.mod(Nat.mul(1n, Nat.pow(Nat.mod(b, m), e)), m), Nat.mod(Nat.pow(Nat.mod(b, m), e), m), Nat.mod(Nat.pow(b, e), m), Equal.cong(Nat, Nat, z => Nat.mod(z, m), Nat.mul(1n, Nat.pow(Nat.mod(b, m), e)), Nat.pow(Nat.mod(b, m), e), LC.one_mul(Nat.pow(Nat.mod(b, m), e))), mod_pow(mp, b, e))))
99  Equal.cong(Nat, Result<&2, &2, M.MathError, Nat>, z => Done{z}, M.pow_mod_go(e, m, e, Nat.mod(b, m), Nat.mod(1n, m)), Nat.mod(Nat.pow(b, e), m), v)