Elligator 1 Variables

In this file we introduce all the independent variables introduced in the definition of Elligator 1.

References

See [bernstein2013a], Section 3.

def Elligator.Elligator1.c {F : Type u_1} [Field F] (s : F) : F

c(s) is a function defined in the paper.

Original:, Section "3.2 The map": Theorem 1

Equations

• Elligator.Elligator1.c s = 2 / s ^ 2

def Elligator.Elligator1.r {F : Type u_1} [Field F] (s : F) : F

r(s) is a function defined in the paper.

Original:, Section "3.2 The map": Theorem 1

Equations

• Elligator.Elligator1.r s = Elligator.Elligator1.c s + 1 / Elligator.Elligator1.c s

def Elligator.Elligator1.d {F : Type u_1} [Field F] (s : F) : F

d(s) is a function defined in the paper.

Original:, Section "3.2 The map": Theorem 1

Equations

• Elligator.Elligator1.d s = -(Elligator.Elligator1.c s + 1) ^ 2 / (Elligator.Elligator1.c s - 1) ^ 2

def Elligator.Elligator1.u {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : F

u(t) is a function defined in the paper.

Original:, Section "3.2 The map": Theorem 1

Equations

• Elligator.Elligator1.u t = (1 - ↑t) / (1 + ↑t)

def Elligator.Elligator1.v {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) : F

v(t, s) is a function defined in the paper.

Original:, Section "3.2 The map": Theorem 1

Equations

• Elligator.Elligator1.v t s = Elligator.Elligator1.u t ^ 5 + (Elligator.Elligator1.r s ^ 2 - 2) * Elligator.Elligator1.u t ^ 3 + Elligator.Elligator1.u t

def Elligator.Elligator1.X {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) : F

X(t, s) is a function defined in the paper.

Original:, Section "3.2 The map": Theorem 1

Equations

• Elligator.Elligator1.X t s = Elligator.LegendreSymbol.χ (Elligator.Elligator1.v t s) * Elligator.Elligator1.u t

def Elligator.Elligator1.Y {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (q : ℕ) : F

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

Equations

• One or more equations did not get rendered due to their size.

def Elligator.Elligator1.x {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (q : ℕ) : F

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

Equations

• Elligator.Elligator1.x t s q = (Elligator.Elligator1.c s - 1) * s * Elligator.Elligator1.X t s * (1 + Elligator.Elligator1.X t s) / Elligator.Elligator1.Y t s q

def Elligator.Elligator1.y {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) : F

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

Equations

• One or more equations did not get rendered due to their size.

def Elligator.Elligator1.η {F : Type u_1} [Field F] (P : F × F) : F

η(s, q, point) is a function defined in the paper.

Original:, Section "3.3 Inverting the map": Theorem 3

Equations

• Elligator.Elligator1.η P = (P.2 - 1) / (2 * (P.2 + 1))

def Elligator.Elligator1.X2 {F : Type u_1} [Field F] (s : F) (P : F × F) (q : ℕ) : F

X2 is a function defined in the paper.

Original:, Section "3.3 Inverting the map": Theorem 3

Equations

• Elligator.Elligator1.X2 s P q = -(1 + Elligator.Elligator1.η P * Elligator.Elligator1.r s) + ((1 + Elligator.Elligator1.η P * Elligator.Elligator1.r s) ^ 2 - 1) ^ ((q + 1) / 4)

def Elligator.Elligator1.z {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (s : F) (P : F × F) (q : ℕ) : F

z is a function defined in the paper.

Original:, Section "3.3 Inverting the map": Theorem 3

Equations

• One or more equations did not get rendered due to their size.

def Elligator.Elligator1.u2 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (s : F) (P : F × F) (q : ℕ) : F

u2 is a function defined in the paper.

Original:, Section "3.3 Inverting the map": Theorem 3

Equations

• Elligator.Elligator1.u2 s P q = Elligator.Elligator1.z s P q * Elligator.Elligator1.X2 s P q

def Elligator.Elligator1.t2 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (s : F) (P : F × F) (q : ℕ) : F

t2 is a function defined in the paper.

Original:, Section "3.3 Inverting the map": Theorem 3

Equations

• Elligator.Elligator1.t2 s P q = (1 - Elligator.Elligator1.u2 s P q) / (1 + Elligator.Elligator1.u2 s P q)

def Elligator.Elligator1.b (q : ℕ) : ℕ

b q is ⌊log₂ q⌋, the number of bits needed.

Original:, Section "3.4 Encoding as strings": Theorem 4

Equations

• Elligator.Elligator1.b q = Nat.log 2 q

def Elligator.Elligator1.bitsToNat {n : ℕ} (τ : Fin n → Bool) : ℕ

Convert a bit vector (τ₀, τ₁, ..., τ_{b-1}) to a natural number via binary expansion: bitsToNat(τ) = Σᵢ τᵢ · 2^i.

Equations

• Elligator.Elligator1.bitsToNat τ = ∑ i : Fin n, if τ i = true then 2 ^ ↑i else 0

def Elligator.Elligator1.σ {F : Type u_1} [Field F] {q : ℕ} (τ : Fin (b q) → Bool) : F

σ 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

Equations

• Elligator.Elligator1.σ τ = ↑(Elligator.Elligator1.bitsToNat τ)

def Elligator.Elligator1.S {q : ℕ} : Finset (Fin (b q) → Bool)

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

Equations

• Elligator.Elligator1.S = {τ : Fin (Elligator.Elligator1.b q) → Bool | Elligator.Elligator1.bitsToNat τ ≤ (q - 1) / 2}