Skip to content
Merged
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

18 changes: 8 additions & 10 deletions bin/cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,7 @@ use executor::{
flamegraph::FlamegraphGenerator,
vm::execution::Executor,
};
use prover::tables::types::{GoldilocksExtension, GoldilocksField};
use stark::proof::stark::MultiProof;
use prover::VmProof;

#[derive(Parser)]
#[command(author, version, about = "Lambda VM - RISC-V zkVM", long_about = None)]
Expand Down Expand Up @@ -216,14 +215,13 @@ fn cmd_verify(proof_path: PathBuf, elf_path: PathBuf) -> ExitCode {
}
};

let proof: MultiProof<GoldilocksField, GoldilocksExtension, ()> =
match bincode::deserialize(&proof_bytes) {
Ok(p) => p,
Err(e) => {
eprintln!("Failed to deserialize proof: {}", e);
return ExitCode::FAILURE;
}
};
let proof: VmProof = match bincode::deserialize(&proof_bytes) {
Ok(p) => p,
Err(e) => {
eprintln!("Failed to deserialize proof: {}", e);
return ExitCode::FAILURE;
}
};

eprintln!("Verifying proof...");
let result = match prover::verify(&proof, &elf_data) {
Expand Down
17 changes: 17 additions & 0 deletions executor/programs/asm/deep_stack.s
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
.attribute 5, "rv64i2p1"
.globl main
main:
# Deep stack usage: allocates 8192 bytes of stack space.
# SP starts at 0xFFFF_FFFF_FFFF_FFF0.
# After allocation: SP = 0x...DFF0 (falls in page 0x...D000).
# With default stack_size=4096, only pages E000 and F000 are
# initialized, so stores into page D000 leave the memory bus
# unbalanced. Increasing stack_size to 8192 adds page D000.
lui t1, 2 # t1 = 8192
sub sp, sp, t1 # sp -= 8192 → 0x...DFF0
addi t0, zero, 0x42
sb t0, 0(sp) # Store byte in page D000
lb a0, 0(sp) # Load it back
add sp, sp, t1 # Restore stack
li a7, 5
ecall
4 changes: 2 additions & 2 deletions executor/src/vm/registers.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use std::fmt::Display;

const STACK_MEMORY_SIZE: u64 = 0xFFFFFFFFFFFFFFF0; // 64-bit max (Multiple of 16 for RV64 ABI)
pub const STACK_TOP: u64 = 0xFFFFFFFFFFFFFFF0; // 64-bit max (Multiple of 16 for RV64 ABI)

#[derive(Debug)]
/// Holds the current value of all 32 registers
Expand All @@ -11,7 +11,7 @@ impl Default for Registers {
fn default() -> Self {
let mut registers = Registers(Default::default());
// Initialize stack pointer according to available memory size
registers.0[1] = STACK_MEMORY_SIZE;
registers.0[1] = STACK_TOP;
registers
}
}
Expand Down
1 change: 1 addition & 0 deletions prover/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ stark = { path = "../crypto/stark" }
crypto = { path = "../crypto/crypto" }
math = { path = "../crypto/math" }
executor = { path = "../executor" }
serde = { version = "1.0", features = ["derive"] }
dhat = { version = "0.3", optional = true }
rayon = { version = "1.8.0", optional = true }

Expand Down
87 changes: 59 additions & 28 deletions prover/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@
//! # Example
//! ```ignore
//! let elf_bytes = std::fs::read("program.elf").unwrap();
//! let proof = lambda_vm_prover::prove(&elf_bytes).unwrap();
//! assert!(lambda_vm_prover::verify(&proof, &elf_bytes).unwrap());
//! let vm_proof = lambda_vm_prover::prove(&elf_bytes).unwrap();
//! assert!(lambda_vm_prover::verify(&vm_proof, &elf_bytes).unwrap());
//! ```

#[cfg(feature = "dhat-heap")]
Expand All @@ -33,16 +33,30 @@ use stark::verifier::{IsStarkVerifier, Verifier};

use crate::tables::bitwise;
use crate::tables::decode;
use crate::tables::page;
use crate::tables::register;
use crate::tables::trace_builder::Traces;
use crate::test_utils::{
E, F, VmAir, create_bitwise_air, create_branch_air, create_cpu_air, create_decode_air,
create_dvrm_air, create_halt_air, create_load_air, create_lt_air, create_memw_air,
create_mul_air, create_page_air, create_register_air,
};

use crate::tables::page::DEFAULT_STACK_SIZE;
use stark::proof::options::ProofOptions;
use stark::proof::stark::MultiProof;

/// A complete VM proof bundle containing the STARK proof and metadata
/// needed by the verifier to reconstruct the AIR configuration.
#[derive(Debug, serde::Serialize, serde::Deserialize)]
pub struct VmProof {
Comment thread
ColoCarletti marked this conversation as resolved.
/// The multi-table STARK proof.
pub proof: MultiProof<F, E, ()>,
/// Stack size used during proving (bytes). The verifier uses this to
/// reconstruct the PAGE table layout.
pub stack_size: u64,
}

/// Error type for the prover crate.
#[derive(Debug)]
pub enum Error {
Expand Down Expand Up @@ -172,10 +186,18 @@ impl VmAirs {
let dvrm = create_dvrm_air(proof_options);
let branch = create_branch_air(proof_options);
let halt = create_halt_air(proof_options);
let register = create_register_air(proof_options);
let register = create_register_air(proof_options).with_preprocessed(
register::preprocessed_commitment(proof_options),
register::NUM_PREPROCESSED_COLS,
);
let pages: Vec<_> = page_configs
.iter()
.map(|config| create_page_air(proof_options, config.page_base))
.map(|config| {
create_page_air(proof_options, config.page_base).with_preprocessed(
page::precomputed_commitment_cached(config, proof_options),
page::NUM_PREPROCESSED_COLS,
)
})
.collect();

#[cfg(feature = "debug-checks")]
Expand All @@ -198,16 +220,16 @@ impl VmAirs {
}
}

/// Prove an ELF binary execution. Returns a serializable proof.
pub fn prove(elf_bytes: &[u8]) -> Result<MultiProof<F, E, ()>, Error> {
/// Prove an ELF binary execution. Returns a serializable proof bundle.
pub fn prove(elf_bytes: &[u8]) -> Result<VmProof, Error> {
prove_with_options(elf_bytes, &ProofOptions::default_proving_options())
}

/// Prove an ELF binary execution with custom proof options.
/// Prove an ELF binary execution with custom proof options and stack size.
Comment thread
ColoCarletti marked this conversation as resolved.
pub fn prove_with_options(
elf_bytes: &[u8],
proof_options: &ProofOptions,
) -> Result<MultiProof<F, E, ()>, Error> {
) -> Result<VmProof, Error> {
let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
let executor = Executor::new(&program, vec![]).map_err(|e| Error::Execution(format!("{e}")))?;
let result = executor
Expand All @@ -216,49 +238,58 @@ pub fn prove_with_options(

// Generate all traces from ELF and execution logs
// This uses the combined ELF processing to generate DECODE and PAGE tables
let mut traces = Traces::from_elf_and_logs(&program, &result.logs)?;
let mut traces = Traces::from_elf_and_logs(&program, &result.logs, DEFAULT_STACK_SIZE)?;
let airs = VmAirs::new(&program, proof_options, false, &traces.page_configs);

Prover::multi_prove(
let proof = Prover::multi_prove(
airs.air_trace_pairs(&mut traces),
&mut DefaultTranscript::<E>::new(&[]),
)
.map_err(|e| Error::Prover(format!("{e:?}")))
}
.map_err(|e| Error::Prover(format!("{e:?}")))?;

Comment thread
ColoCarletti marked this conversation as resolved.
/// Verify a proof produced by [`prove`].
pub fn verify(proof: &MultiProof<F, E, ()>, elf_bytes: &[u8]) -> Result<bool, Error> {
verify_with_options(proof, elf_bytes, &ProofOptions::default_proving_options())
Ok(VmProof {
proof,
stack_size: DEFAULT_STACK_SIZE,
})
}

/// Verify a proof with custom proof options.
/// Verify a proof produced by [`prove`] using default proof options.
///
/// Derives page layout from ELF to reconstruct PAGE AIRs for verification.
/// This works for programs that only use ELF segments and stack (no dynamic heap).
/// Uses [`ProofOptions::default_proving_options`] for verification — the
/// `proof_options` stored in [`VmProof`] are metadata only and NOT trusted.
/// `stack_size` is extracted from the proof; it is safe to trust because
/// preprocessed commitments bind the verifier to the correct page layout.
pub fn verify(vm_proof: &VmProof, elf_bytes: &[u8]) -> Result<bool, Error> {
verify_with_options(
Comment thread
ColoCarletti marked this conversation as resolved.
vm_proof,
elf_bytes,
&ProofOptions::default_proving_options(),
)
}

/// Verify a proof with caller-specified proof options.
///
/// # Note
/// For full production use with dynamic heap allocation, page_configs should be
/// embedded in proof public inputs. This implementation assumes deterministic
/// page layout derivable from ELF.
/// The verifier enforces its own `proof_options` (security parameters),
/// ignoring the options embedded in the proof bundle. This prevents a
/// malicious prover from weakening the security level.
pub fn verify_with_options(
proof: &MultiProof<F, E, ()>,
vm_proof: &VmProof,
elf_bytes: &[u8],
proof_options: &ProofOptions,
) -> Result<bool, Error> {
let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
// Derive page layout from ELF (works for programs without dynamic heap)
let page_configs = Traces::page_configs_from_elf(&program);
let page_configs = Traces::page_configs_from_elf(&program, vm_proof.stack_size);
let airs = VmAirs::new(&program, proof_options, false, &page_configs);

Ok(Verifier::multi_verify(
&airs.air_refs(),
proof,
&vm_proof.proof,
&mut DefaultTranscript::<E>::new(&[]),
))
}

/// Prove and verify in one call (convenience).
pub fn prove_and_verify(elf_bytes: &[u8]) -> Result<bool, Error> {
let proof = prove(elf_bytes)?;
verify(&proof, elf_bytes)
let vm_proof = prove(elf_bytes)?;
verify(&vm_proof, elf_bytes)
}
100 changes: 97 additions & 3 deletions prover/src/tables/page.rs
Original file line number Diff line number Diff line change
Expand Up @@ -32,9 +32,15 @@
//! | PAGE-C4 | Memory | `[0, address, timestamp, fini]` | 1 (sender) |

use std::collections::HashMap;
use std::sync::OnceLock;

use math::fft::cpu::bit_reversing::in_place_bit_reverse_permute;
use math::polynomial::Polynomial;
use stark::config::{BatchedMerkleTree, Commitment};
use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing};
use stark::trace::TraceTable;
use stark::proof::options::ProofOptions;
use stark::prover::evaluate_polynomial_on_lde_domain;
use stark::trace::{TraceTable, columns2rows};

use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField};

Expand All @@ -45,8 +51,11 @@ use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField};
/// Default page size in bytes (4KB).
pub const DEFAULT_PAGE_SIZE: usize = 4096;

/// Stack top address (where SP starts). Must match executor.
pub const STACK_TOP: u64 = 0xFFFF_FFFF_FFFF_FFF0;
/// Stack top address (where SP starts). Re-exported from executor.
pub use executor::vm::registers::STACK_TOP;

/// Default stack size in bytes.
pub const DEFAULT_STACK_SIZE: u64 = 4096;

// =========================================================================
// Column indices for PAGE table
Expand Down Expand Up @@ -195,6 +204,91 @@ pub fn generate_page_trace(
TraceTable::new_main(data, cols::NUM_COLUMNS, 1)
}

// =========================================================================
// Preprocessed commitment
// =========================================================================

/// Cached commitment for zero-initialized 4KB pages.
/// All zero-init pages of the same size have identical OFFSET and INIT columns.
///
/// INVARIANT: All callers within a process must use identical `ProofOptions`.
/// The cache is keyed only by page content, not by options.
static ZERO_PAGE_4K_COMMITMENT: OnceLock<Commitment> = OnceLock::new();
Comment thread
ColoCarletti marked this conversation as resolved.

/// Computes the Merkle root commitment over the LDE of PAGE precomputed columns.
///
/// The commitment covers OFFSET (0..page_size-1) and INIT (from config).
/// Each page may have different INIT data, producing a different commitment.
pub fn compute_precomputed_commitment(config: &PageConfig, options: &ProofOptions) -> Commitment {
let page_size = config.page_size;
assert!(page_size.is_power_of_two(), "Page size must be power of 2");

let num_rows = page_size;

// Precomputed columns: OFFSET and INIT.
//
// OFFSET (col 0): deterministic row index 0..page_size-1, the same for every
// page of a given size regardless of the program being proven.
//
// INIT (col 1): the initial byte value at each offset. For zero-init pages
// (stack, heap, BSS) this is all zeros. For ELF data pages it holds the
// bytes loaded from the binary. Either way the column is fully determined
// before execution, so the verifier can check it against a preprocessed
// commitment instead of including it in the main trace.
let mut offset_col = vec![FE::zero(); num_rows];
let mut init_col = vec![FE::zero(); num_rows];

for i in 0..page_size {
Comment thread
ColoCarletti marked this conversation as resolved.
offset_col[i] = FE::from(i as u64);
init_col[i] = if let Some(ref init_vals) = config.init_values {
FE::from(init_vals[i] as u64)
} else {
FE::zero()
};
}

let columns = [offset_col, init_col];

let polys: Vec<Polynomial<FE>> = columns
.iter()
.map(|col| {
Polynomial::interpolate_fft::<GoldilocksField>(col)
.expect("FFT interpolation failed for page column")
Comment thread
ColoCarletti marked this conversation as resolved.
})
.collect();

let blowup_factor = options.blowup_factor as usize;
let coset_offset = FE::from(options.coset_offset);
let mut lde_columns: Vec<Vec<FE>> = polys
.iter()
.map(|poly| {
evaluate_polynomial_on_lde_domain(poly, blowup_factor, num_rows, &coset_offset)
.expect("LDE evaluation failed for page polynomial")
})
.collect();

for col in lde_columns.iter_mut() {
in_place_bit_reverse_permute(col);
}

let lde_rows = columns2rows(lde_columns);
let tree = BatchedMerkleTree::<GoldilocksField>::build(&lde_rows)
.expect("Failed to build Merkle tree for page LDE");
tree.root
}

/// Returns the preprocessed commitment for a PAGE table, with caching for zero-init pages.
///
/// Zero-init pages of DEFAULT_PAGE_SIZE share a cached commitment.
/// ELF data pages compute their commitment fresh.
pub fn precomputed_commitment_cached(config: &PageConfig, options: &ProofOptions) -> Commitment {
if config.init_values.is_none() && config.page_size == DEFAULT_PAGE_SIZE {
*ZERO_PAGE_4K_COMMITMENT.get_or_init(|| compute_precomputed_commitment(config, options))
} else {
compute_precomputed_commitment(config, options)
}
}

// =========================================================================
// Bus interactions
// =========================================================================
Expand Down
Loading