Curve group orders via the Hasse bound, for prime-order curves and for Pallas/Vesta; includes fast SWPoint scalar mul - #2
Merged
Merged
Conversation
daira
changed the title
|
ACK scaffolding for generic curve in the first commit, haven't reviewed the rest. |
|
ACK scope of diff; Hasse bound as an assumed hypothesis, fast scalar mul for SW, and concrete pallas / vesta orders assuming Hasse. |
daira
changed the title
… bound Add CompElliptic/CurveOrder.lean: a curve-agnostic argument that fixes a prime-order elliptic-curve group's order without point-counting. - Layer 1 (card_eq_of_prime_witness): pure finite-group theory — a prime-order witness plus #G < 2r forces #G = r. - Layer 2: the Hasse bound (hasseInterval / HasseBound), assumed as a hypothesis since Mathlib lacks Hasse's theorem for WeierstrassCurve, discharges #G < 2r. Two routes to the curve capstone: the explicit gap (card_eq_of_hasse) and 37 <= #F with r in the Hasse interval (card_eq_of_hasse_of_field_ge_37). - No sorry/axiom/native_decide; Hasse cited to Crelle 175 (1936), §3.1/§4.2. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…oordinateSystem Add CompElliptic/ScalarMul.lean: `binNsmul`, a generic binary double-and-add over a raw `add`/`zero` (proven equal to the linear fold `linNsmul`), supplying the `nsmul_zero` / `nsmul_succ` obligations. Stated over raw ops so it can fill the `nsmul` field of the very instance it equips. Use it for the `nsmul` field of both the `SWPoint E` and `CoordinateSystem.Quot` AddCommGroup instances, so `n • _` computes in O(log n) and is native_decide-friendly for cryptographic-size scalars (≈ 2^254), while remaining the genuine scalar action (every Mathlib `n • _` lemma still applies). Add `DecidableEq (SWPoint E)`; `[r] G = 𝒪` is now a one-line native_decide. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Instantiate `card_eq_of_hasse_of_field_ge_37` at both Pasta curves: assuming `HasseBound`, the Pallas group has order `PALLAS_SCALAR_CARD` and the Vesta group order `PALLAS_BASE_CARD` (the Pasta cycle). The prime-order witness G = (-1, 2)'s `[order] G = 𝒪` is a one-line `native_decide` (the SWPoint `•` computes in O(log n)); the Hasse-interval membership and `37 ≤ #F` facts are concrete. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- New "group order" section: CurveOrder.lean (prime-order pinning via the Hasse bound) and Curves/PastaOrder.lean (Pallas/Vesta orders); cofactor variant deferred. - ShortWeierstrass: fast `•` via the generic binNsmul (ScalarMul.lean) + DecidableEq SWPoint. - CoordinateSystem.Quot `nsmul` is binNsmul too (affineCoordinateSystem is O(log n)); note the SWPoint-vs-affineCoordinateSystem redundancy as a deferred ergonomics call. - Disambiguate the still-pending circuit-windowed smul from the computational binNsmul. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This was referenced Jun 27, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pin a prime-order elliptic-curve group's order without point-counting, make the curve scalar action computable, and instantiate at the Pasta curves. Three commits:
1.
CurveOrder.lean— order pinning via Hassecard_eq_of_prime_witness): pure finite-group theory — a prime-order witness plus#G < 2rforces#G = r.hasseInterval/HasseBound(the sqrt-free Hasse bound). Mathlib lacks Hasse's theorem forWeierstrassCurve, so it is taken as a hypothesis (cited to Hasse, Crelle 175 (1936), §3.1/§4.2). Capstonescard_eq_of_hasse(explicit gap) andcard_eq_of_hasse_of_field_ge_37(37 ≤ #F+r ∈ hasseInterval #F).2.
ScalarMul.lean— generic fast scalar action •binNsmul, a generic binary double-and-add over rawadd/zero(proven equal to the linear foldlinNsmul, supplyingnsmul_zero/nsmul_succ). This is stated over raw ops so it can fill thensmulfield of the instance it equips. Used fornsmulin both theSWPoint EandCoordinateSystem.QuotAddCommGroupinstances (soaffineCoordinateSystemis fast too), plusDecidableEq (SWPoint E). Result:n • Pitself isO(log n)andnative_decide-friendly for≈ 2^254scalars, while staying the genuine group action — all Mathlib•lemmas still follow fromnsmul_zeroandnsmul_succ.3.
PastaOrder.lean— Pallas & VestaInstantiate
card_eq_of_hasse_of_field_ge_37: assumingHasseBound, the Pallas group has orderPALLAS_SCALAR_CARDand the Vesta groupPALLAS_BASE_CARD. The witness[order] G = 𝒪is a one-linenative_decide(fast•); the field-size facts are concrete.No
sorry/axiomanywhere; the abstract chain rests only on the standard axioms plus the named Hasse hypothesis.native_decideis confined to concrete closed per-curve facts (Independently re-checkable trust).Deferred: cofactor curves (
#G = h·r); Jubjub (not prime-order, and not short Weierstrass); and rationalising theSWPointvsaffineCoordinateSystemAPI redundancy.🤖 Generated with Claude Code