Zero Knowledge Proof — Deep into zkEVM source code (EVM Circuit)
zkEVM is a kind of complicated Zero-Knowledge Proof application, it’s worth reading and learning its source code over and over again.
https://github.com/appliedzkp/zkevm-circuits.git
The last commit version of the source code used in this article is shown below:
commit 1ec38f207f150733a90081d3825b4de9c3a0a724 (HEAD -> main)
Author: z2trillion <z2trillion@users.noreply.github.com>
Date: Thu Mar 24 15:42:09 2022 -0400zkEVM Circuit mainly consists of 2 circuits: EVM Circuit and State Circuit. Firstly the source code of EVM Circuit will be explained in this article. The other part will be explained in a subsequent article. Let’s analyze the design for each column, how to constrain each Opcode, and how to constrain and combine multiple Opcodes in detail.
Circuit Structure
Below is the circuit structure of EVM Circult:
From the view of the Column, EVM Circuit is divided into 3 parts: 1/Step Selector (including the current step, first step, the last step, etc.) 2/Step Circuit, and 3/ Fixed Table (fixed lookup table). Step Circuit logic is the core part. Step is the execution step from the circuit constraints’ point of view. This section is divided into 2 parts: a/ Execution state (Step state selector) b/ Constraints of execution states. Constraint modules are labeled out with the dashed lines in the figure.
To understand EVM Circuit, it’s easier to start with the code of Configure and Assign.
EVM Circuit Configure
EVM Circuit is implemented in zkevm-circuits/src/evm_circuit.rs. Let’s start from its configure function:
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>,The EVM Circuit constraint has 2 parts: 1/ fixed_table 2/ ExecutionConfig. Fixed_table is some fixed table information, taking up 4 columns, and corresponding to tag/value1/value2/result.
There are 10 types of tag, their definitions are in zkevm-circuits/src/evm_circuit/table.rs:
pub enum FixedTableTag {
Range5 = 1,
Range16,
Range32,
Range256,
Range512,
SignByte,
BitwiseAnd,
BitwiseOr,
BitwiseXor,
ResponsibleOpcode,
}Let’s look at the Execution section next. ExecutionConfig’s configure function defines other constraints of the circuit:
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>,
{q_step — Step selector
q_step_first — first Step selector
q_step_last — last Step selector
qs_byte_lookup — byte range check’s selector
For a Step, we define its constraints with 32 Columns.
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;A Step’s definition could be found in zkevm-circuits/src/evm_circuit/step.rs:
pub(crate) struct Step<F> {
pub(crate) state: StepState<F>,
pub(crate) rows: Vec<StepRow<F>>,
}A Step consists of StepState and 16 StepRows. First, a Step Row has all the information involved in a particular Row of a Step:
pub(crate) struct StepRow<F> {
pub(crate) qs_byte_lookup: Cell<F>,
pub(crate) cells: [Cell<F>; STEP_WIDTH],
}For one particular Row in a Step, except for the cells’ data(cells), there should also be the corresponding qs_byte_lookup for that Row to check whether the cell’s data of the Row should be constrained by Range256(qs_byte_lookup will be explained later in detail).
StepState’s data structure contains state information of the Step:
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>,
}Let’s check each StepState variable’s definition.
- 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,
...
}Execution state of Step includes internal state(transactions in a block isolated by BeginTX and EndTx), successful execution state and error state of Opcode. Opcode’s successful execution state can be represented by a constraint that fits the case. In other words, by the same constraint, the execution states of multiple Opcodes can be represented. For example, if both ADD and SUB Opcodes use one constraint, then they can apply the same constraint to each execution state.
- 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
A closer look at the Step construction function (new) shows that StepState and StepRow are created separately when creating a Step.
pub(crate) fn new(
meta: &mut ConstraintSystem<F>,
qs_byte_lookup: Column<Advice>,
advices: [Column<Advice>; STEP_WIDTH],
is_next_step: bool,
) -> Self {The logic to create a StepState is shown below:
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(),
}N_CELLS_STEP_STATE=10 is the number of Cells in the StepState other than the execution_state.
According to the 32 columns by 16 rows, create the corresponding Cells to advise these Columns. It is critical to understand what these Cells represent, Rotation(offset) is used to distinguish different Cells in the same Column. When writing circuits, pay special attention to the abstraction and description of the Cells, these modularized circuits may use multiple instances. Now the circuit constraints of a Step can be accurately described with these Cells for the StepState and their corresponding q_step selectors. Basically, the q_step selectors constrain the rows and the Cell in the Step is located by Rotation (relative offset).
The logic to create a StepRow is shown below:
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()]
});Each row under the StepState is called StepRow.
Custom Gate Constraints
Custom Gate Constraints is more complicated, including:
a. Every Step’s execution_state has only one valid state:
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)
);The implementation is to add up the values of all the Cell’s states. The sum_to_one is a 1-sum expression.
b. Every Step’s execution_state is boolean:
let bool_checks = step_curr.state.execution_state.iter().map(|cell| {
(
"Representation for execution_state should be bool",
cell.expr() * (1u64.expr() - cell.expr()),
)
});Thus it’s a common method to check the boolean value with the expression x*(1-x).
c. The ExecutionState of two adjacent Steps should satisfy transition constraints: e.g. the ExecutionState has to be BeginTx or EndBlock after the EndTx.
[
(
"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)),
)
}),Note that the ExecutionState of last Step doesn’t need to satisfy these adjacent constraints.
.map(move |(name, poly)| (name, (1.expr() - q_step_last.clone()) * poly))d. The ExecutionState of first Step must be BeginTx, and the last one has to be EndBlock:
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),
))
};
Note that these custom gate constraints shown above are only for one Step. So the q_step constraints should be added to all constraints.
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)The current version of the code is not the final, first_step_check and last_step_check are commented out. From TODO, we can tell that these constraints will be added after finishing testing CALLDATACOPY.
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<_>>()
});
}
Until now, we have the circuit’s basic structure including 3 main Column types, circuit range of each Step, internal constraints of each execution state and transition constraints between two execution states.
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 {For every Gadget constraint, there’s a class of ConstraintBuilder:
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"
);
So firstly we can create an instance of ConstraintBuilder using ConstraintBuilder::new. For every type of Gadget, use their corresponding configure function, and then use ConstraintBuilder’s build function to finish the constraint configuration.
Let’s start from ConstraintBuilder’s definition. ConstraintBuilder’s definition is in zkevm-circuits/src/evm_circuit/util/constraint_builder.rs:
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>>,
}a. ConstraintBuilder::new
Create a ConstraintBuilder’s instance.
b. G::configure
All Opcode related Gadget codes are under zkevm-circuits/src/evm_circuit/execution/. Currently, more than thirty types of Gadget are supported, which means more than thirty types of execution_states are supported. The following is the implementation of AddGadget.
pub(crate) struct AddGadget<F> {
same_context: SameContextGadget<F>,
add_words: AddWordsGadget<F, 2, false>,
is_sub: PairSelectGadget<F>,
}AddGadget is dependent upon 3 other Gadgets: SameContextGadget (Context Constraint)，AddWordsGadget (Words add up) and PairSelectGadget(choose a or b). Through AddGadget’s configure function, we can check out the related constraints.
1/ Access the Opcode and the a/b/c in each Cell via cb.query_cell and cb.query_word
let opcode = cb.query_cell();
let a = cb.query_word();
let b = cb.query_word();
let c = cb.query_word();2/ Construct additive constraint(turn subtraction into addition)
let add_words = AddWordsGadget::construct(cb, [a.clone(), b.clone()], c.clone());3/ Check whether opcode is ADD or SUB
let is_sub = PairSelectGadget::construct(
cb,
opcode.expr(),
OpcodeId::SUB.expr(),
OpcodeId::ADD.expr(),
);4/ Constrain the changes of Stack
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()));5/ Constrain the transition of Context
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);Be aware, all constraints are stored in the cb.constraints variable in the end.
c. cb.build
cb.build is to correct and edit every Gadget. For every Row in current Step:
1/ If there’s no Cell used, then constrain the cell to be 0
2/ If need to check the range, use qs_byte_lookup to check
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()
},
));
}
For the current Step’s constraints or lookup table, add on its execution_state selector.
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,
)
Now, we have the Step’s constraint structure. ExecuteState is a possible execution state. For qs_step, execute_state’s relative/corresponding location is fixed. Also, every Cell value of execute_state must be boolean, and only 1 execution state is valid. Every execution state has its own corresponding Gadget circuit. The execution_state_selector should be added to all Gadget circuits in cb.build function. In other words, the whole EVM Circuit contains all execution_state constraints.
Before looking into the Lookup constraints, let’s talk about Stack Constraints and Context Constraints.
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);
}
stack_pop and stack_push have similar implementations, they both edit stack_pointer_offset and constrain the value at the location of stack_pointer_offset in Stack through stack_lookup.
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(),
],
);
}The core part is rw_loopup, and the implementation of rw_loopup is based on rw_lookup_with_counter. The access to Stack consists of call_id, Stack_offset, and rw count. In the same Step State, it’s possible to read and write several times at the same Stack_offset, so it’s necessary to constrain the times of read and write.
How to implement rw_loopup_with_counter? The lookup table is recorded in ConstraintBuilder’s lookups variable through add_lookup for the lookup table’s Configure.
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,
},
);
}Except for the RW lookup table, currently, more types of lookup tables are supported. Lookup enumeration types are defined in zkevm-circuits/src/evm_circuit/table.rs:
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 {
...
}Tx lookup table constraint transaction data, RW lookup table constraints readable and writable data access(Stack/Memory), Bytecode constraints execution programs, and Block constraints block data.
Looking back at the Stack constraint implementation. For each Step, it’s possible to operate Stack or Memory. To constrain these operations, we also need to assign Stack Pointer other than Cells for the data. When the Stack Pointer is assigned, the Stack operation within a Step can be independently constrained. Also, the Cells related to Stack Pointer can be located in the Step via q_step. In other words, constraints can be independently expressed for a Step. Of course, other than constraints for one single Step, there are Stack constraints of data consistency and accuration between multiple Steps. These constraints can be defined by “Lookup constraints”(please check out the Lookup constraints chapter).
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>,
}The specific constraint is implemented in the contruct function:
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,
}
}
The logic is simple and clear, having the following constraints:
1/ opcode_lookup — constrain PC has the same corresponding opcodes
2/ add_lookup — constrain consistency between opcode and execution state in the Step
3/ Check gas_left is sufficient
4/ require_step_state_transition — constrain the State transition between two Steps, e.g. the relations between PCs, Stack Pointers, Call ids, etc.
Please check the source code if you are interested.
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,
);The implementation is simple. Every Lookup constraints not only need to add q_step constraints, but also add various table constraints. Independent_lookups is the extra constraint in a Step.
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)
}In assign_block, it sets up q_step_first and q_step_last, also constrains every Tx in the 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)?;
A Tx’s steps are stored in the steps variable. For each Step, use assign_exec_step to assign. Based on the understanding of Configure, these parts are easier to process. If you are interested, please check out the source codes.
That’s all for EVM Circuit, the upcoming articles will talk about State Circuit and Bytecode Circuit.
