Skip to content

Commit

Permalink
feat/guest-example: refactor SetTableSpec + flexible addr assign
Browse files Browse the repository at this point in the history
  • Loading branch information
Aurélien Nicolas committed Nov 12, 2024
1 parent c624003 commit 889973a
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 46 deletions.
10 changes: 7 additions & 3 deletions ceno_zkvm/src/circuit_builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,14 +78,18 @@ pub struct LogupTableExpression<E: ExtensionField> {
#[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<usize>,
pub offset: Addr,
pub len: usize,
}

Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/scheme/prover.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1024,7 +1024,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
.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
Expand Down
13 changes: 5 additions & 8 deletions ceno_zkvm/src/scheme/verifier.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -539,7 +539,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMVerifier<E, PCS>
[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);
Expand Down Expand Up @@ -718,18 +718,15 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMVerifier<E, PCS>
// 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(),
));
Expand Down
71 changes: 37 additions & 34 deletions ceno_zkvm/src/tables/ram/ram_impl.rs
View file
Original file line number Diff line number Diff line change
@@ -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},
Expand Down Expand Up @@ -77,8 +82,6 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> NonVolatileTableConfig<NVRAM
NVRAM::RAM_TYPE,
SetTableSpec {
addr_type: SetTableAddrType::FixedAddr,
addr_witin_id: None,
offset: NVRAM::OFFSET_ADDR,
len: NVRAM::len(),
},
init_table,
Expand All @@ -88,8 +91,6 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> NonVolatileTableConfig<NVRAM
NVRAM::RAM_TYPE,
SetTableSpec {
addr_type: SetTableAddrType::FixedAddr,
addr_witin_id: None,
offset: NVRAM::OFFSET_ADDR,
len: NVRAM::len(),
},
final_table,
Expand Down Expand Up @@ -141,26 +142,30 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> NonVolatileTableConfig<NVRAM
set_fixed_val!(row, self.addr, (rec.addr as u64).into());
});

// Select addresses from the range as padding.
let accessed_addrs = init_mem
.iter()
.map(|record| record.addr)
.collect::<HashSet<Addr>>();
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<F>], 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
}

Expand Down Expand Up @@ -251,8 +256,6 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> PubIOTableConfig<NVRAM> {
NVRAM::RAM_TYPE,
SetTableSpec {
addr_type: SetTableAddrType::FixedAddr,
addr_witin_id: None,
offset: NVRAM::OFFSET_ADDR,
len: NVRAM::len(),
},
init_table,
Expand All @@ -262,8 +265,6 @@ impl<NVRAM: NonVolatileTable + Send + Sync + Clone> PubIOTableConfig<NVRAM> {
NVRAM::RAM_TYPE,
SetTableSpec {
addr_type: SetTableAddrType::FixedAddr,
addr_witin_id: None,
offset: NVRAM::OFFSET_ADDR,
len: NVRAM::len(),
},
final_table,
Expand Down Expand Up @@ -368,9 +369,10 @@ impl<DVRAM: DynVolatileRamTable + Send + Sync + Clone> 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,
Expand All @@ -379,9 +381,10 @@ impl<DVRAM: DynVolatileRamTable + Send + Sync + Clone> 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,
Expand Down

0 comments on commit 889973a

Please sign in to comment.