feat: conditional compilation of lookup args (#5)

.github/workflows/ci.yml

@@ -17,9 +17,9 @@ jobs:
         os: [ubuntu-latest, windows-latest, macOS-latest]
         include:
           - feature_set: basic
-            features: batch,dev-graph,gadget-traces
+            features: batch,dev-graph,gadget-traces,multicore
           - feature_set: all
-            features: batch,dev-graph,gadget-traces,multicore,test-dev-graph,thread-safe-region,sanity-checks,circuit-params
+            features: batch,dev-graph,gadget-traces,multicore,test-dev-graph,thread-safe-region,sanity-checks,circuit-params,mv-lookup
 
     steps:
       - uses: actions/checkout@v3
@@ -53,6 +53,11 @@ jobs:
         with:
           command: build
           args: --no-default-features --features batch,dev-graph,gadget-traces --target ${{ matrix.target }}
+      - name: cargo build mv-lookup
+        uses: actions-rs/cargo@v1
+        with:
+          command: build
+          args: --no-default-features --features batch,dev-graph,gadget-traces,mv-lookup --target ${{ matrix.target }}
 
   bitrot:
     name: Bitrot check
@@ -68,7 +73,7 @@ jobs:
         uses: actions-rs/cargo@v1
         with:
           command: build
-          args: --benches --examples --all-features
+          args: --benches --examples
 
   doc-links:
     name: Intra-doc links

halo2_proofs/Cargo.toml

@@ -100,6 +100,7 @@ batch = ["rand_core/getrandom"]
 circuit-params = []
 counter = ["lazy_static"]
 icicle_gpu = ["icicle", "rustacuda"]
+mv-lookup = []
 
 [lib]
 bench = false

halo2_proofs/examples/shuffle.rs

@@ -57,11 +57,11 @@ impl<const W: usize> MyConfig<W> {
     fn configure<F: Field>(meta: &mut ConstraintSystem<F>) -> Self {
         let [q_shuffle, q_first, q_last] = [(); 3].map(|_| meta.selector());
         // First phase
-        let original = [(); W].map(|_| meta.advice_column_in(FirstPhase, true));
-        let shuffled = [(); W].map(|_| meta.advice_column_in(FirstPhase, true));
+        let original = [(); W].map(|_| meta.advice_column_in(FirstPhase));
+        let shuffled = [(); W].map(|_| meta.advice_column_in(FirstPhase));
         let [theta, gamma] = [(); 2].map(|_| meta.challenge_usable_after(FirstPhase));
         // Second phase
-        let z = meta.advice_column_in(SecondPhase, true);
+        let z = meta.advice_column_in(SecondPhase);
 
         meta.create_gate("z should start with 1", |_| {
             let one = Expression::Constant(F::ONE);

halo2_proofs/examples/simple-lookup-unblinded.rs

@@ -67,7 +67,7 @@ fn main() {
             meta.enable_equality(config.instance);
             meta.enable_equality(config.other_advice);
 
-            let _ = meta.lookup("", |cs| {
+            meta.lookup("", |cs| {
                 let qlookup = cs.query_selector(config.qlookup);
                 let not_qlookup = Expression::Constant(F::ONE) - qlookup.clone();
                 let (default_x, default_y): (F, F) = (F::from(0), F::from(0));

halo2_proofs/examples/simple-lookup.rs

@@ -67,7 +67,7 @@ fn main() {
             meta.enable_equality(config.instance);
             meta.enable_equality(config.other_advice);
 
-            let _ = meta.lookup("", |cs| {
+            meta.lookup("", |cs| {
                 let qlookup = cs.query_selector(config.qlookup);
                 let not_qlookup = Expression::Constant(F::ONE) - qlookup.clone();
                 let (default_x, default_y): (F, F) = (F::from(0), F::from(0));

halo2_proofs/src/arithmetic.rs

@@ -146,7 +146,8 @@ pub fn small_multiexp<C: CurveAffine>(coeffs: &[C::Scalar], bases: &[C]) -> C::C
 #[cfg(feature = "icicle_gpu")]
 /// Performs a multi-exponentiation operation on GPU using Icicle library
 pub fn best_multiexp_gpu<C: CurveAffine>(coeffs: &[C::Scalar], is_lagrange: bool) -> C::Curve {
-    let scalars_ptr: DeviceBuffer<::icicle::curves::bn254::ScalarField_BN254> = icicle::copy_scalars_to_device::<C>(coeffs);
+    let scalars_ptr: DeviceBuffer<::icicle::curves::bn254::ScalarField_BN254> =
+        icicle::copy_scalars_to_device::<C>(coeffs);
 
     return icicle::multiexp_on_device::<C>(scalars_ptr, is_lagrange);
 }

halo2_proofs/src/dev.rs

@@ -615,6 +615,7 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
         let config = ConcreteCircuit::configure_with_params(&mut cs, circuit.params());
         #[cfg(not(feature = "circuit-params"))]
         let config = ConcreteCircuit::configure(&mut cs);
+        #[cfg(feature = "mv-lookup")]
         let cs = cs.chunk_lookups();
         let cs = cs;
 
@@ -840,7 +841,6 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
                         (self.n as usize - (self.cs.blinding_factors() + 1))..(self.n as usize);
                     (gate_row_ids
                         .clone()
-                        .into_iter()
                         .chain(blinding_rows.into_iter()))
                     .flat_map(move |row| {
                         let row = row as i32 + n;
@@ -943,6 +943,7 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
         let mut cached_table = Vec::new();
         let mut cached_table_identifier = Vec::new();
         // Check that all lookups exist in their respective tables.
+        #[cfg(feature = "mv-lookup")]
         let lookup_errors =
             self.cs
                 .lookups
@@ -1086,6 +1087,105 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
                         .collect::<Vec<_>>()
                 });
 
+        #[cfg(not(feature = "mv-lookup"))]
+        // Check that all lookups exist in their respective tables.
+        let lookup_errors =
+            self.cs
+                .lookups
+                .iter()
+                .enumerate()
+                .flat_map(|(lookup_index, lookup)| {
+                    assert!(lookup.table_expressions.len() == lookup.input_expressions.len());
+                    assert!(self.usable_rows.end > 0);
+
+                    // We optimize on the basis that the table might have been filled so that the last
+                    // usable row now has the fill contents (it doesn't matter if there was no filling).
+                    // Note that this "fill row" necessarily exists in the table, and we use that fact to
+                    // slightly simplify the optimization: we're only trying to check that all input rows
+                    // are contained in the table, and so we can safely just drop input rows that
+                    // match the fill row.
+                    let fill_row: Vec<_> = lookup
+                        .table_expressions
+                        .iter()
+                        .map(move |c| load(c, self.usable_rows.end - 1))
+                        .collect();
+
+                    let table_identifier = lookup
+                        .table_expressions
+                        .iter()
+                        .map(Expression::identifier)
+                        .collect::<Vec<_>>();
+                    if table_identifier != cached_table_identifier {
+                        cached_table_identifier = table_identifier;
+
+                        // In the real prover, the lookup expressions are never enforced on
+                        // unusable rows, due to the (1 - (l_last(X) + l_blind(X))) term.
+                        cached_table = self
+                            .usable_rows
+                            .clone()
+                            .filter_map(|table_row| {
+                                let t = lookup
+                                    .table_expressions
+                                    .iter()
+                                    .map(move |c| load(c, table_row))
+                                    .collect();
+
+                                if t != fill_row {
+                                    Some(t)
+                                } else {
+                                    None
+                                }
+                            })
+                            .collect();
+                        cached_table.sort_unstable();
+                    }
+                    let table = &cached_table;
+
+                    let mut inputs: Vec<(Vec<_>, usize)> = lookup_input_row_ids
+                        .clone()
+                        .filter_map(|input_row| {
+                            let t = lookup
+                                .input_expressions
+                                .iter()
+                                .map(move |c| load(c, input_row))
+                                .collect();
+
+                            if t != fill_row {
+                                // Also keep track of the original input row, since we're going to sort.
+                                Some((t, input_row))
+                            } else {
+                                None
+                            }
+                        })
+                        .collect();
+                    inputs.sort_unstable();
+
+                    let mut i = 0;
+                    inputs
+                        .iter()
+                        .filter_map(move |(input, input_row)| {
+                            while i < table.len() && &table[i] < input {
+                                i += 1;
+                            }
+                            if i == table.len() || &table[i] > input {
+                                assert!(table.binary_search(input).is_err());
+
+                                Some(VerifyFailure::Lookup {
+                                    lookup_index,
+                                    location: FailureLocation::find_expressions(
+                                        &self.cs,
+                                        &self.regions,
+                                        *input_row,
+                                        lookup.input_expressions.iter(),
+                                    ),
+                                })
+                            } else {
+                                None
+                            }
+                        })
+                        .collect::<Vec<_>>()
+                });
+
         let shuffle_errors =
             self.cs
                 .shuffles
@@ -1112,7 +1212,6 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
                     let mut input_rows: Vec<(Vec<Value<F>>, usize)> = self
                         .usable_rows
                         .clone()
-                        .into_iter()
                         .map(|input_row| {
                             let t = shuffle
                                 .input_expressions
@@ -1195,13 +1294,23 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
             })
         };
 
+        #[cfg(feature = "mv-lookup")]
         let mut errors: Vec<_> = iter::empty()
             .chain(selector_errors)
             .chain(gate_errors)
             .chain(lookup_errors.flatten())
             .chain(perm_errors)
             .chain(shuffle_errors)
             .collect();
+        #[cfg(not(feature = "mv-lookup"))]
+        let mut errors: Vec<_> = iter::empty()
+            .chain(selector_errors)
+            .chain(gate_errors)
+            .chain(lookup_errors)
+            .chain(perm_errors)
+            .chain(shuffle_errors)
+            .collect();
+
         if errors.is_empty() {
             Ok(())
         } else {
@@ -1442,6 +1551,7 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
         let mut cached_table = Vec::new();
         let mut cached_table_identifier = Vec::new();
         // Check that all lookups exist in their respective tables.
+        #[cfg(feature = "mv-lookup")]
         let lookup_errors =
             self.cs
                 .lookups
@@ -1572,6 +1682,101 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
                         .collect::<Vec<_>>()
                 });
 
+        #[cfg(not(feature = "mv-lookup"))]
+        // Check that all lookups exist in their respective tables.
+        let lookup_errors =
+            self.cs
+                .lookups
+                .iter()
+                .enumerate()
+                .flat_map(|(lookup_index, lookup)| {
+                    assert!(lookup.table_expressions.len() == lookup.input_expressions.len());
+                    assert!(self.usable_rows.end > 0);
+
+                    // We optimize on the basis that the table might have been filled so that the last
+                    // usable row now has the fill contents (it doesn't matter if there was no filling).
+                    // Note that this "fill row" necessarily exists in the table, and we use that fact to
+                    // slightly simplify the optimization: we're only trying to check that all input rows
+                    // are contained in the table, and so we can safely just drop input rows that
+                    // match the fill row.
+                    let fill_row: Vec<_> = lookup
+                        .table_expressions
+                        .iter()
+                        .map(move |c| load(c, self.usable_rows.end - 1))
+                        .collect();
+
+                    let table_identifier = lookup
+                        .table_expressions
+                        .iter()
+                        .map(Expression::identifier)
+                        .collect::<Vec<_>>();
+                    if table_identifier != cached_table_identifier {
+                        cached_table_identifier = table_identifier;
+
+                        // In the real prover, the lookup expressions are never enforced on
+                        // unusable rows, due to the (1 - (l_last(X) + l_blind(X))) term.
+                        cached_table = self
+                            .usable_rows
+                            .clone()
+                            .into_par_iter()
+                            .filter_map(|table_row| {
+                                let t = lookup
+                                    .table_expressions
+                                    .iter()
+                                    .map(move |c| load(c, table_row))
+                                    .collect();
+
+                                if t != fill_row {
+                                    Some(t)
+                                } else {
+                                    None
+                                }
+                            })
+                            .collect();
+                        cached_table.par_sort_unstable();
+                    }
+                    let table = &cached_table;
+
+                    let mut inputs: Vec<(Vec<_>, usize)> = lookup_input_row_ids
+                        .clone()
+                        .into_par_iter()
+                        .filter_map(|input_row| {
+                            let t = lookup
+                                .input_expressions
+                                .iter()
+                                .map(move |c| load(c, input_row))
+                                .collect();
+
+                            if t != fill_row {
+                                // Also keep track of the original input row, since we're going to sort.
+                                Some((t, input_row))
+                            } else {
+                                None
+                            }
+                        })
+                        .collect();
+                    inputs.par_sort_unstable();
+
+                    inputs
+                        .par_iter()
+                        .filter_map(move |(input, input_row)| {
+                            if table.binary_search(input).is_err() {
+                                Some(VerifyFailure::Lookup {
+                                    lookup_index,
+                                    location: FailureLocation::find_expressions(
+                                        &self.cs,
+                                        &self.regions,
+                                        *input_row,
+                                        lookup.input_expressions.iter(),
+                                    ),
+                                })
+                            } else {
+                                None
+                            }
+                        })
+                        .collect::<Vec<_>>()
+                });
+
         let shuffle_errors =
             self.cs
                 .shuffles
@@ -1598,7 +1803,6 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
                     let mut input_rows: Vec<(Vec<Value<F>>, usize)> = self
                         .usable_rows
                         .clone()
-                        .into_iter()
                         .map(|input_row| {
                             let t = shuffle
                                 .input_expressions
@@ -1681,13 +1885,22 @@ impl<F: FromUniformBytes<64> + Ord> MockProver<F> {
             })
         };
 
+        #[cfg(feature = "mv-lookup")]
         let mut errors: Vec<_> = iter::empty()
             .chain(selector_errors)
             .chain(gate_errors)
             .chain(lookup_errors.flatten())
             .chain(perm_errors)
             .chain(shuffle_errors)
             .collect();
+        #[cfg(not(feature = "mv-lookup"))]
+        let mut errors: Vec<_> = iter::empty()
+            .chain(selector_errors)
+            .chain(gate_errors)
+            .chain(lookup_errors)
+            .chain(perm_errors)
+            .chain(shuffle_errors)
+            .collect();
         if errors.is_empty() {
             Ok(())
         } else {