diff --git a/Cslib.lean b/Cslib.lean index d74457919..1636fafc2 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Crypto/Systems/Elligator/Basic.lean b/Cslib/Crypto/Systems/Elligator/Basic.lean new file mode 100644 index 000000000..7c1526e01 --- /dev/null +++ b/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 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/DecodingFunction.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/DecodingFunction.lean new file mode 100644 index 000000000..b8c0f207a --- /dev/null +++ b/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 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/EdwardsCurve.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/EdwardsCurve.lean new file mode 100644 index 000000000..af62b21c1 --- /dev/null +++ b/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 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/Map.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/Map.lean new file mode 100644 index 000000000..ab5d6339e --- /dev/null +++ b/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 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/Variables.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/Variables.lean new file mode 100644 index 000000000..b55f4abea --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/Variables.lean @@ -0,0 +1,181 @@ +/- +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.LegendreSymbol + +/-! +# Elligator 1 Variables + +In this file we introduce all the independent variables introduced in the definition of Elligator 1. + +## References + +See [bernstein2013a], Section 3. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.LegendreSymbol + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] + +/-- c(s) is a function defined in the paper. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def c (s : F) : F := 2 / s^2 + +/-- r(s) is a function defined in the paper. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def r (s : F) : F := + let c := c s; + c + 1 / c + +/-- d(s) is a function defined in the paper. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def d (s : F) : F := + let c := c s; + -(c + 1)^2 / (c - 1)^2 + +/-- u(t) is a function defined in the paper. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def u (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : F := + let t := t.val; + (1 - t) / (1 + t) + +/-- v(t, s) is a function defined in the paper. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def v (t : {n : F // n ≠ 1 ∧ n ≠ -1}) (s : F) : F := + let u := u t + let r := r s + u^5 + (r^2 - 2) * u^3 + u + +/-- X(t, s) is a function defined in the paper. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def X (t : {n : F // n ≠ 1 ∧ n ≠ -1}) (s : F) : F := + let u := u t + let v := v t s + (χ v) * u + +/-- Y(t, s) is a function defined in the paper. + +`q` is still unrelated to the cardinality F here by intention. The theorems using +`Y` will build the necessary context to show useful properties of `Y` by creating +the relation of Field cardinality and `q`. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def Y (t : {n : F // n ≠ 1 ∧ n ≠ -1}) (s : F) (q : ℕ) : F := + let u := u t + let c := c s + let v := v t s + ((χ v) * v)^((q + 1) / 4) * (χ v) * χ (u^2 + 1 / c^2) + +/-- x(t, s) is a function defined in the paper. It is the x-coordinate of the point on the curve. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def x (t : {n : F // n ≠ 1 ∧ n ≠ -1}) (s : F) (q : ℕ) : F := + let c := c s + let X := X t s + let Y := Y t s q + (c - 1) * s * X * (1 + X) / Y + +/-- y(t, s) is a function defined in the paper. It is the y-coordinate of the point on the curve. + +Original:, Section "3.2 The map": Theorem 1 +-/ +def y (t : {n : F // n ≠ 1 ∧ n ≠ -1}) (s : F) : F := + let r := r s + let X := X t s + (r * X - (1 + X)^2) / (r * X + (1 + X)^2) + +/-- η(s, q, point) is a function defined in the paper. + +Original:, Section "3.3 Inverting the map": Theorem 3 +-/ +def η (P : F × F) : F := + let y := P.snd + (y - 1) / (2 * (y + 1)) + +/-- X2 is a function defined in the paper. + +Original:, Section "3.3 Inverting the map": Theorem 3 +-/ +def X2 (s : F) (P : F × F) (q : ℕ) : F := + let η := η P + let r := r s + (-(1 + η * r) + ((1 + η * r)^2 - 1)^((q + 1) / 4)) + +/-- z is a function defined in the paper. + +Original:, Section "3.3 Inverting the map": Theorem 3 +-/ +def z (s : F) (P : F × F) (q : ℕ) : F := + let x := P.fst + let c := c s + let X2 := X2 s P q + let a := (c - 1) * s * X2 * (1 + X2) * x * (X2^2 + 1 / c^2) + χ a + +/-- u2 is a function defined in the paper. + +Original:, Section "3.3 Inverting the map": Theorem 3 +-/ +def u2 (s : F) (P : F × F) (q : ℕ) : F := + let X2 := X2 s P q + let z := z s P q + z * X2 + +/-- t2 is a function defined in the paper. + +Original:, Section "3.3 Inverting the map": Theorem 3 +-/ +def t2 (s : F) (P : F × F) (q : ℕ) : F := + let u2 := u2 s P q + (1 - u2) / (1 + u2) + +/-- `b q` is `⌊log₂ q⌋`, the number of bits needed. + +Original:, Section "3.4 Encoding as strings": Theorem 4 +-/ +def b (q : ℕ) : ℕ := Nat.log 2 q + +/-- Convert a bit vector (τ₀, τ₁, ..., τ_{b-1}) to a natural number via binary +expansion: bitsToNat(τ) = Σᵢ τᵢ · 2^i. +-/ +def bitsToNat {n : ℕ} (τ : Fin n → Bool) : ℕ := + ∑ i : Fin n, if τ i then 2^(i : ℕ) else 0 + +/-- `σ` interprets a bit vector `(τ₀, τ₁, …, τ_{b−1})` as the field element +`∑ᵢ τᵢ · 2ⁱ ∈ Fq`. This is the standard binary-to-integer conversion followed by casting into `F`. + +Original:, Section "3.4 Encoding as strings": Theorem 4 +-/ +def σ {q : ℕ} (τ : Fin (@b q) → Bool) : F := (bitsToNat τ : F) + +/-- S = σ⁻¹({0, 1, 2, ..., (q-1)/2}), the set of bit vectors whose binary value +falls in the lower half {0, 1, ..., (q-1)/2} of F_q. + +Original:, Section "3.4 Encoding as strings": Theorem 4 +-/ +def S {q : ℕ} : Finset (Fin (@b q) → Bool) := + Finset.univ.filter (fun τ => (bitsToNat τ) ≤ (q - 1) / 2) + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/XProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/XProperties.lean new file mode 100644 index 000000000..fc1f712bf --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/XProperties.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.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.uProperties +public import Cslib.Crypto.Systems.Elligator.Elligator1.vProperties + +/-! +# X Variable Properties + +In this file we introduce some generally helpful lemmas for `X` as introduced in +`Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic +open Elligator.LegendreSymbol + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {s : F} +variable {q : ℕ} + +lemma X_pow_two_add_one_div_c_pow_two_ne_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : (X t s)^2 + 1 / (c s)^2 ≠ 0 := by + let X := X t s + let c := c s + intro h_sum_eq_zero + have h_cleared : X^2 * c^2 + c⁻¹^2 * c^2 = 0 := by grind + have h_prod_eq_neg_one : X^2 * c^2 = -1 := by grind [c_ne_zero] + have h_not_isSquare : ¬IsSquare (-1 : F) := neg_one_non_square hq_card hq_mod + have h_isSquare : IsSquare (-1 : F) := by + rw [← h_prod_eq_neg_one, ← mul_pow] + apply IsSquare.sq (X * c) + contradiction + +lemma X_ne_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : (X t s) ≠ 0 := by + apply mul_ne_zero + · apply χ_a_ne_zero (v_ne_zero hs_ne_zero hq_card hq_mod t) + · apply u_ne_zero t + +lemma X_comparison (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : + let t1 := t.val + let t2 := -t1 + let X1 := X t s + let X2 := X ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s + X2 = 1 / X1 := by + intro t1 t2 X1 X2 + let u1 := u t + let u2 := u ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ + let v1 := v t s + let v2 := v ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s + calc + X2 = (χ v2) * u2 := by rfl + _ = (χ v1) / u1 := by + unfold v2 t2 + rw [v_comparison_implication4 t] + unfold u2 + rw [u_comparison t] + change (χ v1) * (1 / u1) = (χ v1) / u1 + ring_nf + _ = 1 / ((χ v1) * u1) := by + nth_rw 1 [one_div_χ_of_a_eq_χ_a] + ring_nf + _ = 1 / X1 := by rfl + +@[simp] +lemma X_of_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : + let X0 := X ⟨(0 : F), by simp⟩ s + X0 = 1 := by + intro X0 + unfold X0 X + let χ_of_v := χ (v ⟨(0 : F), by simp⟩ s) + rw [u_of_zero] + change χ_of_v * 1 = 1 + unfold χ_of_v + rw [v_of_zero] + rw [χ_sq (r_ne_zero hs_ne_zero hq_card hq_mod)] + simp + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/YProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/YProperties.lean new file mode 100644 index 000000000..f271ed17e --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/YProperties.lean @@ -0,0 +1,225 @@ +/- +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.uProperties +public import Cslib.Crypto.Systems.Elligator.Elligator1.vProperties +public import Cslib.Crypto.Systems.Elligator.Elligator1.XProperties + +/-! +# Y Variable Properties + +In this file we introduce some generally helpful lemmas for `Y` as introduced in +`Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic +open Elligator.LegendreSymbol + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {s : F} +variable {q : ℕ} + +omit [DecidableEq F] in +lemma Y_ne_zero + [DecidableEq F] + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let Y := Y t s q + Y ≠ 0 := by + let u := u t + let v := v t s + let χ_of_sum := χ (u^2 + 1 / (c s)^2) + intro Y + change ((χ v) * v)^((q + 1) / 4) * (χ v) * χ_of_sum ≠ 0 + have hv_ne_zero := v_ne_zero hs_ne_zero hq_card hq_mod t + apply mul_ne_zero + · apply mul_ne_zero + · rw [mul_pow (χ v) v ((q + 1) / 4)] + apply mul_ne_zero + · apply pow_ne_zero (((q + 1) / 4) : ℕ) + apply χ_a_ne_zero hv_ne_zero + · apply pow_ne_zero (((q + 1) / 4) : ℕ) + apply hv_ne_zero + · apply χ_a_ne_zero hv_ne_zero + · apply χ_a_ne_zero (v_factored_third_factor_ne_zero hs_ne_zero hq_card hq_mod t) + +omit [DecidableEq F] in +lemma X_mul_Y_ne_zero + [DecidableEq F] + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let X := X t s + let Y := Y t s q + X * Y ≠ 0 := by + apply mul_ne_zero + · apply X_ne_zero hs_ne_zero hq_card hq_mod t + · apply Y_ne_zero hs_ne_zero hq_card hq_mod t + +omit [DecidableEq F] in +lemma one_add_X_ne_zero + [DecidableEq F] + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let X := X t s + (1 + X) ≠ (0 : F) := by + let u := u t + let v := v t s + let r := r s + have hv_ne_zero := v_ne_zero hs_ne_zero hq_card hq_mod t + intro X + change 1 + (χ v) * u ≠ 0 + intro h_contra + have h_chi_v_mul_u_eq_neg_one : (χ v) * u = -1 := by grind + have h_u_eq_neg_chi_v : u = -(χ v) := by grind [one_div_χ_of_a_eq_χ_a] + have h_v_eq_expand : v = -(χ v) * (1 + r^2 - 2 + 1) := by + change u^5 + (r^2 - 2) * u^3 + u = -(χ v) * (1 + r^2 - 2 + 1) + repeat rw [h_u_eq_neg_chi_v] + rw [← neg_one_mul, mul_pow, mul_pow] + grind [χ_of_a_pow_n_eq_χ_a] + have h_v_eq_neg_chi_v_mul_r_sq : v = -(χ v) * r^2 := by grind + have h_chi_v_eq_neg_chi_v : (χ v) = -(χ v) := by + rw [h_u_eq_neg_chi_v] at h_chi_v_mul_u_eq_neg_one + change (χ v) * -(χ v) = -1 at h_chi_v_mul_u_eq_neg_one + nth_rw 1 [h_v_eq_neg_chi_v_mul_r_sq] at h_chi_v_mul_u_eq_neg_one + rw [χ_mul] at h_chi_v_mul_u_eq_neg_one + nth_rw 1 [← neg_one_mul] at h_chi_v_mul_u_eq_neg_one + rw [χ_mul, χ_neg_one hq_card hq_mod] at h_chi_v_mul_u_eq_neg_one + rw [χ_χ_eq_χ hq_card hq_mod] at h_chi_v_mul_u_eq_neg_one + have hr_sq_ne_zero : r^2 ≠ 0 := pow_ne_zero 2 (r_ne_zero hs_ne_zero hq_card hq_mod) + have hr_sq_isSquare : IsSquare (r^2) := IsSquare.sq r + grind [χ_a_eq_one] + have h_chi_v_ne_neg_chi_v : (χ v) ≠ -(χ v) := neg_χ_a_ne_χ_a hv_ne_zero hq_card hq_mod + contradiction + +omit [DecidableEq F] in +lemma Y_comparison + [DecidableEq F] + (t : { t : F // t ≠ 1 ∧ t ≠ -1}) + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : + let t1 := t.val + let t2 := -t1 + let X1 := X t s + let Y1 := Y t s q + let Y2 := Y ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s q + Y2 = Y1 / X1^3 := by + intro t1 t2 X1 Y1 Y2 + let t_h := neg_t_ne_one_and_neg_t_ne_neg_one t + let c := c s + let r := r s + let u1 := u t + let u2 := u ⟨t2, t_h⟩ + let v1 := v t s + let v2 := v ⟨t2, t_h⟩ s + have hu1_ne_zero := u_ne_zero (t := t) + have first_factor : + ((χ v2) * v2)^((q + 1) / 4) = ((χ v1) * v1)^((q + 1) / 4) * (χ u1) / u1^3 := by + have h_v2_mul_v2_eq_v1_mul_v1_div_u1_pow6 : (χ v2) * v2 = (χ v1) * v1 / u1^6 := by + rw [v_comparison_implication4 t] + unfold v2 + rw [v_comparison_implication2 t] + change (χ v1) * (v1 / u1^6) = (χ v1) * v1 / u1 ^ 6 + rw [← mul_div_assoc] + have h_chi_u1_mul_u1_cubed_isSquare : IsSquare ((χ u1) * u1^3) := by + have h_chi_u1_mul_u1_cubed_ne_zero : (χ u1) * u1^3 ≠ 0 := by + apply mul_ne_zero + · apply χ_a_ne_zero hu1_ne_zero + · apply pow_ne_zero 3 hu1_ne_zero + apply (χ_eq_one_iff_isSquare h_chi_u1_mul_u1_cubed_ne_zero hq_card hq_mod).mp + have h_three_eq_one_add_two : (3 : ℕ) = 1 + 2 := by norm_num + rw [h_three_eq_one_add_two, pow_add u1 1 2, ← mul_assoc, pow_one] + rw [χ_mul, χ_mul] + rw [χ_χ_eq_χ hq_card hq_mod] + rw [← χ_mul, ← pow_two] + have h_u1_sq_isSquare : IsSquare (u1^2) := IsSquare.sq u1 + have h_chi_u1_sq_eq_one : χ (u1 ^ 2) = 1 := by + apply (χ_eq_one_iff_isSquare (pow_ne_zero 2 hu1_ne_zero) hq_card hq_mod).mpr + exact h_u1_sq_isSquare + simp [h_chi_u1_sq_eq_one] + have h_u1_pow6_pow_eq_chi_u1_mul_u1_cubed : (u1^6)^((q + 1) / 4) = (χ u1) * u1^3 := by + have h_six_eq_three_mul_two : 6 = 3 * 2 := by norm_num + rw [h_six_eq_three_mul_two, ← pow_mul, mul_assoc, mul_comm, pow_mul, mul_comm] + rw [add_comm, one_add_q_div_four_mul_two_eq_one_add_q_div_two hq_mod] + rw [add_comm, a_pow_q_add_one_div_two_eq_χ_of_a_mul_a hq_card hq_mod] + change ((χ u1) * u1)^3 = (χ u1) * u1^3 + rw [mul_pow, χ_of_a_pow_n_eq_χ_a u1 ⟨3, by trivial⟩] + calc + ((χ v2) * v2)^((q + 1) / 4) = ((χ v1) * v1 / u1^6)^((q + 1) / 4) := by + rw [h_v2_mul_v2_eq_v1_mul_v1_div_u1_pow6] + _ = ((χ v1) * v1)^((q + 1) / 4) * (χ u1) / u1^3 := by + rw [div_pow, h_u1_pow6_pow_eq_chi_u1_mul_u1_cubed] + nth_rw 2 [one_div_χ_of_a_eq_χ_a] + grind + have second_factor : (χ v2) = (χ v1) := v_comparison_implication4 t + have third_factor : χ (u2^2 + 1 / c^2) = χ (u1 * v1 * (u1^2 + 1 / c^2)) := by + calc + χ (u2^2 + 1 / c^2) + = χ ((c^2 * u1^4 * (u2^2 + 1 / c^2)) * (u1^2 + 1 / c^2)^2) := by + rw [← χ_of_a_eq_χ_a_mul_b_pow_two (c_ne_zero hs_ne_zero hq_card hq_mod)] + rw [mul_comm, ← χ_of_a_eq_χ_a_mul_b_pow_two (pow_ne_zero 2 hu1_ne_zero)] + rw [χ_of_a_eq_χ_a_mul_b_pow_two + (v_factored_third_factor_ne_zero hs_ne_zero hq_card hq_mod t)] + grind + _ = χ ((u1^2 * (c^2 + u1^2)) * (u1^2 + 1 / c^2)^2) := by + rw [pow_two u2] + unfold u2 + rw [u_comparison t] + change χ (c^2 * u1^4 * (1 / u1 * (1 / u1) + 1 / c^2) * (u1^2 + 1 / c^2)^2) + = χ (u1^2 * (c^2 + u1^2) * (u1^2 + 1 / c^2)^2) + have h_clear_denominators : + c^2 * u1^4 * (1 / u1 * (1 / u1) + 1 / c^2) = u1^2 * (c^2 + u1^2) := by + have hc_sq_ne_zero : c^2 ≠ 0 := pow_ne_zero 2 (c_ne_zero hs_ne_zero hq_card hq_mod) + grind + rw [h_clear_denominators] + _ = χ (u1 * v1 * (u1^2 + 1 / c^2)) := by grind [v_factored] + calc + Y2 = Y1 * (χ u1) * χ (u1 * v1) / u1^3 := by + unfold Y2 Y + change ((χ v2) * v2)^((q + 1) / 4) * (χ v2) * χ (u2^2 + 1 / c^2) + = Y1 * (χ u1) * χ (u1 * v1) / u1^3 + rw [first_factor, second_factor, third_factor, χ_mul] + have h_rearrange : + ((χ v1) * v1)^((q + 1) / 4) * (χ u1) / u1^3 * (χ v1) + * (χ (u1 * v1) * (χ (u1^2 + 1 / c^2))) + = ((χ v1) * v1) ^ ((q + 1) / 4) * (χ v1) * (χ (u1^2 + 1 / c^2)) + * (χ u1) * χ (u1 * v1) / u1^3 := by ring_nf + rw [h_rearrange] + rfl + _ = Y1 / ((χ v1) * u1)^3 := by + calc + Y1 * (χ u1) * χ (u1 * v1) / u1^3 = Y1 * (χ v1) / u1^3 := by + rw [χ_mul, ← mul_assoc, mul_assoc Y1, ← χ_mul, ← pow_two, χ_sq hu1_ne_zero, mul_one] + _ = Y1 / ((χ v1) * u1)^(2 + 1) := by + nth_rw 1 [one_div_χ_of_a_eq_χ_a] + rw [mul_div_assoc, div_div] + nth_rw 1 [← χ_of_a_pow_n_eq_χ_a v1 ⟨3, by trivial⟩, ← mul_pow] + ring_nf + _ = Y1 / X1^3 := by rfl + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/cProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/cProperties.lean new file mode 100644 index 000000000..e0c53e408 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/cProperties.lean @@ -0,0 +1,83 @@ +/- +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 + +/-! +# c Variable Properties + +In this file we introduce some generally helpful lemmas for `c` as introduced +in `Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic + +variable {F : Type*} [Field F] [Fintype F] +variable {s : F} +variable {q : ℕ} + +lemma c_ne_zero (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : c s ≠ 0 := by + unfold c + exact div_ne_zero (two_ne_zero hq_card hq_mod) (pow_ne_zero 2 hs_ne_zero) + +omit [Fintype F] in +lemma c_ne_one (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : c s ≠ 1 := by + unfold c + exact div_ne_one_of_ne (s_pow_two_ne_two sq_ne_pm_two).symm + +omit [Fintype F] in +lemma c_sub_one_ne_zero (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : c s - 1 ≠ 0 := + sub_ne_zero.2 (c_ne_one sq_ne_pm_two) + +omit [Fintype F] in +lemma c_ne_neg_one (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : (c s) ≠ -1 := by + unfold c + intro h + have heq : s^2 = -2 := by grind + have hne := s_pow_two_ne_neg_two sq_ne_pm_two + contradiction + +omit [Fintype F] in +lemma c_add_one_ne_zero (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : (c s) + 1 ≠ 0 := by + intro hceq + have hc_ne_neg_one := c_ne_neg_one sq_ne_pm_two + rw [← add_left_inj (-1)] at hceq + ring_nf at hceq + contradiction + +lemma c_mul_sub_one_mul_add_one_ne_zero + (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 c := c s + c * (c - 1) * (c + 1) ≠ 0 := by + unfold c + apply mul_ne_zero + · apply mul_ne_zero + · exact c_ne_zero hs_ne_zero hq_card hq_mod + · exact c_sub_one_ne_zero sq_ne_pm_two + · exact c_add_one_ne_zero sq_ne_pm_two + +lemma s_pow_two_eq_two_div_c + (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : s^2 = 2 / (c s) := by + unfold c + have h := two_ne_zero hq_card hq_mod + field_simp + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/dProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/dProperties.lean new file mode 100644 index 000000000..1b7a8d9b7 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/dProperties.lean @@ -0,0 +1,136 @@ +/- +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.cProperties + +/-! +# d Variable Properties + +In this file we introduce some generally helpful lemmas for `d` as introduced +in `Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic + +variable {F : Type*} [Field F] [Fintype F] +variable {s : F} +variable {q : ℕ} + +lemma d_nonsquare + (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : ¬IsSquare (d s) := by + rw [isSquare_iff_exists_mul_self (d s)] + change ¬∃ r, (-((2 / s^2) + 1)^2 / ((2 / s^2) - 1)^2) = r * r + rintro ⟨w, Pw⟩ + have hdivd : (2 / s^2 - 1)^2 ≠ 0 := by grind + have hdivs : (2 / s^2 + 1)^2 ≠ 0 := by grind + have heq : w^2 * ((2 / s^2) - 1)^2 / ((2 / s^2) + 1)^2 = -1 := by grind + have hsq : IsSquare (-1 : F) := by + rw [← heq] + have hw_sq : IsSquare (w^2) := by + rw [pow_two] + apply IsSquare.mul_self w + have hdiv_sq : IsSquare (((2 / s^2) - 1)^2 / ((2 / s^2) + 1)^2) := by + apply IsSquare.div + · rw [pow_two] + apply IsSquare.mul_self (2 / s^2 - 1) + · rw [pow_two] + apply IsSquare.mul_self (2 / s^2 + 1) + rw [mul_div_assoc] + apply IsSquare.mul hw_sq hdiv_sq + exact false_of_isSquare_neg_one hq_card hq_mod hsq + +lemma d_ne_zero + (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : (d s) ≠ 0 := by + have hd_nsq := d_nonsquare sq_ne_pm_two hq_card hq_mod + intro hd_eq_zero + have hd_sq : IsSquare (d s) := by + unfold IsSquare + use 0 + rwa [mul_zero] + contradiction + +lemma one_div_d_nonsquare + (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : ¬IsSquare (1 / (d s)) := by + rintro ⟨a, ha⟩ + have hd_ne_zero : d s ≠ 0 := d_ne_zero sq_ne_pm_two hq_card hq_mod + -- `1/d = a*a ≠ 0` (since `d ≠ 0`), so `a ≠ 0`. + have ha_ne_zero : a ≠ 0 := by + rintro rfl + simp only [one_div, mul_zero, inv_eq_zero] at ha + exact hd_ne_zero (by rw [ha]) + -- Reciprocal of both sides: `d = 1/(a*a) = (1/a)*(1/a)`. + apply d_nonsquare sq_ne_pm_two hq_card hq_mod + unfold IsSquare + use 1 / a + field_simp + rw [pow_two, ← ha, mul_div_left_comm, div_self hd_ne_zero, mul_one] + +lemma d_ne_one + (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : (d s) ≠ 1 := by + have hd_non_sq := d_nonsquare sq_ne_pm_two hq_card hq_mod + intro hd_eq_one + have hd_sq : IsSquare (d s) := by + rw [hd_eq_one] + apply IsSquare.one + contradiction + +lemma d_ne_zero_and_d_ne_one + (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : (d s) ≠ 0 ∧ (d s) ≠ 1 := + ⟨d_ne_zero sq_ne_pm_two hq_card hq_mod, d_ne_one sq_ne_pm_two hq_card hq_mod⟩ + +lemma neg_d_eq_r_add_two_div_r_sub_two + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : + let r := r s; + let d := d s; + -d = (r + 2) / (r - 2) := by + intro r d + let c := c s + calc + -d = (c + 2 + 1 / c) / (c - 2 + 1 / c) := by + change -(-(c + 1)^2 / (c - 1)^2) = (c + 2 + 1 / c) / (c - 2 + 1 / c) + rw [← neg_one_mul] + nth_rw 2 [← neg_one_mul] + rw [mul_div_assoc, ← mul_assoc, add_pow_two, sub_pow_two] + have hne : 1 / c ≠ 0 := by + rw [← inv_eq_one_div] + apply inv_ne_zero + apply c_ne_zero hs_ne_zero hq_card hq_mod + simp_all + grind + _ = (r + 2) / (r - 2) := by + rw [add_assoc, add_comm 2 (1 / c), ← add_assoc] + nth_rw 3 [add_comm] + rw [← add_sub_assoc] + nth_rw 3 [add_comm] + rfl + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/rProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/rProperties.lean new file mode 100644 index 000000000..9fc50cfcc --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/rProperties.lean @@ -0,0 +1,112 @@ +/- +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.cProperties + +/-! +# r Variable Properties + +In this file we introduce some generally helpful lemmas for `r` as introduced +in `Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic + +variable {F : Type*} [Field F] [Fintype F] +variable {s : F} +variable {q : ℕ} + +lemma r_ne_zero (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : (r s) ≠ 0 := by + intro h + let c := c s + change c + 1 / c = 0 at h + have hcneg : c = (-1 : F) / c := by grind + have hcpow : c^2 = -1 := by + calc + c^2 = -1 / c * c := by grind + _ = -1 := by + nth_rw 1 [← neg_one_mul 1] + ring_nf + rw [mul_inv_cancel₀ (c_ne_zero hs_ne_zero hq_card hq_mod)] + have hsq : IsSquare (-1 : F) := by + rw [← hcpow, pow_two] + apply IsSquare.mul_self c + exact false_of_isSquare_neg_one hq_card hq_mod hsq + +lemma four_add_r_ne_zero + (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) + : 4 + (r s) ≠ 0 := by + intro h_contra + have hc_ne_zero : c s ≠ 0 := c_ne_zero hs_ne_zero hq_card hq_mod + -- Step 1: clear `1/c` from `r`'s definition. + have h_quad : (c s) ^ 2 + 4 * (c s) + 1 = 0 := by + unfold r at h_contra + field_simp at h_contra + linear_combination h_contra + -- Step 2: substitute `c = 2/s²`, clear denominators — `(s²+4)² = 12`. + set a : F := s ^ 2 + 4 with ha_def + have ha_sq : a ^ 2 = 12 := by + unfold c at h_quad + field_simp at h_quad + linear_combination h_quad -- verify exact coefficient + -- Step 3: halving, `u² = 3`. + set u : F := a / 2 with hu_def + have hu_sq : u ^ 2 = 3 := by + rw [hu_def, div_pow, ha_sq] + grind + -- Step 4: `2u = a`, so `u² - 2u + 1 = 3 - a + 1 = -s²`, giving `((u-1)/s)² = -1`. + have hu_eq_a : 2 * u = a := by + rw [hu_def, mul_div_left_comm, div_self (FiniteFieldBasic.two_ne_zero hq_card hq_mod)] + rw [mul_one] + have h_neg_one_sq : (-1 : F) = ((u - 1) / s) ^ 2 := by + rw [div_pow, eq_div_iff (pow_ne_zero 2 hs_ne_zero)] + simp_all + grind + exact neg_one_non_square hq_card hq_mod ⟨_, h_neg_one_sq.trans (sq _)⟩ + +lemma r_sq_sub_two_eq_c_sq_add_inv_c_sq + (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : + let r := r s + let c := c s + (r^2 - 2) = c^2 + 1 / c^2 := by + intro r c + calc + r^2 - 2 = (c + 1 / c)^2 - 2 := by trivial + _ = c^2 + 2 * (c * (1 / c)) + (1 / c)^2 - 2 := by grind + _ = c^2 + 2 + 1 / c^2 - 2 := by + ring_nf + rw [mul_inv_cancel₀ (c_ne_zero hs_ne_zero hq_card hq_mod)] + ring_nf + _ = c^2 + 1 / c^2 := by ring_nf + +lemma r_sub_two_ne_zero + (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) + : (r s) - 2 ≠ 0 := by + let c := c s + have hc_ne_zero := c_ne_zero hs_ne_zero hq_card hq_mod + change (c + 1 / c) - 2 ≠ 0 + have hceq : (c + 1 / c) - 2 = (c - 1)^2 / c := by grind + rw [hceq] + apply div_ne_zero (by grind [c_ne_one ]) hc_ne_zero + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/sProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/sProperties.lean new file mode 100644 index 000000000..16f3d61e3 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/sProperties.lean @@ -0,0 +1,35 @@ +/- +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.Basic + +/-! +# s Variable Properties + +In this file we introduce some generally helpful lemmas for `s` as introduced +in `Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +variable {F : Type*} [Field F] +variable {s : F} + +lemma s_pow_two_ne_two (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : s ^ 2 ≠ 2 := + sub_ne_zero.mp (left_ne_zero_of_mul sq_ne_pm_two) + +lemma s_pow_two_ne_neg_two (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : s ^ 2 ≠ -2 := by + have h := right_ne_zero_of_mul sq_ne_pm_two + rwa [ne_eq, add_eq_zero_iff_eq_neg] at h + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/uProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/uProperties.lean new file mode 100644 index 000000000..93ab384ad --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/uProperties.lean @@ -0,0 +1,66 @@ +/- +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 + +/-! +# u Variable Properties + +In this file we introduce some generally helpful lemmas for `u` as introduced in +`Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic + +variable {F : Type*} [Field F] [Fintype F] +variable {s : F} +variable {q : ℕ} + +omit [Fintype F] in +lemma u_ne_zero (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : u t ≠ (0 : F) := + div_ne_zero (one_sub_t_ne_zero t) (one_add_t_ne_zero t) + +omit [Fintype F] in +lemma u_comparison (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : + let t1 := t.val + let t2 := -t1 + let u1 := u t + let u2 := u ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ + u2 = 1 / u1 := by + intro t1 t2 u1 u2 + calc + u2 = (1 - t2) / (1 + t2) := by simp [u2, u] + _ = (1 + t) / (1 - t) := by simp [t2, t1]; ring_nf + _ = 1 / u1 := by simp [u1, u] + +omit [Fintype F] in +@[simp] +lemma u_of_zero : + let u := u ⟨(0 : F), by simp⟩ + u = 1 := by simp [u] + +lemma one_add_u_ne_zero + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : 1 + (u t) ≠ 0 := by + unfold u + rw [add_div' _ _ _ (one_add_t_ne_zero t)] + norm_num + constructor + · exact two_ne_zero hq_card hq_mod + · exact one_add_t_ne_zero t + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/vProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/vProperties.lean new file mode 100644 index 000000000..b2c154d46 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/vProperties.lean @@ -0,0 +1,198 @@ +/- +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.cProperties +public import Cslib.Crypto.Systems.Elligator.Elligator1.rProperties +public import Cslib.Crypto.Systems.Elligator.Elligator1.uProperties + +/-! +# v Variable Properties + +In this file we introduce some generally helpful lemmas for `v` as introduced in +`Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic +open Elligator.LegendreSymbol + +variable {F : Type*} [Field F] [Fintype F] +variable {s : F} +variable {q : ℕ} + +lemma v_factored + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let v := v t s + let c := c s + let u := u t + v = u * (u^2 + c^2) * (u^2 + 1 / c^2) := by + intro v c u + let r := r s + change u^5 + (r^2 - 2) * u^3 + u = u * (u^2 + c^2) * (u^2 + 1 / c^2) + have hc_sq_ne_zero : c^2 ≠ 0 := pow_ne_zero 2 (c_ne_zero hs_ne_zero hq_card hq_mod) + grind [r_sq_sub_two_eq_c_sq_add_inv_c_sq] + +lemma v_factored_second_factor_ne_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : (u t)^2 + (c s)^2 ≠ 0 := by + intro h_sum_eq_zero + let c := c s + let u := u t + have h_neg_one_sq : -1 = (u / c)^2 := by + have hc_sq_ne_zero := pow_ne_zero 2 (c_ne_zero hs_ne_zero hq_card hq_mod) + grind + have h_isSquare : IsSquare (-1 : F) := by + rw [h_neg_one_sq, pow_two] + apply IsSquare.mul_self (u / c) + rw [FiniteField.isSquare_neg_one_iff, hq_card] at h_isSquare + contradiction + +lemma v_factored_third_factor_ne_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : (u t)^2 + 1 / (c s)^2 ≠ 0 := by + intro h_sum_eq_zero + have h_neg_one_sq : -1 = ((u t) * (c s))^2 := by + grind [pow_ne_zero, c_ne_zero, div_left_inj'] + have h_isSquare : IsSquare (-1 : F) := by + rw [h_neg_one_sq, pow_two] + apply IsSquare.mul_self + rw [FiniteField.isSquare_neg_one_iff, hq_card] at h_isSquare + contradiction + +lemma v_ne_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : v t s ≠ (0 : F) := by + rw [v_factored hs_ne_zero hq_card hq_mod t] + apply mul_ne_zero + · apply mul_ne_zero + · apply u_ne_zero t + · exact (v_factored_second_factor_ne_zero hs_ne_zero hq_card hq_mod t) + · exact (v_factored_third_factor_ne_zero hs_ne_zero hq_card hq_mod t) + +lemma χ_of_v_mul_v_of_t_pow_q_add_one_div_four_ne_zero + [DecidableEq F] + (t : { t : F // t ≠ 1 ∧ t ≠ -1}) + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : + let v := v t s + ((χ v) * v)^((q + 1) / 4) ≠ 0 := by + intro v + rw [mul_pow (χ v) v ((q + 1) / 4)] + apply mul_ne_zero + · apply pow_ne_zero ((q + 1) / 4) (χ_a_ne_zero (v_ne_zero hs_ne_zero hq_card hq_mod t)) + · apply pow_ne_zero ((q + 1) / 4) (v_ne_zero hs_ne_zero hq_card hq_mod t) + +omit [Fintype F] in +lemma v_comparison (t : { t : F // t ≠ 1 ∧ t ≠ -1}) : + let t1 := t.val + let t2 := -t1 + let u1 := u t + let v2 := v ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s + let r := r s + v2 = 1 / u1^5 + (r^2 - 2) * 1 / u1^3 + 1 / u1 := by + intro t1 t2 u1 v2 r_of_s + let u2 := u ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ + calc + v2 = u2^5 + (r_of_s^2 - 2) * u2^3 + u2 := by rfl + _ = 1 / u1^5 + (r_of_s^2 - 2) * 1/ u1^3 + 1 / u1 := by + unfold u2 u1 t2 t1 + rw [u_comparison t] + ring_nf + +omit [Fintype F] in +lemma v_comparison_implication1 (t : { t : F // t ≠ 1 ∧ t ≠ -1}) : + let t1 := t.val + let t2 := -t1 + let u1 := u t + let v1 := v t s + let v2 := v ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s + v2 * u1^6 = v1 := by + intro t1 t2 u1 v1 v2 + let r := r s + calc + v2 * u1^6 = u1 + (r^2 - 2) * u1^3 + u1^5 := by + unfold v2 + rw [v_comparison t] + grind + _ = v1 := by grind [v] + +omit [Fintype F] in +lemma v_comparison_implication2 (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : + let t1 := t.val + let t2 := -t1 + let u1 := u t + let v1 := v t s + let v2 := v ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s + v2 = v1 / u1^6 := by + intro t1 t2 u1 v1 v2 + have hu1_pow6_ne_zero : u1^6 ≠ 0 := pow_ne_zero 6 (u_ne_zero t) + rw [← mul_right_inj' hu1_pow6_ne_zero] + unfold v1 + rw [← v_comparison_implication1 t] + grind + +lemma v_comparison_implication3 + [DecidableEq F] + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : χ ((u t)^6) = 1 := by + let u := u t + have h : u^6 = u^2 * u^2 * u^2 := by ring_nf + rw [h, χ_mul, χ_mul, χ_sq (u_ne_zero t)] + rw [mul_one, mul_one] + +lemma v_comparison_implication4 + [DecidableEq F] + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let t1 := t.val + let t2 := -t1 + let v1 := v t s + let v2 := v ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s + χ v2 = χ v1 := by + intro t1 t2 v1 v2 + let u := u t + unfold v1 + rw [← v_comparison_implication1 t] + change χ v2= χ (v2 * u^6) + rw [χ_mul] + rw [v_comparison_implication3 t] + simp + +omit [Fintype F] in +@[simp] +lemma v_of_zero : + let v := v ⟨(0 : F), by simp⟩ s + v = (r s)^2 := by + intro v_of_t + unfold v_of_t v + rw [u_of_zero] + ring_nf + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/xProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/xProperties.lean new file mode 100644 index 000000000..e0bec67d7 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/xProperties.lean @@ -0,0 +1,113 @@ +/- +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.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 + +/-! +# x Variable Properties + +In this file we introduce some generally helpful lemmas for `x` as introduced in +`Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic + +variable {F : Type*} [Field F] [Fintype F] +variable {s : F} +variable {q : ℕ} + +lemma x_ne_zero + [DecidableEq 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) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let x := x t s q + x ≠ 0 := by + let c := c s + let X := X t s + let Y := Y t s q + change (c - 1) * s * X * (1 + X) / Y ≠ 0 + apply div_ne_zero + · apply mul_ne_zero + · apply mul_ne_zero + · apply mul_ne_zero + · intro hc_eq_one + have hc_eq_one' : c = 1 := by grind + exact (c_ne_one sq_ne_pm_two) hc_eq_one' + · apply hs_ne_zero + · apply X_ne_zero hs_ne_zero hq_card hq_mod t + · apply one_add_X_ne_zero hs_ne_zero hq_card hq_mod t + · apply Y_ne_zero hs_ne_zero hq_card hq_mod t + +lemma x_comparison + [DecidableEq F] + (t : { t : F // t ≠ 1 ∧ t ≠ -1}) + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : + let t1 := t.val + let t2 := -t1 + let x1 := x t s q + let x2 := x ⟨t2, neg_t_ne_one_and_neg_t_ne_neg_one t⟩ s q + x2 = x1 := by + intro t1 t2 x1 x2 + let c := c s + let t_h := neg_t_ne_one_and_neg_t_ne_neg_one t + let X1 := X t s + let X2 := X ⟨t2, t_h⟩ s + let Y1 := Y t s q + let Y2 := Y ⟨t2, t_h⟩ s q + have hX1_pow3_ne_zero : X1^3 ≠ 0 := pow_ne_zero 3 (X_ne_zero hs_ne_zero hq_card hq_mod t) + calc + x2 = (c - 1) * s * X2 * (1 + X2) / Y2 := by rfl + _ = (c - 1) * s * 1 / X1 * (1 + 1 / X1) / (Y1 / X1^3) := by grind [X_comparison, Y_comparison] + _ = (c - 1) * s * X1 * (1 + X1) / Y1 := by simp_all; grind + _ = x1 := by rfl + +lemma x_y_eq_zero_sign_one + (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (P : {P : F × F // P ∈ EOverF sq_ne_pm_two hq_card hq_mod}) + (hx_eq_zero : P.val.1 = 0) + : P.val = ((0 : F), (1 : F)) ∨ P.val = ((0 : F), (-1 : F)) := by + let d := d s + let x := P.val.1 + let y := P.val.2 + unfold EOverF at P + change (x, y) = (0, 1) ∨ (x, y) = (0, -1) + change x = 0 at hx_eq_zero + rw [← hx_eq_zero] + have h_curve_eq : x^2 + y^2 = 1 + d * x^2 * y^2 := by + let hP := P.prop + simp only [edwardsCurveEquation_iff] at hP + exact hP + have hy_eq_pm_one : y = 1 ∨ y = -1 := by grind + rcases hy_eq_pm_one with h | h + · rw [← h]; left; rfl + · rw [← h]; right; rfl + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/Elligator1/yProperties.lean b/Cslib/Crypto/Systems/Elligator/Elligator1/yProperties.lean new file mode 100644 index 000000000..fe19f1dd2 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/Elligator1/yProperties.lean @@ -0,0 +1,294 @@ +/- +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 + +/-! +# y Variable Properties + +In this file we introduce some generally helpful lemmas for `y` as introduced in +`Cslib.Crypto.Systems.Elligator.Elligator1.Variables`. + +## References + +See [bernstein2013a], Section 3.2, Theorem 1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.Elligator1 + +open Elligator.FiniteFieldBasic +open Elligator.LegendreSymbol + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {s : F} +variable {q : ℕ} + +lemma helper_eq + (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 X Y + let c := c s + let u := u t + let v := v t s + have hv_ne_zero := v_ne_zero hs_ne_zero hq_card hq_mod t + have h_X_expand_eq_chi_v_mul_v : X^5 + (r^2 - 2) * X^3 + X = χ v * v := by + calc + X^5 + (r^2 - 2) * X^3 + X = χ v * (u^5 + (r^2 - 2) * u^3 + u) := by + change (χ v * u)^5 + (r^2 - 2) * (χ v * u)^3 + (χ v * u) + = χ v * (u^5 + (r^2 -2 ) * u^3 + u) + rw [mul_pow (χ v) (u) 5, mul_pow (χ v) (u) 3] + rw [χ_of_a_pow_n_eq_χ_a v ⟨5, by trivial⟩] + rw [χ_of_a_pow_n_eq_χ_a v ⟨3, by trivial⟩] + ring_nf + _ = χ v * v := by rfl + have h_chi_v_mul_v_isSquare := χ_a_mul_a_IsSquare hv_ne_zero hq_card hq_mod + have h_chi_v_mul_v_fixed : (χ v * v)^((q + 1) / 2) = χ v * v := + a_pow_q_add_one_div_two_eq_a h_chi_v_mul_v_isSquare hq_card hq_mod + let χ_of_sum := χ (u^2 + 1 / c^2) + have h_Y_sq_eq_chi_v_mul_v : Y^2 = χ v * v := by + calc + Y^2 = (χ v * v)^((q + 1) / 2) * (χ v)^2 * χ_of_sum^2 := by + change ((χ v * v)^((q + 1) / 4) * χ v * χ_of_sum)^2 + = (χ v * v)^((q + 1) / 2) * (χ v)^2 * χ_of_sum^2 + ring_nf + rw [one_add_q_div_four_mul_two_eq_one_add_q_div_two hq_mod] + _ = (χ v * v)^((q + 1) / 2) * 1 := by + rw [χ_of_a_even_pow_n_eq_one hv_ne_zero ⟨2, even_two⟩] + rw [χ_of_a_even_pow_n_eq_one + (v_factored_third_factor_ne_zero hs_ne_zero hq_card hq_mod t) ⟨2, even_two⟩] + rw [mul_one] + _ = χ v * v := by rw [h_chi_v_mul_v_fixed, mul_one] + rw [h_X_expand_eq_chi_v_mul_v] + exact h_Y_sq_eq_chi_v_mul_v + +lemma y_divisor_ne_zero + (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}) + : + let r := r s; + let X := X t s + (r * X + (1 + X)^2) ≠ 0 := by + let Y := Y t s q + let c := c s + intro r X h_contra + have hr_mul_X_eq_neg_expand : r * X = -(1 + X)^2 := + Eq.symm (neg_eq_of_add_eq_zero_left h_contra) + have hY_sq_eq_neg_expand : Y^2 = -(1 + X)^2 * X^2 * (s + 2 / s)^2 := by + calc + Y^2 = X * (X^4 + (r^2 - 2) * X^2 + 1) := by grind [helper_eq] + _ = X^3 * (2 * r^2 + 4 * r) := by grind + _ = r * X * X^2 * (2 * r + 4) := by grind + _ = -(1 + X)^2 * X^2 * (s + 2 / s)^2 := by + rw [← hr_mul_X_eq_neg_expand] + change r * X * X^2 * (2 * (2 / s^2 + 1 / (2 / s^2)) + 4) = r * X * X^2 * (s + 2 / s)^2 + have h_algebra_identity : (2 * (2 / s^2 + 1 / (2 / s^2)) + 4) = (s + 2 / s)^2 := by + ring_nf + rw [inv_inv, mul_inv_cancel₀ hs_ne_zero, one_mul, mul_assoc] + rw [inv_mul_cancel₀ (two_ne_zero hq_card hq_mod)] + ring_nf + rw [h_algebra_identity] + have h_isSquare_neg_one : IsSquare (-1 : F) := by + have h_ratio_eq_neg_one : Y^2 / ((1 + X) * X * (s + 2 / s))^2 = -1 := by + rw [← neg_one_mul, mul_assoc (-1) ((1 + X)^2) (X^2)] at hY_sq_eq_neg_expand + rw [← mul_pow (1 + X) (X) 2, mul_assoc (-1) (((1 + X) * X)^2) _] at hY_sq_eq_neg_expand + rw [← mul_pow (((1 + X) * X))] at hY_sq_eq_neg_expand + have h_denom_ne_zero : ((1 + X) * X * (s + 2 / s))^2 ≠ 0 := by + apply pow_ne_zero 2 + apply mul_ne_zero + · apply mul_ne_zero + · apply one_add_X_ne_zero hs_ne_zero hq_card hq_mod t + · apply X_ne_zero hs_ne_zero hq_card hq_mod t + · grind + rw [← div_left_inj' h_denom_ne_zero, mul_div_assoc, div_self h_denom_ne_zero, mul_one] + at hY_sq_eq_neg_expand + exact hY_sq_eq_neg_expand + have h_ratio_sq_eq_neg_one : (Y / ((1 + X) * X * (s + 2 / s)))^2 = -1 := by + rw [← div_pow] at h_ratio_eq_neg_one + exact h_ratio_eq_neg_one + rw [← h_ratio_sq_eq_neg_one, pow_two] + apply IsSquare.mul_self + have h_mod_ne_three : q % 4 ≠ 3 := by + rw [FiniteField.isSquare_neg_one_iff, hq_card] at h_isSquare_neg_one + exact h_isSquare_neg_one + contradiction + +lemma y_add_one_ne_zero + (hs_ne_zero : s ≠ 0) + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + (t : {n : F // n ≠ 1 ∧ n ≠ -1}) + : + let y := y t s + y + 1 ≠ (0 : F) := by + let r := r s; + let X := X t s + intro y h_contra + have hy_eq_neg_one : y = -1 := Eq.symm (neg_eq_of_add_eq_zero_left h_contra) + have hy_unfolded_eq_neg_one : (r * X - (1 + X)^2) / (r * X + (1 + X)^2) = -1 := by + change y = -1 + exact hy_eq_neg_one + have h_num_eq_neg_denom : r * X - (1 + X)^2 = -(r * X + (1 + X)^2) := by grind + have hr_mul_X_eq_zero : r * X = 0 := by + rw [← add_left_inj (r * X + (1 + X)^2)] at h_num_eq_neg_denom + ring_nf at h_num_eq_neg_denom + rw [← div_left_inj' (two_ne_zero hq_card hq_mod), mul_div_assoc] at h_num_eq_neg_denom + rw [div_self (two_ne_zero hq_card hq_mod)] at h_num_eq_neg_denom + ring_nf at h_num_eq_neg_denom + exact h_num_eq_neg_denom + have hr_mul_X_ne_zero : r * X ≠ 0 := mul_ne_zero + (r_ne_zero hs_ne_zero hq_card hq_mod) (X_ne_zero hs_ne_zero hq_card hq_mod t) + contradiction + +lemma 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 := by + apply mul_ne_zero + · apply mul_ne_zero + · apply mul_ne_zero + · apply mul_ne_zero + · apply mul_ne_zero + · apply u_ne_zero t + · apply v_ne_zero hs_ne_zero hq_card hq_mod t + · apply X_ne_zero hs_ne_zero hq_card hq_mod t + · apply Y_ne_zero hs_ne_zero hq_card hq_mod t + · apply x_ne_zero hs_ne_zero sq_ne_pm_two hq_card hq_mod t + · apply y_add_one_ne_zero hs_ne_zero hq_card hq_mod t + +lemma 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 + x^2 + y^2 = 1 + d * x^2 * y^2 := by + let c := c s + let r := r s + let X := X t s + let Y := Y t s q + intro x y d + have h_c_sub_one_sq_mul_s_sq_eq : (c - 1)^2 * s^2 = 2 * (r - 2) := + calc + (c - 1)^2 * s^2 = (c - 1)^2 * (2 / c) := by grind [s_pow_two_eq_two_div_c] + _ = 2 * (r - 2) := by + rw [sub_pow_two, mul_one, one_pow 2, add_mul, sub_mul] + rw [← mul_div_assoc, one_mul, mul_comm, pow_two, ← mul_assoc] + rw [mul_div_assoc, div_self (c_ne_zero hs_ne_zero hq_card hq_mod), mul_one] + nth_rw 4 [← mul_one 2] + rw [add_comm, ← add_sub_assoc, mul_div_assoc, ← mul_add 2 (1 / c) c, add_comm] + change 2 * r - 2 * c * (2 / c) = 2 * (r - 2) + ring_nf + rw [mul_inv_cancel₀ (c_ne_zero hs_ne_zero hq_card hq_mod)] + ring_nf + have h_Y_sq_mul_one_sub_x_sq_eq : Y^2 * (1 - x^2) = X * (r * X - (1 + X)^2)^2 := by + calc + Y^2 * (1 - x^2) = Y^2 - (c - 1)^2 * s^2 * X^2 * (1 + X)^2 := by + change Y^2 * (1 - (((c - 1) * s * X * (1 + X)) / Y)^2) + = Y^2 - (c - 1)^2 * s^2 * X^2 * (1 + X)^2 + rw [mul_sub, mul_one] + have hY_sq_ne_zero : Y^2 ≠ 0 := pow_ne_zero 2 (Y_ne_zero hs_ne_zero hq_card hq_mod t) + grind + _ = X^5 + (r^2 - 2) * X^3 + X - 2 * (r - 2) * X^2 * (1 + X)^2 := by + rw [h_c_sub_one_sq_mul_s_sq_eq, helper_eq t hs_ne_zero hq_card hq_mod] + _ = X * (r * X - (1 + X)^2)^2 := by ring_nf + have h_neg_d_mul_c_sub_one_sq_mul_s_sq_eq : -d * (c - 1)^2 * s^2 = 2 * (r + 2) := by + rw [neg_d_eq_r_add_two_div_r_sub_two hs_ne_zero hq_card hq_mod, mul_assoc, + h_c_sub_one_sq_mul_s_sq_eq] + rw [mul_comm, ← mul_div_assoc, mul_assoc, mul_comm (r - 2) (r + 2), ← mul_assoc] + have hr_sub_two_ne_zero : r - 2 ≠ 0 := by + intro hr_sub_two_eq_zero + have h_c_sub_one_sq_mul_s_sq_eq_zero : (c - 1)^2 * s^2 = 0 := by grind + have h_c_sub_one_sq_mul_s_sq_ne_zero : (c - 1)^2 * s^2 ≠ 0 := by + apply mul_ne_zero + · exact pow_ne_zero 2 (c_sub_one_ne_zero sq_ne_pm_two) + · exact pow_ne_zero 2 hs_ne_zero + contradiction + rw [mul_div_assoc, div_self hr_sub_two_ne_zero, mul_one] + have h_Y_sq_mul_one_sub_d_mul_x_sq_eq : Y^2 * (1 - d * x^2) = X * (r * X + (1 + X)^2)^2 := by + calc + Y^2 * (1 - d * x^2) = Y^2 - d * (c - 1)^2 * s^2 * X^2 * (1 + X)^2 := by + change Y^2 * (1 - d * (((c - 1) * s * X * (1 + X)) / Y)^2) + = Y^2 - d * (c - 1)^2 * s^2 * X^2 * (1 + X)^2 + rw [mul_sub, mul_one] + have hY_sq_ne_zero : Y^2 ≠ 0 := pow_ne_zero 2 (Y_ne_zero hs_ne_zero hq_card hq_mod t) + rw [div_pow, ← mul_assoc, mul_comm (Y^2)] + grind + _ = X^5 + (r^2 - 2) * X^3 + X + 2 * (r + 2) * X^2 * (1 + X)^2 := by + rw [helper_eq t hs_ne_zero hq_card hq_mod] + grind + _ = X * (r * X + (1 + X)^2)^2 := by grind + have h_one_sub_d_mul_x_sq_ne_zero : (1 - d * x^2) ≠ 0 := by + intro h_one_sub_d_mul_x_sq_eq_zero + have hd_isSquare : IsSquare d := by + rw [← add_right_inj (d * x^2), add_comm] at h_one_sub_d_mul_x_sq_eq_zero + have h_cancel_identity : 1 - d * x^2 + d * x^2 = 1 := by ring + rw [add_zero, h_cancel_identity] at h_one_sub_d_mul_x_sq_eq_zero + have hx_sq_ne_zero : x^2 ≠ 0 := pow_ne_zero 2 + (x_ne_zero hs_ne_zero sq_ne_pm_two hq_card hq_mod t) + rw [← div_left_inj' hx_sq_ne_zero] at h_one_sub_d_mul_x_sq_eq_zero + rw [mul_div_assoc, div_self hx_sq_ne_zero, mul_one] at h_one_sub_d_mul_x_sq_eq_zero + rw [← mul_one 1, ← pow_two, ← div_pow _ _ 2] at h_one_sub_d_mul_x_sq_eq_zero + rw [← h_one_sub_d_mul_x_sq_eq_zero, pow_two] + apply IsSquare.mul_self + have hd_not_isSquare : ¬IsSquare d := d_nonsquare sq_ne_pm_two hq_card hq_mod + contradiction + have h_Y_sq_mul_one_sub_d_mul_x_sq_ne_zero : Y^2 * (1 - d * x^2) ≠ 0 := by + apply mul_ne_zero + · exact pow_ne_zero 2 (Y_ne_zero hs_ne_zero hq_card hq_mod t) + · exact h_one_sub_d_mul_x_sq_ne_zero + have h_ratio_eq_y_sq : (1 - x^2) / (1 - d * x^2) = y^2 := by + calc + (1 - x^2) / (1 - d * x^2) = (r * X - (1 + X)^2)^2 / (r * X + (1 + X)^2)^2 := by + have h_Y_sq_div_self_eq_one : Y^2 / Y^2 = 1 := by + have hY_sq_ne_zero : Y^2 ≠ 0 := pow_ne_zero 2 (Y_ne_zero hs_ne_zero hq_card hq_mod t) + rw [div_self hY_sq_ne_zero] + nth_rw 1 [← one_mul (1 - x^2), ← h_Y_sq_div_self_eq_one] + rw [mul_div_assoc, ← mul_div_mul_comm, h_Y_sq_mul_one_sub_x_sq_eq, + h_Y_sq_mul_one_sub_d_mul_x_sq_eq] + rw [mul_div_mul_comm X _ X _, div_self (X_ne_zero hs_ne_zero hq_card hq_mod t), one_mul] + _ = y^2 := by + rw [← div_pow _ _ 2] + change y^2 = y^2 + rfl + grind + +end Cslib.Crypto.Systems.Elligator.Elligator1 diff --git a/Cslib/Crypto/Systems/Elligator/FiniteFieldBasic.lean b/Cslib/Crypto/Systems/Elligator/FiniteFieldBasic.lean new file mode 100644 index 000000000..4d5ad66a7 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/FiniteFieldBasic.lean @@ -0,0 +1,247 @@ +/- +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, Matthias Güdemann +-/ +module + +public import Cslib.Crypto.Systems.Elligator.Basic +public import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic +public import Mathlib.FieldTheory.Finite.GaloisField + +/-! +# Finite Field Basic + +In this file we introduce some generally helpful lemmas for the finite field `F` with +`q` fulfilling `IsPrimePow`/`Prime`, `Fintype.card F = q` and `q % 4 = 3`. + +The assumption `IsPrimePow q` of [bernstein2013a] never has to be stated: by +`card_isPrimePow` it is a consequence of `Fintype.card F = q`, so `q` ranges over exactly the +prime powers congruent to `3` modulo `4`. Conversely, `prime_of_natCast_surjective` shows that +representing field elements by the naturals `0, 1, …, q - 1`, as the string encoding of +Section 3.4 does, is possible only when `q` is prime. + +## References + +See [bernstein2013a] for the original account on this specifc finite field. +-/ + +@[expose] public section + +variable {F : Type*} [Field F] [Fintype F] +variable {q : ℕ} + +namespace Cslib.Crypto.Systems.Elligator.FiniteFieldBasic + +/-- The cardinality of a finite field is always a prime power. + +This is why no statement of this development has to assume `IsPrimePow q`: the hypothesis +`Fintype.card F = q` already forces `q` to be a prime power, so all results proved for a finite +field `F` with `Fintype.card F = q` and `q % 4 = 3` are exactly the results of [bernstein2013a] +for an arbitrary prime power `q ≡ 3 (mod 4)`. -/ +lemma card_isPrimePow (hq_card : Fintype.card F = q) : IsPrimePow q := by + rw [← hq_card] + exact FiniteField.isPrimePow_card F + +omit [Field F] in +lemma q_odd (hq_mod : q % 4 = 3) : Odd q := by + rw [Nat.odd_iff] + omega + +omit [Field F] in +lemma q_sub_one_div_two_odd (hq_mod : q % 4 = 3) : Odd ((q - 1) / 2) := by + rw [Nat.odd_iff] + omega + +omit [Field F] in +lemma q_sub_one_even (hq_mod : q % 4 = 3) : Even (q - 1) := by + rw [Nat.even_iff] + omega + +omit [Fintype F] in +lemma one_ne_zero : (1 : F) ≠ 0 := by exact one_ne_zero' F + +lemma q_add_one_div_four_ne_zero (hq_mod : q % 4 = 3) : (1 + q) / 4 ≠ 0 := by + apply Nat.div_ne_zero_iff.mpr + norm_num + have hqle : q ≥ 3 := by lia + exact Nat.sub_le_iff_le_add'.mp hqle + +lemma q_add_one_div_two_ne_zero (hq_mod : q % 4 = 3) : (1 + q) / 2 ≠ 0 := by + apply Nat.div_ne_zero_iff.mpr + norm_num + have hqle : q ≥ 2 := by lia + exact Nat.le_add_left_of_le hqle + +lemma two_ne_zero (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : (2 : F) ≠ 0 := by + intro h + -- turn `(2 : F) = 0` into a divisibility statement about the characteristic + have hdvd : ringChar F ∣ 2 := (CharP.cast_eq_zero_iff F (ringChar F) 2).mp h + -- ringChar F ∣ 2 and ringChar F ≠ 1 (F is nontrivial) forces ringChar F = 2 + have hp : ringChar F = 2 := by + rcases (Nat.dvd_prime Nat.prime_two).mp hdvd with hchar | hchar + · exact absurd hchar (CharP.char_ne_one F (ringChar F)) + · exact hchar + have hchar : CharP F 2 := by + rw [← hp] + exact ringChar.charP F + -- a finite field of characteristic 2 has cardinality a power of 2 + obtain ⟨n, -, hcard⟩ := FiniteField.card F 2 + have hqeq : q = 2^(n : ℕ) := by rw [← hq_card, hcard] + have hdvd2 : (2 : ℕ) ∣ q := by + rw [hqeq] + exact dvd_pow_self 2 n.pos.ne' + -- q even contradicts q % 4 = 3 + omega + +lemma four_ne_zero (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : (4 : F) ≠ 0 := by + have hnum : (4 : F) = 2 * 2 := by norm_num + rw [hnum] + apply mul_ne_zero + · exact (two_ne_zero hq_card hq_mod) + · exact (two_ne_zero hq_card hq_mod) + +lemma ringChar_ne_two (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : ringChar F ≠ 2 := by + intro hchar + apply two_ne_zero hq_card hq_mod + have hcon : (2 : F) = 0 := (ringChar.spec F 2).mpr (by rw [hchar]) + exact hcon + +omit [Fintype F] in +lemma neg_one_ne_zero : (-1 : F) ≠ 0 := neg_ne_zero.mpr one_ne_zero + +lemma neg_one_non_square (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : ¬IsSquare (-1 : F) := by grind [FiniteField.isSquare_neg_one_iff] + +/-- If some algebraic identity would force `-1` to be a square, contradiction — `-1` is never +a square when `q % 4 = 3`. A common closing step for the `r`/`d` nonvanishing proofs. -/ +lemma false_of_isSquare_neg_one (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + (h : IsSquare (-1 : F)) : False := neg_one_non_square hq_card hq_mod h + +omit [Fintype F] in +lemma one_sub_t_ne_zero (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : (1 : F) - t.val ≠ 0 := + sub_ne_zero.mpr t.prop.1.symm + +omit [Fintype F] in +lemma one_add_t_ne_zero (t : {n : F // n ≠ 1 ∧ n ≠ -1}) : (1 : F) + t.val ≠ 0 := by + intro h + rw [add_comm] at h + exact t.prop.2 (eq_neg_of_add_eq_zero_left h) + +omit [Fintype F] in +lemma neg_t_ne_one_and_neg_t_ne_neg_one (t : { t : F // t ≠ 1 ∧ t ≠ -1}) : + -t.val ≠ 1 ∧ -t.val ≠ -1 := by + constructor + · intro h + apply t.prop.2 + have := congrArg Neg.neg h + simpa using this + · intro h + apply t.prop.1 + have := congrArg Neg.neg h + simpa using this + +omit [Fintype F] in +lemma not_t_ne_one_and_t_ne_neg_one (t : { t : F // t = 1 ∨ t = -1}) : + ¬(t.val ≠ 1 ∧ t.val ≠ -1) := by + rcases t.prop with th | th <;> simp [th] + +omit [Field F] in +lemma one_add_q_div_four_mul_two_eq_one_add_q_div_two (hq_mod : q % 4 = 3) + : ((1 + q) / 4 * 2) = (1 + q) / 2 := by omega + +/-- If `F` has `q` elements and `q` is prime, `q` is literally the characteristic of `F`. -/ +lemma ringChar_of_F_eq_q (hq_card : Fintype.card F = q) (q_prime : Prime q) : ringChar F = q := by + -- Every finite field's cardinality is a power of its characteristic, and the + -- characteristic itself is prime. + obtain ⟨n, h_char_prime, h_card_eq_pow⟩ := FiniteField.card F (ringChar F) + have h_q_eq_pow : q = (ringChar F) ^ (n : ℕ) := by rw [← hq_card, h_card_eq_pow] + -- In particular `ringChar F` divides `q` (the exponent `n` is at least `1`). + have h_dvd : ringChar F ∣ q := h_q_eq_pow ▸ dvd_pow_self _ n.pos.ne' + -- `q` is prime, so its only divisors are `1` and `q` - and a field's characteristic + -- is never `1`, so it must be `q` itself. + rcases (Nat.dvd_prime (Nat.prime_iff.mpr q_prime)).1 h_dvd with hchar | hchar + · exact absurd hchar h_char_prime.ne_one + · exact hchar + +/-- The cast `Fin q → F` is injective -/ +lemma fin_to_finfield_injective (hq_card : Fintype.card F = q) (q_prime : Prime q) + : Function.Injective (fun n : Fin q => (n : F)) := by + intro a b hab + have h : CharP F q := by + rw [← ringChar_of_F_eq_q hq_card q_prime] + exact ringChar.charP F + exact Fin.ext (CharP.natCast_injOn_Iio F q a.isLt b.isLt hab) + +lemma fin_to_finfield_bijective (hq_card : Fintype.card F = q) (q_prime : Prime q) : + Function.Bijective (fun n : Fin q => (n : F)) := + (Fintype.bijective_iff_injective_and_card _).mpr + ⟨fin_to_finfield_injective hq_card q_prime, by rw [Fintype.card_fin, hq_card]⟩ + +/-- Every element of `F` is the cast of some `n : Fin q`: +this cast is injective and `Fin q` and `F` have the same cardinality, so it is bijective. -/ +lemma exists_fin_cast_eq (hq_card : Fintype.card F = q) (q_prime : Prime q) (t : F) : + ∃ n : Fin q, (n : F) = t := (fin_to_finfield_bijective hq_card q_prime).surjective t + +/- Every element of F can be written as (n : F) for some n < q because Fintype.card F = q and +the natural cast n ↦ (n : F) has period equal to ringChar F = q (since q is prime), +so {(0 : F), (1 : F), ..., (q-1 : F)} gives all q distinct elements. -/ +lemma exists_nat_cast_eq + (hq_card : Fintype.card F = q) + (q_prime : Prime q) + (t : F) + : ∃ (n : ℕ), n < q ∧ (n : F) = t := by + obtain ⟨n, hn⟩ : ∃ n : Fin q, (n : F) = t := exists_fin_cast_eq hq_card q_prime t + exact ⟨n.val, n.isLt, hn⟩ + +/-- A natural number `q` is the cardinality of some finite field iff it is a prime power. + +Together with `Cslib.Crypto.Systems.Elligator.FiniteFieldBasic.card_isPrimePow` this says that +the standing hypotheses `Fintype.card F = q`, `q % 4 = 3` of this development describe exactly +the setting of [bernstein2013a], Section 3.1: an arbitrary prime power `q ≡ 3 (mod 4)`. -/ +lemma exists_field_card_eq_iff_isPrimePow (q : ℕ) : + (∃ (F : Type) (_ : Field F) (_ : Fintype F), Fintype.card F = q) ↔ IsPrimePow q := by + constructor + · rintro ⟨F, _, _, hcard⟩ + exact card_isPrimePow hcard + · rintro ⟨p, k, hp, hk, rfl⟩ + have hp' : Nat.Prime p := Nat.prime_iff.mpr (by exact_mod_cast hp) + have hfact : Fact (Nat.Prime p) := ⟨hp'⟩ + have hk0 : k ≠ 0 := hk.ne' + have htype : Fintype (GaloisField p k) := Fintype.ofFinite _ + refine ⟨GaloisField p k, inferInstance, inferInstance, ?_⟩ + have hcard := GaloisField.card p k hk0 + rw [Nat.card_eq_fintype_card] at hcard + exact hcard + +/-- If every element of `F` is the image of a natural number under the canonical cast, then the +cardinality of `F` is *prime*, not merely a *prime power*. + +This is the precise reason why the string encoding `ι` of [bernstein2013a], Section 3.4, is +formalized for prime `q` only: it represents field elements by the naturals +`0, 1, ..., q - 1`, which requires the natural casts to exhaust `F`. The `ϕ` part of the +development makes no such assumption and therefore covers all *prime powers*. -/ +lemma prime_of_natCast_surjective + (hq_card : Fintype.card F = q) + (hsurj : Function.Surjective (Nat.cast : ℕ → F)) + : q.Prime := by + have h_char_prime : (ringChar F).Prime := CharP.char_is_prime F (ringChar F) + -- Step 1: the cast `Fin (ringChar F) → F` is surjective. + have h_surj : Function.Surjective (fun k : Fin (ringChar F) => ((k : ℕ) : F)) := by + intro t + obtain ⟨n, hn⟩ := hsurj t + refine ⟨⟨n % ringChar F, Nat.mod_lt _ h_char_prime.pos⟩, ?_⟩ + simpa [CharP.cast_eq_mod F (ringChar F) n] using hn + -- Step 2: the same cast is always injective below the characteristic - the defining + -- property of `ringChar`. + have h_inj : Function.Injective (fun k : Fin (ringChar F) => ((k : ℕ) : F)) := fun a b hab => + Fin.ext (CharP.natCast_injOn_Iio F (ringChar F) a.isLt b.isLt hab) + -- Step 3: surjective gives `card F ≤ ringChar F`; injective gives `ringChar F ≤ card F`. + -- Together, `card F = ringChar F` exactly. + have h_le : Fintype.card F ≤ ringChar F := by simpa using Fintype.card_le_of_surjective _ h_surj + have h_ge : ringChar F ≤ Fintype.card F := by simpa using Fintype.card_le_of_injective _ h_inj + have h_eq : q = ringChar F := by omega + rw [h_eq] + exact h_char_prime + +end Cslib.Crypto.Systems.Elligator.FiniteFieldBasic diff --git a/Cslib/Crypto/Systems/Elligator/LegendreSymbol.lean b/Cslib/Crypto/Systems/Elligator/LegendreSymbol.lean new file mode 100644 index 000000000..4bc2f11c1 --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/LegendreSymbol.lean @@ -0,0 +1,196 @@ +/- +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.FiniteFieldBasic + +/-! +# Legendre Symbol + +In this file we introduce a special case of the traditional Legendre Symbol. + +The quadratic character `χ` used here is Mathlib's `quadraticChar`, whose values are cast from +`ℤ` into the finite field `F` itself; this is the form in which the Elligator 1 paper uses it. +All the facts below are consequences of the Mathlib API for `quadraticChar`, specialised to a +field `F` with `Fintype.card F = q` and `q % 4 = 3`. + +## References + +See [bernstein2013a], Section 3.1. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Systems.Elligator.LegendreSymbol + +open Elligator.FiniteFieldBasic + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {q : ℕ} + +/-- χ(a) is the quadratic character of a in the finite field F with q elements, where q is a +prime congruent to 3 modulo 4, viewed as an element of `F`. + +This is Mathlib's `quadraticChar` composed with the cast `ℤ → F`, since +`Mathlib.NumberTheory.LegendreSymbol.Basic` is restricted to `ℤ`. +-/ +def χ (a : F) : F := ((quadraticChar F a : ℤ) : F) + +@[simp] +lemma χ_zero : χ (0 : F) = 0 := by simp [χ] + +lemma χ_one : χ (1 : F) = 1 := by simp [χ] + +/-- Euler's criterion: `χ` is given by the `(q - 1) / 2`-th power. -/ +lemma χ_eq_pow (a : F) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : χ a = a^((q - 1) / 2) := by + have h : (q - 1) / 2 = Fintype.card F / 2 := by + rw [hq_card] + omega + rw [χ, h] + exact quadraticChar_eq_pow_of_char_ne_two' (ringChar_ne_two hq_card hq_mod) a + +lemma χ_values {a : F} : χ a = 0 ∨ χ a = -1 ∨ χ a = 1 := by + rcases eq_or_ne a 0 with ha | ha + · simp [ha] + · rcases quadraticChar_dichotomy ha with h | h <;> simp [χ, h] + +lemma χ_a_ne_zero {a : F} (a_ne_zero : a ≠ 0) : χ a ≠ 0 := by + rcases quadraticChar_dichotomy a_ne_zero with h | h <;> simp [χ, h] + +lemma a_eq_zero_of_χ_of_a_eq_zero {a : F} : χ a = 0 → a = 0 := by + intro h + by_contra ha + apply χ_a_ne_zero ha + exact h + +@[simp] +lemma χ_a_eq_one {a : F} (a_ne_zero : a ≠ 0) (a_square : IsSquare a) : χ a = 1 := by + rw [χ, (quadraticChar_one_iff_isSquare a_ne_zero).mpr a_square] + simp + +lemma χ_eq_one_iff_isSquare {a : F} + (a_ne_zero : a ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : χ a = 1 ↔ IsSquare a := by + constructor + · intro h + rcases quadraticChar_dichotomy a_ne_zero with h' | h' + · exact (quadraticChar_one_iff_isSquare a_ne_zero).mp h' + · simp_all only [χ] + have heq : (2 : F) = 0 := by grind + have hne : (2 : F) ≠ 0 := by simp_all [FiniteFieldBasic.two_ne_zero] + contradiction + · exact χ_a_eq_one a_ne_zero + +@[simp] +lemma χ_sq {a : F} (a_ne_zero : a ≠ 0) : χ (a ^ 2) = 1 := by + rw [χ, quadraticChar_sq_one' a_ne_zero, Int.cast_one] + +lemma χ_neg_one (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : χ (-1 : F) = -1 := by + rw [χ, quadraticChar_neg_one_iff_not_isSquare.mpr (neg_one_non_square hq_card hq_mod)] + simp + +lemma χ_mul {a b : F} : χ (a * b) = (χ a) * (χ b) := by + simp [χ, quadraticCharFun_mul] + +lemma neg_χ_a_ne_χ_a {a : F} + (a_ne_zero : a ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : χ a ≠ -(χ a) := by + intro h + have heq : (2 : F) * χ a = 0 := by + rw [← add_left_inj (χ a)] at h + ring_nf at h + rwa [mul_comm] + rcases mul_eq_zero.mp heq with hzero | hzero + · exact two_ne_zero hq_card hq_mod hzero + · exact χ_a_ne_zero a_ne_zero hzero + +@[simp] +lemma χ_of_a_even_pow_n_eq_one {a : F} + (a_ne_zero : a ≠ 0) (n : {n : ℕ | Even n}) + : χ a ^ (n.val) = 1 := by + rcases χ_values (a := a) with h | h | h + · exact absurd h (χ_a_ne_zero a_ne_zero) + · rw [h] + exact n.prop.neg_one_pow + · rw [h, one_pow] + +@[simp] +lemma χ_of_a_pow_n_eq_χ_a (a : F) (n : {n : ℕ | Odd n}) + : (χ a) ^ (n.val) = χ a := by + have hn := n.prop + rcases χ_values (a := a) with h | h | h + · rw [h, zero_pow hn.pos.ne'] + · rw [h] + exact hn.neg_one_pow + · rw [h, one_pow] + +lemma χ_χ_eq_χ {a : F} + (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : χ (χ a) = χ a := by + rcases χ_values (a := a) with h | h | h + · rw [h, χ_zero] + · rw [h, χ_neg_one hq_card hq_mod] + · rw [h, χ_one] + +lemma χ_inv {a : F} : χ a = χ (1 / a) := by + rcases eq_or_ne a 0 with rfl | ha + · simp + · have heq : χ (1 / a) * χ a = 1 := by + rw [← χ_mul, one_div, inv_mul_cancel₀ ha, χ_one] + rcases χ_values (a := a) with h | h | h + · exact absurd h (χ_a_ne_zero ha) + · rw [h] at heq ⊢ + grind + · rw [h] at heq ⊢ + grind + +lemma one_div_χ_of_a_eq_χ_a {a : F} : χ a = 1 / χ a := by + rcases χ_values (a := a) with h | h | h <;> rw [h] <;> norm_num + +/-- Multiplying by a nonzero square does not change the quadratic character. +Introduced in paper theory theorem 3.A proof. -/ +lemma χ_of_a_eq_χ_a_mul_b_pow_two {a b : F} (b_ne_zero : b ≠ 0) + : χ (a * b ^ 2) = χ a := by + rw [χ_mul, χ_sq b_ne_zero, mul_one] + +lemma a_pow_q_add_one_div_two_eq_χ_of_a_mul_a + {a : F} + (hq_card : Fintype.card F = q) + (hq_mod : q % 4 = 3) + : a ^ ((q + 1) / 2) = (χ a) * a := by + rw [χ_eq_pow a hq_card hq_mod, ← pow_succ] + congr 1 + omega + +omit [DecidableEq F] in +@[simp] +lemma a_pow_q_add_one_div_two_eq_a {a : F} + (a_square : IsSquare a) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : a ^ ((q + 1) / 2) = a := by + rcases eq_or_ne a 0 with rfl | ha + · exact zero_pow (by omega) + · classical + rw [a_pow_q_add_one_div_two_eq_χ_of_a_mul_a hq_card hq_mod] + rw [χ_a_eq_one ha a_square, one_mul] + +lemma b_pow_q_add_one_div_four_eq_χ_of_a_mul_a {a : F} + (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : (a ^ 2) ^ ((q + 1) / 4) = (χ a) * a := by + rw [← pow_mul] + have h : 2 * ((q + 1) / 4) = (q + 1) / 2 := by omega + rw [h, a_pow_q_add_one_div_two_eq_χ_of_a_mul_a hq_card hq_mod] + +lemma χ_a_mul_a_IsSquare {a : F} + (a_ne_zero : a ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) + : IsSquare ((χ a) * a) := by + have h : (χ a) * a ≠ 0 := mul_ne_zero (χ_a_ne_zero a_ne_zero) a_ne_zero + apply (χ_eq_one_iff_isSquare h hq_card hq_mod).mp + rw [χ_mul, χ_χ_eq_χ hq_card hq_mod, ← pow_two] + exact χ_of_a_even_pow_n_eq_one a_ne_zero ⟨2, even_two⟩ + +end Cslib.Crypto.Systems.Elligator.LegendreSymbol diff --git a/Cslib/Crypto/Systems/Elligator/TwistedEdwardsCurve.lean b/Cslib/Crypto/Systems/Elligator/TwistedEdwardsCurve.lean new file mode 100644 index 000000000..71da2683a --- /dev/null +++ b/Cslib/Crypto/Systems/Elligator/TwistedEdwardsCurve.lean @@ -0,0 +1,99 @@ +/- +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 Mathlib.Algebra.Ring.Commute +public import Mathlib.Data.Set.Defs + +/-! +# 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. +-/ + +@[expose] public section +namespace Cslib.Crypto.Systems.Elligator + +/-- Coefficients of the twisted Edwards equation +`a * x^2 + y^2 = 1 + d * x^2 * y^2`. -/ +@[ext] +structure TwistedEdwardsCurve (R : Type*) where + /-- left hand side coefficient -/ + a : R + /-- right hand side coefficient -/ + d : R + +namespace TwistedEdwardsCurve + +variable {R : Type*} [CommRing R] + +/-- The proposition that `(x, y)` is an affine point of a twisted Edwards curve. -/ +def Equation (E : TwistedEdwardsCurve R) (x y : R) : Prop := E.a * x^2 + y^2 = 1 + E.d * x^2 * y^2 + +/-- The set of affine coordinate pairs on a twisted Edwards curve. -/ +def affinePoints (E : TwistedEdwardsCurve R) : Set (R × R) := {p | E.Equation p.1 p.2} + +/-- A bundled affine point on a twisted Edwards curve. -/ +abbrev Point (E : TwistedEdwardsCurve R) := {p : R × R // p ∈ E.affinePoints} + +/-- The neutral affine coordinate pair `(0, 1)`. It lies on every twisted Edwards equation. -/ +def zero : R × R := (0, 1) + +@[simp] +theorem zero_mem_affinePoints (E : TwistedEdwardsCurve R) : zero ∈ E.affinePoints := by + change E.a * 0^2 + 1^2 = 1 + E.d * 0^2 * 1^2 + simp + +/-- The neutral point, bundled as an affine point of `E`. -/ +def zeroPoint (E : TwistedEdwardsCurve R) : E.Point := ⟨zero, E.zero_mem_affinePoints⟩ + +/-- Negation of affine coordinates on a twisted Edwards curve. -/ +def neg (p : R × R) : R × R := (-p.1, p.2) + +@[simp] +theorem neg_mem_affinePoints (E : TwistedEdwardsCurve R) (p : R × R) : + neg p ∈ E.affinePoints ↔ p ∈ E.affinePoints := by + change E.a * (-p.1)^2 + p.2^2 = 1 + E.d * (-p.1)^2 * p.2^2 ↔ + E.a * p.1^2 + p.2^2 = 1 + E.d * p.1^2 * p.2^2 + rw [neg_sq] + +/-- 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. +-/ +def IsValid (E : TwistedEdwardsCurve R) : Prop := E.a ≠ 0 ∧ E.d ≠ 0 ∧ E.a ≠ E.d + +/-- The (untwisted) Edwards curve with parameter `d`, obtained by setting `a = 1`. -/ +def ofD (d : R) : TwistedEdwardsCurve R where + a := 1 + d := d + +@[simp] +theorem ofD_equation (d x y : R) : (ofD d).Equation x y ↔ x^2 + y^2 = 1 + d * x^2 * y^2 := by + simp [Equation, ofD] + +@[simp] +theorem ofD_isValid_iff [Nontrivial R] (d : R) : (ofD d).IsValid ↔ d ≠ 0 ∧ d ≠ 1 := by + constructor + · rintro ⟨_, hd, had⟩ + exact ⟨hd, fun h ↦ had h.symm⟩ + · rintro ⟨hd, hd1⟩ + exact ⟨one_ne_zero, hd, fun h ↦ hd1 h.symm⟩ + +end TwistedEdwardsCurve +end Cslib.Crypto.Systems.Elligator diff --git a/references.bib b/references.bib index 6af9dafc4..8c9649848 100644 --- a/references.bib +++ b/references.bib @@ -509,3 +509,22 @@ @book{Papadimitriou94 publisher={Addison-Wesley}, address={Reading, Massachusetts} } + +@inproceedings{bernstein2013a, + location={Munich, Germany}, + author={Bernstein, Daniel J. and Hamburg, Mike and Krasnova, Anna and Lange, Tanja}, + title={Elligator: elliptic-curve points indistinguishable from uniform random strings}, + year={2013}, + isbn={9781450324779}, + publisher={Association for Computing Machinery}, + address={New York, NY, USA}, + url={https://doi.org/10.1145/2508859.2516734}, + doi={10.1145/2508859.2516734}, + abstract={Censorship-circumvention tools are in an arms race against censors. The censors study all traffic passing into and out of their controlled sphere, and try to disable censorship-circumvention tools without completely shutting down the Internet. Tools aim to shape their traffic patterns to match unblocked programs, so that simple traffic profiling cannot identify the tools within a reasonable number of traces; the censors respond by deploying firewalls with increasingly sophisticated deep-packet inspection. Cryptography hides patterns in user data but does not evade censorship if the censor can recognize patterns in the cryptography itself. In particular, elliptic-curve cryptography often transmits points on known elliptic curves, and those points are easily distinguishable from uniform random strings of bits.This paper introduces high-security high-speed elliptic-curve systems in which elliptic-curve points are encoded so as to be indistinguishable from uniform random strings. At a lower level, this paper introduces a new bijection between strings and about half of all curve points; this bijection is applicable to every odd-characteristic elliptic curve with a point of order 2, except for curves of $j$-invariant 1728. This paper also presents guidelines to construct, and two examples of, secure curves suitable for these encodings.}, + booktitle={Proceedings of the 2013 ACM SIGSAC Conference on Computer \& Communications Security}, + pages={967–980}, + numpages={14}, + keywords={injective maps, elliptic curves, censorship circumvention}, + location={Berlin, Germany}, + series={CCS '13} +}