fix(proof): assert derived block matches claim after derivation

[mw2000]

Closes GHSA-5jh4-3p33-85xc. advance_to_target silently downgrades the local target on EndOfSource, allowing an adversary to bind a valid output root to a future block number. Add a postcondition in WitnessExecutor::run() that rejects execution when the derived safe head block number differs from the claimed L2 block number.

Includes a gated exploit-regression integration test (RUN_GHSA_EXPLOIT_REGRESSION=1) reproducing the attack shape.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

1 Skipped Deployment

Project	Deployment	Actions	Updated (UTC)
base	Ignored	Preview	May 8, 2026 8:53pm

[cb-heimdall]

🟡 Heimdall Review Status

Requirement	Status	More Info
Reviews	🟡 0/1	Denominator calculation Show calculation 1 if user is bot 0 1 if user is external 0 2 if repo is sensitive 0 From .codeflow.yml 1 Additional review requirements Show calculation Max 0 0 From CODEOWNERS 0 Global minimum 0 Max 1 1 1 if commit is unverified 1 Sum 2

[mw2000]

This is a port of succinctlabs/op-succinct#899

[linear]

CHAIN-4349

Approved review 4252328856 from jackchuma is now dismissed due to new commit. Re-request for approval.

[github-actions]

Review Summary

Security fix for GHSA-5jh4-3p33-85xc — the advance_to_target function silently downgrades the derivation target on EndOfSource, allowing a crafted witness to bind a valid output root to a future block number. The postcondition check in WitnessExecutor::run() rejects this by comparing the derived safe-head block number against the claimed block number.

What this PR does

1. Refactors the existing block-number validation at the end of WitnessExecutor::run() from an inline if block into a named ensure_derived_block_matches_claim function with a structured error message containing parseable labels.
2. Rebuilds the range ELF (updated hash in manifest.toml) so the embedded guest binary includes the updated error message.
3. Adds a gated exploit-regression integration test that mutates an honest witness to reproduce the GHSA attack shape, then asserts the postcondition rejects it with the correct error.

Assessment

The fix is correct. The error propagation chain is sound: ensure_derived_block_matches_claim → ? → Err returned from run() → .unwrap() in run_range_program() → panic in zkVM guest → non-zero exit code → proof rejected.

The regression test is well-constructed: properly gated with #[ignore] + #[cfg(unix)], uses anyhow::bail! for missing env vars, and carefully validates that the postcondition (not some other check) is what rejects the exploit.

No new issues found. The changes are minimal, focused, and correct.

Note on previous bot comments: The 5 inline comments from an earlier review run are all based on a misreading of the diff — they claim the old inline check was preserved alongside the new function, creating dead code. In fact, the diff clearly shows the old check was removed (lines prefixed with -) and replaced by the new ensure_derived_block_matches_claim call. Those comments should be disregarded.

[mw2000]

The core issue was fixed by #2581. This main value add of this PR now is just the regression test