Zero Knowledge Proof — Deep into zkEVM source code (EVM Circuit)

commit 1ec38f207f150733a90081d3825b4de9c3a0a724 (HEAD -> main)
Author: z2trillion <z2trillion@users.noreply.github.com>
Date: Thu Mar 24 15:42:09 2022 -0400

Circuit Structure​

Below is the circuit structure of EVM Circult:

pub fn configure<TxTable, RwTable, BytecodeTable, BlockTable>(
meta: &mut ConstraintSystem<F>,
power_of_randomness: [Expression<F>; 31],
tx_table: TxTable,
rw_table: RwTable,
bytecode_table: BytecodeTable,
block_table: BlockTable,
) -> Self
where
TxTable: LookupTable<F, 4>,
RwTable: LookupTable<F, 11>,
BytecodeTable: LookupTable<F, 4>,
BlockTable: LookupTable<F, 3>,
pub enum FixedTableTag {
Range5 = 1,
Range16,
Range32,
Range256,
Range512,
SignByte,
BitwiseAnd,
BitwiseOr,
BitwiseXor,
ResponsibleOpcode,
}
pub(crate) fn configure<TxTable, RwTable, BytecodeTable, BlockTable>(
meta: &mut ConstraintSystem<F>,
power_of_randomness: [Expression<F>; 31],
fixed_table: [Column<Fixed>; 4],
tx_table: TxTable,
rw_table: RwTable,
bytecode_table: BytecodeTable,
block_table: BlockTable,
) -> Self
where
TxTable: LookupTable<F, 4>,
RwTable: LookupTable<F, 11>,
BytecodeTable: LookupTable<F, 4>,
BlockTable: LookupTable<F, 3>,
{
let q_step = meta.complex_selector();
let q_step_first = meta.complex_selector();
let q_step_last = meta.complex_selector();
let qs_byte_lookup = meta.advice_column();
let advices = [(); STEP_WIDTH].map(|_| meta.advice_column());

What is a Step?

From the view of functions, a Step is a “one-step” execution. From the view of circuit, a Step is a circuit with 32 columns by 16 rows, the step’s parameters are defined in zkevm-circuits/src/evm_circuit/param.rs:

const STEP_WIDTH: usize = 32;
const STEP_HEIGHT: usize = 16;
pub(crate) struct Step<F> {
pub(crate) state: StepState<F>,
pub(crate) rows: Vec<StepRow<F>>,
}
pub(crate) struct StepRow<F> {
pub(crate) qs_byte_lookup: Cell<F>,
pub(crate) cells: [Cell<F>; STEP_WIDTH],
}
pub(crate) struct StepState<F> {
/// The execution state for the step
pub(crate) execution_state: Vec<Cell<F>>,
/// The Read/Write counter
pub(crate) rw_counter: Cell<F>,
/// The unique identifier of call in the whole proof, using the
/// `rw_counter` at the call step.
pub(crate) call_id: Cell<F>,
/// Whether the call is root call
pub(crate) is_root: Cell<F>,
/// Whether the call is a create call
pub(crate) is_create: Cell<F>,
// This is the identifier of current executed bytecode, which is used to
// lookup current executed code and used to do code copy. In most time,
// it would be bytecode_hash, but when it comes to root creation call, the
// executed bytecode is actually from transaction calldata, so it might be
// tx_id if we decide to lookup different table.
// However, how to handle root creation call is yet to be determined, see
// issue https://github.com/appliedzkp/zkevm-specs/issues/73 for more
// discussion.
pub(crate) code_source: Cell<F>,
/// The program counter
pub(crate) program_counter: Cell<F>,
/// The stack pointer
pub(crate) stack_pointer: Cell<F>,
/// The amount of gas left
pub(crate) gas_left: Cell<F>,
/// Memory size in words (32 bytes)
pub(crate) memory_word_size: Cell<F>,
/// The counter for state writes
pub(crate) state_write_counter: Cell<F>,
}
  • execution_state — execution state of current Step, which is defined in step.rs:
pub enum ExecutionState {
// Internal state
BeginTx,
EndTx,
EndBlock,
CopyToMemory,
// Opcode successful cases
STOP,
ADD, // ADD, SUB
...
// Error cases
ErrorInvalidOpcode,
ErrorStackOverflow,
ErrorStackUnderflow,
...
}
  • rw_counter — use rw_counter to distinguish the same address when visiting Stack/Memory
  • call_id — each call of functions is given an id to distinguish from each other
  • is_root — whether it is root or not
  • is_create — whether the call of create is called
  • code_source — the label for calling a program (generally a program’s hash result)
  • program_counter — PC
  • stack_point — Stack pointer
  • gas_left — the amount of gas remaining
  • memory_word_size — memory size (unit as a word (32 byte))
  • state_write_counter — counter of state write
pub(crate) fn new(
meta: &mut ConstraintSystem<F>,
qs_byte_lookup: Column<Advice>,
advices: [Column<Advice>; STEP_WIDTH],
is_next_step: bool,
) -> Self {
let num_state_cells = ExecutionState::amount() + N_CELLS_STEP_STATE;

let mut cells = VecDeque::with_capacity(num_state_cells);
meta.create_gate("Query state for step", |meta| {
for idx in 0..num_state_cells {
let column_idx = idx % STEP_WIDTH;
let rotation = idx / STEP_WIDTH + if is_next_step { STEP_HEIGHT } else { 0 };
cells.push_back(Cell::new(meta, advices[column_idx], rotation));
}

vec![0.expr()]
});

StepState {
execution_state: cells.drain(..ExecutionState::amount()).collect(),
rw_counter: cells.pop_front().unwrap(),
call_id: cells.pop_front().unwrap(),
is_root: cells.pop_front().unwrap(),
is_create: cells.pop_front().unwrap(),
code_source: cells.pop_front().unwrap(),
program_counter: cells.pop_front().unwrap(),
stack_pointer: cells.pop_front().unwrap(),
gas_left: cells.pop_front().unwrap(),
memory_word_size: cells.pop_front().unwrap(),
state_write_counter: cells.pop_front().unwrap(),
}
let mut rows = Vec::with_capacity(STEP_HEIGHT - rotation_offset);
meta.create_gate("Query rows for step", |meta| {
for rotation in rotation_offset..STEP_HEIGHT {
let rotation = rotation + if is_next_step { STEP_HEIGHT } else { 0 };
rows.push(StepRow {
qs_byte_lookup: Cell::new(meta, qs_byte_lookup, rotation),
cells: advices.map(|column| Cell::new(meta, column, rotation)),
});
}

vec![0.expr()]
});
let sum_to_one = (
"Only one of execution_state should be enabled",
step_curr
.state
.execution_state
.iter()
.fold(1u64.expr(), |acc, cell| acc - cell.expr()), // expression -> 1 - sum(state's cells)
);
let bool_checks = step_curr.state.execution_state.iter().map(|cell| {
(
"Representation for execution_state should be bool",
cell.expr() * (1u64.expr() - cell.expr()),
)
});
[
(
"EndTx can only transit to BeginTx or EndBlock",
ExecutionState::EndTx,
vec![ExecutionState::BeginTx, ExecutionState::EndBlock],
),
(
"EndBlock can only transit to EndBlock",
ExecutionState::EndBlock,
vec![ExecutionState::EndBlock],
),
]
.map(|(name, from, to)| {
(
name,
step_curr.execution_state_selector([from])
* (1.expr() - step_next.execution_state_selector(to)),
)
}),
.map(move |(name, poly)| (name, (1.expr() - q_step_last.clone()) * poly))
let _first_step_check = {
let begin_tx_selector =
step_curr.execution_state_selector([ExecutionState::BeginTx]);
iter::once((
"First step should be BeginTx",
q_step_first * (1.expr() - begin_tx_selector),
))
};
let _last_step_check = {
let end_block_selector =
step_curr.execution_state_selector([ExecutionState::EndBlock]);
iter::once((
"Last step should be EndBlock",
q_step_last * (1.expr() - end_block_selector),
))
};
iter::once(sum_to_one)
.chain(bool_checks)
.chain(execution_state_transition)
.map(move |(name, poly)| (name, q_step.clone() * poly))
// TODO: Enable these after test of CALLDATACOPY is complete.
// .chain(first_step_check)
// .chain(last_step_check)

Data range constraint for Advice Column

Every advice’s constraints are within byte range(Range256). Because range constraint is accomplished in fixed_table, and made up of 4 fixed columns. So the range constraint of Range256 corresponds to 4 parts — tag/value, etc.

for advice in advices {
meta.lookup_any("Qs byte", |meta| {
let advice = meta.query_advice(advice, Rotation::cur());
let qs_byte_lookup = meta.query_advice(qs_byte_lookup, Rotation::cur());
vec![
qs_byte_lookup.clone() * FixedTableTag::Range256.expr(), //tag constraint
qs_byte_lookup * advice, //value constraint
0u64.expr(), //ignore
0u64.expr(), //ignore
]
.into_iter()
.zip(fixed_table.table_exprs(meta).to_vec().into_iter())
.collect::<Vec<_>>()
});
}

Gadget Constraint

For every type of Opcode, there’s a corresponding Gadget constraint, which is implemented in the function of configure_gadget:

fn configure_gadget<G: ExecutionGadget<F>>(
meta: &mut ConstraintSystem<F>,
q_step: Selector,
q_step_first: Selector,
power_of_randomness: &[Expression<F>; 31],
step_curr: &Step<F>,
step_next: &Step<F>,
independent_lookups: &mut Vec<Vec<Lookup<F>>>,
presets_map: &mut HashMap<ExecutionState, Vec<Preset<F>>>,
) -> G {
let mut cb = ConstraintBuilder::new(
step_curr,
step_next,
power_of_randomness,
G::EXECUTION_STATE,
);
let gadget = G::configure(&mut cb); let (constraints, constraints_first_step, lookups, presets) = cb.build();
debug_assert!(
presets_map.insert(G::EXECUTION_STATE, presets).is_none(),
"execution state already configured"
);
pub(crate) struct ConstraintBuilder<'a, F> {
pub(crate) curr: &'a Step<F>, //current Step
pub(crate) next: &'a Step<F>, //next Step
power_of_randomness: &'a [Expression<F>; 31],
execution_state: ExecutionState, //execution state
cb: BaseConstraintBuilder<F>, //base builder
constraints_first_step: Vec<(&'static str, Expression<F>)>,
lookups: Vec<(&'static str, Lookup<F>)>,
curr_row_usages: Vec<StepRowUsage>, // current StepRow
next_row_usages: Vec<StepRowUsage>, // next StepRow
rw_counter_offset: Expression<F>, //
program_counter_offset: usize, //PC
stack_pointer_offset: i32, //栈指针
in_next_step: bool, //
condition: Option<Expression<F>>,
}
pub(crate) struct AddGadget<F> {
same_context: SameContextGadget<F>,
add_words: AddWordsGadget<F, 2, false>,
is_sub: PairSelectGadget<F>,
}
let opcode = cb.query_cell();
let a = cb.query_word();
let b = cb.query_word();
let c = cb.query_word();
let add_words = AddWordsGadget::construct(cb, [a.clone(), b.clone()], c.clone());
let is_sub = PairSelectGadget::construct(
cb,
opcode.expr(),
OpcodeId::SUB.expr(),
OpcodeId::ADD.expr(),
);
cb.stack_pop(select::expr(is_sub.expr().0, c.expr(), a.expr()));
cb.stack_pop(b.expr());
cb.stack_push(select::expr(is_sub.expr().0, a.expr(), c.expr()));
let step_state_transition = StepStateTransition {
rw_counter: Delta(3.expr()),
program_counter: Delta(1.expr()),
stack_pointer: Delta(1.expr()),
gas_left: Delta(-OpcodeId::ADD.constant_gas_cost().expr()),
..StepStateTransition::default()
};
let same_context = SameContextGadget::construct(cb, opcode, step_state_transition);
for (row, usage) in self.curr.rows.iter().zip(self.curr_row_usages.iter()) {
if usage.is_byte_lookup_enabled {
constraints.push(("Enable byte lookup", row.qs_byte_lookup.expr() - 1.expr()));
}
presets.extend(
row.cells[usage.next_idx..]
.iter()
.map(|cell| (cell.clone(), F::zero())),
);
presets.push((
row.qs_byte_lookup.clone(),
if usage.is_byte_lookup_enabled {
F::one()
} else {
F::zero()
},
));
}
let execution_state_selector = self.curr.execution_state_selector([self.execution_state]);    (
constraints
.into_iter()
.map(|(name, constraint)| (name, execution_state_selector.clone() * constraint))
.collect(),
self.constraints_first_step
.into_iter()
.map(|(name, constraint)| (name, execution_state_selector.clone() * constraint))
.collect(),
self.lookups
.into_iter()
.map(|(name, lookup)| (name, lookup.conditional(execution_state_selector.clone())))
.collect(),
presets,
)

Stack Constraints

Looking back at the AddGadget constraint, we use cb.stack_pop and cb.stack_push function to execute corresponding Stack Constraints.

pub(crate) fn stack_pop(&mut self, value: Expression<F>) {
self.stack_lookup(false.expr(), self.stack_pointer_offset.expr(), value);
self.stack_pointer_offset += 1;
}
pub(crate) fn stack_push(&mut self, value: Expression<F>) {
self.stack_pointer_offset -= 1;
self.stack_lookup(true.expr(), self.stack_pointer_offset.expr(), value);
}
pub(crate) fn stack_lookup(
&mut self,
is_write: Expression<F>, //write operation?
stack_pointer_offset: Expression<F>, //stack offset
value: Expression<F>,
) {
self.rw_lookup(
"Stack lookup",
is_write,
RwTableTag::Stack,
[
self.curr.state.call_id.expr(),
0.expr(),
self.curr.state.stack_pointer.expr() + stack_pointer_offset,
0.expr(),
value,
0.expr(),
0.expr(),
0.expr(),
],
);
}
fn rw_lookup_with_counter(
&mut self,
name: &'static str,
counter: Expression<F>,
is_write: Expression<F>,
tag: RwTableTag,
values: [Expression<F>; 8],
) {
self.add_lookup(
name,
Lookup::Rw {
counter,
is_write,
tag: tag.expr(),
values,
},
);
}
pub(crate) enum Lookup<F> {
/// Lookup to fixed table, which contains serveral pre-built tables such as
/// range tables or bitwise tables.
Fixed {
...
},
Tx {
...
},
Rw {
...
},
Bytecode {
...
},
Block {
...
},
Conditional {
...
}

Context Constraints

The previous constraints focus on the single Execution State. SameContextGadget are used for constraints between multiple Execution States.

pub(crate) struct SameContextGadget<F> {
opcode: Cell<F>,
sufficient_gas_left: RangeCheckGadget<F, N_BYTES_GAS>,
}
pub(crate) fn construct(
cb: &mut ConstraintBuilder<F>,
opcode: Cell<F>,
step_state_transition: StepStateTransition<F>,
) -> Self {
cb.opcode_lookup(opcode.expr(), 1.expr());
cb.add_lookup(
"Responsible opcode lookup",
Lookup::Fixed {
tag: FixedTableTag::ResponsibleOpcode.expr(),
values: [
cb.execution_state().as_u64().expr(),
opcode.expr(),
0.expr(),
],
},
);
// Check gas_left is sufficient
let sufficient_gas_left = RangeCheckGadget::construct(cb, cb.next.state.gas_left.expr());
// State transition
cb.require_step_state_transition(step_state_transition);
Self {
opcode,
sufficient_gas_left,
}
}

Lookup Constraints

When constraints of each Execution State are ready, let’s start processing all Lookup constraints.

Self::configure_lookup(
meta,
q_step,
fixed_table,
tx_table,
rw_table,
bytecode_table,
block_table,
independent_lookups,
);

EVM Circuit Assign

EVM Circuit uses assign_block to prove all transactions in a Block.

pub fn assign_block(
&self,
layouter: &mut impl Layouter<F>,
block: &Block<F>,
) -> Result<(), Error> {
self.execution.assign_block(layouter, block)
}
self.q_step_first.enable(&mut region, offset)?;            for transaction in &block.txs {
for step in &transaction.steps {
let call = &transaction.calls[step.call_index];
self.q_step.enable(&mut region, offset)?;
self.assign_exec_step(&mut region, offset, block, transaction, call, step)?;
offset += STEP_HEIGHT;
}
}
self.q_step_last.enable(&mut region, offset - STEP_HEIGHT)?;

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Trapdoor-Tech

Trapdoor-Tech

Trapdoor-Tech tries to connect the world with zero-knowledge proof technologies. zk-SNARK/STARK solution and proving acceleration are our first small steps :)