		Search-engine friendly clone of the ACL2 documentation.

Secp256k1

Secp256k1+

Add two elliptic curve points.

(secp256k1+ point1 point2) adds point1 and point2 using the elliptic curve group operation. The two input points must be on the secp256k1 elliptic curve. If either is not, a guard violation occurs.

The result is a point on the elliptic curve.

Definitions and Theorems

Function: secp256k1+

(defun secp256k1+ (point1 point2)
 (declare
  (xargs :guard (and (pointp point1)
                     (pointp point2)
                     (point-in-pxp-p point1 (secp256k1-field-prime))
                     (point-in-pxp-p point2 (secp256k1-field-prime))
                     (point-on-weierstrass-elliptic-curve-p
                          point1 (secp256k1-field-prime)
                          (secp256k1-a)
                          (secp256k1-b))
                     (point-on-weierstrass-elliptic-curve-p
                          point2 (secp256k1-field-prime)
                          (secp256k1-a)
                          (secp256k1-b)))))
 (curve-group-+ point1 point2 (secp256k1-field-prime)
                (secp256k1-a)
                (secp256k1-b)))