From 82ca0023a50288143788e8097b4f35d796d80f26 Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Mon, 20 Apr 2026 11:11:33 -0300 Subject: [PATCH 1/2] fix executor bugs --- executor/programs/asm/test_wsuffix_64bit.s | 36 +++++++++++++ .../rust/pure_commit/.cargo/config.toml | 6 +++ executor/programs/rust/pure_commit/Cargo.toml | 8 +++ .../programs/rust/pure_commit/src/main.rs | 39 ++++++++++++++ executor/src/vm/instruction/execution.rs | 24 ++++++--- prover/src/tables/shift.rs | 10 +++- prover/src/tables/types.rs | 8 ++- prover/src/tests/prove_elfs_tests.rs | 51 +++++++++++++++++++ syscalls/src/allocator.rs | 5 +- syscalls/src/syscalls.rs | 3 +- 10 files changed, 175 insertions(+), 15 deletions(-) create mode 100644 executor/programs/asm/test_wsuffix_64bit.s create mode 100644 executor/programs/rust/pure_commit/.cargo/config.toml create mode 100644 executor/programs/rust/pure_commit/Cargo.toml create mode 100644 executor/programs/rust/pure_commit/src/main.rs diff --git a/executor/programs/asm/test_wsuffix_64bit.s b/executor/programs/asm/test_wsuffix_64bit.s new file mode 100644 index 000000000..1e57a1ff2 --- /dev/null +++ b/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 diff --git a/executor/programs/rust/pure_commit/.cargo/config.toml b/executor/programs/rust/pure_commit/.cargo/config.toml new file mode 100644 index 000000000..be730c3ec --- /dev/null +++ b/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" +] diff --git a/executor/programs/rust/pure_commit/Cargo.toml b/executor/programs/rust/pure_commit/Cargo.toml new file mode 100644 index 000000000..95fdfe36f --- /dev/null +++ b/executor/programs/rust/pure_commit/Cargo.toml @@ -0,0 +1,8 @@ +[workspace] + +[package] +name = "pure_commit" +version = "0.1.0" +edition = "2024" + +[dependencies] diff --git a/executor/programs/rust/pure_commit/src/main.rs b/executor/programs/rust/pure_commit/src/main.rs new file mode 100644 index 000000000..c23b46f79 --- /dev/null +++ b/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", + in("a0") 1usize, // fd = stdout + in("a1") buf.as_ptr(), + in("a2") 4usize, + in("a7") 64usize, // Commit + ); + } + // Halt + unsafe { + asm!( + "ecall", + in("a0") 0usize, // exit_code = 0 + in("a7") 93usize, // Halt + ); + } + loop {} +} diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index dcab3f927..3cd299143 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/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, } } diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index bb535c537..ffa247feb 100644 --- a/prover/src/tables/shift.rs +++ b/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 diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index 8e89490ae..fcedf869a 100644 --- a/prover/src/tables/types.rs +++ b/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 => { diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 9a1b8a6d0..ee8890667 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/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")) + .unwrap(); + 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")) + .unwrap(); + 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]]. diff --git a/syscalls/src/allocator.rs b/syscalls/src/allocator.rs index 2469f435d..08dbb2d92 100644 --- a/syscalls/src/allocator.rs +++ b/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 } diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index e31b66619..f85ccd3ae 100644 --- a/syscalls/src/syscalls.rs +++ b/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", From c524af0b84eab0c86a9185fabc419cbc8170ad84 Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Mon, 20 Apr 2026 18:29:52 -0300 Subject: [PATCH 2/2] fix coments --- executor/programs/rust/pure_commit/src/main.rs | 8 ++++---- prover/src/tests/prove_elfs_tests.rs | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/executor/programs/rust/pure_commit/src/main.rs b/executor/programs/rust/pure_commit/src/main.rs index c23b46f79..35ecbf103 100644 --- a/executor/programs/rust/pure_commit/src/main.rs +++ b/executor/programs/rust/pure_commit/src/main.rs @@ -21,18 +21,18 @@ pub extern "C" fn main() -> ! { unsafe { asm!( "ecall", - in("a0") 1usize, // fd = stdout + inlateout("a0") 1usize => _, // fd = stdout; ecall overwrites a0 in("a1") buf.as_ptr(), in("a2") 4usize, - in("a7") 64usize, // Commit + in("a7") 64usize, // Commit ); } // Halt unsafe { asm!( "ecall", - in("a0") 0usize, // exit_code = 0 - in("a7") 93usize, // Halt + inlateout("a0") 0usize => _, // exit_code = 0; ecall overwrites a0 + in("a7") 93usize, // Halt ); } loop {} diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ee8890667..5a52a20fa 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1922,7 +1922,7 @@ fn test_prove_allocator_minimal_reproducer() { .to_path_buf(); let elf_bytes = std::fs::read(workspace_root.join("executor/program_artifacts/rust/allocator.elf")) - .unwrap(); + .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"), @@ -1941,7 +1941,7 @@ fn test_pure_commit_rust() { .to_path_buf(); let elf_bytes = std::fs::read(workspace_root.join("executor/program_artifacts/rust/pure_commit.elf")) - .unwrap(); + .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"),