		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass

Curve-scalar-*

Multiply an elliptic curve point by a scalar.

(curve-scalar-* s point p a b) applies the elliptic group operation to s copies of point.

Since we use + to describe the group operation, this operation can be thought of as multiplying point by the scalar s.

(Alternatively, for those who think of the group operation as multiplication, this operation can be thought of as exponentiation.)

point must be on the Short Weierstrass elliptic curve defined by p, a, and b. If it is not, a guard violation occurs.

The result is a point on the elliptic curve.

Definitions and Theorems

Function: curve-scalar-*

(defun curve-scalar-* (s point p a b)
 (declare
  (xargs :guard
         (and (natp s)
              (dm::primep p)
              (< 3 p)
              (fep a p)
              (fep b p)
              (pointp point)
              (point-in-pxp-p point p)
              (point-on-weierstrass-elliptic-curve-p point p a b))))
 (if (zp s)
     :infinity
  (if (= s 1)
      point
    (if
     (evenp s)
     (let
        ((half-curve-scalar-* (curve-scalar-* (/ s 2) point p a b)))
       (curve-group-+ half-curve-scalar-*
                      half-curve-scalar-* p a b))
     (curve-group-+ point
                    (curve-scalar-* (- s 1) point p a b)
                    p a b)))))