Skip to content

perf(verifier): factor shared zerofier + batch DEEP inversions - #829

Open
diegokingston wants to merge 6 commits into
mainfrom
perf/verifier-step2-deep-arith
Open

perf(verifier): factor shared zerofier + batch DEEP inversions#829
diegokingston wants to merge 6 commits into
mainfrom
perf/verifier-step2-deep-arith

Conversation

@diegokingston

Copy link
Copy Markdown
Collaborator

Two extension-field arithmetic redundancies on the STARK verify path, each turning a per-item inversion into shared work. Stacked on #823 (base is feat/logup-acc-current-row, so the diff is just these two changes; the DEEP one builds on that PR's pruned loop). Retarget to main once #823 lands.

Why

Profiling the ABBA/ethrex verify (204 MiB, ~3.8s) showed the wall-clock is ~85%+ Keccak Merkle-path hashing, single-threaded — these arithmetic wins won't move that number. But they cut serial extension-field inversions, which is exactly what the recursion-guest cycle count pays for (the guest runs this same verifier.rs, and a cubic-extension inversion is a long addition chain). So they're aligned with the g·z-pruning cycle-reduction work, not the native 3.8s.

step_2 — shared zerofier

Every transition constraint's OOD zerofier is 1/(zᴺ − 1) × an end-exemptions correction ∏(z − rᵢ) that depends only on end_exemptions. Before, each constraint recomputed zᴺ (a pow) and a fresh extension inversion, and the sum multiplied every term by its own denominator. Now: compute 1/(zᴺ − 1) once, group constraints by end_exemptions (almost always the single group {0}), accumulate Σ βᵢ·evalᵢ per group, and factor the shared inverse + each group's correction out. Removes ~C pows and ~C inversions per table (C = #transition constraints) — mirroring the prover's existing grouped-zerofier dedup. Also turns a zᴺ = 1 hit from a panic into a clean rejection.

step_3 — batched DEEP inversions

reconstruct_deep_composition_poly_evaluation ran two tiny per-query inversions (a batch-inverse over ~2 denominators + a lone composition-denominator inversion), 2·num_queries times per table — defeating Montgomery amortization. The z·gᵏ row points and z^parts are query-independent, so hoist them once, collect every query point's (h+1) denominators, and run one batch inverse for the whole proof. Collapses ~4·num_queries extension inversions/table → ~1. The inner function now takes the pre-inverted denominators (its evaluation_point/primitive_root args drop out). Malformed-proof rejection is preserved — a denominator on an OOD point fails the single batch inverse.

Tests

Full stark lib suite green (198), including multi_prove roundtrips, soundness negatives (tampered/truncated OOD + composition), and the archived read-in-place path. clippy clean.

@diegokingston

Copy link
Copy Markdown
Collaborator Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

@github-actions

github-actions Bot commented Jul 16, 2026

Copy link
Copy Markdown

Verifier benchmark — ee21913a4c vs main (20 pairs)

=== Verify ABBA result ===

Metric main PR Δ
Verify time 3.605s 3.580s -0.69% 🟢
Proof size 204.30 MiB 204.30 MiB +0.00% ⚪
  pairs: 20   mean A (PR): 3.580s   mean B (main): 3.605s
  [parametric] paired-t   mean -0.69%   sd 0.49%   se 0.11%
               95% CI: [-0.92%, -0.46%]   (t df=19 = 2.093)
  [robust]     median -0.73%   Wilcoxon W+=3 W-=207  p(exact)=9.5e-06  (z=-3.79)

  run-to-run jitter:    A CV 0.37%   B CV 0.37%        (lower = steadier)
  within-session drift: +0.03% over the run, 1st->2nd half -0.03%

🟢 REAL IMPROVEMENT — PR verifies ~0.69% faster (paired-t and Wilcoxon agree).

Drift-free interleaved A/B/B/A measurement. - = PR faster. Trust the verdict when paired-t and Wilcoxon agree.


Recursion guest cycles (main vs PR)

=== Recursion-guest cycle comparison — single query (blowup=2, 1 query) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main 68a120a guest=recursion-min.elf
REF_A (PR) ee21913 ee21913 guest=recursion-min.elf

Metric REF_B (baseline) REF_A (PR) Δ (A-B)
Guest cycles 41.7M 36.6M -5.1M (-12.23%)
Keccak calls 3025 3025 0

note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.

raw (exact integer counts)
ref_b_sha=68a120a6d42bbaf203f4f7db85604ecdb5d300c0 ref_b_elf=recursion-min.elf ref_b_cycles=41727694 ref_b_keccak=3025 ref_b_execute_wall_s=2
ref_a_sha=ee21913a4cc189ac9359d16d2fb3f581e5075398 ref_a_elf=recursion-min.elf ref_a_cycles=36626124 ref_a_keccak=3025 ref_a_execute_wall_s=1
delta_cycles=-5101570 delta_keccak=0

…p_2/3

Two extension-field arithmetic redundancies on the STARK verify path, each
turning a per-item inversion into shared work. Both cut serial field ops, so the
win lands on the recursion-guest cycle count (native wall-clock is dominated by
Keccak Merkle hashing, unaffected). Verified identical on the full stark suite
(198, incl. multi_prove roundtrips + soundness negatives + the archived
read-in-place path); clippy clean.

step_2 (claimed composition polynomial):
- Every transition constraint's OOD zerofier is 1/(zᴺ − 1) times an
  end-exemptions correction ∏(z − rᵢ) that depends only on `end_exemptions`.
  Previously each constraint recomputed zᴺ (a `pow`) AND a fresh cubic-extension
  inversion, then the sum multiplied every term by its own denominator.
- Now: compute 1/(zᴺ − 1) once, group constraints by `end_exemptions` (almost
  always the single group {0}), accumulate Σ βᵢ·evalᵢ per group, and factor the
  shared inverse + each group's correction out of the sum. Removes ~C `pow`s and
  ~C extension inversions per table (C = #transition constraints), matching the
  prover's existing grouped-zerofier dedup. New `end_exemptions_correction` helper
  in constraints/zerofier.rs; `evaluate_zerofier` now delegates to it.
- Also converts a `z on trace domain` (zᴺ = 1) hit from a panic (`.unwrap`) to a
  clean rejection.

step_3 (DEEP composition reconstruction):
- `reconstruct_deep_composition_poly_evaluation` ran two tiny per-query
  inversions — a batch-inverse over the ~2 OOD-row denominators plus a lone
  composition-denominator inversion — 2·num_queries times per table, defeating
  Montgomery amortization.
- The z·gᵏ row points and z^parts are query-independent; hoist them once, then
  collect every query point's (h + 1) denominators and run ONE batch inverse for
  the whole proof. The inner function takes the pre-inverted denominators, so its
  `evaluation_point`/`primitive_root` args drop out. Collapses ~4·num_queries
  extension inversions per table to ~1. Malformed-proof rejection is preserved:
  a denominator landing on an OOD point fails the single batch inverse (closed).
@diegokingston
diegokingston force-pushed the perf/verifier-step2-deep-arith branch from 9b78618 to 4d4d886 Compare July 16, 2026 19:56
@diegokingston

Copy link
Copy Markdown
Collaborator Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

@diegokingston

Copy link
Copy Markdown
Collaborator Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

@MauroToscano MauroToscano left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

⚠️ AI-generated review. Produced by an automated agent and posted from this account — not written by hand. Findings below are leads to verify, not confirmed conclusions.

Two refactors: step_2 regroups Σ βᵢ·evalᵢ into end_exemptions buckets scaled by ∏(z−rᵢ) and a shared 1/(zᴺ−1), and step_3 batches the DEEP denominators across queries. Both are algebraically equivalent to what they replace, no transcript absorb or squeeze moves, and both .inv() / inplace_batch_inverse(...).ok()? fail closed. Two issues.

crypto/stark/src/verifier.rs:338 — the −12.23% guest-cycle headline is the min preset: one FRI query at blowup 2, i.e. the regime that flatters this PR most. The step_2 saving (one pow plus one extension inversion per transition constraint, per table) is query-invariant, so its absolute value is fixed while the baseline grows roughly linearly with queries; at ~219 queries for an inner proof its share drops by about two orders of magnitude. The DEEP half scales the other way (~2 inversions per query per table), but the net will not be ~12%. The bench baseline 68a120a6 is six commits behind, and the run itself reported that blowup2/blowup4 full-query regimes needed RECURSION_DUMP_PRESET on origin/main. #846 landed RECURSION_DUMP_PRESET and RECURSION_DUMP_EPOCH_LOG2 on main on 07-21, so a rebase plus a fresh /bench-verify can run the full-query and real-block regimes. Book that number, not the single-query one.

crypto/stark/src/constraints/zerofier.rs:142end_exemptions_correction re-derives the backward root walk line for line from end_exemptions_roots (same decrement = g^(N−1) seed, same current = current * decrement step, lines 31-37). The old evaluate_zerofier reused the shared helper; the rewrite inlines it, and the new correction_matches_direct_exempt_product_over_cubic_extension test exists only to catch the two copies drifting. The inlining saves one Vec of ≤2 elements per distinct end_exemptions per table — negligible against the extension products. end_exemptions_roots has no callers outside this file, so it can take end_exemptions: usize instead of &ConstraintMeta (its only use of meta is meta.end_exemptions, and end_exemptions_lde_evaluations already has that value), with the correction becoming a fold over its result — roots.iter().fold(one, |acc, r| acc * -(r.clone() - z.clone())), the deleted body. One root derivation, regression test still applies.

Nits:

  • verifier.rs:915 — for (i, _iota) in challenges.iotas.iter().enumerate() binds an iota only to discard it; num_queries is in scope at line 853 and is the quantity both the openings guard and the denominators capacity are stated in, so for i in 0..num_queries reads better.
  • verifier.rs:960 — the call site computes primary_base/sym_base and hand-slices four arguments into a 16-parameter function that re-checks the trace-slice lengths at 1041-1046, splitting the [trace rows | composition] stride between caller and callee; passing the two per-point stride-sized chunks and splitting at ood_height in the callee drops two parameters and the offset arithmetic.
  • The PR body's "~4·num_queries extension inversions/table → ~1" is the pre-fuse shape: on this base the function is already the fused pair (one call per iota, two real inversions), so it is 2·num_queries as the comment at line 882 states, and the 4· figure re-claims the halving #826 already shipped.

@MauroToscano

Copy link
Copy Markdown
Contributor

/bench

@github-actions

github-actions Bot commented Aug 1, 2026

Copy link
Copy Markdown

Benchmark — real block (ethrex_mainnet_25368371.bin) (median of 3)

continuations · epoch 2^22 · 13 epochs

Metric main PR Δ
Peak heap 51856 MB 52480 MB +624 MB (+1.2%) ⚪
Prove time 159.217s 158.199s -1.018s (-0.6%) ⚪

✅ No significant change.

Prove-time spread 1.6% (160.271s / 158.199s / 157.759s)

Commit: f59bc4a · Baseline: cached · Runner: self-hosted bench

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants