|
|
|---|
|
|
|
|---|
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.