Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Commit

Permalink
reserve rw_table first row to be constraints by pi
Browse files Browse the repository at this point in the history
  • Loading branch information
@hero78119
hero78119 committed Oct 4, 2023
1 parent 554789c commit 43ed90e
Show file tree
Hide file tree
Showing 8 changed files with 121 additions and 83 deletions.
9 changes: 8 additions & 1 deletion circuit-benchmarks/src/state_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,14 @@ mod tests {
.parse()
.expect("Cannot parse DEGREE env var as u32");

let empty_circuit = StateCircuit::<Fr>::new(RwMap::default(), 1 << 16);
let empty_circuit = StateCircuit::<Fr>::new(
RwMap::default(),
1 << 16,
Fr::from(1),
Fr::from(1),
Fr::from(1),
Fr::from(1),
);

// Initialize the polynomial commitment parameters
let mut rng = XorShiftRng::from_seed([
Expand Down
43 changes: 28 additions & 15 deletions gadgets/src/permutation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,13 @@ pub struct PermutationChipConfig<F> {
_phantom: PhantomData<F>,
}

type PermutationAssignedCells<F> = (
AssignedCell<F, F>,
AssignedCell<F, F>,
AssignedCell<F, F>,
AssignedCell<F, F>,
);

impl<F: Field> PermutationChipConfig<F> {
/// assign
pub fn assign(
Expand All @@ -41,15 +48,8 @@ impl<F: Field> PermutationChipConfig<F> {
prev_continuous_fingerprint: Value<F>,
_next_continuous_fingerprint: Value<F>,
col_values: &Vec<Vec<Value<F>>>,
) -> Result<
(
AssignedCell<F, F>,
AssignedCell<F, F>,
AssignedCell<F, F>,
AssignedCell<F, F>,
),
Error,
> {
) -> Result<PermutationAssignedCells<F>, Error> {
self.annotate_columns_in_region(region, "state_circuit");
let mut offset = 0;
let alpha_first_cell = region.assign_advice(
|| format!("alpha at index {}", offset),
Expand All @@ -72,11 +72,9 @@ impl<F: Field> PermutationChipConfig<F> {

let power_of_gamma = {
let num_of_col = col_values.get(0).map(|x| x.len()).unwrap_or_default();
std::iter::successors(Some(Value::known(F::ONE)), |prev| {
(prev.clone() * gamma.clone()).into()
})
.take(num_of_col)
.collect::<Vec<Value<F>>>()
std::iter::successors(Some(Value::known(F::ONE)), |prev| (*prev * gamma).into())
.take(num_of_col)
.collect::<Vec<Value<F>>>()
};

offset += 1;
Expand All @@ -94,8 +92,9 @@ impl<F: Field> PermutationChipConfig<F> {
.fold(Value::known(F::ZERO), |prev, cur| {
prev.zip(cur).map(|(a, b)| a + b)
});
alpha.zip(tmp).map(|(alpha, perf_term)| alpha - perf_term)
alpha.zip(tmp).map(|(alpha, tmp)| alpha - tmp)
};

fingerprints = fingerprints.zip(perf_term).map(|(prev, cur)| prev * cur);
let fingerprint_cell = region.assign_advice(
|| format!("fingerprint at index {}", offset),
Expand Down Expand Up @@ -134,6 +133,20 @@ impl<F: Field> PermutationChipConfig<F> {
last_fingerprint_cell.unwrap(),
))
}

/// Annotates columns of this gadget embedded within a circuit region.
pub fn annotate_columns_in_region(&self, region: &mut Region<F>, prefix: &str) {
[
(
self.fingerprints,
"GADGETS_PermutationChipConfig_fingerprints",
),
(self.gamma, "GADGETS_PermutationChipConfig_gamma"),
(self.alpha, "GADGETS_PermutationChipConfig_alpha"),
]
.iter()
.for_each(|(col, ann)| region.name_column(|| format!("{}_{}", prefix, ann), *col));
}
}

/// permutation fingerprint gadget
Expand Down
40 changes: 22 additions & 18 deletions zkevm-circuits/src/evm_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,10 @@ impl<F: Field> SubCircuitConfig<F> for EvmCircuitConfig<F> {
u8_table.annotate_columns(meta);
u16_table.annotate_columns(meta);

<RwTable as LookupTable<F>>::columns(&rw_table)
.iter()
.for_each(|c| meta.enable_equality(*c));

let rw_permutation_config = PermutationChip::configure(
meta,
<RwTable as LookupTable<F>>::advice_columns(&rw_table),
Expand Down Expand Up @@ -299,25 +303,22 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {
config.execution.assign_block(layouter, block, challenges)?;

let rw_rows = block.rws.table_assignments(true);
let (rw_table_row_first, rw_table_row_last) = layouter.assign_region(
|| "evm circuit",
|mut region| {
config
.rw_table
.load_with_region(&mut region, &rw_rows, rw_rows.len())
},
)?;

// permutation cells
let (
alpha_cell,
gamma_cell,
prev_continuous_fingerprint_cell,
next_continuous_fingerprint_cell,
(rw_table_row_first, rw_table_row_last),
(
alpha_cell,
gamma_cell,
prev_continuous_fingerprint_cell,
next_continuous_fingerprint_cell,
),
) = layouter.assign_region(
|| "rw permutation fingerprint",
|| "evm circuit",
|mut region| {
config.rw_permutation_config.assign(
let rw_table_first_n_last_cells =
config
.rw_table
.load_with_region(&mut region, &rw_rows, rw_rows.len())?;
let permutation_cells = config.rw_permutation_config.assign(
&mut region,
Value::known(block.permu_alpha),
Value::known(block.permu_gamma),
Expand All @@ -327,6 +328,7 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {
.rws
.table_assignments(true)
.iter()
.skip(1) // skip first row since it's used for permutation
.map(|row| {
row.table_assignment::<F>()
.unwrap()
Expand All @@ -337,9 +339,11 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {
.collect::<Vec<Value<F>>>()
})
.collect::<Vec<Vec<Value<F>>>>(),
)
)?;
Ok((rw_table_first_n_last_cells, permutation_cells))
},
)?;

// constrain permutation challenges
[alpha_cell, gamma_cell]
.iter()
Expand Down Expand Up @@ -370,7 +374,7 @@ impl<F: Field> SubCircuit<F> for EvmCircuit<F> {
let block = self.block.as_ref().unwrap();
let rws_assignments = block.rws.table_assignments(true);

assert!(rws_assignments.len() > 0);
assert!(!rws_assignments.is_empty());

let rws_values = [0, rws_assignments.len() - 1] // get first/last row and concat
.iter()
Expand Down
81 changes: 42 additions & 39 deletions zkevm-circuits/src/state_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,10 @@ impl<F: Field> SubCircuitConfig<F> for StateCircuitConfig<F> {
u10_table.annotate_columns(meta);
u16_table.annotate_columns(meta);

<RwTable as LookupTable<F>>::columns(&rw_table)
.iter()
.for_each(|c| meta.enable_equality(*c));

let pi_pre_continuity = meta.instance_column();
let pi_next_continuity = meta.instance_column();
let pi_permutation_challenges = meta.instance_column();
Expand Down Expand Up @@ -205,9 +209,7 @@ impl<F: Field> SubCircuitConfig<F> for StateCircuitConfig<F> {
constraint_builder.build(&queries);
constraint_builder.gate(queries.selector)
});
for (name, lookup) in constraint_builder.lookups() {
meta.lookup_any(name, |_| lookup);
}
constraint_builder.lookups(meta, config.selector);

config
}
Expand Down Expand Up @@ -255,11 +257,12 @@ impl<F: Field> StateCircuitConfig<F> {
log::trace!("state circuit assign offset:{} row:{:#?}", offset, row);
}

// disable selector on offset 0 since it will be copy constraints by public input
region.assign_fixed(
|| "selector",
self.selector,
offset,
|| Value::known(F::ONE),
|| Value::known(if offset == 0 { F::ZERO } else { F::ONE }),
)?;

tag_chip.assign(region, offset, &row.tag())?;
Expand Down Expand Up @@ -532,15 +535,47 @@ impl<F: Field> SubCircuit<F> for StateCircuit<F> {
// Assigning to same columns in different regions should be avoided.
// Here we use one single region to assign `overrides` to both rw table and
// other parts.
let (rw_table_row_first, rw_table_row_last) = layouter.assign_region(
let (
(rw_table_row_first, rw_table_row_last),
(
alpha_cell,
gamma_cell,
prev_continuous_fingerprint_cell,
next_continuous_fingerprint_cell,
),
) = layouter.assign_region(
|| "state circuit",
|mut region| {
// TODO Below RwMap::table_assignments_prepad call 3 times, refactor to be more
// efficient
let rw_table_first_n_last_cells =
config
.rw_table
.load_with_region(&mut region, &self.rows, self.n_rows)?;

config.assign_with_region(&mut region, &self.rows, &self.updates, self.n_rows)?;

let (rows, _) = RwMap::table_assignments_prepad(&self.rows, self.n_rows);

let permutation_cells = config.rw_permutation_config.assign(
&mut region,
Value::known(self.permu_alpha),
Value::known(self.permu_gamma),
Value::known(self.permu_prev_continuous_fingerprint),
Value::known(self.permu_next_continuous_fingerprint),
&rows
.iter()
.skip(1) // skip first row since it's used for permutation
.map(|row| {
row.table_assignment::<F>()
.unwrap()
.values()
.iter()
.map(|f| Value::known(*f))
.collect::<Vec<Value<F>>>()
})
.collect::<Vec<Vec<Value<F>>>>(),
)?;
#[cfg(test)]
{
let first_non_padding_index = if self.rows.len() < self.n_rows {
Expand All @@ -564,39 +599,7 @@ impl<F: Field> SubCircuit<F> for StateCircuit<F> {
}
}

Ok(rw_table_first_n_last_cells)
},
)?;

// permutation cells
let (
alpha_cell,
gamma_cell,
prev_continuous_fingerprint_cell,
next_continuous_fingerprint_cell,
) = layouter.assign_region(
|| "rw permutation fingerprint",
|mut region| {
config.rw_permutation_config.assign(
&mut region,
Value::known(self.permu_alpha),
Value::known(self.permu_gamma),
Value::known(self.permu_prev_continuous_fingerprint),
Value::known(self.permu_next_continuous_fingerprint),
&self
.rows
.iter()
.map(|row| {
row.table_assignment::<F>()
.unwrap()
.values()
.to_vec()
.iter()
.map(|f| Value::known(*f))
.collect::<Vec<Value<F>>>()
})
.collect::<Vec<Vec<Value<F>>>>(),
)
Ok((rw_table_first_n_last_cells, permutation_cells))
},
)?;
// constrain permutation challenges
Expand Down Expand Up @@ -625,7 +628,7 @@ impl<F: Field> SubCircuit<F> for StateCircuit<F> {
}

fn instance(&self) -> Vec<Vec<F>> {
assert!(self.rows.len() > 0);
assert!(!self.rows.is_empty());

let rws_values = [0, self.rows.len() - 1] // get first/last row and concat
.iter()
Expand Down
17 changes: 14 additions & 3 deletions zkevm-circuits/src/state_circuit/constraint_builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@ use crate::{
use bus_mapping::operation::Target;
use eth_types::Field;
use gadgets::binary_number::BinaryNumberConfig;
use halo2_proofs::plonk::Expression;
use halo2_proofs::{
plonk::{Column, ConstraintSystem, Expression, Fixed},
poly::Rotation,
};
use strum::IntoEnumIterator;

#[derive(Clone)]
Expand Down Expand Up @@ -109,8 +112,16 @@ impl<F: Field> ConstraintBuilder<F> {
.collect()
}

pub fn lookups(&self) -> Vec<Lookup<F>> {
self.lookups.clone()
pub fn lookups(&self, meta: &mut ConstraintSystem<F>, selector: Column<Fixed>) {
self.lookups.iter().cloned().for_each(|(name, mut lookup)| {
meta.lookup_any(name, |meta| {
let selector = meta.query_fixed(selector, Rotation::cur());
for (expression, _) in lookup.iter_mut() {
*expression = expression.clone() * selector.clone();
}
lookup
});
});
}

pub fn build(&mut self, q: &Queries<F>) {
Expand Down
5 changes: 1 addition & 4 deletions zkevm-circuits/src/state_circuit/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,10 +57,7 @@ fn test_state_circuit_ok(
let instance = circuit.instance();

let prover = MockProver::<Fr>::run(19, &circuit, instance);
let verify_result = prover
.map_err(|err| println!("{:?}", err))
.unwrap()
.verify();
let verify_result = prover.map_err(|err| println!("{}", err)).unwrap().verify();
assert_eq!(verify_result, Ok(()));
}

Expand Down
2 changes: 1 addition & 1 deletion zkevm-circuits/src/super_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ impl<F: Field> SubCircuitConfig<F> for SuperCircuitConfig<F> {
meta,
CopyCircuitConfigArgs {
tx_table: tx_table.clone(),
rw_table: chronological_rw_table.clone(),
rw_table: chronological_rw_table,
bytecode_table: bytecode_table.clone(),
copy_table,
q_enable: q_copy_table,
Expand Down
7 changes: 5 additions & 2 deletions zkevm-circuits/src/table/rw_table.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,9 @@ impl<F: Field> LookupTable<F> for RwTable {
]
}
}

type RwTableFirstNLastAssignedCell<F> = (Vec<AssignedCell<F, F>>, Vec<AssignedCell<F, F>>);

impl RwTable {
/// Construct a new RwTable
pub fn construct<F: Field>(meta: &mut ConstraintSystem<F>) -> Self {
Expand Down Expand Up @@ -129,7 +132,7 @@ impl RwTable {
layouter: &mut impl Layouter<F>,
rws: &[Rw],
n_rows: usize,
) -> Result<(Vec<AssignedCell<F, F>>, Vec<AssignedCell<F, F>>), Error> {
) -> Result<RwTableFirstNLastAssignedCell<F>, Error> {
layouter.assign_region(
|| "rw table",
|mut region| self.load_with_region(&mut region, rws, n_rows),
Expand All @@ -141,7 +144,7 @@ impl RwTable {
region: &mut Region<'_, F>,
rws: &[Rw],
n_rows: usize,
) -> Result<(Vec<AssignedCell<F, F>>, Vec<AssignedCell<F, F>>), Error> {
) -> Result<RwTableFirstNLastAssignedCell<F>, Error> {
let mut assigned_cells = vec![];
let (rows, _) = RwMap::table_assignments_prepad(rws, n_rows);
for (offset, row) in rows.iter().enumerate() {
Expand Down

0 comments on commit 43ed90e

Please sign in to comment.