		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass

Curve-group-+

Add two elliptic curve points.

(curve-group-+ point1 point2 p a b) adds point1 and point2 using the elliptic curve group operation. The two input points must be on the Short Weierstrass elliptic curve defined by p, a, and b. If either is not, a guard violation occurs.

The result is a point on the elliptic curve.

Definitions and Theorems

Function: curve-group-+

(defun curve-group-+ (point1 point2 p a b)
 (declare
   (xargs
        :guard
        (and (dm::primep p)
             (< 3 p)
             (fep a p)
             (fep b p)
             (pointp point1)
             (pointp point2)
             (point-in-pxp-p point1 p)
             (point-in-pxp-p point2 p)
             (point-on-weierstrass-elliptic-curve-p point1 p a b)
             (point-on-weierstrass-elliptic-curve-p point2 p a b))))
 (declare (ignore b))
 (if (equal point1 :infinity)
     point2
   (if (equal point2 :infinity)
       point1
     (let ((x1 (car point1))
           (y1 (cdr point1))
           (x2 (car point2))
           (y2 (cdr point2)))
       (if (= x1 x2)
           (if (= (add y1 y2 p) 0)
               :infinity
             (let* ((slope (div (add (mul 3 (mul x1 x1 p) p) a p)
                                (mul 2 y1 p)
                                p))
                    (x3 (sub (mul slope slope p)
                             (mul 2 x1 p)
                             p))
                    (y3 (sub (mul slope (sub x1 x3 p) p) y1 p)))
               (cons x3 y3)))
         (let* ((slope (div (sub y2 y1 p) (sub x2 x1 p) p))
                (x3 (sub (sub (mul slope slope p) x1 p)
                         x2 p))
                (y3 (sub (mul slope (sub x1 x3 p) p) y1 p)))
           (cons x3 y3)))))))