proofs/crypto/secp256k1/modexp.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend as Modexp

import Base
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR

Definitions

@+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}

@+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}

@+mp:Nat -> @+x:Nat -> @+h:{Nat.is_lt(1n, 1n+mp) == True{} : Bool} -> {1n == Nat.mod(Nat.pow(x, 0n), 1n+mp) : Nat}