feat: extract bit columns from BinaryNumberChip

ed255 · ed255 · commit 3d0d97db945a · 2024-02-16T10:08:11.000Z
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).
diff --git 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<const N: usize>(
+    /// Must be constrained to be binary for correctness.
+    pub [Column<Advice>; N],
+);
+
+impl<const N: usize> BinaryNumberBits<N> {
+    /// Construct a new BinaryNumberBits without adding any constraints.
+    pub fn construct<F: Field>(meta: &mut ConstraintSystem<F>) -> 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<F: Field, T: AsBits<N>>(
+        &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<F: Field>(
+        &self,
+        rotation: Rotation,
+    ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F> {
+        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<T, const N: usize> {
     /// Must be constrained to be binary for correctness.
-    pub bits: [Column<Advice>; N],
+    pub bits: BinaryNumberBits<N>,
     _marker: PhantomData<T>,
 }
 
@@ -51,12 +98,7 @@ where
         &self,
         rotation: Rotation,
     ) -> impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F> {
-        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<F> {
         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<F: Field>(&self, region: &mut Region<F>, 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<F>,
+        bits: BinaryNumberBits<N>,
         selector: Column<Fixed>,
         value: Option<Column<Advice>>,
     ) -> BinaryNumberConfig<T, N> {
-        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
@@ -69,6 +69,8 @@ pub struct CopyCircuitConfig<F> {
     /// 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<CopyDataType, 3>,
     /// 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,14 +130,15 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
         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);
         rw_table.annotate_columns(meta);
         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<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
             q_enable,
             addr_lt_addr_end,
             copy_table,
+            copy_table_tag: tag,
             tx_table,
             rw_table,
             bytecode_table,
@@ -526,7 +530,11 @@ impl<F: Field> CopyCircuitConfig<F> {
                     .zip_eq(table_row)
             {
                 // Leave sr_addr_end and bytes_left unassigned when !is_read
-                if !is_read && (label == "src_addr_end" || label == "bytes_left") {
+                // Leave tag_bit columns unassigned, since they are already assigned via
+                // `tag_chip.assign`
+                if (!is_read && (label == "src_addr_end" || label == "bytes_left"))
+                    || label == "tag_bit"
+                {
                 } else {
                     region.assign_advice(
                         || format!("{} at row: {}", label, offset),
@@ -605,7 +613,7 @@ impl<F: Field> CopyCircuitConfig<F> {
         );
         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
@@ -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<F: Field> SubCircuitConfig<F> for StateCircuitConfig<F> {
         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<F: Field> SubCircuit<F> for StateCircuit<F> {
 
 fn queries<F: Field>(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig<F>) -> Queries<F> {
     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,16 +593,17 @@ fn queries<F: Field>(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig<F>)
             .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
         // 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(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<F: Field>(meta: &mut VirtualCells<'_, F>, c: &StateCircuitConfig<F>)
         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
@@ -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
@@ -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<F>; 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
@@ -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
