Zero Knowledge Proof — Deep into zkEVM source code (State 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 -0400The previous article talked about the zkEVM EVM Circuit, let’s move on to the State Circuit today.
State Circuit Configure
The State Circuit implements the constraints of Stack, Memory, and Storage in zkevm-circuits/src/state_circuit/state.rs.
pub struct StateCircuit<
F: FieldExt,
const SANITY_CHECK: bool,
const RW_COUNTER_MAX: usize,
const MEMORY_ADDRESS_MAX: usize,
const STACK_ADDRESS_MAX: usize,
const ROWS_MAX: usize,
> {
/// randomness used in linear combination
pub randomness: F,
/// witness for rw map
pub rw_map: RwMap,
}StateCircuit’s configure is implemented by configure function in Config.
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
Config::configure(meta)
}The overall circuit strcture of StateCircuit is shown below:
First, let’s focus on the keys. State Circuit constraints are mostly based on key-value constraints. The keys use 5 columns to be compatible with the Key information of Memory, Stack and Storage.
keys[0] — tag
keys[1] — reserved
keys[2] — account address(memory/stack: 0)
keys[3] — address
keys[4] — storage key(memory/stack: 0)
Key[2] and key[4] are for Storage.
The Storage constraint information is not complete. Memory and Stack have similar constraints. This article will talk about Stack constraint implementation in detail. But before that, let’s go over the structure to organize information for Memory/Stack/Storage.
All witness informations are sorted according to key3 (address). The read/write operation of the same address are sorted according to the rw counter.
Tag Classification
Tag classification includes Memory, Stack and Storage. Different constraint method should be applied to different classification.
let q_tag_is = |meta: &mut VirtualCells<F>, tag_value: usize| {
let tag_cur = meta.query_advice(tag, Rotation::cur());
let all_possible_values = EMPTY_TAG..=STORAGE_TAG;
generate_lagrange_base_polynomial(tag_cur, tag_value, all_possible_values)
};
let q_memory = |meta: &mut VirtualCells<F>| q_tag_is(meta, MEMORY_TAG);
let q_stack = |meta: &mut VirtualCells<F>| q_tag_is(meta, STACK_TAG);
let q_storage = |meta: &mut VirtualCells<F>| q_tag_is(meta, STORAGE_TAG);q_tag_is is a Lagrange polynomial that outputs 1 for some Tag and 0 for others. The three types of polynomials are q_memory/q_stack/q_storage.
Key Relationship Constraints
In constraint circuit, there are two types of Key relationships that need to be checked:
1/ Whether the previous and current keys are the same
let key_is_same_with_prev: [IsZeroConfig<F>; 5] = [0, 1, 2, 3, 4].map(|idx| {
IsZeroChip::configure(
meta,
|meta| meta.query_fixed(s_enable, Rotation::cur()),
|meta| {
let value_cur = meta.query_advice(keys[idx], Rotation::cur());
let value_prev = meta.query_advice(keys[idx], Rotation::prev());
value_cur - value_prev
},
keys_diff_inv[idx],
)
});2/ Whether all the keys are the same.
let q_all_keys_same = |_meta: &mut VirtualCells<F>| {
key_is_same_with_prev[0].is_zero_expression.clone()
* key_is_same_with_prev[1].is_zero_expression.clone()
* key_is_same_with_prev[2].is_zero_expression.clone()
* key_is_same_with_prev[3].is_zero_expression.clone()
* key_is_same_with_prev[4].is_zero_expression.clone()
};
let q_not_all_keys_same = |meta: &mut VirtualCells<F>| one.clone() - q_all_keys_same(meta);General Constraints
Whether it is Memory, Stack, or Storage, there’re some general constraints for all of them:
1/ is_write must be a boolean
2/ The data read from the same adress must be the same as the previous row of data. The previous row of data is either read from the same address, or write into the same adress.
cb.require_boolean("is_write should be boolean", is_write);
cb.require_zero(
"if read and keys are same, value should be same with prev",
q_all_keys_same(meta) * is_read * (value_cur - value_prev),
);
cb.gate(s_enable)RWC Constraint
For the read and write operations at the same address, RW counter increases ((rw_counter — rw_counter_prev -1) > 0). Which is defined below in lookup.
meta.lookup_any("rw counter monotonicity", |meta| {
let s_enable = meta.query_fixed(s_enable, Rotation::cur());
let rw_counter_table = meta.query_fixed(rw_counter_table, Rotation::cur());
let rw_counter_prev = meta.query_advice(rw_counter, Rotation::prev());
let rw_counter = meta.query_advice(rw_counter, Rotation::cur());
vec![(
s_enable * q_all_keys_same(meta)
* (rw_counter - rw_counter_prev - one.clone()), /*
* - 1 because it needs to
* be strictly monotone */
rw_counter_table,
)]
});Stack Constraint
When the Stack pointer changes, the first operation must be the write operation.
meta.create_gate("Stack operation", |meta| {
let mut cb = new_cb();
let s_enable = meta.query_fixed(s_enable, Rotation::cur());
let is_write = meta.query_advice(is_write, Rotation::cur());
let q_read = one.clone() - is_write;
let key2 = meta.query_advice(keys[2], Rotation::cur());
let key4 = meta.query_advice(keys[4], Rotation::cur());
cb.require_zero("key2 is 0", key2);
cb.require_zero("key4 is 0", key4);
cb.require_zero(
"if address changes, operation is always a write",
q_not_all_keys_same(meta) * q_read,
);
cb.gate(s_enable * q_stack(meta))
});Stack address must be within a certain range, and the difference between Stack Pointers cannot exceed 1.
meta.lookup_any("Stack address in allowed range", |meta| {
let q_stack = q_stack(meta);
let address_cur = meta.query_advice(address, Rotation::cur());
let stack_address_table_zero =
meta.query_fixed(stack_address_table_zero, Rotation::cur());
vec![(q_stack * address_cur, stack_address_table_zero)]
});
meta.create_gate("Stack pointer diff be 0 or 1", |meta| {
let mut cb = new_cb();
let s_enable = meta.query_fixed(s_enable, Rotation::cur());
let q_stack = q_stack(meta);
let tag_is_same_with_prev = key_is_same_with_prev[0].is_zero_expression.clone();
let call_id_same_with_prev = key_is_same_with_prev[1].is_zero_expression.clone();
let stack_ptr = meta.query_advice(keys[3], Rotation::cur());
let stack_ptr_prev = meta.query_advice(keys[3], Rotation::prev());
cb.require_boolean(
"stack pointer only increases by 0 or 1",
stack_ptr - stack_ptr_prev,
);
cb.gate(s_enable * q_stack * tag_is_same_with_prev * call_id_same_with_prev)
});Now, that’s it for Stack constraints. Let’s take a look at the assign implementation.
State Circuit Assign
All witness informations are stored in the rw_map variables. After filtering out the “Memory/Stack/AccountStorage” information, sort them out according to the key and rw_counter. Assign informations to every rows using the assign_row function.
layouter.assign_region(
|| "State operations",
|mut region| {
// TODO: a "START_TAG" row should be inserted before all other rows in the final
// implmentation. Here we start from 1 to prevent some
// col.prev() problems since blinding rows are unavailable for constaints.
let mut offset = 1;
let mut rows: Vec<RwRow<F>> = [
RwTableTag::Memory,
RwTableTag::Stack,
RwTableTag::AccountStorage,
]
.iter()
.map(|tag| {
rw_map.0[tag]
.iter()
.map(|rw| rw.table_assignment(randomness))
})
.flatten()
.collect();
rows.sort_by_key(|rw| (rw.tag, rw.key1, rw.key2, rw.key3, rw.key4, rw.rw_counter));
if rows.len() >= ROWS_MAX {
panic!("too many storage operations");
}
for (index, row) in rows.iter().enumerate() {
let row_prev = if index == 0 {
RwRow::default()
} else {
rows[index - 1]
};
self.assign_row(
&mut region,
offset,
*row,
row_prev,
&key_is_same_with_prev_chips,
)?;
offset += 1;
}
Ok(())
},
)What does the EVM/State Circuit prove?
The EVM/State Circuit proves the correct execution of the program and proves that the read and write operations to the Memory/Stack are reasonable and correct.
There are some components not yet proved other than these two circuits: 1/ Consistency of execution 2/ Correctness of the Storage state. We’ll talk more about these later.
