From 931d942c5c5b129fd87d73165eb0bd1c64bb5f22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A9lien=20Nicolas?= Date: Thu, 21 Nov 2024 12:49:41 +0100 Subject: [PATCH 1/3] feat/private-input: Unconstrained memory init --- .../src/instructions/riscv/memory/load.rs | 1 + ceno_zkvm/src/tables/ram.rs | 29 +++++++++++++------ ceno_zkvm/src/tables/ram/ram_circuit.rs | 10 +++++-- ceno_zkvm/src/tables/ram/ram_impl.rs | 11 +++++-- 4 files changed, 38 insertions(+), 13 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/memory/load.rs b/ceno_zkvm/src/instructions/riscv/memory/load.rs index 72dbd53f1..5eacd510e 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. Decompose in [u16; 2] here. let memory_read = UInt::new(|| "memory_read", circuit_builder)?; let memory_addr = match I::INST_KIND { diff --git a/ceno_zkvm/src/tables/ram.rs b/ceno_zkvm/src/tables/ram.rs index 5f08668a9..6b6e91892 100644 --- a/ceno_zkvm/src/tables/ram.rs +++ b/ceno_zkvm/src/tables/ram.rs @@ -1,4 +1,4 @@ -use ceno_emul::{Addr, CENO_PLATFORM, VMState, WORD_SIZE}; +use ceno_emul::{Addr, CENO_PLATFORM, VMState}; use ram_circuit::{DynVolatileRamCircuit, NonVolatileRamCircuit, PubIORamCircuit}; use crate::{instructions::riscv::constants::UINT_LIMBS, structs::RAMType}; @@ -8,25 +8,36 @@ 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 OFFSET_ADDR: Addr = CENO_PLATFORM.ram_start(); const END_ADDR: Addr = CENO_PLATFORM.ram_end() + 1; + const ZERO_INIT: bool = true; 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 OFFSET_ADDR: Addr = CENO_PLATFORM.ram_start(); + const END_ADDR: Addr = CENO_PLATFORM.ram_end() + 1; + const ZERO_INIT: bool = false; - fn max_len() -> usize { - let max_size = (Self::END_ADDR - Self::OFFSET_ADDR) / WORD_SIZE 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 c19adfc76..4616bd60e 100644 --- a/ceno_zkvm/src/tables/ram/ram_circuit.rs +++ b/ceno_zkvm/src/tables/ram/ram_circuit.rs @@ -138,6 +138,7 @@ impl TableCirc pub trait DynVolatileRamTable { const RAM_TYPE: RAMType; const V_LIMBS: usize; + const ZERO_INIT: bool; const OFFSET_ADDR: Addr; const END_ADDR: Addr; @@ -145,7 +146,8 @@ pub trait DynVolatileRamTable { fn name() -> &'static str; fn max_len() -> usize { - (Self::END_ADDR - Self::OFFSET_ADDR) as usize / WORD_SIZE + let max_size = (Self::END_ADDR - Self::OFFSET_ADDR) / WORD_SIZE as Addr; + 1 << (u32::BITS - 1 - max_size.leading_zeros()) // prev_power_of_2 } fn addr(entry_index: usize) -> Addr { @@ -155,8 +157,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 4c20bc894..06e69641b 100644 --- a/ceno_zkvm/src/tables/ram/ram_impl.rs +++ b/ceno_zkvm/src/tables/ram/ram_impl.rs @@ -297,10 +297,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(); @@ -309,7 +316,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(); From feb02251f58fb320d00396d3153fc12ae625356b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A9lien=20Nicolas?= Date: Thu, 21 Nov 2024 13:00:53 +0100 Subject: [PATCH 2/3] feat/private-input: remove draft --- .../src/instructions/riscv/memory/store.rs | 1 + ceno_zkvm/src/tables/ram/ram_impl.rs | 17 ----------------- 2 files changed, 1 insertion(+), 17 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/memory/store.rs b/ceno_zkvm/src/instructions/riscv/memory/store.rs index 18b134e57..c193e8ec6 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. Decompose in [u16; 2] 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/ram_impl.rs b/ceno_zkvm/src/tables/ram/ram_impl.rs index 06e69641b..47f665807 100644 --- a/ceno_zkvm/src/tables/ram/ram_impl.rs +++ b/ceno_zkvm/src/tables/ram/ram_impl.rs @@ -405,20 +405,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, -} From 4b38b04107e7093d01e283c0fde320359c704ff7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A9lien=20Nicolas?= Date: Thu, 21 Nov 2024 16:50:40 +0100 Subject: [PATCH 3/3] feat/private-input: clarify comment --- ceno_zkvm/src/instructions/riscv/memory/load.rs | 2 +- ceno_zkvm/src/instructions/riscv/memory/store.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/memory/load.rs b/ceno_zkvm/src/instructions/riscv/memory/load.rs index 5eacd510e..a06c17687 100644 --- a/ceno_zkvm/src/instructions/riscv/memory/load.rs +++ b/ceno_zkvm/src/instructions/riscv/memory/load.rs @@ -84,7 +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. Decompose in [u16; 2] here. + // 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 8ae186efd..d1d941b97 100644 --- a/ceno_zkvm/src/instructions/riscv/memory/store.rs +++ b/ceno_zkvm/src/instructions/riscv/memory/store.rs @@ -65,7 +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. Decompose in [u16; 2] here. + // 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