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