Merge eb938d7415 into 7df93fd855

Fix MD book generation

.github/workflows/book.yml

@@ -12,7 +12,7 @@ jobs:
       - uses: actions/checkout@v3
       - uses: actions-rs/toolchain@v1
         with:
-          toolchain: nightly
+          toolchain: '1.76.0'
           override: true
 
       # - name: Setup mdBook
@@ -26,7 +26,7 @@ jobs:
         uses: actions-rs/cargo@v1
         with:
           command: install
-          args: mdbook --git https://github.com/HollowMan6/mdBook.git --rev 62e01b34c23b957579c04ee1b24b57814ed8a4d5
+          args: mdbook --git https://github.com/HollowMan6/mdBook.git --rev 5830c9555a4dc051675d17f1fcb04dd0920543e8
 
       - name: Install mdbook-katex and mdbook-pdf
         uses: actions-rs/cargo@v1
@@ -40,6 +40,11 @@ jobs:
       - name: Build halo2 book
         run: mdbook build book/
 
+      - uses: actions-rs/toolchain@v1
+        with:
+          toolchain: nightly-2023-10-05 
+          override: true
+
       - name: Build latest rustdocs
         uses: actions-rs/cargo@v1
         with:

book/book.toml

@@ -14,8 +14,6 @@ title = "The halo2 Book"
 macros = "macros.txt"
 renderers = ["html"]
 
-[output.katex]
-
 [output.html]
 
 [output.html.print]

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<String>,
+    fixed_columns: &[Column<Fixed>],
+    advice_columns: &[Column<Advice>],
+) -> 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.

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<F>` now has an additional bound `<F + From<u64>>`.
+    - `graph::CircuitLayout::render<F>` now has an additional bound `<F + From<u64>>`.
 
 ## [0.3.0] - 2023-03-21
 ### Breaking circuit changes

halo2_proofs/Cargo.toml

@@ -96,7 +96,9 @@ beta = [
 ]
 nightly = [
     "beta",
+    "unstable-dynamic-lookups",
 ]
+unstable-dynamic-lookups = []
 # Add flags for in-development features above this line.
 
 [lib]
@@ -105,3 +107,7 @@ bench = false
 [[example]]
 name = "circuit-layout"
 required-features = ["test-dev-graph"]
+
+[[example]]
+name = "dynamic-lookup"
+required-features = ["unstable-dynamic-lookups"]

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<Advice>,
+    // starts at zero to use as default
+    table_vals: Column<Advice>,
+    even: DynamicTable,
+    odd: DynamicTable,
+}
+
+struct DynLookupCircuit {}
+impl Circuit<Fp> for DynLookupCircuit {
+    type Config = EvenOddCircuitConfig;
+    type FloorPlanner = SimpleFloorPlanner;
+
+    fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+    ) -> 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<EqAffine> = Params::new(k);
+    let verifier = SingleVerifier::new(&params);
+    let vk = keygen_vk(&params, &DynLookupCircuit {}).unwrap();
+    let pk = keygen_pk(&params, vk, &DynLookupCircuit {}).unwrap();
+    let mut transcript = Blake2bWrite::<_, vesta::Affine, _>::init(vec![]);
+    create_proof(
+        &params,
+        &pk,
+        &[DynLookupCircuit {}],
+        &[&[]],
+        &mut OsRng,
+        &mut transcript,
+    )
+    .expect("Failed to create proof");
+
+    let proof: Vec<u8> = transcript.finalize();
+
+    let mut transcript = Blake2bRead::init(&proof[..]);
+    verify_proof(&params, pk.get_vk(), verifier, &[&[]], &mut transcript)
+        .expect("could not verify_proof");
+}

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] }]

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.

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<F> + 'a> RegionLayouter<F>
         )
     }
 
+    #[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),

halo2_proofs/src/circuit/floor_planner/v1.rs

@@ -374,6 +374,13 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> 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),

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<F>, CS: Assignment<F> + 'a> Layouter<C> for MyLayouter<'a, C, CS> {
+/// impl<'a, F: Field, C: Chip<F>, CS: Assignment<F> + 'a> Layouter<C> for MyLayouter<'a, C, CS> {
 ///     fn assign_region(
 ///         &mut self,
 ///         assignment: impl FnOnce(Region<'_, F, C>) -> Result<(), Error>,
@@ -49,6 +51,10 @@ pub trait RegionLayouter<F: Field>: 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,
@@ -127,6 +133,9 @@ pub enum RegionColumn {
     Column(Column<Any>),
     /// 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<Column<Any>> for RegionColumn {
@@ -141,13 +150,26 @@ impl From<Selector> for RegionColumn {
     }
 }
 
+#[cfg(feature = "unstable-dynamic-lookups")]
+impl From<TableTag> 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,
         }
     }
 }
@@ -197,6 +219,14 @@ impl<F: Field> RegionLayouter<F> 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),

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::{DynamicTable, 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>,
@@ -479,7 +497,7 @@ impl<F: Field> Assignment<F> for MockProver<F> {
     }
 }
 
-impl<F: Field + Ord> MockProver<F> {
+impl<F: Field + Ord + From<u64>> MockProver<F> {
     /// Runs a synthetic keygen-and-prove operation on the given circuit, collecting data
     /// about the constraints and their assignments.
     pub fn run<ConcreteCircuit: Circuit<F>>(
@@ -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,
         };
@@ -563,6 +585,21 @@ impl<F: Field + Ord> MockProver<F> {
             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)
     }
 
@@ -648,6 +685,8 @@ impl<F: Field + Ord> MockProver<F> {
                             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 +751,8 @@ impl<F: Field + Ord> MockProver<F> {
                         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();
@@ -875,12 +916,72 @@ impl<F: Field + Ord> MockProver<F> {
                 })
         };
 
-        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<F: Field>(
+                regions: &[Region],
+                cell: CellValue<F>,
+                dynamic_table: &DynamicTable,
+                column: Column<Any>,
+                row: usize,
+            ) -> Option<VerifyFailure> {
+                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 {
@@ -921,7 +1022,7 @@ impl<F: Field + Ord> MockProver<F> {
 #[cfg(test)]
 mod tests {
     use group::ff::Field;
-    use pasta_curves::Fp;
+    use pasta_curves::{EqAffine, Fp};
 
     use super::{FailureLocation, MockProver, VerifyFailure};
     use crate::{
@@ -1133,4 +1234,709 @@ 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<Advice>,
+            // A table containing table_vals.
+            table: DynamicTable,
+        }
+
+        impl DynLookupCircuitConfig {
+            fn assign_lookups(
+                &self,
+                layouter: &mut impl Layouter<Fp>,
+                lookup: impl Iterator<Item = usize> + 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 to remove code duplication
+        #[test]
+        fn dynamic_lookup_success() {
+            struct DynLookupCircuit {}
+            impl Circuit<Fp> for DynLookupCircuit {
+                type Config = DynLookupCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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<Fp> for DynLookupCircuit {
+                type Config = DynLookupCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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<Fp> for DynLookupCircuit {
+                type Config = DynLookupCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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<Fp> for DynLookupCircuit {
+                type Config = DynLookupCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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<Fp> for DynLookupCircuit {
+                type Config = DynLookupCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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<Fp> for DynLookupCircuit {
+                type Config = DynLookupCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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<Advice>,
+            even: DynamicTable,
+            odd: DynamicTable,
+        }
+
+        #[test]
+        fn even_odd_dyn_tables() {
+            struct DynLookupCircuit {}
+            impl Circuit<Fp> for DynLookupCircuit {
+                type Config = EvenOddCircuitConfig;
+                type FloorPlanner = SimpleFloorPlanner;
+
+                fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+                ) -> 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();
+        }
+    }
+
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    #[test]
+    fn failing() {
+        struct FailingCircuit {}
+        #[derive(Clone)]
+        struct FailingConfig {
+            first_input: Column<Advice>,
+            second_input: Column<Advice>,
+            is_first_table: Selector,
+            is_second_table: Selector,
+            first_table: crate::plonk::DynamicTable,
+            second_table: crate::plonk::DynamicTable,
+        }
+        impl Circuit<Fp> for FailingCircuit {
+            type Config = FailingConfig;
+            type FloorPlanner = SimpleFloorPlanner;
+
+            fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
+            ) -> 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();
+    }
 }

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,
@@ -271,6 +307,8 @@ impl<G: PrimeGroup, ConcreteCircuit: Circuit<G::Scalar>> CircuitCost<G, Concrete
         )
         .unwrap();
         let (cs, _) = cs.compress_selectors(layout.selectors);
+        #[cfg(feature = "unstable-dynamic-lookups")]
+        let (cs, _) = cs.compress_dynamic_table_tags(layout.dynamic_tables_assignments);
 
         assert!((1 << k) >= cs.minimum_rows());
 

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},
@@ -56,6 +58,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()],
@@ -109,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<Any>,
+        /// 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.
@@ -188,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,
@@ -375,6 +404,7 @@ fn render_constraint_not_satisfied<F: Field>(
     }
 }
 
+// TODO: handle dynamic lookups separately?
 /// Renders `VerifyFailure::Lookup`.
 ///
 /// ```text
@@ -411,18 +441,21 @@ fn render_lookup<F: Field>(
         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"),
             &|_| 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"),
+            &|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"),
         )
     });
@@ -467,6 +500,8 @@ fn render_lookup<F: Field>(
         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),

halo2_proofs/src/dev/failure/emitter.rs

@@ -103,6 +103,8 @@ pub(super) fn expression_to_string<F: Field>(
     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)

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

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

@@ -82,7 +82,7 @@ impl CircuitLayout {
     }
 
     /// Renders the given circuit on the given drawing area.
-    pub fn render<F: Field, ConcreteCircuit: Circuit<F>, DB: DrawingBackend>(
+    pub fn render<F: Field + From<u64>, ConcreteCircuit: Circuit<F>, DB: DrawingBackend>(
         self,
         k: u32,
         circuit: &ConcreteCircuit,
@@ -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,
@@ -106,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;
@@ -113,6 +122,8 @@ impl CircuitLayout {
             let column: Column<Any> = 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() {

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::{
@@ -234,6 +236,12 @@ impl<'r, F: Field> RegionLayouter<F> 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),
@@ -383,6 +391,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/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),

halo2_proofs/src/plonk/circuit.rs

@@ -13,6 +13,8 @@ use crate::{
 };
 
 mod compress_selectors;
+#[cfg(feature = "unstable-dynamic-lookups")]
+mod compress_table_tags;
 
 /// A column type
 pub trait ColumnType:
@@ -268,6 +270,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 +347,43 @@ impl TableColumn {
     }
 }
 
+/// `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<Column<Any>>,
+}
+
+#[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<Any>] {
+        &self.columns
+    }
+
+    /// Includes a row at `offset` in this dynamic lookup table.
+    pub fn add_row<F>(&self, region: &mut Region<F>, 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
 /// for a constraint system.
 pub trait Assignment<F: Field> {
@@ -369,6 +419,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.
@@ -491,6 +545,9 @@ pub enum Expression<F> {
     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
@@ -515,6 +572,7 @@ impl<F: Field> Expression<F> {
         &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,
@@ -526,6 +584,8 @@ impl<F: Field> Expression<F> {
         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),
@@ -533,6 +593,8 @@ impl<F: Field> Expression<F> {
                 let a = a.evaluate(
                     constant,
                     selector_column,
+                    #[cfg(feature = "unstable-dynamic-lookups")]
+                    table_tag,
                     fixed_column,
                     advice_column,
                     instance_column,
@@ -547,6 +609,8 @@ impl<F: Field> Expression<F> {
                 let a = a.evaluate(
                     constant,
                     selector_column,
+                    #[cfg(feature = "unstable-dynamic-lookups")]
+                    table_tag,
                     fixed_column,
                     advice_column,
                     instance_column,
@@ -558,6 +622,8 @@ impl<F: Field> Expression<F> {
                 let b = b.evaluate(
                     constant,
                     selector_column,
+                    #[cfg(feature = "unstable-dynamic-lookups")]
+                    table_tag,
                     fixed_column,
                     advice_column,
                     instance_column,
@@ -572,6 +638,8 @@ impl<F: Field> Expression<F> {
                 let a = a.evaluate(
                     constant,
                     selector_column,
+                    #[cfg(feature = "unstable-dynamic-lookups")]
+                    table_tag,
                     fixed_column,
                     advice_column,
                     instance_column,
@@ -583,6 +651,8 @@ impl<F: Field> Expression<F> {
                 let b = b.evaluate(
                     constant,
                     selector_column,
+                    #[cfg(feature = "unstable-dynamic-lookups")]
+                    table_tag,
                     fixed_column,
                     advice_column,
                     instance_column,
@@ -597,6 +667,8 @@ impl<F: Field> Expression<F> {
                 let a = a.evaluate(
                     constant,
                     selector_column,
+                    #[cfg(feature = "unstable-dynamic-lookups")]
+                    table_tag,
                     fixed_column,
                     advice_column,
                     instance_column,
@@ -615,6 +687,8 @@ impl<F: Field> Expression<F> {
         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,
@@ -635,6 +709,8 @@ impl<F: Field> Expression<F> {
         self.evaluate(
             &|_| false,
             &|selector| selector.is_simple(),
+            #[cfg(feature = "unstable-dynamic-lookups")]
+            &|_| false,
             &|_| false,
             &|_| false,
             &|_| false,
@@ -662,6 +738,8 @@ impl<F: Field> Expression<F> {
                     None
                 }
             },
+            #[cfg(feature = "unstable-dynamic-lookups")]
+            &|_| None,
             &|_| None,
             &|_| None,
             &|_| None,
@@ -678,6 +756,8 @@ impl<F: std::fmt::Debug> std::fmt::Debug for Expression<F> {
         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(vc) => f.debug_tuple("TableTag").field(vc).finish(),
             // Skip enum variant and print query struct directly to maintain backwards compatibility.
             Expression::Fixed(FixedQuery {
                 index,
@@ -941,6 +1021,12 @@ pub struct ConstraintSystem<F: Field> {
     /// fixed column that they were compressed into. This is just used by dev
     /// tooling right now.
     pub(crate) selector_map: Vec<Column<Fixed>>,
+    /// Like selector_map, but for dynamic tables.
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    pub(crate) dynamic_table_tag_map: Vec<Column<Fixed>>,
+
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    pub(crate) dynamic_tables: Vec<DynamicTable>,
 
     pub(crate) gates: Vec<Gate<F>>,
     pub(crate) advice_queries: Vec<(Column<Advice>, Rotation)>,
@@ -1001,6 +1087,10 @@ impl<F: Field> Default for ConstraintSystem<F> {
             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(),
@@ -1083,6 +1173,63 @@ impl<F: Field> ConstraintSystem<F> {
         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<F>, Column<Any>)>),
+    ) -> usize
+    where
+        F: From<u64>,
+    {
+        let mut cells = VirtualCells::new(self);
+        let (selector, table_map) = table_map(&mut cells);
+        let selector = cells.query_selector(selector);
+
+        let mut table_map: Vec<_> = table_map
+            .into_iter()
+            .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");
+                }
+
+                if input.contains_simple_selector() {
+                    panic!("input expression containing simple selector supplied to lookup argument");
+                }
+
+                let table_query = cells.query_any(table_col, 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<Fixed>) -> usize {
         // Return existing query, if it exists
         for (index, fixed_query) in self.fixed_queries.iter().enumerate() {
@@ -1227,6 +1374,80 @@ impl<F: Field> ConstraintSystem<F> {
         });
     }
 
+    #[cfg(feature = "unstable-dynamic-lookups")]
+    pub(crate) fn compress_dynamic_table_tags(
+        mut self,
+        dynamic_tables: Vec<Vec<bool>>,
+    ) -> (Self, Vec<Vec<F>>)
+    where
+        F: From<u64>,
+    {
+        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::<Vec<_>>();
+        let table_tag_replacements = table_tag_replacements
+            .into_iter()
+            .map(|a| a.unwrap())
+            .collect::<Vec<_>>();
+
+        // 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
@@ -1313,6 +1534,8 @@ impl<F: Field> ConstraintSystem<F> {
 
                     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),
@@ -1360,6 +1583,32 @@ impl<F: Field> ConstraintSystem<F> {
         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<String>,
+        fixed_columns: &[Column<Fixed>],
+        advice_columns: &[Column<Advice>],
+    ) -> DynamicTable {
+        let index = self.dynamic_tables.len();
+        let columns: Vec<_> = fixed_columns
+            .iter()
+            .map(|f| Column::<Any>::from(*f))
+            .chain(advice_columns.iter().map(|f| Column::<Any>::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 {

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::<Vec<_>>();
-
-    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<Item = bool>>(
+    virtual_columns: &'a [C],
+    rows: impl Fn(&'a C) -> A,
+) -> Vec<Vec<bool>> {
+    // 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::<Vec<_>>();
+
+    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::*;
@@ -318,6 +323,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);

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<bool>,
+}
+
+/// 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<F> {
+    /// 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<F>,
+}
+
+/// 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<Vec<F>>` 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<F: Field + From<u64>, E>(
+    tables: Vec<TableDescription>,
+    mut allocate_fixed_column: E,
+) -> (Vec<Vec<F>>, Vec<TableAssignment<F>>)
+where
+    E: FnMut() -> Expression<F>,
+{
+    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::<bool>(), assignment_size))
+                        -> Vec<bool> {
+            assignment
+        }
+    }
+
+    prop_compose! {
+        fn arb_table_list(assignment_size: usize, num_tables: impl Into<SizeRange>)
+                            (list in vec(arb_table(assignment_size), num_tables))
+                            -> Vec<TableDescription>
+        {
+            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<TableDescription>
+        {
+            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::<Fp, _>(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));
+                    }
+                }
+            }
+        }
+    }
+}

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,
     };
@@ -226,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);
@@ -267,6 +294,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,
     };
@@ -287,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()))

halo2_proofs/src/plonk/lookup/prover.rs

@@ -111,6 +111,8 @@ impl<F: WithSmallOrderMulGroup<3>> Argument<F> {
                     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<F: WithSmallOrderMulGroup<3>> Argument<F> {
                     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)

halo2_proofs/src/plonk/lookup/verifier.rs

@@ -120,6 +120,8 @@ impl<C: CurveAffine> Evaluated<C> {
                         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],

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>,
@@ -555,6 +564,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)

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