From 0d14709b8edc70a9f1a86210cf04bcc0863c217d Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 18:01:41 +0800 Subject: [PATCH 01/22] halo2_proofs/Cargo.toml: Introduce "unstable-dynamic-lookups" flag --- halo2_proofs/Cargo.toml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/halo2_proofs/Cargo.toml b/halo2_proofs/Cargo.toml index f82e03a5..86222f36 100644 --- a/halo2_proofs/Cargo.toml +++ b/halo2_proofs/Cargo.toml @@ -89,7 +89,9 @@ beta = [ ] nightly = [ "beta", + "unstable-dynamic-lookups", ] +unstable-dynamic-lookups = [] # Add flags for in-development features above this line. [lib] From 77b18df0892e10438163a8d599c68499107a3a40 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 22 Feb 2023 00:53:24 +0800 Subject: [PATCH 02/22] plonk::circuit: DynamicTable, TableTag Co-authored-by: Avi Dessauer --- halo2_proofs/src/plonk/circuit.rs | 51 +++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index fb6a8b56..4b2a2749 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -268,6 +268,17 @@ impl Selector { } } +/// A dynamic table tag +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct TableTag(pub(crate) usize); + +impl TableTag { + /// The value of a table tag is the table's `index` + 1 + fn value(&self) -> u64 { + self.0 as u64 + 1 + } +} + /// Query of fixed column at a certain relative location #[derive(Copy, Clone, Debug)] pub struct FixedQuery { @@ -334,6 +345,36 @@ impl TableColumn { } } +/// `DynamicTable` is used to track the columns and rows comprise a dynamic lookup table. +/// `DynamicTable`s are constructed in the configuration phase by `create_dynamic_table`. +/// To include a row of a region in a dynamic table use `add_row_to_table` during synthesize. +#[cfg_attr( + feature = "unstable-dynamic-lookups", + derive(Clone, Debug, Eq, PartialEq, Hash) +)] +#[cfg(feature = "unstable-dynamic-lookups")] +pub struct DynamicTable { + pub(crate) name: String, + pub(crate) index: usize, + /// Columns contained in this table, excluding the tag column. + pub(crate) columns: Vec>, +} + +#[cfg(feature = "unstable-dynamic-lookups")] +impl DynamicTable { + pub(crate) fn index(&self) -> usize { + self.index + } + + pub(crate) fn tag(&self) -> TableTag { + TableTag(self.index) + } + + pub(crate) fn columns(&self) -> &[Column] { + &self.columns + } +} + /// This trait allows a [`Circuit`] to direct some backend to assign a witness /// for a constraint system. pub trait Assignment { @@ -941,6 +982,12 @@ pub struct ConstraintSystem { /// fixed column that they were compressed into. This is just used by dev /// tooling right now. pub(crate) selector_map: Vec>, + /// Like selector_map, but for dynamic tables. + #[cfg(feature = "unstable-dynamic-lookups")] + pub(crate) dynamic_table_tag_map: Vec>, + + #[cfg(feature = "unstable-dynamic-lookups")] + pub(crate) dynamic_tables: Vec, pub(crate) gates: Vec>, pub(crate) advice_queries: Vec<(Column, Rotation)>, @@ -1001,6 +1048,10 @@ impl Default for ConstraintSystem { num_instance_columns: 0, num_selectors: 0, selector_map: vec![], + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_table_tag_map: vec![], + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables: vec![], gates: vec![], fixed_queries: Vec::new(), advice_queries: Vec::new(), From 78ea483f650879d9a520237746faec26377794a3 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 22 Feb 2023 01:00:52 +0800 Subject: [PATCH 03/22] circuit::layouter::RegionColumn: Introduce TableTag variant Co-authored-by: Avi Dessauer --- halo2_proofs/src/circuit/layouter.rs | 22 ++++++++++++++++++++-- halo2_proofs/src/dev/graph/layout.rs | 2 ++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index 81fa00be..3e3e87b0 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -8,6 +8,8 @@ use ff::Field; pub use super::table_layouter::TableLayouter; use super::{Cell, RegionIndex, Value}; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::TableTag; use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector}; /// Helper trait for implementing a custom [`Layouter`]. @@ -15,7 +17,7 @@ use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Select /// This trait is used for implementing region assignments: /// /// ```ignore -/// impl<'a, F: FieldExt, C: Chip, CS: Assignment + 'a> Layouter for MyLayouter<'a, C, CS> { +/// impl<'a, F: Field, C: Chip, CS: Assignment + 'a> Layouter for MyLayouter<'a, C, CS> { /// fn assign_region( /// &mut self, /// assignment: impl FnOnce(Region<'_, F, C>) -> Result<(), Error>, @@ -127,6 +129,9 @@ pub enum RegionColumn { Column(Column), /// Virtual column representing a (boolean) selector Selector(Selector), + /// Virtual column used for storing dynamic table tags + #[cfg(feature = "unstable-dynamic-lookups")] + TableTag(TableTag), } impl From> for RegionColumn { @@ -141,13 +146,26 @@ impl From for RegionColumn { } } +#[cfg(feature = "unstable-dynamic-lookups")] +impl From for RegionColumn { + fn from(table_tag: TableTag) -> RegionColumn { + RegionColumn::TableTag(table_tag) + } +} + impl Ord for RegionColumn { fn cmp(&self, other: &Self) -> cmp::Ordering { match (self, other) { (Self::Column(ref a), Self::Column(ref b)) => a.cmp(b), (Self::Selector(ref a), Self::Selector(ref b)) => a.0.cmp(&b.0), - (Self::Column(_), Self::Selector(_)) => cmp::Ordering::Less, + #[cfg(feature = "unstable-dynamic-lookups")] + (Self::TableTag(ref a), Self::TableTag(ref b)) => a.0.cmp(&b.0), + (Self::Column(_), _) => cmp::Ordering::Less, (Self::Selector(_), Self::Column(_)) => cmp::Ordering::Greater, + #[cfg(feature = "unstable-dynamic-lookups")] + (Self::TableTag(_), _) => cmp::Ordering::Greater, + #[cfg(feature = "unstable-dynamic-lookups")] + (_, Self::TableTag(_)) => cmp::Ordering::Less, } } } diff --git a/halo2_proofs/src/dev/graph/layout.rs b/halo2_proofs/src/dev/graph/layout.rs index 965e0683..90979aa4 100644 --- a/halo2_proofs/src/dev/graph/layout.rs +++ b/halo2_proofs/src/dev/graph/layout.rs @@ -113,6 +113,8 @@ impl CircuitLayout { let column: Column = match column { RegionColumn::Column(col) => col, RegionColumn::Selector(selector) => cs.selector_map[selector.0].into(), + #[cfg(feature = "unstable-dynamic-lookups")] + RegionColumn::TableTag(tag_col) => cs.dynamic_table_tag_map[tag_col.0].into(), }; column.index() + match column.column_type() { From be3d62f9304ce26380a00f27cc2b12643a807ea2 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 22 Feb 2023 01:37:35 +0800 Subject: [PATCH 04/22] plonk::circuit::Expression: Introduce TableTag variant Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev.rs | 4 +++ halo2_proofs/src/dev/failure.rs | 6 ++++ halo2_proofs/src/dev/failure/emitter.rs | 2 ++ halo2_proofs/src/dev/gates.rs | 9 +++++- halo2_proofs/src/dev/util.rs | 2 ++ halo2_proofs/src/plonk/circuit.rs | 28 +++++++++++++++++++ .../src/plonk/circuit/compress_selectors.rs | 2 ++ halo2_proofs/src/plonk/lookup/prover.rs | 4 +++ halo2_proofs/src/plonk/lookup/verifier.rs | 2 ++ halo2_proofs/src/plonk/prover.rs | 2 ++ halo2_proofs/src/plonk/verifier.rs | 2 ++ 11 files changed, 62 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index a292b0ab..73a949c9 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -648,6 +648,8 @@ impl MockProver { move |(poly_index, poly)| match poly.evaluate( &|scalar| Value::Real(scalar), &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &util::load(n, row, &self.cs.fixed_queries, &self.fixed), &util::load(n, row, &self.cs.advice_queries, &self.advice), &util::load_instance( @@ -712,6 +714,8 @@ impl MockProver { expression.evaluate( &|scalar| Value::Real(scalar), &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| { let query = self.cs.fixed_queries[query.index]; let column_index = query.0.index(); diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index c6c5aecf..948316ea 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -56,6 +56,8 @@ impl FailureLocation { expression.evaluate( &|_| vec![], &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| vec![cs.fixed_queries[query.index].0.into()], &|query| vec![cs.advice_queries[query.index].0.into()], &|query| vec![cs.instance_queries[query.index].0.into()], @@ -417,6 +419,8 @@ fn render_lookup( expr.evaluate( &|_| panic!("no constants in table expressions"), &|_| panic!("no selectors in table expressions"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("no virtual columns in table expressions"), &|query| format!("F{}", query.column_index), &|_| panic!("no advice columns in table expressions"), &|_| panic!("no instance columns in table expressions"), @@ -467,6 +471,8 @@ fn render_lookup( let cell_values = input.evaluate( &|_| BTreeMap::default(), &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &cell_value( Any::Fixed, &util::load(n, row, &cs.fixed_queries, &prover.fixed), diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 071dca6f..9b9ef8d2 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -103,6 +103,8 @@ pub(super) fn expression_to_string( expr.evaluate( &util::format_value, &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| { if let Some(label) = layout .get(&query.rotation.0) diff --git a/halo2_proofs/src/dev/gates.rs b/halo2_proofs/src/dev/gates.rs index fc624e96..36def567 100644 --- a/halo2_proofs/src/dev/gates.rs +++ b/halo2_proofs/src/dev/gates.rs @@ -1,6 +1,7 @@ use std::{ collections::BTreeSet, fmt::{self, Write}, + iter, }; use ff::PrimeField; @@ -119,6 +120,8 @@ impl CircuitGates { expression: constraint.evaluate( &util::format_value, &|selector| format!("S{}", selector.0), + #[cfg(feature = "unstable-dynamic-lookups")] + &|table_tag| format!("T{}", table_tag.0), &|query| format!("F{}@{}", query.column_index, query.rotation.0), &|query| format!("A{}@{}", query.column_index, query.rotation.0), &|query| format!("I{}@{}", query.column_index, query.rotation.0), @@ -152,7 +155,9 @@ impl CircuitGates { ), queries: constraint.evaluate( &|_| BTreeSet::default(), - &|selector| vec![format!("S{}", selector.0)].into_iter().collect(), + &|selector| iter::once(format!("S{}", selector.0)).collect(), + #[cfg(feature = "unstable-dynamic-lookups")] + &|table_tag| iter::once(format!("V{}", table_tag.0)).collect(), &|query| { vec![format!("F{}@{}", query.column_index, query.rotation.0)] .into_iter() @@ -192,6 +197,8 @@ impl CircuitGates { poly.evaluate( &|_| (0, 0, 0), &|_| (0, 0, 0), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| (0, 0, 0), &|_| (0, 0, 0), &|_| (0, 0, 0), &|_| (0, 0, 0), diff --git a/halo2_proofs/src/dev/util.rs b/halo2_proofs/src/dev/util.rs index ee3b7cb1..82feec4c 100644 --- a/halo2_proofs/src/dev/util.rs +++ b/halo2_proofs/src/dev/util.rs @@ -143,6 +143,8 @@ pub(super) fn cell_values<'a, F: Field>( let cell_values = poly.evaluate( &|_| BTreeMap::default(), &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &cell_value(virtual_cells, load_fixed), &cell_value(virtual_cells, load_advice), &cell_value(virtual_cells, load_instance), diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 4b2a2749..f3fdd906 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -532,6 +532,9 @@ pub enum Expression { Constant(F), /// This is a virtual selector Selector(Selector), + /// A placeholder which will be resolved as a fixed column during optimization. + #[cfg(feature = "unstable-dynamic-lookups")] + TableTag(TableTag), /// This is a fixed column queried at a certain relative location Fixed(FixedQuery), /// This is an advice (witness) column queried at a certain relative location @@ -556,6 +559,7 @@ impl Expression { &self, constant: &impl Fn(F) -> T, selector_column: &impl Fn(Selector) -> T, + #[cfg(feature = "unstable-dynamic-lookups")] table_tag: &impl Fn(TableTag) -> T, fixed_column: &impl Fn(FixedQuery) -> T, advice_column: &impl Fn(AdviceQuery) -> T, instance_column: &impl Fn(InstanceQuery) -> T, @@ -567,6 +571,8 @@ impl Expression { match self { Expression::Constant(scalar) => constant(*scalar), Expression::Selector(selector) => selector_column(*selector), + #[cfg(feature = "unstable-dynamic-lookups")] + Expression::TableTag(tag) => table_tag(*tag), Expression::Fixed(query) => fixed_column(*query), Expression::Advice(query) => advice_column(*query), Expression::Instance(query) => instance_column(*query), @@ -574,6 +580,8 @@ impl Expression { let a = a.evaluate( constant, selector_column, + #[cfg(feature = "unstable-dynamic-lookups")] + table_tag, fixed_column, advice_column, instance_column, @@ -588,6 +596,8 @@ impl Expression { let a = a.evaluate( constant, selector_column, + #[cfg(feature = "unstable-dynamic-lookups")] + table_tag, fixed_column, advice_column, instance_column, @@ -599,6 +609,8 @@ impl Expression { let b = b.evaluate( constant, selector_column, + #[cfg(feature = "unstable-dynamic-lookups")] + table_tag, fixed_column, advice_column, instance_column, @@ -613,6 +625,8 @@ impl Expression { let a = a.evaluate( constant, selector_column, + #[cfg(feature = "unstable-dynamic-lookups")] + table_tag, fixed_column, advice_column, instance_column, @@ -624,6 +638,8 @@ impl Expression { let b = b.evaluate( constant, selector_column, + #[cfg(feature = "unstable-dynamic-lookups")] + table_tag, fixed_column, advice_column, instance_column, @@ -638,6 +654,8 @@ impl Expression { let a = a.evaluate( constant, selector_column, + #[cfg(feature = "unstable-dynamic-lookups")] + table_tag, fixed_column, advice_column, instance_column, @@ -656,6 +674,8 @@ impl Expression { match self { Expression::Constant(_) => 0, Expression::Selector(_) => 1, + #[cfg(feature = "unstable-dynamic-lookups")] + Expression::TableTag(_) => 1, Expression::Fixed { .. } => 1, Expression::Advice { .. } => 1, Expression::Instance { .. } => 1, @@ -676,6 +696,8 @@ impl Expression { self.evaluate( &|_| false, &|selector| selector.is_simple(), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| false, &|_| false, &|_| false, &|_| false, @@ -703,6 +725,8 @@ impl Expression { None } }, + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| None, &|_| None, &|_| None, &|_| None, @@ -719,6 +743,8 @@ impl std::fmt::Debug for Expression { match self { Expression::Constant(scalar) => f.debug_tuple("Constant").field(scalar).finish(), Expression::Selector(selector) => f.debug_tuple("Selector").field(selector).finish(), + #[cfg(feature = "unstable-dynamic-lookups")] + Expression::TableTag(tag) => f.debug_tuple("TableTag").field(tag).finish(), // Skip enum variant and print query struct directly to maintain backwards compatibility. Expression::Fixed(FixedQuery { index, @@ -1364,6 +1390,8 @@ impl ConstraintSystem { selector_replacements[selector.0].clone() }, + #[cfg(feature = "unstable-dynamic-lookups")] + &|query| Expression::TableTag(query), &|query| Expression::Fixed(query), &|query| Expression::Advice(query), &|query| Expression::Instance(query), diff --git a/halo2_proofs/src/plonk/circuit/compress_selectors.rs b/halo2_proofs/src/plonk/circuit/compress_selectors.rs index 01cca9bc..523df172 100644 --- a/halo2_proofs/src/plonk/circuit/compress_selectors.rs +++ b/halo2_proofs/src/plonk/circuit/compress_selectors.rs @@ -318,6 +318,8 @@ mod tests { let eval = selector.expression.evaluate( &|c| c, &|_| panic!("should not occur in returned expressions"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("should not occur in returned expressions"), &|query| { // Should be the correct combination in the expression assert_eq!(selector.combination_index, query.index); diff --git a/halo2_proofs/src/plonk/lookup/prover.rs b/halo2_proofs/src/plonk/lookup/prover.rs index a6ad4a62..164c6b79 100644 --- a/halo2_proofs/src/plonk/lookup/prover.rs +++ b/halo2_proofs/src/plonk/lookup/prover.rs @@ -111,6 +111,8 @@ impl> Argument { expression.evaluate( &|scalar| poly::Ast::ConstantTerm(scalar), &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| { fixed_values[query.column_index] .with_rotation(query.rotation) @@ -140,6 +142,8 @@ impl> Argument { expression.evaluate( &|scalar| poly::Ast::ConstantTerm(scalar), &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| { fixed_cosets[query.column_index] .with_rotation(query.rotation) diff --git a/halo2_proofs/src/plonk/lookup/verifier.rs b/halo2_proofs/src/plonk/lookup/verifier.rs index 0e066549..613c3f9a 100644 --- a/halo2_proofs/src/plonk/lookup/verifier.rs +++ b/halo2_proofs/src/plonk/lookup/verifier.rs @@ -120,6 +120,8 @@ impl Evaluated { expression.evaluate( &|scalar| scalar, &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| fixed_evals[query.index], &|query| advice_evals[query.index], &|query| instance_evals[query.index], diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index e54f2129..fbfdff49 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -555,6 +555,8 @@ pub fn create_proof< expr.evaluate( &poly::Ast::ConstantTerm, &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| { fixed_cosets[query.column_index] .with_rotation(query.rotation) diff --git a/halo2_proofs/src/plonk/verifier.rs b/halo2_proofs/src/plonk/verifier.rs index f141ebaf..d6cbda1d 100644 --- a/halo2_proofs/src/plonk/verifier.rs +++ b/halo2_proofs/src/plonk/verifier.rs @@ -231,6 +231,8 @@ pub fn verify_proof< poly.evaluate( &|scalar| scalar, &|_| panic!("virtual selectors are removed during optimization"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("virtual table tags are removed during optimization"), &|query| fixed_evals[query.index], &|query| advice_evals[query.index], &|query| instance_evals[query.index], From fc71bba6ba53f2f336810f0414b98e1569aa74fb Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 22 Feb 2023 02:08:17 +0800 Subject: [PATCH 05/22] plonk::circuit::Assignment: Introduce add_to_lookup() method Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev.rs | 22 +++++++++++++++ halo2_proofs/src/dev/cost.rs | 40 ++++++++++++++++++++++++++-- halo2_proofs/src/dev/graph.rs | 7 +++++ halo2_proofs/src/dev/graph/layout.rs | 8 +++++- halo2_proofs/src/dev/tfp.rs | 9 +++++++ halo2_proofs/src/plonk/circuit.rs | 5 +++- halo2_proofs/src/plonk/keygen.rs | 20 ++++++++++++++ halo2_proofs/src/plonk/prover.rs | 9 +++++++ 8 files changed, 116 insertions(+), 4 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index 73a949c9..9569b2e4 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -8,6 +8,8 @@ use std::ops::{Add, Mul, Neg, Range}; use ff::Field; use crate::plonk::Assigned; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::TableTag; use crate::{ circuit, plonk::{ @@ -288,6 +290,9 @@ pub struct MockProver { instance: Vec>>, selectors: Vec>, + /// A map between DynamicTable.index, and rows included. + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables: Vec>, permutation: permutation::keygen::Assembly, @@ -354,6 +359,19 @@ impl Assignment for MockProver { Ok(()) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, row: usize) -> Result<(), Error> { + self.dynamic_tables[table.0][row] = true; + + if let Some(region) = self.current_region.as_mut() { + for column in self.cs.dynamic_tables[table.0].columns.iter() { + region.update_extent(*column, row); + } + } + + Ok(()) + } + fn query_instance( &self, column: Column, @@ -520,6 +538,8 @@ impl MockProver { // Fixed columns contain no blinding factors. let fixed = vec![vec![CellValue::Unassigned; n]; cs.num_fixed_columns]; let selectors = vec![vec![false; n]; cs.num_selectors]; + #[cfg(feature = "unstable-dynamic-lookups")] + let dynamic_tables = vec![vec![false; n]; cs.dynamic_tables.len()]; // Advice columns contain blinding factors. let blinding_factors = cs.blinding_factors(); let usable_rows = n - (blinding_factors + 1); @@ -547,6 +567,8 @@ impl MockProver { advice, instance, selectors, + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables, permutation, usable_rows: 0..usable_rows, }; diff --git a/halo2_proofs/src/dev/cost.rs b/halo2_proofs/src/dev/cost.rs index 0c3c7efa..5c506515 100644 --- a/halo2_proofs/src/dev/cost.rs +++ b/halo2_proofs/src/dev/cost.rs @@ -11,6 +11,8 @@ use std::{ use ff::{Field, PrimeField}; use group::prime::PrimeGroup; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::{DynamicTable, TableTag}; use crate::{ circuit::{layouter::RegionColumn, Value}, plonk::{ @@ -90,11 +92,21 @@ pub(crate) struct Layout { pub(crate) equality: Vec<(Column, usize, Column, usize)>, /// Selector assignments used for optimization pass pub(crate) selectors: Vec>, + /// A map between DynamicTable.index, and rows included. + #[cfg(feature = "unstable-dynamic-lookups")] + pub(crate) dynamic_tables_assignments: Vec>, + #[cfg(feature = "unstable-dynamic-lookups")] + pub(crate) dynamic_tables: Vec, } impl Layout { /// Creates a empty layout - pub fn new(k: u32, n: usize, num_selectors: usize) -> Self { + pub fn new( + k: u32, + n: usize, + num_selectors: usize, + #[cfg(feature = "unstable-dynamic-lookups")] dynamic_tables: Vec, + ) -> Self { Layout { k, regions: vec![], @@ -108,6 +120,10 @@ impl Layout { equality: vec![], /// Selector assignments used for optimization pass selectors: vec![vec![false; n]; num_selectors], + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables_assignments: vec![vec![false; n]; dynamic_tables.len()], + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables, } } @@ -183,6 +199,20 @@ impl Assignment for Layout { Ok(()) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, row: usize) -> Result<(), Error> { + self.dynamic_tables_assignments[table.0][row] = true; + + for col_index in 0..self.dynamic_tables[table.0].columns.len() { + self.update( + (self.dynamic_tables[table.0].columns[col_index]).into(), + row, + ); + } + + Ok(()) + } + fn query_instance(&self, _: Column, _: usize) -> Result, Error> { Ok(Value::unknown()) } @@ -262,7 +292,13 @@ impl> CircuitCost Assignment for Graph { Ok(()) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, _: TableTag, _: usize) -> Result<(), Error> { + Ok(()) + } + fn query_instance(&self, _: Column, _: usize) -> Result, Error> { Ok(Value::unknown()) } diff --git a/halo2_proofs/src/dev/graph/layout.rs b/halo2_proofs/src/dev/graph/layout.rs index 90979aa4..05d60244 100644 --- a/halo2_proofs/src/dev/graph/layout.rs +++ b/halo2_proofs/src/dev/graph/layout.rs @@ -95,7 +95,13 @@ impl CircuitLayout { // Collect the layout details. let mut cs = ConstraintSystem::default(); let config = ConcreteCircuit::configure(&mut cs); - let mut layout = Layout::new(k, n, cs.num_selectors); + let mut layout = Layout::new( + k, + n, + cs.num_selectors, + #[cfg(feature = "unstable-dynamic-lookups")] + cs.dynamic_tables.clone(), + ); ConcreteCircuit::FloorPlanner::synthesize( &mut layout, circuit, diff --git a/halo2_proofs/src/dev/tfp.rs b/halo2_proofs/src/dev/tfp.rs index 7a8d9df5..77d4657d 100644 --- a/halo2_proofs/src/dev/tfp.rs +++ b/halo2_proofs/src/dev/tfp.rs @@ -3,6 +3,8 @@ use std::{fmt, marker::PhantomData}; use ff::Field; use tracing::{debug, debug_span, span::EnteredSpan}; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::TableTag; use crate::{ circuit::{layouter::RegionLayouter, AssignedCell, Cell, Layouter, Region, Table, Value}, plonk::{ @@ -383,6 +385,13 @@ impl<'cs, F: Field, CS: Assignment> Assignment for TracingAssignment<'cs, self.cs.enable_selector(|| annotation, selector, row) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, row: usize) -> Result<(), Error> { + let _guard = debug_span!("positioned").entered(); + debug!(target: "add_to_lookup", table = ?table, row = row); + self.cs.add_to_lookup(table, row) + } + fn query_instance(&self, column: Column, row: usize) -> Result, Error> { let _guard = debug_span!("positioned").entered(); debug!(target: "query_instance", column = ?column, row = row); diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index f3fdd906..6e1277b7 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -345,7 +345,6 @@ impl TableColumn { } } -/// `DynamicTable` is used to track the columns and rows comprise a dynamic lookup table. /// `DynamicTable`s are constructed in the configuration phase by `create_dynamic_table`. /// To include a row of a region in a dynamic table use `add_row_to_table` during synthesize. #[cfg_attr( @@ -410,6 +409,10 @@ pub trait Assignment { A: FnOnce() -> AR, AR: Into; + /// Adds a row in the provided dynamic lookup table. + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, row: usize) -> Result<(), Error>; + /// Queries the cell of an instance column at a particular absolute row. /// /// Returns the cell's value, if known. diff --git a/halo2_proofs/src/plonk/keygen.rs b/halo2_proofs/src/plonk/keygen.rs index bb26d5a6..e3ec0fbc 100644 --- a/halo2_proofs/src/plonk/keygen.rs +++ b/halo2_proofs/src/plonk/keygen.rs @@ -5,6 +5,8 @@ use std::ops::Range; use ff::{Field, FromUniformBytes}; use group::Curve; +#[cfg(feature = "unstable-dynamic-lookups")] +use super::TableTag; use super::{ circuit::{ Advice, Any, Assignment, Circuit, Column, ConstraintSystem, Fixed, FloorPlanner, Instance, @@ -50,6 +52,9 @@ struct Assembly { fixed: Vec, LagrangeCoeff>>, permutation: permutation::keygen::Assembly, selectors: Vec>, + /// A map between DynamicTable.index, and rows included. + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables: Vec>, // A range of available rows for assignment and copies. usable_rows: Range, _marker: std::marker::PhantomData, @@ -82,6 +87,17 @@ impl Assignment for Assembly { Ok(()) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, row: usize) -> Result<(), Error> { + if !self.usable_rows.contains(&row) { + return Err(Error::not_enough_rows_available(self.k)); + } + + self.dynamic_tables[table.0][row] = true; + + Ok(()) + } + fn query_instance(&self, _: Column, row: usize) -> Result, Error> { if !self.usable_rows.contains(&row) { return Err(Error::not_enough_rows_available(self.k)); @@ -206,6 +222,8 @@ where fixed: vec![domain.empty_lagrange_assigned(); cs.num_fixed_columns], permutation: permutation::keygen::Assembly::new(params.n as usize, &cs.permutation), selectors: vec![vec![false; params.n as usize]; cs.num_selectors], + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables: vec![vec![false; params.n as usize]; cs.dynamic_tables.len()], usable_rows: 0..params.n as usize - (cs.blinding_factors() + 1), _marker: std::marker::PhantomData, }; @@ -267,6 +285,8 @@ where fixed: vec![vk.domain.empty_lagrange_assigned(); cs.num_fixed_columns], permutation: permutation::keygen::Assembly::new(params.n as usize, &cs.permutation), selectors: vec![vec![false; params.n as usize]; cs.num_selectors], + #[cfg(feature = "unstable-dynamic-lookups")] + dynamic_tables: vec![vec![false; params.n as usize]; cs.dynamic_tables.len()], usable_rows: 0..params.n as usize - (cs.blinding_factors() + 1), _marker: std::marker::PhantomData, }; diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index fbfdff49..eb366b9b 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -4,6 +4,8 @@ use rand_core::RngCore; use std::iter; use std::ops::RangeTo; +#[cfg(feature = "unstable-dynamic-lookups")] +use super::TableTag; use super::{ circuit::{ Advice, Any, Assignment, Circuit, Column, ConstraintSystem, Fixed, FloorPlanner, Instance, @@ -172,6 +174,13 @@ pub fn create_proof< Ok(()) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, _: TableTag, _: usize) -> Result<(), Error> { + // We only care about advice columns here + + Ok(()) + } + fn query_instance( &self, column: Column, From 07655b9e7bfa3d69ee6072f6d91a072338c33ab0 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 22 Feb 2023 02:16:23 +0800 Subject: [PATCH 06/22] circuit::layouter::RegionLayouter: Introduce add_to_lookup() method Co-authored-by: Avi Dessauer --- halo2_proofs/src/circuit.rs | 8 ++++++++ .../src/circuit/floor_planner/single_pass.rs | 9 +++++++++ halo2_proofs/src/circuit/floor_planner/v1.rs | 7 +++++++ halo2_proofs/src/circuit/layouter.rs | 12 ++++++++++++ halo2_proofs/src/dev/tfp.rs | 6 ++++++ 5 files changed, 42 insertions(+) diff --git a/halo2_proofs/src/circuit.rs b/halo2_proofs/src/circuit.rs index 0822d8d8..9ad20b94 100644 --- a/halo2_proofs/src/circuit.rs +++ b/halo2_proofs/src/circuit.rs @@ -4,6 +4,8 @@ use std::{fmt, marker::PhantomData}; use ff::Field; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::TableTag; use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn}; mod value; @@ -204,6 +206,12 @@ impl<'r, F: Field> Region<'r, F> { .enable_selector(&|| annotation().into(), selector, offset) } + /// Enables a dynamic table lookup at the given offset. + #[cfg(feature = "unstable-dynamic-lookups")] + pub fn add_to_lookup(&mut self, table: TableTag, offset: usize) -> Result<(), Error> { + self.region.add_to_lookup(table, offset) + } + /// Assign an advice column value (witness). /// /// Even though `to` has `FnMut` bounds, it is guaranteed to be called at most once. diff --git a/halo2_proofs/src/circuit/floor_planner/single_pass.rs b/halo2_proofs/src/circuit/floor_planner/single_pass.rs index 968c3726..8e2c63d6 100644 --- a/halo2_proofs/src/circuit/floor_planner/single_pass.rs +++ b/halo2_proofs/src/circuit/floor_planner/single_pass.rs @@ -5,6 +5,8 @@ use std::marker::PhantomData; use ff::Field; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::TableTag; use crate::{ circuit::{ layouter::{RegionColumn, RegionLayouter, RegionShape}, @@ -259,6 +261,13 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter ) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, offset: usize) -> Result<(), Error> { + self.layouter + .cs + .add_to_lookup(table, *self.layouter.regions[*self.region_index] + offset) + } + fn assign_advice<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), diff --git a/halo2_proofs/src/circuit/floor_planner/v1.rs b/halo2_proofs/src/circuit/floor_planner/v1.rs index 42f197ca..2a54c3dc 100644 --- a/halo2_proofs/src/circuit/floor_planner/v1.rs +++ b/halo2_proofs/src/circuit/floor_planner/v1.rs @@ -374,6 +374,13 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter for V1Region<'r ) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: crate::plonk::TableTag, offset: usize) -> Result<(), Error> { + self.plan + .cs + .add_to_lookup(table, *self.plan.regions[*self.region_index] + offset) + } + fn assign_advice<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index 3e3e87b0..e36839f8 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -51,6 +51,10 @@ pub trait RegionLayouter: fmt::Debug { offset: usize, ) -> Result<(), Error>; + /// Enables a dynamic table lookup at the given offset. + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, offset: usize) -> Result<(), Error>; + /// Assign an advice column value (witness) fn assign_advice<'v>( &'v mut self, @@ -215,6 +219,14 @@ impl RegionLayouter for RegionShape { Ok(()) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, offset: usize) -> Result<(), Error> { + // Track the tag's fixed column as part of the region's shape. + self.columns.insert(table.into()); + self.row_count = cmp::max(self.row_count, offset + 1); + Ok(()) + } + fn assign_advice<'v>( &'v mut self, _: &'v (dyn Fn() -> String + 'v), diff --git a/halo2_proofs/src/dev/tfp.rs b/halo2_proofs/src/dev/tfp.rs index 77d4657d..31cdeb7c 100644 --- a/halo2_proofs/src/dev/tfp.rs +++ b/halo2_proofs/src/dev/tfp.rs @@ -236,6 +236,12 @@ impl<'r, F: Field> RegionLayouter for TracingRegion<'r, F> { self.0.enable_selector(annotation, selector, offset) } + #[cfg(feature = "unstable-dynamic-lookups")] + fn add_to_lookup(&mut self, table: TableTag, offset: usize) -> Result<(), Error> { + debug!(target: "add_to_lookup", table = ?table, offset = ?offset); + self.0.add_to_lookup(table, offset) + } + fn assign_advice<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), From e713366c3e6c1bdf5ce7628b254d470202db08a8 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:18:04 +0800 Subject: [PATCH 07/22] circuit::Region: Implement add_to_lookup() Co-authored-by: Avi Dessauer --- halo2_proofs/src/plonk/circuit.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 6e1277b7..41cb15cf 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -372,6 +372,14 @@ impl DynamicTable { pub(crate) fn columns(&self) -> &[Column] { &self.columns } + + /// Includes a row at `offset` in this dynamic lookup table. + pub fn add_row(&self, region: &mut Region, offset: usize) -> Result<(), Error> + where + F: Field, + { + region.add_to_lookup(self.tag(), offset) + } } /// This trait allows a [`Circuit`] to direct some backend to assign a witness From 8c2f2b18b2355e23957aa3aa2cc1fc854ccf0a07 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:26:43 +0800 Subject: [PATCH 08/22] plonk::circuit::ConstraintSystem: lookup_dynamic(), create_dynamic_table() Co-authored-by: Avi Dessauer --- halo2_proofs/src/plonk/circuit.rs | 91 +++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 41cb15cf..49b828df 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1,6 +1,8 @@ use core::cmp::max; use core::ops::{Add, Mul}; use ff::Field; +#[cfg(feature = "unstable-dynamic-lookups")] +use ff::PrimeField; use std::{ convert::TryFrom, ops::{Neg, Sub}, @@ -1171,6 +1173,69 @@ impl ConstraintSystem { index } + /// Add a dynamic lookup argument for some input expressions and table columns. + /// + /// `table_map` returns a map between input expressions and the table columns + /// they need to match. + /// + /// `table` must contain all table columns used in table_map. + #[cfg(feature = "unstable-dynamic-lookups")] + pub fn lookup_dynamic( + &mut self, + table: &DynamicTable, + table_map: impl FnOnce( + &mut VirtualCells<'_, F>, + ) -> (Selector, Vec<(Expression, Column)>), + ) -> usize + where + F: PrimeField, + { + let mut cells = VirtualCells::new(self); + let (selector, table_map) = table_map(&mut cells); + let selector = cells.query_selector(selector); + + let non_table_columns: Vec<_> = table_map + .iter() + .map(|(_, c)| c) + .filter(|col| !table.columns.contains(col)) + .collect(); + if !non_table_columns.is_empty() { + panic!( + "{:?} does not contain {:?}. Try adding these columns to the dynamic table.", + table, + non_table_columns.as_slice() + ); + } + + let mut table_map: Vec<_> = table_map + .into_iter() + .map(|(input, table)| { + if selector.contains_simple_selector() { + panic!("selector expression containing simple selector supplied to lookup argument"); + } + + // TODO is this needed + if input.contains_simple_selector() { + panic!("input expression containing simple selector supplied to lookup argument"); + } + + let table_query = cells.query_any(table, Rotation::cur()); + (selector.clone() * input, selector.clone() * table_query) + }) + .collect(); + + table_map.push(( + selector.clone() * Expression::Constant(F::from(table.tag().value())), + selector * Expression::TableTag(table.tag()), + )); + + let index = self.lookups.len(); + + self.lookups.push(lookup::Argument::new(table_map)); + + index + } + fn query_fixed_index(&mut self, column: Column) -> usize { // Return existing query, if it exists for (index, fixed_query) in self.fixed_queries.iter().enumerate() { @@ -1450,6 +1515,32 @@ impl ConstraintSystem { Selector(index, false) } + /// Construct a dynamic table consisting of fixed, and advice. + /// `name` is solely for debugging. + #[cfg(feature = "unstable-dynamic-lookups")] + pub fn create_dynamic_table( + &mut self, + name: impl Into, + fixed_columns: &[Column], + advice_columns: &[Column], + ) -> DynamicTable { + let index = self.dynamic_tables.len(); + let columns: Vec<_> = fixed_columns + .iter() + .map(|f| Column::::from(*f)) + .chain(advice_columns.iter().map(|f| Column::::from(*f))) + .collect(); + + let table = DynamicTable { + name: name.into(), + index, + columns, + }; + + self.dynamic_tables.push(table.clone()); + table + } + /// Allocates a new fixed column that can be used in a lookup table. pub fn lookup_table_column(&mut self) -> TableColumn { TableColumn { From 1c9424d16680915e21ce62268f593bab1f3e2fc9 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:34:54 +0800 Subject: [PATCH 09/22] circuit::compress_selectors: Extract exclusion_matrix() method Co-authored-by: Avi Dessauer --- .../src/plonk/circuit/compress_selectors.rs | 57 ++++++++++--------- 1 file changed, 31 insertions(+), 26 deletions(-) diff --git a/halo2_proofs/src/plonk/circuit/compress_selectors.rs b/halo2_proofs/src/plonk/circuit/compress_selectors.rs index 523df172..6b8f9e77 100644 --- a/halo2_proofs/src/plonk/circuit/compress_selectors.rs +++ b/halo2_proofs/src/plonk/circuit/compress_selectors.rs @@ -96,32 +96,8 @@ where }); // All of the remaining `selectors` are simple. Let's try to combine them. - // First, we compute the exclusion matrix that has (j, k) = true if selector - // j and selector k conflict -- that is, they are both enabled on the same - // row. This matrix is symmetric and the diagonal entries are false, so we - // only need to store the lower triangular entries. - let mut exclusion_matrix = (0..selectors.len()) - .map(|i| vec![false; i]) - .collect::>(); - - for (i, rows) in selectors - .iter() - .map(|selector| &selector.activations) - .enumerate() - { - // Loop over the selectors previous to this one - for (j, other_selector) in selectors.iter().enumerate().take(i) { - // Look at what selectors are active at the same row - if rows - .iter() - .zip(other_selector.activations.iter()) - .any(|(l, r)| l & r) - { - // Mark them as incompatible - exclusion_matrix[i][j] = true; - } - } - } + let exclusion_matrix = + exclusion_matrix(&selectors, |selector| selector.activations.iter().cloned()); // Simple selectors that we've added to combinations already. let mut added = vec![false; selectors.len()]; @@ -226,6 +202,35 @@ where (combination_assignments, selector_assignments) } +/// Compute an exclusion matrix for the provided virtual_columns (simple selectors, table tags). +/// Caller must provide a closure `rows`, to create an iterator over a column's rows. +/// The iterator must return true if the cell has been assigned. +pub fn exclusion_matrix<'a, C, A: Iterator>( + virtual_columns: &'a [C], + rows: impl Fn(&'a C) -> A, +) -> Vec> { + // First, we compute the exclusion matrix that has (j, k) = true if assignment + // j and k conflict -- that is, they are both assigned on the same + // row. This matrix is symmetric and the diagonal entries are false, so we + // only need to store the lower triangular entries. + let mut exclusion_matrix = (0..virtual_columns.len()) + .map(|i| vec![false; i]) + .collect::>(); + + for (i, vc) in virtual_columns.iter().enumerate() { + // Loop over the columns previous to this one + for (j, other_selector) in virtual_columns.iter().enumerate().take(i) { + // Look at what virtual columns are assigned at the same row + if rows(vc).zip(rows(other_selector)).any(|(l, r)| l & r) { + // Mark them as incompatible + exclusion_matrix[i][j] = true; + } + } + } + + exclusion_matrix +} + #[cfg(test)] mod tests { use super::*; From cc26963337ddd1657db029d35b10fe45d9f2018f Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:35:35 +0800 Subject: [PATCH 10/22] plonk::circuit::ConstraintSystem: compress_dynamic_table_tags() Co-authored-by: Avi Dessauer --- .../plonk/circuit/compress_table_tags.txt | 7 + halo2_proofs/src/plonk/circuit.rs | 107 ++++++-- .../src/plonk/circuit/compress_table_tags.rs | 232 ++++++++++++++++++ 3 files changed, 327 insertions(+), 19 deletions(-) create mode 100644 halo2_proofs/proptest-regressions/plonk/circuit/compress_table_tags.txt create mode 100644 halo2_proofs/src/plonk/circuit/compress_table_tags.rs diff --git a/halo2_proofs/proptest-regressions/plonk/circuit/compress_table_tags.txt b/halo2_proofs/proptest-regressions/plonk/circuit/compress_table_tags.txt new file mode 100644 index 00000000..4e8c3868 --- /dev/null +++ b/halo2_proofs/proptest-regressions/plonk/circuit/compress_table_tags.txt @@ -0,0 +1,7 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc 88c88a92a8c1799fc2b2dac1a5b9b434fc9ac5e1218e5104a85c345124d8a937 # shrinks to tables = [TableDescription { index: 0, activations: [false] }, TableDescription { index: 1, activations: [true] }] diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 49b828df..c3469c35 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1,8 +1,6 @@ use core::cmp::max; use core::ops::{Add, Mul}; use ff::Field; -#[cfg(feature = "unstable-dynamic-lookups")] -use ff::PrimeField; use std::{ convert::TryFrom, ops::{Neg, Sub}, @@ -15,6 +13,8 @@ use crate::{ }; mod compress_selectors; +#[cfg(feature = "unstable-dynamic-lookups")] +mod compress_table_tags; /// A column type pub trait ColumnType: @@ -757,7 +757,7 @@ impl std::fmt::Debug for Expression { Expression::Constant(scalar) => f.debug_tuple("Constant").field(scalar).finish(), Expression::Selector(selector) => f.debug_tuple("Selector").field(selector).finish(), #[cfg(feature = "unstable-dynamic-lookups")] - Expression::TableTag(tag) => f.debug_tuple("TableTag").field(tag).finish(), + Expression::TableTag(vc) => f.debug_tuple("TableTag").field(vc).finish(), // Skip enum variant and print query struct directly to maintain backwards compatibility. Expression::Fixed(FixedQuery { index, @@ -1188,28 +1188,23 @@ impl ConstraintSystem { ) -> (Selector, Vec<(Expression, Column)>), ) -> usize where - F: PrimeField, + F: From, { let mut cells = VirtualCells::new(self); let (selector, table_map) = table_map(&mut cells); let selector = cells.query_selector(selector); - let non_table_columns: Vec<_> = table_map - .iter() - .map(|(_, c)| c) - .filter(|col| !table.columns.contains(col)) - .collect(); - if !non_table_columns.is_empty() { - panic!( - "{:?} does not contain {:?}. Try adding these columns to the dynamic table.", - table, - non_table_columns.as_slice() - ); - } - let mut table_map: Vec<_> = table_map .into_iter() - .map(|(input, table)| { + .map(|(input, table_col)| { + if !table.columns.contains(&table_col) { + panic!( + "{:?} does not contain {:?}. Try adding this column to the dynamic table.", + table, + table_col + ); + } + if selector.contains_simple_selector() { panic!("selector expression containing simple selector supplied to lookup argument"); } @@ -1219,7 +1214,7 @@ impl ConstraintSystem { panic!("input expression containing simple selector supplied to lookup argument"); } - let table_query = cells.query_any(table, Rotation::cur()); + let table_query = cells.query_any(table_col, Rotation::cur()); (selector.clone() * input, selector.clone() * table_query) }) .collect(); @@ -1380,6 +1375,80 @@ impl ConstraintSystem { }); } + #[cfg(feature = "unstable-dynamic-lookups")] + pub(crate) fn compress_dynamic_table_tags( + mut self, + dynamic_tables: Vec>, + ) -> (Self, Vec>) + where + F: From, + { + assert!(self.dynamic_table_tag_map.is_empty()); + assert_eq!(self.dynamic_tables.len(), dynamic_tables.len()); + + let mut new_columns = vec![]; + let (polys, table_tag_assignment) = compress_table_tags::process( + dynamic_tables + .into_iter() + .enumerate() + .map( + |(index, activations)| compress_table_tags::TableDescription { + index, + activations, + }, + ) + .collect(), + || { + let column = self.fixed_column(); + new_columns.push(column); + Expression::Fixed(FixedQuery { + index: self.query_fixed_index(column), + column_index: column.index, + rotation: Rotation::cur(), + }) + }, + ); + + let mut table_tag_map = vec![None; table_tag_assignment.len()]; + let mut table_tag_replacements = vec![None; table_tag_assignment.len()]; + for assignment in table_tag_assignment { + table_tag_replacements[assignment.index] = Some(assignment.expression); + table_tag_map[assignment.index] = Some(new_columns[assignment.combination_index]); + } + + self.dynamic_table_tag_map = table_tag_map + .into_iter() + .map(|a| a.unwrap()) + .collect::>(); + let table_tag_replacements = table_tag_replacements + .into_iter() + .map(|a| a.unwrap()) + .collect::>(); + + // Substitute virtual tag columns for the real fixed columns in all lookup expressions + for expr in self.lookups.iter_mut().flat_map(|lookup| { + lookup + .input_expressions + .iter_mut() + .chain(lookup.table_expressions.iter_mut()) + }) { + *expr = expr.evaluate( + &|constant| Expression::Constant(constant), + &|selector| Expression::Selector(selector), + &|table| table_tag_replacements[table.0].clone(), + &|query| Expression::Fixed(query), + &|query| Expression::Advice(query), + &|query| Expression::Instance(query), + &|a| -a, + &|a, b| a + b, + &|a, b| a * b, + &|a, f| a * f, + ); + } + + (self, polys) + } + /// This will compress selectors together depending on their provided /// assignments. This `ConstraintSystem` will then be modified to add new /// fixed columns (representing the actual selectors) and will return the diff --git a/halo2_proofs/src/plonk/circuit/compress_table_tags.rs b/halo2_proofs/src/plonk/circuit/compress_table_tags.rs new file mode 100644 index 00000000..9df83ba4 --- /dev/null +++ b/halo2_proofs/src/plonk/circuit/compress_table_tags.rs @@ -0,0 +1,232 @@ +use super::{compress_selectors::exclusion_matrix, Expression}; + +use ff::Field; + +/// This describes a table and where it is activated. +#[derive(Debug, Clone)] +pub struct TableDescription { + /// The table that this description references, by index. + pub index: usize, + + /// The vector of booleans defining which rows are active for this table. + pub activations: Vec, +} + +/// This describes the assigned combination of a particular table as well as +/// the expression it should be substituted with. +#[derive(Debug, Clone)] +pub struct TableAssignment { + /// The table that this structure references, by index. + pub index: usize, + + /// The combination this table was assigned to + pub combination_index: usize, + + /// The expression we wish to substitute with + pub expression: Expression, +} + +/// This function takes a vector that defines each table as well as a closure +/// used to allocate new fixed columns, and returns the assignment of each +/// combination as well as details about each table assignment. +/// +/// This function takes +/// * `tables`, a vector of `TableDescription`s that describe each table +/// * `allocate_fixed_columns`, a closure that constructs a new fixed column and +/// queries it at Rotation::cur(), returning the expression +/// +/// and returns `Vec>` containing the assignment of each new fixed column +/// (which each correspond to a combination) as well as a vector of +/// `TableAssignment` that the caller can use to perform the necessary +/// substitutions to the constraint system. +/// +/// This function is completely deterministic. +pub fn process, E>( + tables: Vec, + mut allocate_fixed_column: E, +) -> (Vec>, Vec>) +where + E: FnMut() -> Expression, +{ + if tables.is_empty() { + // There is nothing to optimize. + return (vec![], vec![]); + } + + // The length of all provided table tags must be the same. + let n = tables[0].activations.len(); + assert!(tables.iter().all(|a| a.activations.len() == n)); + + let mut combination_assignments = vec![]; + let mut table_tag_assignments = vec![]; + + let exclusion_matrix = exclusion_matrix(&tables, |table| table.activations.iter().cloned()); + + // Virtual tag columns that we've added to combinations already. + let mut added = vec![false; tables.len()]; + + for (i, table) in tables.iter().enumerate() { + if added[i] { + continue; + } + added[i] = true; + let mut combination: Vec<_> = vec![table]; + let mut combination_added = vec![i]; + + // Try to find other virtual tag columns that can join this one. + 'try_columns: for (j, table) in tables.iter().enumerate().skip(i + 1) { + // Skip columns that have been added to previous combinations + if added[j] { + continue 'try_columns; + } + + // Is this virtual tag column excluded from co-existing in the same + // combination with any of the other virtual tag column so far? + for i in combination_added.iter() { + if exclusion_matrix[j][*i] { + continue 'try_columns; + } + } + + combination.push(table); + combination_added.push(j); + added[j] = true; + } + + let mut combination_assignment = vec![F::ZERO; n]; + let combination_index = combination_assignments.len(); + let query = allocate_fixed_column(); + + table_tag_assignments.extend(combination.into_iter().map(|table| { + // Update the combination assignment + for (combination, active) in combination_assignment + .iter_mut() + .zip(table.activations.iter()) + { + // This will not overwrite another table tag's activations because + // we have ensured that table tags are disjoint. + if *active { + *combination = F::from(table.index as u64 + 1); + } + } + + TableAssignment { + index: table.index, + combination_index, + expression: query.clone(), + } + })); + + combination_assignments.push(combination_assignment); + } + + (combination_assignments, table_tag_assignments) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::{plonk::FixedQuery, poly::Rotation}; + use pasta_curves::Fp; + use proptest::collection::{vec, SizeRange}; + use proptest::prelude::*; + + prop_compose! { + fn arb_table(assignment_size: usize) + (assignment in vec(any::(), assignment_size)) + -> Vec { + assignment + } + } + + prop_compose! { + fn arb_table_list(assignment_size: usize, num_tables: impl Into) + (list in vec(arb_table(assignment_size), num_tables)) + -> Vec + { + list.into_iter().enumerate().map(|(i, activations)| { + TableDescription { + index: i, + activations, + } + }).collect() + } + } + + prop_compose! { + fn arb_instance(max_assignment_size: usize, + max_tables: usize) + (assignment_size in 1..max_assignment_size, + num_tables in 1..max_tables) + (list in arb_table_list(assignment_size, num_tables)) + -> Vec + { + list + } + } + + proptest! { + #![proptest_config(ProptestConfig::with_cases(10000))] + #[test] + fn test_table_combination(tables in arb_instance(10, 15)) { + let mut query = 0; + let (combination_assignments, table_assignments) = + process::(tables.clone(), || { + let tmp = Expression::Fixed(FixedQuery { + index: query, + column_index: query, + rotation: Rotation::cur(), + }); + query += 1; + tmp + }); + + { + let mut tables_seen = vec![]; + assert_eq!(tables.len(), table_assignments.len()); + for table in &table_assignments { + // Every table should be assigned to a combination + assert!(table.combination_index < combination_assignments.len()); + assert!(!tables_seen.contains(&table.index)); + tables_seen.push(table.index); + } + } + + // Test that, for each table, the provided expression evaluates to + // the table tag on rows where the table's activation is on + for table in table_assignments { + assert_eq!( + tables[table.index].activations.len(), + combination_assignments[table.combination_index].len() + ); + for (&activation, &assignment) in tables[table.index] + .activations + .iter() + .zip(combination_assignments[table.combination_index].iter()) + { + let eval = table.expression.evaluate( + &|c| c, + &|_| panic!("should not occur in returned expressions"), + #[cfg(feature = "unstable-dynamic-lookups")] + &|_| panic!("should not occur in returned expressions"), + &|query| { + // Should be the correct combination in the expression + assert_eq!(table.combination_index, query.index); + assignment + }, + &|_| panic!("should not occur in returned expressions"), + &|_| panic!("should not occur in returned expressions"), + &|a| -a, + &|a, b| a + b, + &|a, b| a * b, + &|a, f| a * f, + ); + + if activation { + assert_eq!(eval, Fp::from(table.index as u64 + 1)); + } + } + } + } + } +} From f32fd2a4a03542ae57b8b6ecd0877d0961331510 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:40:03 +0800 Subject: [PATCH 11/22] plonk::keygen: Handle dynamic table tags in keygen_vk, keygen_pk Co-authored-by: Avi Dessauer --- halo2_proofs/src/plonk/keygen.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/halo2_proofs/src/plonk/keygen.rs b/halo2_proofs/src/plonk/keygen.rs index e3ec0fbc..2ad7be88 100644 --- a/halo2_proofs/src/plonk/keygen.rs +++ b/halo2_proofs/src/plonk/keygen.rs @@ -244,6 +244,15 @@ where .map(|poly| domain.lagrange_from_vec(poly)), ); + #[cfg(feature = "unstable-dynamic-lookups")] + let (cs, dynamic_table_polys) = cs.compress_dynamic_table_tags(assembly.dynamic_tables); + #[cfg(feature = "unstable-dynamic-lookups")] + fixed.extend( + dynamic_table_polys + .into_iter() + .map(|poly| domain.lagrange_from_vec(poly)), + ); + let permutation_vk = assembly .permutation .build_vk(params, &domain, &cs.permutation); @@ -307,6 +316,15 @@ where .map(|poly| vk.domain.lagrange_from_vec(poly)), ); + #[cfg(feature = "unstable-dynamic-lookups")] + let (cs, dynamic_table_polys) = cs.compress_dynamic_table_tags(assembly.dynamic_tables); + #[cfg(feature = "unstable-dynamic-lookups")] + fixed.extend( + dynamic_table_polys + .into_iter() + .map(|poly| vk.domain.lagrange_from_vec(poly)), + ); + let fixed_polys: Vec<_> = fixed .iter() .map(|poly| vk.domain.lagrange_to_coeff(poly.clone())) From cfc14689513faf3e9b2a793cc712a98bd189586e Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:50:37 +0800 Subject: [PATCH 12/22] dev::MockProver::run: Handle dynamic tables Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index 9569b2e4..ffca6a3c 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -497,7 +497,7 @@ impl Assignment for MockProver { } } -impl MockProver { +impl> MockProver { /// Runs a synthetic keygen-and-prove operation on the given circuit, collecting data /// about the constraints and their assignments. pub fn run>( @@ -585,6 +585,21 @@ impl MockProver { v })); + #[cfg(feature = "unstable-dynamic-lookups")] + { + let (cs, tag_polys) = prover + .cs + .compress_dynamic_table_tags(prover.dynamic_tables.clone()); + prover.cs = cs; + prover.fixed.extend(tag_polys.into_iter().map(|poly| { + let mut v = vec![CellValue::Unassigned; n]; + for (v, p) in v.iter_mut().zip(&poly[..]) { + *v = CellValue::Assigned(*p); + } + v + })); + } + Ok(prover) } From 579741f8854b370bb2e1f741b1092c8bca964462 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:56:32 +0800 Subject: [PATCH 13/22] dev::failure::VerifyFailure: DynamicTableCellNotAssigned variant Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev/failure.rs | 37 +++++++++++++++++++++++++++++---- 1 file changed, 33 insertions(+), 4 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 948316ea..41426ff0 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -8,6 +8,8 @@ use super::{ util::{self, AnyQuery}, MockProver, Region, }; +#[cfg(feature = "unstable-dynamic-lookups")] +use crate::plonk::DynamicTable; use crate::{ dev::Value, plonk::{Any, Column, ConstraintSystem, Expression, Gate, Instance}, @@ -111,6 +113,18 @@ impl FailureLocation { /// The reasons why a particular circuit is not satisfied. #[derive(Debug, PartialEq, Eq)] pub enum VerifyFailure { + /// A cell used in an active gate was not assigned to. + #[cfg(feature = "unstable-dynamic-lookups")] + DynamicTableCellNotAssigned { + /// The tag of the table containing a unassigned cell. + dynamic_table: DynamicTable, + /// The region in which this cell should be assigned. + region: metadata::Region, + /// The column in which this cell should be assigned. + column: Column, + /// The offset (relative to the start of the region) at which this cell should be assigned. + offset: usize, + }, /// A cell used in an active gate was not assigned to. CellNotAssigned { /// The index of the active gate. @@ -190,6 +204,19 @@ pub enum VerifyFailure { impl fmt::Display for VerifyFailure { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { + #[cfg(feature = "unstable-dynamic-lookups")] + VerifyFailure::DynamicTableCellNotAssigned { + dynamic_table, + region, + column, + offset, + } => { + write!( + f, + "{:?} includes the row at offset {} in the {}, which requires cell in column {:?} be assigned.", + dynamic_table, offset, region, column + ) + } Self::CellNotAssigned { gate, region, @@ -377,6 +404,7 @@ fn render_constraint_not_satisfied( } } +// TODO: handle dynamic lookups separately? /// Renders `VerifyFailure::Lookup`. /// /// ```text @@ -413,8 +441,9 @@ fn render_lookup( FailureLocation::OutsideRegion { row } => *row, } as i32; - // Recover the fixed columns from the table expressions. We don't allow composite - // expressions for the table side of lookups. + // Recover the fixed columns from the table expressions. + // We don't allow composite expressions for the table side of fixed lookups. + // The table side of Dynamic lookups have a tag column. let table_columns = lookup.table_expressions.iter().map(|expr| { expr.evaluate( &|_| panic!("no constants in table expressions"), @@ -422,11 +451,11 @@ fn render_lookup( #[cfg(feature = "unstable-dynamic-lookups")] &|_| panic!("no virtual columns in table expressions"), &|query| format!("F{}", query.column_index), - &|_| panic!("no advice columns in table expressions"), + &|query| format!("A{}", query.column_index), &|_| panic!("no instance columns in table expressions"), &|_| panic!("no negations in table expressions"), &|_, _| panic!("no sums in table expressions"), - &|_, _| panic!("no products in table expressions"), + &|a, b| format!("{} * {}", a, b), &|_, _| panic!("no scaling in table expressions"), ) }); From 444b8a674c7de49d1389216a4f08776980abefeb Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 10:58:45 +0800 Subject: [PATCH 14/22] dev::MockProver::verify: Handle dynamic table errors Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev.rs | 68 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 64 insertions(+), 4 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index ffca6a3c..f2f26039 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -9,7 +9,7 @@ use ff::Field; use crate::plonk::Assigned; #[cfg(feature = "unstable-dynamic-lookups")] -use crate::plonk::TableTag; +use crate::plonk::{DynamicTable, TableTag}; use crate::{ circuit, plonk::{ @@ -916,12 +916,72 @@ impl> MockProver { }) }; - let mut errors: Vec<_> = iter::empty() + // Check that all cell included in dynamic tables are assigned. + #[cfg(feature = "unstable-dynamic-lookups")] + let dynamic_table_errors = { + fn unassigned_error( + regions: &[Region], + cell: CellValue, + dynamic_table: &DynamicTable, + column: Column, + row: usize, + ) -> Option { + match cell { + CellValue::Unassigned => { + if let FailureLocation::InRegion { region, offset } = + FailureLocation::find(regions, row, iter::once(column).collect()) + { + Some(VerifyFailure::DynamicTableCellNotAssigned { + dynamic_table: dynamic_table.clone(), + region, + column, + offset, + }) + } else { + panic!("Rows cannot be included in a dynamic table outside of a region") + } + } + CellValue::Assigned(_) => None, + CellValue::Poison(_) => panic!("A poisoned cell was used in a dynamic table"), + } + } + + self.dynamic_tables + .iter() + .enumerate() + .flat_map(|(table_index, virtual_rows)| { + self.fixed[self.cs.dynamic_table_tag_map[table_index].index()] + .iter() + .zip(virtual_rows) + .enumerate() + .filter_map(move |(row, r)| match r { + (CellValue::Assigned(tag), true) => { + if F::from(table_index as u64 + 1) == *tag { + let table = &self.cs.dynamic_tables[table_index]; + Some(table.columns.iter().filter_map(move |col| match col.column_type() { + Any::Advice => unassigned_error(&self.regions, self. advice[col.index()][row], table, *col, row), + Any::Fixed => unassigned_error(&self.regions, self.fixed[col.index()][row], table, *col, row), + Any::Instance => panic!("This should be imposible. Instance columns are not yet supported in dynamic tables"), + })) + } else { + panic!("There was an error in dynamic table tag compression, The wrong tag was found in a row") + } + } + (CellValue::Unassigned, true) => panic!("There was an error in dynamic table tag compression, The tag cell was not assigned."), + (CellValue::Poison(_), true) => panic!("There was an error in dynamic table tag compression, The tag cell was poisoned."), + _ => None, + }).flatten() + }) + }; + + let errors = iter::empty() .chain(selector_errors) .chain(gate_errors) .chain(lookup_errors) - .chain(perm_errors) - .collect(); + .chain(perm_errors); + #[cfg(feature = "unstable-dynamic-lookups")] + let errors = errors.chain(dynamic_table_errors); + let mut errors: Vec<_> = errors.collect(); if errors.is_empty() { Ok(()) } else { From eff691740c728b5e5b90b736316c0a368ac6e068 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 11:08:19 +0800 Subject: [PATCH 15/22] cost::CircuitCost::measure: Account for dynamic table tags Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev/cost.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/halo2_proofs/src/dev/cost.rs b/halo2_proofs/src/dev/cost.rs index 5c506515..7ac1d04e 100644 --- a/halo2_proofs/src/dev/cost.rs +++ b/halo2_proofs/src/dev/cost.rs @@ -307,6 +307,8 @@ impl> CircuitCost= cs.minimum_rows()); From 124a1e1d9556c80fa129090ab6ba1a67f5a6dd7f Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 11:30:27 +0800 Subject: [PATCH 16/22] layout::CircuitLayout::render: Handle dynamic table tags Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev/graph/layout.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev/graph/layout.rs b/halo2_proofs/src/dev/graph/layout.rs index 05d60244..89ade47e 100644 --- a/halo2_proofs/src/dev/graph/layout.rs +++ b/halo2_proofs/src/dev/graph/layout.rs @@ -82,7 +82,7 @@ impl CircuitLayout { } /// Renders the given circuit on the given drawing area. - pub fn render, DB: DrawingBackend>( + pub fn render, ConcreteCircuit: Circuit, DB: DrawingBackend>( self, k: u32, circuit: &ConcreteCircuit, @@ -112,6 +112,9 @@ impl CircuitLayout { let (cs, selector_polys) = cs.compress_selectors(layout.selectors); let non_selector_fixed_columns = cs.num_fixed_columns - selector_polys.len(); + #[cfg(feature = "unstable-dynamic-lookups")] + let (cs, _tag_polys) = cs.compress_dynamic_table_tags(layout.dynamic_tables_assignments); + // Figure out what order to render the columns in. // TODO: For now, just render them in the order they were configured. let total_columns = cs.num_instance_columns + cs.num_advice_columns + cs.num_fixed_columns; From 3cb9ab695b488c9f5bcb5d7b446912971bafc631 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Thu, 23 Feb 2023 11:35:44 +0800 Subject: [PATCH 17/22] dev::tests: Add tests for dynamic lookups Co-authored-by: Avi Dessauer --- halo2_proofs/src/dev.rs | 594 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 594 insertions(+) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index f2f26039..29712995 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1234,4 +1234,598 @@ mod tests { }]) ); } + + #[cfg(test)] + #[cfg(feature = "unstable-dynamic-lookups")] + mod dynamic_lookups { + use crate::plonk::DynamicTable; + + use super::*; + + const K: u32 = 7; + + #[derive(Clone)] + struct DynLookupCircuitConfig { + q: Selector, + a: Column, + // A table containing table_vals. + table: DynamicTable, + } + + impl DynLookupCircuitConfig { + fn assign_lookups( + &self, + layouter: &mut impl Layouter, + lookup: impl Iterator + Clone, + ) -> Result<(), Error> { + layouter.assign_region( + || "lookups", + |mut region| { + // Enable the lookup on rows + for (offset, val) in lookup.clone().enumerate() { + self.q.enable(&mut region, offset)?; + + region.assign_advice( + || "", + self.a, + offset, + || Value::known(Fp::from(val as u64)), + )?; + } + + Ok(()) + }, + ) + } + } + + /// Just like dynamic_lookup, but breaks the table into single row regions. + /// TODO refactor + #[test] + fn dynamic_lookup_success() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = DynLookupCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.create_dynamic_table("table", &[], &[table_vals]); + + meta.lookup_dynamic(&table, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + // If q is enabled, a must be in the table. + (q, vec![(a, table_vals.into())]) + }); + + DynLookupCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + config.assign_lookups(&mut layouter, 0..=5)?; + let table_vals = config.table.columns()[0]; + + layouter.assign_region( + || "table", + |mut region| { + for i in 0..=5 { + region.assign_advice( + || "", + table_vals.try_into().unwrap(), + i, + || Value::known(Fp::from(i as u64)), + )?; + region.add_to_lookup(config.table.tag(), i)?; + } + Ok(()) + }, + )?; + Ok(()) + } + } + + MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify() + .unwrap() + } + + #[test] + fn dynamic_lookup_multi_region_success() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = DynLookupCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.create_dynamic_table("table", &[], &[table_vals]); + + meta.lookup_dynamic(&table, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + // If q is enabled, a must be in the table. + (q, vec![(a, table_vals.into())]) + }); + + DynLookupCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + config.assign_lookups(&mut layouter, 0..=5)?; + let table_vals = config.table.columns()[0]; + + for i in 0..=5 { + layouter.assign_region( + || format!("table {}", i), + |mut region| { + region.assign_advice( + || "", + table_vals.try_into().unwrap(), + 0, + || Value::known(Fp::from(i as u64)), + )?; + region.add_to_lookup(config.table.tag(), 0)?; + Ok(()) + }, + )?; + } + Ok(()) + } + } + + MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify() + .unwrap() + } + + #[test] + fn dynamic_lookup_not_in_table_err() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = DynLookupCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.create_dynamic_table("table", &[], &[table_vals]); + + meta.lookup_dynamic(&table, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + // If q is enabled, a must be in the table. + (q, vec![(a, table_vals.into())]) + }); + + DynLookupCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + config.assign_lookups(&mut layouter, 0..=6)?; + let table_vals = config.table.columns()[0]; + + for i in 0..=5 { + layouter.assign_region( + || format!("table {}", i), + |mut region| { + region.assign_advice( + || "", + table_vals.try_into().unwrap(), + 0, + || Value::known(Fp::from(i as u64)), + )?; + config.table.add_row(&mut region, 0) + }, + )?; + } + Ok(()) + } + } + + let errs = MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify() + .expect_err("The table only contains 0..=5, but lookups on 0..=6 succeeded"); + + assert_eq!( + errs[0], + VerifyFailure::Lookup { + lookup_index: 0, + location: FailureLocation::InRegion { + region: (0, "lookups").into(), + offset: 6, + } + } + ); + } + + #[test] + fn dynamic_lookup_no_rows_included() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = DynLookupCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.create_dynamic_table("table", &[], &[table_vals]); + + meta.lookup_dynamic(&table, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + // If q is enabled, a must be in the table. + (q, vec![(a, table_vals.into())]) + }); + + DynLookupCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + config.assign_lookups(&mut layouter, 0..=5)?; + let table_vals = config.table.columns()[0]; + + for i in 0..=5 { + layouter.assign_region( + || format!("table {}", i), + |mut region| { + region.assign_advice( + || "", + table_vals.try_into().unwrap(), + 0, + || Value::known(Fp::from(i as u64)), + ) + // We should error since the table is empty without this line. + // table.include_row(|| "", &mut region, 0)?; + }, + )?; + } + Ok(()) + } + } + + let res = MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify(); + + use FailureLocation::*; + use VerifyFailure::*; + assert_eq!( + res, + Err(vec![ + Lookup { + lookup_index: 0, + location: InRegion { + region: (0, "lookups",).into(), + offset: 0, + }, + }, + Lookup { + lookup_index: 0, + location: InRegion { + region: (0, "lookups",).into(), + offset: 1, + }, + }, + Lookup { + lookup_index: 0, + location: InRegion { + region: (0, "lookups",).into(), + offset: 2, + }, + }, + Lookup { + lookup_index: 0, + location: InRegion { + region: (0, "lookups",).into(), + offset: 3, + }, + }, + Lookup { + lookup_index: 0, + location: InRegion { + region: (0, "lookups",).into(), + offset: 4, + }, + }, + Lookup { + lookup_index: 0, + location: InRegion { + region: (0, "lookups",).into(), + offset: 5, + }, + }, + ],) + ); + } + + #[test] + fn unassigned_dynamic_table_cell() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = DynLookupCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.create_dynamic_table("table", &[], &[table_vals]); + + meta.lookup_dynamic(&table, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + // If q is enabled, a must be in the table. + (q, vec![(a, table_vals.into())]) + }); + + DynLookupCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "table", + |mut region| { + config.table.add_row(&mut region, 0)?; + Ok(()) + }, + )?; + Ok(()) + } + } + + let res = MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify(); + + assert_eq!( + res, + Err(vec![VerifyFailure::DynamicTableCellNotAssigned { + dynamic_table: DynamicTable { + name: "table".to_string(), + index: 0, + columns: vec![Column::new(1, Any::Advice)], + }, + region: (0, "table".to_string(),).into(), + column: Column::new(1, Any::Advice), + offset: 0, + }]) + ) + } + + #[test] + #[should_panic] + fn column_not_in_dynamic_table() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = DynLookupCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let not_table_vals = meta.advice_column(); + let table_vals = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.create_dynamic_table("table", &[], &[table_vals]); + + meta.lookup_dynamic(&table, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + // If q is enabled, a must be in the table. + ( + q, + // Note that we are looking up a in not_table_vals. + // not_table_vals is not a column in the dynamic table. + vec![(a, not_table_vals.into())], + ) + }); + + DynLookupCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "table", + |mut region| { + config.table.add_row(&mut region, 0)?; + Ok(()) + }, + )?; + Ok(()) + } + } + + let res = MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify(); + + assert_eq!( + res, + Err(vec![VerifyFailure::DynamicTableCellNotAssigned { + dynamic_table: DynamicTable { + name: "table".to_string(), + index: 0, + columns: vec![Column::new(1, Any::Advice)], + }, + region: (0, "table".to_string(),).into(), + column: Column::new(1, Any::Advice), + offset: 0, + }]) + ) + } + } + + #[cfg(test)] + #[cfg(feature = "unstable-dynamic-lookups")] + mod even_odd_dyn_tables { + use crate::plonk::DynamicTable; + + use super::*; + + const K: u32 = 7; + + #[derive(Clone)] + struct EvenOddCircuitConfig { + is_even: Selector, + is_odd: Selector, + a: Column, + even: DynamicTable, + odd: DynamicTable, + } + + #[test] + fn even_odd_dyn_tables() { + struct DynLookupCircuit {} + impl Circuit for DynLookupCircuit { + type Config = EvenOddCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let is_even = meta.complex_selector(); + let is_odd = meta.complex_selector(); + let even = meta.create_dynamic_table("even", &[], &[table_vals]); + let odd = meta.create_dynamic_table("odd", &[], &[table_vals]); + + meta.lookup_dynamic(&even, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + (is_even, vec![(a, table_vals.into())]) + }); + + meta.lookup_dynamic(&odd, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + (is_odd, vec![(a, table_vals.into())]) + }); + + EvenOddCircuitConfig { + a, + is_even, + is_odd, + even, + odd, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let table_vals = config.even.columns()[0]; + + for i in 0..=5 { + layouter.assign_region( + || format!("lookup {}", i), + |mut region| { + // Enable the lookup on rows + if i % 2 == 0 { + config.is_even.enable(&mut region, 0)?; + } else { + config.is_odd.enable(&mut region, 0)?; + }; + + region.assign_advice( + || "", + config.a, + 0, + || Value::known(Fp::from(i as u64)), + ) + }, + )?; + } + layouter.assign_region( + || "table", + |mut region| { + for i in 0..=5 { + region.assign_advice( + || "", + table_vals.try_into().unwrap(), + i, + || Value::known(Fp::from(i as u64)), + )?; + + let table = if i % 2 == 0 { + &config.even + } else { + &config.odd + }; + table.add_row(&mut region, i)?; + } + Ok(()) + }, + )?; + Ok(()) + } + } + + MockProver::run(K, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify() + .unwrap(); + } + } } From 5548bdc515fa8bbf9114926f42d195cc49cbddc2 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 21 Feb 2023 23:15:10 +0800 Subject: [PATCH 18/22] halo2_proofs::examples::dynamic_lookup: Dynamic lookup example Co-authored-by: Avi Dessauer --- halo2_proofs/Cargo.toml | 4 + halo2_proofs/examples/dynamic-lookup.rs | 138 ++++++++++++++++++++++++ 2 files changed, 142 insertions(+) create mode 100644 halo2_proofs/examples/dynamic-lookup.rs diff --git a/halo2_proofs/Cargo.toml b/halo2_proofs/Cargo.toml index 86222f36..99e9e0b8 100644 --- a/halo2_proofs/Cargo.toml +++ b/halo2_proofs/Cargo.toml @@ -100,3 +100,7 @@ bench = false [[example]] name = "circuit-layout" required-features = ["test-dev-graph"] + +[[example]] +name = "dynamic-lookup" +required-features = ["unstable-dynamic-lookups"] diff --git a/halo2_proofs/examples/dynamic-lookup.rs b/halo2_proofs/examples/dynamic-lookup.rs new file mode 100644 index 00000000..36c2212b --- /dev/null +++ b/halo2_proofs/examples/dynamic-lookup.rs @@ -0,0 +1,138 @@ +use halo2_proofs::{ + circuit::{Layouter, SimpleFloorPlanner, Value}, + dev::MockProver, + pasta::Fp, + plonk::{ + create_proof, keygen_pk, keygen_vk, verify_proof, Advice, Circuit, Column, + ConstraintSystem, DynamicTable, Error, Selector, SingleVerifier, + }, + poly::{commitment::Params, Rotation}, + transcript::{Blake2bRead, Blake2bWrite}, +}; +use pasta_curves::{vesta, EqAffine}; +use rand_core::OsRng; + +#[derive(Clone)] +struct EvenOddCircuitConfig { + is_even: Selector, + is_odd: Selector, + a: Column, + // starts at zero to use as default + table_vals: Column, + even: DynamicTable, + odd: DynamicTable, +} + +struct DynLookupCircuit {} +impl Circuit for DynLookupCircuit { + type Config = EvenOddCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table_vals = meta.advice_column(); + let is_even = meta.complex_selector(); + let is_odd = meta.complex_selector(); + let even = meta.create_dynamic_table("even", &[], &[table_vals]); + let odd = meta.create_dynamic_table("odd", &[], &[table_vals]); + + meta.lookup_dynamic(&even, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + (is_even, vec![(a, table_vals.into())]) + }); + + meta.lookup_dynamic(&odd, |cells| { + let a = cells.query_advice(a, Rotation::cur()); + + (is_odd, vec![(a, table_vals.into())]) + }); + + EvenOddCircuitConfig { + a, + table_vals, + is_even, + is_odd, + even, + odd, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + for i in 0..=5 { + layouter.assign_region( + || format!("lookup: {}", i), + |mut region| { + // Enable the lookup on rows + if i % 2 == 0 { + config.is_even.enable(&mut region, 0)?; + } else { + config.is_odd.enable(&mut region, 0)?; + }; + + region.assign_advice(|| "", config.a, 0, || Value::known(Fp::from(i as u64))) + }, + )?; + } + layouter.assign_region( + || "table", + |mut region| { + for i in 0..=5 { + region.assign_advice( + || "", + config.table_vals, + i, + || Value::known(Fp::from(i as u64)), + )?; + + let table = if i % 2 == 0 { + &config.even + } else { + &config.odd + }; + table.add_row(&mut region, i)?; + } + Ok(()) + }, + )?; + Ok(()) + } +} + +fn main() { + let k = 5; + + MockProver::run(k, &DynLookupCircuit {}, vec![]) + .unwrap() + .verify() + .unwrap(); + + let params: Params = Params::new(k); + let verifier = SingleVerifier::new(¶ms); + let vk = keygen_vk(¶ms, &DynLookupCircuit {}).unwrap(); + let pk = keygen_pk(¶ms, vk, &DynLookupCircuit {}).unwrap(); + let mut transcript = Blake2bWrite::<_, vesta::Affine, _>::init(vec![]); + create_proof( + ¶ms, + &pk, + &[DynLookupCircuit {}], + &[&[]], + &mut OsRng, + &mut transcript, + ) + .expect("Failed to create proof"); + + let proof: Vec = transcript.finalize(); + + let mut transcript = Blake2bRead::init(&proof[..]); + verify_proof(¶ms, pk.get_vk(), verifier, &[&[]], &mut transcript) + .expect("could not verify_proof"); +} From 162412700d52e6aa4c5d272e69012bda9a2fcd83 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Fri, 24 Feb 2023 15:31:08 +0800 Subject: [PATCH 19/22] Docfixes and minor refactors --- halo2_proofs/src/dev.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index 29712995..9cf7573b 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1280,7 +1280,7 @@ mod tests { } /// Just like dynamic_lookup, but breaks the table into single row regions. - /// TODO refactor + /// TODO refactor to remove code duplication #[test] fn dynamic_lookup_success() { struct DynLookupCircuit {} From a68c7a6525f3e045584c0f5b50b959d1d2ae12d5 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Sun, 12 Mar 2023 10:03:57 +0700 Subject: [PATCH 20/22] CHANGELOG: bound instead of --- halo2_proofs/CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/halo2_proofs/CHANGELOG.md b/halo2_proofs/CHANGELOG.md index 01511fcd..75408d32 100644 --- a/halo2_proofs/CHANGELOG.md +++ b/halo2_proofs/CHANGELOG.md @@ -6,6 +6,12 @@ and this project adheres to Rust's notion of [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ## [Unreleased] +### Added + +### Changed +- `halo2_proofs::dev` + - `MockProver` now has an additional bound `>`. + - `graph::CircuitLayout::render` now has an additional bound `>`. ## [0.3.0] - 2023-03-21 ### Breaking circuit changes From edf0c84c93c21a994c7e969a1a0d865572bf6094 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 5 Apr 2023 01:43:17 +0700 Subject: [PATCH 21/22] book/dev/dynamic-lookups.md: Document dynamic lookups feature --- book/src/dev/dynamic-lookups.md | 85 +++++++++++++++++++++++++++++++ halo2_proofs/src/plonk/circuit.rs | 1 - 2 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 book/src/dev/dynamic-lookups.md diff --git a/book/src/dev/dynamic-lookups.md b/book/src/dev/dynamic-lookups.md new file mode 100644 index 00000000..a4a809a8 --- /dev/null +++ b/book/src/dev/dynamic-lookups.md @@ -0,0 +1,85 @@ +# Dynamic lookups +*Note: This is an unstable nightly feature and can be enabled with the flag `#[cfg(feature = unstable-dynamic-lookups)]`.* + +The current `halo2` [lookup argument](../design/proving-system/lookup.md) only supports fixed tables, whose values are fixed as part of the constraint system definition. However, some use-cases require looking up witnessed values, which can change with each instance: for example, a set of preimages and hashes of the SHA256 hash function. + +## `DynamicTable` +A `DynamicTable` is associated with: + ​ | description +--------|-------------------------------------------------------------------------------------------------------------------------------------- +`index` | This table's index in the constraint system's list of dynamic tables +columns | A list of `Advice` and `Fixed` columns where this table's values can be assigned. + rows | The rows in this table's columns, where its values are assigned. Every table column must be assigned in the same rows. + `tag` | `index` + 1; the tag is appended to each lookup argument involving this table. + +Consider a `DynamicTable` with `index = 1`, `tag = index + 1 = 2`. It is assigned on advice column `A1` and fixed column `F0`, on rows `0`, `2`, `3`. Note that the table need not occupy a contiguous area in the circuit: + +| row | A0 | A1 | A2 | F0 | F1 | +|-----|----|----|----|----|----| +| 0 | | ⬤ | | ⬤ | | +| 1 | | `x`| | `x`| | +| 2 | | ⬤ | | ⬤ | | +| 3 | | ⬤ | | ⬤ | | + +Now, we specify a lookup `[(q_lookup * A0, A1), (q_lookup * A2,F0)]`: i.e., on the rows where `q_lookup = 1` is enabled, we enforce that the values in `A0` (`A2`) appear somewhere in the table column `A1` (`F0`). If all inputs (◯, ◯) indeed map to a table entry (⬤, ⬤), the lookup argument passes. +| row | q_lookup | A0 | A1 | A2 | F0 | F1 | +|-----|----------|----|----|----|----|----| +| 0 | 1 | ◯ | ⬤ | ◯ | ⬤ | | +| 1 | 1 | ◯ | `x`| ◯ | `x`| | +| 2 | 0 | | ⬤ | | ⬤ | | +| 3 | 0 | | ⬤ | | ⬤ | | + +## Table tag +A subtle problem arises in the example above: the cells marked `x` are in the table *columns*, but are not part of the table's *rows*, and therefore must not be considered valid lookup values. To enforce this, we: +- repurpose the fixed column `F1` to serve as the table's "tag column", and +- append the table's **tag** to the lookup argument: `[(q_lookup * A0, A1), (q_lookup * A2,F0), (q_lookup * 2, q_lookup * F1)]`. + +In other words, we append a **tag** to get input entries of the form (◯, ◯, 2), in order to match the tagged table entries (⬤, ⬤, 2). +| row | q_lookup | A0 | A1 | A2 | F0 | F1 | +|-----|----------|----|----|----|----|----| +| 0 | 1 | ◯ | ⬤ | ◯ | ⬤ | 2 | +| 1 | 1 | ◯ | `x`| ◯ | `x`| 0 | +| 2 | 0 | | ⬤ | | ⬤ | 2 | +| 3 | 0 | | ⬤ | | ⬤ | 2 | + +Notice that if we now attempt to lookup some illegal inputs `x` on row 1, the lookup argument will fail, since the input `(x, x, 2)` does not appear anywhere in the table: +```ignore + [(q_lookup * A0, A1), (q_lookup * A2, F0), (q_lookup * 2, q_lookup * F1)] += [(1 * x, A1), (1 * x, F0), (1 * 2, 1 * F1)] += [(x, A1), (x, F0), (2, F1)] +``` + +| row | q_lookup | A0 | A1 | A2 | F0 | F1 | +|-----|----------|----|----|----|----|----| +| 0 | 1 | ◯ | ⬤ | ◯ | ⬤ | 2 | +| 1 | 1 | `x`| `x`| `x`| `x`| 0 | +| 2 | 0 | | ⬤ | | ⬤ | 2 | +| 3 | 0 | | ⬤ | | ⬤ | 2 | + +Table tags also enable an important optimization: it allows unused rows in table columns to be recycled for other purposes, without affecting the lookup argument. By the same reasoning, this also allows dynamic tables to be "stacked" vertically by the layouter. This optimization may easily be applied to fixed lookups too. + +Dynamic table tags are assigned to fixed columns in order to enforce their shape in the circuit: even though the values of a table can change across instances, its shape must stay the same. Under the hood, we use the [selector combining](../design/implementation/selector-combining.md) algorithm to combine table tags into fewer fixed columns without overlapping. + +## Usage +### Creating dynamic tables +A `DynamicTable` is created using the `ConstraintSystem::create_dynamic_table()` method. The `Fixed` and `Advice` columns involved in the table are passed as arguments. (NB: `Instance` columns are not yet supported.) + +```ignore +pub fn create_dynamic_table( + &mut self, + name: impl Into, + fixed_columns: &[Column], + advice_columns: &[Column], +) -> DynamicTable; +``` + +### Configuring dynamic lookups +A `DynamicTable` can be used in a lookup argument configuration using the `ConstraintSystem::lookup_dynamic()` method. This works similarly to `ConstraintSystem::lookup()`; however, it additionally: +- enforces that the table columns involved in the argument are indeed part of the provided `DynamicTable`; and +- adds the table tag to the lookup argument, as described in [[Table tag]](#table-tag). + +### Assigning table values +Table values are assigned within regions, using the method `DynamicTable::add_row(&self, region: Region, offset: usize)`. As usual, the absolute rows involved in the dynamic table are only known after the floor planner rearranges the regions. (See [[Chips]](../concepts/chips.md) for an explanation of floor planners and regions.) + +### Assigning input values +Input values are assigned within regions, and are usually identified by enabling the appropriate `q_lookup` selector at the desired offset. This is the same behavior as in assigning inputs to fixed tables. \ No newline at end of file diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index c3469c35..6e079b0a 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1209,7 +1209,6 @@ impl ConstraintSystem { panic!("selector expression containing simple selector supplied to lookup argument"); } - // TODO is this needed if input.contains_simple_selector() { panic!("input expression containing simple selector supplied to lookup argument"); } From eb938d741573c9c46bf00fd1b00b5f06907bd318 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Wed, 12 Apr 2023 12:41:59 +0200 Subject: [PATCH 22/22] [WIP] dev::tests: Failing example --- halo2_proofs/src/dev.rs | 113 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 112 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index 9cf7573b..2b2f3515 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1022,7 +1022,7 @@ impl> MockProver { #[cfg(test)] mod tests { use group::ff::Field; - use pasta_curves::Fp; + use pasta_curves::{EqAffine, Fp}; use super::{FailureLocation, MockProver, VerifyFailure}; use crate::{ @@ -1828,4 +1828,115 @@ mod tests { .unwrap(); } } + + #[cfg(feature = "unstable-dynamic-lookups")] + #[test] + fn failing() { + struct FailingCircuit {} + #[derive(Clone)] + struct FailingConfig { + first_input: Column, + second_input: Column, + is_first_table: Selector, + is_second_table: Selector, + first_table: crate::plonk::DynamicTable, + second_table: crate::plonk::DynamicTable, + } + impl Circuit for FailingCircuit { + type Config = FailingConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let first_input = meta.advice_column(); + let second_input = meta.advice_column(); + let first_table_vals = meta.advice_column(); + // Reuse table column + let second_table_vals = first_table_vals; + let is_first_table = meta.complex_selector(); + let is_second_table = meta.complex_selector(); + let first_table = + meta.create_dynamic_table("first_table", &[], &[first_table_vals]); + let second_table = + meta.create_dynamic_table("second_table", &[], &[second_table_vals]); + + meta.lookup_dynamic(&first_table, |cells| (is_first_table, vec![])); + + meta.lookup_dynamic(&second_table, |cells| (is_second_table, vec![])); + + FailingConfig { + first_input, + second_input, + is_first_table, + is_second_table, + first_table, + second_table, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "", + |mut region| { + config.is_first_table.enable(&mut region, 0)?; + + Ok(()) + }, + )?; + + layouter.assign_region( + || "", + |mut region| { + config.is_second_table.enable(&mut region, 0)?; + + Ok(()) + }, + )?; + + layouter.assign_region( + || "table", + |mut region| { + region.assign_advice( + || "", + config.first_table.columns()[0].try_into().unwrap(), + 0, + || Value::known(Fp::from(1)), + )?; + config.first_table.add_row(&mut region, 0)?; + + Ok(()) + }, + )?; + + layouter.assign_region( + || "table", + |mut region| { + region.assign_advice( + || "", + config.second_table.columns()[0].try_into().unwrap(), + 0, + || Value::known(Fp::from(1)), + )?; + config.second_table.add_row(&mut region, 0)?; + + Ok(()) + }, + )?; + + Ok(()) + } + } + + const K: u32 = 3; + MockProver::run(K, &FailingCircuit {}, vec![]) + .unwrap() + .assert_satisfied(); + } }