def pm_go

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

import Base
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 A
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/math/natural/arith.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as B

72# the loop: acc < m, e <= fuel give pow_mod_go == acc base^e mod m
73def pm_go(fuel: Nat, +mp: Nat, +e: Nat, +base: Nat, +acc: Nat, +he: {Nat.is_le(e, fuel) == True{} : Bool}, +hacc: {Nat.is_lt(acc, 1n+mp) == True{} : Bool}) -> {M.pow_mod_go(fuel, 1n+mp, e, base, acc) == Nat.mod(Nat.mul(acc, Nat.pow(base, e)), 1n+mp) : Nat}:
74  match fuel e:
75    case 0n 0n:
76      %Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc)) : {acc == Nat.mod(_, 1n+mp) : Nat}
77      Equal.sym(Nat, Nat.mod(acc, 1n+mp), acc, R.mod_of(0n, mp, acc, hacc))
78    case 0n 1n+ep:
79      Empty.absurd({M.pow_mod_go(0n, 1n+mp, 1n+ep, base, acc) == Nat.mod(Nat.mul(acc, Nat.pow(base, 1n+ep)), 1n+mp) : Nat}, L.false_true(he))
80    case 1n+f 0n:
81      %Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc)) : {acc == Nat.mod(_, 1n+mp) : Nat}
82      Equal.sym(Nat, Nat.mod(acc, 1n+mp), acc, R.mod_of(0n, mp, acc, hacc))
83    case 1n+ +f 1n+ +ep:
84      +m = {1n+mp : Nat}
85      +e2 = Nat.div(1n+ep, 2n)
86      +bit = Nat.mod(1n+ep, 2n)
87      +b2 = Nat.mod(Nat.mul(base, base), m)
88      +acc2 = M.pow_mod_odd(m, bit, base, acc)
89      +ih = pm_go(f, mp, e2, b2, acc2, N.le_trans(e2, ep, f, N.lt_succ_le(e2, ep, B.half_lt(ep)), he), odd_lt(mp, bit, base, acc, hacc))
90      %Equal.sym(Nat, 1n+ep, Nat.add(Nat.double(e2), bit), B.half_eq(1n+ep)) : {M.pow_mod_go(f, m, e2, b2, acc2) == Nat.mod(Nat.mul(acc, Nat.pow(base, _)), m) : Nat}
91      Equal.trans(Nat, M.pow_mod_go(f, m, e2, b2, acc2), Nat.mod(Nat.mul(acc2, Nat.pow(b2, e2)), m), Nat.mod(Nat.mul(acc, Nat.pow(base, Nat.add(Nat.double(e2), bit))), m), ih, pm_bit(mp, e2, bit, B.half_rem(1n+ep), base, acc))