From a7ecc3dd478c67a8db92c56874f68170b7b8b3c6 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 16:59:41 -0400 Subject: [PATCH 01/51] Add BinaryNumber chip --- zkevm-circuits/src/state_circuit.rs | 24 ++-- .../src/state_circuit/binary_number.rs | 114 ++++++++++++++++++ .../state_circuit/lexicographic_ordering.rs | 14 ++- 3 files changed, 136 insertions(+), 16 deletions(-) create mode 100644 zkevm-circuits/src/state_circuit/binary_number.rs diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 35eb4e5262..e009c6d344 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -1,4 +1,5 @@ //! The state circuit implementation. +mod binary_number; mod constraint_builder; mod lexicographic_ordering; mod lookups; @@ -9,9 +10,11 @@ mod test; use crate::evm_circuit::{ param::N_BYTES_WORD, + table::RwTableTag, util::RandomLinearCombination, witness::{Rw, RwMap}, }; +use binary_number::{Chip as BinaryNumberChip, Config as BinaryNumberConfig}; use constraint_builder::{ConstraintBuilder, Queries}; use eth_types::{Address, Field, ToLittleEndian}; use gadgets::is_zero::{IsZeroChip, IsZeroConfig, IsZeroInstruction}; @@ -43,7 +46,7 @@ pub struct StateConfig { // https://github.com/appliedzkp/zkevm-circuits/issues/407 rw_counter: MpiConfig, is_write: Column, - tag: Column, + tag: BinaryNumberConfig, id: MpiConfig, is_id_unchanged: IsZeroConfig, address: MpiConfig, @@ -110,8 +113,10 @@ impl Circuit for StateCircuit { let lookups = LookupsChip::configure(meta); let power_of_randomness = [0; N_BYTES_WORD - 1].map(|_| meta.instance_column()); - let [is_write, tag, field_tag, value, is_id_unchanged_column, is_storage_key_unchanged_column] = - [0; 6].map(|_| meta.advice_column()); + let [is_write, field_tag, value, is_id_unchanged_column, is_storage_key_unchanged_column] = + [0; 5].map(|_| meta.advice_column()); + + let tag = BinaryNumberChip::configure(meta, selector); let id = MpiChip::configure(meta, selector, lookups.u16); let address = MpiChip::configure(meta, selector, lookups.u16); @@ -191,6 +196,8 @@ impl Circuit for StateCircuit { let lexicographic_ordering_chip = LexicographicOrderingChip::construct(config.lexicographic_ordering.clone()); + let tag_chip = BinaryNumberChip::construct(config.tag); + layouter.assign_region( || "rw table", |mut region| { @@ -207,12 +214,7 @@ impl Circuit for StateCircuit { offset, || Ok(if row.is_write() { F::one() } else { F::zero() }), )?; - region.assign_advice( - || "tag", - config.tag, - offset, - || Ok(F::from(row.tag() as u64)), - )?; + tag_chip.assign(&mut region, offset, row.tag())?; if let Some(id) = row.id() { config.id.assign(&mut region, offset, id as u32)?; } @@ -281,8 +283,8 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer selector: meta.query_fixed(c.selector, Rotation::cur()), rw_counter: MpiQueries::new(meta, c.rw_counter), is_write: meta.query_advice(c.is_write, Rotation::cur()), - tag: meta.query_advice(c.tag, Rotation::cur()), - prev_tag: meta.query_advice(c.tag, Rotation::prev()), + tag: c.tag.value(Rotation::cur())(meta), + prev_tag: c.tag.value(Rotation::prev())(meta), id: MpiQueries::new(meta, c.id), is_id_unchanged: c.is_id_unchanged.is_zero_expression.clone(), address: MpiQueries::new(meta, c.address), diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs new file mode 100644 index 0000000000..e57afa6e16 --- /dev/null +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -0,0 +1,114 @@ +use crate::evm_circuit::table::RwTableTag; +use crate::util::Expr; +use eth_types::{Address, Field, ToScalar}; +use halo2_proofs::{ + circuit::{AssignedCell, Layouter, Region}, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, + poly::Rotation, +}; +use std::convert::TryInto; +use std::marker::PhantomData; + +pub trait ToBits { + fn to_bits(&self) -> [bool; N]; +} + +impl ToBits<4> for RwTableTag { + fn to_bits(&self) -> [bool; 4] { + let mut bits = [false; 4]; + let mut x = *self as u8; + for i in 0..4 { + bits[3 - i] = x % 2 == 1; + x /= 2; + } + bits + } +} + +#[derive(Clone, Copy)] +pub struct Config +where + T: ToBits, +{ + pub bits: [Column; N], + _marker: PhantomData, +} + +impl Config { + pub fn assign( + &self, + region: &mut Region<'_, F>, + offset: usize, + value: RwTableTag, + ) -> Result<(), Error> { + for (&column, &bit) in self.bits.iter().zip(&value.to_bits()) { + region.assign_advice( + || format!("RwTableTag bit {:?}", column), + column, + offset, + || Ok(if bit { F::one() } else { F::zero() }), + )?; + } + Ok(()) + } + + pub fn value( + &self, + rotation: Rotation, + ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression + '_ { + let bits = self.bits.clone(); + move |meta: &mut VirtualCells<'_, F>| { + let bits = self.bits.map(|bit| meta.query_advice(bit, rotation)); + bits.iter() + .fold(0.expr(), |result, bit| bit.clone() + result * 2.expr()) + } + } +} + +pub struct Chip +where + T: ToBits, +{ + config: Config, + _marker: PhantomData, +} + +impl Chip +where + T: ToBits, +{ + pub fn construct(config: Config) -> Self { + Self { + config, + _marker: PhantomData, + } + } + + pub fn configure(meta: &mut ConstraintSystem, selector: Column) -> Config { + let bits = [0; N].map(|_| meta.advice_column()); + bits.map(|bit| { + meta.create_gate("bit column is 0 or 1", |meta| { + let selector = meta.query_fixed(selector, Rotation::cur()); + let bit = meta.query_advice(bit, Rotation::cur()); + vec![selector * bit.clone() * (1.expr() - bit)] + }) + }); + + Config { + bits, + _marker: PhantomData, + } + } + + pub fn assign( + &self, + region: &mut Region<'_, F>, + offset: usize, + value: RwTableTag, + ) -> Result<(), Error> { + for (&bit, &column) in value.to_bits().iter().zip(&self.config.bits) { + region.assign_advice(|| "bit column", column, offset, || Ok(F::from(bit)))?; + } + Ok(()) + } +} diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index cba31c48a0..d16092ce98 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -1,6 +1,9 @@ -use super::{N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER}; +use super::{ + binary_number::Config as BinaryNumberConfig, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, + N_LIMBS_RW_COUNTER, +}; use crate::{ - evm_circuit::{param::N_BYTES_WORD, witness::Rw}, + evm_circuit::{param::N_BYTES_WORD, table::RwTableTag, witness::Rw}, util::Expr, }; use eth_types::{Field, ToBigEndian}; @@ -76,7 +79,7 @@ pub struct Config { lower_limb_difference: Column, lower_limb_difference_is_zero: IsZeroConfig, // TODO: remove these columns from the config - tag: Column, + tag: BinaryNumberConfig, field_tag: Column, id_limbs: [Column; N_LIMBS_ID], address_limbs: [Column; N_LIMBS_ACCOUNT_ADDRESS], @@ -97,7 +100,7 @@ impl Chip { // TODO: fix this to not have too many arguments? pub fn configure( meta: &mut ConstraintSystem, - tag: Column, + tag: BinaryNumberConfig, field_tag: Column, id_limbs: [Column; N_LIMBS_ID], address_limbs: [Column; N_LIMBS_ACCOUNT_ADDRESS], @@ -282,9 +285,10 @@ struct Queries { impl Queries { fn new(meta: &mut VirtualCells<'_, F>, config: &Config, rotation: Rotation) -> Self { + let tag = config.tag.value(rotation)(meta); let mut query_advice = |column| meta.query_advice(column, rotation); Self { - tag: query_advice(config.tag), + tag, field_tag: query_advice(config.field_tag), id_limbs: config.id_limbs.map(&mut query_advice), address_limbs: config.address_limbs.map(&mut query_advice), From 339eadce4361712bf3b5ecbe44ad2299b6289fd4 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 17:02:19 -0400 Subject: [PATCH 02/51] Cleanup --- zkevm-circuits/src/state_circuit/binary_number.rs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index e57afa6e16..795cd4df88 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -1,12 +1,10 @@ -use crate::evm_circuit::table::RwTableTag; -use crate::util::Expr; -use eth_types::{Address, Field, ToScalar}; +use crate::{evm_circuit::table::RwTableTag, util::Expr}; +use eth_types::Field; use halo2_proofs::{ - circuit::{AssignedCell, Layouter, Region}, + circuit::Region, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, poly::Rotation, }; -use std::convert::TryInto; use std::marker::PhantomData; pub trait ToBits { @@ -56,7 +54,6 @@ impl Config { &self, rotation: Rotation, ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression + '_ { - let bits = self.bits.clone(); move |meta: &mut VirtualCells<'_, F>| { let bits = self.bits.map(|bit| meta.query_advice(bit, rotation)); bits.iter() From 67962c9fdece5ec626672f62e91164f63cefed54 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 17:23:50 -0400 Subject: [PATCH 03/51] Use binary columns to select based on Tag --- zkevm-circuits/src/state_circuit.rs | 4 ++++ .../src/state_circuit/binary_number.rs | 1 + .../src/state_circuit/constraint_builder.rs | 24 ++++++++++++------- 3 files changed, 21 insertions(+), 8 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index e009c6d344..b858a3c178 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -285,6 +285,10 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer is_write: meta.query_advice(c.is_write, Rotation::cur()), tag: c.tag.value(Rotation::cur())(meta), prev_tag: c.tag.value(Rotation::prev())(meta), + tag_bits: c + .tag + .bits + .map(|bit| meta.query_advice(bit, Rotation::cur())), id: MpiQueries::new(meta, c.id), is_id_unchanged: c.is_id_unchanged.is_zero_expression.clone(), address: MpiQueries::new(meta, c.address), diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index 795cd4df88..8472b89fc6 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -7,6 +7,7 @@ use halo2_proofs::{ }; use std::marker::PhantomData; +// TODO: rename to as_bits pub trait ToBits { fn to_bits(&self) -> [bool; N]; } diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 9def9ea301..24918638b0 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -1,7 +1,9 @@ use super::{ - lookups::Queries as LookupsQueries, multiple_precision_integer::Queries as MpiQueries, - random_linear_combination::Queries as RlcQueries, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, - N_LIMBS_RW_COUNTER, + binary_number::{Config as BinaryNumberConfig, ToBits}, + lookups::Queries as LookupsQueries, + multiple_precision_integer::Queries as MpiQueries, + random_linear_combination::Queries as RlcQueries, + N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER, }; use crate::evm_circuit::{ param::N_BYTES_WORD, @@ -20,6 +22,7 @@ pub struct Queries { pub is_write: Expression, pub tag: Expression, pub prev_tag: Expression, + pub tag_bits: [Expression; 4], pub id: MpiQueries, pub is_id_unchanged: Expression, pub address: MpiQueries, @@ -291,11 +294,16 @@ impl Queries { } fn tag_matches(&self, tag: RwTableTag) -> Expression { - generate_lagrange_base_polynomial( - self.tag.clone(), - tag as usize, - RwTableTag::iter().map(|x| x as usize), - ) + tag.to_bits() + .iter() + .zip(&self.tag_bits) + .fold(1.expr(), |product, (&bit, query)| { + (if bit { + query.clone() + } else { + not::expr(query.clone()) + }) * product + }) } fn first_access(&self) -> Expression { From dc462db045ccb8402c5c7c4dcb156314badeac60 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 17:29:29 -0400 Subject: [PATCH 04/51] Clean up and rename to_bits to as_bits --- .../src/state_circuit/binary_number.rs | 18 +++++++++--------- .../src/state_circuit/constraint_builder.rs | 6 +++--- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index 8472b89fc6..0746a40b37 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -8,12 +8,12 @@ use halo2_proofs::{ use std::marker::PhantomData; // TODO: rename to as_bits -pub trait ToBits { - fn to_bits(&self) -> [bool; N]; +pub trait AsBits { + fn as_bits(&self) -> [bool; N]; } -impl ToBits<4> for RwTableTag { - fn to_bits(&self) -> [bool; 4] { +impl AsBits<4> for RwTableTag { + fn as_bits(&self) -> [bool; 4] { let mut bits = [false; 4]; let mut x = *self as u8; for i in 0..4 { @@ -27,7 +27,7 @@ impl ToBits<4> for RwTableTag { #[derive(Clone, Copy)] pub struct Config where - T: ToBits, + T: AsBits, { pub bits: [Column; N], _marker: PhantomData, @@ -40,7 +40,7 @@ impl Config { offset: usize, value: RwTableTag, ) -> Result<(), Error> { - for (&column, &bit) in self.bits.iter().zip(&value.to_bits()) { + for (&column, &bit) in self.bits.iter().zip(&value.as_bits()) { region.assign_advice( || format!("RwTableTag bit {:?}", column), column, @@ -65,7 +65,7 @@ impl Config { pub struct Chip where - T: ToBits, + T: AsBits, { config: Config, _marker: PhantomData, @@ -73,7 +73,7 @@ where impl Chip where - T: ToBits, + T: AsBits, { pub fn construct(config: Config) -> Self { Self { @@ -104,7 +104,7 @@ where offset: usize, value: RwTableTag, ) -> Result<(), Error> { - for (&bit, &column) in value.to_bits().iter().zip(&self.config.bits) { + for (&bit, &column) in value.as_bits().iter().zip(&self.config.bits) { region.assign_advice(|| "bit column", column, offset, || Ok(F::from(bit)))?; } Ok(()) diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 24918638b0..830f2578eb 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -1,5 +1,5 @@ use super::{ - binary_number::{Config as BinaryNumberConfig, ToBits}, + binary_number::AsBits, lookups::Queries as LookupsQueries, multiple_precision_integer::Queries as MpiQueries, random_linear_combination::Queries as RlcQueries, @@ -8,7 +8,7 @@ use super::{ use crate::evm_circuit::{ param::N_BYTES_WORD, table::{AccountFieldTag, RwTableTag}, - util::{math_gadget::generate_lagrange_base_polynomial, not, or}, + util::{not, or}, }; use crate::util::Expr; use eth_types::Field; @@ -294,7 +294,7 @@ impl Queries { } fn tag_matches(&self, tag: RwTableTag) -> Expression { - tag.to_bits() + tag.as_bits() .iter() .zip(&self.tag_bits) .fold(1.expr(), |product, (&bit, query)| { From ddf7ea9a08bf6412f12eef6dfa91dc27d6879683 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 19:37:34 -0400 Subject: [PATCH 05/51] Add check that RwTableTag is in allowed range --- zkevm-circuits/src/evm_circuit/table.rs | 2 +- zkevm-circuits/src/state_circuit.rs | 1 - .../src/state_circuit/binary_number.rs | 61 +++++++++++++++++-- .../src/state_circuit/constraint_builder.rs | 34 +++++------ zkevm-circuits/src/state_circuit/test.rs | 31 +++++++++- 5 files changed, 105 insertions(+), 24 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index cc94351f49..8c9424cb45 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -142,7 +142,7 @@ pub enum BlockContextFieldTag { ChainId, } -#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, EnumIter)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, EnumIter, EnumCount)] pub enum RwTableTag { Start = 1, Stack, diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index b858a3c178..a4a5944c93 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -284,7 +284,6 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer rw_counter: MpiQueries::new(meta, c.rw_counter), is_write: meta.query_advice(c.is_write, Rotation::cur()), tag: c.tag.value(Rotation::cur())(meta), - prev_tag: c.tag.value(Rotation::prev())(meta), tag_bits: c .tag .bits diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index 0746a40b37..d04bac605a 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -1,4 +1,10 @@ -use crate::{evm_circuit::table::RwTableTag, util::Expr}; +use crate::{ + evm_circuit::{ + table::RwTableTag, + util::{and, not}, + }, + util::Expr, +}; use eth_types::Field; use halo2_proofs::{ circuit::Region, @@ -6,6 +12,7 @@ use halo2_proofs::{ poly::Rotation, }; use std::marker::PhantomData; +use strum::EnumCount; // TODO: rename to as_bits pub trait AsBits { @@ -24,6 +31,18 @@ impl AsBits<4> for RwTableTag { } } +impl AsBits for usize { + fn as_bits(&self) -> [bool; N] { + let mut bits = [false; N]; + let mut x = *self as u64; + for i in 0..N { + bits[N - 1 - i] = x % 2 == 1; + x /= 2; + } + bits + } +} + #[derive(Clone, Copy)] pub struct Config where @@ -33,7 +52,10 @@ where _marker: PhantomData, } -impl Config { +impl Config +where + T: AsBits, +{ pub fn assign( &self, region: &mut Region<'_, F>, @@ -61,6 +83,27 @@ impl Config { .fold(0.expr(), |result, bit| bit.clone() + result * 2.expr()) } } + + pub fn value_equals>( + &self, + value: &S, + rotation: Rotation, + ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression + '_ { + let bits = value.as_bits(); + move |meta: &mut VirtualCells<'_, F>| { + and::expr( + bits.iter() + .zip(&self.bits.map(|bit| meta.query_advice(bit, rotation))) + .map(|(&bit, query)| { + if bit { + query.clone() + } else { + not::expr(query.clone()) + } + }), + ) + } + } } pub struct Chip @@ -71,7 +114,7 @@ where _marker: PhantomData, } -impl Chip +impl Chip where T: AsBits, { @@ -92,10 +135,20 @@ where }) }); - Config { + let config = Config { bits, _marker: PhantomData, + }; + + for i in T::COUNT..T::COUNT.next_power_of_two() { + meta.create_gate("binary number value in range", |meta| { + let selector = meta.query_fixed(selector, Rotation::cur()); + let value_equals_i = config.value_equals(&i, Rotation::cur()); + vec![selector * value_equals_i(meta)] + }) } + + config } pub fn assign( diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 830f2578eb..f44ebfd5f6 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -1,14 +1,13 @@ use super::{ - binary_number::AsBits, - lookups::Queries as LookupsQueries, + binary_number::AsBits, lookups::Queries as LookupsQueries, multiple_precision_integer::Queries as MpiQueries, - random_linear_combination::Queries as RlcQueries, - N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER, + random_linear_combination::Queries as RlcQueries, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, + N_LIMBS_RW_COUNTER, }; use crate::evm_circuit::{ param::N_BYTES_WORD, table::{AccountFieldTag, RwTableTag}, - util::{not, or}, + util::{and, not, or}, }; use crate::util::Expr; use eth_types::Field; @@ -21,7 +20,6 @@ pub struct Queries { pub rw_counter: MpiQueries, pub is_write: Expression, pub tag: Expression, - pub prev_tag: Expression, pub tag_bits: [Expression; 4], pub id: MpiQueries, pub is_id_unchanged: Expression, @@ -101,7 +99,7 @@ impl ConstraintBuilder { } fn build_general_constraints(&mut self, q: &Queries) { - self.require_in_set("tag in RwTableTag range", q.tag(), set::()); + // tag value in RwTableTag range is enforced in BinaryNumberChip self.require_boolean("is_write is boolean", q.is_write()); } @@ -294,16 +292,18 @@ impl Queries { } fn tag_matches(&self, tag: RwTableTag) -> Expression { - tag.as_bits() - .iter() - .zip(&self.tag_bits) - .fold(1.expr(), |product, (&bit, query)| { - (if bit { - query.clone() - } else { - not::expr(query.clone()) - }) * product - }) + and::expr( + tag.as_bits() + .iter() + .zip(&self.tag_bits) + .map(|(&bit, query)| { + if bit { + query.clone() + } else { + not::expr(query.clone()) + } + }), + ) } fn first_access(&self) -> Expression { diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 16c023c67a..a784445e7e 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -1,8 +1,9 @@ use super::{StateCircuit, StateConfig}; use crate::evm_circuit::{ - table::{AccountFieldTag, CallContextFieldTag}, + table::{AccountFieldTag, CallContextFieldTag, RwTableTag}, witness::{Rw, RwMap}, }; +use crate::state_circuit::binary_number::AsBits; use bus_mapping::operation::{ MemoryOp, Operation, OperationContainer, RWCounter, StackOp, StorageOp, RW, }; @@ -18,6 +19,7 @@ use halo2_proofs::{ plonk::{Advice, Circuit, Column, ConstraintSystem}, }; use std::collections::HashMap; +use strum::EnumCount; #[derive(Hash, Eq, PartialEq)] pub enum AdviceColumn { @@ -32,6 +34,10 @@ pub enum AdviceColumn { Value, RwCounter, RwCounterLimb0, + TagBit0, + TagBit1, + TagBit2, + TagBit3, } impl AdviceColumn { @@ -48,6 +54,10 @@ impl AdviceColumn { Self::Value => config.value, Self::RwCounter => config.rw_counter.value, Self::RwCounterLimb0 => config.rw_counter.limbs[0], + Self::TagBit0 => config.tag.bits[0], + Self::TagBit1 => config.tag.bits[1], + Self::TagBit2 => config.tag.bits[2], + Self::TagBit3 => config.tag.bits[3], } } } @@ -573,6 +583,7 @@ fn nonlexicographic_order_rw_counter() { } #[test] +<<<<<<< HEAD #[ignore = "read consistency constraint not implemented"] fn read_inconsistency() { let rows = vec![ @@ -700,6 +711,24 @@ fn invalid_stack_address_change() { verify(rows), "if call id is the same, address change is 0 or 1", ); +======= +fn invalid_tags() { + for i in RwTableTag::COUNT..16 { + let bits: [Fr; 4] = i + .as_bits() + .map(|bit| if bit { Fr::one() } else { Fr::zero() }); + let overrides = HashMap::from([ + ((AdviceColumn::TagBit0, 0), bits[0]), + ((AdviceColumn::TagBit1, 0), bits[1]), + ((AdviceColumn::TagBit2, 0), bits[2]), + ((AdviceColumn::TagBit3, 0), bits[3]), + ]); + + let result = verify_with_overrides(vec![], overrides); + + assert_error_matches(result, "binary number value in range"); + } +>>>>>>> 7914dc82 (Add check that RwTableTag is in allowed range) } fn prover(rows: Vec, overrides: HashMap<(AdviceColumn, usize), Fr>) -> MockProver { From 92890a48f93a1f413078cdb4baca5a557316de5b Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 19:48:56 -0400 Subject: [PATCH 06/51] Fix degree test and remove unused function --- .../src/state_circuit/binary_number.rs | 24 +++++-------------- zkevm-circuits/src/state_circuit/test.rs | 2 +- 2 files changed, 7 insertions(+), 19 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index d04bac605a..f64b21ce96 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -56,23 +56,6 @@ impl Config where T: AsBits, { - pub fn assign( - &self, - region: &mut Region<'_, F>, - offset: usize, - value: RwTableTag, - ) -> Result<(), Error> { - for (&column, &bit) in self.bits.iter().zip(&value.as_bits()) { - region.assign_advice( - || format!("RwTableTag bit {:?}", column), - column, - offset, - || Ok(if bit { F::one() } else { F::zero() }), - )?; - } - Ok(()) - } - pub fn value( &self, rotation: Rotation, @@ -158,7 +141,12 @@ where value: RwTableTag, ) -> Result<(), Error> { for (&bit, &column) in value.as_bits().iter().zip(&self.config.bits) { - region.assign_advice(|| "bit column", column, offset, || Ok(F::from(bit)))?; + region.assign_advice( + || format!("binary number {:?}", column), + column, + offset, + || Ok(F::from(bit)), + )?; } Ok(()) } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index a784445e7e..480aa6b906 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -87,7 +87,7 @@ fn test_state_circuit_ok( fn degree() { let mut meta = ConstraintSystem::::default(); StateCircuit::configure(&mut meta); - assert_eq!(meta.degree(), 18); + assert_eq!(meta.degree(), 16); } #[test] From c4ee256327bd7ef642e653ace138b411dd0b23a5 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Thu, 2 Jun 2022 12:25:00 -0400 Subject: [PATCH 07/51] Fix rebase and clean up invalid_values gate --- .../src/state_circuit/binary_number.rs | 26 ++++++++++++++----- zkevm-circuits/src/state_circuit/test.rs | 16 +++++++----- 2 files changed, 29 insertions(+), 13 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index f64b21ce96..999349af81 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -11,10 +11,10 @@ use halo2_proofs::{ plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, poly::Rotation, }; +use std::collections::BTreeSet; use std::marker::PhantomData; -use strum::EnumCount; +use strum::IntoEnumIterator; -// TODO: rename to as_bits pub trait AsBits { fn as_bits(&self) -> [bool; N]; } @@ -97,7 +97,7 @@ where _marker: PhantomData, } -impl Chip +impl Chip where T: AsBits, { @@ -123,12 +123,19 @@ where _marker: PhantomData, }; - for i in T::COUNT..T::COUNT.next_power_of_two() { + // Disallow bit patterns (if any) that don't correspond to a variant of T. + let valid_values: BTreeSet = T::iter().map(|t| from_bits(&t.as_bits())).collect(); + let mut invalid_values = (0..1 << N).filter(|i| !valid_values.contains(i)).peekable(); + if invalid_values.peek().is_some() { meta.create_gate("binary number value in range", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); - let value_equals_i = config.value_equals(&i, Rotation::cur()); - vec![selector * value_equals_i(meta)] - }) + invalid_values + .map(|i| { + let value_equals_i = config.value_equals(&i, Rotation::cur()); + selector.clone() * value_equals_i(meta) + }) + .collect::>() + }); } config @@ -151,3 +158,8 @@ where Ok(()) } } + +fn from_bits(bits: &[bool]) -> usize { + bits.iter() + .fold(0, |result, &bit| bit as usize + 2 * result) +} diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 480aa6b906..02a8bffe28 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -18,8 +18,8 @@ use halo2_proofs::{ pairing::bn256::Fr, plonk::{Advice, Circuit, Column, ConstraintSystem}, }; -use std::collections::HashMap; -use strum::EnumCount; +use std::collections::{BTreeSet, HashMap}; +use strum::IntoEnumIterator; #[derive(Hash, Eq, PartialEq)] pub enum AdviceColumn { @@ -583,7 +583,6 @@ fn nonlexicographic_order_rw_counter() { } #[test] -<<<<<<< HEAD #[ignore = "read consistency constraint not implemented"] fn read_inconsistency() { let rows = vec![ @@ -711,9 +710,15 @@ fn invalid_stack_address_change() { verify(rows), "if call id is the same, address change is 0 or 1", ); -======= +} + +#[test] fn invalid_tags() { - for i in RwTableTag::COUNT..16 { + let tags: BTreeSet = RwTableTag::iter().map(|x| x as usize).collect(); + for i in 0..16 { + if tags.contains(&i) { + continue; + } let bits: [Fr; 4] = i .as_bits() .map(|bit| if bit { Fr::one() } else { Fr::zero() }); @@ -728,7 +733,6 @@ fn invalid_tags() { assert_error_matches(result, "binary number value in range"); } ->>>>>>> 7914dc82 (Add check that RwTableTag is in allowed range) } fn prover(rows: Vec, overrides: HashMap<(AdviceColumn, usize), Fr>) -> MockProver { From 9910424b10683f38c896c97b77cd2d4da880743f Mon Sep 17 00:00:00 2001 From: z2trillion Date: Thu, 2 Jun 2022 12:50:07 -0400 Subject: [PATCH 08/51] Remove unused derive --- zkevm-circuits/src/evm_circuit/table.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index 8c9424cb45..cc94351f49 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -142,7 +142,7 @@ pub enum BlockContextFieldTag { ChainId, } -#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, EnumIter, EnumCount)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, EnumIter)] pub enum RwTableTag { Start = 1, Stack, From 941b394a53de3ba79698f9b6f5486900d0da3ba1 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 8 Jun 2022 14:33:32 -0400 Subject: [PATCH 09/51] Make requested changes --- .../src/state_circuit/binary_number.rs | 27 ++++++++++++------- .../src/state_circuit/constraint_builder.rs | 20 ++++---------- 2 files changed, 22 insertions(+), 25 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index 999349af81..7a4b75c504 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -16,6 +16,7 @@ use std::marker::PhantomData; use strum::IntoEnumIterator; pub trait AsBits { + // Return the bits of self, starting from the most significant. fn as_bits(&self) -> [bool; N]; } @@ -74,19 +75,25 @@ where ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression + '_ { let bits = value.as_bits(); move |meta: &mut VirtualCells<'_, F>| { - and::expr( - bits.iter() - .zip(&self.bits.map(|bit| meta.query_advice(bit, rotation))) - .map(|(&bit, query)| { - if bit { - query.clone() - } else { - not::expr(query.clone()) - } - }), + Self::value_equals_expr( + &bits, + &self.bits.map(|bit| meta.query_advice(bit, rotation)), ) } } + + pub fn value_equals_expr( + value: &[bool], + expressions: &[Expression], + ) -> Expression { + and::expr(value.iter().zip(expressions).map(|(&bit, expression)| { + if bit { + expression.clone() + } else { + not::expr(expression.clone()) + } + })) + } } pub struct Chip diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index f44ebfd5f6..684add486b 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -1,8 +1,9 @@ use super::{ - binary_number::AsBits, lookups::Queries as LookupsQueries, + binary_number::{AsBits, Config as BinaryNumberConfig}, + lookups::Queries as LookupsQueries, multiple_precision_integer::Queries as MpiQueries, - random_linear_combination::Queries as RlcQueries, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, - N_LIMBS_RW_COUNTER, + random_linear_combination::Queries as RlcQueries, + N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER, }; use crate::evm_circuit::{ param::N_BYTES_WORD, @@ -292,18 +293,7 @@ impl Queries { } fn tag_matches(&self, tag: RwTableTag) -> Expression { - and::expr( - tag.as_bits() - .iter() - .zip(&self.tag_bits) - .map(|(&bit, query)| { - if bit { - query.clone() - } else { - not::expr(query.clone()) - } - }), - ) + BinaryNumberConfig::::value_equals_expr(&tag.as_bits(), &self.tag_bits) } fn first_access(&self) -> Expression { From 47c2e4a7159a3a82c97426971b5df4ab40f13919 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 8 Jun 2022 14:37:48 -0400 Subject: [PATCH 10/51] clippy --- zkevm-circuits/src/state_circuit/constraint_builder.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 684add486b..cd174cb655 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -8,7 +8,7 @@ use super::{ use crate::evm_circuit::{ param::N_BYTES_WORD, table::{AccountFieldTag, RwTableTag}, - util::{and, not, or}, + util::{not, or}, }; use crate::util::Expr; use eth_types::Field; From 2a7ca30b4fdc5b266405041231a2e60fd227491f Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 13 Jun 2022 17:14:40 -0400 Subject: [PATCH 11/51] Make requested changes --- zkevm-circuits/src/state_circuit.rs | 2 +- .../src/state_circuit/binary_number.rs | 61 ++++++++++--------- .../src/state_circuit/constraint_builder.rs | 9 ++- 3 files changed, 37 insertions(+), 35 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index a4a5944c93..b89cd49e55 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -214,7 +214,7 @@ impl Circuit for StateCircuit { offset, || Ok(if row.is_write() { F::one() } else { F::zero() }), )?; - tag_chip.assign(&mut region, offset, row.tag())?; + tag_chip.assign(&mut region, offset, &row.tag())?; if let Some(id) = row.id() { config.id.assign(&mut region, offset, id as u32)?; } diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index 7a4b75c504..5dc02bb817 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -45,10 +45,8 @@ impl AsBits for usize { } #[derive(Clone, Copy)] -pub struct Config -where - T: AsBits, -{ +pub struct Config { + // Must be constrained to be binary for correctness. pub bits: [Column; N], _marker: PhantomData, } @@ -70,36 +68,41 @@ where pub fn value_equals>( &self, - value: &S, + value: S, rotation: Rotation, - ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression + '_ { - let bits = value.as_bits(); - move |meta: &mut VirtualCells<'_, F>| { - Self::value_equals_expr( - &bits, - &self.bits.map(|bit| meta.query_advice(bit, rotation)), - ) - } + ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression { + let bits = self.bits; + move |meta| Self::value_equals_expr(value, bits.map(|bit| meta.query_advice(bit, rotation))) } - pub fn value_equals_expr( - value: &[bool], - expressions: &[Expression], + // Returns an expression that evaluates to 1 if expressions are equal to value + // as bits. The returned expression is of degree N. + pub fn value_equals_expr>( + value: S, + expressions: [Expression; N], // must be binary. ) -> Expression { - and::expr(value.iter().zip(expressions).map(|(&bit, expression)| { - if bit { - expression.clone() - } else { - not::expr(expression.clone()) - } - })) + and::expr( + value + .as_bits() + .iter() + .zip(&expressions) + .map(|(&bit, expression)| { + if bit { + expression.clone() + } else { + not::expr(expression.clone()) + } + }), + ) } } -pub struct Chip -where - T: AsBits, -{ +// This chip helps working with binary encoding of integers of length N bits by: +// - enforcing that the binary representation is in the valid range defined by +// T. +// - creating expressions (via the Config) that evaluate to 1 when the bits +// match a specific value and 0 otherwise. +pub struct Chip { config: Config, _marker: PhantomData, } @@ -138,7 +141,7 @@ where let selector = meta.query_fixed(selector, Rotation::cur()); invalid_values .map(|i| { - let value_equals_i = config.value_equals(&i, Rotation::cur()); + let value_equals_i = config.value_equals(i, Rotation::cur()); selector.clone() * value_equals_i(meta) }) .collect::>() @@ -152,7 +155,7 @@ where &self, region: &mut Region<'_, F>, offset: usize, - value: RwTableTag, + value: &T, ) -> Result<(), Error> { for (&bit, &column) in value.as_bits().iter().zip(&self.config.bits) { region.assign_advice( diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index cd174cb655..063479164a 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -1,9 +1,8 @@ use super::{ - binary_number::{AsBits, Config as BinaryNumberConfig}, - lookups::Queries as LookupsQueries, + binary_number::Config as BinaryNumberConfig, lookups::Queries as LookupsQueries, multiple_precision_integer::Queries as MpiQueries, - random_linear_combination::Queries as RlcQueries, - N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER, + random_linear_combination::Queries as RlcQueries, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, + N_LIMBS_RW_COUNTER, }; use crate::evm_circuit::{ param::N_BYTES_WORD, @@ -293,7 +292,7 @@ impl Queries { } fn tag_matches(&self, tag: RwTableTag) -> Expression { - BinaryNumberConfig::::value_equals_expr(&tag.as_bits(), &self.tag_bits) + BinaryNumberConfig::::value_equals_expr(tag, self.tag_bits.clone()) } fn first_access(&self) -> Expression { From 81a18196fbcca3f1b46c8dabae9dfadfe7c6792e Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 20:12:57 -0400 Subject: [PATCH 12/51] Create and use SortKeysConfig --- zkevm-circuits/src/state_circuit.rs | 62 +++++++++---------- .../state_circuit/lexicographic_ordering.rs | 25 +++----- 2 files changed, 40 insertions(+), 47 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index b89cd49e55..610b113f49 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -44,14 +44,9 @@ const N_LIMBS_ID: usize = 2; pub struct StateConfig { selector: Column, // Figure out why you get errors when this is Selector. // https://github.com/appliedzkp/zkevm-circuits/issues/407 - rw_counter: MpiConfig, + sort_keys: SortKeysConfig, is_write: Column, - tag: BinaryNumberConfig, - id: MpiConfig, is_id_unchanged: IsZeroConfig, - address: MpiConfig, - field_tag: Column, - storage_key: RlcConfig, is_storage_key_unchanged: IsZeroConfig, value: Column, lookups: LookupsConfig, @@ -59,6 +54,17 @@ pub struct StateConfig { lexicographic_ordering: LexicographicOrderingConfig, } +/// Keys for sorting the rows of the state circuit +#[derive(Clone, Copy)] +pub struct SortKeysConfig { + tag: BinaryNumberConfig, + id: MpiConfig, + field_tag: Column, + address: MpiConfig, + storage_key: RlcConfig, + rw_counter: MpiConfig, +} + type Lookup = (&'static str, Expression, Expression); /// State Circuit for proving RwTable is valid @@ -123,14 +129,13 @@ impl Circuit for StateCircuit { let storage_key = RlcChip::configure(meta, selector, lookups.u8, power_of_randomness); let rw_counter = MpiChip::configure(meta, selector, lookups.u16); + let sort_keys = SortKeysConfig { + tag, id, field_tag, address, storage_key, rw_counter, + }; + let lexicographic_ordering = LexicographicOrderingChip::configure( meta, - tag, - field_tag, - id.limbs, - address.limbs, - storage_key.bytes, - rw_counter.limbs, + sort_keys, lookups.u16, ); @@ -155,14 +160,9 @@ impl Circuit for StateCircuit { let config = Self::Config { selector, - rw_counter, + sort_keys, is_write, - tag, - id, is_id_unchanged, - address, - field_tag, - storage_key, value, lexicographic_ordering, is_storage_key_unchanged, @@ -196,7 +196,7 @@ impl Circuit for StateCircuit { let lexicographic_ordering_chip = LexicographicOrderingChip::construct(config.lexicographic_ordering.clone()); - let tag_chip = BinaryNumberChip::construct(config.tag); + let tag_chip = BinaryNumberChip::construct(config.sort_keys.tag); layouter.assign_region( || "rw table", @@ -206,7 +206,7 @@ impl Circuit for StateCircuit { for (offset, (row, prev_row)) in rows.zip(prev_rows).enumerate() { region.assign_fixed(|| "selector", config.selector, offset, || Ok(F::one()))?; config - .rw_counter + .sort_keys.rw_counter .assign(&mut region, offset, row.rw_counter() as u32)?; region.assign_advice( || "is_write", @@ -216,21 +216,21 @@ impl Circuit for StateCircuit { )?; tag_chip.assign(&mut region, offset, &row.tag())?; if let Some(id) = row.id() { - config.id.assign(&mut region, offset, id as u32)?; + config.sort_keys.id.assign(&mut region, offset, id as u32)?; } if let Some(address) = row.address() { - config.address.assign(&mut region, offset, address)?; + config.sort_keys.address.assign(&mut region, offset, address)?; } if let Some(field_tag) = row.field_tag() { region.assign_advice( || "field_tag", - config.field_tag, + config.sort_keys.field_tag, offset, || Ok(F::from(field_tag as u64)), )?; } if let Some(storage_key) = row.storage_key() { - config.storage_key.assign( + config.sort_keys.storage_key.assign( &mut region, offset, self.randomness, @@ -281,18 +281,18 @@ impl Circuit for StateCircuit { fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { Queries { selector: meta.query_fixed(c.selector, Rotation::cur()), - rw_counter: MpiQueries::new(meta, c.rw_counter), + rw_counter: MpiQueries::new(meta, c.sort_keys.rw_counter), is_write: meta.query_advice(c.is_write, Rotation::cur()), - tag: c.tag.value(Rotation::cur())(meta), - tag_bits: c + tag: c.sort_keys.tag.value(Rotation::cur())(meta), + tag_bits: c.sort_keys .tag .bits .map(|bit| meta.query_advice(bit, Rotation::cur())), - id: MpiQueries::new(meta, c.id), + id: MpiQueries::new(meta, c.sort_keys.id), is_id_unchanged: c.is_id_unchanged.is_zero_expression.clone(), - address: MpiQueries::new(meta, c.address), - field_tag: meta.query_advice(c.field_tag, Rotation::cur()), - storage_key: RlcQueries::new(meta, c.storage_key), + address: MpiQueries::new(meta, c.sort_keys.address), + field_tag: meta.query_advice(c.sort_keys.field_tag, Rotation::cur()), + storage_key: RlcQueries::new(meta, c.sort_keys.storage_key), value: meta.query_advice(c.value, Rotation::cur()), lookups: LookupsQueries::new(meta, c.lookups), power_of_randomness: c diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index d16092ce98..260afd34fe 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -1,6 +1,6 @@ use super::{ - binary_number::Config as BinaryNumberConfig, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, - N_LIMBS_RW_COUNTER, + binary_number::Config as BinaryNumberConfig, SortKeysConfig, N_LIMBS_ACCOUNT_ADDRESS, + N_LIMBS_ID, N_LIMBS_RW_COUNTER, }; use crate::{ evm_circuit::{param::N_BYTES_WORD, table::RwTableTag, witness::Rw}, @@ -96,16 +96,9 @@ impl Chip { Self { config } } - #[allow(clippy::too_many_arguments)] - // TODO: fix this to not have too many arguments? pub fn configure( meta: &mut ConstraintSystem, - tag: BinaryNumberConfig, - field_tag: Column, - id_limbs: [Column; N_LIMBS_ID], - address_limbs: [Column; N_LIMBS_ACCOUNT_ADDRESS], - storage_key_bytes: [Column; N_BYTES_WORD], - rw_counter_limbs: [Column; N_LIMBS_RW_COUNTER], + keys: SortKeysConfig, u16_range: Column, ) -> Config { let selector = meta.fixed_column(); @@ -137,12 +130,12 @@ impl Chip { upper_limb_difference_is_zero: upper_limb_difference_is_zero_config, lower_limb_difference, lower_limb_difference_is_zero: lower_limb_difference_is_zero_config, - tag, - field_tag, - id_limbs, - address_limbs, - storage_key_bytes, - rw_counter_limbs, + tag: keys.tag, + field_tag: keys.field_tag, + id_limbs: keys.id.limbs, + address_limbs: keys.address.limbs, + storage_key_bytes: keys.storage_key.bytes, + rw_counter_limbs: keys.rw_counter.limbs, }; meta.create_gate("upper_limb_difference is one of 15 values", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); From 7ac83e659f6056ee10a4564541087933c47e0d22 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 30 May 2022 20:16:53 -0400 Subject: [PATCH 13/51] Cleanup lexicographic ordering config --- .../state_circuit/lexicographic_ordering.rs | 39 +++++++------------ 1 file changed, 13 insertions(+), 26 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 260afd34fe..9af23fc967 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -78,13 +78,6 @@ pub struct Config { pub(crate) upper_limb_difference_is_zero: IsZeroConfig, lower_limb_difference: Column, lower_limb_difference_is_zero: IsZeroConfig, - // TODO: remove these columns from the config - tag: BinaryNumberConfig, - field_tag: Column, - id_limbs: [Column; N_LIMBS_ID], - address_limbs: [Column; N_LIMBS_ACCOUNT_ADDRESS], - storage_key_bytes: [Column; N_BYTES_WORD], - rw_counter_limbs: [Column; N_LIMBS_RW_COUNTER], } pub struct Chip { @@ -130,17 +123,11 @@ impl Chip { upper_limb_difference_is_zero: upper_limb_difference_is_zero_config, lower_limb_difference, lower_limb_difference_is_zero: lower_limb_difference_is_zero_config, - tag: keys.tag, - field_tag: keys.field_tag, - id_limbs: keys.id.limbs, - address_limbs: keys.address.limbs, - storage_key_bytes: keys.storage_key.bytes, - rw_counter_limbs: keys.rw_counter.limbs, }; meta.create_gate("upper_limb_difference is one of 15 values", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, &config, Rotation::cur()); - let prev = Queries::new(meta, &config, Rotation::prev()); + let cur = Queries::new(meta, &config, keys, Rotation::cur()); + let prev = Queries::new(meta, &config, keys, Rotation::prev()); let upper_limb_difference = meta.query_advice(upper_limb_difference, Rotation::cur()); vec![ selector @@ -155,8 +142,8 @@ impl Chip { "upper_limb_difference is zero iff all 15 possible values are 0", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, &config, Rotation::cur()); - let prev = Queries::new(meta, &config, Rotation::prev()); + let cur = Queries::new(meta, &config, keys, Rotation::cur()); + let prev = Queries::new(meta, &config, keys, Rotation::prev()); vec![ // all 15 possible values are 0 iff the final linear combination is 0 selector @@ -167,8 +154,8 @@ impl Chip { ); meta.create_gate("lower_limb_difference is one of 15 values", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, &config, Rotation::cur()); - let prev = Queries::new(meta, &config, Rotation::prev()); + let cur = Queries::new(meta, &config, keys, Rotation::cur()); + let prev = Queries::new(meta, &config, keys, Rotation::prev()); let lower_limb_difference = meta.query_advice(lower_limb_difference, Rotation::cur()); vec![ selector @@ -277,16 +264,16 @@ struct Queries { } impl Queries { - fn new(meta: &mut VirtualCells<'_, F>, config: &Config, rotation: Rotation) -> Self { - let tag = config.tag.value(rotation)(meta); + fn new(meta: &mut VirtualCells<'_, F>, config: &Config, keys: SortKeysConfig, rotation: Rotation) -> Self { + let tag = keys.tag.value(rotation)(meta); let mut query_advice = |column| meta.query_advice(column, rotation); Self { tag, - field_tag: query_advice(config.field_tag), - id_limbs: config.id_limbs.map(&mut query_advice), - address_limbs: config.address_limbs.map(&mut query_advice), - storage_key_bytes: config.storage_key_bytes.map(&mut query_advice), - rw_counter_limbs: config.rw_counter_limbs.map(query_advice), + field_tag: query_advice(keys.field_tag), + id_limbs: keys.id.limbs.map(&mut query_advice), + address_limbs: keys.address.limbs.map(&mut query_advice), + storage_key_bytes: keys.storage_key.bytes.map(&mut query_advice), + rw_counter_limbs: keys.rw_counter.limbs.map(query_advice), } } From f55976a141d88d7d3c2cded0d48f822934be8ac4 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 00:22:25 -0400 Subject: [PATCH 14/51] Fix rebase and limb count errors --- zkevm-circuits/src/state_circuit.rs | 57 ++-- .../src/state_circuit/constraint_builder.rs | 10 +- .../state_circuit/lexicographic_ordering.rs | 311 ++++++++---------- zkevm-circuits/src/state_circuit/test.rs | 61 ++-- 4 files changed, 188 insertions(+), 251 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 610b113f49..d6fbc2e5c2 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -25,9 +25,7 @@ use halo2_proofs::{ }, poly::Rotation, }; -use lexicographic_ordering::{ - Chip as LexicographicOrderingChip, Config as LexicographicOrderingConfig, -}; +use lexicographic_ordering::Config as LexicographicOrderingConfig; use lookups::{Chip as LookupsChip, Config as LookupsConfig, Queries as LookupsQueries}; use multiple_precision_integer::{Chip as MpiChip, Config as MpiConfig, Queries as MpiQueries}; use random_linear_combination::{Chip as RlcChip, Config as RlcConfig, Queries as RlcQueries}; @@ -47,11 +45,11 @@ pub struct StateConfig { sort_keys: SortKeysConfig, is_write: Column, is_id_unchanged: IsZeroConfig, - is_storage_key_unchanged: IsZeroConfig, + is_storage_key_unchanged: IsZeroConfig, // can be removed value: Column, lookups: LookupsConfig, power_of_randomness: [Column; N_BYTES_WORD - 1], - lexicographic_ordering: LexicographicOrderingConfig, + lexicographic_ordering: LexicographicOrderingConfig, } /// Keys for sorting the rows of the state circuit @@ -83,9 +81,10 @@ impl StateCircuit { rows.sort_by_key(|row| { ( row.tag() as u64, - row.field_tag().unwrap_or_default(), row.id().unwrap_or_default(), + row.field_tag().unwrap_or_default(), row.address().unwrap_or_default(), + // row.field_tag().unwrap_or_default(), // this is the correct place row.storage_key().unwrap_or_default(), row.rw_counter(), ) @@ -130,14 +129,16 @@ impl Circuit for StateCircuit { let rw_counter = MpiChip::configure(meta, selector, lookups.u16); let sort_keys = SortKeysConfig { - tag, id, field_tag, address, storage_key, rw_counter, + tag, + id, + field_tag, + address, + storage_key, + rw_counter, }; - let lexicographic_ordering = LexicographicOrderingChip::configure( - meta, - sort_keys, - lookups.u16, - ); + let lexicographic_ordering = + LexicographicOrderingConfig::configure(meta, sort_keys, lookups.u16); let is_id_unchanged = IsZeroChip::configure( meta, @@ -193,8 +194,6 @@ impl Circuit for StateCircuit { let is_id_unchanged = IsZeroChip::construct(config.is_id_unchanged.clone()); let is_storage_key_unchanged = IsZeroChip::construct(config.is_storage_key_unchanged.clone()); - let lexicographic_ordering_chip = - LexicographicOrderingChip::construct(config.lexicographic_ordering.clone()); let tag_chip = BinaryNumberChip::construct(config.sort_keys.tag); @@ -205,9 +204,11 @@ impl Circuit for StateCircuit { let prev_rows = once(&Rw::Start).chain(rows.clone()); for (offset, (row, prev_row)) in rows.zip(prev_rows).enumerate() { region.assign_fixed(|| "selector", config.selector, offset, || Ok(F::one()))?; - config - .sort_keys.rw_counter - .assign(&mut region, offset, row.rw_counter() as u32)?; + config.sort_keys.rw_counter.assign( + &mut region, + offset, + row.rw_counter() as u32, + )?; region.assign_advice( || "is_write", config.is_write, @@ -219,7 +220,10 @@ impl Circuit for StateCircuit { config.sort_keys.id.assign(&mut region, offset, id as u32)?; } if let Some(address) = row.address() { - config.sort_keys.address.assign(&mut region, offset, address)?; + config + .sort_keys + .address + .assign(&mut region, offset, address)?; } if let Some(field_tag) = row.field_tag() { region.assign_advice( @@ -245,7 +249,9 @@ impl Circuit for StateCircuit { )?; if offset != 0 { - lexicographic_ordering_chip.assign(&mut region, offset, row, prev_row)?; + config + .lexicographic_ordering + .assign(&mut region, offset, row, prev_row)?; let id_change = F::from(row.id().unwrap_or_default() as u64) - F::from(prev_row.id().unwrap_or_default() as u64); @@ -284,7 +290,8 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer rw_counter: MpiQueries::new(meta, c.sort_keys.rw_counter), is_write: meta.query_advice(c.is_write, Rotation::cur()), tag: c.sort_keys.tag.value(Rotation::cur())(meta), - tag_bits: c.sort_keys + tag_bits: c + .sort_keys .tag .bits .map(|bit| meta.query_advice(bit, Rotation::cur())), @@ -299,10 +306,10 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer .power_of_randomness .map(|c| meta.query_instance(c, Rotation::cur())), is_storage_key_unchanged: c.is_storage_key_unchanged.is_zero_expression.clone(), - lexicographic_ordering_upper_limb_difference_is_zero: c - .lexicographic_ordering - .upper_limb_difference_is_zero - .is_zero_expression - .clone(), + /* lexicographic_ordering_upper_limb_difference_is_zero: c + * .lexicographic_ordering + * .upper_limb_difference_is_zero + * .is_zero_expression + * .clone(), */ } } diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 063479164a..a5650ef132 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -30,7 +30,7 @@ pub struct Queries { pub lookups: LookupsQueries, pub power_of_randomness: [Expression; N_BYTES_WORD - 1], pub is_storage_key_unchanged: Expression, - pub lexicographic_ordering_upper_limb_difference_is_zero: Expression, + // pub lexicographic_ordering_upper_limb_difference_is_zero: Expression, } type Constraint = (&'static str, Expression); @@ -297,10 +297,10 @@ impl Queries { fn first_access(&self) -> Expression { or::expr(&[ - not::expr( - self.lexicographic_ordering_upper_limb_difference_is_zero - .clone(), - ), + // not::expr( + // self.lexicographic_ordering_upper_limb_difference_is_zero + // .clone(), + // ), not::expr(self.is_storage_key_unchanged.clone()), ]) } diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 9af23fc967..18db6afe14 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -1,20 +1,21 @@ use super::{ - binary_number::Config as BinaryNumberConfig, SortKeysConfig, N_LIMBS_ACCOUNT_ADDRESS, - N_LIMBS_ID, N_LIMBS_RW_COUNTER, + binary_number::{AsBits, Chip as BinaryNumberChip, Config as BinaryNumberConfig}, + SortKeysConfig, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER, }; use crate::{ evm_circuit::{param::N_BYTES_WORD, table::RwTableTag, witness::Rw}, util::Expr, }; use eth_types::{Field, ToBigEndian}; -use gadgets::is_zero::{IsZeroChip, IsZeroConfig, IsZeroInstruction}; use halo2_proofs::{ circuit::Region, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, poly::Rotation, }; use itertools::Itertools; -use std::ops::Mul; +use std::iter::once; +use strum::IntoEnumIterator; +use strum_macros::{EnumCount, EnumIter}; // We use this chip to show that the rows of the rw table are in lexicographic // order, i.e. ordered by (tag, field_tag, id, address, storage_key, and @@ -71,130 +72,119 @@ use std::ops::Mul; // ----------------------------------- // = 480 bits -#[derive(Clone)] -pub struct Config { - pub(crate) selector: Column, - upper_limb_difference: Column, - pub(crate) upper_limb_difference_is_zero: IsZeroConfig, - lower_limb_difference: Column, - lower_limb_difference_is_zero: IsZeroConfig, +#[derive(Clone, Copy, Debug, EnumIter, EnumCount)] +enum Limb { + Tag, + Id1, + Id0, + FieldTag, + Address9, + Address8, + Address7, + Address6, + Address5, + Address4, + Address3, + Address2, + Address1, + Address0, + StorageKey15, + StorageKey14, + StorageKey13, + StorageKey12, + StorageKey11, + StorageKey10, + StorageKey9, + StorageKey8, + StorageKey7, + StorageKey6, + StorageKey5, + StorageKey4, + StorageKey3, + StorageKey2, + StorageKey1, + StorageKey0, + RwCounter1, + RwCounter0, } -pub struct Chip { - config: Config, +impl AsBits<5> for Limb { + fn as_bits(&self) -> [bool; 5] { + let mut bits = [false; 5]; + let mut x = *self as u8; + for i in 0..5 { + bits[4 - i] = x % 2 == 1; + x /= 2; + } + bits + } } -impl Chip { - pub fn construct(config: Config) -> Self { - Self { config } - } +#[derive(Clone)] +pub struct Config { + pub(crate) selector: Column, + first_different_limb: BinaryNumberConfig, + limb_difference: Column, + limb_difference_inverse: Column, +} - pub fn configure( +impl Config { + pub fn configure( meta: &mut ConstraintSystem, keys: SortKeysConfig, u16_range: Column, - ) -> Config { + ) -> Self { let selector = meta.fixed_column(); - let [upper_limb_difference, upper_limb_difference_inverse, lower_limb_difference, lower_limb_difference_inverse] = - [0; 4].map(|_| meta.advice_column()); - let [upper_limb_difference_is_zero_config, lower_limb_difference_is_zero_config] = [ - (upper_limb_difference, upper_limb_difference_inverse), - (lower_limb_difference, lower_limb_difference_inverse), - ] - .map(|(value, advice)| { - IsZeroChip::configure( - meta, - |meta| meta.query_fixed(selector, Rotation::cur()), - |meta| meta.query_advice(value, Rotation::cur()), - advice, - ) - }); - - let upper_limb_difference_is_zero = upper_limb_difference_is_zero_config - .is_zero_expression - .clone(); - let lower_limb_difference_is_zero = lower_limb_difference_is_zero_config - .is_zero_expression - .clone(); + let first_different_limb = BinaryNumberChip::configure(meta, selector); + let limb_difference = meta.advice_column(); + let limb_difference_inverse = meta.advice_column(); let config = Config { selector, - upper_limb_difference, - upper_limb_difference_is_zero: upper_limb_difference_is_zero_config, - lower_limb_difference, - lower_limb_difference_is_zero: lower_limb_difference_is_zero_config, + first_different_limb, + limb_difference, + limb_difference_inverse, }; - meta.create_gate("upper_limb_difference is one of 15 values", |meta| { - let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, &config, keys, Rotation::cur()); - let prev = Queries::new(meta, &config, keys, Rotation::prev()); - let upper_limb_difference = meta.query_advice(upper_limb_difference, Rotation::cur()); - vec![ - selector - * upper_limb_difference_possible_values(cur, prev) - .iter() - .map(|e| upper_limb_difference.clone() - e.clone()) - .fold(1.expr(), Expression::mul), - ] - }); - assert!(meta.degree() <= 16); - meta.create_gate( - "upper_limb_difference is zero iff all 15 possible values are 0", - |meta| { - let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, &config, keys, Rotation::cur()); - let prev = Queries::new(meta, &config, keys, Rotation::prev()); - vec![ - // all 15 possible values are 0 iff the final linear combination is 0 - selector - * upper_limb_difference_is_zero.clone() - * upper_limb_difference_possible_values(cur, prev)[14].clone(), - ] - }, - ); - meta.create_gate("lower_limb_difference is one of 15 values", |meta| { - let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, &config, keys, Rotation::cur()); - let prev = Queries::new(meta, &config, keys, Rotation::prev()); - let lower_limb_difference = meta.query_advice(lower_limb_difference, Rotation::cur()); - vec![ - selector - * lower_limb_difference_possible_values(cur, prev) - .iter() - .map(|e| lower_limb_difference.clone() - e.clone()) - .fold(1.expr(), Expression::mul), - ] - }); - assert!(meta.degree() <= 16); - meta.lookup_any("upper_limb_difference fits into u16", |meta| { - let upper_limb_difference = meta.query_advice(upper_limb_difference, Rotation::cur()); + + meta.lookup_any("limb_difference fits into u16", |meta| { vec![( - upper_limb_difference, + meta.query_advice(limb_difference, Rotation::cur()), meta.query_fixed(u16_range, Rotation::cur()), )] }); - meta.lookup_any( - "upper_limb_difference is zero or lower_limb_difference fits into u16", - |meta| { - let lower_limb_difference = - meta.query_advice(lower_limb_difference, Rotation::cur()); - vec![( - upper_limb_difference_is_zero * lower_limb_difference, - meta.query_fixed(u16_range, Rotation::cur()), - )] - }, - ); - assert!(meta.degree() <= 16); - meta.create_gate("lower_limb_difference is not zero", |meta| { + + meta.create_gate("limb_difference is not zero", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); - vec![(selector * lower_limb_difference_is_zero)] + let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); + let limb_difference_inverse = + meta.query_advice(limb_difference_inverse, Rotation::cur()); + vec![selector * (1.expr() - limb_difference * limb_difference_inverse)] }); - assert!(meta.degree() <= 16); + + meta.create_gate("limbs match before first_different_limb", |meta| { + let selector = meta.query_fixed(selector, Rotation::cur()); + let cur = Queries::new(meta, keys, Rotation::cur()); + let prev = Queries::new(meta, keys, Rotation::prev()); + let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); + + let mut constraints = vec![]; + for (limb, e) in Limb::iter().zip(&limb_difference_possible_values(cur, prev)) { + constraints.push( + selector.clone() + * first_different_limb.value_equals(&limb, Rotation::cur())(meta) + * e.clone(), + ) + } + constraints + }); + + // need one more constraint here that limb difference is the difference of the + // cliamed limbs config } - pub fn assign( + pub fn assign( &self, region: &mut Region<'_, F>, offset: usize, @@ -203,53 +193,40 @@ impl Chip { ) -> Result<(), Error> { region.assign_fixed( || "upper_limb_difference", - self.config.selector, + self.selector, offset, || Ok(F::one()), )?; - // this doesn't make sense that we have to "construct" the chip every time we - // assign? - let upper_limb_difference_is_zero_chip = - IsZeroChip::construct(self.config.upper_limb_difference_is_zero.clone()); - let lower_limb_difference_is_zero_chip = - IsZeroChip::construct(self.config.lower_limb_difference_is_zero.clone()); - let cur_be_limbs = rw_to_be_limbs(cur); let prev_be_limbs = rw_to_be_limbs(prev); - let find_result = cur_be_limbs - .iter() + let find_result = Limb::iter() + .zip(&cur_be_limbs) .zip(&prev_be_limbs) - .enumerate() - .find(|(_, (a, b))| a != b); - let (index, (cur_limb, prev_limb)) = if cfg!(test) { - find_result.unwrap_or((30, (&0, &0))) + .find(|((_, a), b)| a != b); + let ((index, cur_limb), prev_limb) = if cfg!(test) { + find_result.unwrap_or(((Limb::RwCounter0, &0), &0)) } else { find_result.expect("repeated rw counter") }; - let mut upper_limb_difference = F::from(*cur_limb as u64) - F::from(*prev_limb as u64); - let mut lower_limb_difference = lower_limb_difference_value(&cur_be_limbs, &prev_be_limbs); - if index >= 15 { - lower_limb_difference = upper_limb_difference; - upper_limb_difference = F::zero(); - } + BinaryNumberChip::construct(self.first_different_limb).assign(region, offset, index)?; + let limb_difference = F::from(*cur_limb as u64) - F::from(*prev_limb as u64); region.assign_advice( - || "upper_limb_difference", - self.config.upper_limb_difference, + || "limb_difference", + self.limb_difference, offset, - || Ok(upper_limb_difference), + || Ok(limb_difference.clone()), )?; region.assign_advice( - || "lower_limb_difference", - self.config.lower_limb_difference, + || "limb_difference_inverse", + self.limb_difference_inverse, offset, - || Ok(lower_limb_difference), + || Ok(limb_difference.invert().unwrap()), )?; - upper_limb_difference_is_zero_chip.assign(region, offset, Some(upper_limb_difference))?; - lower_limb_difference_is_zero_chip.assign(region, offset, Some(lower_limb_difference))?; + Ok(()) } } @@ -264,7 +241,7 @@ struct Queries { } impl Queries { - fn new(meta: &mut VirtualCells<'_, F>, config: &Config, keys: SortKeysConfig, rotation: Rotation) -> Self { + fn new(meta: &mut VirtualCells<'_, F>, keys: SortKeysConfig, rotation: Rotation) -> Self { let tag = keys.tag.value(rotation)(meta); let mut query_advice = |column| meta.query_advice(column, rotation); Self { @@ -277,10 +254,6 @@ impl Queries { } } - fn packed_tags(&self) -> Expression { - (1u64 << 5).expr() * self.tag.clone() + self.field_tag.clone() - } - fn storage_key_be_limbs(&self) -> Vec> { self.storage_key_bytes .iter() @@ -291,32 +264,23 @@ impl Queries { } fn be_limbs(&self) -> Vec> { - let mut limbs: Vec<_> = self - .id_limbs - .iter() - .rev() + once(&self.tag) + .chain(self.id_limbs.iter().rev()) + .chain(once(&self.field_tag)) .chain(self.address_limbs.iter().rev()) .chain(&self.storage_key_be_limbs()) .chain(self.rw_counter_limbs.iter().rev()) .cloned() - .collect(); - // The packed tags are shifted left by 7 bits so that they occupy the most - // significant 9 bits of the first 16-bit limb. - limbs[0] = limbs[0].clone() + self.packed_tags() * (1u64 << 7).expr(); - limbs + .collect() } } fn rw_to_be_limbs(row: &Rw) -> Vec { - let mut id = row.id().unwrap_or_default() as u32; - assert_eq!(id.to_be_bytes().len(), 4); - // The max value of `id` is 2^23 - 1, so the 9 most significant bits should be - // 0. We use these 9 bits to hold value of `tag` and `field_tag`. - assert!(id < (1 << 23)); - id += (((row.tag() as u32) << 5) + (row.field_tag().unwrap_or_default() as u32)) << 23; - - let mut be_bytes = vec![]; - be_bytes.extend_from_slice(&id.to_be_bytes()); + let mut be_bytes = vec![0u8]; + be_bytes.push(row.tag() as u8); + be_bytes.extend_from_slice(&(row.id().unwrap_or_default() as u32).to_be_bytes()); + be_bytes.push(0u8); + be_bytes.push(row.field_tag().unwrap_or_default() as u8); be_bytes.extend_from_slice(&(row.address().unwrap_or_default().0)); be_bytes.extend_from_slice(&(row.storage_key().unwrap_or_default().to_be_bytes())); be_bytes.extend_from_slice(&((row.rw_counter() as u32).to_be_bytes())); @@ -328,39 +292,26 @@ fn rw_to_be_limbs(row: &Rw) -> Vec { .collect() } -fn upper_limb_difference_possible_values( +fn limb_difference_possible_values( cur: Queries, prev: Queries, ) -> Vec> { let mut result = vec![]; let mut partial_sum = 0u64.expr(); - for (cur_limb, prev_limb) in cur.be_limbs()[..15].iter().zip(&prev.be_limbs()[..15]) { + for (cur_limb, prev_limb) in cur.be_limbs().iter().zip(&prev.be_limbs()) { + result.push(partial_sum.clone()); partial_sum = partial_sum * (1u64 << 16).expr() + cur_limb.clone() - prev_limb.clone(); - result.push(partial_sum.clone()) } result } -fn lower_limb_difference_possible_values( - cur: Queries, - prev: Queries, -) -> Vec> { - let mut result = vec![]; - let mut partial_sum = 0u64.expr(); - for (cur_limb, prev_limb) in cur.be_limbs()[15..].iter().zip(&prev.be_limbs()[15..]) { - partial_sum = partial_sum * (1u64 << 16).expr() + cur_limb.clone() - prev_limb.clone(); - result.push(partial_sum.clone()) - } - assert_eq!(result.len(), 15); - result -} +#[cfg(test)] +mod test { + use super::Limb; + use strum::IntoEnumIterator; -fn lower_limb_difference_value(cur_limbs: &[u16], prev_limbs: &[u16]) -> F { - be_limbs_to_value::(&cur_limbs[15..]) - be_limbs_to_value::(&prev_limbs[15..]) -} - -fn be_limbs_to_value(limbs: &[u16]) -> F { - limbs.iter().fold(F::zero(), |result, &limb| { - result * F::from(1u64 << 16) + F::from(limb as u64) - }) + #[test] + fn n_limbs() { + assert_eq!(Limb::iter().len(), 32); + } } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 02a8bffe28..9f19805e2f 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -44,20 +44,20 @@ impl AdviceColumn { pub fn value(&self, config: &StateConfig) -> Column { match self { Self::IsWrite => config.is_write, - Self::Address => config.address.value, - Self::AddressLimb0 => config.address.limbs[0], - Self::AddressLimb1 => config.address.limbs[1], - Self::StorageKey => config.storage_key.encoded, - Self::StorageKeyByte0 => config.storage_key.bytes[0], - Self::StorageKeyByte1 => config.storage_key.bytes[1], + Self::Address => config.sort_keys.address.value, + Self::AddressLimb0 => config.sort_keys.address.limbs[0], + Self::AddressLimb1 => config.sort_keys.address.limbs[1], + Self::StorageKey => config.sort_keys.storage_key.encoded, + Self::StorageKeyByte0 => config.sort_keys.storage_key.bytes[0], + Self::StorageKeyByte1 => config.sort_keys.storage_key.bytes[1], Self::StorageKeyChangeInverse => config.is_storage_key_unchanged.value_inv, Self::Value => config.value, - Self::RwCounter => config.rw_counter.value, - Self::RwCounterLimb0 => config.rw_counter.limbs[0], - Self::TagBit0 => config.tag.bits[0], - Self::TagBit1 => config.tag.bits[1], - Self::TagBit2 => config.tag.bits[2], - Self::TagBit3 => config.tag.bits[3], + Self::RwCounter => config.sort_keys.rw_counter.value, + Self::RwCounterLimb0 => config.sort_keys.rw_counter.limbs[0], + Self::TagBit0 => config.sort_keys.tag.bits[0], + Self::TagBit1 => config.sort_keys.tag.bits[1], + Self::TagBit2 => config.sort_keys.tag.bits[2], + Self::TagBit3 => config.sort_keys.tag.bits[3], } } } @@ -87,7 +87,7 @@ fn test_state_circuit_ok( fn degree() { let mut meta = ConstraintSystem::::default(); StateCircuit::configure(&mut meta); - assert_eq!(meta.degree(), 16); + assert_eq!(meta.degree(), 9); } #[test] @@ -418,10 +418,7 @@ fn nonlexicographic_order_tag() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] @@ -442,10 +439,7 @@ fn nonlexicographic_order_field_tag() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] @@ -466,10 +460,7 @@ fn nonlexicographic_order_id() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] @@ -492,10 +483,7 @@ fn nonlexicographic_order_address() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] @@ -522,10 +510,7 @@ fn nonlexicographic_order_storage_key_upper() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] @@ -552,10 +537,7 @@ fn nonlexicographic_order_storage_key_lower() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference is zero or lower_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] @@ -576,10 +558,7 @@ fn nonlexicographic_order_rw_counter() { }; assert_eq!(verify(vec![first, second]), Ok(())); - assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference is zero or lower_limb_difference fits into u16", - ); + assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } #[test] From e5bd60b27fc65446c52fef0f6ff452ee272bfe38 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 10:34:08 -0400 Subject: [PATCH 15/51] Fix first_access expression and remove unused IsZero gadget --- zkevm-circuits/src/state_circuit.rs | 61 ++++++++----------- .../src/state_circuit/constraint_builder.rs | 12 +--- .../state_circuit/lexicographic_ordering.rs | 5 +- zkevm-circuits/src/state_circuit/test.rs | 14 +---- 4 files changed, 31 insertions(+), 61 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index d6fbc2e5c2..ad7cd7e823 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -11,9 +11,10 @@ mod test; use crate::evm_circuit::{ param::N_BYTES_WORD, table::RwTableTag, - util::RandomLinearCombination, + util::{not, RandomLinearCombination}, witness::{Rw, RwMap}, }; +use crate::util::Expr; use binary_number::{Chip as BinaryNumberChip, Config as BinaryNumberConfig}; use constraint_builder::{ConstraintBuilder, Queries}; use eth_types::{Address, Field, ToLittleEndian}; @@ -25,7 +26,7 @@ use halo2_proofs::{ }, poly::Rotation, }; -use lexicographic_ordering::Config as LexicographicOrderingConfig; +use lexicographic_ordering::{Config as LexicographicOrderingConfig, Limb}; use lookups::{Chip as LookupsChip, Config as LookupsConfig, Queries as LookupsQueries}; use multiple_precision_integer::{Chip as MpiChip, Config as MpiConfig, Queries as MpiQueries}; use random_linear_combination::{Chip as RlcChip, Config as RlcConfig, Queries as RlcQueries}; @@ -45,11 +46,10 @@ pub struct StateConfig { sort_keys: SortKeysConfig, is_write: Column, is_id_unchanged: IsZeroConfig, - is_storage_key_unchanged: IsZeroConfig, // can be removed value: Column, + lexicographic_ordering: LexicographicOrderingConfig, lookups: LookupsConfig, power_of_randomness: [Column; N_BYTES_WORD - 1], - lexicographic_ordering: LexicographicOrderingConfig, } /// Keys for sorting the rows of the state circuit @@ -118,8 +118,8 @@ impl Circuit for StateCircuit { let lookups = LookupsChip::configure(meta); let power_of_randomness = [0; N_BYTES_WORD - 1].map(|_| meta.instance_column()); - let [is_write, field_tag, value, is_id_unchanged_column, is_storage_key_unchanged_column] = - [0; 5].map(|_| meta.advice_column()); + let [is_write, field_tag, value, is_id_unchanged_column] = + [0; 4].map(|_| meta.advice_column()); let tag = BinaryNumberChip::configure(meta, selector); @@ -149,15 +149,6 @@ impl Circuit for StateCircuit { }, is_id_unchanged_column, ); - let is_storage_key_unchanged = IsZeroChip::configure( - meta, - |meta| meta.query_fixed(lexicographic_ordering.selector, Rotation::cur()), - |meta| { - meta.query_advice(storage_key.encoded, Rotation::cur()) - - meta.query_advice(storage_key.encoded, Rotation::prev()) - }, - is_storage_key_unchanged_column, - ); let config = Self::Config { selector, @@ -166,7 +157,6 @@ impl Circuit for StateCircuit { is_id_unchanged, value, lexicographic_ordering, - is_storage_key_unchanged, lookups, power_of_randomness, }; @@ -192,8 +182,6 @@ impl Circuit for StateCircuit { LookupsChip::construct(config.lookups).load(&mut layouter)?; let is_id_unchanged = IsZeroChip::construct(config.is_id_unchanged.clone()); - let is_storage_key_unchanged = - IsZeroChip::construct(config.is_storage_key_unchanged.clone()); let tag_chip = BinaryNumberChip::construct(config.sort_keys.tag); @@ -256,19 +244,6 @@ impl Circuit for StateCircuit { let id_change = F::from(row.id().unwrap_or_default() as u64) - F::from(prev_row.id().unwrap_or_default() as u64); is_id_unchanged.assign(&mut region, offset, Some(id_change))?; - - let storage_key_change = RandomLinearCombination::random_linear_combine( - row.storage_key().unwrap_or_default().to_le_bytes(), - self.randomness, - ) - RandomLinearCombination::random_linear_combine( - prev_row.storage_key().unwrap_or_default().to_le_bytes(), - self.randomness, - ); - is_storage_key_unchanged.assign( - &mut region, - offset, - Some(storage_key_change), - )?; } } @@ -305,11 +280,23 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer power_of_randomness: c .power_of_randomness .map(|c| meta.query_instance(c, Rotation::cur())), - is_storage_key_unchanged: c.is_storage_key_unchanged.is_zero_expression.clone(), - /* lexicographic_ordering_upper_limb_difference_is_zero: c - * .lexicographic_ordering - * .upper_limb_difference_is_zero - * .is_zero_expression - * .clone(), */ + // this isn't binary! 0 only if most significant 4 bits are all 1. + first_access: 4.expr() + - meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[0], + Rotation::cur(), + ) + - meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[1], + Rotation::cur(), + ) + - meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[2], + Rotation::cur(), + ) + - meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[3], + Rotation::cur(), + ), } } diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index a5650ef132..f7ff64fceb 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -29,8 +29,7 @@ pub struct Queries { pub value: Expression, pub lookups: LookupsQueries, pub power_of_randomness: [Expression; N_BYTES_WORD - 1], - pub is_storage_key_unchanged: Expression, - // pub lexicographic_ordering_upper_limb_difference_is_zero: Expression, + pub first_access: Expression, } type Constraint = (&'static str, Expression); @@ -107,6 +106,7 @@ impl ConstraintBuilder { self.require_zero("rw_counter is 0 for Start", q.rw_counter.value.clone()); } + // 4+ 5 + 1 + 1+ 1 = 12 -> can reduce to 11... fn build_memory_constraints(&mut self, q: &Queries) { self.require_zero("field_tag is 0 for Memory", q.field_tag()); self.require_zero("storage_key is 0 for Memory", q.storage_key.encoded.clone()); @@ -296,13 +296,7 @@ impl Queries { } fn first_access(&self) -> Expression { - or::expr(&[ - // not::expr( - // self.lexicographic_ordering_upper_limb_difference_is_zero - // .clone(), - // ), - not::expr(self.is_storage_key_unchanged.clone()), - ]) + self.first_access.clone() } fn address_change(&self) -> Expression { diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 18db6afe14..010040f874 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -73,7 +73,8 @@ use strum_macros::{EnumCount, EnumIter}; // = 480 bits #[derive(Clone, Copy, Debug, EnumIter, EnumCount)] -enum Limb { +// TODO: unpub this +pub enum Limb { Tag, Id1, Id0, @@ -123,7 +124,7 @@ impl AsBits<5> for Limb { #[derive(Clone)] pub struct Config { pub(crate) selector: Column, - first_different_limb: BinaryNumberConfig, + pub first_different_limb: BinaryNumberConfig, limb_difference: Column, limb_difference_inverse: Column, } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 9f19805e2f..c895f7dee7 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -30,7 +30,6 @@ pub enum AdviceColumn { StorageKey, StorageKeyByte0, StorageKeyByte1, - StorageKeyChangeInverse, Value, RwCounter, RwCounterLimb0, @@ -50,7 +49,6 @@ impl AdviceColumn { Self::StorageKey => config.sort_keys.storage_key.encoded, Self::StorageKeyByte0 => config.sort_keys.storage_key.bytes[0], Self::StorageKeyByte1 => config.sort_keys.storage_key.bytes[1], - Self::StorageKeyChangeInverse => config.is_storage_key_unchanged.value_inv, Self::Value => config.value, Self::RwCounter => config.sort_keys.rw_counter.value, Self::RwCounterLimb0 => config.sort_keys.rw_counter.limbs[0], @@ -344,13 +342,7 @@ fn storage_key_mismatch() { tx_id: 4, committed_value: U256::from(5), }]; - let overrides = HashMap::from([ - ((AdviceColumn::StorageKey, 1), Fr::from(10)), - ( - (AdviceColumn::StorageKeyChangeInverse, 1), - Fr::from(10).invert().unwrap(), - ), - ]); + let overrides = HashMap::from([((AdviceColumn::StorageKey, 1), Fr::from(10))]); let result = verify_with_overrides(rows, overrides); @@ -373,10 +365,6 @@ fn storage_key_byte_out_of_range() { ((AdviceColumn::StorageKey, 1), Fr::from(256)), ((AdviceColumn::StorageKeyByte0, 1), Fr::from(256)), ((AdviceColumn::StorageKeyByte1, 1), Fr::zero()), - ( - (AdviceColumn::StorageKeyChangeInverse, 1), - Fr::from(256).invert().unwrap(), - ), ]); let result = verify_with_overrides(rows, overrides); From bc80250911834fa823f9dc9fd5c22d051fd73c2b Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 11:12:44 -0400 Subject: [PATCH 16/51] Clean up invalid values gate --- zkevm-circuits/src/state_circuit.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index ad7cd7e823..1e552fa3ec 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -280,7 +280,7 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer power_of_randomness: c .power_of_randomness .map(|c| meta.query_instance(c, Rotation::cur())), - // this isn't binary! 0 only if most significant 4 bits are all 1. + // this isn't binary! only 0 if most significant 4 bits are all 1. first_access: 4.expr() - meta.query_advice( c.lexicographic_ordering.first_different_limb.bits[0], From 725b53beb2d391e83120813426ae8a48677d667e Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 12:36:07 -0400 Subject: [PATCH 17/51] Replace is_id_uncchanged with binary expression --- zkevm-circuits/src/state_circuit.rs | 47 +++++++------------ .../src/state_circuit/constraint_builder.rs | 6 +-- .../state_circuit/lexicographic_ordering.rs | 10 ++-- zkevm-circuits/src/state_circuit/test.rs | 2 +- 4 files changed, 27 insertions(+), 38 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 1e552fa3ec..627c44cabd 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -18,7 +18,6 @@ use crate::util::Expr; use binary_number::{Chip as BinaryNumberChip, Config as BinaryNumberConfig}; use constraint_builder::{ConstraintBuilder, Queries}; use eth_types::{Address, Field, ToLittleEndian}; -use gadgets::is_zero::{IsZeroChip, IsZeroConfig, IsZeroInstruction}; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner}, plonk::{ @@ -39,13 +38,12 @@ const N_LIMBS_ACCOUNT_ADDRESS: usize = 10; const N_LIMBS_ID: usize = 2; /// Config for StateCircuit -#[derive(Clone)] -pub struct StateConfig { +#[derive(Clone, Copy)] +pub struct StateConfig { selector: Column, // Figure out why you get errors when this is Selector. // https://github.com/appliedzkp/zkevm-circuits/issues/407 sort_keys: SortKeysConfig, is_write: Column, - is_id_unchanged: IsZeroConfig, value: Column, lexicographic_ordering: LexicographicOrderingConfig, lookups: LookupsConfig, @@ -57,8 +55,8 @@ pub struct StateConfig { pub struct SortKeysConfig { tag: BinaryNumberConfig, id: MpiConfig, - field_tag: Column, address: MpiConfig, + field_tag: Column, storage_key: RlcConfig, rw_counter: MpiConfig, } @@ -82,9 +80,8 @@ impl StateCircuit { ( row.tag() as u64, row.id().unwrap_or_default(), - row.field_tag().unwrap_or_default(), row.address().unwrap_or_default(), - // row.field_tag().unwrap_or_default(), // this is the correct place + row.field_tag().unwrap_or_default(), row.storage_key().unwrap_or_default(), row.rw_counter(), ) @@ -106,7 +103,7 @@ impl StateCircuit { } impl Circuit for StateCircuit { - type Config = StateConfig; + type Config = StateConfig; type FloorPlanner = SimpleFloorPlanner; fn without_witnesses(&self) -> Self { @@ -118,8 +115,7 @@ impl Circuit for StateCircuit { let lookups = LookupsChip::configure(meta); let power_of_randomness = [0; N_BYTES_WORD - 1].map(|_| meta.instance_column()); - let [is_write, field_tag, value, is_id_unchanged_column] = - [0; 4].map(|_| meta.advice_column()); + let [is_write, field_tag, value] = [0; 3].map(|_| meta.advice_column()); let tag = BinaryNumberChip::configure(meta, selector); @@ -140,21 +136,10 @@ impl Circuit for StateCircuit { let lexicographic_ordering = LexicographicOrderingConfig::configure(meta, sort_keys, lookups.u16); - let is_id_unchanged = IsZeroChip::configure( - meta, - |meta| meta.query_fixed(lexicographic_ordering.selector, Rotation::cur()), - |meta| { - meta.query_advice(id.value, Rotation::cur()) - - meta.query_advice(id.value, Rotation::prev()) - }, - is_id_unchanged_column, - ); - let config = Self::Config { selector, sort_keys, is_write, - is_id_unchanged, value, lexicographic_ordering, lookups, @@ -181,8 +166,6 @@ impl Circuit for StateCircuit { ) -> Result<(), Error> { LookupsChip::construct(config.lookups).load(&mut layouter)?; - let is_id_unchanged = IsZeroChip::construct(config.is_id_unchanged.clone()); - let tag_chip = BinaryNumberChip::construct(config.sort_keys.tag); layouter.assign_region( @@ -240,10 +223,6 @@ impl Circuit for StateCircuit { config .lexicographic_ordering .assign(&mut region, offset, row, prev_row)?; - - let id_change = F::from(row.id().unwrap_or_default() as u64) - - F::from(prev_row.id().unwrap_or_default() as u64); - is_id_unchanged.assign(&mut region, offset, Some(id_change))?; } } @@ -259,7 +238,7 @@ impl Circuit for StateCircuit { } } -fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { +fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { Queries { selector: meta.query_fixed(c.selector, Rotation::cur()), rw_counter: MpiQueries::new(meta, c.sort_keys.rw_counter), @@ -271,7 +250,17 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Quer .bits .map(|bit| meta.query_advice(bit, Rotation::cur())), id: MpiQueries::new(meta, c.sort_keys.id), - is_id_unchanged: c.is_id_unchanged.is_zero_expression.clone(), + is_tag_and_id_unchanged: not::expr( + c.lexicographic_ordering + .first_different_limb + .value_equals(&Limb::Tag, Rotation::cur())(meta) + + c.lexicographic_ordering + .first_different_limb + .value_equals(&Limb::Id1, Rotation::cur())(meta) + + c.lexicographic_ordering + .first_different_limb + .value_equals(&Limb::Id0, Rotation::cur())(meta), + ), address: MpiQueries::new(meta, c.sort_keys.address), field_tag: meta.query_advice(c.sort_keys.field_tag, Rotation::cur()), storage_key: RlcQueries::new(meta, c.sort_keys.storage_key), diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index f7ff64fceb..8ab81da54b 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -22,7 +22,7 @@ pub struct Queries { pub tag: Expression, pub tag_bits: [Expression; 4], pub id: MpiQueries, - pub is_id_unchanged: Expression, + pub is_tag_and_id_unchanged: Expression, pub address: MpiQueries, pub field_tag: Expression, pub storage_key: RlcQueries, @@ -136,9 +136,9 @@ impl ConstraintBuilder { "stack address fits into 10 bits", (q.address.value.clone(), q.lookups.u10.clone()), ); - self.condition(q.is_id_unchanged.clone(), |cb| { + self.condition(q.is_tag_and_id_unchanged.clone(), |cb| { cb.require_boolean( - "if call id is the same, address change is 0 or 1", + "if previous row is Stack with unchanged call id, address change is 0 or 1", q.address_change(), ) }); diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 010040f874..497ebc8a42 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -78,7 +78,6 @@ pub enum Limb { Tag, Id1, Id0, - FieldTag, Address9, Address8, Address7, @@ -89,6 +88,7 @@ pub enum Limb { Address2, Address1, Address0, + FieldTag, StorageKey15, StorageKey14, StorageKey13, @@ -121,7 +121,7 @@ impl AsBits<5> for Limb { } } -#[derive(Clone)] +#[derive(Clone, Copy)] pub struct Config { pub(crate) selector: Column, pub first_different_limb: BinaryNumberConfig, @@ -247,9 +247,9 @@ impl Queries { let mut query_advice = |column| meta.query_advice(column, rotation); Self { tag, - field_tag: query_advice(keys.field_tag), id_limbs: keys.id.limbs.map(&mut query_advice), address_limbs: keys.address.limbs.map(&mut query_advice), + field_tag: query_advice(keys.field_tag), storage_key_bytes: keys.storage_key.bytes.map(&mut query_advice), rw_counter_limbs: keys.rw_counter.limbs.map(query_advice), } @@ -267,8 +267,8 @@ impl Queries { fn be_limbs(&self) -> Vec> { once(&self.tag) .chain(self.id_limbs.iter().rev()) - .chain(once(&self.field_tag)) .chain(self.address_limbs.iter().rev()) + .chain(once(&self.field_tag)) .chain(&self.storage_key_be_limbs()) .chain(self.rw_counter_limbs.iter().rev()) .cloned() @@ -280,9 +280,9 @@ fn rw_to_be_limbs(row: &Rw) -> Vec { let mut be_bytes = vec![0u8]; be_bytes.push(row.tag() as u8); be_bytes.extend_from_slice(&(row.id().unwrap_or_default() as u32).to_be_bytes()); + be_bytes.extend_from_slice(&(row.address().unwrap_or_default().0)); be_bytes.push(0u8); be_bytes.push(row.field_tag().unwrap_or_default() as u8); - be_bytes.extend_from_slice(&(row.address().unwrap_or_default().0)); be_bytes.extend_from_slice(&(row.storage_key().unwrap_or_default().to_be_bytes())); be_bytes.extend_from_slice(&((row.rw_counter() as u32).to_be_bytes())); diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index c895f7dee7..fceebe2b2d 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -40,7 +40,7 @@ pub enum AdviceColumn { } impl AdviceColumn { - pub fn value(&self, config: &StateConfig) -> Column { + pub fn value(&self, config: &StateConfig) -> Column { match self { Self::IsWrite => config.is_write, Self::Address => config.sort_keys.address.value, From 4bfcca737cc33a0ae66f4b96ed6edeba13617772 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 13:06:37 -0400 Subject: [PATCH 18/51] cargo fix and fix tests --- zkevm-circuits/src/state_circuit.rs | 5 +++-- zkevm-circuits/src/state_circuit/lexicographic_ordering.rs | 4 ++-- zkevm-circuits/src/state_circuit/test.rs | 6 +++--- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 627c44cabd..661b03b6a3 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -11,13 +11,13 @@ mod test; use crate::evm_circuit::{ param::N_BYTES_WORD, table::RwTableTag, - util::{not, RandomLinearCombination}, + util::not, witness::{Rw, RwMap}, }; use crate::util::Expr; use binary_number::{Chip as BinaryNumberChip, Config as BinaryNumberConfig}; use constraint_builder::{ConstraintBuilder, Queries}; -use eth_types::{Address, Field, ToLittleEndian}; +use eth_types::{Address, Field}; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner}, plonk::{ @@ -250,6 +250,7 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries .bits .map(|bit| meta.query_advice(bit, Rotation::cur())), id: MpiQueries::new(meta, c.sort_keys.id), + // this is degree five.... is_tag_and_id_unchanged: not::expr( c.lexicographic_ordering .first_different_limb diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 497ebc8a42..e1f67f1d04 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -3,7 +3,7 @@ use super::{ SortKeysConfig, N_LIMBS_ACCOUNT_ADDRESS, N_LIMBS_ID, N_LIMBS_RW_COUNTER, }; use crate::{ - evm_circuit::{param::N_BYTES_WORD, table::RwTableTag, witness::Rw}, + evm_circuit::{param::N_BYTES_WORD, witness::Rw}, util::Expr, }; use eth_types::{Field, ToBigEndian}; @@ -166,7 +166,7 @@ impl Config { let selector = meta.query_fixed(selector, Rotation::cur()); let cur = Queries::new(meta, keys, Rotation::cur()); let prev = Queries::new(meta, keys, Rotation::prev()); - let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); + let _limb_difference = meta.query_advice(limb_difference, Rotation::cur()); let mut constraints = vec![]; for (limb, e) in Limb::iter().zip(&limb_difference_possible_values(cur, prev)) { diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index fceebe2b2d..5307de4110 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -10,7 +10,7 @@ use bus_mapping::operation::{ use eth_types::{ address, evm_types::{MemoryAddress, StackAddress}, - Address, Field, ToAddress, Word, U256, + Address, ToAddress, Word, U256, }; use halo2_proofs::{ arithmetic::{BaseExt, Field as halo2_field}, @@ -85,7 +85,7 @@ fn test_state_circuit_ok( fn degree() { let mut meta = ConstraintSystem::::default(); StateCircuit::configure(&mut meta); - assert_eq!(meta.degree(), 9); + assert_eq!(meta.degree(), 12); } #[test] @@ -675,7 +675,7 @@ fn invalid_stack_address_change() { assert_error_matches( verify(rows), - "if call id is the same, address change is 0 or 1", + "if previous row is Stack with unchanged call id, address change is 0 or 1", ); } From 8f3fe8f82b3f1cc160ab8e4a79d9efd94018e7c5 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 13:56:25 -0400 Subject: [PATCH 19/51] lower degree --- zkevm-circuits/src/state_circuit.rs | 34 ++++++++++++------- .../state_circuit/lexicographic_ordering.rs | 26 +++++++++++--- zkevm-circuits/src/state_circuit/test.rs | 2 +- 3 files changed, 44 insertions(+), 18 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 661b03b6a3..a476e180ae 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -239,6 +239,14 @@ impl Circuit for StateCircuit { } fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { + let x = meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[3], + Rotation::cur(), + ) + meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[4], + Rotation::cur(), + ); + Queries { selector: meta.query_fixed(c.selector, Rotation::cur()), rw_counter: MpiQueries::new(meta, c.sort_keys.rw_counter), @@ -250,18 +258,20 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries .bits .map(|bit| meta.query_advice(bit, Rotation::cur())), id: MpiQueries::new(meta, c.sort_keys.id), - // this is degree five.... - is_tag_and_id_unchanged: not::expr( - c.lexicographic_ordering - .first_different_limb - .value_equals(&Limb::Tag, Rotation::cur())(meta) - + c.lexicographic_ordering - .first_different_limb - .value_equals(&Limb::Id1, Rotation::cur())(meta) - + c.lexicographic_ordering - .first_different_limb - .value_equals(&Limb::Id0, Rotation::cur())(meta), - ), + // this isn't binary! only 0 if most significant 3 bits are all 0 and at most 1 of the two + // least significant bits is 1. + is_tag_and_id_unchanged: 10.expr() + * (meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[0], + Rotation::cur(), + ) + meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[1], + Rotation::cur(), + ) + meta.query_advice( + c.lexicographic_ordering.first_different_limb.bits[2], + Rotation::cur(), + )) + + x.clone() * (1.expr() - x), address: MpiQueries::new(meta, c.sort_keys.address), field_tag: meta.query_advice(c.sort_keys.field_tag, Rotation::cur()), storage_key: RlcQueries::new(meta, c.sort_keys.storage_key), diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index e1f67f1d04..c3da597729 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -74,6 +74,7 @@ use strum_macros::{EnumCount, EnumIter}; #[derive(Clone, Copy, Debug, EnumIter, EnumCount)] // TODO: unpub this +// should call this limb index pub enum Limb { Tag, Id1, @@ -166,21 +167,36 @@ impl Config { let selector = meta.query_fixed(selector, Rotation::cur()); let cur = Queries::new(meta, keys, Rotation::cur()); let prev = Queries::new(meta, keys, Rotation::prev()); - let _limb_difference = meta.query_advice(limb_difference, Rotation::cur()); let mut constraints = vec![]; - for (limb, e) in Limb::iter().zip(&limb_difference_possible_values(cur, prev)) { + for (limb, e) in Limb::iter().zip(limb_difference_possible_values(cur, prev)) { constraints.push( selector.clone() * first_different_limb.value_equals(&limb, Rotation::cur())(meta) - * e.clone(), + * e, ) } constraints }); - // need one more constraint here that limb difference is the difference of the - // cliamed limbs + meta.create_gate("limb_difference is equal to the difference at claimed limb", |meta| { + let selector = meta.query_fixed(selector, Rotation::cur()); + let cur = Queries::new(meta, keys, Rotation::cur()); + let prev = Queries::new(meta, keys, Rotation::prev()); + let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); + + let mut constraints = vec![]; + for ((limb, cur_expression), prev_expression) in + Limb::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) + { + constraints.push( + selector.clone() + * first_different_limb.value_equals(&limb, Rotation::cur())(meta) + * (limb_difference.clone() - cur_expression + prev_expression), + ); + } + constraints + }); config } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 5307de4110..257bac4fd5 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -85,7 +85,7 @@ fn test_state_circuit_ok( fn degree() { let mut meta = ConstraintSystem::::default(); StateCircuit::configure(&mut meta); - assert_eq!(meta.degree(), 12); + assert_eq!(meta.degree(), 9); } #[test] From 65723bea0584a538acfdf3933e208ecff7bc7263 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 31 May 2022 14:03:03 -0400 Subject: [PATCH 20/51] clippy, fix, and fmt --- zkevm-circuits/src/state_circuit.rs | 3 +- .../state_circuit/lexicographic_ordering.rs | 41 ++++++++++--------- zkevm-circuits/src/state_circuit/test.rs | 2 +- 3 files changed, 24 insertions(+), 22 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index a476e180ae..c098162853 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -11,7 +11,6 @@ mod test; use crate::evm_circuit::{ param::N_BYTES_WORD, table::RwTableTag, - util::not, witness::{Rw, RwMap}, }; use crate::util::Expr; @@ -25,7 +24,7 @@ use halo2_proofs::{ }, poly::Rotation, }; -use lexicographic_ordering::{Config as LexicographicOrderingConfig, Limb}; +use lexicographic_ordering::Config as LexicographicOrderingConfig; use lookups::{Chip as LookupsChip, Config as LookupsConfig, Queries as LookupsQueries}; use multiple_precision_integer::{Chip as MpiChip, Config as MpiConfig, Queries as MpiQueries}; use random_linear_combination::{Chip as RlcChip, Config as RlcConfig, Queries as RlcQueries}; diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index c3da597729..bf863b47b6 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -179,24 +179,27 @@ impl Config { constraints }); - meta.create_gate("limb_difference is equal to the difference at claimed limb", |meta| { - let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, keys, Rotation::cur()); - let prev = Queries::new(meta, keys, Rotation::prev()); - let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); - - let mut constraints = vec![]; - for ((limb, cur_expression), prev_expression) in - Limb::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) - { - constraints.push( - selector.clone() - * first_different_limb.value_equals(&limb, Rotation::cur())(meta) - * (limb_difference.clone() - cur_expression + prev_expression), - ); - } - constraints - }); + meta.create_gate( + "limb_difference is equal to the difference at claimed limb", + |meta| { + let selector = meta.query_fixed(selector, Rotation::cur()); + let cur = Queries::new(meta, keys, Rotation::cur()); + let prev = Queries::new(meta, keys, Rotation::prev()); + let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); + + let mut constraints = vec![]; + for ((limb, cur_expression), prev_expression) in + Limb::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) + { + constraints.push( + selector.clone() + * first_different_limb.value_equals(&limb, Rotation::cur())(meta) + * (limb_difference.clone() - cur_expression + prev_expression), + ); + } + constraints + }, + ); config } @@ -235,7 +238,7 @@ impl Config { || "limb_difference", self.limb_difference, offset, - || Ok(limb_difference.clone()), + || Ok(limb_difference), )?; region.assign_advice( || "limb_difference_inverse", diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 257bac4fd5..7e2605483e 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -13,7 +13,7 @@ use eth_types::{ Address, ToAddress, Word, U256, }; use halo2_proofs::{ - arithmetic::{BaseExt, Field as halo2_field}, + arithmetic::BaseExt, dev::{MockProver, VerifyFailure}, pairing::bn256::Fr, plonk::{Advice, Circuit, Column, ConstraintSystem}, From 2df49e70826b8d32b9e2bd20988c438da80358e7 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 1 Jun 2022 12:10:23 -0400 Subject: [PATCH 21/51] clean up --- zkevm-circuits/src/state_circuit/lexicographic_ordering.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index bf863b47b6..544812e58f 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -15,7 +15,7 @@ use halo2_proofs::{ use itertools::Itertools; use std::iter::once; use strum::IntoEnumIterator; -use strum_macros::{EnumCount, EnumIter}; +use strum_macros::EnumIter; // We use this chip to show that the rows of the rw table are in lexicographic // order, i.e. ordered by (tag, field_tag, id, address, storage_key, and @@ -72,7 +72,7 @@ use strum_macros::{EnumCount, EnumIter}; // ----------------------------------- // = 480 bits -#[derive(Clone, Copy, Debug, EnumIter, EnumCount)] +#[derive(Clone, Copy, Debug, EnumIter)] // TODO: unpub this // should call this limb index pub enum Limb { From 9666e11dd5920c749d1c8272b0474be426d33c7d Mon Sep 17 00:00:00 2001 From: Zhang Zhuo Date: Tue, 14 Jun 2022 16:54:27 +0800 Subject: [PATCH 22/51] feat(evm-circuit): add dummy gadget (#563) * feat(evm-circuit): add dummy gadget; make sha3 uses dummy gadget; enable erc20 integration tests * some comments --- .github/workflows/integration.yml | 4 +- bus-mapping/src/evm/opcodes.rs | 2 +- integration-tests/tests/circuits.rs | 4 ++ zkevm-circuits/src/evm_circuit/execution.rs | 5 ++ .../src/evm_circuit/execution/dummy.rs | 67 +++++++++++++++++++ zkevm-circuits/src/evm_circuit/witness.rs | 1 + zkevm-circuits/src/lib.rs | 5 ++ 7 files changed, 84 insertions(+), 4 deletions(-) create mode 100644 zkevm-circuits/src/evm_circuit/execution/dummy.rs diff --git a/.github/workflows/integration.yml b/.github/workflows/integration.yml index 64968bff63..fb73b77c26 100644 --- a/.github/workflows/integration.yml +++ b/.github/workflows/integration.yml @@ -57,7 +57,5 @@ jobs: - run: ./run.sh --steps "gendata" - run: ./run.sh --steps "tests" --tests "rpc" - run: ./run.sh --steps "tests" --tests "circuit_input_builder" - # Uncomment once the evm and state circuits tests pass for the block - # where Greeter.sol is deployed. - # - run: ./run.sh --steps "tests" --tests "circuits" + - run: ./run.sh --steps "tests" --tests "circuits" - run: ./run.sh --steps "cleanup" diff --git a/bus-mapping/src/evm/opcodes.rs b/bus-mapping/src/evm/opcodes.rs index ac07957a97..24b24d5c1f 100644 --- a/bus-mapping/src/evm/opcodes.rs +++ b/bus-mapping/src/evm/opcodes.rs @@ -122,7 +122,7 @@ fn fn_gen_associated_ops(opcode_id: &OpcodeId) -> FnGenAssociatedOps { OpcodeId::SHL => StackOnlyOpcode::<2, 1>::gen_associated_ops, OpcodeId::SHR => StackOnlyOpcode::<2, 1>::gen_associated_ops, OpcodeId::SAR => StackOnlyOpcode::<2, 1>::gen_associated_ops, - // OpcodeId::SHA3 => {}, + OpcodeId::SHA3 => StackOnlyOpcode::<2, 1>::gen_associated_ops, // OpcodeId::ADDRESS => {}, // OpcodeId::BALANCE => {}, OpcodeId::ORIGIN => Origin::gen_associated_ops, diff --git a/integration-tests/tests/circuits.rs b/integration-tests/tests/circuits.rs index 9c7f17feef..81a9dd5c62 100644 --- a/integration-tests/tests/circuits.rs +++ b/integration-tests/tests/circuits.rs @@ -17,6 +17,7 @@ lazy_static! { } async fn test_evm_circuit_block(block_num: u64) { + log::info!("test evm circuit, block number: {}", block_num); let cli = get_client(); let cli = BuilderClient::new(cli).await.unwrap(); let builder = cli.gen_inputs(block_num).await.unwrap(); @@ -29,6 +30,7 @@ async fn test_state_circuit_block(block_num: u64) { use halo2_proofs::arithmetic::BaseExt; use halo2_proofs::pairing::bn256::Fr; + log::info!("test state circuit, block number: {}", block_num); let cli = get_client(); let cli = BuilderClient::new(cli).await.unwrap(); let builder = cli.gen_inputs(block_num).await.unwrap(); @@ -77,6 +79,7 @@ macro_rules! declare_tests { }; } +/* declare_tests!( test_evm_circuit_block_transfer_0, test_state_circuit_block_transfer_0, @@ -92,6 +95,7 @@ declare_tests!( test_state_circuit_multiple_transfers_0, "Multiple transfers 0" ); +*/ declare_tests!( test_evm_circuit_erc20_openzeppelin_transfer_fail, test_state_circuit_erc20_openzeppelin_transfer_fail, diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 4a4cdfefd3..34f6390096 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -39,6 +39,7 @@ mod codesize; mod comparator; mod copy_code_to_memory; mod copy_to_log; +mod dummy; mod dup; mod end_block; mod end_tx; @@ -85,6 +86,7 @@ use codesize::CodesizeGadget; use comparator::ComparatorGadget; use copy_code_to_memory::CopyCodeToMemoryGadget; use copy_to_log::CopyToLogGadget; +use dummy::DummyGadget; use dup::DupGadget; use end_block::EndBlockGadget; use end_tx::EndTxGadget; @@ -183,6 +185,7 @@ pub(crate) struct ExecutionConfig { push_gadget: PushGadget, selfbalance_gadget: SelfbalanceGadget, shr_gadget: ShrGadget, + sha3_gadget: DummyGadget, signed_comparator_gadget: SignedComparatorGadget, signextend_gadget: SignextendGadget, sload_gadget: SloadGadget, @@ -373,6 +376,7 @@ impl ExecutionConfig { pop_gadget: configure_gadget!(), push_gadget: configure_gadget!(), selfbalance_gadget: configure_gadget!(), + sha3_gadget: configure_gadget!(), shr_gadget: configure_gadget!(), signed_comparator_gadget: configure_gadget!(), signextend_gadget: configure_gadget!(), @@ -813,6 +817,7 @@ impl ExecutionConfig { ExecutionState::BLOCKCTXU160 => assign_exec_step!(self.block_ctx_u160_gadget), ExecutionState::BLOCKCTXU256 => assign_exec_step!(self.block_ctx_u256_gadget), ExecutionState::SELFBALANCE => assign_exec_step!(self.selfbalance_gadget), + ExecutionState::SHA3 => assign_exec_step!(self.sha3_gadget), ExecutionState::SHR => assign_exec_step!(self.shr_gadget), ExecutionState::SIGNEXTEND => assign_exec_step!(self.signextend_gadget), ExecutionState::SLOAD => assign_exec_step!(self.sload_gadget), diff --git a/zkevm-circuits/src/evm_circuit/execution/dummy.rs b/zkevm-circuits/src/evm_circuit/execution/dummy.rs new file mode 100644 index 0000000000..626c43b8b3 --- /dev/null +++ b/zkevm-circuits/src/evm_circuit/execution/dummy.rs @@ -0,0 +1,67 @@ +use std::marker::PhantomData; + +use crate::evm_circuit::{ + execution::ExecutionGadget, + step::ExecutionState, + util::{constraint_builder::ConstraintBuilder, CachedRegion, Word}, + witness::{Block, Call, ExecStep, Transaction}, +}; +use crate::util::Expr; +use eth_types::Field; +use eth_types::ToLittleEndian; +use halo2_proofs::plonk::Error; + +#[derive(Clone, Debug)] +pub(crate) struct DummyGadget { + pops: [Word; N_POP], + pushes: [Word; N_PUSH], + _marker: PhantomData, +} + +impl ExecutionGadget + for DummyGadget +{ + const NAME: &'static str = "DUMMY"; + + const EXECUTION_STATE: ExecutionState = S; + + fn configure(cb: &mut ConstraintBuilder) -> Self { + log::warn!( + "evm circuit: ExecutionState::{:?} is implemented with DummyGadget", + S + ); + let pops: [Word; N_POP] = [(); N_POP].map(|_| cb.query_word()); + let pushes: [Word; N_PUSH] = [(); N_PUSH].map(|_| cb.query_word()); + for pop in pops.iter() { + cb.stack_pop(pop.expr()); + } + for push in pushes.iter() { + cb.stack_push(push.expr()); + } + Self { + pops, + pushes, + _marker: PhantomData, + } + } + + fn assign_exec_step( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + block: &Block, + _: &Transaction, + _: &Call, + step: &ExecStep, + ) -> Result<(), Error> { + for i in 0..N_POP { + let value = block.rws[step.rw_indices[i]].stack_value(); + self.pops[i].assign(region, offset, Some(value.to_le_bytes()))?; + } + for i in 0..N_PUSH { + let value = block.rws[step.rw_indices[N_POP + i]].stack_value(); + self.pushes[i].assign(region, offset, Some(value.to_le_bytes()))?; + } + Ok(()) + } +} diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index 8f0d70fc86..a0c8bcc2e0 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -1214,6 +1214,7 @@ impl From<&circuit_input_builder::ExecStep> for ExecutionState { OpcodeId::DIFFICULTY | OpcodeId::BASEFEE => ExecutionState::BLOCKCTXU256, OpcodeId::GAS => ExecutionState::GAS, OpcodeId::SELFBALANCE => ExecutionState::SELFBALANCE, + OpcodeId::SHA3 => ExecutionState::SHA3, OpcodeId::SHR => ExecutionState::SHR, OpcodeId::SLOAD => ExecutionState::SLOAD, OpcodeId::SSTORE => ExecutionState::SSTORE, diff --git a/zkevm-circuits/src/lib.rs b/zkevm-circuits/src/lib.rs index ddb88f9d0f..1e65801c3d 100644 --- a/zkevm-circuits/src/lib.rs +++ b/zkevm-circuits/src/lib.rs @@ -1,5 +1,10 @@ //! # zk_evm +// We should try not to use incomplete_features unless it is really really needed and cannot be +// avoided like `adt_const_params` used by DummyGadget +#![allow(incomplete_features)] +// Needed by DummyGadget in evm circuit +#![feature(adt_const_params)] #![cfg_attr(docsrs, feature(doc_cfg))] // Temporary until we have more of the crate implemented. #![allow(dead_code)] From ed91540df38dd8e8661e924d4a6b7480706b40f3 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Thu, 16 Jun 2022 17:47:14 -0400 Subject: [PATCH 23/51] cleanup --- zkevm-circuits/src/state_circuit.rs | 2 +- zkevm-circuits/src/state_circuit/constraint_builder.rs | 1 - zkevm-circuits/src/state_circuit/lexicographic_ordering.rs | 6 ++---- 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index c098162853..f42f49119c 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -40,7 +40,7 @@ const N_LIMBS_ID: usize = 2; #[derive(Clone, Copy)] pub struct StateConfig { selector: Column, // Figure out why you get errors when this is Selector. - // https://github.com/appliedzkp/zkevm-circuits/issues/407 + // https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/407 sort_keys: SortKeysConfig, is_write: Column, value: Column, diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 29c78bf2e9..3536cb55fe 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -106,7 +106,6 @@ impl ConstraintBuilder { self.require_zero("rw_counter is 0 for Start", q.rw_counter.value.clone()); } - // 4+ 5 + 1 + 1+ 1 = 12 -> can reduce to 11... fn build_memory_constraints(&mut self, q: &Queries) { self.require_zero("field_tag is 0 for Memory", q.field_tag()); self.require_zero("storage_key is 0 for Memory", q.storage_key.encoded.clone()); diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index b9908b8083..91736f5d97 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -73,9 +73,7 @@ use strum_macros::EnumIter; // = 480 bits #[derive(Clone, Copy, Debug, EnumIter)] -// TODO: unpub this -// should call this limb index -pub enum Limb { +enum LimbIndex { Tag, Id1, Id0, @@ -125,7 +123,7 @@ impl AsBits<5> for Limb { #[derive(Clone, Copy)] pub struct Config { pub(crate) selector: Column, - pub first_different_limb: BinaryNumberConfig, + pub first_different_limb: BinaryNumberConfig, limb_difference: Column, limb_difference_inverse: Column, } From 9b2539bcbde1bd23688754369bd70d2ad6c7b3e4 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 01:34:25 -0400 Subject: [PATCH 24/51] update comments --- .../state_circuit/lexicographic_ordering.rs | 82 ++++++------------- 1 file changed, 27 insertions(+), 55 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 91736f5d97..fc296c7b3c 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -18,62 +18,33 @@ use strum::IntoEnumIterator; use strum_macros::EnumIter; // We use this chip to show that the rows of the rw table are in lexicographic -// order, i.e. ordered by (tag, field_tag, id, address, storage_key, and -// rw_counter). We do this by packing these 6 fields into a 480 bit value X, and -// then showing that X_cur > X_prev. Let A0, A1, ..., A29 be the 30 16-bit limbs -// of X_cur and B0, B1, ..., B29 be 30 16-bit limbs of X_prev, in big endian +// order, i.e. ordered by (tag, id, address, field_tag, storage_key, and +// rw_counter). We do this by packing these 6 fields into a 512 bit value X, and +// then showing that X_cur > X_prev. Let A0, A1, ..., A31 be the 32 16-bit limbs +// of X_cur and B0, B1, ..., B31 be 32 16-bit limbs of X_prev, in big endian // order. // Let // C0 = A0 - B0, // C1 = C0 << 16 + A1 - B1, // ... -// C14 = C13 << 16 + A14 - B14, -// and -// C15 = A15 - B15, -// C16 = C15 << 16 + A16 - B16, -// ... -// C29 = C28 << 16 + A29 - B29. -// We have to split the 30 limbs into upper and lower halves between C14 and C15 -// because a field element can only hold 15 16-bit limbs. - -// X_cur > X_prev iff one of the following is true: -// 1. one of C0, ..., C14 is non-zero and fits into 16 bits. -// 2. all of C0, ..., C14 are 0 and one of C15, ..., C29 is non-zero and fits -// into 16 bits. (note that "all of C0, ..., C14 are 0" is equivalent to -// "C14 is 0".) - -// We show that one of these is true with the following constraints: -// 1. upper_limb_difference is (at least) 1 of the 15 values C0, ..., C14. -// 2. lower_limb_difference is (at least) 1 of the 15 values C15, ..., C29. -// 3. upper_limb_difference fits into 16 bits. -// 4. if upper_limb_difference is 0, then lower_limb_difference fits into 16 -// bits. -// 5. if upper_limb_difference is 0, then C14 is 0. -// 6. at least one of upper_limb_difference or lower_limb_difference is not 0. - -// We satisfy these constraints by assigning upper_limb_difference -// to be the first non-zero difference between the first 15 big-endian limbs of -// X_cur and X_prev or 0 if the the limbs are all equal. E.g. if X_curr = (2, 1, -// 6, ...) and X_prev = (2, 1, 2, ...), then upper_limb_difference = C2 = 6 - 2 -// = 4. If there is no difference between the first 15 pairs of limbs, then -// lower_limb_difference is assigned to be the first non-zero difference between -// the last 15 pairs of limbs. This non-zero difference will exist because there -// are no duplicate entries in the rw table. If upper_limb_difference has a -// non-zero value, then we assign lower_limb_difference to be the value of C29. - -// Packing the field into 480 bits: -// 4 bits for tag, -// + 5 bits for field_tag -// + 23 bits for id -// + 160 bits for address, -// + 256 bits for storage key -// + 32 bits for rw_counter -// ----------------------------------- -// = 480 bits +// C31 = C30 << 16 + A31 - B21. + +// X_cur > X_prev iff one of C0, ..., C31 is non-zero and fits into 16 bits. + +// We show this with following advice columns and constraints: +// - first_different_limb: first index where the limbs differ. +// - limb_difference: the difference between the limbs at first_different_limb. +// - limb_difference_inverse: the inverse of limb_difference + +// 1. limb_difference fits into 16 bits. +// 2. limb_difference is not zero because its inverse exists. +// 3. limbs before first_different_limb are equal. +// 4. limb_difference equals the difference of the limbs at +// first_different_limb. #[derive(Clone, Copy, Debug, EnumIter)] -enum LimbIndex { +pub enum LimbIndex { Tag, Id1, Id0, @@ -108,7 +79,7 @@ enum LimbIndex { RwCounter0, } -impl AsBits<5> for Limb { +impl AsBits<5> for LimbIndex { fn as_bits(&self) -> [bool; 5] { let mut bits = [false; 5]; let mut x = *self as u8; @@ -167,7 +138,8 @@ impl Config { let prev = Queries::new(meta, keys, Rotation::prev()); let mut constraints = vec![]; - for (limb, e) in Limb::iter().zip(limb_difference_possible_values(cur, prev)) { + // RLC this? + for (limb, e) in LimbIndex::iter().zip(limb_difference_possible_values(cur, prev)) { constraints.push( selector.clone() * first_different_limb.value_equals(limb, Rotation::cur())(meta) @@ -187,7 +159,7 @@ impl Config { let mut constraints = vec![]; for ((limb, cur_expression), prev_expression) in - Limb::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) + LimbIndex::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) { constraints.push( selector.clone() @@ -219,12 +191,12 @@ impl Config { let cur_be_limbs = rw_to_be_limbs(cur); let prev_be_limbs = rw_to_be_limbs(prev); - let find_result = Limb::iter() + let find_result = LimbIndex::iter() .zip(&cur_be_limbs) .zip(&prev_be_limbs) .find(|((_, a), b)| a != b); let ((index, cur_limb), prev_limb) = if cfg!(test) { - find_result.unwrap_or(((Limb::RwCounter0, &0), &0)) + find_result.unwrap_or(((LimbIndex::RwCounter0, &0), &0)) } else { find_result.expect("repeated rw counter") }; @@ -325,11 +297,11 @@ fn limb_difference_possible_values( #[cfg(test)] mod test { - use super::Limb; + use super::LimbIndex; use strum::IntoEnumIterator; #[test] fn n_limbs() { - assert_eq!(Limb::iter().len(), 32); + assert_eq!(LimbIndex::iter().len(), 32); } } From 1f50ebc2c134562cdf895757c1d13a3529931af8 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 01:47:46 -0400 Subject: [PATCH 25/51] Use RLC to avoid overflow --- zkevm-circuits/src/state_circuit.rs | 8 +++++-- .../state_circuit/lexicographic_ordering.rs | 23 ++++++++++++++----- 2 files changed, 23 insertions(+), 8 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index f42f49119c..737bba2924 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -132,8 +132,12 @@ impl Circuit for StateCircuit { rw_counter, }; - let lexicographic_ordering = - LexicographicOrderingConfig::configure(meta, sort_keys, lookups.u16); + let lexicographic_ordering = LexicographicOrderingConfig::configure( + meta, + sort_keys, + lookups.u16, + power_of_randomness, + ); let config = Self::Config { selector, diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index fc296c7b3c..c934692919 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -9,7 +9,7 @@ use crate::{ use eth_types::{Field, ToBigEndian}; use halo2_proofs::{ circuit::Region, - plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Instance, VirtualCells}, poly::Rotation, }; use itertools::Itertools; @@ -104,6 +104,7 @@ impl Config { meta: &mut ConstraintSystem, keys: SortKeysConfig, u16_range: Column, + power_of_randomness: [Column; 31], ) -> Self { let selector = meta.fixed_column(); let first_different_limb = BinaryNumberChip::configure(meta, selector); @@ -136,10 +137,13 @@ impl Config { let selector = meta.query_fixed(selector, Rotation::cur()); let cur = Queries::new(meta, keys, Rotation::cur()); let prev = Queries::new(meta, keys, Rotation::prev()); + let powers_of_randomness = + power_of_randomness.map(|i| meta.query_instance(i, Rotation::cur())); let mut constraints = vec![]; - // RLC this? - for (limb, e) in LimbIndex::iter().zip(limb_difference_possible_values(cur, prev)) { + for (limb, e) in + LimbIndex::iter().zip(rlc_limb_differences(cur, prev, powers_of_randomness)) + { constraints.push( selector.clone() * first_different_limb.value_equals(limb, Rotation::cur())(meta) @@ -282,15 +286,22 @@ fn rw_to_be_limbs(row: &Rw) -> Vec { .collect() } -fn limb_difference_possible_values( +fn rlc_limb_differences( cur: Queries, prev: Queries, + powers_of_randomness: [Expression; 31], ) -> Vec> { let mut result = vec![]; let mut partial_sum = 0u64.expr(); - for (cur_limb, prev_limb) in cur.be_limbs().iter().zip(&prev.be_limbs()) { + let powers_of_randomness = once(1.expr()).chain(powers_of_randomness.into_iter()); + for ((cur_limb, prev_limb), powers_of_randomness) in cur + .be_limbs() + .iter() + .zip(&prev.be_limbs()) + .zip(powers_of_randomness) + { result.push(partial_sum.clone()); - partial_sum = partial_sum * (1u64 << 16).expr() + cur_limb.clone() - prev_limb.clone(); + partial_sum = partial_sum + powers_of_randomness * (cur_limb.clone() - prev_limb.clone()); } result } From faaa6eb17ffabd11e73e59667feecc1dc8f17094 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 02:20:09 -0400 Subject: [PATCH 26/51] Add test --- zkevm-circuits/src/state_circuit/test.rs | 43 ++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 7e2605483e..61915ef729 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -37,6 +37,11 @@ pub enum AdviceColumn { TagBit1, TagBit2, TagBit3, + LimbIndexBit0, + LimbIndexBit1, + LimbIndexBit2, + LimbIndexBit3, + LimbIndexBit4, } impl AdviceColumn { @@ -56,6 +61,11 @@ impl AdviceColumn { Self::TagBit1 => config.sort_keys.tag.bits[1], Self::TagBit2 => config.sort_keys.tag.bits[2], Self::TagBit3 => config.sort_keys.tag.bits[3], + Self::LimbIndexBit0 => config.lexicographic_ordering.first_different_limb.bits[0], + Self::LimbIndexBit1 => config.lexicographic_ordering.first_different_limb.bits[1], + Self::LimbIndexBit2 => config.lexicographic_ordering.first_different_limb.bits[2], + Self::LimbIndexBit3 => config.lexicographic_ordering.first_different_limb.bits[3], + Self::LimbIndexBit4 => config.lexicographic_ordering.first_different_limb.bits[4], } } } @@ -549,6 +559,39 @@ fn nonlexicographic_order_rw_counter() { assert_error_matches(verify(vec![second, first]), "limb_difference fits into u16"); } +#[test] +fn lexicographic_ordering_previous_limb_differences_nonzero() { + let rows = vec![ + Rw::TxRefund { + rw_counter: 1, + is_write: true, + tx_id: 23, + value: 20, + value_prev: 40, + }, + Rw::Account { + rw_counter: 2, + is_write: true, + account_address: Address::zero(), + field_tag: AccountFieldTag::Nonce, + value: Word::zero(), + value_prev: Word::zero(), + }, + ]; + + let overrides = HashMap::from([ + ((AdviceColumn::LimbIndexBit0, 2), Fr::one()), + ((AdviceColumn::LimbIndexBit1, 2), Fr::one()), + ((AdviceColumn::LimbIndexBit2, 2), Fr::one()), + ((AdviceColumn::LimbIndexBit3, 2), Fr::one()), + ((AdviceColumn::LimbIndexBit4, 2), Fr::one()), + ]); + + let result = verify_with_overrides(rows, overrides); + + assert_error_matches(result, "limbs match before first_different_limb"); +} + #[test] #[ignore = "read consistency constraint not implemented"] fn read_inconsistency() { From caf9ab061722fb477aad3d3a2ed588ed354b8fbe Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 02:21:20 -0400 Subject: [PATCH 27/51] cleanup --- zkevm-circuits/src/state_circuit/constraint_builder.rs | 2 +- zkevm-circuits/src/state_circuit/lexicographic_ordering.rs | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 3536cb55fe..458a17830b 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -137,7 +137,7 @@ impl ConstraintBuilder { ); self.condition(q.is_tag_and_id_unchanged.clone(), |cb| { cb.require_boolean( - "if previous row is Stack with unchanged call id, address change is 0 or 1", + "if previous row is also Stack with unchanged call id, address change is 0 or 1", q.address_change(), ) }); diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index c934692919..55ebe46b91 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -162,13 +162,13 @@ impl Config { let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); let mut constraints = vec![]; - for ((limb, cur_expression), prev_expression) in + for ((i, cur_limb), prev_limb) in LimbIndex::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) { constraints.push( selector.clone() - * first_different_limb.value_equals(limb, Rotation::cur())(meta) - * (limb_difference.clone() - cur_expression + prev_expression), + * first_different_limb.value_equals(i, Rotation::cur())(meta) + * (limb_difference.clone() - cur_limb + prev_limb), ); } constraints From 18d2bc01be973774e37dc9cc8bc9196cb2fbd274 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 02:24:35 -0400 Subject: [PATCH 28/51] clean up name --- zkevm-circuits/src/state_circuit.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 737bba2924..5be3ac7a44 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -242,7 +242,7 @@ impl Circuit for StateCircuit { } fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { - let x = meta.query_advice( + let final_bits_sum = meta.query_advice( c.lexicographic_ordering.first_different_limb.bits[3], Rotation::cur(), ) + meta.query_advice( @@ -263,7 +263,7 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries id: MpiQueries::new(meta, c.sort_keys.id), // this isn't binary! only 0 if most significant 3 bits are all 0 and at most 1 of the two // least significant bits is 1. - is_tag_and_id_unchanged: 10.expr() + is_tag_and_id_unchanged: 4.expr() * (meta.query_advice( c.lexicographic_ordering.first_different_limb.bits[0], Rotation::cur(), @@ -274,7 +274,7 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries c.lexicographic_ordering.first_different_limb.bits[2], Rotation::cur(), )) - + x.clone() * (1.expr() - x), + + final_bits_sum.clone() * (1.expr() - final_bits_sum), address: MpiQueries::new(meta, c.sort_keys.address), field_tag: meta.query_advice(c.sort_keys.field_tag, Rotation::cur()), storage_key: RlcQueries::new(meta, c.sort_keys.storage_key), From 36632cd202a0bd59dd0199c142a725f3ecbc31cc Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 02:29:40 -0400 Subject: [PATCH 29/51] Add todo --- zkevm-circuits/src/state_circuit.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 5be3ac7a44..6866e5cbbc 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -263,6 +263,8 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries id: MpiQueries::new(meta, c.sort_keys.id), // this isn't binary! only 0 if most significant 3 bits are all 0 and at most 1 of the two // least significant bits is 1. + // TODO: this can mask off just the top 3 bits if you want, since the 4th limb index is + // Address9, which is always 0 for Rw::Stack rows. is_tag_and_id_unchanged: 4.expr() * (meta.query_advice( c.lexicographic_ordering.first_different_limb.bits[0], From 85752593574b774248eb5190c8f3190fde124c64 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 12:05:23 -0400 Subject: [PATCH 30/51] fix test --- zkevm-circuits/src/state_circuit/test.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 61915ef729..05be8b9f68 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -718,7 +718,7 @@ fn invalid_stack_address_change() { assert_error_matches( verify(rows), - "if previous row is Stack with unchanged call id, address change is 0 or 1", + "if previous row is also Stack with unchanged call id, address change is 0 or 1", ); } From fb776f33e02c572c582e1d24890e355d46ae1fe1 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 6 Jun 2022 14:10:05 -0400 Subject: [PATCH 31/51] Add failing test --- zkevm-circuits/src/state_circuit/test.rs | 30 ++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 02a8bffe28..75bdd05550 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -12,11 +12,12 @@ use eth_types::{ evm_types::{MemoryAddress, StackAddress}, Address, Field, ToAddress, Word, U256, }; +use halo2_proofs::poly::commitment::Params; use halo2_proofs::{ arithmetic::{BaseExt, Field as halo2_field}, dev::{MockProver, VerifyFailure}, - pairing::bn256::Fr, - plonk::{Advice, Circuit, Column, ConstraintSystem}, + pairing::bn256::{Bn256, Fr, G1Affine}, + plonk::{keygen_vk, Advice, Circuit, Column, ConstraintSystem}, }; use std::collections::{BTreeSet, HashMap}; use strum::IntoEnumIterator; @@ -90,6 +91,31 @@ fn degree() { assert_eq!(meta.degree(), 16); } +#[test] +fn verifying_key_independent_of_rw_length() { + let randomness = Fr::rand(); + let degree = 17; + let params = Params::::unsafe_setup::(degree); + + let no_rows = StateCircuit::new(randomness, RwMap::default()); + let one_row = StateCircuit::new( + randomness, + RwMap::from(&OperationContainer { + memory: vec![Operation::new( + RWCounter::from(1), + RW::WRITE, + MemoryOp::new(1, MemoryAddress::from(0), 32), + )], + ..Default::default() + }), + ); + + assert_eq!( + format!("{:?}", keygen_vk(¶ms, &no_rows).unwrap()), + format!("{:?}", keygen_vk(¶ms, &one_row).unwrap()) + ); +} + #[test] fn state_circuit_simple_2() { let memory_op_0 = Operation::new( From ed65af7ede3d517e6f26470b971f7ea8c980148a Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 6 Jun 2022 18:30:10 -0400 Subject: [PATCH 32/51] Add Rw::Padding --- zkevm-circuits/src/evm_circuit/table.rs | 1 + zkevm-circuits/src/evm_circuit/witness.rs | 28 ++++++++++++++++------- 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index cc94351f49..f5e6e88e93 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -156,6 +156,7 @@ pub enum RwTableTag { CallContext, TxLog, TxReceipt, + Padding, } impl RwTableTag { diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index b706222de1..83b347aaf5 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -524,6 +524,9 @@ pub enum Rw { field_tag: TxReceiptFieldTag, value: u64, }, + Padding { + rw_counter: usize, + }, } #[derive(Default, Clone, Copy)] pub struct RwRow { @@ -686,13 +689,14 @@ impl Rw { | Self::AccountDestructed { rw_counter, .. } | Self::CallContext { rw_counter, .. } | Self::TxLog { rw_counter, .. } - | Self::TxReceipt { rw_counter, .. } => *rw_counter, + | Self::TxReceipt { rw_counter, .. } + | Self::Padding { rw_counter } => *rw_counter, } } pub fn is_write(&self) -> bool { match self { - Self::Start => false, + Self::Start | Self::Padding { .. } => false, Self::Memory { is_write, .. } | Self::Stack { is_write, .. } | Self::AccountStorage { is_write, .. } @@ -721,6 +725,7 @@ impl Rw { Self::CallContext { .. } => RwTableTag::CallContext, Self::TxLog { .. } => RwTableTag::TxLog, Self::TxReceipt { .. } => RwTableTag::TxReceipt, + Self::Padding { .. } => RwTableTag::Padding, } } @@ -735,7 +740,10 @@ impl Rw { Self::CallContext { call_id, .. } | Self::Stack { call_id, .. } | Self::Memory { call_id, .. } => Some(*call_id), - Self::Start | Self::Account { .. } | Self::AccountDestructed { .. } => None, + Self::Start + | Self::Account { .. } + | Self::AccountDestructed { .. } + | Self::Padding { .. } => None, } } @@ -766,7 +774,8 @@ impl Rw { Self::Start | Self::CallContext { .. } | Self::TxRefund { .. } - | Self::TxReceipt { .. } => None, + | Self::TxReceipt { .. } + | Self::Padding { .. } => None, } } @@ -783,7 +792,8 @@ impl Rw { | Self::TxAccessListAccount { .. } | Self::TxAccessListAccountStorage { .. } | Self::TxRefund { .. } - | Self::AccountDestructed { .. } => None, + | Self::AccountDestructed { .. } + | Self::Padding { .. } => None, } } @@ -800,13 +810,14 @@ impl Rw { | Self::TxAccessListAccount { .. } | Self::AccountDestructed { .. } | Self::TxLog { .. } - | Self::TxReceipt { .. } => None, + | Self::TxReceipt { .. } + | Self::Padding { .. } => None, } } pub fn value_assignment(&self, randomness: F) -> F { match self { - Self::Start => F::zero(), + Self::Start | Self::Padding { .. } => F::zero(), Self::CallContext { field_tag, value, .. } => { @@ -866,7 +877,8 @@ impl Rw { | Self::Memory { .. } | Self::CallContext { .. } | Self::TxLog { .. } - | Self::TxReceipt { .. } => None, + | Self::TxReceipt { .. } + | Self::Padding { .. } => None, } } From 49b2dce84027dec6cf48718ddc710893f45d9028 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 6 Jun 2022 18:33:24 -0400 Subject: [PATCH 33/51] Add padding rows to state circuit to fix test --- zkevm-circuits/src/state_circuit.rs | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index ac5ce7394d..dc9c1c2757 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -35,6 +35,7 @@ use random_linear_combination::{Chip as RlcChip, Config as RlcConfig, Queries as use std::collections::HashMap; use std::iter::once; +const N_ROWS: usize = 1 << 16; const N_LIMBS_RW_COUNTER: usize = 2; const N_LIMBS_ACCOUNT_ADDRESS: usize = 10; const N_LIMBS_ID: usize = 2; @@ -201,8 +202,21 @@ impl Circuit for StateCircuit { layouter.assign_region( || "rw table", |mut region| { - let rows = once(&Rw::Start).chain(&self.rows); - let prev_rows = once(&Rw::Start).chain(rows.clone()); + let padding_rw_counter_start = 1 + self + .rows + .iter() + .map(Rw::rw_counter) + .max() + .unwrap_or_default(); + let padding = (self.rows.len()..N_ROWS).map(|i| Rw::Padding { + rw_counter: i + padding_rw_counter_start, + }); + + let rows = once(Rw::Start) + .chain(self.rows.iter().cloned()) + .chain(padding); + let prev_rows = once(None).chain(rows.clone().map(Some)); + for (offset, (row, prev_row)) in rows.zip(prev_rows).enumerate() { region.assign_fixed(|| "selector", config.selector, offset, || Ok(F::one()))?; config @@ -244,8 +258,8 @@ impl Circuit for StateCircuit { || Ok(row.value_assignment(self.randomness)), )?; - if offset != 0 { - lexicographic_ordering_chip.assign(&mut region, offset, row, prev_row)?; + if let Some(prev_row) = prev_row { + lexicographic_ordering_chip.assign(&mut region, offset, &row, &prev_row)?; let id_change = F::from(row.id().unwrap_or_default() as u64) - F::from(prev_row.id().unwrap_or_default() as u64); From 65db2313f08d32b63056757d27569a723ae403bc Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 6 Jun 2022 22:44:50 -0400 Subject: [PATCH 34/51] Fix degree test and add comment --- zkevm-circuits/src/state_circuit/test.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 75bdd05550..725135c695 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -110,6 +110,8 @@ fn verifying_key_independent_of_rw_length() { }), ); + // halo2::plonk::VerifyingKey doesn't derive Eq, so we check for equality using + // its debug string. assert_eq!( format!("{:?}", keygen_vk(¶ms, &no_rows).unwrap()), format!("{:?}", keygen_vk(¶ms, &one_row).unwrap()) From 54840062373fbbb132b2e47462a0cf8773b1d40d Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 8 Jun 2022 07:24:18 -0400 Subject: [PATCH 35/51] Add rw_counter to Start for padding --- zkevm-circuits/src/evm_circuit/witness.rs | 24 +++++++------ zkevm-circuits/src/state_circuit.rs | 23 +++++------- .../src/state_circuit/constraint_builder.rs | 5 ++- zkevm-circuits/src/state_circuit/test.rs | 36 +++++++++---------- 4 files changed, 44 insertions(+), 44 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index 83b347aaf5..463f2f3841 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -431,7 +431,9 @@ impl RwMap { #[derive(Clone, Copy, Debug)] pub enum Rw { - Start, + Start { + rw_counter: usize, + }, TxAccessListAccount { rw_counter: usize, is_write: bool, @@ -678,8 +680,8 @@ impl Rw { pub fn rw_counter(&self) -> usize { match self { - Self::Start => 0, - Self::Memory { rw_counter, .. } + Self::Start { rw_counter } + | Self::Memory { rw_counter, .. } | Self::Stack { rw_counter, .. } | Self::AccountStorage { rw_counter, .. } | Self::TxAccessListAccount { rw_counter, .. } @@ -696,7 +698,7 @@ impl Rw { pub fn is_write(&self) -> bool { match self { - Self::Start | Self::Padding { .. } => false, + Self::Start { .. } | Self::Padding { .. } => false, Self::Memory { is_write, .. } | Self::Stack { is_write, .. } | Self::AccountStorage { is_write, .. } @@ -713,7 +715,7 @@ impl Rw { pub fn tag(&self) -> RwTableTag { match self { - Self::Start => RwTableTag::Start, + Self::Start { .. } => RwTableTag::Start, Self::Memory { .. } => RwTableTag::Memory, Self::Stack { .. } => RwTableTag::Stack, Self::AccountStorage { .. } => RwTableTag::AccountStorage, @@ -740,7 +742,7 @@ impl Rw { Self::CallContext { call_id, .. } | Self::Stack { call_id, .. } | Self::Memory { call_id, .. } => Some(*call_id), - Self::Start + Self::Start { .. } | Self::Account { .. } | Self::AccountDestructed { .. } | Self::Padding { .. } => None, @@ -771,7 +773,7 @@ impl Rw { Self::TxLog { log_id, index, .. } => { Some((U256::from(*index as u64) + (U256::from(*log_id) << 8)).to_address()) } - Self::Start + Self::Start { .. } | Self::CallContext { .. } | Self::TxRefund { .. } | Self::TxReceipt { .. } @@ -785,7 +787,7 @@ impl Rw { Self::CallContext { field_tag, .. } => Some(*field_tag as u64), Self::TxLog { field_tag, .. } => Some(*field_tag as u64), Self::TxReceipt { field_tag, .. } => Some(*field_tag as u64), - Self::Start + Self::Start { .. } | Self::Memory { .. } | Self::Stack { .. } | Self::AccountStorage { .. } @@ -801,7 +803,7 @@ impl Rw { match self { Self::AccountStorage { storage_key, .. } | Self::TxAccessListAccountStorage { storage_key, .. } => Some(*storage_key), - Self::Start + Self::Start { .. } | Self::CallContext { .. } | Self::Stack { .. } | Self::Memory { .. } @@ -817,7 +819,7 @@ impl Rw { pub fn value_assignment(&self, randomness: F) -> F { match self { - Self::Start | Self::Padding { .. } => F::zero(), + Self::Start { .. } | Self::Padding { .. } => F::zero(), Self::CallContext { field_tag, value, .. } => { @@ -872,7 +874,7 @@ impl Rw { is_destructed_prev, .. } => Some(F::from(*is_destructed_prev as u64)), Self::TxRefund { value_prev, .. } => Some(F::from(*value_prev)), - Self::Start + Self::Start { .. } | Self::Stack { .. } | Self::Memory { .. } | Self::CallContext { .. } diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index dc9c1c2757..4ab8163677 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -96,7 +96,7 @@ impl StateCircuit { /// powers of randomness for instance columns pub fn instance(&self) -> Vec> { (1..32) - .map(|exp| vec![self.randomness.pow(&[exp, 0, 0, 0]); self.rows.len() + 1]) + .map(|exp| vec![self.randomness.pow(&[exp, 0, 0, 0]); N_ROWS]) .collect() } } @@ -202,19 +202,13 @@ impl Circuit for StateCircuit { layouter.assign_region( || "rw table", |mut region| { - let padding_rw_counter_start = 1 + self - .rows - .iter() - .map(Rw::rw_counter) - .max() - .unwrap_or_default(); - let padding = (self.rows.len()..N_ROWS).map(|i| Rw::Padding { - rw_counter: i + padding_rw_counter_start, + let padding_length = N_ROWS - self.rows.len(); + let padding = (0..padding_length).map(|i| Rw::Start { + rw_counter: u32::MAX as usize + i - padding_length + 1, }); + dbg!(padding.len() + self.rows.len()); - let rows = once(Rw::Start) - .chain(self.rows.iter().cloned()) - .chain(padding); + let rows = padding.chain(self.rows.iter().cloned()); let prev_rows = once(None).chain(rows.clone().map(Some)); for (offset, (row, prev_row)) in rows.zip(prev_rows).enumerate() { @@ -281,9 +275,10 @@ impl Circuit for StateCircuit { } #[cfg(test)] - for ((column, offset), &f) in &self.overrides { + for ((column, row_offset), &f) in &self.overrides { let advice_column = column.value(&config); - region.assign_advice(|| "override", advice_column, *offset, || Ok(f))?; + let offset = *row_offset + padding_length; + region.assign_advice(|| "override", advice_column, offset, || Ok(f))?; } Ok(()) diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 063479164a..f842fc7da9 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -104,7 +104,10 @@ impl ConstraintBuilder { } fn build_start_constraints(&mut self, q: &Queries) { - self.require_zero("rw_counter is 0 for Start", q.rw_counter.value.clone()); + self.require_zero("field_tag is 0 for Stack", q.field_tag()); + self.require_zero("address is 0 for Stack", q.address.value.clone()); + self.require_zero("id is 0 for Stack", q.id()); + self.require_zero("storage_key is 0 for Stack", q.storage_key.encoded.clone()); } fn build_memory_constraints(&mut self, q: &Queries) { diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 725135c695..134c045114 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -1,4 +1,4 @@ -use super::{StateCircuit, StateConfig}; +use super::{StateCircuit, StateConfig, N_ROWS}; use crate::evm_circuit::{ table::{AccountFieldTag, CallContextFieldTag, RwTableTag}, witness::{Rw, RwMap}, @@ -333,7 +333,7 @@ fn address_limb_mismatch() { value: U256::zero(), value_prev: U256::zero(), }]; - let overrides = HashMap::from([((AdviceColumn::Address, 1), Fr::from(10))]); + let overrides = HashMap::from([((AdviceColumn::Address, 0), Fr::from(10))]); let result = verify_with_overrides(rows, overrides); @@ -351,8 +351,8 @@ fn address_limb_out_of_range() { value_prev: U256::zero(), }]; let overrides = HashMap::from([ - ((AdviceColumn::AddressLimb0, 1), Fr::from(1 << 16)), - ((AdviceColumn::AddressLimb1, 1), Fr::zero()), + ((AdviceColumn::AddressLimb0, 0), Fr::from(1 << 16)), + ((AdviceColumn::AddressLimb1, 0), Fr::zero()), ]); let result = verify_with_overrides(rows, overrides); @@ -373,9 +373,9 @@ fn storage_key_mismatch() { committed_value: U256::from(5), }]; let overrides = HashMap::from([ - ((AdviceColumn::StorageKey, 1), Fr::from(10)), + ((AdviceColumn::StorageKey, 0), Fr::from(10)), ( - (AdviceColumn::StorageKeyChangeInverse, 1), + (AdviceColumn::StorageKeyChangeInverse, 0), Fr::from(10).invert().unwrap(), ), ]); @@ -398,11 +398,11 @@ fn storage_key_byte_out_of_range() { committed_value: U256::from(5), }]; let overrides = HashMap::from([ - ((AdviceColumn::StorageKey, 1), Fr::from(256)), - ((AdviceColumn::StorageKeyByte0, 1), Fr::from(256)), - ((AdviceColumn::StorageKeyByte1, 1), Fr::zero()), + ((AdviceColumn::StorageKey, 0), Fr::from(256)), + ((AdviceColumn::StorageKeyByte0, 0), Fr::from(256)), + ((AdviceColumn::StorageKeyByte1, 0), Fr::zero()), ( - (AdviceColumn::StorageKeyChangeInverse, 1), + (AdviceColumn::StorageKeyChangeInverse, 0), Fr::from(256).invert().unwrap(), ), ]); @@ -421,7 +421,7 @@ fn is_write_nonbinary() { field_tag: CallContextFieldTag::TxId, value: U256::one(), }]; - let overrides = HashMap::from([((AdviceColumn::IsWrite, 1), Fr::from(4))]); + let overrides = HashMap::from([((AdviceColumn::IsWrite, 0), Fr::from(4))]); let result = verify_with_overrides(rows, overrides); @@ -635,8 +635,7 @@ fn read_inconsistency() { #[test] fn invalid_start_rw_counter() { - // Start row is included automatically. - let rows = vec![]; + let rows = vec![Rw::Start {rw_counter: 10}]; let overrides = HashMap::from([ ((AdviceColumn::RwCounter, 0), Fr::from(2)), ((AdviceColumn::RwCounterLimb0, 0), Fr::from(2)), @@ -682,7 +681,7 @@ fn invalid_memory_value() { memory_address: 10, byte: 0, }]; - let overrides = HashMap::from([((AdviceColumn::Value, 1), Fr::from(256))]); + let overrides = HashMap::from([((AdviceColumn::Value, 0), Fr::from(256))]); let result = verify_with_overrides(rows, overrides); @@ -776,8 +775,9 @@ fn prover(rows: Vec, overrides: HashMap<(AdviceColumn, usize), Fr>) -> MockP } fn verify(rows: Vec) -> Result<(), Vec> { - let n_rows = rows.len(); - prover(rows, HashMap::new()).verify_at_rows(0..n_rows + 1, 0..n_rows + 1) + let used_rows = rows.len(); + prover(rows, HashMap::new()) + .verify_at_rows(N_ROWS - used_rows..N_ROWS, N_ROWS - used_rows..N_ROWS) } fn verify_with_overrides( @@ -787,8 +787,8 @@ fn verify_with_overrides( // Sanity check that the original RwTable without overrides is valid. assert_eq!(verify(rows.clone()), Ok(())); - let n_rows = rows.len(); - prover(rows, overrides).verify_at_rows(0..n_rows + 1, 0..n_rows + 1) + let used_rows = rows.len(); + prover(rows, overrides).verify_at_rows(N_ROWS - used_rows..N_ROWS, N_ROWS - used_rows..N_ROWS) } fn assert_error_matches(result: Result<(), Vec>, name: &str) { From 78a89eec5e5339d9c3ac771017d349d863862475 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 8 Jun 2022 13:22:42 -0400 Subject: [PATCH 36/51] Ignore start test for now --- zkevm-circuits/src/state_circuit/test.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 134c045114..fc773205f8 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -634,6 +634,7 @@ fn read_inconsistency() { } #[test] +#[ignore = "fix and re-enable once BinaryNumberChip is used for LexicographicOrderingChip"] fn invalid_start_rw_counter() { let rows = vec![Rw::Start {rw_counter: 10}]; let overrides = HashMap::from([ From 8567f733c8ce4989ec80c1669e3f56edc29ca25b Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 8 Jun 2022 13:25:11 -0400 Subject: [PATCH 37/51] Remove Rw::Padding --- zkevm-circuits/src/evm_circuit/table.rs | 1 - zkevm-circuits/src/evm_circuit/witness.rs | 28 +++++++---------------- zkevm-circuits/src/state_circuit/test.rs | 2 +- 3 files changed, 9 insertions(+), 22 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index f5e6e88e93..cc94351f49 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -156,7 +156,6 @@ pub enum RwTableTag { CallContext, TxLog, TxReceipt, - Padding, } impl RwTableTag { diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index 463f2f3841..bf08949272 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -526,9 +526,6 @@ pub enum Rw { field_tag: TxReceiptFieldTag, value: u64, }, - Padding { - rw_counter: usize, - }, } #[derive(Default, Clone, Copy)] pub struct RwRow { @@ -691,14 +688,13 @@ impl Rw { | Self::AccountDestructed { rw_counter, .. } | Self::CallContext { rw_counter, .. } | Self::TxLog { rw_counter, .. } - | Self::TxReceipt { rw_counter, .. } - | Self::Padding { rw_counter } => *rw_counter, + | Self::TxReceipt { rw_counter, .. } => *rw_counter, } } pub fn is_write(&self) -> bool { match self { - Self::Start { .. } | Self::Padding { .. } => false, + Self::Start { .. } => false, Self::Memory { is_write, .. } | Self::Stack { is_write, .. } | Self::AccountStorage { is_write, .. } @@ -727,7 +723,6 @@ impl Rw { Self::CallContext { .. } => RwTableTag::CallContext, Self::TxLog { .. } => RwTableTag::TxLog, Self::TxReceipt { .. } => RwTableTag::TxReceipt, - Self::Padding { .. } => RwTableTag::Padding, } } @@ -742,10 +737,7 @@ impl Rw { Self::CallContext { call_id, .. } | Self::Stack { call_id, .. } | Self::Memory { call_id, .. } => Some(*call_id), - Self::Start { .. } - | Self::Account { .. } - | Self::AccountDestructed { .. } - | Self::Padding { .. } => None, + Self::Start { .. } | Self::Account { .. } | Self::AccountDestructed { .. } => None, } } @@ -776,8 +768,7 @@ impl Rw { Self::Start { .. } | Self::CallContext { .. } | Self::TxRefund { .. } - | Self::TxReceipt { .. } - | Self::Padding { .. } => None, + | Self::TxReceipt { .. } => None, } } @@ -794,8 +785,7 @@ impl Rw { | Self::TxAccessListAccount { .. } | Self::TxAccessListAccountStorage { .. } | Self::TxRefund { .. } - | Self::AccountDestructed { .. } - | Self::Padding { .. } => None, + | Self::AccountDestructed { .. } => None, } } @@ -812,14 +802,13 @@ impl Rw { | Self::TxAccessListAccount { .. } | Self::AccountDestructed { .. } | Self::TxLog { .. } - | Self::TxReceipt { .. } - | Self::Padding { .. } => None, + | Self::TxReceipt { .. } => None, } } pub fn value_assignment(&self, randomness: F) -> F { match self { - Self::Start { .. } | Self::Padding { .. } => F::zero(), + Self::Start { .. } => F::zero(), Self::CallContext { field_tag, value, .. } => { @@ -879,8 +868,7 @@ impl Rw { | Self::Memory { .. } | Self::CallContext { .. } | Self::TxLog { .. } - | Self::TxReceipt { .. } - | Self::Padding { .. } => None, + | Self::TxReceipt { .. } => None, } } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index fc773205f8..631038ffa3 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -636,7 +636,7 @@ fn read_inconsistency() { #[test] #[ignore = "fix and re-enable once BinaryNumberChip is used for LexicographicOrderingChip"] fn invalid_start_rw_counter() { - let rows = vec![Rw::Start {rw_counter: 10}]; + let rows = vec![Rw::Start { rw_counter: 10 }]; let overrides = HashMap::from([ ((AdviceColumn::RwCounter, 0), Fr::from(2)), ((AdviceColumn::RwCounterLimb0, 0), Fr::from(2)), From 656b673f105d58a1bde002d459bbcf4d3094da57 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 8 Jun 2022 13:36:30 -0400 Subject: [PATCH 38/51] Fix test and cleanup --- zkevm-circuits/src/state_circuit.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 4ab8163677..78dec44d67 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -206,7 +206,6 @@ impl Circuit for StateCircuit { let padding = (0..padding_length).map(|i| Rw::Start { rw_counter: u32::MAX as usize + i - padding_length + 1, }); - dbg!(padding.len() + self.rows.len()); let rows = padding.chain(self.rows.iter().cloned()); let prev_rows = once(None).chain(rows.clone().map(Some)); From 5afbdda7411294b24f4ff70ca2a6dd1ce7dd44fd Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 13 Jun 2022 22:49:25 -0400 Subject: [PATCH 39/51] Add rw_counter constraint for Rw::Start and comment --- zkevm-circuits/src/state_circuit.rs | 4 ++++ zkevm-circuits/src/state_circuit/constraint_builder.rs | 9 +++++++++ 2 files changed, 13 insertions(+) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 78dec44d67..a46c45baed 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -35,7 +35,9 @@ use random_linear_combination::{Chip as RlcChip, Config as RlcConfig, Queries as use std::collections::HashMap; use std::iter::once; +// TODO: use a better value for production. const N_ROWS: usize = 1 << 16; + const N_LIMBS_RW_COUNTER: usize = 2; const N_LIMBS_ACCOUNT_ADDRESS: usize = 10; const N_LIMBS_ID: usize = 2; @@ -289,6 +291,8 @@ impl Circuit for StateCircuit { fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { Queries { selector: meta.query_fixed(c.selector, Rotation::cur()), + lexicographic_ordering_selector: meta + .query_fixed(c.lexicographic_ordering.selector, Rotation::cur()), rw_counter: MpiQueries::new(meta, c.rw_counter), is_write: meta.query_advice(c.is_write, Rotation::cur()), tag: c.tag.value(Rotation::cur())(meta), diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index f842fc7da9..f165a1d033 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -17,6 +17,7 @@ use strum::IntoEnumIterator; #[derive(Clone)] pub struct Queries { pub selector: Expression, + pub lexicographic_ordering_selector: Expression, pub rw_counter: MpiQueries, pub is_write: Expression, pub tag: Expression, @@ -108,6 +109,10 @@ impl ConstraintBuilder { self.require_zero("address is 0 for Stack", q.address.value.clone()); self.require_zero("id is 0 for Stack", q.id()); self.require_zero("storage_key is 0 for Stack", q.storage_key.encoded.clone()); + self.require_zero( + "rw_counter increases by 1 for every non-first row", + q.lexicographic_ordering_selector.clone() * (q.rw_counter_change() - 1.expr()), + ); } fn build_memory_constraints(&mut self, q: &Queries) { @@ -311,6 +316,10 @@ impl Queries { fn address_change(&self) -> Expression { self.address.value.clone() - self.address.value_prev.clone() } + + fn rw_counter_change(&self) -> Expression { + self.rw_counter.value.clone() - self.rw_counter.value_prev.clone() + } } fn from_digits(digits: &[Expression], base: Expression) -> Expression { From 3a33e74275bb2c63ffc999c17cbb3aeb7012046e Mon Sep 17 00:00:00 2001 From: z2trillion Date: Mon, 13 Jun 2022 22:52:26 -0400 Subject: [PATCH 40/51] Allow overrides in padding --- zkevm-circuits/src/state_circuit.rs | 4 ++-- zkevm-circuits/src/state_circuit/test.rs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index a46c45baed..2a1abadb50 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -70,7 +70,7 @@ pub struct StateCircuit { pub(crate) randomness: F, pub(crate) rows: Vec, #[cfg(test)] - overrides: HashMap<(test::AdviceColumn, usize), F>, + overrides: HashMap<(test::AdviceColumn, isize), F>, } impl StateCircuit { @@ -278,7 +278,7 @@ impl Circuit for StateCircuit { #[cfg(test)] for ((column, row_offset), &f) in &self.overrides { let advice_column = column.value(&config); - let offset = *row_offset + padding_length; + let offset = padding_length + usize::try_from(*row_offset).unwrap(); region.assign_advice(|| "override", advice_column, offset, || Ok(f))?; } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 631038ffa3..2e53f2cafb 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -763,7 +763,7 @@ fn invalid_tags() { } } -fn prover(rows: Vec, overrides: HashMap<(AdviceColumn, usize), Fr>) -> MockProver { +fn prover(rows: Vec, overrides: HashMap<(AdviceColumn, isize), Fr>) -> MockProver { let randomness = Fr::rand(); let circuit = StateCircuit { randomness, @@ -783,7 +783,7 @@ fn verify(rows: Vec) -> Result<(), Vec> { fn verify_with_overrides( rows: Vec, - overrides: HashMap<(AdviceColumn, usize), Fr>, + overrides: HashMap<(AdviceColumn, isize), Fr>, ) -> Result<(), Vec> { // Sanity check that the original RwTable without overrides is valid. assert_eq!(verify(rows.clone()), Ok(())); From 04a18789fc7e4bc8b0e35c8f4a7e775d2f21634f Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 14 Jun 2022 00:08:38 -0400 Subject: [PATCH 41/51] Update tests --- zkevm-circuits/src/state_circuit.rs | 9 ++++++- zkevm-circuits/src/state_circuit/test.rs | 33 ++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 1 deletion(-) diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 2a1abadb50..a7f89aa521 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -205,10 +205,14 @@ impl Circuit for StateCircuit { || "rw table", |mut region| { let padding_length = N_ROWS - self.rows.len(); + dbg!(N_ROWS); + dbg!(padding_length); let padding = (0..padding_length).map(|i| Rw::Start { rw_counter: u32::MAX as usize + i - padding_length + 1, }); + // dbg!(u32::MAX as usize - padding_length + 1) + let rows = padding.chain(self.rows.iter().cloned()); let prev_rows = once(None).chain(rows.clone().map(Some)); @@ -278,7 +282,10 @@ impl Circuit for StateCircuit { #[cfg(test)] for ((column, row_offset), &f) in &self.overrides { let advice_column = column.value(&config); - let offset = padding_length + usize::try_from(*row_offset).unwrap(); + let offset = + usize::try_from(isize::try_from(padding_length).unwrap() + *row_offset) + .unwrap(); + dbg!(offset); region.assign_advice(|| "override", advice_column, offset, || Ok(f))?; } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 2e53f2cafb..2c6b6d50a1 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -39,6 +39,7 @@ pub enum AdviceColumn { TagBit1, TagBit2, TagBit3, + RwCounterLimb1, } impl AdviceColumn { @@ -59,6 +60,7 @@ impl AdviceColumn { Self::TagBit1 => config.tag.bits[1], Self::TagBit2 => config.tag.bits[2], Self::TagBit3 => config.tag.bits[3], + Self::RwCounterLimb1 => config.rw_counter.limbs[1], } } } @@ -647,6 +649,37 @@ fn invalid_start_rw_counter() { assert_error_matches(result, "rw_counter is 0 for Start"); } +#[test] +fn all_padding() { + assert_eq!( + prover(vec![], HashMap::new()).verify_at_rows(0..100, 0..100), + Ok(()) + ); +} + +#[test] +fn skipped_start_rw_counter() { + let rows = vec![]; + + let first_padding_row_offset = -isize::try_from(N_ROWS).unwrap(); + let overrides = HashMap::from([ + ( + (AdviceColumn::RwCounter, first_padding_row_offset), + // The correct assignment is (1 << 32) - (1 << 16). Choosing this new value for the + // rw_counter allows us to not have to override assigments in the lexicographic + // ordering chip. + Fr::from((1 << 32) - (1 << 17)), + ), + ( + (AdviceColumn::RwCounterLimb1, first_padding_row_offset), + Fr::from((1 << 16) - 2), + ), + ]); + + let result = prover(rows, overrides).verify_at_rows(0..10, 0..10); + assert_error_matches(result, "rw_counter increases by 1 for every non-first row"); +} + #[test] fn invalid_memory_address() { let rows = vec![Rw::Memory { From b61f20d19cca31b662a3f8bfd8d7f50be2629a8d Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 12:46:11 -0400 Subject: [PATCH 42/51] Make state circuit generic over N_ROWS and fix constraint names --- prover/src/compute_proof.rs | 3 ++- zkevm-circuits/src/state_circuit.rs | 9 +++------ .../src/state_circuit/constraint_builder.rs | 8 ++++---- zkevm-circuits/src/state_circuit/test.rs | 14 ++++++++------ zkevm-circuits/src/test_util.rs | 3 ++- 5 files changed, 19 insertions(+), 18 deletions(-) diff --git a/prover/src/compute_proof.rs b/prover/src/compute_proof.rs index 3fed746ed8..f2b3124e1a 100644 --- a/prover/src/compute_proof.rs +++ b/prover/src/compute_proof.rs @@ -61,7 +61,8 @@ pub async fn compute_proof( { // generate state_circuit proof - let circuit = StateCircuit::new(block.randomness, block.rws); + const N_ROWS: usize = 1 << 16; + let circuit = StateCircuit::::new(block.randomness, block.rws); // TODO: same quest like in the first scope let vk = keygen_vk(params, &circuit)?; diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index a7f89aa521..4abc29accf 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -35,9 +35,6 @@ use random_linear_combination::{Chip as RlcChip, Config as RlcConfig, Queries as use std::collections::HashMap; use std::iter::once; -// TODO: use a better value for production. -const N_ROWS: usize = 1 << 16; - const N_LIMBS_RW_COUNTER: usize = 2; const N_LIMBS_ACCOUNT_ADDRESS: usize = 10; const N_LIMBS_ID: usize = 2; @@ -66,14 +63,14 @@ type Lookup = (&'static str, Expression, Expression); /// State Circuit for proving RwTable is valid #[derive(Default)] -pub struct StateCircuit { +pub struct StateCircuit { pub(crate) randomness: F, pub(crate) rows: Vec, #[cfg(test)] overrides: HashMap<(test::AdviceColumn, isize), F>, } -impl StateCircuit { +impl StateCircuit { /// make a new state circuit from an RwMap pub fn new(randomness: F, rw_map: RwMap) -> Self { let mut rows: Vec<_> = rw_map.0.into_values().flatten().collect(); @@ -103,7 +100,7 @@ impl StateCircuit { } } -impl Circuit for StateCircuit { +impl Circuit for StateCircuit { type Config = StateConfig; type FloorPlanner = SimpleFloorPlanner; diff --git a/zkevm-circuits/src/state_circuit/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index f165a1d033..0945576354 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -105,10 +105,10 @@ impl ConstraintBuilder { } fn build_start_constraints(&mut self, q: &Queries) { - self.require_zero("field_tag is 0 for Stack", q.field_tag()); - self.require_zero("address is 0 for Stack", q.address.value.clone()); - self.require_zero("id is 0 for Stack", q.id()); - self.require_zero("storage_key is 0 for Stack", q.storage_key.encoded.clone()); + self.require_zero("field_tag is 0 for Start", q.field_tag()); + self.require_zero("address is 0 for Start", q.address.value.clone()); + self.require_zero("id is 0 for Start", q.id()); + self.require_zero("storage_key is 0 for Start", q.storage_key.encoded.clone()); self.require_zero( "rw_counter increases by 1 for every non-first row", q.lexicographic_ordering_selector.clone() * (q.rw_counter_change() - 1.expr()), diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 2c6b6d50a1..0049006b44 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -1,4 +1,4 @@ -use super::{StateCircuit, StateConfig, N_ROWS}; +use super::{StateCircuit, StateConfig}; use crate::evm_circuit::{ table::{AccountFieldTag, CallContextFieldTag, RwTableTag}, witness::{Rw, RwMap}, @@ -22,6 +22,8 @@ use halo2_proofs::{ use std::collections::{BTreeSet, HashMap}; use strum::IntoEnumIterator; +const N_ROWS: usize = 1 << 16; + #[derive(Hash, Eq, PartialEq)] pub enum AdviceColumn { IsWrite, @@ -78,7 +80,7 @@ fn test_state_circuit_ok( }); let randomness = Fr::rand(); - let circuit = StateCircuit::new(randomness, rw_map); + let circuit = StateCircuit::::new(randomness, rw_map); let power_of_randomness = circuit.instance(); let prover = MockProver::::run(19, &circuit, power_of_randomness).unwrap(); @@ -89,7 +91,7 @@ fn test_state_circuit_ok( #[test] fn degree() { let mut meta = ConstraintSystem::::default(); - StateCircuit::configure(&mut meta); + StateCircuit::::configure(&mut meta); assert_eq!(meta.degree(), 16); } @@ -99,8 +101,8 @@ fn verifying_key_independent_of_rw_length() { let degree = 17; let params = Params::::unsafe_setup::(degree); - let no_rows = StateCircuit::new(randomness, RwMap::default()); - let one_row = StateCircuit::new( + let no_rows = StateCircuit::::new(randomness, RwMap::default()); + let one_row = StateCircuit::::new( randomness, RwMap::from(&OperationContainer { memory: vec![Operation::new( @@ -798,7 +800,7 @@ fn invalid_tags() { fn prover(rows: Vec, overrides: HashMap<(AdviceColumn, isize), Fr>) -> MockProver { let randomness = Fr::rand(); - let circuit = StateCircuit { + let circuit = StateCircuit:: { randomness, rows, overrides, diff --git a/zkevm-circuits/src/test_util.rs b/zkevm-circuits/src/test_util.rs index 421ff7dfcb..86182447b0 100644 --- a/zkevm-circuits/src/test_util.rs +++ b/zkevm-circuits/src/test_util.rs @@ -90,7 +90,8 @@ pub fn test_circuits_using_witness_block( // TODO: use randomness as one of the circuit public input, since randomness in // state circuit and evm circuit must be same if config.enable_state_circuit_test { - let state_circuit = StateCircuit::new(block.randomness, block.rws); + const N_ROWS: usize = 1 << 16; + let state_circuit = StateCircuit::::new(block.randomness, block.rws); let power_of_randomness = state_circuit.instance(); let prover = MockProver::::run(18, &state_circuit, power_of_randomness).unwrap(); prover.verify_at_rows(0..state_circuit.rows.len(), 0..state_circuit.rows.len())? From 0a0a35e5827ba379e8007d619bd291fbc220520b Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 17 Jun 2022 13:54:30 -0400 Subject: [PATCH 43/51] Fix tests and build --- circuit-benchmarks/src/state_circuit.rs | 2 +- integration-tests/tests/circuits.rs | 2 +- zkevm-circuits/src/state_circuit.rs | 9 +----- zkevm-circuits/src/state_circuit/test.rs | 40 +++++++++++------------- 4 files changed, 21 insertions(+), 32 deletions(-) diff --git a/circuit-benchmarks/src/state_circuit.rs b/circuit-benchmarks/src/state_circuit.rs index 4535b0ca94..7a305c1b38 100644 --- a/circuit-benchmarks/src/state_circuit.rs +++ b/circuit-benchmarks/src/state_circuit.rs @@ -17,7 +17,7 @@ mod tests { #[cfg_attr(not(feature = "benches"), ignore)] #[test] fn bench_state_circuit_prover() { - let empty_circuit = StateCircuit::::default(); + let empty_circuit = StateCircuit::::default(); // Initialize the polynomial commitment parameters let rng = XorShiftRng::from_seed([ diff --git a/integration-tests/tests/circuits.rs b/integration-tests/tests/circuits.rs index 81a9dd5c62..e7aeabf962 100644 --- a/integration-tests/tests/circuits.rs +++ b/integration-tests/tests/circuits.rs @@ -53,7 +53,7 @@ async fn test_state_circuit_block(block_num: u64) { }); let randomness = Fr::rand(); - let circuit = StateCircuit::::new(randomness, rw_map); + let circuit = StateCircuit::::new(randomness, rw_map); let power_of_randomness = circuit.instance(); use halo2_proofs::pairing::bn256::Fr as Fp; diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 4abc29accf..b09b86cce5 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -202,13 +202,7 @@ impl Circuit for StateCircuit { || "rw table", |mut region| { let padding_length = N_ROWS - self.rows.len(); - dbg!(N_ROWS); - dbg!(padding_length); - let padding = (0..padding_length).map(|i| Rw::Start { - rw_counter: u32::MAX as usize + i - padding_length + 1, - }); - - // dbg!(u32::MAX as usize - padding_length + 1) + let padding = (1..=padding_length).map(|rw_counter| Rw::Start { rw_counter }); let rows = padding.chain(self.rows.iter().cloned()); let prev_rows = once(None).chain(rows.clone().map(Some)); @@ -282,7 +276,6 @@ impl Circuit for StateCircuit { let offset = usize::try_from(isize::try_from(padding_length).unwrap() + *row_offset) .unwrap(); - dbg!(offset); region.assign_advice(|| "override", advice_column, offset, || Ok(f))?; } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 0049006b44..fd6c52ed85 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -37,11 +37,11 @@ pub enum AdviceColumn { Value, RwCounter, RwCounterLimb0, + RwCounterLimb1, TagBit0, TagBit1, TagBit2, TagBit3, - RwCounterLimb1, } impl AdviceColumn { @@ -58,11 +58,11 @@ impl AdviceColumn { Self::Value => config.value, Self::RwCounter => config.rw_counter.value, Self::RwCounterLimb0 => config.rw_counter.limbs[0], + Self::RwCounterLimb1 => config.rw_counter.limbs[1], Self::TagBit0 => config.tag.bits[0], Self::TagBit1 => config.tag.bits[1], Self::TagBit2 => config.tag.bits[2], Self::TagBit3 => config.tag.bits[3], - Self::RwCounterLimb1 => config.rw_counter.limbs[1], } } } @@ -661,24 +661,16 @@ fn all_padding() { #[test] fn skipped_start_rw_counter() { - let rows = vec![]; - - let first_padding_row_offset = -isize::try_from(N_ROWS).unwrap(); let overrides = HashMap::from([ ( - (AdviceColumn::RwCounter, first_padding_row_offset), - // The correct assignment is (1 << 32) - (1 << 16). Choosing this new value for the - // rw_counter allows us to not have to override assigments in the lexicographic - // ordering chip. - Fr::from((1 << 32) - (1 << 17)), - ), - ( - (AdviceColumn::RwCounterLimb1, first_padding_row_offset), - Fr::from((1 << 16) - 2), + (AdviceColumn::RwCounter, -1), + // The original assignment is 1 << 16. + Fr::from((1 << 16) + 1), ), + ((AdviceColumn::RwCounterLimb0, -1), Fr::one()), ]); - let result = prover(rows, overrides).verify_at_rows(0..10, 0..10); + let result = prover(vec![], overrides).verify_at_rows(N_ROWS - 1..N_ROWS, N_ROWS - 1..N_ROWS); assert_error_matches(result, "rw_counter increases by 1 for every non-first row"); } @@ -777,6 +769,7 @@ fn invalid_stack_address_change() { #[test] fn invalid_tags() { + let first_row_offset = -isize::try_from(N_ROWS).unwrap(); let tags: BTreeSet = RwTableTag::iter().map(|x| x as usize).collect(); for i in 0..16 { if tags.contains(&i) { @@ -786,13 +779,13 @@ fn invalid_tags() { .as_bits() .map(|bit| if bit { Fr::one() } else { Fr::zero() }); let overrides = HashMap::from([ - ((AdviceColumn::TagBit0, 0), bits[0]), - ((AdviceColumn::TagBit1, 0), bits[1]), - ((AdviceColumn::TagBit2, 0), bits[2]), - ((AdviceColumn::TagBit3, 0), bits[3]), + ((AdviceColumn::TagBit0, first_row_offset), bits[0]), + ((AdviceColumn::TagBit1, first_row_offset), bits[1]), + ((AdviceColumn::TagBit2, first_row_offset), bits[2]), + ((AdviceColumn::TagBit3, first_row_offset), bits[3]), ]); - let result = verify_with_overrides(vec![], overrides); + let result = prover(vec![], overrides).verify_at_rows(0..1, 0..1); assert_error_matches(result, "binary number value in range"); } @@ -823,8 +816,11 @@ fn verify_with_overrides( // Sanity check that the original RwTable without overrides is valid. assert_eq!(verify(rows.clone()), Ok(())); - let used_rows = rows.len(); - prover(rows, overrides).verify_at_rows(N_ROWS - used_rows..N_ROWS, N_ROWS - used_rows..N_ROWS) + let n_active_rows = rows.len(); + prover(rows, overrides).verify_at_rows( + N_ROWS - n_active_rows..N_ROWS, + N_ROWS - n_active_rows..N_ROWS, + ) } fn assert_error_matches(result: Result<(), Vec>, name: &str) { From a21884e599300169988d9a91ada7446a4bc7fb77 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 21 Jun 2022 12:53:31 -0400 Subject: [PATCH 44/51] Update comments --- .../src/state_circuit/lexicographic_ordering.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 55ebe46b91..1506c977ba 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -39,8 +39,8 @@ use strum_macros::EnumIter; // 1. limb_difference fits into 16 bits. // 2. limb_difference is not zero because its inverse exists. -// 3. limbs before first_different_limb are equal. -// 4. limb_difference equals the difference of the limbs at +// 3. RLC of the pairwise limb differences before the first_different_limb is +// 0. 4. limb_difference equals the difference of the limbs at // first_different_limb. #[derive(Clone, Copy, Debug, EnumIter)] @@ -154,13 +154,16 @@ impl Config { }); meta.create_gate( - "limb_difference is equal to the difference at claimed limb", + "limb differences before first_different_limb are all 0", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); let cur = Queries::new(meta, keys, Rotation::cur()); let prev = Queries::new(meta, keys, Rotation::prev()); let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); + // E.g. if first_different_limb = 5, four limb differences before need to be 0. + // Using RLC, we check that (cur_1 - prev_1) + r(cur_2 - prev_2) + r^2(cur_3 - + // prev_3) + r^3(cur_4 - prev_4) = 0. let mut constraints = vec![]; for ((i, cur_limb), prev_limb) in LimbIndex::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) From 7da5f3f29fa79fc2b4591d026ce658321ead0bef Mon Sep 17 00:00:00 2001 From: z2trillion Date: Tue, 21 Jun 2022 19:11:09 -0400 Subject: [PATCH 45/51] fix merge --- zkevm-circuits/src/state_circuit/test.rs | 27 ------------------------ 1 file changed, 27 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index 82d2585cff..e8cff9527d 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -130,33 +130,6 @@ fn verifying_key_independent_of_rw_length() { ); } -#[test] -fn verifying_key_independent_of_rw_length() { - let randomness = Fr::rand(); - let degree = 17; - let params = Params::::unsafe_setup::(degree); - - let no_rows = StateCircuit::::new(randomness, RwMap::default()); - let one_row = StateCircuit::::new( - randomness, - RwMap::from(&OperationContainer { - memory: vec![Operation::new( - RWCounter::from(1), - RW::WRITE, - MemoryOp::new(1, MemoryAddress::from(0), 32), - )], - ..Default::default() - }), - ); - - // halo2::plonk::VerifyingKey doesn't derive Eq, so we check for equality using - // its debug string. - assert_eq!( - format!("{:?}", keygen_vk(¶ms, &no_rows).unwrap()), - format!("{:?}", keygen_vk(¶ms, &one_row).unwrap()) - ); -} - #[test] fn state_circuit_simple_2() { let memory_op_0 = Operation::new( From 47e731fbb7e86c2dcddc99d5e33fc5fb0ca7388e Mon Sep 17 00:00:00 2001 From: z2trillion Date: Wed, 22 Jun 2022 11:56:32 -0400 Subject: [PATCH 46/51] Update comment and constraint names --- .../state_circuit/lexicographic_ordering.rs | 52 +++++++++++-------- 1 file changed, 29 insertions(+), 23 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 1506c977ba..bf7010d97e 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -31,6 +31,9 @@ use strum_macros::EnumIter; // C31 = C30 << 16 + A31 - B21. // X_cur > X_prev iff one of C0, ..., C31 is non-zero and fits into 16 bits. +// C16, ..., C31 do not necessarily fit into a field element, so to check that +// Cn fits into 16 bits, we use an RLC to check that Cn-1 = 0 and then do a +// lookup for An-Bn. // We show this with following advice columns and constraints: // - first_different_limb: first index where the limbs differ. @@ -133,37 +136,40 @@ impl Config { vec![selector * (1.expr() - limb_difference * limb_difference_inverse)] }); - meta.create_gate("limbs match before first_different_limb", |meta| { - let selector = meta.query_fixed(selector, Rotation::cur()); - let cur = Queries::new(meta, keys, Rotation::cur()); - let prev = Queries::new(meta, keys, Rotation::prev()); - let powers_of_randomness = - power_of_randomness.map(|i| meta.query_instance(i, Rotation::cur())); - - let mut constraints = vec![]; - for (limb, e) in - LimbIndex::iter().zip(rlc_limb_differences(cur, prev, powers_of_randomness)) - { - constraints.push( - selector.clone() - * first_different_limb.value_equals(limb, Rotation::cur())(meta) - * e, - ) - } - constraints - }); - meta.create_gate( "limb differences before first_different_limb are all 0", + |meta| { + let selector = meta.query_fixed(selector, Rotation::cur()); + let cur = Queries::new(meta, keys, Rotation::cur()); + let prev = Queries::new(meta, keys, Rotation::prev()); + let powers_of_randomness = + power_of_randomness.map(|i| meta.query_instance(i, Rotation::cur())); + + let mut constraints = vec![]; + for (i, rlc_expression) in + LimbIndex::iter().zip(rlc_limb_differences(cur, prev, powers_of_randomness)) + { + // E.g. if first_different_limb = 5, four limb differences before need to be 0. + // Using RLC, we check that (cur_1 - prev_1) + r(cur_2 - prev_2) + r^2(cur_3 - + // prev_3) + r^3(cur_4 - prev_4) = 0. + constraints.push( + selector.clone() + * first_different_limb.value_equals(i, Rotation::cur())(meta) + * rlc_expression, + ) + } + constraints + }, + ); + + meta.create_gate( + "limb_difference equals difference of limbs at index", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); let cur = Queries::new(meta, keys, Rotation::cur()); let prev = Queries::new(meta, keys, Rotation::prev()); let limb_difference = meta.query_advice(limb_difference, Rotation::cur()); - // E.g. if first_different_limb = 5, four limb differences before need to be 0. - // Using RLC, we check that (cur_1 - prev_1) + r(cur_2 - prev_2) + r^2(cur_3 - - // prev_3) + r^3(cur_4 - prev_4) = 0. let mut constraints = vec![]; for ((i, cur_limb), prev_limb) in LimbIndex::iter().zip(cur.be_limbs()).zip(prev.be_limbs()) From d4c6156ecdf9043f3f32e7d0e57eba43af4545a4 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Thu, 23 Jun 2022 13:29:16 -0400 Subject: [PATCH 47/51] Update zkevm-circuits/src/state_circuit/lexicographic_ordering.rs Co-authored-by: Eduard S. --- zkevm-circuits/src/state_circuit/lexicographic_ordering.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index bf7010d97e..5aa6c30368 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -42,8 +42,8 @@ use strum_macros::EnumIter; // 1. limb_difference fits into 16 bits. // 2. limb_difference is not zero because its inverse exists. -// 3. RLC of the pairwise limb differences before the first_different_limb is -// 0. 4. limb_difference equals the difference of the limbs at +// 3. RLC of the pairwise limb differences before the first_different_limb is 0. +// 4. limb_difference equals the difference of the limbs at // first_different_limb. #[derive(Clone, Copy, Debug, EnumIter)] From b9484872a12560a3166af0c8a1d808b15a3e70f0 Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 24 Jun 2022 17:24:38 -0400 Subject: [PATCH 48/51] Update test to check that 5 bits is enough --- zkevm-circuits/src/state_circuit/binary_number.rs | 2 +- .../src/state_circuit/lexicographic_ordering.rs | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/binary_number.rs b/zkevm-circuits/src/state_circuit/binary_number.rs index 5dc02bb817..e471eaa6a8 100644 --- a/zkevm-circuits/src/state_circuit/binary_number.rs +++ b/zkevm-circuits/src/state_circuit/binary_number.rs @@ -169,7 +169,7 @@ where } } -fn from_bits(bits: &[bool]) -> usize { +pub fn from_bits(bits: &[bool]) -> usize { bits.iter() .fold(0, |result, &bit| bit as usize + 2 * result) } diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 5aa6c30368..23a2b87ad9 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -90,6 +90,7 @@ impl AsBits<5> for LimbIndex { bits[4 - i] = x % 2 == 1; x /= 2; } + assert_eq!(x, 0); bits } } @@ -317,11 +318,14 @@ fn rlc_limb_differences( #[cfg(test)] mod test { + use super::super::binary_number::{from_bits, AsBits}; use super::LimbIndex; use strum::IntoEnumIterator; #[test] - fn n_limbs() { - assert_eq!(LimbIndex::iter().len(), 32); + fn enough_bits_for_limb_index() { + for index in LimbIndex::iter() { + assert_eq!(from_bits(&index.as_bits()), index as usize); + } } } From 0fbda8915dc64c691717c30c1490c58893d5a94f Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 24 Jun 2022 17:24:49 -0400 Subject: [PATCH 49/51] update test for new constraint name --- zkevm-circuits/src/state_circuit/test.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index e8cff9527d..d46db53ebc 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -621,7 +621,7 @@ fn lexicographic_ordering_previous_limb_differences_nonzero() { let result = verify_with_overrides(rows, overrides); - assert_error_matches(result, "limbs match before first_different_limb"); + assert_error_matches(result, "limb differences before first_different_limb are all 0"); } #[test] From ea20e50f016e92c321f9076797f8e609323221bf Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 24 Jun 2022 17:56:12 -0400 Subject: [PATCH 50/51] Update names and fmt --- zkevm-circuits/src/state_circuit/lexicographic_ordering.rs | 6 ++++-- zkevm-circuits/src/state_circuit/test.rs | 5 ++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 23a2b87ad9..ec586b07fa 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -296,6 +296,8 @@ fn rw_to_be_limbs(row: &Rw) -> Vec { .collect() } +// Returns a vector of length 32 with the rlc of the limb differences between +// from 0 to i-l. 0 for i=0, fn rlc_limb_differences( cur: Queries, prev: Queries, @@ -304,14 +306,14 @@ fn rlc_limb_differences( let mut result = vec![]; let mut partial_sum = 0u64.expr(); let powers_of_randomness = once(1.expr()).chain(powers_of_randomness.into_iter()); - for ((cur_limb, prev_limb), powers_of_randomness) in cur + for ((cur_limb, prev_limb), power_of_randomness) in cur .be_limbs() .iter() .zip(&prev.be_limbs()) .zip(powers_of_randomness) { result.push(partial_sum.clone()); - partial_sum = partial_sum + powers_of_randomness * (cur_limb.clone() - prev_limb.clone()); + partial_sum = partial_sum + power_of_randomness * (cur_limb.clone() - prev_limb.clone()); } result } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index d46db53ebc..891d88b977 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -621,7 +621,10 @@ fn lexicographic_ordering_previous_limb_differences_nonzero() { let result = verify_with_overrides(rows, overrides); - assert_error_matches(result, "limb differences before first_different_limb are all 0"); + assert_error_matches( + result, + "limb differences before first_different_limb are all 0", + ); } #[test] From ef2c0fb571fe32a6d219fd1f668ced9e540dbdac Mon Sep 17 00:00:00 2001 From: z2trillion Date: Fri, 24 Jun 2022 18:11:00 -0400 Subject: [PATCH 51/51] Update comments --- .../src/state_circuit/lexicographic_ordering.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index ec586b07fa..7effe25727 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -36,15 +36,17 @@ use strum_macros::EnumIter; // lookup for An-Bn. // We show this with following advice columns and constraints: -// - first_different_limb: first index where the limbs differ. +// - first_different_limb: first index where the limbs differ. We use a +// BinaryNumberChip here to reduce the degree of the constraints. // - limb_difference: the difference between the limbs at first_different_limb. // - limb_difference_inverse: the inverse of limb_difference // 1. limb_difference fits into 16 bits. // 2. limb_difference is not zero because its inverse exists. -// 3. RLC of the pairwise limb differences before the first_different_limb is 0. +// 3. RLC of the pairwise limb differences before the first_different_limb is +// zero. // 4. limb_difference equals the difference of the limbs at -// first_different_limb. +// first_different_limb. #[derive(Clone, Copy, Debug, EnumIter)] pub enum LimbIndex {