		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-interface

Secp256k1-priv-to-pub

Calculate a secp256k1 public key from a private key.

We constrain this function to return a public key unconditionally.

We also constrain this function to fix its argument to a private key.

Definitions and Theorems

Theorem: secp256k1-pub-key-p-of-secp256k1-priv-to-pub

(defthm secp256k1-pub-key-p-of-secp256k1-priv-to-pub
  (secp256k1-pub-key-p (secp256k1-priv-to-pub priv)))

Theorem: secp256k1-priv-to-pub-fixes-input-priv

(defthm secp256k1-priv-to-pub-fixes-input-priv
  (equal (secp256k1-priv-to-pub (secp256k1-priv-key-fix priv))
         (secp256k1-priv-to-pub priv)))

Theorem: secp256k1-priv-key-equiv-implies-equal-secp256k1-priv-to-pub-1

(defthm
     secp256k1-priv-key-equiv-implies-equal-secp256k1-priv-to-pub-1
  (implies (secp256k1-priv-key-equiv priv priv-equiv)
           (equal (secp256k1-priv-to-pub priv)
                  (secp256k1-priv-to-pub priv-equiv)))
  :rule-classes (:congruence))