feat(zk): implement lookup verification evaluations

See [Evaluated<C>::expressions()](https://github.com/kroma-network/halo2/blob/7d0a36990452c8e7ebd600de258420781a9b7917/halo2_proofs/src/plonk/lookup/verifier.rs#L92-L168).
kroma-network · Dec 20, 2023 · b550240 · b550240
1 parent cf06441
commit b550240
Show file tree

Hide file tree

Showing 8 changed files with 182 additions and 8 deletions.
diff --git a/tachyon/zk/lookup/BUILD.bazel b/tachyon/zk/lookup/BUILD.bazel
@@ -73,6 +73,22 @@ tachyon_cc_library(
     ],
 )
 
+tachyon_cc_library(
+    name = "lookup_verification_data",
+    hdrs = ["lookup_verification_data.h"],
+    deps = ["//tachyon/zk/plonk/vanishing:vanishing_verification_data"],
+)
+
+tachyon_cc_library(
+    name = "lookup_verification",
+    hdrs = ["lookup_verification.h"],
+    deps = [
+        ":lookup_argument",
+        ":lookup_verification_data",
+        "//tachyon/zk/plonk/vanishing:vanishing_verification_evaluator",
+    ],
+)
+
 tachyon_cc_library(
     name = "permute_expression_pair",
     hdrs = ["permute_expression_pair.h"],

diff --git a/tachyon/zk/lookup/lookup_verification.h b/tachyon/zk/lookup/lookup_verification.h
@@ -0,0 +1,78 @@
+// Copyright 2020-2022 The Electric Coin Company
+// Copyright 2022 The Halo2 developers
+// Use of this source code is governed by a MIT/Apache-2.0 style license that
+// can be found in the LICENSE-MIT.halo2 and the LICENCE-APACHE.halo2
+// file.
+
+#ifndef TACHYON_ZK_LOOKUP_LOOKUP_VERIFICATION_H_
+#define TACHYON_ZK_LOOKUP_LOOKUP_VERIFICATION_H_
+
+#include <memory>
+#include <vector>
+
+#include "tachyon/zk/lookup/lookup_argument.h"
+#include "tachyon/zk/lookup/lookup_verification_data.h"
+#include "tachyon/zk/plonk/vanishing/vanishing_verification_evaluator.h"
+
+namespace tachyon::zk {
+
+template <typename F>
+F CompressExpressions(
+    const std::vector<std::unique_ptr<Expression<F>>>& expressions,
+    const F& theta, VanishingVerificationEvaluator<F>& evaluator) {
+  F compressed_value = F::Zero();
+  for (size_t expr_idx = 0; expr_idx < expressions.size(); ++expr_idx) {
+    compressed_value *= theta;
+    compressed_value += evaluator.Evaluate(expressions[expr_idx].get());
+  }
+  return compressed_value;
+}
+
+template <typename F>
+F CreateProductExpression(const LookupVerificationData<F>& data,
+                          const LookupArgument<F>& argument) {
+  VanishingVerificationEvaluator<F> evaluator(data);
+  // z(ω * X) * (a'(X) + β) * (s'(X) + γ)
+  // - z(X) * (θᵐ⁻¹a₀(X) + ... + aₘ₋₁(X) + β) * (θᵐ⁻¹s₀(X) + ... + sₘ₋₁(X) + γ)
+  F left = data.product_next_eval * (data.permuted_input_eval + data.beta) *
+           (data.permuted_table_eval + data.gamma);
+  F compressed_input_expression =
+      CompressExpressions(argument.input_expressions(), data.theta, evaluator);
+  F compressed_table_expression =
+      CompressExpressions(argument.table_expressions(), data.theta, evaluator);
+  F right = data.product_eval * (compressed_input_expression + data.beta) *
+            (compressed_table_expression + data.gamma);
+  return left - right;
+}
+
+constexpr size_t GetSizeOfLookupVerificationExpressions() { return 5; }
+
+template <typename F>
+std::vector<F> CreateLookupVerificationExpressions(
+    const LookupVerificationData<F>& data, const LookupArgument<F>& argument) {
+  F active_rows = F::One() - (data.l_last + data.l_blind);
+  std::vector<F> ret;
+  ret.reserve(GetSizeOfLookupVerificationExpressions());
+  // l_first(X) * (1 - z'(X)) = 0
+  ret.push_back(data.l_first * (F::One() - data.product_eval));
+  // l_last(X) * (z(X)² - z(X)) = 0
+  ret.push_back(data.l_last * (data.product_eval.Square() - data.product_eval));
+  // (1 - (l_last(X) + l_blind(X))) * (
+  //   z(ω * X) * (a'(X) + β) * (s'(X) + γ)
+  //   - z(X) (θᵐ⁻¹a₀(X) + ... + aₘ₋₁(X) + β) (θᵐ⁻¹s₀(X) + ... + sₘ₋₁(X) + γ)
+  // ) = 0
+  ret.push_back(active_rows * CreateProductExpression(data, argument));
+  // l_first(X) * (a'(X) - s'(X)) = 0
+  ret.push_back(data.l_first *
+                (data.permuted_input_eval - data.permuted_table_eval));
+  // (1 - (l_last(X) + l_blind(X))) *
+  // (a'(X) − s'(X)) * (a'(X) − a'(ω⁻¹ * X)) = 0
+  ret.push_back(active_rows *
+                (data.permuted_input_eval - data.permuted_table_eval) *
+                (data.permuted_input_eval - data.permuted_input_inv_eval));
+  return ret;
+}
+
+}  // namespace tachyon::zk
+
+#endif  // TACHYON_ZK_LOOKUP_LOOKUP_VERIFICATION_H_
diff --git a/tachyon/zk/lookup/lookup_verification_data.h b/tachyon/zk/lookup/lookup_verification_data.h
@@ -0,0 +1,26 @@
+#ifndef TACHYON_ZK_LOOKUP_LOOKUP_VERIFICATION_DATA_H_
+#define TACHYON_ZK_LOOKUP_LOOKUP_VERIFICATION_DATA_H_
+
+#include "tachyon/zk/plonk/vanishing/vanishing_verification_data.h"
+
+namespace tachyon::zk {
+
+template <typename F>
+struct LookupVerificationData : public VanishingVerificationData<F> {
+  F product_eval;
+  F product_next_eval;
+  F permuted_input_eval;
+  F permuted_input_inv_eval;
+  F permuted_table_eval;
+  F theta;
+  F beta;
+  F gamma;
+  F x;
+  F l_first;
+  F l_blind;
+  F l_last;
+};
+
+}  // namespace tachyon::zk
+
+#endif  // TACHYON_ZK_LOOKUP_LOOKUP_VERIFICATION_DATA_H_
diff --git a/tachyon/zk/plonk/circuit/examples/simple_circuit_unittest.cc b/tachyon/zk/plonk/circuit/examples/simple_circuit_unittest.cc
@@ -651,8 +651,9 @@ TEST_F(SimpleCircuitTest, Verify) {
       std::move(instance_columns)};
 
   Proof<F, Commitment> proof;
-  ASSERT_TRUE(
-      verifier->VerifyProofForTesting(vkey, instance_columns_vec, &proof));
+  F expected_h_eval;
+  ASSERT_TRUE(verifier->VerifyProofForTesting(vkey, instance_columns_vec,
+                                              &proof, &expected_h_eval));
 
   std::vector<std::vector<Commitment>> expected_advice_commitments_vec;
   {
@@ -827,6 +828,10 @@ TEST_F(SimpleCircuitTest, Verify) {
 
   ASSERT_EQ(proof.lookup_permuted_table_evals_vec.size(), 1);
   EXPECT_TRUE(proof.lookup_permuted_table_evals_vec[0].empty());
+
+  F expected_expected_h_eval = F::FromHexString(
+      "0x0b91cc8fe9296c94157f8f2b226da12d1ef112be8e9e30c88b402e1b36bbab6e");
+  EXPECT_EQ(expected_h_eval, expected_expected_h_eval);
 }
 
 }  // namespace tachyon::zk::halo2
diff --git a/tachyon/zk/plonk/circuit/examples/simple_lookup_circuit_unittest.cc b/tachyon/zk/plonk/circuit/examples/simple_lookup_circuit_unittest.cc
@@ -535,8 +535,9 @@ TEST_F(SimpleLookupCircuitTest, Verify) {
       std::move(instance_columns)};
 
   Proof<F, Commitment> proof;
-  ASSERT_TRUE(
-      verifier->VerifyProofForTesting(vkey, instance_columns_vec, &proof));
+  F expected_h_eval;
+  ASSERT_TRUE(verifier->VerifyProofForTesting(vkey, instance_columns_vec,
+                                              &proof, &expected_h_eval));
 
   std::vector<std::vector<Commitment>> expected_advice_commitments_vec;
   {
@@ -710,6 +711,10 @@ TEST_F(SimpleLookupCircuitTest, Verify) {
   }
   EXPECT_EQ(proof.lookup_permuted_table_evals_vec,
             expected_lookup_permuted_table_evals_vec);
+
+  F expected_expected_h_eval = F::FromHexString(
+      "0x01d8f3b1cc0f65fe4a711b22ac8843f20b8f0ca5cf6f01757c018ef1a9a44c7f");
+  EXPECT_EQ(expected_h_eval, expected_expected_h_eval);
 }
 
 }  // namespace tachyon::zk::halo2
diff --git a/tachyon/zk/plonk/halo2/BUILD.bazel b/tachyon/zk/plonk/halo2/BUILD.bazel
@@ -83,6 +83,7 @@ tachyon_cc_library(
     hdrs = ["proof.h"],
     deps = [
         "//tachyon/zk/lookup:lookup_pair",
+        "//tachyon/zk/lookup:lookup_verification_data",
         "//tachyon/zk/plonk/permutation:permutation_verification_data",
         "//tachyon/zk/plonk/vanishing:vanishing_verification_data",
     ],
@@ -166,6 +167,7 @@ tachyon_cc_library(
         ":proof_reader",
         "//tachyon/base/containers:container_util",
         "//tachyon/zk/base/entities:verifier_base",
+        "//tachyon/zk/lookup:lookup_verification",
         "//tachyon/zk/plonk/keys:verifying_key",
         "//tachyon/zk/plonk/permutation:permutation_verification",
         "//tachyon/zk/plonk/vanishing:vanishing_verification_evaluator",

diff --git a/tachyon/zk/plonk/halo2/proof.h b/tachyon/zk/plonk/halo2/proof.h
@@ -6,6 +6,7 @@
 #include <vector>
 
 #include "tachyon/zk/lookup/lookup_pair.h"
+#include "tachyon/zk/lookup/lookup_verification_data.h"
 #include "tachyon/zk/plonk/permutation/permutation_verification_data.h"
 #include "tachyon/zk/plonk/vanishing/vanishing_verification_data.h"
 
@@ -69,6 +70,30 @@ struct Proof {
     ret.l_last = l_last;
     return ret;
   }
+
+  LookupVerificationData<F> ToLookupVerificationData(size_t i, size_t j,
+                                                     const F& l_first,
+                                                     const F& l_blind,
+                                                     const F& l_last) const {
+    LookupVerificationData<F> ret;
+    ret.fixed_evals = absl::MakeConstSpan(fixed_evals);
+    ret.advice_evals = absl::MakeConstSpan(advice_evals_vec[i]);
+    ret.instance_evals = absl::MakeConstSpan(instance_evals_vec[i]);
+    ret.challenges = absl::MakeConstSpan(challenges);
+    ret.product_eval = lookup_product_evals_vec[i][j];
+    ret.product_next_eval = lookup_product_next_evals_vec[i][j];
+    ret.permuted_input_eval = lookup_permuted_input_evals_vec[i][j];
+    ret.permuted_input_inv_eval = lookup_permuted_input_inv_evals_vec[i][j];
+    ret.permuted_table_eval = lookup_permuted_table_evals_vec[i][j];
+    ret.theta = theta;
+    ret.beta = beta;
+    ret.gamma = gamma;
+    ret.x = x;
+    ret.l_first = l_first;
+    ret.l_blind = l_blind;
+    ret.l_last = l_last;
+    return ret;
+  }
 };
 
 }  // namespace tachyon::zk::halo2

diff --git a/tachyon/zk/plonk/halo2/verifier.h b/tachyon/zk/plonk/halo2/verifier.h
@@ -17,6 +17,7 @@
 
 #include "tachyon/base/containers/container_util.h"
 #include "tachyon/zk/base/entities/verifier_base.h"
+#include "tachyon/zk/lookup/lookup_verification.h"
 #include "tachyon/zk/plonk/halo2/proof_reader.h"
 #include "tachyon/zk/plonk/keys/verifying_key.h"
 #include "tachyon/zk/plonk/permutation/permutation_verification.h"
@@ -38,7 +39,7 @@ class Verifier : public VerifierBase<PCSTy> {
   [[nodiscard]] bool VerifyProof(
       const VerifyingKey<PCSTy>& vkey,
       const std::vector<std::vector<Evals>>& instance_columns_vec) {
-    return VerifyProofForTesting(vkey, instance_columns_vec, nullptr);
+    return VerifyProofForTesting(vkey, instance_columns_vec, nullptr, nullptr);
   }
 
  private:
@@ -48,7 +49,7 @@ class Verifier : public VerifierBase<PCSTy> {
   bool VerifyProofForTesting(
       const VerifyingKey<PCSTy>& vkey,
       const std::vector<std::vector<Evals>>& instance_columns_vec,
-      Proof<F, Commitment>* proof_out) {
+      Proof<F, Commitment>* proof_out, F* expected_h_eval_out) {
     if (!ValidateInstanceColumnsVec(vkey, instance_columns_vec)) return false;
 
     std::vector<std::vector<Commitment>> instance_commitments_vec;
@@ -100,7 +101,10 @@ class Verifier : public VerifierBase<PCSTy> {
 
     F expected_h_eval =
         ComputeExpectedHEval(instance_columns_vec.size(), vkey, proof);
-    std::ignore = expected_h_eval;
+    if (expected_h_eval_out) {
+      *expected_h_eval_out = expected_h_eval;
+    }
+
     return true;
   }
 
@@ -272,7 +276,8 @@ class Verifier : public VerifierBase<PCSTy> {
     expressions.reserve(
         num_circuits *
         (constraint_system.gates().size() +
-         GetSizeOfPermutationVerificationExpressions(constraint_system)));
+         GetSizeOfPermutationVerificationExpressions(constraint_system) +
+         GetSizeOfLookupVerificationExpressions()));
     for (size_t i = 0; i < num_circuits; ++i) {
       VanishingVerificationEvaluator<F> vanishing_verification_evaluator(
           proof.ToVanishingVerificationData(i));
@@ -291,6 +296,18 @@ class Verifier : public VerifierBase<PCSTy> {
           expressions.end(),
           std::make_move_iterator(permutation_expressions.begin()),
           std::make_move_iterator(permutation_expressions.end()));
+
+      const std::vector<LookupArgument<F>>& lookups =
+          constraint_system.lookups();
+      for (size_t j = 0; j < lookups.size(); ++j) {
+        const LookupArgument<F>& lookup = lookups[j];
+        std::vector<F> lookup_expressions = CreateLookupVerificationExpressions(
+            proof.ToLookupVerificationData(i, j, l_first, l_blind, l_last),
+            lookup);
+        expressions.insert(expressions.end(),
+                           std::make_move_iterator(lookup_expressions.begin()),
+                           std::make_move_iterator(lookup_expressions.end()));
+      }
     }
     const F& y = proof.y;
     F expected_h_eval =