String Encoding

This file formalizes Theorem 4 of the Elligator paper. A bit string in S is interpreted as a lower-half field representative by σ, then mapped to the Edwards curve by ϕ. Restricting to the lower half removes the sign ambiguity ϕ t = ϕ (-t).

Main results

• ι: the paper's encoding ι(τ) = ϕ(σ(τ)) from admissible bit strings to curve points.
• S_card: the admissible set has (q + 1) / 2 elements.
• ι_injective: ι is injective, so encoded strings have distinct curve images.
• ϕOverF_eq_ιOverS: the image of ι is exactly the image of the Elligator map ϕ.

Together, the last two results formalize the paper's conclusion that ι is a bijection from S onto ϕ(F).

References

See [bernstein2013a], Section 3.4, theorem 4.

def Elligator.Elligator1.ι {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (τ : ↥S) (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) : { P : F × F // P ∈ EOverF sq_ne_pm_two hq_card hq_mod }

The Elligator string encoding from Theorem 4 of the paper. For an admissible b-bit string τ ∈ S, ι τ is the curve point ϕ (σ τ). The return subtype records that this point lies on the Edwards curve.

Equations

• Elligator.Elligator1.ι τ hs_ne_zero sq_ne_pm_two hq_card hq_mod = Elligator.Elligator1.ϕ (Elligator.Elligator1.σ ↑τ) hs_ne_zero sq_ne_pm_two hq_card hq_mod

theorem Elligator.Elligator1.S_card {q : ℕ} (hq_mod : q % 4 = 3) : S.card = (q + 1) / 2

The admissible string set S has (q + 1) / 2 elements. This is the cardinality assertion in Theorem 4. Here S consists of the b-bit strings whose binary values lie in the integer interval from 0 through (q - 1) / 2.

theorem Elligator.Elligator1.σ_eq_of_eq_or_eq_neg {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) (τ τ' : ↥S) (h : σ ↑τ = σ ↑τ' ∨ σ ↑τ = -σ ↑τ') : σ ↑τ = σ ↑τ'

Lower-half representatives resolve the sign ambiguity of ϕ.

If two strings in S represent equal or opposite field elements, then they in fact represent the same field element: two distinct integers in [0, (q - 1) / 2] cannot be negatives modulo q.

theorem Elligator.Elligator1.ι_injective {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (q_prime : Prime q) (hq_mod : q % 4 = 3) : Function.Injective fun (τ : ↥S) => ι τ hs_ne_zero sq_ne_pm_two hq_card hq_mod

The Elligator string encoding ι : S → E(F) is injective.

Following Theorem 4 of the paper, equality of encoded points first gives equality of their field representatives up to sign by Theorem 3. Membership in the lower-half set S eliminates the negative case, and injectivity of binary evaluation then identifies the original strings.

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

The set of curve points produced by the string encoding ι. This is the range ι(S) appearing in Theorem 4 of the paper.

Equations

• Elligator.Elligator1.ιOverS hs_ne_zero sq_ne_pm_two hq_card hq_mod = Set.range fun (τ : ↥Elligator.Elligator1.S) => ↑(Elligator.Elligator1.ι τ hs_ne_zero sq_ne_pm_two hq_card hq_mod)

theorem Elligator.Elligator1.ϕOverF_eq_ιOverS {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (q_prime : Prime q) (hq_mod : q % 4 = 3) : have ϕOverF := ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod; have ιOverS := ιOverS hs_ne_zero sq_ne_pm_two hq_card hq_mod; ϕOverF = ιOverS

The string encoding and the Elligator map have exactly the same image: ι(S) = ϕ(F). For each t : F, one of t and -t has a lower-half representative σ τ with τ ∈ S; since ϕ t = ϕ (-t), this proves that every point in ϕ(F) is encoded by ι. The reverse inclusion is immediate from the definition ι τ = ϕ (σ τ). This is the surjectivity-onto-ϕ(F) part of Theorem 4.

def Elligator.Elligator1.ιToϕOverF {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (τ : ↥S) : { P : F × F // P ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod }

The encoding ι, with its codomain restricted to the image ϕ(F).

Unlike ι, whose codomain is the full Edwards curve, this map records in its result type the stronger fact that every encoded point belongs to the image of ϕ.

Equations

• Elligator.Elligator1.ιToϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod τ = ⟨↑(Elligator.Elligator1.ι τ hs_ne_zero sq_ne_pm_two hq_card hq_mod), ⋯⟩

theorem Elligator.Elligator1.ιToϕOverF_bijective {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (q_prime : Prime q) (hq_mod : q % 4 = 3) : Function.Bijective (ιToϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod)

The encoding ι is a bijection from S onto ϕ(F). The codomain restriction in ιToϕOverF makes “onto ϕ(F)” literal in the type. Injectivity is ι_injective, while surjectivity is the image equality ϕOverF_eq_ιOverS.