feat/private-input: Unconstrained memory init (#617)

_Issues #614 and #607_

Initialize memory with unconstrained prover hints.

- It is practically identical to the zero-init circuit; just without the
zero-init part.
- The address range must be contiguous, but its size is dynamic.
- The `u32` range check is already done by the LOAD and STORE circuits.

e2e integration will be done in another PR. Need #608 to configure the
address space.

---------

Co-authored-by: Aurélien Nicolas <[email protected]>

Author: naure

ceno_zkvm/src/instructions/riscv/memory/load.rs

@@ -84,6 +84,7 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for LoadInstruction<E,
     ) -> Result<Self::InstructionConfig, ZKVMError> {
         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 {

ceno_zkvm/src/instructions/riscv/memory/store.rs

@@ -65,6 +65,7 @@ impl<E: ExtensionField, I: RIVInstruction, const N_ZEROS: usize> Instruction<E>
     ) -> Result<Self::InstructionConfig, ZKVMError> {
         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
 

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<E> = DynVolatileRamCircuit<E, DynMemTable>;
+
+#[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<E> = DynVolatileRamCircuit<E, MemTable>;
+pub type PrivateMemCircuit<E> = DynVolatileRamCircuit<E, PrivateMemTable>;
 
 /// RegTable, fix size without offset
 #[derive(Clone)]

ceno_zkvm/src/tables/ram/ram_circuit.rs

@@ -141,13 +141,18 @@ impl<E: ExtensionField, NVRAM: NonVolatileTable + Send + Sync + Clone> 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<E, R>(PhantomData<(E, R)>);
 
 impl<E: ExtensionField, DVRAM: DynVolatileRamTable + Send + Sync + Clone> TableCircuit<E>

ceno_zkvm/src/tables/ram/ram_impl.rs

@@ -303,10 +303,17 @@ impl<DVRAM: DynVolatileRamTable + Send + Sync + Clone> DynVolatileRamTableConfig
             .collect::<Vec<WitIn>>();
         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<DVRAM: DynVolatileRamTable + Send + Sync + Clone> 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<DVRAM: DynVolatileRamTable + Send + Sync + Clone> 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<RAM: DynVolatileRamTable + Send + Sync + Clone> {
-    addr: WitIn,
-
-    init_v: Vec<WitIn>,
-
-    final_v: Vec<WitIn>,
-    final_cycle: WitIn,
-
-    phantom: PhantomData<RAM>,
-}