		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-curve

Fixtype of elliptic curve over prime fields in Montgomery form.

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

Fields

p
a
b

Additional Requirements

The following invariant is enforced on the fields:

(and (dm::primep p) 
     (> p 2) 
     (fep a p) 
     (fep b p) 
     (not (equal a 2)) 
     (not (equal a (mod -2 p))) 
     (not (equal b 0)))

This kind of curve is specified by the prime p and the coefficients A and B; see montgomery. 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 montgomery.

We require A and B to be in the prime field of p. We also require them to satisfy the condition montgomery.

To fix the three components to satisfy the requirements above, we pick 3 for p, 0 for A, and 1 for B.

Subtopics

Montgomery-curve-fix: Fixing function for montgomery-curve structures.
Montgomery-curve-equiv: Basic equivalence relation for montgomery-curve structures.
Make-montgomery-curve: Basic constructor macro for montgomery-curve structures.
Montgomery-curvep: Recognizer for montgomery-curve structures.
Change-montgomery-curve: Modifying constructor for montgomery-curve structures.
Montgomery-curve->b: Get the b field from a montgomery-curve.
Montgomery-curve->a: Get the a field from a montgomery-curve.
Montgomery-curve->p: Get the p field from a montgomery-curve.