diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index b09b86cce5..cfcd05c8a1 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -11,13 +11,12 @@ mod test; use crate::evm_circuit::{ param::N_BYTES_WORD, table::RwTableTag, - util::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}; -use gadgets::is_zero::{IsZeroChip, IsZeroConfig, IsZeroInstruction}; +use eth_types::{Address, Field}; use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner}, plonk::{ @@ -25,9 +24,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}; @@ -40,23 +37,27 @@ 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/privacy-scaling-explorations/zkevm-circuits/issues/407 - rw_counter: MpiConfig, + sort_keys: SortKeysConfig, is_write: Column, + value: Column, + lexicographic_ordering: LexicographicOrderingConfig, + lookups: LookupsConfig, + power_of_randomness: [Column; N_BYTES_WORD - 1], +} + +/// Keys for sorting the rows of the state circuit +#[derive(Clone, Copy)] +pub struct SortKeysConfig { 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, - power_of_randomness: [Column; N_BYTES_WORD - 1], - lexicographic_ordering: LexicographicOrderingConfig, + rw_counter: MpiConfig, } type Lookup = (&'static str, Expression, Expression); @@ -77,9 +78,9 @@ impl StateCircuit { rows.sort_by_key(|row| { ( row.tag() as u64, - row.field_tag().unwrap_or_default(), row.id().unwrap_or_default(), row.address().unwrap_or_default(), + row.field_tag().unwrap_or_default(), row.storage_key().unwrap_or_default(), row.rw_counter(), ) @@ -101,7 +102,7 @@ impl StateCircuit { } impl Circuit for StateCircuit { - type Config = StateConfig; + type Config = StateConfig; type FloorPlanner = SimpleFloorPlanner; fn without_witnesses(&self) -> Self { @@ -113,8 +114,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, is_storage_key_unchanged_column] = - [0; 5].map(|_| meta.advice_column()); + let [is_write, field_tag, value] = [0; 3].map(|_| meta.advice_column()); let tag = BinaryNumberChip::configure(meta, selector); @@ -123,49 +123,28 @@ 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 lexicographic_ordering = LexicographicOrderingChip::configure( - meta, + let sort_keys = SortKeysConfig { tag, + id, field_tag, - id.limbs, - address.limbs, - storage_key.bytes, - rw_counter.limbs, - lookups.u16, - ); + address, + storage_key, + rw_counter, + }; - 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 is_storage_key_unchanged = IsZeroChip::configure( + let lexicographic_ordering = LexicographicOrderingConfig::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, + sort_keys, + lookups.u16, + power_of_randomness, ); 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, lookups, power_of_randomness, }; @@ -190,13 +169,7 @@ 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 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.tag); + let tag_chip = BinaryNumberChip::construct(config.sort_keys.tag); layouter.assign_region( || "rw table", @@ -209,9 +182,11 @@ 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 - .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, @@ -220,21 +195,24 @@ 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, @@ -249,23 +227,11 @@ impl Circuit for StateCircuit { )?; 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); - 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( + config.lexicographic_ordering.assign( &mut region, offset, - Some(storage_key_change), + &row, + &prev_row, )?; } } @@ -285,33 +251,69 @@ impl Circuit for StateCircuit { } } -fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { +fn queries(meta: &mut VirtualCells<'_, F>, c: &StateConfig) -> Queries { + let final_bits_sum = 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()), lexicographic_ordering_selector: meta .query_fixed(c.lexicographic_ordering.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: 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), - 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), + 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], + 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(), + )) + + 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), value: meta.query_advice(c.value, Rotation::cur()), lookups: LookupsQueries::new(meta, c.lookups), 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! 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], + 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/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/constraint_builder.rs b/zkevm-circuits/src/state_circuit/constraint_builder.rs index 0945576354..79b8b8ab8f 100644 --- a/zkevm-circuits/src/state_circuit/constraint_builder.rs +++ b/zkevm-circuits/src/state_circuit/constraint_builder.rs @@ -7,7 +7,7 @@ use super::{ use crate::evm_circuit::{ param::N_BYTES_WORD, table::{AccountFieldTag, RwTableTag}, - util::{not, or}, + util::not, }; use crate::util::Expr; use eth_types::Field; @@ -23,15 +23,14 @@ 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, 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); @@ -144,9 +143,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 also Stack with unchanged call id, address change is 0 or 1", q.address_change(), ) }); @@ -304,13 +303,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 d16092ce98..7effe25727 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -1,220 +1,196 @@ use super::{ - binary_number::Config as BinaryNumberConfig, 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}, + evm_circuit::{param::N_BYTES_WORD, 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}, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Instance, VirtualCells}, poly::Rotation, }; use itertools::Itertools; -use std::ops::Mul; +use std::iter::once; +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 - -#[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, - // 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], -} +// 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. -pub struct Chip { - config: Config, +// We show this with following advice columns and constraints: +// - 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 +// zero. +// 4. limb_difference equals the difference of the limbs at +// first_different_limb. + +#[derive(Clone, Copy, Debug, EnumIter)] +pub enum LimbIndex { + Tag, + Id1, + Id0, + Address9, + Address8, + Address7, + Address6, + Address5, + Address4, + Address3, + Address2, + Address1, + Address0, + FieldTag, + StorageKey15, + StorageKey14, + StorageKey13, + StorageKey12, + StorageKey11, + StorageKey10, + StorageKey9, + StorageKey8, + StorageKey7, + StorageKey6, + StorageKey5, + StorageKey4, + StorageKey3, + StorageKey2, + StorageKey1, + StorageKey0, + RwCounter1, + RwCounter0, } -impl Chip { - pub fn construct(config: Config) -> Self { - Self { config } +impl AsBits<5> for LimbIndex { + 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; + } + assert_eq!(x, 0); + bits } +} - #[allow(clippy::too_many_arguments)] - // TODO: fix this to not have too many arguments? - pub fn configure( +#[derive(Clone, Copy)] +pub struct Config { + pub(crate) selector: Column, + pub first_different_limb: BinaryNumberConfig, + limb_difference: Column, + limb_difference_inverse: Column, +} + +impl Config { + 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 { + power_of_randomness: [Column; 31], + ) -> 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, - tag, - field_tag, - id_limbs, - address_limbs, - storage_key_bytes, - rw_counter_limbs, + first_different_limb, + limb_difference, + limb_difference_inverse, }; - meta.create_gate("upper_limb_difference is one of 15 values", |meta| { + + meta.lookup_any("limb_difference fits into u16", |meta| { + vec![( + meta.query_advice(limb_difference, Rotation::cur()), + meta.query_fixed(u16_range, Rotation::cur()), + )] + }); + + meta.create_gate("limb_difference is not zero", |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 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), - ] + 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( - "upper_limb_difference is zero iff all 15 possible values are 0", + "limb differences before first_different_limb are all 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()); - 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(), - ] + 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("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 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()); - vec![( - upper_limb_difference, - meta.query_fixed(u16_range, Rotation::cur()), - )] - }); - meta.lookup_any( - "upper_limb_difference is zero or lower_limb_difference fits into u16", + + meta.create_gate( + "limb_difference equals difference of limbs at index", |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()), - )] + 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 ((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(i, Rotation::cur())(meta) + * (limb_difference.clone() - cur_limb + prev_limb), + ); + } + constraints }, ); - assert!(meta.degree() <= 16); - meta.create_gate("lower_limb_difference is not zero", |meta| { - let selector = meta.query_fixed(selector, Rotation::cur()); - vec![(selector * lower_limb_difference_is_zero)] - }); - assert!(meta.degree() <= 16); config } - pub fn assign( + pub fn assign( &self, region: &mut Region<'_, F>, offset: usize, @@ -223,53 +199,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 = LimbIndex::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(((LimbIndex::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), )?; 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(()) } } @@ -284,23 +247,19 @@ 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>, 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), + 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), } } - 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() @@ -311,33 +270,24 @@ 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(self.address_limbs.iter().rev()) + .chain(once(&self.field_tag)) .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.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.storage_key().unwrap_or_default().to_be_bytes())); be_bytes.extend_from_slice(&((row.rw_counter() as u32).to_be_bytes())); @@ -348,39 +298,38 @@ fn rw_to_be_limbs(row: &Rw) -> Vec { .collect() } -fn upper_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()) - } - result -} - -fn lower_limb_difference_possible_values( +// 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, + 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()[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()) + let powers_of_randomness = once(1.expr()).chain(powers_of_randomness.into_iter()); + 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 + power_of_randomness * (cur_limb.clone() - prev_limb.clone()); } - assert_eq!(result.len(), 15); result } -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..]) -} +#[cfg(test)] +mod test { + use super::super::binary_number::{from_bits, AsBits}; + use super::LimbIndex; + use strum::IntoEnumIterator; -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 enough_bits_for_limb_index() { + for index in LimbIndex::iter() { + assert_eq!(from_bits(&index.as_bits()), index as usize); + } + } } diff --git a/zkevm-circuits/src/state_circuit/test.rs b/zkevm-circuits/src/state_circuit/test.rs index fd6c52ed85..891d88b977 100644 --- a/zkevm-circuits/src/state_circuit/test.rs +++ b/zkevm-circuits/src/state_circuit/test.rs @@ -10,11 +10,11 @@ use bus_mapping::operation::{ use eth_types::{ address, evm_types::{MemoryAddress, StackAddress}, - Address, Field, ToAddress, Word, U256, + Address, ToAddress, Word, U256, }; use halo2_proofs::poly::commitment::Params; use halo2_proofs::{ - arithmetic::{BaseExt, Field as halo2_field}, + arithmetic::BaseExt, dev::{MockProver, VerifyFailure}, pairing::bn256::{Bn256, Fr, G1Affine}, plonk::{keygen_vk, Advice, Circuit, Column, ConstraintSystem}, @@ -33,7 +33,6 @@ pub enum AdviceColumn { StorageKey, StorageKeyByte0, StorageKeyByte1, - StorageKeyChangeInverse, Value, RwCounter, RwCounterLimb0, @@ -42,27 +41,36 @@ pub enum AdviceColumn { TagBit1, TagBit2, TagBit3, + LimbIndexBit0, + LimbIndexBit1, + LimbIndexBit2, + LimbIndexBit3, + LimbIndexBit4, } 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.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::StorageKeyChangeInverse => config.is_storage_key_unchanged.value_inv, + 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::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::RwCounter => config.sort_keys.rw_counter.value, + Self::RwCounterLimb0 => config.sort_keys.rw_counter.limbs[0], + Self::RwCounterLimb1 => config.sort_keys.rw_counter.limbs[1], + 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], + 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], } } } @@ -92,7 +100,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] @@ -376,13 +384,7 @@ fn storage_key_mismatch() { tx_id: 4, committed_value: U256::from(5), }]; - let overrides = HashMap::from([ - ((AdviceColumn::StorageKey, 0), Fr::from(10)), - ( - (AdviceColumn::StorageKeyChangeInverse, 0), - Fr::from(10).invert().unwrap(), - ), - ]); + let overrides = HashMap::from([((AdviceColumn::StorageKey, 0), Fr::from(10))]); let result = verify_with_overrides(rows, overrides); @@ -405,10 +407,6 @@ fn storage_key_byte_out_of_range() { ((AdviceColumn::StorageKey, 0), Fr::from(256)), ((AdviceColumn::StorageKeyByte0, 0), Fr::from(256)), ((AdviceColumn::StorageKeyByte1, 0), Fr::zero()), - ( - (AdviceColumn::StorageKeyChangeInverse, 0), - Fr::from(256).invert().unwrap(), - ), ]); let result = verify_with_overrides(rows, overrides); @@ -450,10 +448,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] @@ -474,10 +469,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] @@ -498,10 +490,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] @@ -524,10 +513,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] @@ -554,10 +540,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] @@ -584,10 +567,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] @@ -608,9 +588,42 @@ fn nonlexicographic_order_rw_counter() { }; assert_eq!(verify(vec![first, second]), Ok(())); + 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, 1), Fr::one()), + ((AdviceColumn::LimbIndexBit1, 1), Fr::one()), + ((AdviceColumn::LimbIndexBit2, 1), Fr::one()), + ((AdviceColumn::LimbIndexBit3, 1), Fr::one()), + ((AdviceColumn::LimbIndexBit4, 1), Fr::one()), + ]); + + let result = verify_with_overrides(rows, overrides); + assert_error_matches( - verify(vec![second, first]), - "upper_limb_difference is zero or lower_limb_difference fits into u16", + result, + "limb differences before first_different_limb are all 0", ); } @@ -763,7 +776,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 also Stack with unchanged call id, address change is 0 or 1", ); }