The Edwards-BLS12 complete twisted Edwards elliptic curve.

We define the Edwards-BLS12 curve,
as a constant value of the fixtype `twisted-edwards-curve`
of twisted Edwards elliptic curves.
We show that the curve is complete.

The prime and coefficients of Edwards-BLS12 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 Edwards-BLS12, such as recognizers of points in the curve's group and subgroup.

- Edwards-bls12-pointp
- Recognize elements of Edwards-BLS12 curve.
- Edwards-bls12-d
- The Edwards-BLS12 coefficient
d - Edwards-bls12-point->v
- The function
\mathcal{V} in TODO - Edwards-bls12-point->u
- The function
\mathcal{U} in TODO - Maybe-edwards-bls12-pointp
- Recognize Edwards-BLS12 points and
nil . - Edwards-bls12-q
- The Edwards-BLS12 base field prime
F_q . - Edwards-bls12-add
- Group addition on Edwards-BLS12.
- Edwards-bls12-mul-fast
- Fast scalar multiplication on Edwards-BLS12.
- Edwards-bls12-rstar-pointp
- Recognize elements of
r except the zero point. - Edwards-bls12-mul
- Scalar multiplication on Edwards-BLS12.
- Edwards-bls12-a
- The Edwards-BLS12 coefficient
a . - Edwards-bls12-r-pointp
- Recognize elements of
r . - Edwards-bls12-neg
- Group point negation on Edwards-BLS12.
- Edwards-bls12-curve
- The Edwards-BLS12 curve
- Edwards-bls12-h
- The elliptic curve cofactor.
- Edwards-bls12-r
- The prime number that is the order of the large subgroup of Edwards-BLS12.