noncomputable def Elligator.Elligator1.c {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

• Elligator.Elligator1.c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = 2 / s ^ 2

noncomputable def Elligator.Elligator1.r {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.d {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.u {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

• Elligator.Elligator1.u t q field_cardinality q_prime_power q_mod_4_congruent_3 = (1 - ↑t) / (1 + ↑t)

noncomputable def Elligator.Elligator1.v {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.X {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.Y {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.x {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

x(t, s) is a function defined in the paper. It is the x-coordinate of the point on the curve.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.y {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

y(t, s) is a function defined in the paper. It is the y-coordinate of the point on the curve.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Elligator.Elligator1.η {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : F

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

Paper definition at chapter 3.3 theorem 3.

Equations

• Elligator.Elligator1.η q field_cardinality q_prime_power q_mod_4_congruent_3 point = (point.2 - 1) / (2 * (point.2 + 1))

noncomputable def Elligator.Elligator1.X2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : F

Equations

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

noncomputable def Elligator.Elligator1.z {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : F

Equations

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

noncomputable def Elligator.Elligator1.u2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : F

Equations

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

noncomputable def Elligator.Elligator1.t2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : F

Equations

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

noncomputable def Elligator.Elligator1.b {q : ℕ} : ℕ

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

Equations

• Elligator.Elligator1.b = 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

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

Equations

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

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

Equations

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