Skip to content

Commit aaf9299

Browse files
committed
fix_bugs
1 parent eb5cc73 commit aaf9299

8 files changed

Lines changed: 75 additions & 46 deletions

File tree

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

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
// Minimal Rust program that proves on main:
2-
// - no_std, no_main (no Rust std runtime)
3-
// - no allocator (no TLSF init)
4-
// - no syscalls crate (no Print/Panic ecalls)
5-
// - Only uses Commit (64) and Halt (93) ecalls, both of which have
6-
// receivers on the Ecall bus.
1+
// Minimal Rust guest program: no_std, no_main, no allocator, no syscalls crate.
2+
// Uses only raw inline `asm!("ecall")` for Commit (64) and Halt (93).
3+
// Serves as a control case in the prover test suite (`test_pure_commit_rust`):
4+
// verifies that Rust can compile to a provable ELF when the heap allocator is
5+
// bypassed, independent of the Rust-std startup path.
76
#![no_std]
87
#![no_main]
98

executor/tests/asm.rs

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -21,17 +21,6 @@ fn run_program(elf_path: &str) {
2121
);
2222
}
2323

24-
#[test]
25-
fn test_debug_commit_sum_count() {
26-
let elf_data = std::fs::read("./program_artifacts/rust/commit_sum.elf").unwrap();
27-
let program = Elf::load(&elf_data).unwrap();
28-
let executor = Executor::new(&program, vec![3u8, 5u8]).unwrap();
29-
let result = executor.run().unwrap();
30-
eprintln!("Instructions: {}", result.logs.len());
31-
eprintln!("Output: {:?}", result.return_values.memory_values);
32-
assert_eq!(result.return_values.memory_values, vec![8u8]);
33-
}
34-
3524
/// Test that the memory-mapped private input region is readable by guest programs.
3625
/// The ASM program reads from 0xFF000000 and commits 8 bytes of data.
3726
#[test]
1.83 KB
Binary file not shown.

prover/src/lib.rs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -493,8 +493,12 @@ pub fn prove(elf_bytes: &[u8]) -> Result<VmProof, Error> {
493493

494494
/// Prove an ELF binary execution with a private input.
495495
///
496-
/// The `private_input` bytes are passed to the executor; the guest program
497-
/// retrieves them via the `GetPrivateInputs` syscall.
496+
/// The `private_input` bytes are pre-loaded at `PRIVATE_INPUT_START_INDEX`
497+
/// (`0xFF000000`) as an initial memory segment (4-byte LE length prefix +
498+
/// data). The guest reads them via normal RISC-V loads — see
499+
/// `syscalls::syscalls::get_private_input`. The bytes are also included in
500+
/// the returned `VmProof` so the verifier can reconstruct the matching PAGE
501+
/// preprocessed commitments.
498502
pub fn prove_with_input(elf_bytes: &[u8], private_input: Vec<u8>) -> Result<VmProof, Error> {
499503
prove_with_options(
500504
elf_bytes,

prover/src/tables/shift.rs

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -181,8 +181,14 @@ impl ShiftOperation {
181181
let left = !self.direction;
182182
let right = self.direction;
183183

184-
// is_negative = MSB of in[3]
185-
let is_negative = (self.in_halves[3] >> 15) & 1 == 1;
184+
// is_negative is the MSB of in[3] BUT gated by `signed`. The SHIFT
185+
// AIR constrains IS_NEGATIVE via the MSB16 bus (SHIFT-C14) only when
186+
// `signed = 1` — for `signed = 0` IS_NEGATIVE is free, so we set it
187+
// to zero. This makes `extension = 65535 * is_negative = 0` for SRL,
188+
// so the extension contribution in `compute_shifted_half` naturally
189+
// vanishes (zero fill) — matching RISC-V SRL semantics regardless of
190+
// the top-bit value of the input.
191+
let is_negative = self.signed && (self.in_halves[3] >> 15) & 1 == 1;
186192
let extension: u16 = if is_negative { 0xFFFF } else { 0 };
187193

188194
// bit_shift
@@ -642,7 +648,11 @@ impl ShiftConstraint {
642648
let left = &mu - &dir; // μ - direction
643649
let right = dir;
644650

645-
// extension = 65535 * is_negative
651+
// extension = 65535 * is_negative (virtual; matches SHIFT-C7 HWSL send).
652+
// The IS_NEGATIVE column is only constrained by MSB16 when signed=1
653+
// (SHIFT-C14's bus send is gated by SIGNED). For SRL (signed=0) the
654+
// trace sets IS_NEGATIVE=0 explicitly so extension=0 → x[4]=0 → no
655+
// spurious extension bleed into `shifted`.
646656
let is_neg = step.get_main_evaluation_element(0, cols::IS_NEGATIVE);
647657
let extension = is_neg * FieldElement::<F>::from(65535u64);
648658

prover/src/tables/trace_builder.rs

Lines changed: 20 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1343,19 +1343,14 @@ fn collect_byte_check_ops_for_padding(num_padding_rows: usize) -> Vec<BitwiseOpe
13431343
ops
13441344
}
13451345

1346-
/// Collects IS_BYTE lookups from PAGE data (init and fini values).
1347-
///
1348-
/// Each PAGE byte generates 2 IS_BYTE lookups:
1349-
/// - C1: IS_BYTE[init] for initialization range check
1350-
/// - C2: IS_BYTE[fini] for finalization range check
1351-
///
1352-
/// This must be called BEFORE bitwise multiplicities are updated.
1353-
/// Build a page_base → init_data map from the ELF segments and the private input region.
1346+
/// Build a `page_base → init_data` map from the ELF segments and the private
1347+
/// input region.
13541348
///
1355-
/// The private input is laid out at `PRIVATE_INPUT_START_INDEX` as a 4-byte LE length
1356-
/// prefix followed by the raw bytes (matching `Memory::store_private_inputs` and
1357-
/// `MemoryState::add_private_input`). Both the prover (trace generation) and verifier
1358-
/// (page config reconstruction) call this so they agree on PAGE init values exactly.
1349+
/// The private input is laid out at `PRIVATE_INPUT_START_INDEX` as a 4-byte LE
1350+
/// length prefix followed by the raw bytes (matching
1351+
/// `Memory::store_private_inputs` and `MemoryState::add_private_input`). Both
1352+
/// the prover (trace generation) and verifier (page config reconstruction) call
1353+
/// this so they agree on PAGE init values exactly.
13591354
fn build_init_page_data(elf: &Elf, private_input: &[u8]) -> HashMap<u64, Vec<u8>> {
13601355
use executor::vm::memory::PRIVATE_INPUT_START_INDEX;
13611356
let page_size = page::DEFAULT_PAGE_SIZE;
@@ -1400,6 +1395,13 @@ fn build_init_page_data(elf: &Elf, private_input: &[u8]) -> HashMap<u64, Vec<u8>
14001395
init_page_data
14011396
}
14021397

1398+
/// Collects IS_BYTE lookups from PAGE data (init and fini values).
1399+
///
1400+
/// Each PAGE byte generates 2 IS_BYTE lookups:
1401+
/// - C1: IS_BYTE[init] for initialization range check
1402+
/// - C2: IS_BYTE[fini] for finalization range check
1403+
///
1404+
/// This must be called BEFORE bitwise multiplicities are updated.
14031405
fn collect_bitwise_from_page(
14041406
elf: &Elf,
14051407
memory_state: &MemoryState,
@@ -1694,11 +1696,13 @@ impl Traces {
16941696
}
16951697
}
16961698

1697-
/// Extract page configurations from ELF only (deterministic from binary).
1699+
/// Extract page configurations for the deterministic portion of memory:
1700+
/// ELF segments and the private-input region at `PRIVATE_INPUT_START_INDEX`.
16981701
///
1699-
/// Returns PageConfigs for pages covered by ELF segments, with their
1700-
/// init data populated. Used by the verifier to reconstruct the ELF
1701-
/// portion of the PAGE table layout.
1702+
/// Returns PageConfigs for every page covered by an ELF segment or by the
1703+
/// private-input bytes, with init data populated. Used by the verifier to
1704+
/// reconstruct these pages (runtime-only pages like stack/heap come from
1705+
/// `page_configs_from_elf_and_runtime`).
17021706
pub fn page_configs_from_elf(elf: &Elf, private_input: &[u8]) -> Vec<PageConfig> {
17031707
let page_size = page::DEFAULT_PAGE_SIZE;
17041708
let init_page_data = build_init_page_data(elf, private_input);

prover/src/tables/types.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -668,7 +668,15 @@ impl DecodeEntry {
668668
}
669669

670670
Instruction::CSR { .. } => {
671-
// CSR instructions not yet supported in prover
671+
// CSR instructions are executed as no-ops by the VM (see
672+
// `executor/src/vm/instruction/execution.rs` Instruction::CSR arm
673+
// returning `dst_val: 0, src1/2_val: 0`). Mirror that here by
674+
// treating them as `ADDI x0, x0, 0` — same pattern as `Fence`.
675+
// This sets `op_add=true` so CM54's "1 - pad" (sum of ALU flags)
676+
// multiplicity is non-zero and the CPU's PC-update Memw sender
677+
// fires to match the MEMW_R PC row that
678+
// `collect_register_ops_from_cpu` unconditionally emits.
679+
entry.op_add = true;
672680
}
673681

674682
Instruction::EcallEbreak => {

prover/src/tests/prove_elfs_tests.rs

Lines changed: 22 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1981,14 +1981,7 @@ fn test_verify_rejects_tampered_private_input() {
19811981

19821982
/// End-to-end test: prove+verify a Rust program (commit_sum) with private input.
19831983
/// commit_sum reads input[0] + input[1] and commits the u8 sum.
1984-
///
1985-
/// NOTE: currently ignored because Rust std programs hit a pre-existing
1986-
/// Memory/Shift bus imbalance (likely from `init_allocator`'s TLSF heap setup).
1987-
/// This is unrelated to the private input handling — confirmed by running the
1988-
/// ASM tests above (`test_prove_private_input_xpage` etc.) which exercise the
1989-
/// full memory-mapped private input path and verify correctly.
19901984
#[test]
1991-
#[ignore = "Blocked on pre-existing Rust std allocator bus imbalance (not private-input related)"]
19921985
fn test_prove_commit_sum() {
19931986
let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
19941987
.parent()
@@ -2006,6 +1999,28 @@ fn test_prove_commit_sum() {
20061999
assert_eq!(proof.public_output, vec![8u8]); // 3 + 5
20072000
}
20082001

2002+
/// Regression test: a minimal Rust std program that uses `init_allocator()`
2003+
/// and `String::from("Hello World") + commit`. Exercises the full stack:
2004+
/// TLSF heap init, SRL on high-bit-set values (fixed in `shift::compute_aux`)
2005+
/// and CSR instructions (fixed in `DecodeEntry::from(Instruction::CSR)`).
2006+
#[test]
2007+
fn test_prove_allocator_minimal_reproducer() {
2008+
let _ = env_logger::builder().is_test(true).try_init();
2009+
let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
2010+
.parent()
2011+
.unwrap()
2012+
.to_path_buf();
2013+
let elf_bytes =
2014+
std::fs::read(workspace_root.join("executor/program_artifacts/rust/allocator.elf"))
2015+
.unwrap();
2016+
let proof = crate::prove(&elf_bytes).expect("prove should succeed");
2017+
assert!(
2018+
crate::verify(&proof, &elf_bytes).expect("verify should not error"),
2019+
"allocator.elf should verify"
2020+
);
2021+
assert_eq!(proof.public_output, b"Hello World");
2022+
}
2023+
20092024
/// Minimal Rust program that proves on main: no_std, no_main,
20102025
/// no syscalls crate → only Commit + Halt ecalls (both have receivers).
20112026
/// Demonstrates that Rust CAN prove when it avoids Print/Panic.

0 commit comments

Comments
 (0)