plonk::circuit::Assignment: Introduce add_to_lookup() method

Co-authored-by: Avi Dessauer <avi.dessauer@platonic.systems>

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<F: Field> {
     instance: Vec<Vec<InstanceValue<F>>>,
 
     selectors: Vec<Vec<bool>>,
+    /// A map between DynamicTable.index, and rows included.
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    dynamic_tables: Vec<Vec<bool>>,
 
     permutation: permutation::keygen::Assembly,
 
@@ -354,6 +359,19 @@ impl<F: Field> Assignment<F> for MockProver<F> {
         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<Instance>,
@@ -520,6 +538,8 @@ impl<F: Field + Ord> MockProver<F> {
         // 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<F: Field + Ord> MockProver<F> {
             advice,
             instance,
             selectors,
+            #[cfg(feature = "unstable-dynamic-lookups")]
+            dynamic_tables,
             permutation,
             usable_rows: 0..usable_rows,
         };

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<Any>, usize, Column<Any>, usize)>,
     /// Selector assignments used for optimization pass
     pub(crate) selectors: Vec<Vec<bool>>,
+    /// A map between DynamicTable.index, and rows included.
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    pub(crate) dynamic_tables_assignments: Vec<Vec<bool>>,
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    pub(crate) dynamic_tables: Vec<DynamicTable>,
 }
 
 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<DynamicTable>,
+    ) -> 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<F: Field> Assignment<F> 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<Instance>, _: usize) -> Result<Value<F>, Error> {
         Ok(Value::unknown())
     }
@@ -262,7 +292,13 @@ impl<G: PrimeGroup, ConcreteCircuit: Circuit<G::Scalar>> CircuitCost<G, Concrete
         // Collect the layout details.
         let mut cs = ConstraintSystem::default();
         let config = ConcreteCircuit::configure(&mut cs);
-        let mut layout = Layout::new(k, 1 << k, cs.num_selectors);
+        let mut layout = Layout::new(
+            k,
+            1 << k,
+            cs.num_selectors,
+            #[cfg(feature = "unstable-dynamic-lookups")]
+            cs.dynamic_tables.clone(),
+        );
         ConcreteCircuit::FloorPlanner::synthesize(
             &mut layout,
             circuit,

halo2_proofs/src/dev/graph.rs

@@ -1,6 +1,8 @@
 use ff::Field;
 use tabbycat::{AttrList, Edge, GraphBuilder, GraphType, Identity, StmtList};
 
+#[cfg(feature = "unstable-dynamic-lookups")]
+use crate::plonk::TableTag;
 use crate::{
     circuit::Value,
     plonk::{
@@ -99,6 +101,11 @@ impl<F: Field> Assignment<F> for Graph {
         Ok(())
     }
 
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    fn add_to_lookup(&mut self, _: TableTag, _: usize) -> Result<(), Error> {
+        Ok(())
+    }
+
     fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Value<F>, Error> {
         Ok(Value::unknown())
     }

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,

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<F>> Assignment<F> 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<Instance>, row: usize) -> Result<Value<F>, Error> {
         let _guard = debug_span!("positioned").entered();
         debug!(target: "query_instance", column = ?column, row = row);

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<F: Field> {
         A: FnOnce() -> AR,
         AR: Into<String>;
 
+    /// 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.

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<F: Field> {
     fixed: Vec<Polynomial<Assigned<F>, LagrangeCoeff>>,
     permutation: permutation::keygen::Assembly,
     selectors: Vec<Vec<bool>>,
+    /// A map between DynamicTable.index, and rows included.
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    dynamic_tables: Vec<Vec<bool>>,
     // A range of available rows for assignment and copies.
     usable_rows: Range<usize>,
     _marker: std::marker::PhantomData<F>,
@@ -82,6 +87,17 @@ impl<F: Field> Assignment<F> for Assembly<F> {
         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<Instance>, row: usize) -> Result<Value<F>, 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,
     };

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<Instance>,