		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass-curves

Short-weierstrass

Fixtype of elliptic curves over prime fields in short Weierstrass form.

This is a product type introduced by fty::defprod.

Fields

p — natp
a — natp
b — natp

Additional Requirements

The following invariant is enforced on the fields:

(and (> p 3) 
     (fep a p) 
     (fep b p) 
     (posp (mod (+ (* 4 a a a) (* 27 b b)) p)))

This kind of curve is specified by the prime p and the coefficients a and b; see short-weierstrass-curves. Thus, we formalize a curve as a triple of these numbers, via a fixtype product.

Because primep is slow on large numbers, we do not include this requirement into the fixtype; otherwise, it may take a long time to construct a value of this fixtype for a practical curve. We just require p to be greater than 3; see short-weierstrass-curves. We express the primality of p separately.

We require a and b to be in the prime field of p. We also require them to satisfy the condition ensuring that the cubic equation has no multiple roots; see short-weierstrass-curves. We express this condition by saying that 4 a^3 + 27 b^2 \mod p > 0, where the operations are not field operations: this formulation is equivalent to requiring 4 a^3 + 27 b^2 with field operation to be different from 0.

To fix the three components to satisfy the requirements above, we pick 5 for p, 0 for a, and 1 for b. It would be fine to pick 4 for p as far as this fixtype is concerned (since primality is not captured in the fixtype requirements), but we pick a prime (the smallest one above 3) since we know that this should be a prime.

Subtopics

Short-weierstrass-fix: Fixing function for short-weierstrass structures.
Short-weierstrass-equiv: Basic equivalence relation for short-weierstrass structures.
Make-short-weierstrass: Basic constructor macro for short-weierstrass structures.
Curve-scalar-*: Multiply an elliptic curve point by a scalar.
Short-weierstrass->p: Get the p field from a short-weierstrass.
Short-weierstrass->b: Get the b field from a short-weierstrass.
Short-weierstrass->a: Get the a field from a short-weierstrass.
Curve-group-+: Add two elliptic curve points.
Change-short-weierstrass: Modifying constructor for short-weierstrass structures.
Short-weierstrass-p: Recognizer for short-weierstrass structures.
Point-on-weierstrass-elliptic-curve-p: Test if a point is on an elliptic curve.
Curve-negate: Negate an elliptic curve point.
Weierstrass-elliptic-curve-p: Test if curve parameters are valid.