[WIP] Rebase dynamic lookups

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

@@ -89,7 +89,9 @@ beta = [
 ]
 nightly = [
     "beta",
+    "unstable-dynamic-lookups",
 ]
+unstable-dynamic-lookups = []
 # Add flags for in-development features above this line.
 
 [lib]
@@ -98,3 +100,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),