feat(zk): implement proof verification part2

tachyon/math/polynomials/univariate/univariate_evaluation_domain.h

@@ -166,9 +166,11 @@ class UnivariateEvaluationDomain : public EvaluationDomain<F, MaxDegree> {
 
   // Almost same with above, but it only computes parts of the lagrange
   // coefficients defined by |range|.
-  template <typename T>
+  // TODO(chokobole): If we want to accept IsStartInclusive as a template
+  // parameter, we need a way to get a starting index from |range|.
+  template <typename T, bool IsEndInclusive>
   constexpr std::vector<F> EvaluatePartialLagrangeCoefficients(
-      const F& tau, base::Range<T> range) const {
+      const F& tau, base::Range<T, true, IsEndInclusive> range) const {
     size_t size = range.GetSize();
     CHECK_LE(size, size_);
     if (size == 0) return {};

tachyon/zk/expressions/evaluator/BUILD.bazel

@@ -7,7 +7,11 @@ tachyon_cc_library(
     hdrs = ["selector_replacer.h"],
     deps = [
         "//tachyon/zk/expressions:evaluator",
+        "//tachyon/zk/expressions:negated_expression",
+        "//tachyon/zk/expressions:product_expression",
+        "//tachyon/zk/expressions:scaled_expression",
         "//tachyon/zk/expressions:selector_expression",
+        "//tachyon/zk/expressions:sum_expression",
     ],
 )
 

tachyon/zk/expressions/evaluator/selector_replacer.h

@@ -11,7 +11,11 @@
 #include <vector>
 
 #include "tachyon/zk/expressions/evaluator.h"
+#include "tachyon/zk/expressions/negated_expression.h"
+#include "tachyon/zk/expressions/product_expression.h"
+#include "tachyon/zk/expressions/scaled_expression.h"
 #include "tachyon/zk/expressions/selector_expression.h"
+#include "tachyon/zk/expressions/sum_expression.h"
 
 namespace tachyon::zk {
 

tachyon/zk/expressions/evaluator/simple_evaluator.h

@@ -68,6 +68,7 @@ class SimpleEvaluator
         return input->ToConstant()->value();
 
       case ExpressionType::kSelector:
+        NOTREACHED() << "virtual selectors are removed during optimization";
         break;
 
       case ExpressionType::kFixed: {

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"],

tachyon/zk/lookup/compress_expression.h

@@ -16,10 +16,10 @@
 namespace tachyon::zk {
 
 template <typename Domain, typename Evals, typename F>
-bool CompressExpressions(
+Evals CompressExpressions(
     const Domain* domain,
     const std::vector<std::unique_ptr<Expression<F>>>& expressions,
-    const F& theta, const SimpleEvaluator<Evals>& evaluator_tpl, Evals* out) {
+    const F& theta, const SimpleEvaluator<Evals>& evaluator_tpl) {
   Evals compressed_value = domain->template Empty<Evals>();
   Evals values = domain->template Empty<Evals>();
 
@@ -38,9 +38,7 @@ bool CompressExpressions(
     compressed_value *= theta;
     compressed_value += values;
   }
-
-  *out = Evals(std::move(compressed_value));
-  return true;
+  return compressed_value;
 }
 
 }  // namespace tachyon::zk

tachyon/zk/lookup/compress_expression_unittest.cc

@@ -37,9 +37,8 @@ TEST_F(CompressExpressionTest, CompressExpressions) {
     }
   }
 
-  Evals out;
-  ASSERT_TRUE(CompressExpressions(prover_->domain(), expressions, theta_,
-                                  evaluator_, &out));
+  Evals out =
+      CompressExpressions(prover_->domain(), expressions, theta_, evaluator_);
   EXPECT_EQ(out, Evals(std::move(expected)));
 }
 

tachyon/zk/lookup/lookup_argument_runner_impl.h

@@ -23,16 +23,13 @@ LookupPermuted<Poly, Evals> LookupArgumentRunner<Poly, Evals>::PermuteArgument(
     ProverBase<PCSTy>* prover, const LookupArgument<F>& argument,
     const F& theta, const SimpleEvaluator<Evals>& evaluator_tpl) {
   // A_compressed(X) = θᵐ⁻¹A₀(X) + θᵐ⁻²A₁(X) + ... + θAₘ₋₂(X) + Aₘ₋₁(X)
-  Evals compressed_input_expression;
-  CHECK(CompressExpressions(prover->domain(), argument.input_expressions(),
-                            theta, evaluator_tpl,
-                            &compressed_input_expression));
+  Evals compressed_input_expression = CompressExpressions(
+      prover->domain(), argument.input_expressions(), theta, evaluator_tpl);
 
   // S_compressed(X) = θᵐ⁻¹S₀(X) + θᵐ⁻²S₁(X) + ... + θSₘ₋₂(X) + Sₘ₋₁(X)
-  Evals compressed_table_expression;
-  CHECK(CompressExpressions(prover->domain(), argument.table_expressions(),
-                            theta, evaluator_tpl,
-                            &compressed_table_expression));
+  Evals compressed_table_expression =
+      CompressExpressions(prover->domain(), argument.table_expressions(), theta,
+                          evaluator_tpl, &compressed_table_expression);
 
   // Permute compressed (InputExpression, TableExpression) pair.
   LookupPair<Evals> compressed_evals_pair(

tachyon/zk/lookup/lookup_argument_runner_unittest.cc

@@ -36,12 +36,10 @@ TEST_F(LookupArgumentRunnerTest, ComputePermutationProduct) {
     table_expressions.push_back(ExpressionFactory<F>::Constant(random));
   }
 
-  Evals compressed_input_expression;
-  ASSERT_TRUE(CompressExpressions(prover_->domain(), input_expressions, theta_,
-                                  evaluator_, &compressed_input_expression));
-  Evals compressed_table_expression;
-  ASSERT_TRUE(CompressExpressions(prover_->domain(), table_expressions, theta_,
-                                  evaluator_, &compressed_table_expression));
+  Evals compressed_input_expression = CompressExpressions(
+      prover_->domain(), input_expressions, theta_, evaluator_);
+  Evals compressed_table_expression = CompressExpressions(
+      prover_->domain(), table_expressions, theta_, evaluator_);
 
   LookupPair<Evals> compressed_evals_pair(
       std::move(compressed_input_expression),

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_

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_

tachyon/zk/plonk/BUILD.bazel

@@ -18,6 +18,7 @@ tachyon_cc_library(
         "//tachyon/zk/plonk/circuit:selector_compressor",
         "//tachyon/zk/plonk/circuit:virtual_cells",
         "//tachyon/zk/plonk/permutation:permutation_argument",
+        "//tachyon/zk/plonk/permutation:permutation_utils",
     ],
 )
 

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 h_eval;
+  ASSERT_TRUE(verifier->VerifyProofForTesting(vkey, instance_columns_vec,
+                                              &proof, &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_h_eval = F::FromHexString(
+      "0x0b91cc8fe9296c94157f8f2b226da12d1ef112be8e9e30c88b402e1b36bbab6e");
+  EXPECT_EQ(h_eval, expected_h_eval);
 }
 
 }  // namespace tachyon::zk::halo2

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 h_eval;
+  ASSERT_TRUE(verifier->VerifyProofForTesting(vkey, instance_columns_vec,
+                                              &proof, &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_h_eval = F::FromHexString(
+      "0x01d8f3b1cc0f65fe4a711b22ac8843f20b8f0ca5cf6f01757c018ef1a9a44c7f");
+  EXPECT_EQ(h_eval, expected_h_eval);
 }
 
 }  // namespace tachyon::zk::halo2

tachyon/zk/plonk/constraint_system.h

@@ -28,6 +28,7 @@
 #include "tachyon/zk/plonk/circuit/selector_compressor.h"
 #include "tachyon/zk/plonk/circuit/virtual_cells.h"
 #include "tachyon/zk/plonk/permutation/permutation_argument.h"
+#include "tachyon/zk/plonk/permutation/permutation_utils.h"
 
 namespace tachyon::zk {
 
@@ -502,6 +503,17 @@ class ConstraintSystem {
            + 1;  // for at least one row
   }
 
+  // Return the length of permutation chunk.
+  size_t ComputePermutationChunkLen() const {
+    return ComputePermutationChunkLength(ComputeDegree());
+  }
+
+  // Return the number of permutation products.
+  size_t ComputePermutationProductNums() const {
+    size_t chunk_len = ComputePermutationChunkLen();
+    return (permutation_.columns().size() + chunk_len - 1) / chunk_len;
+  }
+
  private:
   template <typename QueryDataTy, typename ColumnTy>
   static bool QueryIndex(const std::vector<QueryDataTy>& queries,

tachyon/zk/plonk/halo2/BUILD.bazel

@@ -81,7 +81,12 @@ tachyon_cc_library(
 tachyon_cc_library(
     name = "proof",
     hdrs = ["proof.h"],
-    deps = ["//tachyon/zk/lookup:lookup_pair"],
+    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",
+    ],
 )
 
 tachyon_cc_library(
@@ -92,6 +97,7 @@ tachyon_cc_library(
         "//tachyon/base:logging",
         "//tachyon/crypto/transcripts:transcript",
         "//tachyon/zk/plonk/keys:verifying_key",
+        "//tachyon/zk/plonk/permutation:permutation_utils",
     ],
 )
 
@@ -160,7 +166,10 @@ 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",
         "@com_google_absl//absl/functional:bind_front",
         "@com_google_googletest//:gtest_prod",
     ],