Integrate mv-lookup to verifier

Cargo.toml

@@ -35,7 +35,7 @@ inherits = "release"
 debug = true
 
 [patch."https://github.com/privacy-scaling-explorations/halo2.git"]
-halo2_proofs = { git = "https://github.com/scroll-tech/halo2.git", branch = "develop" }
+halo2_proofs = { git = "https://github.com/scroll-tech/halo2.git", branch = "develop-rc" }
 [patch."https://github.com/privacy-scaling-explorations/poseidon.git"]
 poseidon = { git = "https://github.com/scroll-tech/poseidon.git", branch = "scroll-dev-0220" }
 [patch."https://github.com/privacy-scaling-explorations/halo2curves.git"]

snark-verifier-sdk/src/tests/mod.rs

@@ -1,7 +1,7 @@
 use halo2_base::halo2_proofs;
 use halo2_proofs::{
     halo2curves::bn256::Fr,
-    plonk::{Advice, Column, ConstraintSystem, Fixed, Instance},
+    plonk::{Advice, Column, ConstraintSystem, Fixed, Instance, TableColumn},
     poly::Rotation,
 };
 use test_circuit_1::TestCircuit1;
@@ -25,13 +25,15 @@ pub struct StandardPlonkConfig {
     constant: Column<Fixed>,
     #[allow(dead_code)]
     instance: Column<Instance>,
+    table: TableColumn,
 }
 
 impl StandardPlonkConfig {
     fn configure(meta: &mut ConstraintSystem<Fr>) -> Self {
         let [a, b, c] = [(); 3].map(|_| meta.advice_column());
         let [q_a, q_b, q_c, q_ab, constant] = [(); 5].map(|_| meta.fixed_column());
         let instance = meta.instance_column();
+        let table = meta.lookup_table_column();
 
         [a, b, c].map(|column| meta.enable_equality(column));
 
@@ -53,6 +55,14 @@ impl StandardPlonkConfig {
             },
         );
 
-        StandardPlonkConfig { a, b, c, q_a, q_b, q_c, q_ab, constant, instance }
+        // Lookup for multiple times to test mv-lookup.
+        (0..5).for_each(|_| {
+            meta.lookup("lookup a", |meta| {
+                let a = meta.query_advice(a, Rotation::cur());
+                vec![(a, table)]
+            })
+        });
+
+        StandardPlonkConfig { a, b, c, q_a, q_b, q_c, q_ab, constant, instance, table }
     }
 }

snark-verifier-sdk/src/tests/single_layer_aggregation.rs

@@ -18,7 +18,7 @@ use std::path::Path;
 fn test_shplonk_then_sphplonk_with_evm_verification() {
     std::env::set_var("VERIFY_CONFIG", "./configs/example_evm_accumulator.config");
     let k = 8;
-    let k_agg = 21;
+    let k_agg = 24;
 
     let mut rng = test_rng();
     let params_outer = gen_srs(k_agg);
@@ -46,15 +46,15 @@ fn test_shplonk_then_sphplonk_with_evm_verification() {
     let snarks_2 = gen_snark_shplonk(
         &params_inner,
         &pk_inner_2,
-        circuit_1.clone(),
+        circuit_2.clone(),
         &mut rng,
         Some(Path::new("data/inner_2.snark")),
     );
     println!("finished snark generation for circuit 1");
 
     // Proof for circuit 2
     let circuit_3 = TestCircuit2::rand(&mut rng);
-    let pk_inner_3 = gen_pk(&params_inner, &circuit_1, Some(Path::new("data/inner_3.pkey")));
+    let pk_inner_3 = gen_pk(&params_inner, &circuit_3, Some(Path::new("data/inner_3.pkey")));
     let snarks_3 = gen_snark_shplonk(
         &params_inner,
         &pk_inner_3,

snark-verifier-sdk/src/tests/test_circuit_1.rs

@@ -66,6 +66,17 @@ impl Circuit<Fr> for TestCircuit1 {
                 a.copy_advice(|| "", &mut region, config.b, 3)?;
                 a.copy_advice(|| "", &mut region, config.c, 4)?;
 
+                Ok(())
+            },
+        )?;
+
+        layouter.assign_table(
+            || "lookup table for values of `a`",
+            |mut table| {
+                for (i, value) in [self.0, Fr::zero(), Fr::one(), -Fr::from(5)].iter().enumerate() {
+                    table.assign_cell(|| "", config.table, i, || Value::known(value))?;
+                }
+
                 Ok(())
             },
         )

snark-verifier-sdk/src/tests/test_circuit_2.rs

@@ -61,6 +61,17 @@ impl Circuit<Fr> for TestCircuit2 {
                 a.copy_advice(|| "", &mut region, config.b, 3)?;
                 a.copy_advice(|| "", &mut region, config.c, 4)?;
 
+                Ok(())
+            },
+        )?;
+
+        layouter.assign_table(
+            || "lookup table for values of `a`",
+            |mut table| {
+                for (i, value) in [self.0, Fr::zero(), Fr::one(), -Fr::from(5)].iter().enumerate() {
+                    table.assign_cell(|| "", config.table, i, || Value::known(value))?;
+                }
+
                 Ok(())
             },
         )

snark-verifier/src/system/halo2.rs

@@ -1,4 +1,5 @@
 //! [`halo2_proofs`] proof system
+//! Reference <https://hackmd.io/@dieGzUCgSGmRZFQ7SDxXCA/rk_0OgSla> for mv-lookup
 use crate::{
     halo2_proofs::{
         plonk::{
@@ -12,6 +13,7 @@ use crate::{
     },
     util::{
         arithmetic::{root_of_unity, CurveAffine, Domain, FieldExt, Rotation},
+        izip,
         protocol::{
             CommonPolynomial, Expression, InstanceCommittingKey, Query, QuotientPolynomial,
         },
@@ -116,7 +118,7 @@ pub fn compile<'a, C: CurveAffine, P: Params<'a, C>>(
         .chain(polynomials.random_query())
         .chain(polynomials.permutation_fixed_queries())
         .chain((0..num_proof).flat_map(move |t| polynomials.permutation_z_queries::<true>(t)))
-        .chain((0..num_proof).flat_map(move |t| polynomials.lookup_queries::<true>(t)))
+        .chain((0..num_proof).flat_map(move |t| polynomials.lookup_queries(t)))
         .collect();
 
     let queries = (0..num_proof)
@@ -125,7 +127,7 @@ pub fn compile<'a, C: CurveAffine, P: Params<'a, C>>(
                 .chain(polynomials.instance_queries(t))
                 .chain(polynomials.advice_queries(t))
                 .chain(polynomials.permutation_z_queries::<false>(t))
-                .chain(polynomials.lookup_queries::<false>(t))
+                .chain(polynomials.lookup_queries(t))
         })
         .chain(polynomials.fixed_queries())
         .chain(polynomials.permutation_fixed_queries())
@@ -180,10 +182,10 @@ struct Polynomials<'a, F: FieldExt> {
     num_challenge: Vec<usize>,
     advice_index: Vec<usize>,
     challenge_index: Vec<usize>,
-    num_lookup_permuted: usize,
+    num_lookup_m: usize,
     permutation_chunk_size: usize,
     num_permutation_z: usize,
-    num_lookup_z: usize,
+    num_lookup_phi: usize,
 }
 
 impl<'a, F: FieldExt> Polynomials<'a, F> {
@@ -236,13 +238,13 @@ impl<'a, F: FieldExt> Polynomials<'a, F> {
             num_challenge,
             advice_index,
             challenge_index,
-            num_lookup_permuted: 2 * cs.lookups().len(),
+            num_lookup_m: cs.lookups().len(),
             permutation_chunk_size,
             num_permutation_z: Integer::div_ceil(
                 &cs.permutation().get_columns().len(),
                 &permutation_chunk_size,
             ),
-            num_lookup_z: cs.lookups().len(),
+            num_lookup_phi: cs.lookups().len(),
         }
     }
 
@@ -258,8 +260,8 @@ impl<'a, F: FieldExt> Polynomials<'a, F> {
         iter::empty()
             .chain(self.num_advice.clone().iter().map(|num| self.num_proof * num))
             .chain([
-                self.num_proof * self.num_lookup_permuted,
-                self.num_proof * (self.num_permutation_z + self.num_lookup_z) + self.zk as usize,
+                self.num_proof * self.num_lookup_m,
+                self.num_proof * (self.num_permutation_z + self.num_lookup_phi) + self.zk as usize,
             ])
             .collect()
     }
@@ -376,40 +378,17 @@ impl<'a, F: FieldExt> Polynomials<'a, F> {
         }
     }
 
-    fn lookup_poly(&'a self, t: usize, i: usize) -> (usize, usize, usize) {
-        let permuted_offset = self.cs_witness_offset();
-        let z_offset = permuted_offset
-            + self.num_witness()[self.num_advice.len()]
-            + self.num_proof * self.num_permutation_z;
-        let z = z_offset + t * self.num_lookup_z + i;
-        let permuted_input = permuted_offset + 2 * (t * self.num_lookup_z + i);
-        let permuted_table = permuted_input + 1;
-        (z, permuted_input, permuted_table)
+    fn lookup_poly(&'a self, t: usize, i: usize) -> (usize, usize) {
+        let m = self.cs_witness_offset() + t * self.num_lookup_m + i;
+        let phi =
+            m + self.num_witness()[self.num_advice.len()] + self.num_proof * self.num_permutation_z;
+        (m, phi)
     }
 
-    fn lookup_queries<const EVAL: bool>(
-        &'a self,
-        t: usize,
-    ) -> impl IntoIterator<Item = Query> + 'a {
-        (0..self.num_lookup_z).flat_map(move |i| {
-            let (z, permuted_input, permuted_table) = self.lookup_poly(t, i);
-            if EVAL {
-                [
-                    Query::new(z, 0),
-                    Query::new(z, 1),
-                    Query::new(permuted_input, 0),
-                    Query::new(permuted_input, -1),
-                    Query::new(permuted_table, 0),
-                ]
-            } else {
-                [
-                    Query::new(z, 0),
-                    Query::new(permuted_input, 0),
-                    Query::new(permuted_table, 0),
-                    Query::new(permuted_input, -1),
-                    Query::new(z, 1),
-                ]
-            }
+    fn lookup_queries(&'a self, t: usize) -> impl IntoIterator<Item = Query> + 'a {
+        (0..self.num_lookup_phi).flat_map(move |i| {
+            let (m, phi) = self.lookup_poly(t, i);
+            [Query::new(phi, 0), Query::new(phi, 1), Query::new(m, 0)]
         })
     }
 
@@ -598,22 +577,18 @@ impl<'a, F: FieldExt> Polynomials<'a, F> {
     }
 
     fn lookup_constraints(&'a self, t: usize) -> impl IntoIterator<Item = Expression<F>> + 'a {
-        let one = &Expression::Constant(F::one());
         let l_0 = &Expression::<F>::CommonPolynomial(CommonPolynomial::Lagrange(0));
         let l_last = &self.l_last();
         let l_active = &self.l_active();
         let beta = &self.beta();
-        let gamma = &self.gamma();
 
-        let polys = (0..self.num_lookup_z)
+        let polys = (0..self.num_lookup_phi)
             .map(|i| {
-                let (z, permuted_input, permuted_table) = self.lookup_poly(t, i);
+                let (m, phi) = self.lookup_poly(t, i);
                 (
-                    Expression::<F>::Polynomial(Query::new(z, 0)),
-                    Expression::<F>::Polynomial(Query::new(z, 1)),
-                    Expression::<F>::Polynomial(Query::new(permuted_input, 0)),
-                    Expression::<F>::Polynomial(Query::new(permuted_input, -1)),
-                    Expression::<F>::Polynomial(Query::new(permuted_table, 0)),
+                    Expression::<F>::Polynomial(Query::new(phi, 0)),
+                    Expression::<F>::Polynomial(Query::new(phi, 1)),
+                    Expression::<F>::Polynomial(Query::new(m, 0)),
                 )
             })
             .collect_vec();
@@ -629,35 +604,38 @@ impl<'a, F: FieldExt> Polynomials<'a, F> {
             .lookups()
             .iter()
             .zip(polys.iter())
-            .flat_map(
-                |(
-                    lookup,
-                    (z, z_omega, permuted_input, permuted_input_omega_inv, permuted_table),
-                )| {
-                    let input = compress(lookup.input_expressions());
-                    let table = compress(lookup.table_expressions());
-                    iter::empty()
-                        .chain(Some(l_0 * (one - z)))
-                        .chain(self.zk.then(|| l_last * (z * z - z)))
-                        .chain(Some(if self.zk {
-                            l_active
-                                * (z_omega * (permuted_input + beta) * (permuted_table + gamma)
-                                    - z * (input + beta) * (table + gamma))
-                        } else {
-                            z_omega * (permuted_input + beta) * (permuted_table + gamma)
-                                - z * (input + beta) * (table + gamma)
-                        }))
-                        .chain(self.zk.then(|| l_0 * (permuted_input - permuted_table)))
-                        .chain(Some(if self.zk {
-                            l_active
-                                * (permuted_input - permuted_table)
-                                * (permuted_input - permuted_input_omega_inv)
-                        } else {
-                            (permuted_input - permuted_table)
-                                * (permuted_input - permuted_input_omega_inv)
-                        }))
-                },
-            )
+            .flat_map(|(lookup, (phi, phi_omega, m))| {
+                let inputs = lookup
+                    .input_expressions()
+                    .iter()
+                    .map(|expressions| compress(expressions) + beta)
+                    .collect_vec();
+                let table = &(compress(lookup.table_expressions()) + beta);
+                iter::empty().chain(Some(l_0 * phi)).chain(self.zk.then(|| l_last * phi)).chain(
+                    Some(if self.zk {
+                        let input_prod = &inputs.iter().cloned().product::<Expression<_>>();
+                        let lhs = table * input_prod * (phi_omega - phi);
+                        let rhs = (inputs.len() > 1)
+                            .then(|| {
+                                (0..inputs.len())
+                                    .map(|i| {
+                                        izip!(0.., &inputs)
+                                            .filter_map(|(j, input)| (i != j).then_some(input))
+                                            .cloned()
+                                            .product()
+                                    })
+                                    .sum::<Expression<_>>()
+                                    * table
+                            })
+                            .unwrap_or_else(|| table.clone())
+                            - m * input_prod;
+
+                        l_active * (lhs - rhs)
+                    } else {
+                        unimplemented!()
+                    }),
+                )
+            })
             .collect_vec()
     }
 

snark-verifier/src/util.rs

@@ -7,7 +7,7 @@ pub mod poly;
 pub mod protocol;
 pub mod transcript;
 
-pub(crate) use itertools::Itertools;
+pub(crate) use itertools::{izip, Itertools};
 
 #[cfg(feature = "parallel")]
 pub(crate) use rayon::current_num_threads;

snark-verifier/src/util/protocol.rs

@@ -14,7 +14,7 @@ use std::{
     collections::{BTreeMap, BTreeSet},
     fmt::Debug,
     iter::{
-        Sum, {self},
+        Product, Sum, {self},
     },
     ops::{Add, Mul, Neg, Sub},
 };
@@ -346,6 +346,12 @@ impl<F: Clone + Default> Sum for Expression<F> {
     }
 }
 
+impl<F: Field> Product for Expression<F> {
+    fn product<I: Iterator<Item = Self>>(iter: I) -> Self {
+        iter.reduce(|acc, item| acc * item).unwrap_or_else(|| Expression::Constant(F::one()))
+    }
+}
+
 impl<F: Field> One for Expression<F> {
     fn one() -> Self {
         Expression::Constant(F::one())