Map

This file formalizes the construction and well-definedness results in Theorem 1 of the Elligator paper. For a field input t ≠ ±1, the auxiliary quantities u, v, X, and Y determine a point (x, y) on the complete Edwards curve. The exceptional inputs t = ±1 are incorporated by ϕ, which sends both to (0, 1).

Main results

• u_defined, Y_defined, x_defined, y_defined: the denominators in the paper's formulas are nonzero, so the displayed expressions are defined.
• map_fulfills_helper_equation: the auxiliary coordinates satisfy Y² = X⁵ + (r² - 2)X³ + X.
• variable_mul_ne_zero: the nonvanishing assertion u * v * X * Y * x * (y + 1) ≠ 0 from Theorem 1.
• map_fulfills_curve_equation: the resulting (x, y) satisfies the Edwards curve equation.
• ϕ: Definition 2's total map from field elements to points on the Edwards curve.

References

See [bernstein2013a], Section 3.2, Theorem 1 and Definition 2.

theorem Elligator.Elligator1.u_defined {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 + ↑t ≠ 0

theorem Elligator.Elligator1.Y_defined {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : c s ^ 2 ≠ 0

theorem Elligator.Elligator1.x_defined {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : Y t s q ≠ 0

theorem Elligator.Elligator1.y_defined {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : r s * X t s + (1 + X t s) ^ 2 ≠ 0

theorem Elligator.Elligator1.map_fulfills_auxiliary_equation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have r := r s; have X := X t s; have Y := Y t s q; Y ^ 2 = X ^ 5 + (r ^ 2 - 2) * X ^ 3 + X

The auxiliary coordinates X and Y satisfy the hyperelliptic equation used in Theorem 1: Y² = X⁵ + (r² - 2)X³ + X.

theorem Elligator.Elligator1.variable_mul_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have u := u t; have v := v t s; have X := X t s; have Y := Y t s q; have x := x t s q; have y := y t s; u * v * X * Y * x * (y + 1) ≠ 0

The quantities constructed for a nonexceptional input are all nonzero as asserted in Theorem 1: u * v * X * Y * x * (y + 1) ≠ 0.

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

The coordinates produced from a nonexceptional input satisfy the Edwards curve equation x² + y² = 1 + d * x² * y². This is the final conclusion of Theorem 1.

def Elligator.Elligator1.ϕ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : F) (hs_ne_zero : s ≠ 0) (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)

The total Elligator map ϕ : F → E(F) from Definition 2 of the paper.

For t ≠ ±1, it returns the coordinates x(t) and y(t) constructed in Theorem 1. The two exceptional inputs t = ±1 are both mapped to the neutral point (0, 1). The codomain subtype records that the result satisfies the Edwards curve equation.

Equations

• Elligator.Elligator1.ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod = ⟨if h : t ≠ 1 ∧ t ≠ -1 then (Elligator.Elligator1.x ⟨t, h⟩ s q, Elligator.Elligator1.y ⟨t, h⟩ s) else (0, 1), ⋯⟩