Twisted Edwards curves

This file contains the curve-level definitions that are independent of any specific Elligator. A twisted Edwards curve with coefficients a and d has affine equation a * x^2 + y^2 = 1 + d * x^2 * y^2.

The definitions are made over a commutative ring. Finiteness and the hypotheses used by a particular cryptographic construction belong in that construction, rather than in the definition of a curve or its affine points.

Mathlib's elliptic-curve API is currently centred on Weierstrass models. A twisted Edwards model is not itself a Weierstrass equation, so using WeierstrassCurve.Affine.Equation here would require a birational coordinate conversion and extra invertibility hypotheses. The API below follows the same useful separation as that API: coefficients, an affine equation, a set of affine points, and a bundled point type.

structure Elligator.TwistedEdwardsCurve (R : Type u_1) : Type u_1

Coefficients of the twisted Edwards equation a * x^2 + y^2 = 1 + d * x^2 * y^2.

• a : R

  left hand side coefficient

• d : R

  right hand side coefficient

theorem Elligator.TwistedEdwardsCurve.ext_iff {R : Type u_1} {x y : TwistedEdwardsCurve R} : x = y ↔ x.a = y.a ∧ x.d = y.d

theorem Elligator.TwistedEdwardsCurve.ext {R : Type u_1} {x y : TwistedEdwardsCurve R} (a : x.a = y.a) (d : x.d = y.d) : x = y

def Elligator.TwistedEdwardsCurve.Equation {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) (x y : R) : Prop

The proposition that (x, y) is an affine point of a twisted Edwards curve.

Equations

• E.Equation x y = (E.a * x ^ 2 + y ^ 2 = 1 + E.d * x ^ 2 * y ^ 2)

def Elligator.TwistedEdwardsCurve.affinePoints {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) : Set (R × R)

The set of affine coordinate pairs on a twisted Edwards curve.

Equations

• E.affinePoints = {p : R × R | E.Equation p.fst p.snd}

@[reducible, inline]

abbrev Elligator.TwistedEdwardsCurve.Point {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) : Type u_1

A bundled affine point on a twisted Edwards curve.

Equations

• E.Point = { p : R × R // p ∈ E.affinePoints }

def Elligator.TwistedEdwardsCurve.zero {R : Type u_1} [CommRing R] : R × R

The neutral affine coordinate pair (0, 1). It lies on every twisted Edwards equation.

Equations

• Elligator.TwistedEdwardsCurve.zero = (0, 1)

@[simp]

theorem Elligator.TwistedEdwardsCurve.zero_mem_affinePoints {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) : zero ∈ E.affinePoints

def Elligator.TwistedEdwardsCurve.zeroPoint {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) : E.Point

The neutral point, bundled as an affine point of E.

Equations

• E.zeroPoint = ⟨Elligator.TwistedEdwardsCurve.zero, ⋯⟩

def Elligator.TwistedEdwardsCurve.neg {R : Type u_1} [CommRing R] (p : R × R) : R × R

Negation of affine coordinates on a twisted Edwards curve.

Equations

• Elligator.TwistedEdwardsCurve.neg p = (-p.fst, p.snd)

@[simp]

theorem Elligator.TwistedEdwardsCurve.neg_mem_affinePoints {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) (p : R × R) : neg p ∈ E.affinePoints ↔ p ∈ E.affinePoints

def Elligator.TwistedEdwardsCurve.IsValid {R : Type u_1} [CommRing R] (E : TwistedEdwardsCurve R) : Prop

The usual coefficient conditions for a nonsingular twisted Edwards model over a field. Keeping this predicate separate from TwistedEdwardsCurve permits the equation and its points to be used over more general rings and also permits partially specified curves during developments.

Equations

• E.IsValid = (E.a ≠ 0 ∧ E.d ≠ 0 ∧ E.a ≠ E.d)

def Elligator.TwistedEdwardsCurve.ofD {R : Type u_1} [CommRing R] (d : R) : TwistedEdwardsCurve R

The (untwisted) Edwards curve with parameter d, obtained by setting a = 1.

Equations

• Elligator.TwistedEdwardsCurve.ofD d = { a := 1, d := d }

@[simp]

theorem Elligator.TwistedEdwardsCurve.ofD_equation {R : Type u_1} [CommRing R] (d x y : R) : (ofD d).Equation x y ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2

@[simp]

theorem Elligator.TwistedEdwardsCurve.ofD_isValid_iff {R : Type u_1} [CommRing R] [Nontrivial R] (d : R) : (ofD d).IsValid ↔ d ≠ 0 ∧ d ≠ 1