		Search-engine friendly clone of the ACL2 documentation.

Secp256k1

Secp256k1*

Multiply an elliptic curve point by a scalar.

(secp256k1* s point) 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 secp256k1 elliptic curve. If it is not, a guard violation occurs.

The result is a point on the elliptic curve.

Definitions and Theorems

Function: secp256k1*

(defun secp256k1* (s point)
 (declare
   (xargs :guard (and (natp s)
                      (pointp point)
                      (point-in-pxp-p point (secp256k1-field-prime))
                      (point-on-weierstrass-elliptic-curve-p
                           point (secp256k1-field-prime)
                           (secp256k1-a)
                           (secp256k1-b)))))
 (curve-scalar-* s point (secp256k1-field-prime)
                 (secp256k1-a)
                 (secp256k1-b)))