Fast EC arithmetic: projective addition, Pippenger MSM, 8-limb Montgomery fields

[mitschabaude-bot]

Human summary

This adds some very fast, certified curve arithmetic, motivated by the need in zcash/ironwood#99 to check correctness of dozens of size $2^{12}$ MSMs with native_decide (for the verifying key pin). In a first iteration that took 1.5 hours to build, these additions got it down to < 1min.

Interesting bits that I learned while doing this:

• You can do multi-threading in Lean quite easily, without breaking out of formally verified world
• precompileModules lets you compile modules and later import them normally in Lean. This is necessary for some stuff, like the Uint32-backed limb field arithmetic, which happens to be not very fast in Lean's interpreter

Additional AI summary

What is proven

Two tiers, the second proven equal to the first — and the first proven against the repository's pre-existing complete affine group law on SWPoint Vesta.curve (its nsmul for the ladder; the MSM specs are generic over [AddCommMonoid M] and consume the same instance at G). No new reference semantics is introduced, and no Mathlib bridge is involved.

• Curves/Pasta/Fast/Projective.lean — Renes–Costello–Batina complete addition (add-2015-rcb, a = 0) on (X : Y : Z) over 𝔽_q: toAffine_padd against SWPoint Vesta.curve, closure, leaf bridges, pnsmulFast_spec. Completeness rests on Vesta having no 2-torsion (Vesta.no_onCurve_y_zero); the polynomial cofactors were found by an offline Gröbner search and are re-checked here by ring, so they are re-derivable rather than trusted.
• Msm.lean / MsmProj.lean — windowed Pippenger, pippenger_eq_msm-proven equal to the naive MSM, generic over [AddCommMonoid M]; MsmProj runs the interior in projective coordinates (measured at n = 2048: naive 242 s → projective scatter 4.3 s → windows-parallel 0.8 s).
• ProjectiveMontDefs.lean / ProjectiveMontEquiv.lean — the same schedules on eight-limb Montgomery residues, importing nothing beyond Lean core, with every kernel operation proven to compute the reference: toPVesM_padd/_pid/_pneg, pnsmulM_spec, msmM_spec. The bridge is one hop — the vendored field's toField is a ring isomorphism onto ZMod q, so the coordinate map pushes through the RCB formulas, and the schedules are structural inductions against their MsmProj twins.

No sorry; #print axioms on every headline spec gives exactly propext / Classical.choice / Quot.sound — nothing extends the trust base. This is a build-time check: CompElliptic/TrustBoundary.lean pins the seven headline specs (toAffine_padd, smulFast_eq, padd_eq_paddFast, pippengerFastPar_eq_msm, commitLagrangeFastWith_eq, pnsmulM_spec, msmM_spec) at the flagless assert_axioms tier, so reaching native_decide or sorry anywhere in the fast tier fails the build.

Vendored CompPoly (CompElliptic/Vendor/)

The Montgomery tier needs eight-limb arithmetic not in the pinned CompPoly, so Vendor/CompPoly/Montgomery/ vendors branch fast_multilimb_fields @ b3850f0, namespaces left at upstream's Montgomery.*. Deletion criterion: the CompPoly pin advancing past CompPoly #258 + #274 — then the directory is deleted and the imports re-point; only Pasta.lean was rewritten (to reuse this repo's Pratt certificates, keeping a single Field instance). Details in CompElliptic/Vendor/README.md.

The precompile lane

lean_lib FastFieldNative precompiles the two zero-import definition modules so the arithmetic evaluates as compiled C rather than in the interpreter. Two invariants, both enforced by scripts/check_native_lane.sh and commented in the lakefile: the lane's import closure must stay core-only (native codegen over a mathlib closure OOMs), and the root module must be named after the library (the dynlib initializer symbol is derived from the .so name). Opt-in — import CompElliptic pulls in none of it — and easy to drop wholesale if unwanted.

Notes

• Not a CoordinateSystem instance: PVes is a bare triple with proven commutation. When the planned abstraction lands, the reusable part here is the RCB completeness argument; the two should be reconciled.
• Msm.lean is curve-generic apart from its commit_lagrange wrapper; it sits under Curves/Pasta/Fast/ only to keep the tree in one place.
• API stability: the Fast interfaces are provisional — they are not guaranteed to remain public, and may be folded into the existing API or otherwise changed incompatibly (see the CoordinateSystem reconciliation, Reconcile the fast projective arithmetic with the CoordinateSystem abstraction #15).

[Edited by @daira (assisted by Claude Fable 5): stated the correctness anchor (the pre-existing SWPoint affine law) up front, noted the trust-boundary pin added on the branch, and added the API-stability note.]

[daira]

Reviewed the full diff. Verdict: approve modulo the small items below. The trust discipline is exactly right throughout, and the two places where fast code could have quietly extended the trust base — native overrides and parallelism — both take the proven route instead.

One point worth stating up front, since it is the natural first question about a "proven fast arithmetic" PR: the correctness anchor is CompElliptic's pre-existing reference, not the PR's own definitions. toAffine_padd and smulFast_eq are stated against the existing complete affine group law on SWPoint Vesta.curve and its nsmul; the MSM specs are generic over [AddCommMonoid M], so at G they consume that same existing structure. Only the Montgomery tier is proven against the PR's own projective tier — which is in turn anchored as above. No Mathlib bridge is involved (unchanged from the rest of the repo).

What I verified

• Projective.lean in full: the RCB closed forms at a = 0, b = 5, b3 = 15; the Z = 1 core equivalence with all four case splits (distinct x, doubling, inverse, identity); completeness via the cube-root-of-−5 arguments (Z_ne_zero_dist, Y_ne_zero_inv), which are the paper's exceptional-cases-force-2-torsion claim made concrete against Vesta.no_onCurve_y_zero; homogeneity lifting to general valid points; and the toAffine homomorphism into SWPoint Vesta.curve. The offline Gröbner cofactors are re-verified in-kernel by linear_combination/ring, so nothing rests on the search. Citation checks out (EUROCRYPT 2016; EFD add-2015-rcb; the file states the polynomial form rather than the paper's operation schedule).
• padd_eq_paddFast is the proven counterpart of implemented_by — the fast raw-ℕ spelling never becomes the statement surface, and the decision not to register it @[csimp] yet is justified by measurement and documented with the exact condition under which to flip it.
• parMap: the trust analysis in the docstring is correct — Task is logically the one-field structure, the spawn/get round-trip is definitional, so parMap_eq_map makes parallelism purely an evaluation strategy inside the existing native_decide boundary. The kernel's view is literally List.map.
• Msm.lean/MsmProj.lean statement surface: pippengerFast(Par)_eq_msm against the naive MSM, generic over [AddCommMonoid M]; commitLagrangeFastWith_eq against the Pedersen spec; the projective interior via psum/pwindowValue specs.
• The Montgomery tier's statement surface (WF/montVal algebra, msmM_spec, pnsmulM_spec) and the vendoring discipline: deletion criterion pinned to CompPoly #258 + #274, per-file change table, upstream namespaces preserved, and the Pasta.lean rewrite keeping a single Field (ZMod PALLAS_SCALAR_CARD) instance.
• The precompile lane is opt-in (import CompElliptic pulls none of it), the core-only invariant is real (codegen over a mathlib closure), and check_native_lane.sh enforces the lane's import closure inductively.

Asks

1. Build-enforce the axiom claim — done on the branch (898f088). The body says #print axioms on every headline spec gives exactly propext/Classical.choice/Quot.sound; that is now a build-time check: TrustBoundary.lean pins toAffine_padd, smulFast_eq, pippengerFastPar_eq_msm, commitLagrangeFastWith_eq, padd_eq_paddFast, pnsmulM_spec, and msmM_spec at the standard tier, and the full build passes — confirming empirically that nothing in the fast tier reaches native_decide (completeness routes through no_onCurve_y_zero, a kernel decide).
2. Wire check_native_lane.sh into ci.yml. The script exists but nothing runs it; the invariant it guards fails silently (a build that quietly becomes enormous), which is exactly the kind of thing CI should catch. One step next to the generated-fields freshness check.
3. CI has not run on this branch — workflows now approved and running.
4. Nit, padd_eq_paddFast docstring: "makes every compiled call site … runs the fused raw-ℕ form" → "run".

Posted with the assistance of Claude Fable 5.