[nicole-graus]

Motivation

Several AIR tables leave their multiplicity column μ unconstrained. Since μ lives in the field, it can be set to −1, which flips a row's role on the bus: it starts receiving its range checks instead of sending them. This is exploitable: the bugs were proven end-to-end by a test where the verifier accepts a false statement against an unmodified ELF.

Description

Follows the spec in #1017. Two fix shapes, by whether the table deduplicates rows:

1. Dedup tables (LT, BYTEWISE, MUL, DVRM, BRANCH): bound μ ∈ [0, 256) with an IS_BYTE check sent with multiplicity 1, so no ARE_BYTES sender carries a negative weight:

• LT, BYTEWISE: ARE_BYTES[μ, 0].

• MUL, DVRM: one batched ARE_BYTES[μ_a, μ_b].

• BRANCH: one batched ARE_BYTES[μ, next_pc_low_1]. next_pc_low_1 was previously sent with weight μ, which let two BRANCH rows (μ = −2, μ = −1) cancel the bound of a forged LT row (branch_carrier_poc).

• Rows whose count exceeds 255 are split (types::dedup_rows, and dedup_mul_rows/dedup_dvrm_rows for the two-count tables). The BITWISE collectors count one lookup per row, padding rows included (ARE_BYTES[0, 0]).

• Feat/skip empty tables #977 guard: no_optional_table_uses_a_constant_multiplicity now allows Multiplicity::One only on ARE_BYTES sends whose values vanish on padding rows (a byte check on zero values is harmless). Every other bus still requires an empty table to send nothing.

2. Non-dedup tables (SHIFT, LOAD, EQ, KECCAK, KECCAK_RND): bit-constrain μ (μ·(1−μ) = 0, plus zbs for SHIFT), and force is_negative = 0 on unsigned SHIFT rows.

• SHIFT: IS_BYTE[shift[0]] and IS_BYTE[shift[1]] are batched into one ARE_BYTES[shift[0], shift[1]] with multiplicity 1, as in the spec.

• EQ no longer deduplicates rows (one row per op, μ is a bit, as in the spec).

• KECCAK_RND: its byte checks now use multiplicity 1 as in the spec, and padding is counted in the collector. The Cxz_right IS_BIT is no longer gated by μ, which lowers the table's max degree from 3 to 2.

[nicole-graus]

/bench

[github-actions]

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

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

Metric	main	PR	Δ
Peak heap	47154 MB	47177 MB	+23 MB (+0.0%) ⚪
Prove time	101.862s	103.421s	+1.559s (+1.5%) ⚪

✅ No significant change.

_{Prove-time spread 0.6% (103.778s / 103.149s / 103.421s)}

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

[nicole-graus]

/bench

[nicole-graus]

/bench

[nicole-graus]

/ai-review

[github-actions]

Codex Code Review

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

[claude]

Review summary

The fix looks sound. I checked these points and found no problems:

• Bounds: IS_BYTE[μ] sent with multiplicity 1 keeps μ in [0, 256), so no ARE_BYTES sender has a negative weight anymore. BRANCH's next_pc_low_1 no longer being weighted by μ closes the cross-table cycle.
• Collectors match the traces: the BITWISE collectors use the same chunks(max_rows) → dedup_*_rows → next_power_of_two().max(4) path as chunk_and_generate_optional. HashMap order doesn't affect the counts. Empty optional tables produce no chunks, so the collectors count no padding for them.
• KECCAK_RND padding: padding_are_bytes matches generate_keccak_rnd_trace, which builds a single unchunked table of 24·n rows padded to a power of two.
• New constraints on padding rows: SHIFT's zbs/MuIsBit/(1−signed)·is_negative, MuIsBit on LOAD/EQ/KECCAK/KECCAK_RND, and the now-unconditional Cxz_right IS_BIT all hold on all-zero padding rows.
• Splitting: dedup_*_rows never produces more rows than the raw chunk length, so splitting at 255 can't overflow an instance.

Notes (Low / readability)

1. Duplicated test scaffolding (~2.2k lines). branch_carrier_poc, branch_multiplicity_poc, lt_multiplicity_poc and mul_mu_carrier_poc each re-define almost the same helpers: eval_mult (4 copies), lookup_air/mock, lookup_trace/mock_trace, a *_net bus tally and prove_and_verify. lt_multiplicity_poc already makes some of them pub(crate). Moving them into one shared module would make the PoCs much shorter and easier to maintain. Some PoCs also overlap with the new per-table *_bounds_its_multiplicity and *_match_collector tests, so consider whether every PoC needs to stay.
2. Copied dedup logic. dedup_lt_rows, dedup_branch_rows and dedup_bytewise_rows have the same body: count, then split at MU_MAX. The four MU_MAX = 255 constants are also the same value. One generic helper (for example split_counts<T: Hash + Eq + Clone>(ops) -> Vec<(T, u64)>) and a single shared constant would remove the duplication. MUL and DVRM could split their pairs with the same helper.
3. Performance (EQ): EQ no longer deduplicates, so the table now grows with the number of executed EQ ops rather than the number of unique ones. A hot loop running the same compare now adds one row per iteration. This follows the spec, but it's a real increase in trace size, so it's worth benchmarking. If it matters, the LT approach (dedup plus the IS_BYTE[μ] bound) would also work for EQ.
4. Nits:
   • The rewritten comment block in build_traces (near "LT/MUL/DVRM/BRANCH/BYTEWISE count their per-row lookups") has one very long line; please re-wrap it.
   • In branch.rs, the bus_interactions doc now says next_pc_high[0..2] while the module header still says next_pc_high[0..3]. Please pick one range notation for both.

I left one inline comment, on the #977 guard exemption.

[github-actions]

AI Review

PR #1016 · 36 changed files

Warning: the diff was truncated before review.

Findings

Status	Sev	Location	Finding	Found by
uncertain	low	prover/src/tables/mod.rs:79	Stale bus-interaction counts in MaxRowsConfig comment table	glm openrouter/z-ai/glm-5.2

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

AI-002: Stale bus-interaction counts in MaxRowsConfig comment table

• Status: uncertain
• Severity: low
• Location: prover/src/tables/mod.rs:79
• Found by: glm:openrouter/z-ai/glm-5.2
• Verified by: -
• Rejected by: -

Claim

The comment table listing per-table bus-interaction counts and effective widths is now stale for tables whose bus interactions changed in this PR: LT went from 9→10, DVRM from 34→35, and SHIFT from 18→17 interactions, but the comment still lists the old values (9, 34, and 15 respectively).

Evidence

The mod.rs comment table (lines 71-93) lists 'LT | 15 | 9 | 42', 'DVRM | 34 | 34 | 136', and 'SHIFT | 27 | 15 | 72'. The actual bus_interactions() counts are now 10 for LT (added ARE_BYTES[μ,0]), 35 for DVRM (added ARE_BYTES[μ_q,μ_r]), and 17 for SHIFT (merged two ARE_BYTES into one). The eff-width column (main + 3×bus) is correspondingly wrong. The max_rows constants are hardcoded and not derived from this comment, so there is no functional impact, but the documentation is misleading for anyone sizing new tables from the formula.

Suggested fix

Update the comment table to reflect the new bus-interaction counts: LT→10, DVRM→35, SHIFT→17 (and recompute effective widths).

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	success	1
kimi	openrouter/moonshotai/kimi-k2.7-code	general	success	1
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	0

Verification Lanes

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

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

Discarded candidates (1) — rejected by the verifier

• BRANCH doc comment uses wrong halfword index range (prover/src/tables/branch.rs:27, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — The comment says 'IS_HALFWORD (×3 for next_pc_high[0..2])'. The ×3 explicitly declares three lookups, so there is no ambiguity. The [0..2] uses column-index notation matching the column names NEXT_PC_HIGH_0, NEXT_PC_HIGH_1, NEXT_PC_HIGH_2 — not Rust range syntax. This is a documentation nitpick with zero functional impact; no actual confusion is likely given the ×3 count right next to it.

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