diff --git a/ceno_zkvm/src/instructions/riscv/memory/load.rs b/ceno_zkvm/src/instructions/riscv/memory/load.rs index 72dbd53f1..a06c17687 100644 --- a/ceno_zkvm/src/instructions/riscv/memory/load.rs +++ b/ceno_zkvm/src/instructions/riscv/memory/load.rs @@ -84,6 +84,7 @@ impl Instruction for LoadInstruction Result { let rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?; // unsigned 32-bit value let imm = circuit_builder.create_witin(|| "imm"); // signed 12-bit value + // Memory initialization is not guaranteed to contain u32. Range-check it here. let memory_read = UInt::new(|| "memory_read", circuit_builder)?; let memory_addr = match I::INST_KIND { diff --git a/ceno_zkvm/src/instructions/riscv/memory/store.rs b/ceno_zkvm/src/instructions/riscv/memory/store.rs index 00624d2c9..d1d941b97 100644 --- a/ceno_zkvm/src/instructions/riscv/memory/store.rs +++ b/ceno_zkvm/src/instructions/riscv/memory/store.rs @@ -65,6 +65,7 @@ impl Instruction ) -> Result { let rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?; // unsigned 32-bit value let rs2_read = UInt::new_unchecked(|| "rs2_read", circuit_builder)?; + // Memory initialization is not guaranteed to contain u32. Range-check it here. let prev_memory_value = UInt::new(|| "prev_memory_value", circuit_builder)?; let imm = circuit_builder.create_witin(|| "imm"); // signed 12-bit value diff --git a/ceno_zkvm/src/tables/ram.rs b/ceno_zkvm/src/tables/ram.rs index 475ca71b0..182892603 100644 --- a/ceno_zkvm/src/tables/ram.rs +++ b/ceno_zkvm/src/tables/ram.rs @@ -1,4 +1,4 @@ -use ceno_emul::{Addr, VMState, WORD_SIZE}; +use ceno_emul::{Addr, VMState}; use ram_circuit::{DynVolatileRamCircuit, NonVolatileRamCircuit, PubIORamCircuit}; use crate::{ @@ -11,11 +11,12 @@ mod ram_impl; pub use ram_circuit::{DynVolatileRamTable, MemFinalRecord, MemInitRecord, NonVolatileTable}; #[derive(Clone)] -pub struct MemTable; +pub struct DynMemTable; -impl DynVolatileRamTable for MemTable { +impl DynVolatileRamTable for DynMemTable { const RAM_TYPE: RAMType = RAMType::Memory; const V_LIMBS: usize = 1; // See `MemoryExpr`. + const ZERO_INIT: bool = true; fn offset_addr(params: &ProgramParams) -> Addr { params.platform.ram_start() @@ -26,17 +27,32 @@ impl DynVolatileRamTable for MemTable { } fn name() -> &'static str { - "MemTable" + "DynMemTable" + } +} + +pub type DynMemCircuit = DynVolatileRamCircuit; + +#[derive(Clone)] +pub struct PrivateMemTable; +impl DynVolatileRamTable for PrivateMemTable { + const RAM_TYPE: RAMType = RAMType::Memory; + const V_LIMBS: usize = 1; // See `MemoryExpr`. + const ZERO_INIT: bool = false; + + fn offset_addr(params: &ProgramParams) -> Addr { + params.platform.ram_start() + } + + fn end_addr(params: &ProgramParams) -> Addr { + params.platform.ram_end() } - fn max_len(params: &ProgramParams) -> usize { - let max_size = - (Self::end_addr(params) - Self::offset_addr(params)).div_ceil(WORD_SIZE as u32) as Addr; - 1 << (u32::BITS - 1 - max_size.leading_zeros()) // prev_power_of_2 + fn name() -> &'static str { + "PrivateMemTable" } } - -pub type MemCircuit = DynVolatileRamCircuit; +pub type PrivateMemCircuit = DynVolatileRamCircuit; /// RegTable, fix size without offset #[derive(Clone)] diff --git a/ceno_zkvm/src/tables/ram/ram_circuit.rs b/ceno_zkvm/src/tables/ram/ram_circuit.rs index baa9883f5..81f0fcfaa 100644 --- a/ceno_zkvm/src/tables/ram/ram_circuit.rs +++ b/ceno_zkvm/src/tables/ram/ram_circuit.rs @@ -141,13 +141,18 @@ impl TableCirc pub trait DynVolatileRamTable { const RAM_TYPE: RAMType; const V_LIMBS: usize; + const ZERO_INIT: bool; fn offset_addr(params: &ProgramParams) -> Addr; fn end_addr(params: &ProgramParams) -> Addr; fn name() -> &'static str; - fn max_len(params: &ProgramParams) -> usize; + fn max_len(params: &ProgramParams) -> usize { + let max_size = + (Self::end_addr(params) - Self::offset_addr(params)).div_ceil(WORD_SIZE as u32) as Addr; + 1 << (u32::BITS - 1 - max_size.leading_zeros()) // prev_power_of_2 + } fn addr(params: &ProgramParams, entry_index: usize) -> Addr { Self::offset_addr(params) + (entry_index * WORD_SIZE) as Addr @@ -156,8 +161,12 @@ pub trait DynVolatileRamTable { /// DynVolatileRamCircuit initializes and finalizes memory /// - at witnessed addresses, in a contiguous range chosen by the prover, -/// - with zeros as initial content, +/// - with zeros as initial content if ZERO_INIT, /// - with witnessed final content that the program wrote. +/// +/// If not ZERO_INIT: +/// - The initial content is an unconstrained prover hint. +/// - The final content is equal to this initial content. pub struct DynVolatileRamCircuit(PhantomData<(E, R)>); impl TableCircuit diff --git a/ceno_zkvm/src/tables/ram/ram_impl.rs b/ceno_zkvm/src/tables/ram/ram_impl.rs index 86c034a4e..07f36cdab 100644 --- a/ceno_zkvm/src/tables/ram/ram_impl.rs +++ b/ceno_zkvm/src/tables/ram/ram_impl.rs @@ -303,10 +303,17 @@ impl DynVolatileRamTableConfig .collect::>(); let final_cycle = cb.create_witin(|| "final_cycle"); + let final_expr = final_v.iter().map(|v| v.expr()).collect_vec(); + let init_expr = if DVRAM::ZERO_INIT { + vec![Expression::ZERO; DVRAM::V_LIMBS] + } else { + final_expr.clone() + }; + let init_table = [ vec![(DVRAM::RAM_TYPE as usize).into()], vec![addr.expr()], - vec![Expression::ZERO], + init_expr, vec![Expression::ZERO], // Initial cycle. ] .concat(); @@ -315,7 +322,7 @@ impl DynVolatileRamTableConfig // a v t vec![(DVRAM::RAM_TYPE as usize).into()], vec![addr.expr()], - final_v.iter().map(|v| v.expr()).collect_vec(), + final_expr, vec![final_cycle.expr()], ] .concat(); @@ -409,20 +416,3 @@ impl DynVolatileRamTableConfig Ok(final_table) } } - -#[allow(dead_code)] -/// DynUnConstrainRamTableConfig with unconstrain init value and final value -/// dynamic address as witin, relied on augment of knowledge to prove address form -/// do not check init_value -/// TODO implement DynUnConstrainRamTableConfig -#[derive(Clone, Debug)] -pub struct DynUnConstrainRamTableConfig { - addr: WitIn, - - init_v: Vec, - - final_v: Vec, - final_cycle: WitIn, - - phantom: PhantomData, -}