From b9bef9215334ad124ea2bad9dee630404814651b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Mon, 17 Aug 2026 07:20:36 +0000 Subject: [PATCH 1/8] adds new Crypto/Primitives/ECC directory with basic twisted Edwards curve notions --- Cslib.lean | 2 + Cslib/Crypto/Primitives/ECC/Basic.lean | 9 ++ .../Primitives/ECC/TwistedEdwardsCurve.lean | 102 ++++++++++++++++++ 3 files changed, 113 insertions(+) create mode 100644 Cslib/Crypto/Primitives/ECC/Basic.lean create mode 100644 Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean diff --git a/Cslib.lean b/Cslib.lean index f21b49009..4aaff12d7 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -54,6 +54,8 @@ public import Cslib.Computability.URM.Defs public import Cslib.Computability.URM.Execution public import Cslib.Computability.URM.StandardForm public import Cslib.Computability.URM.StraightLine +public import Cslib.Crypto.Primitives.ECC.Basic +public import Cslib.Crypto.Primitives.ECC.TwistedEdwardsCurve public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption diff --git a/Cslib/Crypto/Primitives/ECC/Basic.lean b/Cslib/Crypto/Primitives/ECC/Basic.lean new file mode 100644 index 000000000..730199853 --- /dev/null +++ b/Cslib/Crypto/Primitives/ECC/Basic.lean @@ -0,0 +1,9 @@ +/- +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 diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean new file mode 100644 index 000000000..28e884984 --- /dev/null +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -0,0 +1,102 @@ +/- +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.Primitives.ECC.Basic +public import Mathlib.Algebra.Ring.Commute +public import Mathlib.Data.Set.Defs + +/-! +# Twisted Edwards curves + +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.Primitives.ECC + +/-- 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.Primitives.ECC From cd56149a6112cd85c8230dbf8c2e29d8377eae53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Mon, 17 Aug 2026 07:29:26 +0000 Subject: [PATCH 2/8] adds def of edwardsCurve to TwistedEdwardsCurve.lean --- Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index 28e884984..c43df168c 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -98,5 +98,10 @@ theorem ofD_isValid_iff [Nontrivial R] (d : R) : (ofD d).IsValid ↔ d ≠ 0 ∧ · rintro ⟨hd, hd1⟩ exact ⟨one_ne_zero, hd, fun h ↦ hd1 h.symm⟩ +/-- The general Edwards curve with coefficient `d`. +This is an alias for the `a = 1` specialization of a twisted Edwards curve. -/ +def edwardsCurve (d : R) : TwistedEdwardsCurve R := TwistedEdwardsCurve.ofD d + end TwistedEdwardsCurve + end Cslib.Crypto.Primitives.ECC From fb3cc3534632e19559f75928a36fe8568d0d09cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Mon, 17 Aug 2026 11:18:39 +0000 Subject: [PATCH 3/8] adds generic EdwardsCurve notions derived from TwistedEdwardsCurve --- Cslib.lean | 1 + Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean | 78 +++++++++++++++++++ .../Primitives/ECC/TwistedEdwardsCurve.lean | 8 +- 3 files changed, 81 insertions(+), 6 deletions(-) create mode 100644 Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean diff --git a/Cslib.lean b/Cslib.lean index 4aaff12d7..1e16cb2be 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -55,6 +55,7 @@ public import Cslib.Computability.URM.Execution public import Cslib.Computability.URM.StandardForm public import Cslib.Computability.URM.StraightLine public import Cslib.Crypto.Primitives.ECC.Basic +public import Cslib.Crypto.Primitives.ECC.EdwardsCurve public import Cslib.Crypto.Primitives.ECC.TwistedEdwardsCurve public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs diff --git a/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean new file mode 100644 index 000000000..8bee2829e --- /dev/null +++ b/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean @@ -0,0 +1,78 @@ +/- +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.Primitives.ECC.TwistedEdwardsCurve + +/-! +# Complete Edwards curves + +This file develops the (untwisted) Edwards curve +`x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2` +as the `a = 1` specialization of `Elligator.TwistedEdwardsCurve`. + +Everything here is stated over an arbitrary commutative ring and for an arbitrary coefficient `d`. +No finite field, and no cardinality assumption. + +## Main definitions + +* `edwardsCurve d`: the Edwards curve with coefficient `d`. +* `edwardsCurveEquation x y d`: the Edwards curve equation for a coefficient `d ∉ {0, 1}`, packaged + as a subtype argument. + +## Main results + +* `edwardsCurve_equation_iff`, `edwardsCurveEquation_iff`: unfolding lemmas for the equation. +* `edwardsCurve_isValid_iff`: `edwardsCurve d` is a valid model iff `d ≠ 0` and `d ≠ 1`. +* `edwardsCurveEquation_zero_one`: the neutral point `(0, 1)` lies on every Edwards curve. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Primitives.ECC + +variable {R : Type*} [CommRing R] + +/-- The Edwards curve with coefficient `d`. +This is an alias for the `a = 1` specialization of a twisted Edwards curve. -/ +def edwardsCurve (d : R) : TwistedEdwardsCurve R := TwistedEdwardsCurve.ofD d + +@[simp] +theorem edwardsCurve_equation_iff (d x y : R) : + (edwardsCurve d).Equation x y ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by + simp [edwardsCurve] + +@[simp] +theorem edwardsCurve_isValid_iff [Nontrivial R] (d : R) : + (edwardsCurve d).IsValid ↔ d ≠ 0 ∧ d ≠ 1 := by + simp [edwardsCurve] + +/-- `edwardsCurveEquation` is the standard Edwards curve equation, with the coefficient carried as +a subtype element recording `d ≠ 0` and `d ≠ 1`. New generic developments should normally use +`(edwardsCurve d).Equation x y` and carry coefficient validity separately via +`TwistedEdwardsCurve.IsValid`; see `edwardsCurve_isValid_iff`. +-/ +def edwardsCurveEquation (x y : R) (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : Prop := + (edwardsCurve d.val).Equation x y + +@[simp] +theorem edwardsCurveEquation_iff (x y : R) (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : + edwardsCurveEquation x y d ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by + simp [edwardsCurveEquation] + +/-- The set of affine points of the Edwards curve with coefficient `d`. -/ +theorem edwardsCurve_affinePoints (d : R) : + (edwardsCurve d).affinePoints = + {p : R × R | p.1 ^ 2 + p.2 ^ 2 = 1 + d * p.1 ^ 2 * p.2 ^ 2} := by + ext p + simp [TwistedEdwardsCurve.affinePoints] + +lemma edwardsCurveEquation_zero_one (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : + edwardsCurveEquation (0 : R) (1 : R) d := by + simp + +end Cslib.Crypto.Primitives.ECC diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index c43df168c..7c7a8e7db 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -13,6 +13,7 @@ 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`. @@ -22,7 +23,7 @@ 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 +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. -/ @@ -98,10 +99,5 @@ theorem ofD_isValid_iff [Nontrivial R] (d : R) : (ofD d).IsValid ↔ d ≠ 0 ∧ · rintro ⟨hd, hd1⟩ exact ⟨one_ne_zero, hd, fun h ↦ hd1 h.symm⟩ -/-- The general Edwards curve with coefficient `d`. -This is an alias for the `a = 1` specialization of a twisted Edwards curve. -/ -def edwardsCurve (d : R) : TwistedEdwardsCurve R := TwistedEdwardsCurve.ofD d - end TwistedEdwardsCurve - end Cslib.Crypto.Primitives.ECC From 2b9de9bdbc609c1f96c998c13071d17602087792 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Mon, 17 Aug 2026 11:48:32 +0000 Subject: [PATCH 4/8] adds concrete references to ECC notions --- Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean | 4 +++ .../Primitives/ECC/TwistedEdwardsCurve.lean | 4 +++ references.bib | 31 +++++++++++++++++++ 3 files changed, 39 insertions(+) diff --git a/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean index 8bee2829e..609f6f0b3 100644 --- a/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean @@ -29,6 +29,10 @@ No finite field, and no cardinality assumption. * `edwardsCurve_equation_iff`, `edwardsCurveEquation_iff`: unfolding lemmas for the equation. * `edwardsCurve_isValid_iff`: `edwardsCurve d` is a valid model iff `d ≠ 0` and `d ≠ 1`. * `edwardsCurveEquation_zero_one`: the neutral point `(0, 1)` lies on every Edwards curve. + +## References + +See [Bernstein2007a], Section 2. -/ @[expose] public section diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index 7c7a8e7db..e48dc82ba 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -26,6 +26,10 @@ is not itself a Weierstrass equation, so using `WeierstrassCurve.Affine.Equation 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. + +## References + +See [Bernstein2008a], Section 2, Definition 2.1 . -/ @[expose] public section diff --git a/references.bib b/references.bib index d2a7dfb13..3d31f9dda 100644 --- a/references.bib +++ b/references.bib @@ -551,3 +551,34 @@ @book{Papadimitriou94 publisher={Addison-Wesley}, address={Reading, Massachusetts} } + +@inproceedings{Bernstein2008a, + author={Daniel J. Bernstein and Peter Birkner and Marc Joye and Tanja Lange and Christiane Peters}, + title={Twisted Edwards Curves}, + booktitle={Progress in Cryptology - {AFRICACRYPT} 2008, First International Conference + on Progress in Cryptology, Casablanca, Morocco, June 11-14, 2008. + Proceedings}, + series={Lecture Notes in Computer Science}, + volume={5023}, + isbn="978-35-40-68159-5", + pages= {389--405}, + publisher={Springer Verlag, Berlin}, + year={2008}, + doi={10.1007/978-3-540-68164-9\_26} +} + +@inproceedings{Bernstein2007a, + author={Bernstein, Daniel J. and Lange, Tanja}, + title={Faster addition and doubling on elliptic curves}, + year={2007}, + isbn={3540768998}, + publisher={Springer-Verlag}, + address={Berlin, Heidelberg}, + abstract={Edwards recently introduced a new normal form for elliptic curves. Every elliptic curve over a non-binary field is birationally equivalent to a curve in Edwards form over an extension of the field, and in many cases over the original field.This paper presents fast explicit formulas (and register allocations) for group operations on an Edwards curve. The algorithm for doubling uses only 3M + 4S, i.e., 3 field multiplications and 4 field squarings. If curve parameters are chosen to be small then the algorithm for mixed addition uses only 9M + 1S and the algorithm for non-mixed addition uses only 10M + 1S. Arbitrary Edwards curves can be handled at the cost of just one extra multiplication by a curve parameter.For comparison, the fastest algorithms known for the popular "a4=-3 Jacobian" form use 3M + 5S for doubling; use 7M + 4S for mixed addition; use 11M + 5S for non-mixed addition; and use 10M + 4S for non-mixed addition when one input has been added before.The explicit formulas for non-mixed addition on an Edwards curve can be used for doublings at no extra cost, simplifying protection against side-channel attacks. Even better, many elliptic curves (approximately 1/4 of all isomorphism classes of elliptic curves over a non-binary finite field) are birationally equivalent--over the original field--to Edwards curves where this addition algorithm works for all pairs of curve points, including inverses, the neutral element, etc.This paper contains an extensive comparison of different forms of elliptic curves and different coordinate systems for the basic group operations (doubling, mixed addition, non-mixed addition, and unified addition) as well as higher-level operations such as multi-scalar multiplication.}, + booktitle={Proceedings of the Advances in Crypotology 13th International Conference on Theory and Application of Cryptology and Information Security}, + pages={29–50}, + numpages={22}, + keywords={unified addition formulas, sidechannel countermeasures, scalar multiplication, register allocation, performance evaluation, multi-scalar multiplication, explicit formulas, elliptic curves, efficient implementation, doubling, complete addition formulas, addition}, + location={Kuching, Malaysia}, + series={ASIACRYPT'07} +} From 59ce03d2d8f27b561f28759e993e5cb574695363 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Wed, 19 Aug 2026 09:18:21 +0000 Subject: [PATCH 5/8] removes EdwardsCurve.lean while moving useful defs and dropping ofD --- Cslib.lean | 1 - Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean | 82 ------------------- .../Primitives/ECC/TwistedEdwardsCurve.lean | 24 +++--- 3 files changed, 13 insertions(+), 94 deletions(-) delete mode 100644 Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean diff --git a/Cslib.lean b/Cslib.lean index 1e16cb2be..4aaff12d7 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -55,7 +55,6 @@ public import Cslib.Computability.URM.Execution public import Cslib.Computability.URM.StandardForm public import Cslib.Computability.URM.StraightLine public import Cslib.Crypto.Primitives.ECC.Basic -public import Cslib.Crypto.Primitives.ECC.EdwardsCurve public import Cslib.Crypto.Primitives.ECC.TwistedEdwardsCurve public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs diff --git a/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean deleted file mode 100644 index 609f6f0b3..000000000 --- a/Cslib/Crypto/Primitives/ECC/EdwardsCurve.lean +++ /dev/null @@ -1,82 +0,0 @@ -/- -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.Primitives.ECC.TwistedEdwardsCurve - -/-! -# Complete Edwards curves - -This file develops the (untwisted) Edwards curve -`x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2` -as the `a = 1` specialization of `Elligator.TwistedEdwardsCurve`. - -Everything here is stated over an arbitrary commutative ring and for an arbitrary coefficient `d`. -No finite field, and no cardinality assumption. - -## Main definitions - -* `edwardsCurve d`: the Edwards curve with coefficient `d`. -* `edwardsCurveEquation x y d`: the Edwards curve equation for a coefficient `d ∉ {0, 1}`, packaged - as a subtype argument. - -## Main results - -* `edwardsCurve_equation_iff`, `edwardsCurveEquation_iff`: unfolding lemmas for the equation. -* `edwardsCurve_isValid_iff`: `edwardsCurve d` is a valid model iff `d ≠ 0` and `d ≠ 1`. -* `edwardsCurveEquation_zero_one`: the neutral point `(0, 1)` lies on every Edwards curve. - -## References - -See [Bernstein2007a], Section 2. --/ - -@[expose] public section - -namespace Cslib.Crypto.Primitives.ECC - -variable {R : Type*} [CommRing R] - -/-- The Edwards curve with coefficient `d`. -This is an alias for the `a = 1` specialization of a twisted Edwards curve. -/ -def edwardsCurve (d : R) : TwistedEdwardsCurve R := TwistedEdwardsCurve.ofD d - -@[simp] -theorem edwardsCurve_equation_iff (d x y : R) : - (edwardsCurve d).Equation x y ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by - simp [edwardsCurve] - -@[simp] -theorem edwardsCurve_isValid_iff [Nontrivial R] (d : R) : - (edwardsCurve d).IsValid ↔ d ≠ 0 ∧ d ≠ 1 := by - simp [edwardsCurve] - -/-- `edwardsCurveEquation` is the standard Edwards curve equation, with the coefficient carried as -a subtype element recording `d ≠ 0` and `d ≠ 1`. New generic developments should normally use -`(edwardsCurve d).Equation x y` and carry coefficient validity separately via -`TwistedEdwardsCurve.IsValid`; see `edwardsCurve_isValid_iff`. --/ -def edwardsCurveEquation (x y : R) (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : Prop := - (edwardsCurve d.val).Equation x y - -@[simp] -theorem edwardsCurveEquation_iff (x y : R) (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : - edwardsCurveEquation x y d ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by - simp [edwardsCurveEquation] - -/-- The set of affine points of the Edwards curve with coefficient `d`. -/ -theorem edwardsCurve_affinePoints (d : R) : - (edwardsCurve d).affinePoints = - {p : R × R | p.1 ^ 2 + p.2 ^ 2 = 1 + d * p.1 ^ 2 * p.2 ^ 2} := by - ext p - simp [TwistedEdwardsCurve.affinePoints] - -lemma edwardsCurveEquation_zero_one (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : - edwardsCurveEquation (0 : R) (1 : R) d := by - simp - -end Cslib.Crypto.Primitives.ECC diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index e48dc82ba..a6e231422 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -44,10 +44,10 @@ structure TwistedEdwardsCurve (R : Type*) where /-- right hand side coefficient -/ d : R -namespace TwistedEdwardsCurve - variable {R : Type*} [CommRing R] +namespace TwistedEdwardsCurve + /-- 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 @@ -85,23 +85,25 @@ be used over more general rings and also permits partially specified curves duri -/ 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 +end TwistedEdwardsCurve + +/-- The (untwisted) Edwards curve with coefficient `d`, obtained by setting `a = 1`. -/ +def edwardsCurve (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] +/-- The equation of `edwardsCurve d`, written out. -/ +theorem edwardsCurve_equation_iff (d x y : R) : + (edwardsCurve d).Equation x y ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by + simp [TwistedEdwardsCurve.Equation, edwardsCurve] -@[simp] -theorem ofD_isValid_iff [Nontrivial R] (d : R) : (ofD d).IsValid ↔ d ≠ 0 ∧ d ≠ 1 := by +/-- `edwardsCurve d` is a valid (nonsingular) model exactly when `d ≠ 0` and `d ≠ 1`. -/ +theorem edwardsCurve_isValid_iff [Nontrivial R] (d : R) : + (edwardsCurve 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.Primitives.ECC From 11c33ca169f36cd24ab0d03b9bb1f4404c9732bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Wed, 19 Aug 2026 09:20:38 +0000 Subject: [PATCH 6/8] removes simp annotation from lemmas --- Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index a6e231422..4ddef9163 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -61,7 +61,6 @@ 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 @@ -72,7 +71,6 @@ def zeroPoint (E : TwistedEdwardsCurve R) : E.Point := ⟨zero, E.zero_mem_affin /-- 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 ↔ From e5562c208346cd94bfac8a58d7272fab387c28d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Wed, 19 Aug 2026 09:22:44 +0000 Subject: [PATCH 7/8] updates comments to mention ultimate mathlib destination, references and general results --- .../Primitives/ECC/TwistedEdwardsCurve.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index 4ddef9163..1f576fbb6 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -27,9 +27,22 @@ a birational coordinate conversion and extra invertibility hypotheses. The API same useful separation as that API: coefficients, an affine equation, a set of affine points, and a bundled point type. +## Main definitions + +* `TwistedEdwardsCurve`: the coefficients `a`, `d` of a twisted Edwards model, with its equation + `TwistedEdwardsCurve.Equation`, its affine points `TwistedEdwardsCurve.affinePoints` and the + nonsingularity condition `TwistedEdwardsCurve.IsValid`. +* `edwardsCurve d`: the untwisted Edwards curve `x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2`. + +## TODO + +- Move into mathlib next to Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass + ## References -See [Bernstein2008a], Section 2, Definition 2.1 . +* [Bernstein2007a], Section 2. +* [Bernstein2008a], Section 2, Definition 2.1. + -/ @[expose] public section From d5215c6bcddc3e20cb888df7b5a0af07b36f2954 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Chris=20Anto=20Fr=C3=B6schl?= Date: Wed, 19 Aug 2026 09:23:50 +0000 Subject: [PATCH 8/8] relabels most of the results to lemmas instead of theorems --- Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean index 1f576fbb6..2f5f5dd7c 100644 --- a/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean +++ b/Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean @@ -74,7 +74,7 @@ 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) -theorem zero_mem_affinePoints (E : TwistedEdwardsCurve R) : zero ∈ E.affinePoints := by +lemma 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 @@ -84,7 +84,7 @@ def zeroPoint (E : TwistedEdwardsCurve R) : E.Point := ⟨zero, E.zero_mem_affin /-- Negation of affine coordinates on a twisted Edwards curve. -/ def neg (p : R × R) : R × R := (-p.1, p.2) -theorem neg_mem_affinePoints (E : TwistedEdwardsCurve R) (p : R × R) : +lemma 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 @@ -104,12 +104,12 @@ def edwardsCurve (d : R) : TwistedEdwardsCurve R where d := d /-- The equation of `edwardsCurve d`, written out. -/ -theorem edwardsCurve_equation_iff (d x y : R) : +lemma edwardsCurve_equation_iff (d x y : R) : (edwardsCurve d).Equation x y ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by simp [TwistedEdwardsCurve.Equation, edwardsCurve] /-- `edwardsCurve d` is a valid (nonsingular) model exactly when `d ≠ 0` and `d ≠ 1`. -/ -theorem edwardsCurve_isValid_iff [Nontrivial R] (d : R) : +lemma edwardsCurve_isValid_iff [Nontrivial R] (d : R) : (edwardsCurve d).IsValid ↔ d ≠ 0 ∧ d ≠ 1 := by constructor · rintro ⟨_, hd, had⟩