feat(Crypto/Systems): Elligator 1, Theorem 1 and Definition 2

[chris-anto-froeschl]

Formalizes results from Elligator: Elliptic-curve points indistinguishable from uniform random strings (Bernstein, Hamburg, Krasnova, Lange). Elligator is a way to encode points on certain elliptic curves as strings indistinguishable from uniform random data, used to make elliptic-curve-based protocols resistant to traffic analysis/censorship.

This PR is the foundational layer of a larger, ongoing effort. Beyond finishing Elligator 1 (Theorems 3 and 4, and a Curve1174 instantiation - see below), I intend to formalize the other members of the Elligator family over time, aiming for CSLib to eventually have a complete treatment of the Elligator line of constructions rather than just this one variant. The relevant papers are collected here. Flagging this now so the scope and naming decisions in this PR (e.g. Elligator1 as a namespace, not just Elligator) read as intended groundwork rather than arbitrary.

This PR contains only the foundational layer: Theorem 1 (the map from a field element to a curve point) and Definition 2 (the total map ϕ, extending Theorem 1 to all of F), kept "small" deliberately for review. The full Elligator 1 development - Theorem 3 (inversion), Theorem 4 (the bit-string encoding that gives Elligator its name), and an instantiation at Curve1174 (the paper's Section 4 curve, q = 2^251 - 9) - is complete in my working repository at chris-anto-froeschl/elligator and will follow as separate PRs once this base layer stabilizes. For orientation:

• README, including a translation table from the paper's numbering to the Lean declarations
• Blueprint, for the full dependency graph and statements

Scope of this PR

Main results:

• c, r, d: the curve parameters derived from s
• u, v, X, Y, x, y: the auxiliary and output coordinates, each with its own well-definedness/nonvanishing file
• χ: the quadratic character used throughout, built directly on Mathlib's quadraticChar (LegendreSymbol.lean)
• TwistedEdwardsCurve: a small, purpose-built structure for the complete Edwards curve equation and its affine points
• map_fulfills_curve_equation, variable_mul_ne_zero: Theorem 1's two conclusions
• ϕ: Definition 2's total map, packaged with a proof it lands on the curve (Map.lean)
• DecodingFunction: a thin wrapper exposing ϕ's result unwrapped from its subtype, for presentation

Generalization beyond the paper

The paper's standing hypothesis is q prime; several results here (including ϕ itself) hold for q a prime power congruent to 3 mod 4, so I've stated them with IsPrimePow q rather than Prime q throughout, and used Prime q only where the argument genuinely needs it (injectivity results relying on unique factorization of naturals below q).

Futhermore, all definitions are computable. ([DecidableEq F] is threaded explicitly rather than relying on Classical.choice). Whether this is fast at cryptographic field sizes is a separate question - see below.

Known lint-style failure: filenames

lake exe lint-style flags every file named after a lowercase paper variable (cProperties.lean, dProperties.lean, rProperties.lean, sProperties.lean, uProperties.lean, vProperties.lean, xProperties.lean, yProperties.lean) as not being UpperCamelCase. I've deliberately kept these as-is rather than mechanically renaming, for two reasons:

1. Each file's name mirrors the paper's own single-letter notation for that variable (c, d, r, s, u, v, x, y), which I think aids readability for anyone cross-referencing against the paper or the blueprint.
2. A straightforward rename isn't actually available for two of these without a collision: xProperties.lean → XProperties.lean and yProperties.lean → YProperties.lean would collide with the already-distinct XProperties.lean/YProperties.lean files in this same PR (the auxiliary coordinates X/Y, as opposed to the curve coordinates x/y) - these are only distinguishable by case on a case-sensitive filesystem today.

I'm open to either adding exceptions to scripts/nolints-style.txt, or renaming to content-distinguishing names (e.g. curveXProperties.lean) if that's preferred - happy to go whichever way maintainers want; just didn't want to make that call unilaterally before hearing a preference, and would rather open the PR with a known, explained lint failure than hold it up.

A general property merge distinguishing between parameters, helper variables and curve variables could also work. Although this would results in rather large files. This is all unavoidable due to the linearity of the paper.

χ and Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

χ is defined as quadraticChar F cast from ℤ into F itself (the form the paper uses), and every fact about it here is derived from Mathlib's quadraticChar API rather than reproven from scratch. I considered whether any of the resulting lemmas belong in Mathlib itself rather than here, but I think everything remaining is specific enough to this development (either tied to q ≡ 3 (mod 4), or small enough that a standalone Mathlib PR for it wouldn't be worth the overhead) - genuinely open to being told otherwise if a reviewer sees something worth splitting out.

Performance at cryptographic scale (help wanted)

Curve1174 (q = 2^251 - 9, not part of this PR) is where this becomes relevant: χ and anything built from it have a (q-1)/2- or (q+1)/4-sized exponent, and generic Monoid.npow is O(n) in the exponent rather than O(log n) - naively evaluating χ at that scale is not just slow but algorithmically infeasible. I got as far as building a Pratt/Lucas primality certificate (binary modular exponentiation, kernel-checked) to prove Curve1174's characteristic is actually prime, but I'm not an expert on the broader performance question of making the rest of the pipeline (χ, X, Y, …) execute efficiently at this scale, and would very much welcome input from anyone more experienced with this if/when the Curve1174 follow-up PR comes up.

Edwards curve infrastructure

I couldn't find existing (twisted) Edwards curve infrastructure in Mathlib/CSLib, so I wrote a minimal TwistedEdwardsCurve structure (equation, validity, affine points) sufficient for this development. I'd appreciate guidance on:

1. whether this belongs in this PR's location, or should move to a more general curves location;
2. whether it's worth generalizing now (e.g. beyond the "complete" case this development needs) or better left minimal until a second consumer appears.

File organization

The proof follows a linear dependency chain - each variable (c, r, u, v, X, Y, x, y) is defined in terms of the previous ones, with its well-definedness/nonvanishing lemmas following immediately after. I organized files to mirror this chain (one file per variable's properties) rather than by topic, since the paper's own argument is inherently linear and a topic-based split would just relocate the ordering into implicit cross-file dependencies instead of making it visible. Map.lean itself stays intentionally thin - a presentation layer over the *Properties.lean files, restating each of Theorem 1/Definition 2's actual claims as a short delegation, so a reader can follow the paper's structure without wading through the underlying algebra.

I'm proposing a new Crypto/Systems subfolder for this, since CSLib's cryptography directory doesn't yet have an obvious home for a specific published construction (cryptosystem) like this - open to a different location if one's preferred, and, per above, would ideally be a home the rest of the Elligator family can share as those land too.

AI usage

I used Aristotle at a few points to find tactic proofs for lemmas I was stuck on, mostly in the finite-field/character-theoretic arithmetic. I reviewed and understood every proof it produced before merging, and rewrote several for clarity/idiom afterward; none of the mathematical statements themselves were AI-generated, only some proof scripts.

Context

This project started as my first real Lean project and bachelor's thesis. I've continued refining it over the past several months since to bring it up to a quality I'd consider submission-ready. Happy to iterate on structure, naming, or proof style based on review feedback.

[chris-anto-froeschl]

Just as a follow-up to the file-naming issue:

I came up with two other naming conventions, each with its own pros and cons.

a) Organize files by content

Elligator1/
    ├── CurveParameterProperties.lean
    ├── AuxiliaryCoordinatesProperties.lean
    └── OutputCoordinatesProperties.lean

The main disadvantage here is that it becomes harder to find a specific fact about a specific variable. For example, if I am looking for c_ne_zero, I would have to know that c is a curve parameter and then look for the corresponding section inside CurveParameterProperties.lean.

The other issue is that the files could become very large. Looking ahead to Theorem 3, the property files for individual variables are already around ~1000 LOC, so grouping all properties by content would likely result in some rather unwieldy files. Smaller content splits might be findable though (although perhaps just artificially). Some content related proofs are just rather large at the end of the day.

b) Organize properties hierarchically

To address the issue of increasingly large files, we could instead structure them like this:

Elligator1/
├── Variables.lean
├── Map.lean
├── DecodingFunction.lean
├── EdwardsCurve.lean
└── Properties/
    ├── CurveParameters/
    │   ├── SProperties.lean
    │   ├── CProperties.lean
    │   ├── RProperties.lean
    │   └── DProperties.lean
    ├── AuxiliaryCoordinates/
    │   ├── UProperties.lean
    │   ├── VProperties.lean
    │   ├── XProperties.lean
    │   └── YProperties.lean
    └── OutputCoordinates/
        ├── XProperties.lean
        └── YProperties.lean

This would keep the individual files at a manageable size and provide some context about what kind of properties they contain. It also avoids the casing conflict we would otherwise get with names such as sProperties and SProperties.

However, I still dislike the fact that you have to remember whether the variable mentioned in a filename is actually the lowercase or uppercase version. The current naming scheme avoids this issue entirely, since we do not have to worry about the corresponding linter complaints.

I hope that gives more helpful context.

[fmontesi]

@SamuelSchlesinger Could you have a look? @chris-anto-froeschl is looking for feedback on how to organise and polish/fix this.

[BoltonBailey]

I'm not Sam, but maybe it would be useful to comment that there are a few aspects of the code that aren't consistent with the mathlib style guidelines that CSLib uses. Also, it might be easier to review this if some of the files near the bottom of the dependency tree in this PR were split off into their own PR, like the twisted Edwards curve file.

[BoltonBailey]

Usually in mathlib style, we put the colon at the end of the previous line

[chris-anto-froeschl]

Fixed in 30a853b

[BoltonBailey]

If you have to omit a typeclass variable that is usually considered bad style, it is preferred that you put theorems that don't need an assumption in a section that doesn't have it.

[chris-anto-froeschl]

I hope to minimize this with my upcoming content-based file structuring (see convention a) from above comment) which makes more use of sections. I will notify as soon as this is done.

[BoltonBailey]

hypotheses are usually indented 4 spaces.

[chris-anto-froeschl]

Fixed in 30a853b

[BoltonBailey]

I think this might be the kind of lemma which people sometimes ask "do we need this" i.e. can we just inline it wherever it's applied by writing grind [Nat.odd_iff] or something.

[chris-anto-froeschl]

Indeed, I removed some similar lemmas in FiniteFieldBasic.lean during Fixed in 30a853b . I think the remaining ones are often enough needed to make render them genuinely helpful. Let me know if there are other "do we need this" lemmas left.

[BoltonBailey]

Maybe this is a more substantive criticism: It is odd to see this repeated use of let in the lemma statements throughout this PR. Is there some way we could make a structure which would have these variables as methods so that we could just let those structures be the inputs to the lemma and state the conclusion of the lemma directly in terms of the methods?

[chris-anto-froeschl]

Thanks for the suggestion. I haven't been using structures like this before, but this looks like a nice fit.

I think I see a way to do this with a small structure hierarchy (MapInput with just t, extended by ParamInput adding s, extended by FullInput adding q), so each lemma only takes the level of structure it actually needs. E.g. v_ne_zero (M : ParamInput F) never has to mention q at all, since v doesn't depend on it.

Concretely this could look like the following for the current content (I have to test how good this scales up to the end of the paper, just a quick draft here):

structure MapInput (F : Type*) [Field F] where
  t : {n : F // n ≠ 1 ∧ n ≠ -1}

structure ParamInput (F : Type*) [Field F] extends MapInput F where
  s : F

structure FullInput (F : Type*) [Field F] extends ParamInput F where
  q : ℕ

def MapInput.u (M : MapInput F) : F := Elligator1.u M.t

def ParamInput.v (M : ParamInput F) : F := Elligator1.v M.t M.s
def ParamInput.X (M : ParamInput F) : F := Elligator1.X M.t M.s
def ParamInput.y (M : ParamInput F) : F := Elligator1.y M.t M.s

def FullInput.Y (M : FullInput F) : F := Elligator1.Y M.t M.s M.q
def FullInput.x (M : FullInput F) : F := Elligator1.x M.t M.s M.q

lemma v_ne_zero {q : ℕ} (M : ParamInput F) (hs_ne_zero : M.s ≠ 0)
    (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : M.v ≠ 0 := by
  -- same proof with adjusted sublemmas
  sorry

Before I commit to reworking the whole PR around this: is that roughly the shape you had in mind, or something more specific? It's a fairly large structural change from what's here now, so wanted to check before doing the full pass. I definitely see it would be worthwhile to do this. Especially since the let problems only becomes much worse as we continue.

[BoltonBailey]

Yes this looks great! Perhaps it would even be possible to wrap Fintype.card F = q and/or (hq_mod : q % 4 = 3) into the FullInput structure if those assumptions are uniformly used throughout.

[SamuelSchlesinger]

This is quite a lot and there are some severe style issues, but I want to find a way to get this in. Lets try to do it in much smaller chunks, I think that is going to be a much easier process cause the style remedies in the earlier PRs should transfer to the later ones. I think once we shake all this out we're going to wind up with a lot less code as well.

Lets start out with the Twisted Edwards curves as a first, much more focused, PR.

[chris-anto-froeschl]

This is quite a lot and there are some severe style issues, but I want to find a way to get this in. Lets try to do it in much smaller chunks, I think that is going to be a much easier process cause the style remedies in the earlier PRs should transfer to the later ones. I think once we shake all this out we're going to wind up with a lot less code as well.

Lets start out with the Twisted Edwards curves as a first, much more focused, PR.

I agree. Sorry for the noise. I hope the quality of my upcoming PRs will improve as I become more familiar with the project's conventions and standards.

The requested focused PR is now up as #809. Let me know whether I should close this PR for now, or whether you'd prefer to come back to it at a later stage.