Jubjub
The Jubjub complete twisted Edwards elliptic curve [ZPS:5.4.9.3].
We define the Jubjub curve,
as a constant value of the fixtype ecurve::twisted-edwards-curve
of twisted Edwards elliptic curves.
We show that the curve is complete.
The prime and coefficient of Jubjub are formalized as nullary functions.
We keep disabled also their executable counterparts because
we generally want to treat them as algebraic quantities in proofs;
in particular, we want to avoid their combination into new constants
by the prime field normalizing rules.
We also define various notions related to Jubjub,
such as recognizers of points in the curve's group and subgroup.
Subtopics
- Jubjub-abst
- The function \mathsf{abst}_\mathbb{J} [ZPS:5.4.9.3].
- Jubjub-r-pointp
- Recognize elements of \mathbb{J}^{(r)} [ZPS:5.4.9.3].
- Jubjub-pointp
- Recognize elements of \mathbb{J} [ZPS:5.4.9.3].
- Jubjub-d
- The Jubjub coefficient d_\mathbb{J} [ZPS:5.4.9.3].
- Jubjub-montgomery
- The Montgomery form of the Jubjub curve [ZPS:A.2].
- Maybe-jubjub-pointp
- Recognize Jubjub points and nil.
- Jubjub-point->u
- The function \mathcal{U} in [ZPS:5.4.9.4].
- Jubjub-q
- The Jubjub prime q_\mathbb{J} [ZPS:5.4.9.3].
- Jubjub-point->v
- The function \mathcal{V} in [ZPS:5.4.9.4].
- Point-on-jubjub-p
- Check if a point is on the Jubjub curve [ZPS:5.4.9.3].
- Jubjub-rstar-pointp
- Recognize elements of \mathbb{J}^{(r)*} [ZPS:5.4.9.3].
- Jubjub-add
- Group addition [ZPS:4.1.8], on Jubjub.
- Jubjub-r-properties
- Properties about jubjub-r-pointp.
- Jubjub-point-abscissa-is-not-1
- A Jubjub point cannot have abscissa 1.
- Jubjub-mul
- Scalar multiplication [ZPS:4.1.8], on Jubjub.
- Jubjub-curve
- The Jubjub curve [ZPS:5.4.9.3].
- Jubjub-a
- The Jubjub coefficient a_\mathbb{J} [ZPS:5.4.9.3].
- Jubjub-neg
- Group negation, on Jubjub.
- Jubjub-r
- The constant r_\mathbb{J} in [ZPS:5.4.9.3].
- Jubjub-point-satisfies-curve-equation
- A Jubjub point satisfies the curve equation.
- Jubjub-h
- The constant h_\mathbb{J} in [ZPS:5.4.9.3].
- Jubjub-mul-of-2
- Doubling a point is like adding the point to itself.
- *jubjub-l*
- The constant \ell_\mathbb{J} [ZPS:5.4.9.3].
