perf(verifier): factor shared zerofier + batch DEEP inversions#829
perf(verifier): factor shared zerofier + batch DEEP inversions#829diegokingston wants to merge 5 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 | 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).
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. |
2 participants
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.