The Edwards curve used by Elligator 1

This file specializes the general Elligator.TwistedEdwardsCurve API to the untwisted Edwards curve and parameter produced by Elligator 1.

The general curve definition deliberately does not depend on a finite field, its cardinality, or the Elligator parameter s; those assumptions occur only in the specialization proving that d s is a valid coefficient.

Main results

• curve: the untwisted Edwards curve with the paper's coefficient d(s).
• curve_isValid: the Elligator hypotheses imply that d(s) is a valid Edwards coefficient.
• EOverF: the set of affine field-valued points satisfying the Elligator 1 curve equation.
• EOverF_eq_affinePoints: EOverF agrees with the general twisted-Edwards affine-point set.

References

See [bernstein2013a], Section 3.

def Elligator.Elligator1.edwardsCurve {F : Type u_1} [Field F] (d : F) : TwistedEdwardsCurve F

The general Edwards curve with coefficient d. This is an alias for the a = 1 specialization of a twisted Edwards curve.

Equations

• Elligator.Elligator1.edwardsCurve d = Elligator.TwistedEdwardsCurve.ofD d

def Elligator.Elligator1.edwardsCurveEquation {F : Type u_1} [Field F] (x y : F) (d : { d : F // d ≠ 0 ∧ d ≠ 1 }) : Prop

edwardsCurveEquation is the standard Edwards curve equation. The subtype argument is preserved for compatibility. New generic developments should normally use (edwardsCurve d).Equation x y, and carry coefficient validity separately via TwistedEdwardsCurve.IsValid.

Equations

• Elligator.Elligator1.edwardsCurveEquation x y d = (Elligator.Elligator1.edwardsCurve ↑d).Equation x y

@[simp]

theorem Elligator.Elligator1.edwardsCurveEquation_iff {F : Type u_1} [Field F] (x y : F) (d : { d : F // d ≠ 0 ∧ d ≠ 1 }) : edwardsCurveEquation x y d ↔ x ^ 2 + y ^ 2 = 1 + ↑d * x ^ 2 * y ^ 2

def Elligator.Elligator1.curve {F : Type u_1} [Field F] (s : F) : TwistedEdwardsCurve F

The Edwards curve selected by the Elligator 1 parameter s.

Equations

• Elligator.Elligator1.curve s = Elligator.Elligator1.edwardsCurve (Elligator.Elligator1.d s)

theorem Elligator.Elligator1.curve_isValid {F : Type u_1} [Field F] [Fintype F] {q : ℕ} {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : (curve s).IsValid

The Elligator 1 coefficient hypotheses imply that its specialized curve is valid.

def Elligator.Elligator1.EOverF {F : Type u_1} [Field F] [Fintype F] {q : ℕ} {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : Set (F × F)

EOverF is the set of affine points on the Edwards curve selected by Elligator 1. See EOverF_eq_affinePoints for the generic curve view.

Equations

• Elligator.Elligator1.EOverF sq_ne_pm_two hq_card hq_mod = {p : F × F | Elligator.Elligator1.edwardsCurveEquation p.1 p.2 ⟨Elligator.Elligator1.d s, ⋯⟩}

theorem Elligator.Elligator1.EOverF_eq_affinePoints {F : Type u_1} [Field F] [Fintype F] {q : ℕ} {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : EOverF sq_ne_pm_two hq_card hq_mod = (curve s).affinePoints

The compatibility set EOverF is exactly the affine point set of the general curve model.

theorem Elligator.Elligator1.edwardsCurveEquation_zero_one {F : Type u_1} [Field F] [Fintype F] {q : ℕ} {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : let d := d s; have d_h := ⋯; edwardsCurveEquation 0 1 ⟨d, d_h⟩