feat(Crypto/Systems): Elligator 1, Theorem 1 and Definition 2

Cslib.lean

@@ -62,6 +62,24 @@ public import Cslib.Crypto.Protocols.SecretSharing.Defs
 public import Cslib.Crypto.Protocols.SecretSharing.Scheme
 public import Cslib.Crypto.Protocols.SecretSharing.Shamir
 public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial
+public import Cslib.Crypto.Systems.Elligator.Basic
+public import Cslib.Crypto.Systems.Elligator.Elligator1.DecodingFunction
+public import Cslib.Crypto.Systems.Elligator.Elligator1.EdwardsCurve
+public import Cslib.Crypto.Systems.Elligator.Elligator1.Map
+public import Cslib.Crypto.Systems.Elligator.Elligator1.Variables
+public import Cslib.Crypto.Systems.Elligator.Elligator1.XProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.YProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.cProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.dProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.rProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.sProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.uProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.vProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.xProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.yProperties
+public import Cslib.Crypto.Systems.Elligator.FiniteFieldBasic
+public import Cslib.Crypto.Systems.Elligator.LegendreSymbol
+public import Cslib.Crypto.Systems.Elligator.TwistedEdwardsCurve
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects

Cslib/Crypto/Systems/Elligator/Basic.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+module
+
+public import Cslib.Init
+public import Mathlib.Algebra.Field.Defs
+public import Mathlib.FieldTheory.Finite.Basic

Cslib/Crypto/Systems/Elligator/Elligator1/DecodingFunction.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+module
+
+public import Cslib.Crypto.Systems.Elligator.Elligator1.Map
+
+/-!
+# DecodingFunction
+
+This file exposes the total field-to-curve map from Definition 2 of the Elligator paper under the
+name `DecodingFunction`. The underlying construction is `ϕ`: it maps `t = ±1` to `(0, 1)` and,
+for every other `t`, returns the coordinates constructed in Theorem 1.
+
+## Main results
+
+* `DecodingFunction`: the Elligator 1 decoding map `F → F × F`, obtained from the curve-valued
+  map `ϕ` by forgetting its proof of curve membership.
+
+## References
+
+See [bernstein2013a], Section 3.2, Definition 2.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Systems.Elligator.Elligator1
+
+variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]
+variable {s : F}
+variable {q : ℕ}
+
+/-- The decoding function for the complete Edwards curve -/
+def DecodingFunction
+  (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)
+  : F × F := ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod
+
+end Cslib.Crypto.Systems.Elligator.Elligator1

Cslib/Crypto/Systems/Elligator/Elligator1/EdwardsCurve.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+module
+
+public import Cslib.Crypto.Systems.Elligator.TwistedEdwardsCurve
+public import Cslib.Crypto.Systems.Elligator.Elligator1.dProperties
+
+/-!
+# The Edwards curve used by Elligator 1
+
+This file specializes the general `Cslib.Crypto.Systems.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.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Systems.Elligator.Elligator1
+
+variable {F : Type*} [Field F] [Fintype F]
+variable {q : ℕ}
+
+/-- The general Edwards curve with coefficient `d`.
+This is an alias for the `a = 1` specialization of a twisted Edwards curve. -/
+def edwardsCurve (d : F) : TwistedEdwardsCurve F := TwistedEdwardsCurve.ofD d
+
+/-- `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`.
+-/
+def edwardsCurveEquation (x y : F) (d : {d : F // d ≠ 0 ∧ d ≠ 1}) : Prop :=
+  (edwardsCurve (F := F) d.val).Equation x y
+
+omit [Fintype F] in
+@[simp]
+theorem edwardsCurveEquation_iff (x y : F) (d : {d : F // d ≠ 0 ∧ d ≠ 1}) :
+  edwardsCurveEquation x y d ↔ x^2 + y^2 = 1 + d * x^2 * y^2 := by
+    simp [edwardsCurveEquation, edwardsCurve]
+
+/-- The Edwards curve selected by the Elligator 1 parameter `s`. -/
+def curve (s : F) : TwistedEdwardsCurve F :=
+  edwardsCurve (d s)
+
+/-- The Elligator 1 coefficient hypotheses imply that its specialized curve is valid. -/
+theorem curve_isValid
+  {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 := by
+    rw [curve, edwardsCurve, TwistedEdwardsCurve.ofD_isValid_iff]
+    exact d_ne_zero_and_d_ne_one sq_ne_pm_two hq_card hq_mod
+
+/-- `EOverF` is the set of affine points on the Edwards curve selected by Elligator 1.
+See `EOverF_eq_affinePoints` for the generic curve view. -/
+def EOverF
+  {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) :=
+  let d := d s
+  let d_h : d ≠ 0 ∧ d ≠ 1 :=
+    d_ne_zero_and_d_ne_one sq_ne_pm_two hq_card hq_mod
+  {p | edwardsCurveEquation p.fst p.snd ⟨d, d_h⟩}
+
+/-- The compatibility set `EOverF` is exactly the affine point set of the general curve model. -/
+theorem EOverF_eq_affinePoints
+  {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 := by
+  rfl
+
+lemma edwardsCurveEquation_zero_one
+  {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
+  let d_h : d ≠ 0 ∧ d ≠ 1 := d_ne_zero_and_d_ne_one sq_ne_pm_two hq_card hq_mod
+  edwardsCurveEquation (0 : F) (1 : F) ⟨d, d_h⟩ := by
+    intro d_of_s d_h
+    unfold edwardsCurveEquation
+    simp [edwardsCurve]
+
+end Cslib.Crypto.Systems.Elligator.Elligator1

Cslib/Crypto/Systems/Elligator/Elligator1/Map.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+module
+
+public import Cslib.Crypto.Systems.Elligator.Elligator1.Variables
+public import Cslib.Crypto.Systems.Elligator.Elligator1.sProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.cProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.dProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.EdwardsCurve
+public import Cslib.Crypto.Systems.Elligator.Elligator1.uProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.vProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.XProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.YProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.xProperties
+public import Cslib.Crypto.Systems.Elligator.Elligator1.yProperties
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Systems.Elligator.Elligator1
+
+variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]
+variable {s : F}
+variable {q : ℕ}
+
+omit [Fintype F] [DecidableEq F] in
+theorem u_defined :
+  ∀ t : {n : F // n ≠ 1 ∧ n ≠ -1}, (1 + t.val) ≠ 0 := by
+    intro t
+    exact FiniteFieldBasic.one_add_t_ne_zero t
+
+omit [DecidableEq F] in
+theorem Y_defined
+  (hs_ne_zero : s ≠ 0)
+  (hq_card : Fintype.card F = q)
+  (hq_mod : q % 4 = 3)
+  : (c s)^2 ≠ 0 := by
+    exact pow_ne_zero 2 (c_ne_zero hs_ne_zero hq_card hq_mod)
+
+theorem x_defined
+  (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 := by
+    intro t
+    exact Y_ne_zero hs_ne_zero hq_card hq_mod t
+
+theorem y_defined
+  (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 := by
+    intro t
+    exact y_divisor_ne_zero hs_ne_zero sq_ne_pm_two hq_card hq_mod t
+
+/-- The auxiliary coordinates `X` and `Y` satisfy the hyperelliptic equation used in Theorem 1:
+`Y² = X⁵ + (r² - 2)X³ + X`. -/
+theorem map_fulfills_auxiliary_equation
+  (t : {n : F // n ≠ 1 ∧ n ≠ -1})
+  (hs_ne_zero : s ≠ 0)
+  (hq_card : Fintype.card F = q)
+  (hq_mod : q % 4 = 3)
+  :
+  let r := r s
+  let X := X t s
+  let Y := Y t s q
+  Y^2 = X^5 + (r^2 - 2) * X^3 + X := by
+    intro r_of_s X_of_t Y_of_t
+    exact helper_eq t hs_ne_zero hq_card hq_mod
+
+/-- The quantities constructed for a nonexceptional input are all nonzero as asserted in
+Theorem 1: `u * v * X * Y * x * (y + 1) ≠ 0`. -/
+theorem variable_mul_ne_zero
+  (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)
+  :
+  let u := u t
+  let v := v t s
+  let X := X t s
+  let Y := Y t s q
+  let x := x t s q
+  let y := y t s
+  u * v * X  * Y * x * (y + 1) ≠ 0 :=
+    variable_mul_ne_zero' t hs_ne_zero sq_ne_pm_two hq_card hq_mod
+
+/-- 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. -/
+theorem map_fulfills_curve_equation
+  (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)
+  :
+  let x := x t s q
+  let y := y t s
+  let d := d s
+  have d_h : d ≠ 0 ∧ d ≠ 1 := d_ne_zero_and_d_ne_one sq_ne_pm_two hq_card hq_mod
+  edwardsCurveEquation x y ⟨d, d_h⟩ := by
+    intro x_of_t y_of_t d_of_s
+    rw [edwardsCurveEquation_iff]
+    exact curve_equation t hs_ne_zero 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. -/
+def ϕ
+  (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 :=
+  let P := if h : t ≠ 1 ∧ t ≠ -1
+    then (x ⟨t, h⟩ s q, y ⟨t, h⟩ s)
+    else (0, 1)
+  have P_in_EOverF : P ∈ (EOverF sq_ne_pm_two hq_card hq_mod) := by
+    unfold EOverF
+    rw [Set.mem_ofPred_eq]
+    unfold P
+    by_cases ht : t ≠ 1 ∧ t ≠ -1
+    · rw [dif_pos ht]
+      exact map_fulfills_curve_equation ⟨t, ht⟩ hs_ne_zero sq_ne_pm_two hq_card hq_mod
+    · rw [dif_neg ht]
+      simp
+  ⟨P, P_in_EOverF⟩
+
+end Cslib.Crypto.Systems.Elligator.Elligator1