def mul_step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/modexp.bend:18

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

18def mul_step(+mp: Nat, +x: Nat, +e: Nat, +a: Nat, +he: {a == Nat.mod(Nat.pow(x, e), 1n+mp) : Nat}) -> {Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(Nat.pow(x, Nat.add(e, 1n)), 1n+mp) : Nat}:
19  %Equal.sym(Nat, a, Nat.mod(Nat.pow(x, e), 1n+mp), he) : {Nat.mod(Nat.mul(_, x), 1n+mp) == Nat.mod(Nat.pow(x, Nat.add(e, 1n)), 1n+mp) : Nat}
20  %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.pow(x, e), 1n+mp), x), 1n+mp), Nat.mod(Nat.mul(Nat.pow(x, e), x), 1n+mp), NR.mod_mul_l(mp, Nat.pow(x, e), x)) : {_ == Nat.mod(Nat.pow(x, Nat.add(e, 1n)), 1n+mp) : Nat}
21  %Equal.sym(Nat, Nat.pow(x, Nat.add(e, 1n)), Nat.mul(Nat.pow(x, e), Nat.pow(x, 1n)), NR.pow_add(x, e, 1n)) : {Nat.mod(Nat.mul(Nat.pow(x, e), x), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}
22  %Equal.sym(Nat, Nat.mul(x, 1n), x, NA.mul_one(x)) : {Nat.mod(Nat.mul(Nat.pow(x, e), x), 1n+mp) == Nat.mod(Nat.mul(Nat.pow(x, e), _), 1n+mp) : Nat}
23  {==}