perf(verifier): amortize per-table/per-query verifier work (Tier 0 + Tier 1)#830
perf(verifier): amortize per-table/per-query verifier work (Tier 0 + Tier 1)#830diegokingston wants to merge 1 commit 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.582s | 3.581s | -0.01% ⚪ |
| Proof size | 204.30 MiB | 204.30 MiB | +0.00% ⚪ |
pairs: 20 mean A (PR): 3.581s mean B (main): 3.582s
[parametric] paired-t mean -0.01% sd 0.65% se 0.15%
95% CI: [-0.32%, +0.30%] (t df=19 = 2.093)
[robust] median +0.10% Wilcoxon W+=132 W-=78 p(exact)=0.3300 (z=+0.99)
run-to-run jitter: A CV 0.30% B CV 0.48% (lower = steadier)
within-session drift: +0.12% over the run, 1st->2nd half +0.14%
⚪ INCONCLUSIVE — effect not separable from 0 at n=20 (point estimate ~+0.10%). Add pairs to resolve.
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 a864832 guest=recursion-min.elf
REF_A (PR) 1ea7876 1ea7876 guest=recursion-min.elf
| Metric | REF_B (baseline) | REF_A (PR) | Δ (A-B) |
|---|---|---|---|
| Guest cycles | 43.6M | 38.3M | -5.3M (-12.21%) |
| 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=a8648320867f7f4242fe286a5b266ffed1fb5519 ref_b_elf=recursion-min.elf ref_b_cycles=43608950 ref_b_keccak=3025 ref_b_execute_wall_s=1
ref_a_sha=1ea787697917bf6e4b85620c8913907b5b5a3683 ref_a_elf=recursion-min.elf ref_a_cycles=38284840 ref_a_keccak=3025 ref_a_execute_wall_s=1
delta_cycles=-5324110 delta_keccak=0
|
/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. |
9b78618 to
4d4d886
Compare
Two recursion-cycle savings in the verifier (= serial recursion guest): 1. Drop VerifierDomain::root_order. The DEEP driver recomputed the trace primitive root via get_primitive_root_of_unity (repeated squarings) every proof; reuse the precomputed domain.trace_primitive_root instead. 2. Compute the Q primary FRI evaluation points once in step_3 and share them between the DEEP reconstruction and the FRI fold. The DEEP driver previously recomputed all 2Q (primary+symmetric) points and the fold recomputed Q more. Now: Q pow() total; each symmetric point is -primary (bit-reversed index primary+N/2, lde_root^(N/2)=-1), so negate instead of a second pow(); the fold moves the same Q points into its inverses. Byte-identical. 204 stark tests pass, clippy clean.
2084def to
1ea7876
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. |
Stacked on #829. Removes redundancies from the per-table verify path. Each runs
Ttimes for the ~100–140 un-batched sub-proofs of an ethrex proof, andverifier.rsdoubles as the recursion guest, so cycles count as well as wall-clock.Tier 0 (micro)
hash_data_from_slices+verify_merkle_path_from_leaf_hash, mirroringverify_opening_pair) instead of allocating avec![a, b]per layer per query.𝜐^(-2ⁱ)lazily and zip them into the fold, dropping the pre-collectedevaluation_point_vec.gviaget_primitive_root_of_unity(root_order)(~log₂N squarings/table) although the verifier domain already stores it astrace_primitive_root. Use that; drop the now-deadVerifierDomain::root_orderfield.Qprimary FRI points once in step 3 and reuse them for both the DEEP denominators and the FRI eval-point inverses. The symmetric point is the primary's negation (sym_index = primary + N/2,lde_root^(N/2) = −1), so no secondpowper point.Tier 1 (structural)
1/(zᴺ − 1)into the boundary-constraint batch inverse as one trailing element (~3 muls) instead of a separate extension inversion (~70 base muls) per table.verify_rounds_2_to_4(with the soundness-I3 shape validation, now inreconstruct_ood_grid) and thread it into both step 2 and step 3 instead of each rebuilding it.Tier 2 (per-query DEEP arithmetic)
Σ_col Σ_row (t_col(x) − ood[row][col])·inv_den[row]·γmultiplied the shared row denominator1/(x − z·gʳᵒʷ)in per(col,row)element. Factor it out of the column sum (Σ_row inv_den[row]·Σ_col (…)·γ): one extension multiply per row instead of per cell, ~halving the trace-term extension muls over 2·Q queries × T tables. Byte-identical (field add/mul are associative + commutative); the g·z pruning skip is preserved and thetrace_term_coeffsshape guard is strengthened to exact per-dimension equality so the row-major indexing is panic-safe.Soundness
No checks removed. The I3 OOD-shape validation still runs (moved into
reconstruct_ood_grid, returnsNone→ reject). The folded1/(zᴺ − 1)still fails closed: a zero denominator (z on a boundary step or on the trace domain) fails the batch inverse and rejects. Thesym = −primaryidentity is the same one the openings already rely on. The DEEP factoring reorders a finite-field sum/product, so it is exact.Testing
starktests pass — thetest_prove_verify_*suite generates real proofs and runs them through the fullmulti_verify_views → verify_rounds_2_to_4 → step_2/3/4path, exercising every changed line; any DEEP drift would desync the codeword from the FRI folding.cargo clippy -p starkclean; no new warnings.Considered but deferred
multi_verify_views— unsafe when tables have different trace lengths (table splitting), and structural; belongs with the batched-FRI lane.boundary_constraintsper table (counted in replay, rebuilt in step 2) — a small per-table alloc, not arithmetic; avoiding it needs a new AIR-trait count method orChallengesplumbing not justified by the saving.