From b55024043c48376be5376ca1cd6cc4d19d815a4f Mon Sep 17 00:00:00 2001 From: Ryan Kim Date: Wed, 20 Dec 2023 09:12:50 +0900 Subject: [PATCH] feat(zk): implement lookup verification evaluations See [Evaluated::expressions()](https://github.com/kroma-network/halo2/blob/7d0a36990452c8e7ebd600de258420781a9b7917/halo2_proofs/src/plonk/lookup/verifier.rs#L92-L168). --- tachyon/zk/lookup/BUILD.bazel | 16 ++++ tachyon/zk/lookup/lookup_verification.h | 78 +++++++++++++++++++ tachyon/zk/lookup/lookup_verification_data.h | 26 +++++++ .../examples/simple_circuit_unittest.cc | 9 ++- .../simple_lookup_circuit_unittest.cc | 9 ++- tachyon/zk/plonk/halo2/BUILD.bazel | 2 + tachyon/zk/plonk/halo2/proof.h | 25 ++++++ tachyon/zk/plonk/halo2/verifier.h | 25 +++++- 8 files changed, 182 insertions(+), 8 deletions(-) create mode 100644 tachyon/zk/lookup/lookup_verification.h create mode 100644 tachyon/zk/lookup/lookup_verification_data.h diff --git a/tachyon/zk/lookup/BUILD.bazel b/tachyon/zk/lookup/BUILD.bazel index 1348ace98e..e17337703a 100644 --- 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 new file mode 100644 index 0000000000..4265b370d3 --- /dev/null +++ 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 +#include + +#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 +F CompressExpressions( + const std::vector>>& expressions, + const F& theta, VanishingVerificationEvaluator& 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 +F CreateProductExpression(const LookupVerificationData& data, + const LookupArgument& argument) { + VanishingVerificationEvaluator 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 +std::vector CreateLookupVerificationExpressions( + const LookupVerificationData& data, const LookupArgument& argument) { + F active_rows = F::One() - (data.l_last + data.l_blind); + std::vector 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 new file mode 100644 index 0000000000..5a19f8a1a2 --- /dev/null +++ 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 +struct LookupVerificationData : public VanishingVerificationData { + 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 index 9cf566bee8..f1056d1117 100644 --- 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 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> 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 index ed7b090ae2..b1bc189289 100644 --- 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 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> 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 index ad6f771172..1f4607bde7 100644 --- 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 index 3a188f0dfb..45a9be8801 100644 --- a/tachyon/zk/plonk/halo2/proof.h +++ b/tachyon/zk/plonk/halo2/proof.h @@ -6,6 +6,7 @@ #include #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 ToLookupVerificationData(size_t i, size_t j, + const F& l_first, + const F& l_blind, + const F& l_last) const { + LookupVerificationData 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 index 3db1b05f55..f3afd71327 100644 --- 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 { [[nodiscard]] bool VerifyProof( const VerifyingKey& vkey, const std::vector>& 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 { bool VerifyProofForTesting( const VerifyingKey& vkey, const std::vector>& instance_columns_vec, - Proof* proof_out) { + Proof* proof_out, F* expected_h_eval_out) { if (!ValidateInstanceColumnsVec(vkey, instance_columns_vec)) return false; std::vector> instance_commitments_vec; @@ -100,7 +101,10 @@ class Verifier : public VerifierBase { 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 { 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 vanishing_verification_evaluator( proof.ToVanishingVerificationData(i)); @@ -291,6 +296,18 @@ class Verifier : public VerifierBase { expressions.end(), std::make_move_iterator(permutation_expressions.begin()), std::make_move_iterator(permutation_expressions.end())); + + const std::vector>& lookups = + constraint_system.lookups(); + for (size_t j = 0; j < lookups.size(); ++j) { + const LookupArgument& lookup = lookups[j]; + std::vector 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 =