Fix(prover): fix issues blocking Rust std program verification

[ColoCarletti]

Summary

• Fix SRL producing arithmetic-shift output when input MSB is set (Bus 13 imbalance)
• Fix CSR instructions missing PC-update on Memw bus (Bus 14 imbalance)
• Fix W-suffix instructions truncating 64-bit register values in executor Log (Bus 16 imbalance)
• Remove stray print_string calls that emitted orphan Print ecalls (Bus 19 imbalance)

These four issues combined made it impossible to prove any Rust std program. After this PR, allocator.elf, commit_sum.elf, and ethrex.elf all verify correctly.

Changes

SRL extension gating (prover/src/tables/shift.rs)

compute_aux() set is_negative = MSB(in[3]) regardless of the signed flag. For logical right shift (SRL, signed=0), this filled the output with 1s instead of 0s when the input's
top bit was set — producing arithmetic-shift output. The SHIFT trace disagreed with the CPU trace, imbalancing Bus 13.

The spec's SHIFT-C13 constraint (MSB16[is_negative; in[3]]) is gated by signed, leaving is_negative unconstrained for SRL. The fix sets is_negative = self.signed && MSB(in[3]),
which is the only value that produces correct SRL output.

CSR instruction decoding (prover/src/tables/types.rs)

DecodeEntry::from(Instruction::CSR) left all ALU flags at zero. This made pad = 1, so CM54's multiplicity was 0 — the CPU never sent PC-update tokens for CSR rows. But MEMW_R
unconditionally generated PC rows, creating orphan receivers on Bus 14.

The fix sets op_add = true, mirroring the existing Instruction::Fence treatment (no-op as ADDI x0, x0, 0). CSR instructions appear in Rust std programs because the toolchain
injects csrrci x10, mstatus, 0 during startup.

W-suffix register value truncation (executor/src/vm/instruction/execution.rs)

ArithImmW and ArithRegW stored the truncated 32-bit value in Log.src1_val/src2_val:

// Before:
let op1 = registers.read(src)? as i32;   // truncates to 32 bits
src1_val: op1 as u64,                     // upper 32 bits lost

// After:
let raw_src = registers.read(src)?;       // full 64 bits preserved
let op1 = raw_src as i32;                // truncate only for ALU
src1_val: raw_src,                        // full value in Log

The prover uses src1_val as the register value for the MEMW_R Memory bus chain. When the upper 32 bits were lost, the chain broke for any register holding a 64-bit value accessed by a
W-suffix instruction. This only manifested in programs that put large values in registers (e.g., ethrex's hash computations).

Stray Print ecall removal (syscalls/)

sys_halt() and sys_getenv() called print_string(), emitting Print ecalls (#1) that have no receiver on the Ecall bus. Every Rust std program hit this on every execution, imbalancing Bus
19.

[github-actions]

Codex Code Review

No actionable issues found in the PR diff.

I reviewed the changed hunks for security (VM/prover semantics, syscall behavior, Rust unsafe/asm), correctness, and significant performance risks, and didn’t find regressions or vulnerabilities introduced by these changes.

Residual risk: I did not run the test suite in this review pass.

[claude]

Review

Four targeted, well-described fixes. The root-cause analysis in the PR description is accurate and matches the diffs.

What's correct

• SRL fix (shift.rs): Gating is_negative by self.signed is the minimal correct change. The explanation of SHIFT-C14 being unconstrained for signed=0 makes this unambiguous.
• CSR fix (types.rs): Setting op_add = true to mirror Fence is consistent with the executor returning dst_val: 0 for all CSR instructions. Correct for the toolchain-injected csrrci x10, mstatus, 0 no-op.
• W-suffix fix (execution.rs): Splitting raw_src from op1 is the right pattern — truncation only for the ALU, full width for the Log.
• Stray ecall removal (syscalls/): Clean removal; the comments explaining why print_string can't be called here are the right thing to leave behind.

Issues found

Three low-severity issues, all in new test/example code — the core fixes are clean:

1. [Low — Fragile test] prove_elfs_tests.rs — .unwrap() on pre-built ELF artifact reads will panic with a cryptic message when artifacts are absent. See inline.
2. [Low — Technically UB] pure_commit/src/main.rs — a0 is clobbered by the ecall but not declared as inlateout in the asm block. No practical consequence since the function is -> ! and the return is never read, but worth fixing. See inline.
3. [Low — Latent risk] types.rs — CSR-as-no-op is consistent with the executor, but a // TODO noting that only no-op CSR forms are safe would prevent a future contributor from unknowingly relying on CSR reads returning real values. See inline.

[github-actions]

Benchmark Results for modified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head hashmap	136.2 ± 6.6	129.3	150.4	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head keccak	132.5 ± 11.8	124.5	163.2	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head syscall_commit	93.5 ± 0.8	92.3	94.8	1.00

[github-actions]

Benchmark Results for unmodified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base binary_search	60.2 ± 3.5	58.4	70.1	1.00
head binary_search	63.0 ± 9.7	59.0	90.2	1.05 ± 0.17

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	59.5 ± 0.6	58.8	60.6	1.01 ± 0.01
head bitwise_ops	59.2 ± 0.5	58.8	60.6	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	63.3 ± 0.7	62.6	65.1	1.00
head fibonacci_26	64.1 ± 1.1	62.9	66.3	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	63.9 ± 1.0	63.0	66.2	1.00
head matrix_multiply	64.3 ± 1.8	62.4	69.1	1.01 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	59.5 ± 0.8	58.7	61.6	1.00 ± 0.02
head modular_exp	59.3 ± 0.4	58.5	59.9	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	63.1 ± 1.0	62.1	65.4	1.00
head quicksort	70.3 ± 17.3	61.8	114.4	1.12 ± 0.27

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	64.9 ± 0.3	64.5	65.4	1.00
head sieve	65.8 ± 1.2	64.5	68.8	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	73.8 ± 0.5	72.9	74.5	1.00
head sum_array	74.3 ± 0.3	73.7	74.8	1.01 ± 0.01

[ColoCarletti]

/bench

[github-actions]

Benchmark — fib_iterative_8M (median of 3)

_{Table parallelism: 32 (auto = cores / 3)}

Metric	main	PR	Δ
Peak heap	69446 MB	66890 MB	-2556 MB (-3.7%) ⚪
Prove time	33.966s	33.874s	-0.092s (-0.3%) ⚪

✅ No significant change.

✅ Low variance (time: 1.9%, heap: 2.8%)

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