		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-pub-key

Secp256k1-pub-key-fix

Fixer for secp256k1-pub-key.

Signature
(secp256k1-pub-key-fix x) → fixed-x
Arguments: x — Guard (secp256k1-pub-key-p x).
Returns: fixed-x — Type (secp256k1-pub-key-p fixed-x).

Definitions and Theorems

Function: secp256k1-pub-key-fix

(defun secp256k1-pub-key-fix (x)
  (declare (xargs :guard (secp256k1-pub-key-p x)))
  (mbe :logic
       (if (secp256k1-pub-key-p x)
           x
         (secp256k1-point 1 1))
       :exec x))

Theorem: secp256k1-pub-key-p-of-secp256k1-pub-key-fix

(defthm secp256k1-pub-key-p-of-secp256k1-pub-key-fix
  (b* ((fixed-x (secp256k1-pub-key-fix x)))
    (secp256k1-pub-key-p fixed-x))
  :rule-classes :rewrite)

Theorem: secp256k1-pub-key-fix-when-secp256k1-pub-key-p

(defthm secp256k1-pub-key-fix-when-secp256k1-pub-key-p
  (implies (secp256k1-pub-key-p x)
           (equal (secp256k1-pub-key-fix x) x)))