proofs/crypto/secp256k1/modexp.bend source

proofs/crypto/secp256k1/modexp.bend on the hub · documented module

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/modexp.src; edit the .srcimport Baseimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../math/natural/arith.bend as NR# Square-and-multiply steps on residues: with a = x^E mod m,# a a mod m = x^(2 E) mod m and a x mod m = x^(E + 1) mod m.def sq_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, a), 1n+mp) == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}:  %Equal.sym(Nat, a, Nat.mod(Nat.pow(x, e), 1n+mp), he) : {Nat.mod(Nat.mul(_, a), 1n+mp) == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}  %Equal.sym(Nat, a, Nat.mod(Nat.pow(x, e), 1n+mp), he) : {Nat.mod(Nat.mul(Nat.mod(Nat.pow(x, e), 1n+mp), _), 1n+mp) == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.pow(x, e), 1n+mp), Nat.mod(Nat.pow(x, e), 1n+mp)), 1n+mp), Nat.mod(Nat.mul(Nat.pow(x, e), Nat.mod(Nat.pow(x, e), 1n+mp)), 1n+mp), NR.mod_mul_l(mp, Nat.pow(x, e), Nat.mod(Nat.pow(x, e), 1n+mp))) : {_ == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.pow(x, e), Nat.mod(Nat.pow(x, e), 1n+mp)), 1n+mp), Nat.mod(Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), 1n+mp), NR.mod_mul_r(mp, Nat.pow(x, e), Nat.pow(x, e))) : {_ == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.double(e), Nat.add(e, e), NA.double_self(e)) : {Nat.mod(Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), 1n+mp) == Nat.mod(Nat.pow(x, _), 1n+mp) : Nat}  %Equal.sym(Nat, Nat.pow(x, Nat.add(e, e)), Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), NR.pow_add(x, e, e)) : {Nat.mod(Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}  {==}def 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}:  %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}  %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}  %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}  %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}  {==}# x^0 mod m = 1 for m > 1def pow0(+mp: Nat, +x: Nat, +h: {Nat.is_lt(1n, 1n+mp) == True{} : Bool}) -> {1n == Nat.mod(Nat.pow(x, 0n), 1n+mp) : Nat}:  Equal.sym(Nat, Nat.mod(1n, 1n+mp), 1n, NR.mod_of(0n, mp, 1n, h))