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

* fix executor bugs

* fix coments

Author: ColoCarletti

executor/programs/asm/test_wsuffix_64bit.s

@@ -0,0 +1,36 @@
+	.attribute	5, "rv64i2p1"
+	.globl	main
+main:
+	# Exercises W-suffix instructions (ADDIW, SRLIW) on a register holding
+	# a 64-bit value with non-zero upper 32 bits. The executor's Log must
+	# store the full 64-bit register value in src1_val/src2_val so the
+	# prover's MEMW_R Memory bus chain stays consistent.
+
+	# Load a 64-bit value with non-zero hi32 into a0 (x10).
+	# 0xDEADBEEF_12345678
+	li	t0, 0xDEADBEEF		# t0 = 0xDEADBEEF (sign-extended)
+	slli	t0, t0, 32		# t0 = 0xDEADBEEF_00000000
+	li	t1, 0x12345678
+	or	a0, t0, t1		# a0 = 0xDEADBEEF_12345678
+
+	# Execute ADDIW on a0 — reads a0 (64-bit) but operates on lower 32.
+	# If src1_val is truncated to 32 bits, the upper 0xDEADBEEF is lost and
+	# the prover's MEMW_R chain for x10 word 1 won't balance.
+	addiw	t2, a0, 1		# t2 = sign_extend32(0x12345678 + 1) = 0x12345679
+
+	# Execute SRLIW — another W-suffix that reads a0.
+	srliw	t3, a0, 4		# t3 = sign_extend32(0x12345678 >> 4) = 0x01234567
+
+	# Commit 8 bytes of a0 (the original 64-bit value should be intact).
+	# a0 was never written by ADDIW/SRLIW (they write t2/t3, not a0).
+	addi	a1, sp, -8		# buf on stack
+	sd	a0, 0(a1)		# store a0 to buf
+	li	a0, 1			# fd = 1
+	li	a2, 8			# count = 8
+	li	a7, 64			# Commit
+	ecall
+
+	# Halt
+	li	a0, 0
+	li	a7, 93
+	ecall

executor/programs/rust/pure_commit/.cargo/config.toml

@@ -0,0 +1,6 @@
+[target.riscv64im-lambda-vm-elf]
+rustflags = [
+  "-C", "link-arg=-e",
+  "-C", "link-arg=main",
+  "-C", "passes=lower-atomic"
+]

executor/programs/rust/pure_commit/Cargo.toml

@@ -0,0 +1,8 @@
+[workspace]
+
+[package]
+name = "pure_commit"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

executor/programs/rust/pure_commit/src/main.rs

@@ -0,0 +1,39 @@
+// Minimal Rust guest program: no_std, no_main, no allocator, no syscalls crate.
+// Uses only raw inline `asm!("ecall")` for Commit (64) and Halt (93).
+// Serves as a control case in the prover test suite (`test_pure_commit_rust`):
+// verifies that Rust can compile to a provable ELF when the heap allocator is
+// bypassed, independent of the Rust-std startup path.
+#![no_std]
+#![no_main]
+
+use core::arch::asm;
+use core::panic::PanicInfo;
+
+#[panic_handler]
+fn panic(_info: &PanicInfo) -> ! {
+    loop {}
+}
+
+#[unsafe(export_name = "main")]
+pub extern "C" fn main() -> ! {
+    // Commit 4 bytes [0xAA, 0xBB, 0xCC, 0xDD]
+    let buf: [u8; 4] = [0xAA, 0xBB, 0xCC, 0xDD];
+    unsafe {
+        asm!(
+            "ecall",
+            inlateout("a0") 1usize => _, // fd = stdout; ecall overwrites a0
+            in("a1") buf.as_ptr(),
+            in("a2") 4usize,
+            in("a7") 64usize,            // Commit
+        );
+    }
+    // Halt
+    unsafe {
+        asm!(
+            "ecall",
+            inlateout("a0") 0usize => _, // exit_code = 0; ecall overwrites a0
+            in("a7") 93usize,            // Halt
+        );
+    }
+    loop {}
+}

executor/src/vm/instruction/execution.rs

@@ -66,8 +66,12 @@ impl Instruction {
                 }
             }
             Instruction::ArithImmW { dst, src, imm, op } => {
-                // W-suffix: operate on lower 32 bits, sign-extend result to 64 bits
-                let op1 = registers.read(src)? as i32;
+                // W-suffix: operate on lower 32 bits, sign-extend result to 64 bits.
+                // Log must store the RAW register value in src1_val (full 64 bits)
+                // for the prover's MEMW register chain. The truncation to i32 is only
+                // for the ALU computation.
+                let raw_src = registers.read(src)?;
+                let op1 = raw_src as i32;
                 if matches!(op, ArithOp::Sub) {
                     return Err(ExecutionError::SubImmNotSupported);
                 }
@@ -77,7 +81,7 @@ impl Instruction {
                 Log {
                     current_pc: pc,
                     next_pc: pc.wrapping_add(REGULAR_PC_UPDATE),
-                    src1_val: op1 as u64,
+                    src1_val: raw_src,
                     src2_val: 0,
                     dst_val: res,
                 }
@@ -247,17 +251,21 @@ impl Instruction {
                 src2,
                 op,
             } => {
-                // W-suffix: operate on lower 32 bits, sign-extend result to 64 bits
-                let a = registers.read(src1)? as i32;
-                let b = registers.read(src2)? as i32;
+                // W-suffix: operate on lower 32 bits, sign-extend result to 64 bits.
+                // Log must store RAW register values (full 64 bits) for the prover's
+                // MEMW register chain. Truncation to i32 is only for ALU computation.
+                let raw_src1 = registers.read(src1)?;
+                let raw_src2 = registers.read(src2)?;
+                let a = raw_src1 as i32;
+                let b = raw_src2 as i32;
                 let res32 = op.apply_word(a, b)?;
                 let res = res32 as i64 as u64; // Sign-extend to 64 bits
                 registers.write(dst, res)?;
                 Log {
                     current_pc: pc,
                     next_pc: pc.wrapping_add(REGULAR_PC_UPDATE),
-                    src1_val: a as u64,
-                    src2_val: b as u64,
+                    src1_val: raw_src1,
+                    src2_val: raw_src2,
                     dst_val: res,
                 }
             }

prover/src/tables/shift.rs

@@ -181,8 +181,14 @@ impl ShiftOperation {
         let left = !self.direction;
         let right = self.direction;
 
-        // is_negative = MSB of in[3]
-        let is_negative = (self.in_halves[3] >> 15) & 1 == 1;
+        // is_negative is the MSB of in[3] BUT gated by `signed`. The SHIFT
+        // AIR constrains IS_NEGATIVE via the MSB16 bus (SHIFT-C14) only when
+        // `signed = 1` — for `signed = 0` IS_NEGATIVE is free, so we set it
+        // to zero. This makes `extension = 65535 * is_negative = 0` for SRL,
+        // so the extension contribution in `compute_shifted_half` naturally
+        // vanishes (zero fill) — matching RISC-V SRL semantics regardless of
+        // the top-bit value of the input.
+        let is_negative = self.signed && (self.in_halves[3] >> 15) & 1 == 1;
         let extension: u16 = if is_negative { 0xFFFF } else { 0 };
 
         // bit_shift

prover/src/tables/types.rs

@@ -668,7 +668,13 @@ impl DecodeEntry {
             }
 
             Instruction::CSR { .. } => {
-                // CSR instructions not yet supported in prover
+                // CSR instructions are executed as no-ops by the VM (see
+                // executor Instruction::CSR arm returning dst_val: 0,
+                // src1/2_val: 0). Mirror that here by treating them as
+                // `ADDI x0, x0, 0` — same pattern as `Fence`. This sets
+                // `op_add=true` so CM54's multiplicity is non-zero and the
+                // CPU's PC-update Memw sender fires.
+                entry.op_add = true;
             }
 
             Instruction::EcallEbreak => {

prover/src/tests/prove_elfs_tests.rs

@@ -1899,6 +1899,57 @@ fn test_verify_rejects_inflated_table_counts() {
     );
 }
 
+/// Proves a program that uses W-suffix instructions (ADDIW, SRLIW) on a
+/// register holding a 64-bit value with non-zero upper 32 bits.
+/// Verifies that the full 64-bit value is preserved in the MEMW_R chain.
+#[test]
+fn test_prove_wsuffix_64bit() {
+    let elf_bytes = crate::test_utils::asm_elf_bytes("test_wsuffix_64bit");
+    let result = crate::prove_and_verify(&elf_bytes).expect("prove_and_verify failed");
+    assert!(result, "W-suffix 64-bit register test should verify");
+}
+
+/// Proves a minimal Rust std program that uses `init_allocator()` and
+/// `String::from("Hello World") + commit`. Exercises the full Rust-std stack:
+/// TLSF heap init (SRL on high-bit values), CSR instructions injected by
+/// the Rust toolchain, and the allocator's memory access patterns.
+#[test]
+fn test_prove_allocator_minimal_reproducer() {
+    let _ = env_logger::builder().is_test(true).try_init();
+    let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .unwrap()
+        .to_path_buf();
+    let elf_bytes =
+        std::fs::read(workspace_root.join("executor/program_artifacts/rust/allocator.elf"))
+            .expect("allocator.elf not found — run `make compile-programs-rust`");
+    let proof = crate::prove(&elf_bytes).expect("prove should succeed");
+    assert!(
+        crate::verify(&proof, &elf_bytes).expect("verify should not error"),
+        "allocator.elf should verify"
+    );
+    assert_eq!(proof.public_output, b"Hello World");
+}
+
+/// Minimal Rust program that proves: no_std, no_main, no allocator, no
+/// syscalls crate. Only Commit + Halt ecalls (both have receivers).
+#[test]
+fn test_pure_commit_rust() {
+    let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .unwrap()
+        .to_path_buf();
+    let elf_bytes =
+        std::fs::read(workspace_root.join("executor/program_artifacts/rust/pure_commit.elf"))
+            .expect("pure_commit.elf not found — run `make compile-programs-rust`");
+    let proof = crate::prove(&elf_bytes).expect("prove should succeed");
+    assert!(
+        crate::verify(&proof, &elf_bytes).expect("verify should not error"),
+        "pure_commit.elf should verify"
+    );
+    assert_eq!(proof.public_output, vec![0xAA, 0xBB, 0xCC, 0xDD]);
+}
+
 /// Regression test: addiw with negative immediate must verify.
 /// arg2_sign_bit is the sign bit of rv2 (bit 31), not of arg2, per spec
 /// constraint CPU-CE61: MSB16[arg2_sign_bit; rv2[1]].

syscalls/src/allocator.rs

@@ -1,8 +1,6 @@
 use embedded_alloc::TlsfHeap as Heap;
 use riscv as _;
 
-use crate::syscalls::print_string;
-
 #[global_allocator]
 static HEAP: Heap = Heap::empty();
 
@@ -49,6 +47,7 @@ pub unsafe extern "C" fn sys_getenv(
     _varname: *const u8,
     _varname_len: usize,
 ) -> usize {
-    print_string("sys_getenv is disabled");
+    // NOTE: no print_string here — the Print ecall (#1) has no receiver on the
+    // Ecall bus and would cause a verification failure.
     usize::MAX
 }

syscalls/src/syscalls.rs

@@ -105,7 +105,8 @@ pub enum SyscallError {
 
 #[cfg(target_arch = "riscv64")]
 pub fn sys_halt() -> ! {
-    print_string("sys_halt called\n");
+    // NOTE: no print_string here — the Print ecall is unmatched on the Ecall bus
+    // and would cause a verification failure.
     unsafe {
         asm!(
             "ecall",