Repository navigation
Sync with upstream: unconditional Pasta group orders (daira/CompElliptic#6) - #2
Merged
Merged
Conversation
The role names stated the Pasta cycle as a pun (VestaBaseField = PallasScalarField and vice versa) — four names for two fields. The fields now carry their standard absolute names: Fp (the Pallas base field, also the Vesta scalar field) and Fq (the Pallas scalar field, also the Vesta base field), matching proof-systems' own convention. Role information belongs to consumers' relative projections, not to which alias was picked. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Several facts were being re-derived ad hoc at each use site. Pull them
out to a single home so that callers, existing and future, can consume
them instead of restating them.
* `SWPoint.equivSubtype` — the `SWPoint E ≃ { pr : F × F // Valid .. }`
injection was hand-rolled separately for decidable equality and for
finiteness. Both now derive from the equiv, as does anything that
wants to count points as a subtype of `F × F`.
* `Decidable (Valid a b p)` — sits beside the `OnCurve` instance it
builds on. This removes the need to write `Or.inl (by decide)` to
exhibit a representable point, and with it the comment in
`Encodings/Pasta` explaining why `Valid` could not be decided
directly.
* `SWPoint.neg_x` / `SWPoint.neg_y` — `(-P).y = -P.y` is `rfl`, but was
inlined with a "there is no named lemma for it" apology at each use.
Now there is one.
* `dvd_natCard_of_prime_witness` — the prime-witness half of
`card_eq_of_prime_witness`, split off so other order-pinning routes
can share it. Its body also stops hand-rolling Mathlib's
`addOrderOf_eq_prime`, which is exactly the three lines it spelled out.
No new mathematical results and no statement changes: every existing
theorem keeps its signature, and only proofs and locations move.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fix the Pallas and Vesta group orders to their known primes with no assumption. A prime-order witness ([order]·G = 𝒪) gives r ∣ #E; it then remains to bound #E. Mathlib has no Hasse bound for WeierstrassCurve, so use the elementary fibre bound looser than Hasse (a factor of ~2 rather than 2√q) but unconditional, and enough when r ≈ #F: Pallas closes directly (#F < r ⇒ #E < 2r), and Vesta additionally rules out CurveOrder holds the reusable core: Layer 1 pins the order from the witness plus an upper bound (< 2r, or < 3r without 2-torsion); Layer 2 is the fibre bound. Curves.PastaOrder instantiates it at the two curves. Every remaining obligation is a closed comparison of Co-authored-by: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
Pin the Pasta group orders without assuming Hasse
Upstream deletes the HasseBound hypothesis entirely: card_eq is now unconditional via the elementary fibre bound #E <= 2#F + 1 + the prime-order witness (Vesta's #E = 2p case excluded by -5 not being a cube). Conflicts resolved by taking upstream's proofs with this fork's absolute field names (Fp/Fq) substituted for the old role aliases.
The absolute-field-names commit renamed the four role aliases to Fp/Fq in the generated CompElliptic/Fields/Pasta.lean but never updated scripts/gen_pasta.py, so the generator-reproducibility CI gate failed once it ran on a PR. field_block gains an optional fielddoc parameter (the committed file carries docstrings on the field abbrevs; gen_jubjub.py is unaffected by the default), and gen_pasta.py emits Fp/Fq throughout. Verified: both gen_pasta.py and gen_jubjub.py reproduce the committed files byte-identically under PARI/GP.
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
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.
Merges daira/CompElliptic
main(through daira/CompElliptic#6) into this fork, on top of ourabsolute-field-namesline.Upstream deletes the
HasseBoundhypothesis entirely:card_eqis now unconditional, via the elementary fibre bound#E ≤ 2·#F + 1plus thenative_decideprime-order witness (Vesta's leftover#E = 2pcase is excluded because−5is not a cube — newFields/Residue.lean).Gpt/Gpt_ne_zeronow discharge by kerneldecide.Conflict resolution (PastaOrder, Encodings, plus alias fixes in Curves/Pasta): take upstream's proofs with this fork's absolute field names (
Fp/Fq) substituted for the old role aliases. OurSWPoint ↔ Affine.Pointequivalence + card bridge and the v4.30.0 toolchain are preserved.Downstream (l-adic/snarky
formal/pasta) this deletes the two Hasse axioms — the workspace's last declared curve axioms.🤖 Generated with Claude Code
https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD