Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Commit

Permalink
feat: extract bit columns from BinaryNumberChip
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
ed255 committed Feb 12, 2024
1 parent be3f121 commit 9eae48d
Show file tree
Hide file tree
Showing 7 changed files with 99 additions and 50 deletions.
77 changes: 57 additions & 20 deletions gadgets/src/binary_number.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
}

Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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));
Expand Down Expand Up @@ -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());
Expand Down Expand Up @@ -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)
}
}

Expand Down
8 changes: 6 additions & 2 deletions zkevm-circuits/src/copy_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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),
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -605,7 +609,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)?;
Expand Down
18 changes: 10 additions & 8 deletions zkevm-circuits/src/state_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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),
Expand All @@ -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()),
Expand Down
18 changes: 9 additions & 9 deletions zkevm-circuits/src/state_circuit/dev.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
5 changes: 3 additions & 2 deletions zkevm-circuits/src/state_circuit/lexicographic_ordering.rs
Original file line number Diff line number Diff line change
@@ -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},
Expand Down Expand Up @@ -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();

Expand Down
2 changes: 1 addition & 1 deletion zkevm-circuits/src/table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand Down
21 changes: 13 additions & 8 deletions zkevm-circuits/src/table/copy_table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,12 @@ pub struct CopyTable {
pub rwc_inc_left: Column<Advice>,
/// Selector for the tag BinaryNumberChip
pub q_enable: Column<Fixed>,
// 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<CopyDataType, 3>,
pub tag: BinaryNumberBits<3>,
}

impl CopyTable {
Expand All @@ -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(),
Expand Down Expand Up @@ -223,7 +225,6 @@ impl CopyTable {
}
offset += 1;

let tag_chip = BinaryNumberChip::construct(self.tag);
let copy_table_columns = <CopyTable as LookupTable<F>>::advice_columns(self);
for copy_event in block.copy_events.iter() {
for (tag, row, _) in Self::assignments(copy_event, *challenges) {
Expand All @@ -235,7 +236,7 @@ impl CopyTable {
|| value,
)?;
}
tag_chip.assign(&mut region, offset, &tag)?;
self.tag.assign(&mut region, offset, &tag)?;
offset += 1;
}
}
Expand All @@ -259,7 +260,7 @@ impl CopyTable {

impl<F: Field> LookupTable<F> for CopyTable {
fn columns(&self) -> Vec<Column<Any>> {
vec![
let mut columns = vec![
self.is_first.into(),
self.id.lo().into(),
self.id.hi().into(),
Expand All @@ -269,11 +270,13 @@ impl<F: Field> LookupTable<F> for CopyTable {
self.rlc_acc.into(),
self.rw_counter.into(),
self.rwc_inc_left.into(),
]
];
columns.extend(self.tag.0.iter().map(|c| Into::<Column<Any>>::into(*c)));
columns
}

fn annotations(&self) -> Vec<String> {
vec![
let mut names = vec![
String::from("is_first"),
String::from("id_lo"),
String::from("id_hi"),
Expand All @@ -283,7 +286,9 @@ impl<F: Field> LookupTable<F> 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<F>) -> Vec<Expression<F>> {
Expand Down

0 comments on commit 9eae48d

Please sign in to comment.