Curve1174

This file instantiates the general Elligator 1 development at the concrete curve of [bernstein2013a], Section 4: Curve1174, the complete Edwards curve

$$ x^2 + y^2 = 1 - 1174 x^2 y^2 $$

over the prime field $\mathbb{F}_q$ with $q = 2^{251} - 9$.

Following the paper, the curve is not given by its coefficient but produced by the Elligator 1 construction from the parameter

$$ s = 1806494121122717992522804053500797229648438766985538871240722010849934886421, $$

and the resulting coefficient d s is shown to be exactly -1174.

All numerical statements are checked by kernel computation. Field elements of F1174 are Fin residues, so decide evaluates ring operations directly; the two places where an exponent is astronomically large (the primality certificate and the quadratic character) go through the binary modular exponentiation of Elligator.PrimalityCertificate.

Main results

• q1174_prime, card_F1174, q1174_mod_four: F1174 is a field with q = 2^251 - 9 elements and q ≡ 3 (mod 4), so it satisfies the standing hypotheses of Elligator 1.
• s1174_ne_zero, s1174_sq_ne_pm_two: the parameter s satisfies the hypotheses of Theorem 1.
• c1174_eq, r1174_eq: the values of the derived parameters c = 2/s^2 and r = c + 1/c.
• d1174_eq: d = -(c + 1)^2/(c - 1)^2 = -1174, i.e. the Elligator 1 curve for (q, s) is Curve1174.
• chi_d1174_eq_neg_one, d1174_not_isSquare: -1174 is a non-square in F1174, which is the completeness criterion quoted in Section 4.1.
• decode1174_mem_affinePoints, decode1174_equation: Theorem 1 and Definition 2 for Curve1174.
• decode1174_neg, decode1174_preimages: Theorem 3 for Curve1174.
• b1174, S1174_card, encode1174_injective, encode1174_bijective: Theorem 4 for Curve1174.
• basePointV_montgomery, basePoint1174_mem_affinePoints: the point (U, V) = (4, V) of Section 4.1 lies on the Montgomery model, and the corresponding point (4/V, 3/5) lies on Curve1174.

References

See [bernstein2013a], Section 4.

The base field

def Elligator.Elligator1.Curve1174.q1174 : ℕ

The characteristic of the Curve1174 base field, q = 2 ^ 251 - 9.

Equations

• Elligator.Elligator1.Curve1174.q1174 = 3618502788666131106986593281521497120414687020801267626233049500247285301239

theorem Elligator.Elligator1.Curve1174.q1174_eq_two_pow : q1174 = 2 ^ 251 - 9

The numeral defining q1174 is 2 ^ 251 - 9.

theorem Elligator.Elligator1.Curve1174.prime_q1174 : Nat.Prime q1174

instance Elligator.Elligator1.Curve1174.instFactPrimeQ1174 : Fact (Nat.Prime q1174)

instance Elligator.Elligator1.Curve1174.instNeZeroNatQ1174 : NeZero q1174

@[reducible, inline]

abbrev Elligator.Elligator1.Curve1174.F1174 : Type

The Curve1174 base field F_q with q = 2 ^ 251 - 9.

Equations

• Elligator.Elligator1.Curve1174.F1174 = ZMod Elligator.Elligator1.Curve1174.q1174

theorem Elligator.Elligator1.Curve1174.card_F1174 : Fintype.card F1174 = q1174

F1174 has q1174 elements.

theorem Elligator.Elligator1.Curve1174.q1174_mod_four : q1174 % 4 = 3

q ≡ 3 (mod 4), one of the standing hypotheses of Elligator 1.

theorem Elligator.Elligator1.Curve1174.q1174_isPrimePow : IsPrimePow q1174

q1174 is a prime power, as required by the Elligator 1 development.

The Elligator 1 parameter s and the derived parameters c, r, d

def Elligator.Elligator1.Curve1174.s1174 : F1174

The Elligator 1 parameter s chosen for Curve1174 in [bernstein2013a], Section 4.1.

Equations

• Elligator.Elligator1.Curve1174.s1174 = 1806494121122717992522804053500797229648438766985538871240722010849934886421

theorem Elligator.Elligator1.Curve1174.s1174_ne_zero : s1174 ≠ 0

The parameter s is nonzero.

theorem Elligator.Elligator1.Curve1174.s1174_sq_ne_pm_two : (s1174 ^ 2 - 2) * (s1174 ^ 2 + 2) ≠ 0

The parameter s satisfies (s^2 - 2)(s^2 + 2) ≠ 0.

theorem Elligator.Elligator1.Curve1174.c1174_eq : c s1174 = 2179648967284864129978754827181620133949030013113193603783078030367640144353

The value of the curve parameter c = 2/s^2 for Curve1174.

theorem Elligator.Elligator1.Curve1174.r1174_eq : r s1174 = 169665518650159600071835149602457239235130252467237612483220564802728637315

The value of the curve parameter r = c + 1/c for Curve1174.

theorem Elligator.Elligator1.Curve1174.d1174_eq : d s1174 = -1174

The Edwards coefficient produced by Elligator 1 from (q, s) is -1174: the curve of Theorem 1 and Definition 2 for this choice of parameters is exactly Curve1174.

theorem Elligator.Elligator1.Curve1174.chi_d1174_eq_neg_one : LegendreSymbol.χ (d s1174) = -1

The quadratic character of the Edwards coefficient is -1.

theorem Elligator.Elligator1.Curve1174.d1174_not_isSquare : ¬IsSquare (d s1174)

-1174 is not a square in F1174; by [bernstein2013a], Section 4.1 this is what makes Curve1174 a complete Edwards curve.

The curve

def Elligator.Elligator1.Curve1174.curve1174 : TwistedEdwardsCurve F1174

Curve1174 as the Edwards curve produced by Elligator 1 from the parameter s.

Equations

• Elligator.Elligator1.Curve1174.curve1174 = Elligator.Elligator1.curve Elligator.Elligator1.Curve1174.s1174

theorem Elligator.Elligator1.Curve1174.curve1174_eq : curve1174 = edwardsCurve (-1174)

Curve1174 is the Edwards curve with coefficient -1174.

theorem Elligator.Elligator1.Curve1174.curve1174_equation (x y : F1174) : curve1174.Equation x y ↔ x ^ 2 + y ^ 2 = 1 - 1174 * x ^ 2 * y ^ 2

The defining equation of Curve1174: x^2 + y^2 = 1 - 1174 x^2 y^2.

theorem Elligator.Elligator1.Curve1174.curve1174_isValid : curve1174.IsValid

Curve1174 is a valid (nonsingular) Edwards model.

The Elligator 1 maps for Curve1174

def Elligator.Elligator1.Curve1174.decode1174 (t : F1174) : F1174 × F1174

The Elligator 1 decoding function φ : F_q → E(F_q) of Definition 2, for Curve1174.

Equations

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

theorem Elligator.Elligator1.Curve1174.decode1174_mem_affinePoints (t : F1174) : decode1174 t ∈ curve1174.affinePoints

Theorem 1 for Curve1174: every decoded value is a point of the curve.

theorem Elligator.Elligator1.Curve1174.decode1174_equation (t : F1174) : have x := (decode1174 t).1; have y := (decode1174 t).2; x ^ 2 + y ^ 2 = 1 - 1174 * x ^ 2 * y ^ 2

Theorem 1 for Curve1174, in coordinates.

theorem Elligator.Elligator1.Curve1174.decode1174_neg (t : F1174) : decode1174 (-t) = decode1174 t

Theorem 3 for Curve1174: φ identifies t and -t.

theorem Elligator.Elligator1.Curve1174.decode1174_preimages (t : F1174) : ¬∃ (p : { n : F1174 // n ≠ t ∧ n ≠ -t }), decode1174 ↑p = decode1174 t

Theorem 3 for Curve1174: t and -t are the only preimages of φ t.

The string encoding for Curve1174

theorem Elligator.Elligator1.Curve1174.b1174 : b q1174 = 250

Curve1174 encodes field elements as strings of b = ⌊log₂ q⌋ = 250 bits.

theorem Elligator.Elligator1.Curve1174.S1174_card : S.card = (q1174 + 1) / 2

Theorem 4 for Curve1174: there are (q + 1)/2 admissible bit strings.

theorem Elligator.Elligator1.Curve1174.encode1174_injective : Function.Injective fun (τ : ↥S) => ι τ s1174_ne_zero s1174_sq_ne_pm_two card_F1174 q1174_mod_four

Theorem 4 for Curve1174: the string encoding ι : S → E(F_q) is injective.

theorem Elligator.Elligator1.Curve1174.encode1174_bijective : Function.Bijective (ιToϕOverF s1174_ne_zero s1174_sq_ne_pm_two card_F1174 q1174_mod_four)

Theorem 4 for Curve1174: the string encoding is a bijection from S onto φ(F_q).

The base point

def Elligator.Elligator1.Curve1174.basePointV : F1174

The V-coordinate of the base point of Section 4.1 on the Montgomery model (4/1175) V^2 = U^3 + (4/1175 - 2) U^2 + U, at U = 4.

Equations

• Elligator.Elligator1.Curve1174.basePointV = 19225777642111670230408712442205514783403012708409058383774613284963344096

def Elligator.Elligator1.Curve1174.basePoint1174 : F1174 × F1174

The base point (x, y) = (4/V, 3/5) of Curve1174 given in [bernstein2013a], Section 4.1.

Equations

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

theorem Elligator.Elligator1.Curve1174.basePointV_montgomery : 4 / 1175 * basePointV ^ 2 = 4 ^ 3 + (4 / 1175 - 2) * 4 ^ 2 + 4

The point (U, V) = (4, V) of [bernstein2013a], Section 4.1 lies on the Montgomery model (4/1175) V^2 = U^3 + (4/1175 - 2) U^2 + U to which Curve1174 is birationally equivalent.

theorem Elligator.Elligator1.Curve1174.basePoint1174_fst : basePoint1174.1 * basePointV = 4

The first coordinate of the base point is 4/V.

theorem Elligator.Elligator1.Curve1174.basePoint1174_snd : basePoint1174.2 * 5 = 3

The second coordinate of the base point is 3/5.

theorem Elligator.Elligator1.Curve1174.basePoint1174_mem_affinePoints : basePoint1174 ∈ curve1174.affinePoints

The base point of Section 4.1 lies on Curve1174.