Skip to content
This repository was archived by the owner on Apr 18, 2025. It is now read-only.
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
110 changes: 61 additions & 49 deletions zkevm-circuits/src/evm_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -147,9 +147,10 @@ pub mod test {
witness::{Block, BlockContext, Bytecode, RwMap, Transaction},
EvmCircuit,
},
rw_table::RwTable,
rw_table::RwTableRlc,
util::Expr,
};
use bus_mapping::evm::OpcodeId;
use eth_types::{Field, Word};
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner},
Expand Down Expand Up @@ -187,7 +188,7 @@ pub mod test {
#[derive(Clone)]
pub struct TestCircuitConfig<F> {
tx_table: [Column<Advice>; 4],
rw_table: RwTable,
rw_table: RwTableRlc,
bytecode_table: [Column<Advice>; 5],
block_table: [Column<Advice>; 3],
evm_circuit: EvmCircuit<F>,
Expand Down Expand Up @@ -241,30 +242,11 @@ pub mod test {
layouter.assign_region(
|| "rw table",
|mut region| {
let mut offset = 0;
rws.check_rw_counter_sanity();
// TODO: fix this after cs.challenge() is implemented in halo2
let randomness_phase_next = randomness;
self.rw_table
.assign(&mut region, offset, &Default::default())?;
offset += 1;

let mut rows = rws
.0
.values()
.flat_map(|rws| rws.iter())
.collect::<Vec<_>>();

rows.sort_by_key(|a| a.rw_counter());
let mut expected_rw_counter = 1;
for rw in rows {
assert!(rw.rw_counter() == expected_rw_counter);
expected_rw_counter += 1;

self.rw_table.assign(
&mut region,
offset,
&rw.table_assignment(randomness),
)?;
offset += 1;
}
.assign(&mut region, randomness, rws, randomness_phase_next)?;
Ok(())
},
)
Expand Down Expand Up @@ -352,13 +334,62 @@ pub mod test {
fixed_table_tags: Vec<FixedTableTag>,
}

impl<F> TestCircuit<F> {
impl<F: Field> TestCircuit<F> {
pub fn new(block: Block<F>, fixed_table_tags: Vec<FixedTableTag>) -> Self {
let mut fixed_table_tags = fixed_table_tags;
if fixed_table_tags.is_empty() {
// create fixed_table_tags by trace
let need_bitwise_lookup = block.txs.iter().any(|tx| {
tx.steps.iter().any(|step| {
matches!(
step.opcode,
Some(OpcodeId::AND) | Some(OpcodeId::OR) | Some(OpcodeId::XOR)
)
})
});
fixed_table_tags = FixedTableTag::iter()
.filter(|t| {
!matches!(
t,
FixedTableTag::BitwiseAnd
| FixedTableTag::BitwiseOr
| FixedTableTag::BitwiseXor
) || need_bitwise_lookup
})
.collect();
}
Self {
block,
fixed_table_tags,
}
}

pub fn estimate_k(&self) -> u32 {
let log2_ceil = |n| u32::BITS - (n as u32).leading_zeros() - (n & (n - 1) == 0) as u32;

let k = log2_ceil(
64 + self
.fixed_table_tags
.iter()
.map(|tag| tag.build::<F>().count())
.sum::<usize>(),
);

let num_rows_required_for_steps = TestCircuit::get_num_rows_required(&self.block);
let k = k.max(log2_ceil(64 + num_rows_required_for_steps));

let k = k.max(log2_ceil(
64 + self
.block
.bytecodes
.iter()
.map(|bytecode| bytecode.bytes.len())
.sum::<usize>(),
));

log::debug!("evm circuit uses k = {}", k);
k
}
}

impl<F: Field> Circuit<F> for TestCircuit<F> {
Expand All @@ -371,7 +402,7 @@ pub mod test {

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let tx_table = [(); 4].map(|_| meta.advice_column());
let rw_table = RwTable::construct(meta);
let rw_table = RwTableRlc::construct(meta);
let bytecode_table = [(); 5].map(|_| meta.advice_column());
let block_table = [(); 3].map(|_| meta.advice_column());

Expand Down Expand Up @@ -446,31 +477,12 @@ pub mod test {
block: Block<F>,
fixed_table_tags: Vec<FixedTableTag>,
) -> Result<(), Vec<VerifyFailure>> {
let log2_ceil = |n| u32::BITS - (n as u32).leading_zeros() - (n & (n - 1) == 0) as u32;

let num_rows_required_for_steps = TestCircuit::get_num_rows_required(&block);

let k = log2_ceil(
64 + fixed_table_tags
.iter()
.map(|tag| tag.build::<F>().count())
.sum::<usize>(),
);
let k = k.max(log2_ceil(
64 + block
.bytecodes
.iter()
.map(|bytecode| bytecode.bytes.len())
.sum::<usize>(),
));
let k = k.max(log2_ceil(64 + num_rows_required_for_steps));
log::debug!("evm circuit uses k = {}", k);

let (active_gate_rows, active_lookup_rows) = TestCircuit::get_active_rows(&block);
let circuit = TestCircuit::<F>::new(block.clone(), fixed_table_tags);
let k = circuit.estimate_k();
let power_of_randomness = (1..32)
.map(|exp| vec![block.randomness.pow(&[exp, 0, 0, 0]); (1 << k) - 64])
.collect();
let (active_gate_rows, active_lookup_rows) = TestCircuit::get_active_rows(&block);
let circuit = TestCircuit::<F>::new(block, fixed_table_tags);
let prover = MockProver::<F>::run(k, &circuit, power_of_randomness).unwrap();
prover.verify_at_rows(active_gate_rows.into_iter(), active_lookup_rows.into_iter())
}
Expand Down
68 changes: 61 additions & 7 deletions zkevm-circuits/src/evm_circuit/table.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
use crate::{evm_circuit::step::ExecutionState, impl_expr};
use eth_types::Field;
use halo2_proofs::{
arithmetic::FieldExt,
plonk::{Advice, Column, Expression, Fixed, VirtualCells},
Expand Down Expand Up @@ -158,6 +159,12 @@ pub enum RwTableTag {
TxReceipt,
}

impl Default for RwTableTag {
fn default() -> Self {
RwTableTag::Start
}
}

impl RwTableTag {
pub fn is_reversible(self) -> bool {
return matches!(
Expand Down Expand Up @@ -251,6 +258,43 @@ pub(crate) enum Table {
Byte,
}

#[derive(Clone, Debug)]
pub struct RwValues<F> {
pub id: Expression<F>,
pub address: Expression<F>,
pub field_tag: Expression<F>,
pub storage_key: Expression<F>,
pub value: Expression<F>,
pub value_prev: Expression<F>,
pub aux1: Expression<F>,
pub aux2: Expression<F>,
}

impl<F: Field> RwValues<F> {
#[allow(clippy::too_many_arguments)]
pub fn new(
id: Expression<F>,
address: Expression<F>,
field_tag: Expression<F>,
storage_key: Expression<F>,
value: Expression<F>,
value_prev: Expression<F>,
aux1: Expression<F>,
aux2: Expression<F>,
) -> Self {
Self {
id,
address,
field_tag,
storage_key,
value,
value_prev,
aux1,
aux2,
}
}
}

#[derive(Clone, Debug)]
pub(crate) enum Lookup<F> {
/// Lookup to fixed table, which contains serveral pre-built tables such as
Expand Down Expand Up @@ -285,7 +329,7 @@ pub(crate) enum Lookup<F> {
/// all tags.
tag: Expression<F>,
/// Values corresponding to the tag.
values: [Expression<F>; 8],
values: RwValues<F>,
},
/// Lookup to bytecode table, which contains all used creation code and
/// contract code.
Expand Down Expand Up @@ -322,7 +366,7 @@ pub(crate) enum Lookup<F> {
Conditional(Expression<F>, Box<Lookup<F>>),
}

impl<F: FieldExt> Lookup<F> {
impl<F: Field> Lookup<F> {
pub(crate) fn conditional(self, condition: Expression<F>) -> Self {
Self::Conditional(condition, self.into())
}
Expand Down Expand Up @@ -353,11 +397,21 @@ impl<F: FieldExt> Lookup<F> {
is_write,
tag,
values,
} => [
vec![counter.clone(), is_write.clone(), tag.clone()],
values.to_vec(),
]
.concat(),
} => {
vec![
counter.clone(),
is_write.clone(),
tag.clone(),
values.id.clone(),
values.address.clone(),
values.field_tag.clone(),
values.storage_key.clone(),
values.value.clone(),
values.value_prev.clone(),
values.aux1.clone(),
values.aux2.clone(),
]
}
Self::Bytecode {
hash,
tag,
Expand Down
Loading