diff --git a/gadgets/src/binary_number.rs b/gadgets/src/binary_number.rs index 788074c5fd..68a3dd2e86 100644 --- a/gadgets/src/binary_number.rs +++ b/gadgets/src/binary_number.rs @@ -9,7 +9,7 @@ use halo2_proofs::{ plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, poly::Rotation, }; -use std::{collections::BTreeSet, marker::PhantomData}; +use std::{collections::BTreeSet, marker::PhantomData, ops::Deref}; use strum::IntoEnumIterator; /// Helper trait that implements functionality to represent a generic type as @@ -34,11 +34,66 @@ 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 Deref for BinaryNumberBits { + type Target = [Column; N]; + + fn deref(&self) -> &Self::Target { + &self.0 + } +} + +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.iter()) { + 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 +106,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. @@ -140,10 +190,10 @@ 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| { meta.create_gate("bit column is 0 or 1", |meta| { let selector = meta.query_fixed(selector, Rotation::cur()); @@ -194,15 +244,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/integration-tests/Cargo.toml b/integration-tests/Cargo.toml index 068341dcdf..bd8e732c20 100644 --- a/integration-tests/Cargo.toml +++ b/integration-tests/Cargo.toml @@ -13,7 +13,7 @@ serde_json = { version = "1.0.66", features = ["unbounded_depth"] } serde = { version = "1.0.130", features = ["derive"] } bus-mapping = { path = "../bus-mapping", features = ["test"] } eth-types = { path = "../eth-types" } -zkevm-circuits = { path = "../zkevm-circuits", features = ["test-circuits"] } +zkevm-circuits = { path = "../zkevm-circuits", features = ["test-circuits", "mock-challenge"] } tokio = { version = "1.13", features = ["macros", "rt-multi-thread"] } url = "2.2.2" pretty_assertions = "1.0.0" diff --git a/zkevm-circuits/Cargo.toml b/zkevm-circuits/Cargo.toml index 3a64d19a9f..b48e98e538 100644 --- a/zkevm-circuits/Cargo.toml +++ b/zkevm-circuits/Cargo.toml @@ -63,7 +63,8 @@ test-circuits = [] # Test utilities for testool crate to consume test-util = ["dep:mock"] warn-unimplemented = ["eth-types/warn-unimplemented"] -stats = ["warn-unimplemented", "dep:cli-table"] +stats = ["warn-unimplemented", "dep:cli-table", "test-util", "test-circuits", "mock-challenge"] +mock-challenge = [] [[bin]] name = "stats" diff --git a/zkevm-circuits/src/bin/stats/halo2_stats.rs b/zkevm-circuits/src/bin/stats/halo2_stats.rs new file mode 100644 index 0000000000..fe17d11e3f --- /dev/null +++ b/zkevm-circuits/src/bin/stats/halo2_stats.rs @@ -0,0 +1,387 @@ +//! Utility functions and types to get circuit stats from any halo2 circuit + +use eth_types::Field; +use halo2_proofs::plonk::ConstraintSystem; +use std::collections::BTreeSet; + +// From Scroll https://github.com/scroll-tech/zkevm-circuits/blob/7d9bc181953cfc6e7baf82ff0ce651281fd70a8a/zkevm-circuits/src/util.rs#L275 +#[allow(dead_code)] +#[derive(Debug, Default)] +pub(crate) struct CircuitStats { + pub num_constraints: usize, + pub num_fixed_columns: usize, + pub num_lookups: usize, + pub num_shuffles: usize, + pub num_advice_columns: usize, + pub num_instance_columns: usize, + pub num_selectors: usize, + pub num_permutation_columns: usize, + pub degree: usize, + pub blinding_factors: usize, + pub num_challenges: usize, + pub max_phase: u8, + pub num_rotation: usize, + pub min_rotation: i32, + pub max_rotation: i32, + pub verification_msm_size: usize, + // Aux data to diff between records + num_advice_queries: usize, + num_gates: usize, +} + +impl CircuitStats { + // Peak memory analysis by Han: + // + // fn create_proof(params: &KZGParams, pk: &ProvingKey, circuit: &Circuit, instances: &[&[F]]) { + // Let: + // + // - k: log 2 of number of rows + // - n: `1 << k` + // - d: Degree of circuit + // - e: Extension magnitude, equal to `(d - 1).next_power_of_two()` + // - c_f: number of fixed columns + // - c_a: number of advice columns + // - c_i: number of instance columns + // - c_p: number of columns enabled with copy constraint + // - c_pg: number of grand product in permutation argument, equal to `div_ceil(c_p, d - 2)` + // - c_l: number of lookup argument + // + // The memory usage M.C and M.S stands for: + // + // - M.C: number of "elliptic curve points" (with symbol ◯) + // - M.S: number of "field elements" (with symbol △) + // - M.E: number of "field elements" that will be extended by "* e" (with symbol ⬡) + // + // So the actual memory usage in terms of bytes will be: + // + // M = 32 * n * (2 * M.C + M.S + e * M.E) + // + // We'll ignore other values with sublinear amount to n. + // + // + // 0. In the beginning: + // + // `params` has: + // ◯ powers_of_tau + // ◯ ifft(powers_of_tau) + // + // M.C = 2 (+= 2) + // M.S = 0 + // M.E = 0 + // + // `pk` has: + // ⬡ l0 + // ⬡ l_last + // ⬡ l_active_row + // △ fixed_lagranges (c_f) + // △ fixed_monomials (c_f) + // ⬡ fixed_extended_lagranges (c_f) + // △ permutation_lagranges (c_p) + // △ permutation_monomials (c_p) + // ⬡ permutation_extended_lagranges (c_p) + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p (+= 2 * c_f + 2 * c_p) + // M.E = 3 + c_f + c_p (+= 3 + c_f + c_p) + // + // And let's ignore `circuit` + // + // + // ### 1. Pad instances as lagrange form and compute its monomial form. + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p + 2 * c_i (+= 2 * c_i) + // M.E = 3 + c_f + c_p + // ``` + // let instance_lagranges = instances.to_lagranges(); + // let instance_monomials = instance_lagranges.to_monomials(); + // ``` + // + // + // ### 2. Synthesize circuit and collect advice column values. + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p + 2 * c_i + c_a (+= c_a) + // M.E = 3 + c_f + c_p + // ``` + // let advice_lagranges = circuit.synthesize_all_phases(); + // ``` + // + // + // ### 3. Generate permuted input and table of lookup argument. + // For each lookup argument, we have: + // + // △ compressed_input_lagranges - cached for later computation + // △ permuted_input_lagranges + // △ permuted_input_monomials + // △ compressed_table_lagranges - cached for later computation + // △ permuted_table_lagranges + // △ permuted_table_monomials + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p + 2 * c_i + c_a + 6 * c_l (+= 6 * c_l) + // M.E = 3 + c_f + c_p + // ``` + // let ( + // compressed_input_lagranges, + // permuted_input_lagranges, + // permuted_input_monomials, + // compressed_table_lagranges, + // permuted_table_lagranges, + // permuted_table_monomials, + // ) = lookup_permuted() + // ``` + // + // + // ### 4. Generate grand products of permutation argument. + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p + 2 * c_i + c_a + 6 * c_l + c_pg (+= c_pg) + // M.E = 3 + c_f + c_p + c_pg (+= c_pg) + // ``` + // let ( + // perm_grand_product_monomials, + // perm_grand_product_extended_lagranges, + // ) = permutation_grand_products(); + // ``` + // + // + // ### 5. Generate grand products of lookup argument. + // And then drops unnecessary lagranges values. + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg (-= 3 * c_l) + // M.E = 3 + c_f + c_p + c_pg + // > let lookup_product_monomials = lookup_grand_products(); + // > drop(compressed_input_lagranges); + // > drop(permuted_input_lagranges); + // > drop(compressed_table_lagranges); + // > drop(permuted_table_lagranges); + // + // + // ### 6. Generate random polynomial. + // + // M.C = 2 + // M.S = 1 + 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg (+= 1) + // M.E = 3 + c_f + c_p + c_pg + // ``` + // let random_monomial = random(); + // ``` + // + // + // ### 7. Turn advice_lagranges into advice_monomials. + // ``` + // let advice_monomials = advice_lagranges.to_monomials(); + // drop(advice_lagranges); + // ``` + // + // + // ### 8. Generate necessary extended lagranges. + // + // M.C = 2 + // M.S = 1 + 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg + // M.E = 3 + c_f + c_p + c_pg + c_i + c_a (+= c_i + c_a) + // ``` + // let instances_extended_lagrnages = instances_monomials.to_extended_lagranges(); + // let advice_extended_lagrnages = advice_monomials.to_extended_lagranges(); + // ``` + // + // + // ### 9. While computing the quotient, these extended lagranges: + // + // ⬡ permuted_input_extended_lagranges + // ⬡ permuted_table_extended_lagranges + // ⬡ lookup_product_extended_lagranges + // + // of each lookup argument are generated on the fly and drop before next. + // + // And 1 extra quotient_extended_lagrange is created. So the peak memory: + // + // M.C = 2 + // M.S = 1 + 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg + // M.E = 4 + c_f + c_p + c_pg + c_i + c_a + 3 * (c_l > 0) (+= 3 * (c_l > 0) + 1) + // ``` + // let quotient_extended_lagrange = quotient_extended_lagrange(); + // ``` + // + // + // ### 10. After quotient is comuputed, drop all the other extended lagranges. + // + // M.C = 2 + // M.S = 1 + 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg + // M.E = 4 + c_f + c_p (-= c_pg + c_i + c_a + 3 * (c_l > 0)) + // drop(instances_extended_lagrnages) + // drop(advice_extended_lagrnages) + // drop(perm_grand_product_extended_lagranges) + // + // + // ### 11. Turn quotient_extended_lagrange into monomial form. + // And then cut int `d - 1` pieces. + // + // M.C = 2 + // M.S = 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg + d (+= d - 1) + // M.E = 3 + c_f + c_p (-= 1) + // ``` + // let quotient_monomials = quotient_monomials() + // drop(quotient_extended_lagrange) + // ``` + // + // + // ### 12. Evaluate and open all polynomial except instance ones. + // } + pub(crate) fn estimate_peak_mem(&self, k: u32) -> usize { + let field_bytes = 32; + let c_f = self.num_fixed_columns; + let c_a = self.num_advice_columns; + let c_i = self.num_instance_columns; + let c_p = self.num_permutation_columns; + let c_l = self.num_lookups; + let c_pg = c_p.div_ceil(self.degree - 2); + let e = (self.degree - 1).next_power_of_two(); + // The estimated peak memory formula comes from step 9 of the analysis, which is the step + // of proving that needs the most memory (after that step, allocations start getting freed) + + // number of "elliptic curve points" + let m_c = 2; + // number of "field elements" + let m_s = 1 + 2 * c_f + 2 * c_p + 2 * c_i + c_a + 3 * c_l + c_pg; + // number of "field elements" that will be extended by "* e" + let m_e = 4 + c_f + c_p + c_pg + c_i + c_a + 3 * (c_l > 0) as usize; + let unit = 2 * m_c + m_s + e * m_e; + unit * 2usize.pow(k) * field_bytes + } +} + +// Return the stats in `meta`, accounting only for the circuit delta from the last aggregated stats +// in `agg`. +// Adapted from Scroll https://github.com/scroll-tech/zkevm-circuits/blob/7d9bc181953cfc6e7baf82ff0ce651281fd70a8a/zkevm-circuits/src/util.rs#L294 +pub(crate) fn circuit_stats( + agg: &CircuitStats, + meta: &ConstraintSystem, +) -> CircuitStats { + let max_phase = meta + .advice_column_phase() + .iter() + .skip(agg.num_advice_columns) + .max() + .copied() + .unwrap_or_default(); + + let rotations = meta + .advice_queries() + .iter() + .skip(agg.num_advice_queries) + .map(|(_, q)| q.0) + .collect::>(); + + let degree = meta.degree(); + let num_fixed_columns = meta.num_fixed_columns() - agg.num_fixed_columns; + let num_lookups = meta.lookups().len() - agg.num_lookups; + let num_shuffles = meta.shuffles().len() - agg.num_shuffles; + let num_advice_columns = meta.num_advice_columns() - agg.num_advice_columns; + let num_instance_columns = meta.num_instance_columns() - agg.num_instance_columns; + let num_selectors = meta.num_selectors() - agg.num_selectors; + let num_permutation_columns = + meta.permutation().get_columns().len() - agg.num_permutation_columns; + + // This calculation has some differences with the Scroll implementation at + // https://github.com/scroll-tech/zkevm-circuits/blob/7d9bc181953cfc6e7baf82ff0ce651281fd70a8a/zkevm-circuits/src/util.rs#L320-L326 + // - Remove `num_instance_columns` because it doesn't contribute when using the KZG commitment + // scheme + // - Assume SHPLONK for batch opening scheme (replaces `rotations.len()` by `1`) + // - Add `degree -1` to account for quotients + // - Add `div_ceil(num_permutation_columns, degree - 2)` for permutation arguments grand + // products. + let verification_msm_size = num_advice_columns + + num_permutation_columns // Preprocessed permutation column + + num_permutation_columns.div_ceil(degree-2) // Grand product for permutations + + num_shuffles // Grand product of each shuffle + + num_selectors // Assume no selector compression (giving us an upper bound estimation) + + num_fixed_columns + // Grand product, permuted input expression and permuted table expression for each lookup + + 3 * num_lookups + + 2 // SHPLONK batch opening scheme + + (degree -1); // quotients + + CircuitStats { + num_constraints: meta + .gates() + .iter() + .skip(agg.num_gates) + .map(|g| g.polynomials().len()) + .sum::(), + num_fixed_columns, + num_lookups, + num_shuffles, + num_advice_columns, + num_instance_columns, + num_selectors, + num_permutation_columns, + degree, + blinding_factors: meta.blinding_factors(), + num_challenges: meta.num_challenges() - agg.num_challenges, + max_phase, + num_rotation: rotations.len(), + min_rotation: rotations.first().cloned().unwrap_or_default(), + max_rotation: rotations.last().cloned().unwrap_or_default(), + verification_msm_size, + num_advice_queries: meta.advice_queries().len() - agg.num_advice_queries, + num_gates: meta.gates().len() - agg.num_gates, + } +} + +pub(crate) struct StatsCollection { + aggregate: bool, + shared_cs: ConstraintSystem, + pub(crate) agg: CircuitStats, + pub(crate) list: Vec<(String, CircuitStats)>, +} + +impl StatsCollection { + // With aggregate=true, all records are overwritten each time, leading to a single + // aggregate stats that represents the final circuit. + // With aggregate=false, each record is stored in a different entry with a name, and the + // ConstraintSystem is reset so that each entry is independent. + pub(crate) fn new(aggregate: bool) -> Self { + Self { + aggregate, + shared_cs: ConstraintSystem::default(), + agg: CircuitStats::default(), + list: Vec::new(), + } + } + + // Record a shared table + pub(crate) fn record_shared(&mut self, name: &str, meta: &mut ConstraintSystem) { + // Shared tables should only add columns, and nothing more + assert_eq!(meta.lookups().len(), 0); + assert_eq!(meta.shuffles().len(), 0); + assert_eq!(meta.permutation().get_columns().len(), 0); + assert_eq!(meta.degree(), 3); // 3 comes from the permutation argument + assert_eq!(meta.blinding_factors(), 5); // 5 is the minimum blinding factor + assert_eq!(meta.advice_queries().len(), 0); + assert_eq!(meta.gates().len(), 0); + + if self.aggregate { + self.agg = circuit_stats(&CircuitStats::default(), meta); + } else { + let stats = circuit_stats(&self.agg, meta); + self.agg = circuit_stats(&CircuitStats::default(), meta); + self.list.push((name.to_string(), stats)); + // Keep the ConstraintSystem with all the tables + self.shared_cs = meta.clone(); + } + } + + // Record a subcircuit + pub(crate) fn record(&mut self, name: &str, meta: &mut ConstraintSystem) { + if self.aggregate { + self.agg = circuit_stats(&CircuitStats::default(), meta); + } else { + let stats = circuit_stats(&self.agg, meta); + self.list.push((name.to_string(), stats)); + // Revert meta to the ConstraintSystem just with the tables + *meta = self.shared_cs.clone(); + } + } +} diff --git a/zkevm-circuits/src/bin/stats/main.rs b/zkevm-circuits/src/bin/stats/main.rs index 73514d35cc..dbf9b4b9a3 100644 --- a/zkevm-circuits/src/bin/stats/main.rs +++ b/zkevm-circuits/src/bin/stats/main.rs @@ -1,23 +1,43 @@ +//! Build with `--features="stats"` + +mod halo2_stats; +mod helpers; + use bus_mapping::circuit_input_builder::FeatureConfig; use cli_table::{print_stdout, Cell, Style, Table}; use eth_types::{bytecode, evm_types::OpcodeId, ToWord}; use halo2_proofs::{ halo2curves::bn256::Fr, - plonk::{Circuit, ConstraintSystem}, + plonk::{Circuit, ConstraintSystem, Expression}, }; -mod helpers; +use halo2_stats::StatsCollection; use helpers::{bytecode_prefix_op_big_rws, print_circuit_stats_by_states}; use itertools::Itertools; use mock::MOCK_ACCOUNTS; -use std::env; -use zkevm_circuits::evm_circuit::{ - param::{ - LOOKUP_CONFIG, N_COPY_COLUMNS, N_PHASE1_COLUMNS, N_PHASE2_COLUMNS, N_U16_LOOKUPS, - N_U8_LOOKUPS, +use std::{array, env, iter}; +use zkevm_circuits::{ + bytecode_circuit::{BytecodeCircuitConfig, BytecodeCircuitConfigArgs}, + copy_circuit::{CopyCircuitConfig, CopyCircuitConfigArgs}, + evm_circuit::{ + param::{ + LOOKUP_CONFIG, N_COPY_COLUMNS, N_PHASE1_COLUMNS, N_PHASE2_COLUMNS, N_U16_LOOKUPS, + N_U8_LOOKUPS, + }, + step::ExecutionState, + EvmCircuit, EvmCircuitConfig, EvmCircuitConfigArgs, + }, + exp_circuit::ExpCircuitConfig, + keccak_circuit::{KeccakCircuitConfig, KeccakCircuitConfigArgs}, + pi_circuit::{PiCircuitConfig, PiCircuitConfigArgs}, + state_circuit::{StateCircuitConfig, StateCircuitConfigArgs}, + table::{ + BlockTable, BytecodeTable, CopyTable, ExpTable, KeccakTable, MptTable, RwTable, SigTable, + TxTable, UXTable, WdTable, }, - step::ExecutionState, - EvmCircuit, + tx_circuit::{TxCircuitConfig, TxCircuitConfigArgs}, + util::{Challenges, SubCircuitConfig}, }; + fn main() { let args: Vec = env::args().collect(); @@ -26,6 +46,7 @@ fn main() { "state" => state_states_stats(), "copy" => copy_states_stats(), "exec" => get_exec_steps_occupancy(), + "general" => general_subcircuit_stats(), &_ => unreachable!("Unsupported arg"), } } @@ -204,3 +225,196 @@ fn get_exec_steps_occupancy() { LOOKUP_CONFIG[7].1 ); } + +#[allow(unused_variables)] +fn record_stats( + stats: &mut StatsCollection, + meta: &mut ConstraintSystem, +) { + let max_txs = 1; + let max_withdrawals = 5; + let max_calldata = 32; + let mock_randomness = F::from(0x100); + let feature_config = FeatureConfig::default(); + + // Shared Tables + let tx_table = TxTable::construct(meta); + stats.record_shared("tx_table", meta); + let wd_table = WdTable::construct(meta); + stats.record_shared("wd_table", meta); + let rw_table = RwTable::construct(meta); + stats.record_shared("rw_table", meta); + let mpt_table = MptTable::construct(meta); + stats.record_shared("mpt_table", meta); + let bytecode_table = BytecodeTable::construct(meta); + stats.record_shared("bytecode_table", meta); + let block_table = BlockTable::construct(meta); + stats.record_shared("block_table", meta); + let q_copy_table = meta.fixed_column(); + let copy_table = CopyTable::construct(meta, q_copy_table); + stats.record_shared("copy_table", meta); + let exp_table = ExpTable::construct(meta); + stats.record_shared("exp_table", meta); + let keccak_table = KeccakTable::construct(meta); + stats.record_shared("keccak_table", meta); + let sig_table = SigTable::construct(meta); + stats.record_shared("sig_table", meta); + let u8_table = UXTable::construct(meta); + stats.record_shared("u8_table", meta); + let u10_table = UXTable::construct(meta); + stats.record_shared("u10_table", meta); + let u16_table = UXTable::construct(meta); + stats.record_shared("u16_table", meta); + + // Use a mock randomness instead of the randomness derived from the challenge + // (either from mock or real prover) to help debugging assignments. + let power_of_randomness: [Expression; 31] = + array::from_fn(|i| Expression::Constant(mock_randomness.pow([1 + i as u64, 0, 0, 0]))); + + let challenges = Challenges::mock( + power_of_randomness[0].clone(), + power_of_randomness[0].clone(), + ); + + let keccak_circuit = KeccakCircuitConfig::new( + meta, + KeccakCircuitConfigArgs { + keccak_table: keccak_table.clone(), + challenges: challenges.clone(), + }, + ); + stats.record("keccak", meta); + + let pi_circuit = PiCircuitConfig::new( + meta, + PiCircuitConfigArgs { + max_txs, + max_withdrawals, + max_calldata, + block_table: block_table.clone(), + tx_table: tx_table.clone(), + wd_table, + keccak_table: keccak_table.clone(), + challenges: challenges.clone(), + }, + ); + stats.record("pi", meta); + let tx_circuit = TxCircuitConfig::new( + meta, + TxCircuitConfigArgs { + tx_table: tx_table.clone(), + keccak_table: keccak_table.clone(), + challenges: challenges.clone(), + }, + ); + stats.record("tx", meta); + let bytecode_circuit = BytecodeCircuitConfig::new( + meta, + BytecodeCircuitConfigArgs { + bytecode_table: bytecode_table.clone(), + keccak_table: keccak_table.clone(), + challenges: challenges.clone(), + }, + ); + stats.record("bytecode", meta); + let copy_circuit = CopyCircuitConfig::new( + meta, + CopyCircuitConfigArgs { + tx_table: tx_table.clone(), + rw_table, + bytecode_table: bytecode_table.clone(), + copy_table, + q_enable: q_copy_table, + challenges: challenges.clone(), + }, + ); + stats.record("copy", meta); + let state_circuit = StateCircuitConfig::new( + meta, + StateCircuitConfigArgs { + rw_table, + mpt_table, + u8_table, + u10_table, + u16_table, + challenges: challenges.clone(), + }, + ); + stats.record("state", meta); + let exp_circuit = ExpCircuitConfig::new(meta, exp_table); + stats.record("exp", meta); + let evm_circuit = EvmCircuitConfig::new( + meta, + EvmCircuitConfigArgs { + challenges, + tx_table, + rw_table, + bytecode_table, + block_table, + copy_table, + keccak_table, + exp_table, + u8_table, + u16_table, + sig_table, + feature_config, + }, + ); + stats.record("evm", meta); +} + +fn general_subcircuit_stats() { + let mut stats_list = StatsCollection::::new(false); + let mut meta = ConstraintSystem::::default(); + record_stats(&mut stats_list, &mut meta); + let mut stats_agg = StatsCollection::::new(true); + let mut meta = ConstraintSystem::::default(); + record_stats(&mut stats_agg, &mut meta); + + let mut table = Vec::new(); + for (name, stats) in stats_list + .list + .iter() + .chain(iter::once(&("super".to_string(), stats_agg.agg))) + { + // At 0.0139 gas/row this gives us 2^26 * 0.0139 = ~900k gas. For 30M gas we would need 33 + // chunks. + let k = 26; + let peak_mem_gb = stats.estimate_peak_mem(k) / 1024 / 1024 / 1024; + table.push(vec![ + name.cell(), + stats.num_constraints.cell(), + stats.num_rotation.cell(), + format!("{}/{}", stats.min_rotation, stats.max_rotation).cell(), + stats.num_fixed_columns.cell(), + stats.num_selectors.cell(), + stats.num_advice_columns.cell(), + stats.num_permutation_columns.cell(), + stats.num_lookups.cell(), + stats.degree.cell(), + peak_mem_gb.cell(), + ]); + } + let table = table + .table() + .title( + [ + "circuit", + "constraints", + "rots", + "min/max(rots)", + "fix_cols", + "selectors", + "adv_cols", + "perm_cols", + "lookups", + "degree", + "mem_gb", + ] + .iter() + .map(|s| s.cell().bold(true)), + ) + .bold(true); + + assert!(print_stdout(table).is_ok()); +} diff --git a/zkevm-circuits/src/copy_circuit.rs b/zkevm-circuits/src/copy_circuit.rs index 489dfbcca2..dff1f99a42 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, @@ -526,7 +530,11 @@ impl CopyCircuitConfig { .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 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 81825492f4..141eab0e51 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); diff --git a/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs b/zkevm-circuits/src/state_circuit/lexicographic_ordering.rs index 4d90c23dae..b8a5f4de45 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}, @@ -108,7 +108,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/super_circuit.rs b/zkevm-circuits/src/super_circuit.rs index 786493e399..53b7a90c30 100644 --- a/zkevm-circuits/src/super_circuit.rs +++ b/zkevm-circuits/src/super_circuit.rs @@ -97,6 +97,8 @@ pub struct SuperCircuitConfig { keccak_circuit: KeccakCircuitConfig, pi_circuit: PiCircuitConfig, exp_circuit: ExpCircuitConfig, + #[cfg(not(feature = "mock-challenge"))] + challenges: Challenges, } impl SubCircuitConfig for SuperCircuitConfig { @@ -128,21 +130,31 @@ impl SubCircuitConfig for SuperCircuitConfig { let u16_table = UXTable::construct(meta); // Use a mock randomness instead of the randomness derived from the challenge - // (either from mock or real prover) to help debugging assignments. + // (either from mock or real prover) to help debugging assignments, when "mock-challenge" + // feature is enabled. + #[allow(unused_variables)] let power_of_randomness: [Expression; 31] = array::from_fn(|i| Expression::Constant(mock_randomness.pow([1 + i as u64, 0, 0, 0]))); - let challenges = Challenges::mock( + // Use the real challenges for real use, when "mock-challenge" feature is disabled. + #[cfg(not(feature = "mock-challenge"))] + let challenges = Challenges::construct(meta); + + #[cfg(feature = "mock-challenge")] + let challenges_exprs = Challenges::mock( power_of_randomness[0].clone(), power_of_randomness[0].clone(), ); + #[cfg(not(feature = "mock-challenge"))] + let challenges_exprs = challenges.exprs(meta); + let sig_table = SigTable::construct(meta); let keccak_circuit = KeccakCircuitConfig::new( meta, KeccakCircuitConfigArgs { keccak_table: keccak_table.clone(), - challenges: challenges.clone(), + challenges: challenges_exprs.clone(), }, ); @@ -156,7 +168,7 @@ impl SubCircuitConfig for SuperCircuitConfig { tx_table: tx_table.clone(), wd_table, keccak_table: keccak_table.clone(), - challenges: challenges.clone(), + challenges: challenges_exprs.clone(), }, ); let tx_circuit = TxCircuitConfig::new( @@ -164,7 +176,7 @@ impl SubCircuitConfig for SuperCircuitConfig { TxCircuitConfigArgs { tx_table: tx_table.clone(), keccak_table: keccak_table.clone(), - challenges: challenges.clone(), + challenges: challenges_exprs.clone(), }, ); let bytecode_circuit = BytecodeCircuitConfig::new( @@ -172,7 +184,7 @@ impl SubCircuitConfig for SuperCircuitConfig { BytecodeCircuitConfigArgs { bytecode_table: bytecode_table.clone(), keccak_table: keccak_table.clone(), - challenges: challenges.clone(), + challenges: challenges_exprs.clone(), }, ); let copy_circuit = CopyCircuitConfig::new( @@ -183,7 +195,7 @@ impl SubCircuitConfig for SuperCircuitConfig { bytecode_table: bytecode_table.clone(), copy_table, q_enable: q_copy_table, - challenges: challenges.clone(), + challenges: challenges_exprs.clone(), }, ); let state_circuit = StateCircuitConfig::new( @@ -194,14 +206,14 @@ impl SubCircuitConfig for SuperCircuitConfig { u8_table, u10_table, u16_table, - challenges: challenges.clone(), + challenges: challenges_exprs.clone(), }, ); let exp_circuit = ExpCircuitConfig::new(meta, exp_table); let evm_circuit = EvmCircuitConfig::new( meta, EvmCircuitConfigArgs { - challenges, + challenges: challenges_exprs, tx_table, rw_table, bytecode_table, @@ -230,6 +242,8 @@ impl SubCircuitConfig for SuperCircuitConfig { keccak_circuit, pi_circuit, exp_circuit, + #[cfg(not(feature = "mock-challenge"))] + challenges, } } } @@ -421,10 +435,14 @@ impl Circuit for SuperCircuit { mut layouter: impl Layouter, ) -> Result<(), Error> { let block = self.evm_circuit.block.as_ref().unwrap(); + #[cfg(feature = "mock-challenge")] let challenges = Challenges::mock( Value::known(block.randomness), Value::known(block.randomness), ); + #[cfg(not(feature = "mock-challenge"))] + let challenges = config.challenges.values(&mut layouter); + let rws = &self.state_circuit.rows; config.block_table.load(&mut layouter, &block.context)?; diff --git a/zkevm-circuits/src/table.rs b/zkevm-circuits/src/table.rs index fb0be4aefd..93c1d0f1e1 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::{ @@ -46,20 +46,18 @@ pub(crate) mod ux_table; /// withdrawal table pub(crate) mod wd_table; -pub(crate) use block_table::{BlockContextFieldTag, BlockTable}; -pub(crate) use bytecode_table::{BytecodeFieldTag, BytecodeTable}; -pub(crate) use copy_table::CopyTable; -pub(crate) use exp_table::ExpTable; +pub use block_table::{BlockContextFieldTag, BlockTable}; +pub use bytecode_table::{BytecodeFieldTag, BytecodeTable}; +pub use copy_table::CopyTable; +pub use exp_table::ExpTable; pub use keccak_table::KeccakTable; -pub(crate) use ux_table::UXTable; +pub use ux_table::UXTable; pub use mpt_table::{MPTProofType, MptTable}; -pub(crate) use rw_table::RwTable; -pub(crate) use sig_table::SigTable; -pub(crate) use tx_table::{ - TxContextFieldTag, TxFieldTag, TxLogFieldTag, TxReceiptFieldTag, TxTable, -}; -pub(crate) use wd_table::WdTable; +pub use rw_table::RwTable; +pub use sig_table::SigTable; +pub use tx_table::{TxContextFieldTag, TxFieldTag, TxLogFieldTag, TxReceiptFieldTag, TxTable}; +pub use wd_table::WdTable; /// Trait used to define lookup tables pub trait LookupTable { diff --git a/zkevm-circuits/src/table/copy_table.rs b/zkevm-circuits/src/table/copy_table.rs index cbd9cbbdb2..eeeb1a2eb1 100644 --- a/zkevm-circuits/src/table/copy_table.rs +++ b/zkevm-circuits/src/table/copy_table.rs @@ -1,6 +1,8 @@ use super::*; +use gadgets::binary_number::AsBits; -type CopyTableRow = [(Value, &'static str); 9]; +// The row also includes the 3 column bits from the tag +type CopyTableRow = [(Value, &'static str); 12]; type CopyCircuitRow = [(Value, &'static str); 5]; /// Copy Table, used to verify copies of byte chunks between Memory, Bytecode, @@ -34,10 +36,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 +51,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(), @@ -160,36 +164,43 @@ impl CopyTable { // is_code let is_code = Value::known(copy_step.is_code.map_or(F::ZERO, |v| F::from(v as u64))); + let tag_bits: [_; 3] = tag + .as_bits() + .map(|b| (Value::known(F::from(b as u64)), "tag_bit")); + let copy_table_row = [ + (is_first, "is_first"), + (id.lo(), "id_lo"), + (id.hi(), "id_hi"), + (addr, "addr"), + ( + Value::known(F::from(copy_event.src_addr_end)), + "src_addr_end", + ), + (Value::known(F::from(bytes_left)), "bytes_left"), + ( + match (copy_event.src_type, copy_event.dst_type) { + (CopyDataType::Memory, CopyDataType::Bytecode) => rlc_acc, + (_, CopyDataType::RlcAcc) => rlc_acc, + (CopyDataType::RlcAcc, _) => rlc_acc, + _ => Value::known(F::ZERO), + }, + "rlc_acc", + ), + ( + Value::known(F::from(copy_event.rw_counter(step_idx))), + "rw_counter", + ), + ( + Value::known(F::from(copy_event.rw_counter_increase_left(step_idx))), + "rwc_inc_left", + ), + tag_bits[0], + tag_bits[1], + tag_bits[2], + ]; assignments.push(( tag, - [ - (is_first, "is_first"), - (id.lo(), "id_lo"), - (id.hi(), "id_hi"), - (addr, "addr"), - ( - Value::known(F::from(copy_event.src_addr_end)), - "src_addr_end", - ), - (Value::known(F::from(bytes_left)), "bytes_left"), - ( - match (copy_event.src_type, copy_event.dst_type) { - (CopyDataType::Memory, CopyDataType::Bytecode) => rlc_acc, - (_, CopyDataType::RlcAcc) => rlc_acc, - (CopyDataType::RlcAcc, _) => rlc_acc, - _ => Value::known(F::ZERO), - }, - "rlc_acc", - ), - ( - Value::known(F::from(copy_event.rw_counter(step_idx))), - "rw_counter", - ), - ( - Value::known(F::from(copy_event.rw_counter_increase_left(step_idx))), - "rwc_inc_left", - ), - ], + copy_table_row, [ (is_last, "is_last"), (value, "value"), @@ -223,10 +234,9 @@ 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) { + for (_, row, _) in Self::assignments(copy_event, *challenges) { for (&column, (value, label)) in copy_table_columns.iter().zip_eq(row) { region.assign_advice( || format!("{} at row: {}", label, offset), @@ -235,7 +245,6 @@ impl CopyTable { || value, )?; } - tag_chip.assign(&mut region, offset, &tag)?; offset += 1; } } @@ -259,7 +268,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 +278,13 @@ impl LookupTable for CopyTable { self.rlc_acc.into(), self.rw_counter.into(), self.rwc_inc_left.into(), - ] + ]; + columns.extend(self.tag.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 +294,9 @@ impl LookupTable for CopyTable { String::from("rlc_acc"), String::from("rw_counter"), String::from("rwc_inc_left"), - ] + ]; + names.extend((0..self.tag.len()).map(|i| format!("tag_bit{i}"))); + names } fn table_exprs(&self, meta: &mut VirtualCells) -> Vec> { diff --git a/zkevm-circuits/src/table/mpt_table.rs b/zkevm-circuits/src/table/mpt_table.rs index 2e24e0fef7..08ae579283 100644 --- a/zkevm-circuits/src/table/mpt_table.rs +++ b/zkevm-circuits/src/table/mpt_table.rs @@ -100,7 +100,7 @@ impl LookupTable for MptTable { impl MptTable { /// Construct a new MptTable - pub(crate) fn construct(meta: &mut ConstraintSystem) -> Self { + pub fn construct(meta: &mut ConstraintSystem) -> Self { Self { address: meta.advice_column(), storage_key: WordLoHi::new([meta.advice_column(), meta.advice_column()]), diff --git a/zkevm-circuits/src/util.rs b/zkevm-circuits/src/util.rs index e8da067cff..b0d8d0449f 100644 --- a/zkevm-circuits/src/util.rs +++ b/zkevm-circuits/src/util.rs @@ -92,7 +92,9 @@ impl Challenges { [&self.keccak_input, &self.lookup_input] } - pub(crate) fn mock(keccak_input: T, lookup_input: T) -> Self { + /// Returns a mock Challenges for testing purposes + #[cfg(feature = "mock-challenge")] + pub fn mock(keccak_input: T, lookup_input: T) -> Self { Self { keccak_input, lookup_input,