Skip to content

Fast, proven Pasta arithmetic + fixture-check speedup - #111

Merged
TalDerei merged 17 commits into
zcash:mainfrom
mitschabaude-bot:front-arithmetic
Jul 27, 2026
Merged

Fast, proven Pasta arithmetic + fixture-check speedup#111
TalDerei merged 17 commits into
zcash:mainfrom
mitschabaude-bot:front-arithmetic

Conversation

@mitschabaude-bot

@mitschabaude-bot mitschabaude-bot commented Jul 26, 2026 •
edited by daira
Loading

Copy link
Copy Markdown
Contributor

Human summary

This splits out the fast-arithmetic additions in #99, mostly via daira/CompElliptic#13 (see that PR for the motivation)

To find a logical home for plain arithmetic / mathematical algorithms, we added a new module called Zcash.Arithmetic. We then concluded that stuff like Field, Fp, Group, URS etc should also live in that module (it would have been awkward to import Snark from Arithmetic). This decision makes the PR somewhat large.

AI Contents

  • CompElliptic pin → daira/CompElliptic#13, now merged; the pin points at the canonical daira/CompElliptic merge commit. The proven fast Vesta arithmetic — complete projective addition, Pippenger MSM, the Montgomery-limb kernel.
  • Zcash/Arithmetic/ — new bottom layer (Snark → Arithmetic ← Vendor): the spec modules formerly in Snark/Core (Field, Domain, Group, Msm), the module-generic radix-2 FFT (bestFftG — instantiated here only at G := Fp as the scalar inverse-DFT spec; Integrate circuit soundness with the verifier soundness stack #99 instantiates it at the group), the scalar-FFT correctness proof, and the adapters over the pinned kernels. Namespace Zcash.Arithmetic throughout; Fp and URS are exported as root vocabulary under Zcash (one block in the Zcash/Arithmetic.lean umbrella), and one compat line (Zcash/Snark/Core.lean, exporting Msm) serves the byte-locked generated captures until their next regeneration.
  • Zcash/Vendor/CompPoly/ — one file: the scalar-FFT defs, verbatim from CompPoly's PR branch. Delete once the CompPoly pin passes #258 + #274.
  • Zcash.FastFieldNative — the local precompileModules leaf (scalar FFT only). The dotted name is load-bearing: module names are global, and a lib named like the pin's FastFieldNative collides silently — build stays green, the local dylib just never gets built.
  • Arithmetic/FastMsm.lean — proves the fixtures' naive Msm.evalNat equal to the pinned windowed Pippenger and registers it @[csimp]; wiring is one import line, no fixture file modified.

Measured

Same machine, fixture build artifacts deleted between runs; only the two generated captures evaluate the MSM.

module before after
Fixtures.MultiAction.Fixture 321 s 84 s
Fixtures.SingleAction.Fixture 306 s 69 s
whole FixtureCheck target 355 s 117 s

No sorry, no maxHeartbeats changes, axiom sets unchanged, lake build --wfail green.

🤖 Generated with Claude Code

[Edited by @daira (assisted by Claude Fable 5): the CompElliptic pin now references the canonical repository — #13 merged.]

mitschabaude-bot and others added 8 commits July 26, 2026 10:11
@mitschabaude-bot @claude
Add the fast-arithmetic prerequisites: ParMap and the evaluation domain
cdaf461 
Two new leaf modules that the fast Pasta arithmetic in the following commits
builds on, and nothing else in the repository yet depends on:

* `Zcash/Common/ParMap.lean` — a task-parallel `List.map` (`parMap`) proven equal
  to `List.map`, so parallelising a computation is a rewrite rather than a new
  trusted implementation.
* `Zcash/Snark/Core/Domain.lean` — the multiplicative evaluation domain of the
  Vesta scalar field: the `2^k` roots of unity, the domain generator and its
  order facts, shared by the group FFT and the scalar inverse DFT.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Vendor the CompPoly and CompElliptic fast-arithmetic trees
9c22f32 
Two self-contained, temporarily-vendored trees under `Zcash/Vendor/`, each with a
README stating its provenance and its deletion criterion:

* `Zcash/Vendor/CompPoly/` — eight-limb (8 x 32-bit in `UInt64`) Montgomery
  arithmetic for 255-bit primes, vendored from the CompPoly branch
  `fast_multilimb_fields`, plus the radix-2 DIT scalar FFT developed here.
  Deleted once ironwood's CompPoly pin carries both CompPoly#258 (the field) and
  CompPoly#274 (the scalar FFT).
* `Zcash/Vendor/CompElliptic/` — RCB complete projective Vesta addition, the
  bucket-method Pippenger MSM, the zero-import `Nat`-carrier kernel and its
  operation-for-operation equivalence proof, and the same kernel again on
  Montgomery residues. Developed here but generic; deleted once ironwood's
  CompElliptic pin provides it (daira/CompElliptic#13).

Layering, mirroring the upstream dependency direction: `Vendor/CompElliptic/`
may import `Vendor/CompPoly/`, never the reverse, so the two migrations stay
independent. Neither tree imports Keygen, Soundness or Clean.

The `*Defs.lean` modules are split out from their proofs and import nothing
beyond Lean core, so they can be native-compiled without dragging a mathlib
import closure through codegen.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Add Zcash/Arithmetic: the mathlib-side glue over the vendored kernels
538551f 
The ironwood-permanent half of the fast Pasta arithmetic — the part that stays
after the two `Zcash/Vendor/` trees are deleted:

* `Fft.lean` — the group FFT specification (`bestFftG`, `bitreverse`) over the
  evaluation domain, and its DFT characterisation.
* `FastFft.lean` / `FastFftPar.lean` — the projective drivers, the latter mapping
  the independent transforms through `parMap`.
* `NatKernelAdapter.lean` / `MontKernelAdapter.lean` — transport the vendored
  kernels' simulation proofs up to the mathlib-side statement surface, so callers
  see `bestFftG` and the Pippenger MSM, not `Nat` limbs.
* `ScalarFftEquiv.lean` — correctness of the scalar inverse DFT against the
  eight-limb Montgomery carrier.
* `VestaModule.lean` — the Vesta scalar-module structure the MSM is stated over.

Nothing here imports Keygen, Soundness or Clean.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Run the fixture MSM through the proven Pippenger accelerator
599aa05 
`Msm.evalNat` -- the executable natural-scalar MSM that the captured-fixture check
`capturedMsm_eval_eq_zero` evaluates under `native_decide` -- is spelled as its
specification: a `Finset` sum of per-generator `nsmul`s. Evaluated naively that is
~2050 binary double-and-add scalar multiplications, each paying a field inversion
per affine point addition, and it dominated the two generated fixture modules'
build times.

`Zcash/Snark/Fingerprint/FastMsm.lean` adds `Msm.evalNatFast`, computing the same
value through the windowed Pippenger accelerator with the windows evaluated in
parallel, and registers the kernel-checked equality `Msm.evalNat_eq_evalNatFast`
as `@[csimp]`. The compiler substitutes the fast implementation at every
subsequently compiled call site -- including the fixtures' `native_decide`
auxiliaries -- while the statement surface and the kernel-level meaning of
`evalNat` are untouched. This is the proven-equality counterpart of
`implemented_by`, which is unchecked and so not admissible here.

The hook fires wherever `FastMsm` is in the compiling module's import closure, so
the single import added to `Zcash/Snark.lean` is the whole wiring: the generated
fixture modules `import Zcash.Snark` and are not edited.

Two `lakefile.toml` targets come with it:

* `Arithmetic`, globbing `Zcash.Arithmetic.+`, `Zcash.Vendor.CompPoly.+` and
  `Zcash.Vendor.CompElliptic.+`, in `defaultTargets`. Not every module in those
  trees has an importer (`Zcash.Arithmetic.FastFftPar` has none), so without a
  target of their own they would silently stop being compiled.
* `FastFieldNative`, the only `precompileModules` target here. It is a core-only
  leaf -- its modules import nothing beyond Lean core, so native compilation
  covers four files rather than a mathlib import closure. It keeps a root module
  named after the library because Lean derives the dynlib's `initialize_…` symbol
  from the shared object's file name; without it every importer fails with
  `error loading plugin, initializer not found`.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Whitelist the padd identifier in the typos config
9c118a2 
The vendored projective point addition is named padd throughout
Vendor/CompElliptic and Arithmetic; the checker reads it as "pad".

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Adopt the upstream CompElliptic namespaces in the vendored tree
cd614ee 
The vendored fast-arithmetic tree under Zcash/Vendor/CompElliptic/ is destined
for CompElliptic, so its declaration namespaces should already be the ones the
upstream PR uses. Rename them accordingly:

  Zcash.Snark.Keygen.Fast.{Projective,Msm,MsmProj}
    -> CompElliptic.Curves.Pasta.Fast.{Projective,Msm,MsmProj}
  Zcash.Vendor.NatKernel      -> CompElliptic.Curves.Pasta.Fast.NatKernel
  Zcash.Vendor.ProjectiveMont -> CompElliptic.Curves.Pasta.Fast.ProjectiveMont

The inner PVes / PM namespaces are unchanged. With this the migration is an
import-path rewrite rather than a rename.

The ironwood-permanent glue keeps its own namespaces and reaches the vendored
declarations through `open CompElliptic.Curves.Pasta.Fast`.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Prune the superseded group-FFT lane
6eca79a 
Nothing evaluates a group FFT any more: the live chain runs the FFT over the
scalar field (ScalarFftDefs + ScalarFftEquiv) and uses the group kernels only
for the MSM. The group-FFT drivers and their simulation proofs were carried
along unused, and they were also the only reason the vendored equiv files
diverged from their upstream copies.

Deleted:

* Zcash/Arithmetic/FastFft.lean, Zcash/Arithmetic/FastFftPar.lean (whole files:
  bestFftGWith/bestFftGFast/bestFftGParFast and the derivedUrsGLagrange twins)
* Zcash/Vendor/CompElliptic/NatKernelEquiv.lean: fft_spec plus the twiddle
  table and the Sim/butterfly simulation lemmas that only served it
* Zcash/Vendor/CompElliptic/ProjectiveMontEquiv.lean: fftM_spec plus RA_fft,
  RA_roundFold, RA_butterfly, RA_permStep and the two loop-nest rfl lemmas
* Zcash/Arithmetic/NatKernelAdapter.lean: derivedUrsGLagrangeKernel and its _eq
* Zcash/Arithmetic/MontKernelAdapter.lean: derivedUrsGLagrangeMont and its _eq

Kept: the kernel fft/pneg/bitreverse definitions (they match the upstream copy,
so the eventual pin swap stays trivial), bestFftG and all of Zcash/Arithmetic/
Fft.lean, the commitLagrange*With committers and their _eq lemmas, the scalar
chain, and every MSM/ladder/cast spec.

The type-generic loop-nest declarations (fftGen, permStep, butterflyGen,
roundFoldGen, fftGen_eq_folds) are still used by the live ScalarFftEquiv, so
they move out of the vendored NatKernelEquiv into Zcash/Arithmetic/Fft.lean —
they need nothing beyond `bitreverse`, and this is what lets the two vendored
equiv files converge on their upstream shape.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Consume the fast Vesta arithmetic from the CompElliptic pin
97eebed 
Pin CompElliptic to daira/CompElliptic#13's head (a descendant of the
previously pinned rev; CompPoly and mathlib pins unchanged) and delete
the vendored copies it replaces. Vendor/CompPoly keeps only the scalar
FFT defs, which no pin provides until CompPoly#274 lands. The local
precompile lane becomes Zcash.FastFieldNative: a lib named exactly like
the pin's FastFieldNative collides silently (module names are global)
and the local dylib never gets built.

Fixture-check speedups verified at parity after the swap.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
mitschabaude-bot and others added 7 commits July 26, 2026 23:38
@mitschabaude-bot @claude
Explain why the module-generic FFT ships in this PR
748a421 
Its only instantiation here is G := Fp, as the scalar inverse-DFT
kernel's specification; the group instantiations arrive with the
verifying-key derivation built on top.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Keep the FFT docstring timeless
036a3c8 
The PR-scoped rationale lives in the PR description; the comment keeps
only the invariant (one generic definition, no scalar-vs-group
agreement lemma).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Move the arithmetic-tier specs into Zcash/Arithmetic
26e2dfc 
The scalar field, the verifier group/URS, the evaluation-domain scalars and the
fingerprint MSM are arithmetic, not verifier transcription: nothing in them
mentions the proof string, the challenges or the assembly. They sat under
Zcash/Snark/Core/ only for historical reasons, which left Zcash/Arithmetic/
importing *upwards* into Zcash/Snark/.

Move them one tier down, so Zcash/Arithmetic/ is genuinely below Zcash/Snark/:

  Zcash/Snark/Core/Field.lean        -> Zcash/Arithmetic/Field.lean
  Zcash/Snark/Core/Group.lean        -> Zcash/Arithmetic/Group.lean
  Zcash/Snark/Core/Domain.lean       -> Zcash/Arithmetic/Domain.lean
  Zcash/Snark/Core/Msm.lean          -> Zcash/Arithmetic/Msm.lean
  Zcash/Snark/Fingerprint/FastMsm.lean -> Zcash/Arithmetic/FastMsm.lean

FastMsm carries no fingerprint content at all: it is the proven Pippenger
accelerator for Msm.evalNat, registered with @[csimp], so it belongs beside the
MSM it accelerates.

This commit is import paths only -- every declaration keeps its namespace, so
nothing about the statements changes. The Arithmetic lean_lib glob
(Zcash.Arithmetic.+) already covers the new modules, and Zcash/Snark.lean keeps
them in the Zcash library's closure.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Adopt the Zcash.Arithmetic namespace
3b14127 
Everything under Zcash/Arithmetic/ now declares `namespace Zcash.Arithmetic`,
so the directory and the namespace agree. This replaces `Zcash.Snark`
(Field/Group/Domain/Msm), `Zcash.Snark.Keygen` (Fft), `Zcash.Snark.Keygen.Fast`
(MontKernelAdapter, VestaModule) and `Zcash.Vendor.ScalarMont`
(ScalarFftEquiv); genuine sub-namespaces stay nested, so the MSM operations are
`Zcash.Arithmetic.Msm.*` and the csimp accelerator joins them there.

Consumers are re-pointed properly: every module that spelled these names bare
under `namespace Zcash.Snark` now also opens `Zcash.Arithmetic`. `lake build
Zcash --wfail` passes with the shims below removed from the closure entirely,
which is the check that no editable module depends on them.

Zcash/Snark/Core/{Field,Group,Msm}.lean become three-line `export` shims for the
two byte-locked generated captures, which spell `Fp`, `URS` and `Msm` bare under
`open Zcash.Snark`; `Msm.evalNat` reaches them through field notation on the
structure and needs no alias. Core/Domain.lean gets no shim -- it had no
importer outside the tree at all. Both Fixture.lean files are byte-identical.

Also aligns the vendored scalar FFT with upstream, which now exists: the file is
CompPoly `fast_multilimb_fields`' CompPoly/Fields/Montgomery/ScalarFft.lean
verbatim (namespace `Montgomery.ScalarFft`, generic over `(q, negInv)`), edited
only in its import line to take the limb definitions from the CompElliptic pin.
That is the vendor rule: vendored files carry the upstream namespace so a pin
swap is an import-line change. The monomorphization ironwood needs is
`Zcash.Arithmetic.fftS`, at PallasFq's constants -- the Vesta *scalar* field is
the Pallas *base* field, and `fftS_eq_gen`'s `rfl` is the machine check that the
constants are the ones the deleted monomorphic copy used.

Statement spellings change namespace; statement structure does not. The fully
elaborated types of `fftS_spec` and the FastMsm csimp theorem are identical to
their pre-move forms after namespace renaming, and both keep the axiom set
[propext, Classical.choice, Quot.sound].

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Drop the dead chunked parMap and its ghost namespace
400579a 
chunk/parMapChunked lost their last caller with the group-FFT lane;
List.parMap and its simp lemma are root-level, so nothing remained in
Zcash.Snark.Keygen.Fast.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Name the commit-Lagrange module for its content
624cbd6 
`MontKernelAdapter` named the module after its implementation lineage — an adapter over the
Montgomery kernel, sibling of the since-deleted `NatKernelAdapter`. What it actually exports is
the fast `commit_lagrange` path and its proven equality to the naive spec, so it is now
`CommitLagrange`. The namespace is unchanged.

The docstring led with the same lineage framing; it now leads with the commitment and keeps the
Montgomery-lane notes where they state a real constraint (the native lane's glob boundary, and
`ofPVesM` never being safe to compare definitionally).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot @claude
Give Fp and URS root vocabulary, and drop the blanket Arithmetic opens
95baf6c 
Moving the arithmetic tier into `Zcash.Arithmetic` left 56 modules opening that namespace
wholesale just to say `Fp`. That is a lot of ceremony for two names, and a blanket open drags
in the whole tier's vocabulary as a side effect.

Instead, `Fp` and `URS` are re-exported at the `Zcash` root, from a new umbrella module
`Zcash/Arithmetic.lean`. Every module in this repository declares inside `Zcash.*`, so Lean's
enclosing-namespace walk finds them with no `open` at all — including the generated captures,
which declare in `Zcash.Snark.Fixture`. The 56 blanket opens are gone; 23 modules that use
non-rooted names (`scalarFieldOrder`, `card_Fp`, `Msm` and its lemmas) carry a scoped
`open Zcash.Arithmetic (...)` listing exactly what they use.

Only `Fp` and `URS` earn root vocabulary. There is deliberately no `G`: the verifier group is a
type variable throughout, and the concrete instantiations bind their own.

The three per-name `Core/{Field,Group,Msm}.lean` shims collapse to one `Core.lean` carrying
`Msm` alone — the one capture spelling the root export does not cover, since `Msm` is not
common enough to belong at the root. Editable consumers reach it through
`open Zcash.Arithmetic (Msm)`, never through the compat name, so the file can be deleted
outright when the captures are regenerated.

The base modules everything else imports (`Fingerprint/{Batch,SchwartzZippel}`,
`Soundness/{Constraints,InnerProduct,Forking/Oracle,Deployed/ConcreteBounds}`,
`Verifier/{Checks,Ipa}`) now import the umbrella rather than the individual definition
modules, which is what puts the root names in everyone's closure.

Verified: `lake build --wfail` green with zero warnings, and both generated captures byte-identical.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@mitschabaude-bot
mitschabaude-bot marked this pull request as ready for review July 27, 2026 00:28
daira
daira reviewed Jul 27, 2026
View reviewed changes

@daira daira left a comment •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reviewed the full diff (the CompElliptic side is reviewed separately on daira/CompElliptic#13). Verdict: the structure is right — Zcash.Arithmetic as the bottom layer (Snark → Arithmetic ← Vendor) is a sensible home, and the trust discipline carried over from the CompElliptic side is intact. Approve once the pin item below is resolved.

What I verified

  • FastMsm.lean: evalNat_eq_evalNatFast is a kernel-checked equality registered @[csimp] — the proven-equality counterpart of implemented_by, which the module doc correctly identifies as forbidden. The statement surface (evalNat as the Finset-sum spec) is untouched; the fixtures' native_decide auxiliaries pick up the windows-parallel Pippenger automatically. The genericity constraint (a csimp lemma replaces the whole constant, so the replacement stays generic over [AddCommGroup G] and the Vesta-projective interior is not admissible) is real and well documented.
  • The lakefile: the Arithmetic target keeps otherwise-unreached modules compiled and warning-checked; the Zcash.FastFieldNative dotted-name requirement is exactly the right fix for the silent dynlib collision with the pin's own lane, and the comment documenting the failure mode (build green, wrong plugin, interpreted fallback) is the kind that saves someone a day.
  • Vendoring: Zcash/Vendor/CompPoly/ follows the same discipline as the CompElliptic side — one file, README, deletion criterion pinned to CompPoly #258 + #274.
  • The moves: the Snark/Core → Arithmetic relocation is import-path and namespace mechanics; the Zcash/Snark/Core.lean compat line for the byte-locked captures has a stated retirement point (next regeneration).

Asks

  1. Re-pin before merge (done). The manifest points CompElliptic at mitschabaude-bot/CompElliptic.git — fine as an interim while daira/CompElliptic#13 is in review, but main should not land pinned to a personal fork: the SHA is content-stable, but availability and the provenance anchor belong on the canonical repo. Ordering: land CompElliptic#13 first, re-pin here to the resulting daira/CompElliptic commit, then merge.
  2. Confirm CI ran on the head that gets merged — the fixture modules are the expensive path and the measured table is from a local machine.

Posted with the assistance of Claude Fable 5.

@daira @claude
Re-pin CompElliptic to the canonical repository after daira/CompEllip…
caaf766 
…tic#13 merged

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
daira
daira reviewed Jul 27, 2026
View reviewed changes
Comment thread Zcash/Arithmetic/CommitLagrange.lean Outdated
@mitschabaude @daira
Update Zcash/Arithmetic/CommitLagrange.lean
308b6ac 
Co-authored-by: Daira-Emma Hopwood <daira@jacaranda.org>
TalDerei
TalDerei approved these changes Jul 27, 2026
View reviewed changes

@TalDerei TalDerei left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ACK

@TalDerei
TalDerei merged commit 8bed737 into zcash:main Jul 27, 2026
11 checks passed
TalDerei pushed a commit that referenced this pull request Jul 28, 2026
@mitschabaude-bot
Merge origin/main (PR #111) into the circuit-soundness integration br…
b9e4378 
…anch

Closes out the fast-arithmetic arc. The branch already carried #111's content
through 95baf6c via prior direct merges; main adds only the two commits that
landed on the PR branch after that point:

* caaf766 re-pins CompElliptic to the canonical daira/CompElliptic after
  daira/CompElliptic#13 merged (fd997734, was mitschabaude-bot @ 53b35333).
  The two revisions differ only in docstrings and a TrustBoundary.lean
  `assert_axioms` block for the Fast tier -- no definition or proof changes.
* 308b6ac expands "CIOS" in the Zcash/Arithmetic/CommitLagrange.lean docstring.

No conflicts. The lakefile/manifest automerge keeps this branch's Clean pin
(18c8a6b9) and its FixtureCheck/CircuitCheck target layout while taking main's
CompElliptic re-pin.

Nothing else landed on main outside #111. Captured fixtures are byte-identical.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@daira daira daira left review comments
@TalDerei TalDerei TalDerei approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mitschabaude-bot @daira @TalDerei @mitschabaude