		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-curve

Fixtype of elliptic curves over prime fields in twisted Edwards form.

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

Fields

p — natp
a
d

Additional Requirements

The following invariant is enforced on the fields:

(and (dm::primep p) 
     (> p 2) 
     (fep a p) 
     (fep d p) 
     (not (equal a d)) 
     (not (equal a 0)) 
     (not (equal d 0)))

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

We require p to be a prime greater than 2; see twisted-edwards.

We require a and d to be in the prime field of p. We also require them to be distinct and non-zero.

To fix the three components to satisfy the requirements above, we pick 3 for p, 1 for a, and 2 for d.

Subtopics

Twisted-edwards-curve-fix: Fixing function for twisted-edwards-curve structures.
Twisted-edwards-curve-equiv: Basic equivalence relation for twisted-edwards-curve structures.
Twisted-edwards-curvep: Recognizer for twisted-edwards-curve structures.
Make-twisted-edwards-curve: Basic constructor macro for twisted-edwards-curve structures.
Twisted-edwards-curve->p: Get the p field from a twisted-edwards-curve.
Change-twisted-edwards-curve: Modifying constructor for twisted-edwards-curve structures.
Twisted-edwards-curve->d: Get the d field from a twisted-edwards-curve.
Twisted-edwards-curve->a: Get the a field from a twisted-edwards-curve.