Consolidate BN254 field math under the Lampe layer#305
Merged
Conversation
kustosz
approved these changes
Jun 4, 2026
Eduardogbg
force-pushed
the
edu/bn254-refactor
branch
2 times, most recently
from
fa79a81 to
5add67c
Compare
…e Lampe layer Move r_scalar, plo, phi, pow128, the Bn254.Prime typeclass, and the pure-math limb-arithmetic lemmas out of Stdlib/Field/Bn254.lean into the new Lampe/Crypto/Bn254.lean, and move the Pratt primality certificate with the concrete prime (Stdlib/Field/Bn254/Prime.lean -> Lampe/Crypto/Bn254/Prime.lean), matching the Secp256k1/Secp256r1 layering. The stdlib files now only house Noir-extracted bindings and STHoare specs. The Bn254.Prime contract is unified on natVal_eq_r_scalar (the limb form stays available as the natVal_eq_limbs lemma). The concrete prime is namespaced as Lampe.Crypto.Bn254.prime, mirroring Lampe.Crypto.Secp256k1.prime, with primeNat defined as r_scalar so the Bn254.Prime Bn254.prime instance holds by rfl, shrinking the trust path. Also fixes Mathlib bitrot in EmbeddedCurveOps/Bn254: WeierstrassCurve.Affine.Point.some now takes x y explicitly.
Drop the duplicated scalarModulus definition in favour of re-exporting Lampe.Crypto.Bn254.r_scalar via `export`. Tests/Poseidon2 picks up the exported name through the existing `open Lampe.Crypto.Poseidon2.BN254T4`.
…k_all Stdlib/EcdsaSecp256K1.lean, Stdlib/EcdsaSecp256R1.lean and Stdlib/EmbeddedCurveOps/Bn254.lean were never imported from the Stdlib library root, so lake build (and CI) never elaborated them and their proofs could silently rot; this is how the ECDSA specs went unbuilt since #296. All three compile cleanly once registered. The Stdlib lib root is now the flat mk_all-managed import list (Stdlib/Stdlib.lean shrinks to the env export it exists for), and CI runs `lake exe mk_all --check --lib Stdlib` after the stdlib build - the same guard the Lampe package has. The testing Spec roots import the new root.
gen_pratt.py now serves all three Prime.lean files and the bespoke gen_bn254_pratt.py is deleted. Rather than carrying per-namespace header/footer templates, the checked-in Prime.lean files own their hand-maintained headers/footers, and the generated certificate region is delimited by BEGIN/END marker comments: - Update mode: `gen_pratt.py --prime <P> --update <Prime.lean>` regenerates only the marked region in place, preserving everything outside the markers byte-for-byte. Errors if markers are missing or duplicated, or if the file never references prime_<P> outside the region (wrong --prime). - Bootstrap mode for brand-new primes: `--prime <P> --namespace <Name>` emits a generic scaffold (with markers) to stdout for the author to hand-tune. The Secp256k1 and Secp256r1 Prime.lean files gain the markers and updated regeneration instructions (comment-only changes; defs, theorems and instances untouched); the Bn254 file carries them since its extraction. --update is verified idempotent on all three.
Eduardogbg
force-pushed
the
edu/bn254-refactor
branch
from
5add67c to
9b32bca
Compare
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.
I created this PR to organize BN254 logic to match the pattern we introduced
on the curve ops + ECDSA work. It was a bit ad-hoc and scattered, with a lot
of pure logic living on Stdlib, and about to get worse due to the Pedersen PR.
Now it has a Pratt certificate and the necessary instances, and only Hoare
triples live on Stdlib.
Update: I also added a few things around detecting orphan modules to this PR, which is a bit of misc but fit this PR better than the other one and it would require an annoying juggling of rebases to make this in a third branch