feat: logup

Cargo.toml

@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2", tag = "v2023_04_20" }
+halo2_proofs = { git = "https://github.com/han0110/halo2", branch = "feature/logup" }
 askama = { version = "0.12.0", features = ["config"], default-features = false }
 hex = "0.4.3"
 ruint = "1.10.1"
@@ -29,3 +29,6 @@ evm = ["dep:revm"]
 [[example]]
 name = "separately"
 required-features = ["evm"]
+
+[patch."https://github.com/privacy-scaling-explorations/halo2"]
+halo2_proofs = { git = "https://github.com/han0110/halo2", branch = "feature/logup" }

src/codegen/evaluator.rs

@@ -121,75 +121,110 @@ where
     }
 
     pub fn lookup_computations(&self) -> Vec<(Vec<String>, String)> {
-        let input_tables = self
+        let evaluate = |expressions: &Vec<_>| {
+            let (lines, inputs) = expressions
+                .iter()
+                .map(|expression| self.evaluate(expression))
+                .fold((Vec::new(), Vec::new()), |mut acc, result| {
+                    acc.0.extend(result.0);
+                    acc.1.push(result.1);
+                    acc
+                });
+            self.reset();
+            (lines, inputs)
+        };
+        let inputs_tables = self
             .cs
             .lookups()
             .iter()
             .map(|lookup| {
-                let [(input_lines, inputs), (table_lines, tables)] =
-                    [lookup.input_expressions(), lookup.table_expressions()].map(|expressions| {
-                        let (lines, inputs) = expressions
-                            .iter()
-                            .map(|expression| self.evaluate(expression))
-                            .fold((Vec::new(), Vec::new()), |mut acc, result| {
-                                acc.0.extend(result.0);
-                                acc.1.push(result.1);
-                                acc
-                            });
-                        self.reset();
-                        (lines, inputs)
-                    });
-                (input_lines, inputs, table_lines, tables)
+                let inputs = lookup
+                    .input_expressions()
+                    .iter()
+                    .map(evaluate)
+                    .collect_vec();
+                let table = evaluate(lookup.table_expressions());
+                (inputs, table)
             })
             .collect_vec();
-        izip!(input_tables, &self.data.lookup_evals)
-            .flat_map(|(input_table, evals)| {
-                let (input_lines, inputs, table_lines, tables) = input_table;
-                let (input_0, rest_inputs) = inputs.split_first().unwrap();
+        izip!(inputs_tables, &self.data.lookup_evals)
+            .flat_map(|(inputs_tables, evals)| {
+                let (inputs, (table_lines, tables)) = inputs_tables;
+                let num_inputs = inputs.len();
                 let (table_0, rest_tables) = tables.split_first().unwrap();
-                let (z, z_next, p_input, p_input_prev, p_table) = evals;
+                let (phi, phi_next, m) = evals;
                 [
                     vec![
                         format!("let l_0 := mload(L_0_MPTR)"),
-                        format!("let eval := addmod(l_0, mulmod(l_0, sub(r, {z}), r), r)"),
+                        format!("let eval := mulmod(l_0, {phi}, r)"),
+                    ],
+                    vec![
+                        format!("let l_last := mload(L_LAST_MPTR)"),
+                        format!("let eval := mulmod(l_last, {phi}, r)"),
                     ],
-                    {
-                        let item = format!("addmod(mulmod({z}, {z}, r), sub(r, {z}), r)");
-                        vec![
-                            format!("let l_last := mload(L_LAST_MPTR)"),
-                            format!("let eval := mulmod(l_last, {item}, r)"),
-                        ]
-                    },
                     chain![
-                        ["let theta := mload(THETA_MPTR)", "let input"].map(str::to_string),
-                        code_block::<1, false>(chain![
-                            input_lines,
-                            [format!("input := {input_0}")],
-                            rest_inputs.iter().map(|input| format!(
-                                "input := addmod(mulmod(input, theta, r), {input}, r)"
-                            ))
-                        ]),
-                        ["let table"].map(str::to_string),
+                        [
+                            "let theta := mload(THETA_MPTR)",
+                            "let beta := mload(BETA_MPTR)",
+                            "let table"
+                        ]
+                        .map(str::to_string),
                         code_block::<1, false>(chain![
                             table_lines,
                             [format!("table := {table_0}")],
                             rest_tables.iter().map(|table| format!(
                                 "table := addmod(mulmod(table, theta, r), {table}, r)"
-                            ))
+                            )),
+                            [format!("table := addmod(table, beta, r)")],
                         ]),
-                        {
-                            let lhs = format!("addmod({p_input}, beta, r)");
-                            let rhs = format!("addmod({p_table}, gamma, r)");
-                            let permuted = format!("mulmod({lhs}, {rhs}, r)");
-                            let input =
-                                "mulmod(addmod(input, beta, r), addmod(table, gamma, r), r)";
-                            [
-                                format!("let beta := mload(BETA_MPTR)"),
-                                format!("let gamma := mload(GAMMA_MPTR)"),
-                                format!("let lhs := mulmod({z_next}, {permuted}, r)"),
-                                format!("let rhs := mulmod({z}, {input}, r)"),
+                        izip!(0.., inputs.into_iter()).flat_map(|(idx, (input_lines, inputs))| {
+                            let (input_0, rest_inputs) = inputs.split_first().unwrap();
+                            let ident = format!("input_{idx}");
+                            chain![
+                                [format!("let {ident}")],
+                                code_block::<1, false>(chain![
+                                    input_lines,
+                                    [format!("{ident} := {input_0}")],
+                                    rest_inputs.iter().map(|input| format!(
+                                        "{ident} := addmod(mulmod({ident}, theta, r), {input}, r)"
+                                    )),
+                                    [format!("{ident} := addmod({ident}, beta, r)")],
+                                ]),
                             ]
-                        },
+                        }),
+                        [format!("let lhs"), format!("let rhs")],
+                        (0..num_inputs).flat_map(|i| {
+                            assert_ne!(num_inputs, 0);
+                            if num_inputs == 1 {
+                                vec![format!("rhs := table")]
+                            } else {
+                                let idents = (0..num_inputs)
+                                    .filter(|j| *j != i)
+                                    .map(|idx| format!("input_{idx}"))
+                                    .collect_vec();
+                                let (ident_0, rest_idents) = idents.split_first().unwrap();
+                                code_block::<1, false>(chain![
+                                    [format!("let tmp := {ident_0}")],
+                                    chain![rest_idents]
+                                        .map(|ident| format!("tmp := mulmod(tmp, {ident}, r)")),
+                                    [format!("rhs := addmod(rhs, tmp, r)"),],
+                                    (i == num_inputs - 1)
+                                        .then(|| format!("rhs := mulmod(rhs, table, r)")),
+                                ])
+                            }
+                        }),
+                        code_block::<1, false>(chain![
+                            [format!("let tmp := input_0")],
+                            (1..num_inputs)
+                                .map(|idx| format!("tmp := mulmod(tmp, input_{idx}, r)")),
+                            [
+                                format!("rhs := addmod(rhs, sub(r, mulmod({m}, tmp, r)), r)"),
+                                {
+                                    let item = format!("addmod({phi_next}, sub(r, {phi}), r)");
+                                    format!("lhs := mulmod(mulmod(table, tmp, r), {item}, r)")
+                                },
+                            ],
+                        ]),
                         {
                             let l_inactive = "addmod(mload(L_BLIND_MPTR), mload(L_LAST_MPTR), r)";
                             let l_active = format!("addmod(1, sub(r, {l_inactive}), r)");
@@ -199,20 +234,6 @@ where
                         },
                     ]
                     .collect_vec(),
-                    {
-                        let l_0 = "mload(L_0_MPTR)";
-                        let item = format!("addmod({p_input}, sub(r, {p_table}), r)");
-                        vec![format!("let eval := mulmod({l_0}, {item}, r)")]
-                    },
-                    {
-                        let l_inactive = "addmod(mload(L_BLIND_MPTR), mload(L_LAST_MPTR), r)";
-                        let l_active = format!("addmod(1, sub(r, {l_inactive}), r)");
-                        let lhs = format!("addmod({p_input}, sub(r, {p_table}), r)");
-                        let rhs = format!("addmod({p_input}, sub(r, {p_input_prev}), r)");
-                        vec![format!(
-                            "let eval := mulmod({l_active}, mulmod({lhs}, {rhs}, r), r)"
-                        )]
-                    },
                 ]
             })
             .zip(iter::repeat("eval".to_string()))

src/codegen/pcs.rs

@@ -47,17 +47,15 @@ pub(crate) fn queries(meta: &ConstraintSystemMeta, data: &Data) -> Vec<Query> {
             .skip(1)
             .map(|(&comm, evals)| Query::new(comm, meta.rotation_last, evals.2)),
         izip!(
-            &data.lookup_permuted_comms,
-            &data.lookup_z_comms,
+            &data.lookup_m_comms,
+            &data.lookup_phi_comms,
             &data.lookup_evals
         )
-        .flat_map(|(permuted_comms, &z_comm, evals)| {
+        .flat_map(|(&m_comm, &phi_comm, evals)| {
             [
-                Query::new(z_comm, 0, evals.0),
-                Query::new(permuted_comms.0, 0, evals.2),
-                Query::new(permuted_comms.1, 0, evals.4),
-                Query::new(permuted_comms.0, -1, evals.3),
-                Query::new(z_comm, 1, evals.1),
+                Query::new(phi_comm, 0, evals.0),
+                Query::new(phi_comm, 1, evals.1),
+                Query::new(m_comm, 0, evals.2),
             ]
         }),
         meta.fixed_queries.iter().map(|query| {

src/codegen/util.rs

@@ -20,9 +20,9 @@ pub(crate) struct ConstraintSystemMeta {
     pub(crate) num_fixeds: usize,
     pub(crate) permutation_columns: Vec<Column<Any>>,
     pub(crate) permutation_chunk_len: usize,
-    pub(crate) num_lookup_permuteds: usize,
+    pub(crate) num_lookup_ms: usize,
     pub(crate) num_permutation_zs: usize,
-    pub(crate) num_lookup_zs: usize,
+    pub(crate) num_lookup_phis: usize,
     pub(crate) num_quotients: usize,
     pub(crate) advice_queries: Vec<(usize, i32)>,
     pub(crate) fixed_queries: Vec<(usize, i32)>,
@@ -39,13 +39,13 @@ impl ConstraintSystemMeta {
         let num_fixeds = cs.num_fixed_columns();
         let permutation_columns = cs.permutation().get_columns();
         let permutation_chunk_len = cs.degree() - 2;
-        let num_lookup_permuteds = 2 * cs.lookups().len();
+        let num_lookup_ms = cs.lookups().len();
         let num_permutation_zs = cs
             .permutation()
             .get_columns()
             .chunks(cs.degree() - 2)
             .count();
-        let num_lookup_zs = cs.lookups().len();
+        let num_lookup_phis = cs.lookups().len();
         let num_quotients = cs.degree() - 1;
         let advice_queries = cs
             .advice_queries()
@@ -62,7 +62,7 @@ impl ConstraintSystemMeta {
             + 1
             + cs.permutation().get_columns().len()
             + (3 * num_permutation_zs - 1)
-            + 5 * cs.lookups().len();
+            + 3 * cs.lookups().len();
         let num_phase = *cs.advice_column_phase().iter().max().unwrap_or(&0) as usize + 1;
         // Indices of advice and challenge are not same as their position in calldata/memory,
         // because we support multiple phases, we need to remap them and find their actual indices.
@@ -95,9 +95,9 @@ impl ConstraintSystemMeta {
             num_fixeds,
             permutation_columns,
             permutation_chunk_len,
-            num_lookup_permuteds,
+            num_lookup_ms,
             num_permutation_zs,
-            num_lookup_zs,
+            num_lookup_phis,
             num_quotients,
             advice_queries,
             fixed_queries,
@@ -113,10 +113,10 @@ impl ConstraintSystemMeta {
     pub(crate) fn num_advices(&self) -> Vec<usize> {
         chain![
             self.num_user_advices.iter().cloned(),
-            (self.num_lookup_permuteds != 0).then_some(self.num_lookup_permuteds), // lookup permuted
+            (self.num_lookup_ms != 0).then_some(self.num_lookup_ms), // lookup permuted
             [
-                self.num_permutation_zs + self.num_lookup_zs + 1, // permutation and lookup grand products, random
-                self.num_quotients,                               // quotients
+                self.num_permutation_zs + self.num_lookup_phis + 1, // permutation and lookup grand products, random
+                self.num_quotients,                                 // quotients
             ],
         ]
         .collect()
@@ -127,7 +127,7 @@ impl ConstraintSystemMeta {
         // If there is no lookup used, merge also beta and gamma into the last user phase, to avoid
         // squeezing challenge from nothing.
         // Otherwise, merge theta into last user phase since they are originally adjacent.
-        if self.num_lookup_permuteds == 0 {
+        if self.num_lookup_ms == 0 {
             *num_challenges.last_mut().unwrap() += 3; // theta, beta, gamma
             num_challenges.extend([
                 1, // y
@@ -149,7 +149,7 @@ impl ConstraintSystemMeta {
     }
 
     pub(crate) fn num_lookups(&self) -> usize {
-        self.num_lookup_zs
+        self.num_lookup_phis
     }
 
     pub(crate) fn proof_len(&self, scheme: BatchOpenScheme) -> usize {
@@ -179,9 +179,9 @@ pub(crate) struct Data {
     pub(crate) fixed_comms: Vec<EcPoint>,
     pub(crate) permutation_comms: HashMap<Column<Any>, EcPoint>,
     pub(crate) advice_comms: Vec<EcPoint>,
-    pub(crate) lookup_permuted_comms: Vec<(EcPoint, EcPoint)>,
+    pub(crate) lookup_m_comms: Vec<EcPoint>,
     pub(crate) permutation_z_comms: Vec<EcPoint>,
-    pub(crate) lookup_z_comms: Vec<EcPoint>,
+    pub(crate) lookup_phi_comms: Vec<EcPoint>,
     pub(crate) random_comm: EcPoint,
 
     pub(crate) challenges: Vec<Word>,
@@ -192,7 +192,7 @@ pub(crate) struct Data {
     pub(crate) random_eval: Word,
     pub(crate) permutation_evals: HashMap<Column<Any>, Word>,
     pub(crate) permutation_z_evals: Vec<(Word, Word, Word)>,
-    pub(crate) lookup_evals: Vec<(Word, Word, Word, Word, Word)>,
+    pub(crate) lookup_evals: Vec<(Word, Word, Word)>,
 
     pub(crate) computed_quotient_comm: EcPoint,
     pub(crate) computed_quotient_eval: Word,
@@ -211,10 +211,10 @@ impl Data {
         let theta_mptr = challenge_mptr + meta.challenge_indices.len();
 
         let advice_comm_start = proof_cptr;
-        let lookup_permuted_comm_start = advice_comm_start + 2 * meta.advice_indices.len();
-        let permutation_z_comm_start = lookup_permuted_comm_start + 2 * meta.num_lookup_permuteds;
-        let lookup_z_comm_start = permutation_z_comm_start + 2 * meta.num_permutation_zs;
-        let random_comm_start = lookup_z_comm_start + 2 * meta.num_lookup_zs;
+        let lookup_m_comm_start = advice_comm_start + 2 * meta.advice_indices.len();
+        let permutation_z_comm_start = lookup_m_comm_start + 2 * meta.num_lookup_ms;
+        let lookup_phi_comm_start = permutation_z_comm_start + 2 * meta.num_permutation_zs;
+        let random_comm_start = lookup_phi_comm_start + 2 * meta.num_lookup_phis;
         let quotient_comm_start = random_comm_start + 2;
 
         let eval_cptr = quotient_comm_start + 2 * meta.num_quotients;
@@ -224,7 +224,7 @@ impl Data {
         let permutation_eval_cptr = random_eval_cptr + 1;
         let permutation_z_eval_cptr = permutation_eval_cptr + meta.num_permutations();
         let lookup_eval_cptr = permutation_z_eval_cptr + 3 * meta.num_permutation_zs - 1;
-        let w_cptr = lookup_eval_cptr + 5 * meta.num_lookups();
+        let w_cptr = lookup_eval_cptr + 3 * meta.num_lookups();
 
         let fixed_comms = EcPoint::range(fixed_comm_mptr)
             .take(meta.num_fixeds)
@@ -240,15 +240,14 @@ impl Data {
             .map(|idx| advice_comm_start + 2 * idx)
             .map_into()
             .collect();
-        let lookup_permuted_comms = EcPoint::range(lookup_permuted_comm_start)
-            .take(meta.num_lookup_permuteds)
-            .tuples()
+        let lookup_m_comms = EcPoint::range(lookup_m_comm_start)
+            .take(meta.num_lookup_ms)
             .collect();
         let permutation_z_comms = EcPoint::range(permutation_z_comm_start)
             .take(meta.num_permutation_zs)
             .collect();
-        let lookup_z_comms = EcPoint::range(lookup_z_comm_start)
-            .take(meta.num_lookup_zs)
+        let lookup_phi_comms = EcPoint::range(lookup_phi_comm_start)
+            .take(meta.num_lookup_phis)
             .collect();
         let random_comm = random_comm_start.into();
         let computed_quotient_comm = EcPoint::new(
@@ -284,7 +283,7 @@ impl Data {
             .tuples()
             .collect_vec();
         let lookup_evals = Word::range(lookup_eval_cptr)
-            .take(5 * meta.num_lookup_zs)
+            .take(3 * meta.num_lookup_phis)
             .tuples()
             .collect_vec();
         let computed_quotient_eval = Ptr::memory("QUOTIENT_EVAL_MPTR").into();
@@ -298,9 +297,9 @@ impl Data {
             fixed_comms,
             permutation_comms,
             advice_comms,
-            lookup_permuted_comms,
+            lookup_m_comms,
             permutation_z_comms,
-            lookup_z_comms,
+            lookup_phi_comms,
             random_comm,
             computed_quotient_comm,