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

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

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,
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
Config::configure(meta)
}

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);

Key Relationship Constraints

In constraint circuit, there are two types of Key relationships that need to be checked:

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],
)
});
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:

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))
});
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)
});

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.

--

--

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 :)