From 889973a2aabcf8fa8e48cbb5d8d5eec08c5cec2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A9lien=20Nicolas?= Date: Tue, 12 Nov 2024 05:16:14 +0100 Subject: [PATCH] feat/guest-example: refactor SetTableSpec + flexible addr assign --- ceno_zkvm/src/circuit_builder.rs | 10 ++-- ceno_zkvm/src/scheme/prover.rs | 2 +- ceno_zkvm/src/scheme/verifier.rs | 13 ++--- ceno_zkvm/src/tables/ram/ram_impl.rs | 71 +++++++++++++++------------- 4 files changed, 50 insertions(+), 46 deletions(-) diff --git a/ceno_zkvm/src/circuit_builder.rs b/ceno_zkvm/src/circuit_builder.rs index ec3b440db..90461d5d9 100644 --- a/ceno_zkvm/src/circuit_builder.rs +++ b/ceno_zkvm/src/circuit_builder.rs @@ -78,14 +78,18 @@ pub struct LogupTableExpression { #[derive(Clone, Debug)] pub enum SetTableAddrType { FixedAddr, - DynamicAddr, + DynamicAddr(DynamicAddr), +} + +#[derive(Clone, Debug)] +pub struct DynamicAddr { + pub addr_witin_id: usize, + pub offset: Addr, } #[derive(Clone, Debug)] pub struct SetTableSpec { pub addr_type: SetTableAddrType, - pub addr_witin_id: Option, - pub offset: Addr, pub len: usize, } diff --git a/ceno_zkvm/src/scheme/prover.rs b/ceno_zkvm/src/scheme/prover.rs index a387f55e8..25a08bfec 100644 --- a/ceno_zkvm/src/scheme/prover.rs +++ b/ceno_zkvm/src/scheme/prover.rs @@ -1024,7 +1024,7 @@ impl> ZKVMProver { .map(|(t, mle)| match t.table_spec.addr_type { // for fixed address, prover SetTableAddrType::FixedAddr => 0, - SetTableAddrType::DynamicAddr => mle.num_vars(), + SetTableAddrType::DynamicAddr(_) => mle.num_vars(), }) .collect_vec(); // TODO implement mechanism to skip commitment diff --git a/ceno_zkvm/src/scheme/verifier.rs b/ceno_zkvm/src/scheme/verifier.rs index 464d1b853..87200d32d 100644 --- a/ceno_zkvm/src/scheme/verifier.rs +++ b/ceno_zkvm/src/scheme/verifier.rs @@ -539,7 +539,7 @@ impl> ZKVMVerifier [num_vars, num_vars] } // dynamic: respect prover hint - SetTableAddrType::DynamicAddr => { + SetTableAddrType::DynamicAddr(_) => { // check number of vars doesn't exceed max len defined in vk // this is important to prevent address overlapping assert!((1 << hint_num_vars) <= r.table_spec.len); @@ -718,18 +718,15 @@ impl> ZKVMVerifier // verify dynamic address evaluation succinctly // TODO we can also skip their mpcs proof for r_table in cs.r_table_expressions.iter() { - match r_table.table_spec.addr_type { + match &r_table.table_spec.addr_type { SetTableAddrType::FixedAddr => (), - SetTableAddrType::DynamicAddr => { - let offset = r_table.table_spec.offset; + SetTableAddrType::DynamicAddr(spec) => { let expected_eval = eval_wellform_address_vec( - offset as u64, + spec.offset as u64, WORD_SIZE as u64, &input_opening_point, ); - if expected_eval - != proof.wits_in_evals[r_table.table_spec.addr_witin_id.unwrap()] - { + if expected_eval != proof.wits_in_evals[spec.addr_witin_id] { return Err(ZKVMError::VerifyError( "dynamic addr evaluate != expected_evals".into(), )); diff --git a/ceno_zkvm/src/tables/ram/ram_impl.rs b/ceno_zkvm/src/tables/ram/ram_impl.rs index a84fe4834..2dc9eeb84 100644 --- a/ceno_zkvm/src/tables/ram/ram_impl.rs +++ b/ceno_zkvm/src/tables/ram/ram_impl.rs @@ -1,12 +1,17 @@ -use std::{collections::HashMap, marker::PhantomData, mem::MaybeUninit}; +use std::{ + collections::{HashMap, HashSet}, + marker::PhantomData, + mem::MaybeUninit, +}; +use ceno_emul::Addr; use ff_ext::ExtensionField; use goldilocks::SmallField; use itertools::Itertools; use rayon::iter::{IndexedParallelIterator, IntoParallelIterator, ParallelIterator}; use crate::{ - circuit_builder::{CircuitBuilder, SetTableAddrType, SetTableSpec}, + circuit_builder::{CircuitBuilder, DynamicAddr, SetTableAddrType, SetTableSpec}, error::ZKVMError, expression::{Expression, Fixed, ToExpr, WitIn}, instructions::riscv::constants::{LIMB_BITS, LIMB_MASK}, @@ -77,8 +82,6 @@ impl NonVolatileTableConfig NonVolatileTableConfig NonVolatileTableConfig>(); + let unused_addrs = (NVRAM::OFFSET_ADDR..NVRAM::END_ADDR) + .filter(|&addr| !accessed_addrs.contains(&addr)) + .take(NVRAM::len() - init_mem.len()) + .collect_vec(); + // set padding with well-form address with 0 value - if NVRAM::len() - init_mem.len() > 0 { - let paddin_entry_start = init_mem.len(); - init_table - .par_iter_mut() - .skip(init_mem.len()) - .enumerate() - .with_min_len(MIN_PAR_SIZE) - .for_each(|(i, row)| { - // set value limb to 0 - self.init_v.iter().for_each(|limb| { - set_fixed_val!(row, limb, 0u64.into()); - }); - set_fixed_val!( - row, - self.addr, - (NVRAM::addr(paddin_entry_start + i) as u64).into() - ); + init_table + .par_iter_mut() + .skip(init_mem.len()) + .zip_eq(unused_addrs) + .with_min_len(MIN_PAR_SIZE) + .for_each(|(row, addr): (&mut [MaybeUninit], Addr)| { + // set value limb to 0 + self.init_v.iter().for_each(|limb| { + set_fixed_val!(row, limb, 0u64.into()); }); - } + set_fixed_val!(row, self.addr, (addr as u64).into()); + }); + init_table } @@ -251,8 +256,6 @@ impl PubIOTableConfig { NVRAM::RAM_TYPE, SetTableSpec { addr_type: SetTableAddrType::FixedAddr, - addr_witin_id: None, - offset: NVRAM::OFFSET_ADDR, len: NVRAM::len(), }, init_table, @@ -262,8 +265,6 @@ impl PubIOTableConfig { NVRAM::RAM_TYPE, SetTableSpec { addr_type: SetTableAddrType::FixedAddr, - addr_witin_id: None, - offset: NVRAM::OFFSET_ADDR, len: NVRAM::len(), }, final_table, @@ -368,9 +369,10 @@ impl DynVolatileRamTableConfig || "init_table", DVRAM::RAM_TYPE, SetTableSpec { - addr_type: SetTableAddrType::DynamicAddr, - addr_witin_id: Some(addr.id.into()), - offset: DVRAM::OFFSET_ADDR, + addr_type: SetTableAddrType::DynamicAddr(DynamicAddr { + addr_witin_id: addr.id.into(), + offset: DVRAM::OFFSET_ADDR, + }), len: DVRAM::max_len(), }, init_table, @@ -379,9 +381,10 @@ impl DynVolatileRamTableConfig || "final_table", DVRAM::RAM_TYPE, SetTableSpec { - addr_type: SetTableAddrType::DynamicAddr, - addr_witin_id: Some(addr.id.into()), - offset: DVRAM::OFFSET_ADDR, + addr_type: SetTableAddrType::DynamicAddr(DynamicAddr { + addr_witin_id: addr.id.into(), + offset: DVRAM::OFFSET_ADDR, + }), len: DVRAM::max_len(), }, final_table,