perf(verifier): factor shared zerofier + batch DEEP inversions - #829
perf(verifier): factor shared zerofier + batch DEEP inversions#829diegokingston wants to merge 9 commits into
Conversation
|
/bench-verify |
|
⏳ 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. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 20 pairs) | 2.553s | 2.575s | +0.87% 🔴 |
| Proof size (exact, 1 reading) | 115.67 MiB | 115.67 MiB | +0.00% ⚪ |
pairs: 20 mean A (PR): 2.575s mean B (main): 2.553s
[parametric] paired-t mean +0.87% sd 0.56% se 0.12%
95% CI: [+0.61%, +1.13%] (t df=19 = 2.093)
[robust] median +0.94% Wilcoxon W+=210 W-=0 p(exact)=1.9e-06 (z=+3.90)
run-to-run jitter: A CV 0.45% B CV 0.40% (lower = steadier)
within-session drift: -0.14% over the run, 1st->2nd half +0.10%
🔴 REAL REGRESSION — PR verifies ~0.87% slower (paired-t and Wilcoxon agree).
ethrex 20-tx block · continuations, epoch 2^20 (4 epochs) · blowup=2, 219 queries
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 8 pairs) | 3.976s | 3.995s | +0.48% 🔴 |
| Proof size (exact, 1 reading) | 231.37 MiB | 231.37 MiB | +0.00% ⚪ |
pairs: 8 mean A (PR): 3.995s mean B (main): 3.976s
[parametric] paired-t mean +0.48% sd 0.54% se 0.19%
95% CI: [+0.02%, +0.93%] (t df=7 = 2.365)
[robust] median +0.38% Wilcoxon W+=26 W-=2 p(exact)=0.0469 (z=+1.94)
run-to-run jitter: A CV 0.42% B CV 0.51% (lower = steadier)
within-session drift: -0.23% over the run, 1st->2nd half -0.28%
🔴 REAL REGRESSION — PR verifies ~0.48% slower (paired-t and Wilcoxon agree).
Verify-time rows only: drift-free interleaved A/B/B/A, with paired-t and exact Wilcoxon — trust the verdict when the two agree. Proof sizes are single exact readings (no averaging). - = PR faster.
Recursion guest cycles — verifier running INSIDE the VM (main vs PR)
empty program · monolithic · blowup=2, 1 query (diagnostic — NOT a real verifier cost)
Single exact reading per ref — no ABBA: guest cycles are deterministic for a fixed
(guest ELF, input blob), so there is no machine drift to cancel.
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 331.7M | 326.3M | -5.3M (-1.60%) |
| Keccak calls | 3029 | 3029 | 0 |
baseline origin/main 8064a8efee guest=recursion-min.elf
PR dba9d0941b5fd21f71993006438c9fe1f10129aa dba9d0941b guest=recursion-min.elf
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism);
treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=8064a8efee4bd3edc9f064337d4e1d8bad54ae1a ref_b_elf=recursion-min.elf ref_b_cycles=331650450 ref_b_keccak=3029 ref_b_execute_wall_s=9
ref_a_sha=dba9d0941b5fd21f71993006438c9fe1f10129aa ref_a_elf=recursion-min.elf ref_a_cycles=326333311 ref_a_keccak=3029 ref_a_execute_wall_s=10
delta_cycles=-5317139 delta_keccak=0
ethrex 20-tx block · continuations, epoch 2^21 (2 epochs) · blowup=2, 219 queries (128-bit)
Single exact reading per ref — no ABBA: guest cycles are deterministic for a fixed
(guest ELF, input blob), so there is no machine drift to cancel.
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 2280.0M | 2219.4M | -60.6M (-2.66%) |
| Keccak calls | 3538646 | 3538634 | -12 |
baseline origin/main 8064a8efee guest=recursion-cont-blowup2.elf
PR dba9d0941b5fd21f71993006438c9fe1f10129aa dba9d0941b guest=recursion-cont-blowup2.elf
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism);
treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=8064a8efee4bd3edc9f064337d4e1d8bad54ae1a ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=2280036712 ref_b_keccak=3538646 ref_b_execute_wall_s=37
ref_a_sha=dba9d0941b5fd21f71993006438c9fe1f10129aa ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=2219400359 ref_a_keccak=3538634 ref_a_execute_wall_s=35
delta_cycles=-60636353 delta_keccak=-12
…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).
9b78618 to
4d4d886
Compare
|
/bench-verify |
|
⏳ 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. |
|
/bench-verify |
|
⏳ 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. |
There was a problem hiding this comment.
⚠️ 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:142 — end_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_queriesis in scope at line 853 and is the quantity both the openings guard and thedenominatorscapacity are stated in, sofor i in 0..num_queriesreads better. - verifier.rs:960 — the call site computes
primary_base/sym_baseand 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-pointstride-sized chunks and splitting atood_heightin 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.
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 48158 MB | 48102 MB | -56 MB (-0.1%) ⚪ |
| Prove time | 138.698s | 137.722s | -0.976s (-0.7%) ⚪ |
✅ No significant change.
Prove-time spread 0.5% (137.374s / 137.722s / 138.001s)
Commit: 43e3dda · Baseline: built from main · Runner: self-hosted bench
|
/bench |
|
/bench-verify |
|
⏳ Benchmark started on the bench server. Two verifier arms (monolithic + continuations over an ethrex 20-tx block), then the recursion-guest cycle comparison, which adds guest builds on top — longer on a cold runner. The bench server is occupied until it finishes. |
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 tomainonce #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 onend_exemptions. Before, each constraint recomputedzᴺ(apow) and a fresh extension inversion, and the sum multiplied every term by its own denominator. Now: compute1/(zᴺ − 1)once, group constraints byend_exemptions(almost always the single group{0}), accumulateΣ βᵢ·evalᵢper group, and factor the shared inverse + each group's correction out. Removes ~Cpows and ~C inversions per table (C = #transition constraints) — mirroring the prover's existing grouped-zerofier dedup. Also turns azᴺ = 1hit from a panic into a clean rejection.step_3 — batched DEEP inversions
reconstruct_deep_composition_poly_evaluationran two tiny per-query inversions (a batch-inverse over ~2 denominators + a lone composition-denominator inversion),2·num_queriestimes per table — defeating Montgomery amortization. Thez·gᵏrow points andz^partsare 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_queriesextension inversions/table → ~1. The inner function now takes the pre-inverted denominators (itsevaluation_point/primitive_rootargs drop out). Malformed-proof rejection is preserved — a denominator on an OOD point fails the single batch inverse.Tests
Full
starklib suite green (198), including multi_prove roundtrips, soundness negatives (tampered/truncated OOD + composition), and the archived read-in-place path. clippy clean.