		Search-engine friendly clone of the ACL2 documentation.

Secp256k1

Secp256k1-negate

Negate an elliptic curve point.

(secp256k1-negate point) finds the inverse of point with respect to the secp256k1 elliptic curve group operation.

The result is a point on the elliptic curve.

Definitions and Theorems

Function: secp256k1-negate

(defun secp256k1-negate (point)
 (declare
  (xargs
       :guard (and (pointp point)
                   (point-in-pxp-p point (secp256k1-field-prime)))))
 (curve-negate point (secp256k1-field-prime)))

Theorem: pointp-of-secp256k1-negate

(defthm pointp-of-secp256k1-negate
  (implies (pointp point)
           (pointp (secp256k1-negate point))))

Theorem: point-in-pxp-p-of-secp256k1-negate

(defthm point-in-pxp-p-of-secp256k1-negate
  (implies (and (pointp point)
                (point-in-pxp-p point (secp256k1-field-prime)))
           (point-in-pxp-p (secp256k1-negate point)
                           (secp256k1-field-prime))))

Theorem: point-on-weierstrass-elliptic-curve-p-of-secp256k1-negate

(defthm point-on-weierstrass-elliptic-curve-p-of-secp256k1-negate
 (implies
     (and (pointp point)
          (point-in-pxp-p point (secp256k1-field-prime))
          (point-on-weierstrass-elliptic-curve-p
               point (secp256k1-field-prime)
               (secp256k1-a)
               (secp256k1-b)))
     (point-on-weierstrass-elliptic-curve-p (secp256k1-negate point)
                                            (secp256k1-field-prime)
                                            (secp256k1-a)
                                            (secp256k1-b))))