From 9eae48de288f5ceb7a66e93a2e89925ff5456890 Mon Sep 17 00:00:00 2001 From: Eduard S Date: Fri, 9 Feb 2024 16:25:40 +0000 Subject: [PATCH] feat: extract bit columns from BinaryNumberChip Extract the bit columns from BinaryNumberChip into BinaryNumberBits so that the columns can be used in a table without associated constraints. This is useful for the CopyTable to be used in unit tests outside of the CopyCircuit (without needing the BinaryNumberChip constraints). --- gadgets/src/binary_number.rs | 77 ++++++++++++++----- zkevm-circuits/src/copy_circuit.rs | 8 +- zkevm-circuits/src/state_circuit.rs | 18 +++-- zkevm-circuits/src/state_circuit/dev.rs | 18 ++--- .../state_circuit/lexicographic_ordering.rs | 5 +- zkevm-circuits/src/table.rs | 2 +- zkevm-circuits/src/table/copy_table.rs | 21 +++-- 7 files changed, 99 insertions(+), 50 deletions(-) diff --git a/gadgets/src/binary_number.rs b/gadgets/src/binary_number.rs index 788074c5fdd..15da9945f50 100644 --- a/gadgets/src/binary_number.rs +++ b/gadgets/src/binary_number.rs @@ -34,11 +34,58 @@ where } } +/// Columns of the binary number chip. This can be instantiated without the associated constraints +/// of the BinaryNumberChip in order to be used as part of a shared table for unit tests. +#[derive(Clone, Copy, Debug)] +pub struct BinaryNumberBits( + /// Must be constrained to be binary for correctness. + pub [Column; N], +); + +impl BinaryNumberBits { + /// Construct a new BinaryNumberBits without adding any constraints. + pub fn construct(meta: &mut ConstraintSystem) -> Self { + Self([0; N].map(|_| meta.advice_column())) + } + + /// Assign a value to the binary number bits. A generic type that implements + /// the AsBits trait can be provided for assignment. + pub fn assign>( + &self, + region: &mut Region<'_, F>, + offset: usize, + value: &T, + ) -> Result<(), Error> { + for (&bit, &column) in value.as_bits().iter().zip(&self.0) { + region.assign_advice( + || format!("binary number {:?}", column), + column, + offset, + || Value::known(F::from(bit as u64)), + )?; + } + Ok(()) + } + + /// Returns the expression value of the bits at the given rotation. + pub fn value( + &self, + rotation: Rotation, + ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression { + let bits = self.0; + move |meta: &mut VirtualCells<'_, F>| { + let bits = bits.map(|bit| meta.query_advice(bit, rotation)); + bits.iter() + .fold(0.expr(), |result, bit| bit.clone() + result * 2.expr()) + } + } +} + /// Config for the binary number chip. #[derive(Clone, Copy, Debug)] pub struct BinaryNumberConfig { /// Must be constrained to be binary for correctness. - pub bits: [Column; N], + pub bits: BinaryNumberBits, _marker: PhantomData, } @@ -51,12 +98,7 @@ where &self, rotation: Rotation, ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression { - let bits = self.bits; - move |meta: &mut VirtualCells<'_, F>| { - let bits = bits.map(|bit| meta.query_advice(bit, rotation)); - bits.iter() - .fold(0.expr(), |result, bit| bit.clone() + result * 2.expr()) - } + self.bits.value(rotation) } /// Return the constant that represents a given value. To be compared with the value expression. @@ -77,7 +119,9 @@ where rotation: 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))) + move |meta| { + Self::value_equals_expr(value, bits.0.map(|bit| meta.query_advice(bit, rotation))) + } } /// Returns a binary expression that evaluates to 1 if expressions are equal @@ -104,10 +148,11 @@ where /// Annotates columns of this gadget embedded within a circuit region. pub fn annotate_columns_in_region(&self, region: &mut Region, prefix: &str) { let mut annotations = Vec::new(); - for (i, _) in self.bits.iter().enumerate() { + for (i, _) in self.bits.0.iter().enumerate() { annotations.push(format!("GADGETS_binary_number_{}", i)); } self.bits + .0 .iter() .zip(annotations.iter()) .for_each(|(col, ann)| region.name_column(|| format!("{}_{}", prefix, ann), *col)); @@ -140,11 +185,11 @@ where /// Configure constraints for the binary number chip. pub fn configure( meta: &mut ConstraintSystem, + bits: BinaryNumberBits, selector: Column, value: Option>, ) -> BinaryNumberConfig { - let bits = [0; N].map(|_| meta.advice_column()); - bits.map(|bit| { + bits.0.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()); @@ -194,15 +239,7 @@ where offset: usize, value: &T, ) -> Result<(), Error> { - for (&bit, &column) in value.as_bits().iter().zip(&self.config.bits) { - region.assign_advice( - || format!("binary number {:?}", column), - column, - offset, - || Value::known(F::from(bit as u64)), - )?; - } - Ok(()) + self.config.bits.assign(region, offset, value) } } diff --git a/zkevm-circuits/src/copy_circuit.rs b/zkevm-circuits/src/copy_circuit.rs index 7e9cc18759b..77371bf7fb1 100644 --- a/zkevm-circuits/src/copy_circuit.rs +++ b/zkevm-circuits/src/copy_circuit.rs @@ -69,6 +69,8 @@ pub struct CopyCircuitConfig { /// The Copy Table contains the columns that are exposed via the lookup /// expressions pub copy_table: CopyTable, + /// BinaryNumber config out of the tag bits from `copy_table` + copy_table_tag: BinaryNumberConfig, /// Lt chip to check: src_addr < src_addr_end. /// Since `src_addr` and `src_addr_end` are u64, 8 bytes are sufficient for /// the Lt chip. @@ -128,7 +130,7 @@ impl SubCircuitConfig for CopyCircuitConfig { let rlc_acc = copy_table.rlc_acc; let rw_counter = copy_table.rw_counter; let rwc_inc_left = copy_table.rwc_inc_left; - let tag = copy_table.tag; + let tag_bits = copy_table.tag; // annotate table columns tx_table.annotate_columns(meta); @@ -136,6 +138,7 @@ impl SubCircuitConfig for CopyCircuitConfig { bytecode_table.annotate_columns(meta); copy_table.annotate_columns(meta); + let tag = BinaryNumberChip::configure(meta, tag_bits, q_enable, None); let addr_lt_addr_end = LtChip::configure( meta, |meta| meta.query_selector(q_step), @@ -471,6 +474,7 @@ impl SubCircuitConfig for CopyCircuitConfig { q_enable, addr_lt_addr_end, copy_table, + copy_table_tag: tag, tx_table, rw_table, bytecode_table, @@ -605,7 +609,7 @@ impl CopyCircuitConfig { ); let filler_rows = max_copy_rows - copy_rows_needed - DISABLED_ROWS; - let tag_chip = BinaryNumberChip::construct(self.copy_table.tag); + let tag_chip = BinaryNumberChip::construct(self.copy_table_tag); let lt_chip = LtChip::construct(self.addr_lt_addr_end); lt_chip.load(layouter)?; diff --git a/zkevm-circuits/src/state_circuit.rs b/zkevm-circuits/src/state_circuit.rs index 4dcbda633fe..d1f0f81dd4c 100644 --- a/zkevm-circuits/src/state_circuit.rs +++ b/zkevm-circuits/src/state_circuit.rs @@ -26,7 +26,7 @@ use constraint_builder::{ConstraintBuilder, Queries}; use eth_types::{Address, Field, Word}; use gadgets::{ batched_is_zero::{BatchedIsZeroChip, BatchedIsZeroConfig}, - binary_number::{BinaryNumberChip, BinaryNumberConfig}, + binary_number::{BinaryNumberBits, BinaryNumberChip, BinaryNumberConfig}, }; use halo2_proofs::{ circuit::{Layouter, Region, Value}, @@ -107,7 +107,8 @@ impl SubCircuitConfig for StateCircuitConfig { let lookups = LookupsChip::configure(meta, u8_table, u10_table, u16_table); let rw_counter = MpiChip::configure(meta, selector, [rw_table.rw_counter], lookups); - let tag = BinaryNumberChip::configure(meta, selector, Some(rw_table.tag)); + let bits = BinaryNumberBits::construct(meta); + let tag = BinaryNumberChip::configure(meta, bits, selector, Some(rw_table.tag)); let id = MpiChip::configure(meta, selector, [rw_table.id], lookups); let address = MpiChip::configure(meta, selector, [rw_table.address], lookups); @@ -529,8 +530,8 @@ impl SubCircuit for StateCircuit { fn queries(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig) -> Queries { let first_different_limb = c.lexicographic_ordering.first_different_limb; - let final_bits_sum = meta.query_advice(first_different_limb.bits[3], Rotation::cur()) - + meta.query_advice(first_different_limb.bits[4], Rotation::cur()); + let final_bits_sum = meta.query_advice(first_different_limb.bits.0[3], Rotation::cur()) + + meta.query_advice(first_different_limb.bits.0[4], Rotation::cur()); let mpt_update_table_expressions = c.mpt_table.table_exprs(meta); assert_eq!(mpt_update_table_expressions.len(), 12); @@ -592,6 +593,7 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig) .sort_keys .tag .bits + .0 .map(|bit| meta.query_advice(bit, Rotation::cur())), 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 @@ -599,9 +601,9 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig) // 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(first_different_limb.bits[0], Rotation::cur()) - + meta.query_advice(first_different_limb.bits[1], Rotation::cur()) - + meta.query_advice(first_different_limb.bits[2], Rotation::cur())) + * (meta.query_advice(first_different_limb.bits.0[0], Rotation::cur()) + + meta.query_advice(first_different_limb.bits.0[1], Rotation::cur()) + + meta.query_advice(first_different_limb.bits.0[2], Rotation::cur())) + final_bits_sum.clone() * (1.expr() - final_bits_sum), address: MpiQueries::new(meta, c.sort_keys.address), storage_key: MpiQueries::new(meta, c.sort_keys.storage_key), @@ -611,7 +613,7 @@ fn queries(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig) mpt_proof_type: meta.query_advice(c.mpt_proof_type, Rotation::cur()), lookups: LookupsQueries::new(meta, c.lookups), first_different_limb: [0, 1, 2, 3] - .map(|idx| meta.query_advice(first_different_limb.bits[idx], Rotation::cur())), + .map(|idx| meta.query_advice(first_different_limb.bits.0[idx], Rotation::cur())), not_first_access: meta.query_advice(c.not_first_access, Rotation::cur()), last_access: 1.expr() - meta.query_advice(c.not_first_access, Rotation::next()), state_root: meta_query_word(meta, c.state_root, Rotation::cur()), diff --git a/zkevm-circuits/src/state_circuit/dev.rs b/zkevm-circuits/src/state_circuit/dev.rs index 193cf2e52cc..c99b41fc3f4 100644 --- a/zkevm-circuits/src/state_circuit/dev.rs +++ b/zkevm-circuits/src/state_circuit/dev.rs @@ -119,15 +119,15 @@ impl AdviceColumn { Self::RwCounterLimb0 => config.sort_keys.rw_counter.limbs[0], Self::_RwCounterLimb1 => config.sort_keys.rw_counter.limbs[1], Self::Tag => config.rw_table.tag, - 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], + Self::TagBit0 => config.sort_keys.tag.bits.0[0], + Self::TagBit1 => config.sort_keys.tag.bits.0[1], + Self::TagBit2 => config.sort_keys.tag.bits.0[2], + Self::TagBit3 => config.sort_keys.tag.bits.0[3], + Self::_LimbIndexBit0 => config.lexicographic_ordering.first_different_limb.bits.0[0], + Self::LimbIndexBit1 => config.lexicographic_ordering.first_different_limb.bits.0[1], + Self::LimbIndexBit2 => config.lexicographic_ordering.first_different_limb.bits.0[2], + Self::_LimbIndexBit3 => config.lexicographic_ordering.first_different_limb.bits.0[3], + Self::_LimbIndexBit4 => config.lexicographic_ordering.first_different_limb.bits.0[4], Self::InitialValueLo => config.initial_value.lo(), Self::InitialValueHi => config.initial_value.hi(), Self::IsZero => config.is_non_exist.is_zero, diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 062a85cb008..77786b88e02 100644 --- a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs +++ b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs @@ -1,7 +1,7 @@ use super::{lookups, param::*, SortKeysConfig}; use crate::{evm_circuit::param::N_BYTES_WORD, impl_expr, util::Expr, witness::Rw}; use eth_types::{Field, ToBigEndian}; -use gadgets::binary_number::{AsBits, BinaryNumberChip, BinaryNumberConfig}; +use gadgets::binary_number::{AsBits, BinaryNumberBits, BinaryNumberChip, BinaryNumberConfig}; use halo2_proofs::{ circuit::{Region, Value}, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, @@ -110,7 +110,8 @@ impl Config { powers_of_randomness: [Expression; N_BYTES_WORD - 1], ) -> Self { let selector = meta.fixed_column(); - let first_different_limb = BinaryNumberChip::configure(meta, selector, None); + let bits = BinaryNumberBits::construct(meta); + let first_different_limb = BinaryNumberChip::configure(meta, bits, selector, None); let limb_difference = meta.advice_column(); let limb_difference_inverse = meta.advice_column(); diff --git a/zkevm-circuits/src/table.rs b/zkevm-circuits/src/table.rs index 8b19355a7e3..74b1f4c7fe6 100644 --- a/zkevm-circuits/src/table.rs +++ b/zkevm-circuits/src/table.rs @@ -11,7 +11,7 @@ use bus_mapping::circuit_input_builder::{CopyDataType, CopyEvent, CopyStep}; use core::iter::once; use eth_types::{Field, ToScalar, U256}; use gadgets::{ - binary_number::{BinaryNumberChip, BinaryNumberConfig}, + binary_number::BinaryNumberBits, util::{split_u256, split_u256_limb64}, }; use halo2_proofs::{ diff --git a/zkevm-circuits/src/table/copy_table.rs b/zkevm-circuits/src/table/copy_table.rs index cbd9cbbdb2e..50639820694 100644 --- a/zkevm-circuits/src/table/copy_table.rs +++ b/zkevm-circuits/src/table/copy_table.rs @@ -34,10 +34,12 @@ pub struct CopyTable { pub rwc_inc_left: Column, /// Selector for the tag BinaryNumberChip pub q_enable: Column, + // We use the `BinaryNumberBits` instead of `BinaryNumberChip` in order to construct the table + // without attaching any constraints. /// Binary chip to constrain the copy table conditionally depending on the /// current row's tag, whether it is Bytecode, Memory, TxCalldata or /// TxLog. - pub tag: BinaryNumberConfig, + pub tag: BinaryNumberBits<3>, } impl CopyTable { @@ -47,7 +49,7 @@ impl CopyTable { is_first: meta.advice_column(), id: WordLoHi::new([meta.advice_column(), meta.advice_column()]), q_enable, - tag: BinaryNumberChip::configure(meta, q_enable, None), + tag: BinaryNumberBits::construct(meta), addr: meta.advice_column(), src_addr_end: meta.advice_column(), bytes_left: meta.advice_column(), @@ -223,7 +225,6 @@ impl CopyTable { } offset += 1; - let tag_chip = BinaryNumberChip::construct(self.tag); let copy_table_columns = >::advice_columns(self); for copy_event in block.copy_events.iter() { for (tag, row, _) in Self::assignments(copy_event, *challenges) { @@ -235,7 +236,7 @@ impl CopyTable { || value, )?; } - tag_chip.assign(&mut region, offset, &tag)?; + self.tag.assign(&mut region, offset, &tag)?; offset += 1; } } @@ -259,7 +260,7 @@ impl CopyTable { impl LookupTable for CopyTable { fn columns(&self) -> Vec> { - vec![ + let mut columns = vec![ self.is_first.into(), self.id.lo().into(), self.id.hi().into(), @@ -269,11 +270,13 @@ impl LookupTable for CopyTable { self.rlc_acc.into(), self.rw_counter.into(), self.rwc_inc_left.into(), - ] + ]; + columns.extend(self.tag.0.iter().map(|c| Into::>::into(*c))); + columns } fn annotations(&self) -> Vec { - vec![ + let mut names = vec![ String::from("is_first"), String::from("id_lo"), String::from("id_hi"), @@ -283,7 +286,9 @@ impl LookupTable for CopyTable { String::from("rlc_acc"), String::from("rw_counter"), String::from("rwc_inc_left"), - ] + ]; + names.extend((0..self.tag.0.len()).map(|i| format!("tag_bit{i}"))); + names } fn table_exprs(&self, meta: &mut VirtualCells) -> Vec> {