Implement Dynamic lookups

halo2_proofs/examples/dynamic_lookup.rs

@@ -0,0 +1,146 @@
+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, DynamicTableMap, 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());
+            let is_even = cells.query_selector(is_even);
+
+            DynamicTableMap {
+                selector: is_even,
+                table_map: vec![(a, table_vals.into())],
+            }
+        });
+
+        meta.lookup_dynamic(&odd, |cells| {
+            let a = cells.query_advice(a, Rotation::cur());
+            let is_odd = cells.query_selector(is_odd);
+
+            DynamicTableMap {
+                selector: is_odd,
+                table_map: 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/src/circuit.rs

@@ -6,7 +6,9 @@ use ff::Field;
 
 use crate::{
     arithmetic::FieldExt,
-    plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn},
+    plonk::{
+        Advice, Any, Assigned, Column, DynamicTable, Error, Fixed, Instance, Selector, TableColumn,
+    },
 };
 
 mod value;
@@ -204,6 +206,15 @@ impl<'r, F: Field> Region<'r, F> {
             .enable_selector(&|| annotation().into(), selector, offset)
     }
 
+    /// Includes a row at `offset` in this dynamic lookup table.
+    pub(crate) fn add_row_to_table(
+        &mut self,
+        table: DynamicTable,
+        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

@@ -11,8 +11,8 @@ use crate::{
         Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value,
     },
     plonk::{
-        Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance,
-        Selector, TableColumn,
+        Advice, Any, Assigned, Assignment, Circuit, Column, DynamicTable, Error, Fixed,
+        FloorPlanner, Instance, Selector, TableColumn,
     },
 };
 
@@ -275,6 +275,12 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
         )
     }
 
+    fn add_to_lookup(&mut self, table: DynamicTable, offset: usize) -> Result<(), Error> {
+        self.layouter
+            .cs
+            .add_row_to_table(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

@@ -391,6 +391,16 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
         )
     }
 
+    fn add_to_lookup(
+        &mut self,
+        table: crate::plonk::DynamicTable,
+        offset: usize,
+    ) -> Result<(), Error> {
+        self.plan
+            .cs
+            .add_row_to_table(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

@@ -7,7 +7,9 @@ use std::fmt;
 use ff::Field;
 
 use super::{Cell, RegionIndex, Value};
-use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn};
+use crate::plonk::{
+    Advice, Any, Assigned, Column, DynamicTable, Error, Fixed, Instance, Selector, TableColumn,
+};
 
 /// Helper trait for implementing a custom [`Layouter`].
 ///
@@ -48,6 +50,9 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
         offset: usize,
     ) -> Result<(), Error>;
 
+    /// Enables a selector at the given offset.
+    fn add_to_lookup(&mut self, table: DynamicTable, offset: usize) -> Result<(), Error>;
+
     /// Assign an advice column value (witness)
     fn assign_advice<'v>(
         &'v mut self,
@@ -144,6 +149,8 @@ pub enum RegionColumn {
     Column(Column<Any>),
     /// Virtual column representing a (boolean) selector
     Selector(Selector),
+    /// Virtual column used for storing dynamic table tags
+    TableTag(DynamicTable),
 }
 
 impl From<Column<Any>> for RegionColumn {
@@ -158,13 +165,22 @@ impl From<Selector> for RegionColumn {
     }
 }
 
+impl From<DynamicTable> for RegionColumn {
+    fn from(table: DynamicTable) -> RegionColumn {
+        RegionColumn::TableTag(table)
+    }
+}
+
 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,
+            (Self::TableTag(ref a), Self::TableTag(ref b)) => a.cmp(b),
+            (Self::Column(_), _) => cmp::Ordering::Less,
             (Self::Selector(_), Self::Column(_)) => cmp::Ordering::Greater,
+            (Self::TableTag(_), _) => cmp::Ordering::Greater,
+            (_, Self::TableTag(_)) => cmp::Ordering::Less,
         }
     }
 }
@@ -214,6 +230,13 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
         Ok(())
     }
 
+    fn add_to_lookup(&mut self, table: DynamicTable, 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),