[nicole-graus]

Motivation

HALT's pc column is unconstrained. A prover can set it to 1, so HALT's consume and emit of the PC token cancel each other. The real next_pc of the exit ecall is then left free on the memory bus, more CPU rows can execute after the exit, and the chain closes through REGISTER's final token, which nothing checks. For example, a program that calls exit(1) can be proven as exit(0). This affects both monolithic and continuation proofs.

Description

• The verifier now fixes the final register file (REGISTER FINI, now preprocessed) to the halted state: x1-x31 = 0, x254 = committed bytes, PC = 1 (register::halted_fini). Real rows never write next_pc = 1, so the PC chain can only end through HALT.
• Monolithic: REGISTER preprocesses OFFSET, INIT and FINI, the same layout continuations already used. The old two-column layout is removed.
• Continuations: the verifier requires the final epoch's reg_fini to equal the halted state.
• PoCs: halt_pc_forgery_poc (monolithic) and halt_continuation_poc (continuations). The attack verifies on main and is rejected here.

[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	47797 MB	+643 MB (+1.4%) ⚪
Prove time	101.862s	102.077s	+0.215s (+0.2%) ⚪

✅ No significant change.

_{Prove-time spread 0.7% (102.521s / 102.077s / 101.832s)}

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

[nicole-graus]

/ai-review

[github-actions]

Codex Code Review

No actionable issues found in the PR changes. The final-register commitments and continuation checks are consistent with HALT trace generation and cumulative output counts.

Reviewed statically; no builds or tests run.

[claude]

Review

I found no blocking issues. The fix closes the hole the PR describes, and I checked the soundness argument it relies on.

What I checked

• The final PC can only be 1 through HALT: only CPU and HALT put tokens on the x255 (addr 510/511) address. CPU next_pc is either pc + 4 (pc is even, by induction from the even entry point and even epoch INITs) or comes from BRANCH, which masks the low bit with 0xFE, so it stays even. With FINI pinned to pc = 1, the last post-exit next_pc has nowhere to land. Both new negative tests check this (with and without the forged FINI).
• The halted state matches an honest run: HALT zeroizes x1–x9 and x11–x31 and reads x10 as 0. x0 is never written. The PC high word is 0. x254 is the running commit index, carried across epochs through reg_fini, so public_output.len() + epoch_public_output.len() in the final epoch is the right total.
• u32 bounds: the verifier rejects outputs longer than u32::MAX without panicking (Ok(false) / Ok(None)). The prover-side expect can't fire, because trace build already panics on a commit count over u32.
• Removed parameters: every VmAirs::new caller is updated in the diff. Nothing else uses the removed compute_precomputed_commitment or preprocessed_commitment.

Minor

• Low: the _WITH_FINI names are now redundant (see the inline comment).
• Low / defense in depth: soundness now depends on the invariant "no row ever writes next_pc = 1". It's documented on halted_fini. A short note next to the BRANCH LSB mask (and the CPU pc + 4 path) pointing back to it would stop a future change, such as compressed instructions or a new PC-writing table, from quietly breaking it.
• The final PC timestamp is still prover-chosen, which differs from halt.typ. That's documented and fine given the argument above.

The extra commitment work per prove/verify is negligible: an LDE plus a Merkle tree over 128 rows.

[github-actions]

AI Review

PR #1020 · 15 changed files

Findings

Status	Sev	Location	Finding	Found by
confirmed	low	prover/src/lib.rs:1342	Prover panics when public output exceeds u32	kimi openrouter/moonshotai/kimi-k2.7-code

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

AI-001: Prover panics when public output exceeds u32

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

Claim

The monolithic prover uses expect when converting traces.public_output_bytes.len() to u32, which panics if the public output is larger than u32::MAX. The corresponding verifier path returns Ok(false), so the prover should return an error instead of panicking for consistency and robustness.

Evidence

In prove_with_options_and_inputs the code adds: let committed_bytes = u32::try_from(traces.public_output_bytes.len()).expect("trace build bounds the commit index to u32");. In contrast, verify_proof_parts handles the same conversion with let Ok(committed_bytes) = u32::try_from(public_output.len()) else { return Ok(false); };.

Suggested fix

Replace the expect with a proper error return, e.g., u32::try_from(traces.public_output_bytes.len()).map_err(|_| Error::Execution("public output exceeds u32 commit index bound".to_string()))?.

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	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	1	0	0

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

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