Feat/skip empty tables

[jotabulacios]

Every chip used to cost a padded four-row sub-proof — a full commitment, FRI chain and
OOD opening set — even when the program never executed one of its operations. A table a
run never reaches is now left out, and each epoch decides that on its own: a table absent
from one epoch still appears in another that uses it. Computing the set over the whole run
instead would drag every table used anywhere into every epoch, which is most of what there
is to win.

The twelve chunked chips get chunk_and_generate_optional; CPU and MEMW_R stay mandatory.
The six accelerators (COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS, HINT) get counts of their
own so they can be absent too, which drops FIXED_TABLE_COUNT from 11 to 5 and takes the
statement encoding to V4. BITWISE, DECODE, KECCAK_RC, REGISTER, HALT, the PAGEs and L2G
stay always-present — they have no count for a prover to zero.

Soundness comes from the bus, not from the count check. TableCounts::validate no longer
requires a positive count on the optional tables; what rejects a proof that declares away a
table whose operations ran is the LogUp balance, which sums the contribution of every AIR
with a trace interaction and stops matching once the CPU's sends have no receiver.
validate still refuses a proof with no CPU or no register file, and the declared counts
are still cross-checked against the sub-proof count — with a checked sum, because they are
prover-supplied and a wrapped total would let one field stay large enough to size a Vec
from.

Tested in both directions:

• An unused chip is absent and the proof still verifies. A chip whose operations ran cannot
  be dropped: MUL, HINT, KECCAK_RND (dispatched by another chip rather than by the CPU),
  and COMMIT — the one table whose bus target is not zero — both on its own and together
  with the output that sets that target.
• Each of those shows the balance is what rejected it, not something else: the same proof
  is re-verified with the target moved onto the forged sum, and has to pass.
• Every droppable table is weighed on the bus across six programs and none contributes
  zero, which is the property that would let one be dropped unnoticed however many rows it
  carries.
• The epochs disagree, and one table leaves and comes back — a shape no whole-run or prefix
  scheme produces. An epoch that declares away a table it carries is rejected on both
  branches of the cross-check, and a bundle whose table set varies by epoch survives the
  recursion path. Every field of the V4 encoding is shown to move the transcript.

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

No actionable issues found in the PR diff. Reviewed statically; no builds or tests were run.

[claude]

Review: skip empty tables

Read the full diff plus the surrounding prover/verifier/bus machinery. The core design holds up. I traced the soundness argument end to end and it checks out:

• Verifier::multi_verify (crypto/stark/src/verifier.rs:1403-1423) sums table_contribution over every AIR with has_trace_interaction(), and has_trace_interaction() is a purely structural property (crypto/stark/src/lookup.rs:1055 — !interactions.is_empty()), independent of trace content. So a dropped chip whose ops actually ran leaves its counterparty's terms unmatched and the sum diverges.
• The expected_proof_count cross-check runs before VmAirs::new in both verify_with_options (prover/src/lib.rs:1393) and verify_epoch (prover/src/continuation.rs:806), so adversarial counts cannot drive an unbounded AIR allocation.
• FIXED_TABLE_COUNT: 11 -> 5 is right (bitwise, decode, keccak_rc, register, halt), and test_crafted_zero_count_proof_must_not_verify still holds with include_halt = true.
• Prover and verifier AIR orderings stay in lockstep (air_trace_pairs and air_refs both push halt before the six accelerator loops).
• padded_chunked_rows = padded_chunked_rows_optional(..).max(4) is exactly equivalent to the old function for ops_count > 0 (the per-chunk .max(4) already guaranteed >= 4).
• Domain tags correctly bumped (_V3 -> _V4, epoch _V2 -> _V3); leaving CONTINUATION_GLOBAL_TAG alone is right since the global statement carries no table counts.
• COMMIT going optional is safe: the offset is computed from the claimed public_output_bytes, so dropping the table while output was committed leaves the CPU sends unmatched.
• No non-test code still indexes the newly-optional vectors; the remaining traces.lts[0] uses in trace_builder_tests.rs are all on programs that execute SLT.

Findings (all in tests / comments — no product-code defects)

High — the test the soundness argument cites does not cover the tables it claims. every_table_participates_in_the_bus builds its AIR set from test_mul_8's own table counts. That program is 8 instructions of addi/mul/mulw + exit — no memory, no branches, no accelerators — so ~13 of the newly-droppable tables have count 0, produce no AIRs, and are never checked. TableCounts::validate's doc says this test "pins it down for the whole AIR set"; it does not. Build from an all-ones TableCounts instead. (Inline, with a secondary note that has_trace_interaction() is weaker than the property actually needed.)

Medium — negative tests can pass for the wrong reason. The new prove_and_verify helper returns false on prover error as well as verification failure, so omitting_a_table_whose_ops_ran_fails_the_bus_balance / omitting_a_used_accelerator_fails_the_bus_balance would pass even if the prover simply refused to build the reduced-shape proof — the opposite of what their doc comments assert. (Inline.)

Medium — omitting_a_used_accelerator_fails_the_bus_balance silently returns green when hint_min.elf is absent, and it is the only negative test for the accelerator direction. (Inline.)

Low — the helper is a near-verbatim copy of prove_elfs_tests::prove_and_verify_vm_minimal. Make that one pub(crate) and reuse it. (Inline.)

Low — comment split. The new continuation test lands between the two halves of test_prove_and_verify_continuation's comment, leaving a dangling "...is ~34 cycles, so" on the new test and a mid-sentence fragment on the old one. (Inline.)

Low / follow-up — KECCAK_RC is still in the fixed set. When keccak == 0 its multiplicities are all zero (keccak_rc::update_multiplicities(.., keccak_ops.len())), so it contributes nothing to the bus yet still costs a full commitment + FRI chain + OOD opening set — the same cost this PR just removed for the other six accelerators. Making it conditional on keccak_rnd > 0 would require FIXED_TABLE_COUNT to become a function of the counts, so deferring is reasonable, but it is the last always-paid table a keccak-free program does not use.

Not findings, noted for the record

• TableCounts::total() can wrap on adversarial counts before the expected_proof_count comparison. Pre-existing (14 fields -> 20 makes no material difference), and the page-config path already has its own proofs.len() cap, so no new exposure here.
• Accelerator traces now spill to disk under StorageMode::Disk where KECCAK/ECSM/ECDAS/HINT previously did not (they route through generate_chunks). That is a strict improvement — flagging it only as an intentional-looking side effect.

[github-actions]

AI Review

PR #977 · 10 changed files

Findings

Status	Sev	Location	Finding	Found by
confirmed	medium	prover/src/auto_storage.rs:108	Disk-spill RAM estimator missing optional accelerator/auxiliary tables	kimi openrouter/moonshotai/kimi-k2.7-code
confirmed	medium	prover/src/lib.rs:171	Validation relaxation shifts trust from structural checks to bus balance	nemotron openrouter/nvidia/nemotron-3-ultra-550b-a55b
uncertain	low	prover/src/tests/prove_elfs_tests.rs:150	Test helper panics on prover failure rather than returning false	kimi openrouter/moonshotai/kimi-k2.7-code

Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro).

AI-001: Disk-spill RAM estimator missing optional accelerator/auxiliary tables

• Status: confirmed
• Severity: medium
• Location: prover/src/auto_storage.rs:108
• Found by: kimi:openrouter/moonshotai/kimi-k2.7-code
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

The disk-spill peak-RAM estimator in auto_storage.rs is out of sync with the new optional table model. table_specs only accounts for CPU/MEMW/MEMW_A/MEMW_R/LOAD/LT/SHIFT/MUL/DVRM/BRANCH/COMMIT, BITWISE/DECODE/HALT/REGISTER and PAGE; it omits EQ, BYTEWISE, STORE, CPU32, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT. count_table_lengths likewise does not track row counts for those tables. Because the PR moves several accelerator tables from fixed to optional, programs that actually use them will have their memory footprint underestimated, which can cause auto_storage::decide to select StorageMode::Ram when StorageMode::Disk is required and lead to OOM during proving.

Evidence

In prover/src/auto_storage.rs, table_specs builds specs from TableLengths fields (cpu_padded_rows, memw_padded_rows, etc.) and never references eq, bytewise, store, cpu32, keccak, keccak_rnd, ecsm, ecdas or hint. In prover/src/tables/trace_builder.rs, count_table_lengths returns TableLengths which lacks those fields and only counts commit_padded_rows among the newly-optional accelerator/auxiliary tables. The comment in table_specs says 'Per-table specs in the same order as air_trace_pairs in prove', but air_trace_pairs (lib.rs) now emits commits, keccaks, keccak_rnds, ecsms, ecdases, hints, eqs, bytewises, stores and cpu32s, none of which are reflected in the RAM estimate.

Suggested fix

Extend TableLengths in trace_builder.rs/count_table_lengths to count rows for eq, bytewise, store, cpu32, keccak, keccak_rnd, ecsm, ecdas and hint (mirroring how commit_padded_rows is already tracked), then extend auto_storage.rs/table_specs to include corresponding TableSpec entries so peak_bytes accounts for every table that air_trace_pairs can produce.

AI-002: Validation relaxation shifts trust from structural checks to bus balance

• Status: confirmed
• Severity: medium
• Location: prover/src/lib.rs:171
• Found by: nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

TableCounts::validate() now only requires cpu>0 and memw_register>0, allowing all other 18 tables to have zero counts. Security for omitted tables relies entirely on LogUp bus balance checks.

Evidence

The validate() function at lines 171-181 only checks cpu and memw_register. The comment acknowledges: 'What keeps a zero count honest is the LogUp bus, not this check.' The new tests every_table_participates_in_the_bus and no_present_table_contributes_zero_to_the_bus (in skip_empty_tables_tests.rs) verify this property for current tables, but this is a significant trust model change.

Suggested fix

Consider adding a debug-only assertion or a #[cfg(debug_assertions)] check that validates all tables present in the trace have non-zero counts, to catch accidental omissions during development. The current design is intentional and tested, but the trust shift should be explicitly documented in the security model.

AI-005: Test helper panics on prover failure rather than returning false

• Status: uncertain
• Severity: low
• Location: prover/src/tests/prove_elfs_tests.rs:150
• Found by: kimi:openrouter/moonshotai/kimi-k2.7-code
• Verified by: -
• Rejected by: -

Claim

prove_and_verify_vm_minimal and weigh_the_bus now panic if the prover fails, which changes the contract of several existing negative tests. While the new helpers document that false is reserved for verifier rejection, callers that previously expected a proving failure to return false will now panic. None of the current callers appear to rely on proving failure, but the helper is pub(crate) and a future test that passes a malformed trace expecting a prover-side rejection could abort the test suite instead of failing gracefully.

Evidence

In prover/src/tests/prove_elfs_tests.rs, weigh_the_bus matches multi_prove_ram with Ok(proof) => proof and Err(e) => panic!(...). prove_and_verify_vm_minimal wraps weigh_the_bus with recheck_with_moved_target=false. All current negative tests use weigh_the_bus(..., true) after a successful honest proof and then mutate the trace, so they only exercise verifier rejection. The risk is future misuse of the pub(crate) helper.

Suggested fix

Keep the current panic behavior for weigh_the_bus (it is test-only and the distinction is valuable), but add a doc comment on the helper reminding callers that proving failures panic and that negative tests must mutate an already-proven trace.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	success	0
kimi	openrouter/moonshotai/kimi-k2.7-code	general	success	3
minimax	minimax/MiniMax-M3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
moonmath	zro/minimax-m3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
nemotron	openrouter/nvidia/nemotron-3-ultra-550b-a55b	general	success	3

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	success	2	3	1

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Discarded candidates (3) — rejected by the verifier

• Statement encoding version bumps lack explicit changelog (prover/src/statement.rs:20, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The version bumps are correct: DOMAIN_TAG V3->V4 and CONTINUATION_EPOCH_TAG V2->V3. The six new TableCounts fields ARE included in the encoding — the destructure at statement.rs lines 99-144 includes keccak, keccak_rnd, ecsm, ecdas, hint, commit, and the array absorption at lines 145-157 feeds them all into the transcript. The comment at line 19 already states 'Bump the suffix on any encoding change.' There is a new test state_depends_on_every_table_count that verifies every field reaches the transcript. This is documentation style, not a bug.
• keccak_rnd generation depends on keccak_ops structure (prover/src/tables/trace_builder.rs:3583, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The mapping from keccak_ops to keccak_rnd_ops at trace_builder.rs lines 3584-3591 is a standard iterator .map() which produces exactly one element per input element. A non-empty keccak_ops always produces a non-empty keccak_rnd_ops. Both tables use generate_optional, so both produce either 0 or 1 table. The claim itself acknowledges this is 'unlikely' and that the verifier cross-checks would catch any mismatch. This is not a real issue.
• Dynamic bus-contribution coverage relies on hard-coded program list (prover/src/tests/skip_empty_tables_tests.rs:142, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — The test at skip_empty_tables_tests.rs lines 227-233 asserts every entry in the hard-coded droppable array appears in seen. If a table in droppable becomes uncovered by any fixture program, the assertion FAILS — the test catches the regression. The only uncaught gap is when a developer adds a new droppable table to the AIR but forgets to add it to the droppable array, which is standard developer oversight for any hard-coded list. The test comment at line 224 explicitly acknowledges this: 'Coverage is the weak point of a dynamic check.' The finding's central claim — that 'a newly added table that is never exercised would not be caught' — is wrong when the developer properly adds it to droppable (the test would then fail because it's not in seen). This is not a test design flaw.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[jotabulacios]

/bench-verify

[github-actions]

⏳ 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.

[github-actions]

Verifier benchmark — 3ae8bf2018 vs main (20 pairs, monolithic + continuations)

ethrex 20-tx block · monolithic · blowup=2, 219 queries

Metric	main	PR	Δ
Verify time (ABBA, 20 pairs, per-side)	2.508s	2.525s	+0.70% 🔴
Proof size (exact, 1 reading)	102.33 MiB	102.33 MiB	+0.00% ⚪

Per-side (PR can't deserialize the baseline's proof — proof-format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.

  pairs: 20   mean A (PR): 2.525s   mean B (main): 2.508s
  [parametric] paired-t   mean +0.70%   sd 0.78%   se 0.17%
               95% CI: [+0.34%, +1.06%]   (t df=19 = 2.093)
  [robust]     median +0.80%   Wilcoxon W+=185 W-=25  p(exact)=0.0017  (z=+2.97)

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

🔴 REAL REGRESSION — PR verifies ~0.70% slower (paired-t and Wilcoxon agree).

ethrex 20-tx block · continuations, epoch 2^20 (3 epochs) · blowup=2, 219 queries

Metric	main	PR	Δ
Verify time (ABBA, 8 pairs, per-side)	3.152s	3.173s	+0.65% 🔴
Proof size (exact, 1 reading)	177.07 MiB	166.28 MiB	-6.10% 🟢

Per-side (PR can't deserialize the baseline's proof — proof-format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.

  pairs: 8   mean A (PR): 3.173s   mean B (main): 3.152s
  [parametric] paired-t   mean +0.65%   sd 0.54%   se 0.19%
               95% CI: [+0.20%, +1.11%]   (t df=7 = 2.365)
  [robust]     median +0.53%   Wilcoxon W+=36 W-=0  p(exact)=0.0078  (z=+2.45)

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

🔴 REAL REGRESSION — PR verifies ~0.65% 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	32.1M	3.7M	-28.5M (-88.63%)
Keccak calls	3029	1109	-1920

  baseline  origin/main  99d7567afe  guest=recursion-min.elf
  PR        3ae8bf2018e37b483349dfe5a89935a5dae698fc  3ae8bf2018  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=99d7567afec95c672e78065bc2bacb4416fb7577 ref_b_elf=recursion-min.elf ref_b_cycles=32137866 ref_b_keccak=3029 ref_b_execute_wall_s=1
ref_a_sha=3ae8bf2018e37b483349dfe5a89935a5dae698fc ref_a_elf=recursion-min.elf ref_a_cycles=3652699 ref_a_keccak=1109 ref_a_execute_wall_s=0
delta_cycles=-28485167 delta_keccak=-1920

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	1910.0M	1690.7M	-219.2M (-11.48%)
Keccak calls	3296811	3213617	-83194

  baseline  origin/main  99d7567afe  guest=recursion-cont-blowup2.elf
  PR        3ae8bf2018e37b483349dfe5a89935a5dae698fc  3ae8bf2018  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=99d7567afec95c672e78065bc2bacb4416fb7577 ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=1909967824 ref_b_keccak=3296811 ref_b_execute_wall_s=31
ref_a_sha=3ae8bf2018e37b483349dfe5a89935a5dae698fc ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=1690738371 ref_a_keccak=3213617 ref_a_execute_wall_s=26
delta_cycles=-219229453 delta_keccak=-83194

[jotabulacios]

/bench

[github-actions]

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

_{continuations · epoch 2^22 · 8 epochs}

Metric	main	PR	Δ
Peak heap	46886 MB	47467 MB	+581 MB (+1.2%) ⚪
Prove time	110.675s	110.190s	-0.485s (-0.4%) ⚪

✅ No significant change.

_{Prove-time spread 0.7% (110.012s / 110.792s / 110.190s)}

_{Commit: 3ae8bf2 · Baseline: cached · Runner: self-hosted bench}

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

No actionable issues found in the PR diff. Reviewed statically; no builds or tests were run.

[jotabulacios]

/bench

[jotabulacios]

/bench-verify

[github-actions]

⏳ 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.