perf(verifier): compute shared LogUp α-powers once, slice per table#842
perf(verifier): compute shared LogUp α-powers once, slice per table#842diegokingston wants to merge 1 commit into
Conversation
step_2 rebuilt [1, α, α², …] (α-powers up to the table's bus width) once per table via compute_alpha_powers, even though the LogUp α challenge is a single value sampled once in multi_verify_views and shared across every table. Each table's power vector is just a prefix of the same geometric sequence. Compute the sequence ONCE after sampling the shared challenges — to the global-max bus width across all AIRs — and slice each table's prefix in step_2. Saves (Σ_tables max_bus_elements − max_bus_elements) ext-field multiplications and N−1 heap allocations per proof (allocations = proven memory-table writes in the recursion guest). Byte-identical: the sliced prefix equals what each table computed before. 204 stark tests pass, clippy clean, prover builds.
|
/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.587s | 3.583s | -0.09% ⚪ |
| Proof size | 204.30 MiB | 204.30 MiB | +0.00% ⚪ |
pairs: 20 mean A (PR): 3.583s mean B (main): 3.587s
[parametric] paired-t mean -0.09% sd 0.80% se 0.18%
95% CI: [-0.47%, +0.28%] (t df=19 = 2.093)
[robust] median -0.10% Wilcoxon W+=49 W-=161 p(exact)=0.0362 (z=-2.07)
run-to-run jitter: A CV 0.66% B CV 0.47% (lower = steadier)
within-session drift: +0.13% over the run, 1st->2nd half +0.16%
⚪ BORDERLINE — parametric and robust disagree; suspect outlier pair(s). Trust the median (-0.10%); add pairs.
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) a4b3aaa a4b3aaa guest=recursion-min.elf
| Metric | REF_B (baseline) | REF_A (PR) | Δ (A-B) |
|---|---|---|---|
| Guest cycles | 43.6M | 38.2M | -5.4M (-12.44%) |
| 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=a4b3aaacf09c154bf4a20995d599c537b2c83153 ref_a_elf=recursion-min.elf ref_a_cycles=38182244 ref_a_keccak=3025 ref_a_execute_wall_s=2
delta_cycles=-5426706 delta_keccak=0
Stacked on #830.
What
step_2_verify_claimed_composition_polynomialrebuilt the LogUp α-power vector[1, α, α², …](up to the table's bus width) once per table viacompute_alpha_powers, even though the LogUp α challenge is a single value sampled once inmulti_verify_views(Round 1 Phase B) and shared across every table. Each table's vector is just a prefix of the same geometric sequence.This computes the sequence once, right after sampling the shared challenges, to the global-max bus width across all AIRs, and each table's
step_2slices the prefix it needs.Why
The verifier doubles as the serial recursion guest, so per-table recompute costs real cycles:
(Σ_tables max_bus_elements − max_t max_bus_elements)extension-field multiplications per proof (E×E ≈ 9 base muls each).N−1heap allocations per proof — each heap alloc is a proven memory-table write in the guest.Correctness
Byte-identical: the sliced prefix
&shared_alpha_powers[..air.max_bus_elements()]equals the vector each table computed before. When the proof carries LogUp challenges,shared_alpha_powers.len()is the global max, so every table's slice is in range; otherwise both old and new paths yield an empty slice. Comment atlookup.rs:96documents that α must be shared across all AIRs.Testing