feat(Crypto/Primitives/ECC): Edwards Curves - #809
Conversation
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
I like this a lot better! I think we can still remove some of it for now. Lets rename the file to EllipticCurves, the placement is fine for now.
| `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 |
There was a problem hiding this comment.
Given that we deprecate this in this comment and we're making this PR for the first time, lets just make these changes as we go instead and remove this definition altogether.
|
|
||
| /-- 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 |
There was a problem hiding this comment.
Lets delete this and let consumers write TwistedEdwardsCurve.ofD or keep Edwards Curve as the name there and drop ofD. Either way, this file looks more or less unnecessary.
|
|
||
| lemma edwardsCurveEquation_zero_one (d : {d : R // d ≠ 0 ∧ d ≠ 1}) : | ||
| edwardsCurveEquation (0 : R) (1 : R) d := by | ||
| simp |
There was a problem hiding this comment.
Yeah, overall this whole file looks like a duplicate to me. If this is the interface you want, give it to yourself from the TwistedEdwardsCurve file.
There was a problem hiding this comment.
Fixed in 59ce03d. I decided to drop the ofD interface and go with the ones that are actually a bit more elegant in usage of my Elligator infrastructure.
Regarding the file rename: are you sure something like EllipticCurves.lean is correct? I would have rather renamed this to EdwardsCurve.lean (since we do not only talk about twisted ones now there) and be open for other curve families getting their own file if needed. Although this discussion is perhaps rather irrelevant if this is ultimately destined to land in mathlib anyway.
| 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] |
There was a problem hiding this comment.
This is probably the best @[simp] lemma here, but my preference is to remove the @[simp] lemmata and add them back when they have users and where it is obvious how they justify themselves.
|
I wonder if we should do a general treatment of elliptic curves before doing Edwards specifically, that way we can come prepared with a set of abstractions. |
I agree that this is worth thinking about before continuing. In fact, I'm not even sure that a general treatment of elliptic curves belongs in CSLib at all, given that mathlib already provides abstract families such as This makes me wonder whether CSLib should instead focus on concrete curve constructions, such as Ed25519 and Curve1174, while relying on mathlib for the more general theory. What do you think? I'm also not entirely sure why such common theory was not established thus far. The downside of going this route for the Elligator development is that it would make the subsequent PRs depend on the corresponding mathlib work being merged in a timely manner (even assuming that the current version is abstract enough to be acceptable). That could potentially slow down the Elligator PR chain, even if it is the cleaner long-term separation of responsibilities. I would advocate doing the correct separation of concerns. |
|
In the past, we've erred towards merging things into CSLib with clear TODOs to PR into Mathlib. I agree that we shouldn't abstract over elliptic curves here. |
I've added a comment in e5562c2 . I intend to start such mathlib PR as soon as we are advanced enough in this PR chain to be sure, that the general notions of Edwards curves are fixed. |
2 participants
Formalizes some basic notions for (twisted) Edwards curves. As part of this, I propose introducing a new
Crypto/Primitives/ECCsubfolder.Contents
This PR adds two files:
Crypto/Primitives/ECC/TwistedEdwardsCurve.lean: the coefficientsa,dof a twisted Edwards curve, its defining equation, affine point set, bundled points, neutral point and negation, plus a validity (nonsingularity) predicate.Crypto/Primitives/ECC/EdwardsCurve.lean: the untwisted Edwards curve as thea = 1specialization, with unfolding lemmas, the criteriond ≠ 0 ∧ d ≠ 1for a valid model, and the fact that(0, 1)lies on every such curve.Everything is stated over an arbitrary commutative ring: no finite field, no cardinality assumption, and no dependence on any parameter of a particular cryptosystem.
Context
This PR is primarily preparatory work for #783 and subsequent PRs introducing the Elligator cryptosystem.
I am by no means a cryptographer by profession, so the definitions introduced here may not represent the most general or canonical formulation found in the literature. My immediate goal is simply to establish the standard notions needed for the twisted Edwards curve equation used by Elligator 1.
I would therefore welcome improvements to the terminology and generality from someone with more expertise in elliptic-curve cryptography. For now, however, this provides a small set of ECC primitives that can be built upon by the subsequent Elligator work.
Follow-ups
Future PRs will build on these primitives with concrete curve constructions under
Crypto/Primitives/ECC/Curves, such asCurve1174andCurve25519. The intended shape is that a curve is described purely in terms of these primitives (its base field, its Edwards coefficient, the non-squareness of that coefficient, and its base point) and that any cryptosystem-specific parameter build-up lives separately and merely proves it lands on that curve. A preview of this usage can be found here.I'm happy to provide further context if usage of some lemmas/defs is non-obvious by this current stage.