From b3d1f280913494322baee369e6ee4f04353891b3 Mon Sep 17 00:00:00 2001 From: Innokentii Sennovskii Date: Thu, 12 Oct 2023 20:35:52 +0100 Subject: [PATCH] feat: Goblin translator opcode constraint and accumulator transfer relations (Goblin Translator part 5) (#2805) Relations and consistency tests of Opcode Constraint relation (enforces particular values on the Opcode in EccOpQueue) and accumulator transfer relation (Checks all non-arithmetic accumulator transitions) --- .../relations/extra_relations.hpp | 188 ++++++++++++++++++ ...n_translator_relation_consistency.test.cpp | 75 +++++++ .../relations/relation_parameters.hpp | 8 +- 3 files changed, 270 insertions(+), 1 deletion(-) create mode 100644 barretenberg/cpp/src/barretenberg/proof_system/relations/extra_relations.hpp diff --git a/barretenberg/cpp/src/barretenberg/proof_system/relations/extra_relations.hpp b/barretenberg/cpp/src/barretenberg/proof_system/relations/extra_relations.hpp new file mode 100644 index 00000000000..edd78f45377 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/proof_system/relations/extra_relations.hpp @@ -0,0 +1,188 @@ +#pragma once +#include "barretenberg/numeric/uint256/uint256.hpp" +#include "relation_parameters.hpp" +#include "relation_types.hpp" + +namespace proof_system { + +template class GoblinTranslatorOpcodeConstraintRelationImpl { + public: + using FF = FF_; + + // 1 + polynomial degree of this relation + static constexpr size_t RELATION_LENGTH = 7; // degree(op(op - 1)(op - 2)(op - 3)(op - 4)(op - 8)) = 6 + static constexpr std::array SUBRELATION_LENGTHS{ + 7 // opcode constraint relation + }; + + /** + * @brief Expression for enforcing the value of the Opcode to be {0,1,2,3,4,8} + * @details This relation enforces the opcode to be one of described values. Since we don't care about even + * values in the opcode wire and usually just set them to zero, we don't use a lagrange polynomial to specify + * the relation to be enforced just at odd indices, which brings the degree down by 1. + * + * @param evals transformed to `evals + C(in(X)...)*scaling_factor` + * @param in an std::array containing the fully extended Univariate edges. + * @param parameters contains beta, gamma, and public_input_delta, .... + * @param scaling_factor optional term to scale the evaluation before adding to evals. + */ + template + void static accumulate(ContainerOverSubrelations& accumulators, + const AllEntitites& in, + const RelationParameters&, + const FF& scaling_factor) + { + + using Accumulator = std::tuple_element_t<0, ContainerOverSubrelations>; + using View = typename Accumulator::View; + + auto op = View(in.op); + static const FF minus_one = FF(-1); + static const FF minus_two = FF(-2); + static const FF minus_three = FF(-3); + static const FF minus_four = FF(-4); + static const FF minus_eight = FF(-8); + + // Contribution (1) (op(op-1)(op-2)(op-3)(op-4)(op-8)) + auto tmp_1 = op * (op + minus_one); + tmp_1 *= (op + minus_two); + tmp_1 *= (op + minus_three); + tmp_1 *= (op + minus_four); + tmp_1 *= (op + minus_eight); + tmp_1 *= scaling_factor; + std::get<0>(accumulators) += tmp_1; + }; +}; + +template class GoblinTranslatorAccumulatorTransferRelationImpl { + public: + using FF = FF_; + + // 1 + polynomial degree of this relation + static constexpr size_t RELATION_LENGTH = 3; // degree((SOME_LAGRANGE)(A-B)) = 2 + static constexpr std::array SUBRELATION_LENGTHS{ + 3, // transfer accumulator limb 0 at even index subrelation + 3, // transfer accumulator limb 1 at even index subrelation + 3, // transfer accumulator limb 2 at even index subrelation + 3, // transfer accumulator limb 3 at even index subrelation + 3, // accumulator limb 0 is zero at the start of accumulation subrelation + 3, // accumulator limb 1 is zero at the start of accumulation subrelation + 3, // accumulator limb 2 is zero at the start of accumulation subrelation + 3, // accumulator limb 3 is zero at the start of accumulation subrelation + 3, // accumulator limb 0 is equal to given result at the end of accumulation subrelation + 3, // accumulator limb 1 is equal to given result at the end of accumulation subrelation + 3, // accumulator limb 2 is equal to given result at the end of accumulation subrelation + 3 // accumulator limb 3 is equal to given result at the end of accumulation subrelation + + }; + + /** + * @brief Relation enforcing non-arithmetic transitions of accumulator (value that is tracking the batched + * evaluation of polynomials in non-native field) + * @details This relation enforces three pieces of logic: + * 1) Accumulator starts as zero before we start accumulating stuff + * 2) Accumulator limbs stay the same if accumulation is not occurring (at even indices) + * 3) Accumulator limbs result in the values specified by relation parameters after accumulation + * + * @param evals transformed to `evals + C(in(X)...)*scaling_factor` + * @param in an std::array containing the fully extended Univariate edges. + * @param parameters contains beta, gamma, and public_input_delta, .... + * @param scaling_factor optional term to scale the evaluation before adding to evals. + */ + template + void static accumulate(ContainerOverSubrelations& accumulators, + const AllEntities& in, + const RelationParameters& relation_parameters, + const FF& scaling_factor) + { + using Accumulator = std::tuple_element_t<0, ContainerOverSubrelations>; + using View = typename Accumulator::View; + // We use combination of lagrange polynomials at even indices in the minicircuit for copying the accumulator + auto lagrange_even = View(in.lagrange_even); + + // Lagrange at index 1 is used to confirm the accumulator result + auto lagrange_second = View(in.lagrange_second); + + // Lagrange at index (size of minicircuit - 2) is used to enforce that it starts with zero + auto lagrange_second_to_last_in_minicircuit = View(in.lagrange_second_to_last_in_minicircuit); + + auto accumulators_binary_limbs_0 = View(in.accumulators_binary_limbs_0); + auto accumulators_binary_limbs_1 = View(in.accumulators_binary_limbs_1); + auto accumulators_binary_limbs_2 = View(in.accumulators_binary_limbs_2); + auto accumulators_binary_limbs_3 = View(in.accumulators_binary_limbs_3); + auto accumulators_binary_limbs_0_shift = View(in.accumulators_binary_limbs_0_shift); + auto accumulators_binary_limbs_1_shift = View(in.accumulators_binary_limbs_1_shift); + auto accumulators_binary_limbs_2_shift = View(in.accumulators_binary_limbs_2_shift); + auto accumulators_binary_limbs_3_shift = View(in.accumulators_binary_limbs_3_shift); + + // Contribution (1) (1-4 ensure transfer of accumulator limbs at even indices of the minicircuit) + auto tmp_1 = accumulators_binary_limbs_0 - accumulators_binary_limbs_0_shift; + tmp_1 *= lagrange_even; + tmp_1 *= scaling_factor; + std::get<0>(accumulators) += tmp_1; + + // Contribution (2) + auto tmp_2 = accumulators_binary_limbs_1 - accumulators_binary_limbs_1_shift; + tmp_2 *= lagrange_even; + tmp_2 *= scaling_factor; + std::get<1>(accumulators) += tmp_2; + // Contribution (3) + auto tmp_3 = accumulators_binary_limbs_2 - accumulators_binary_limbs_2_shift; + tmp_3 *= lagrange_even; + tmp_3 *= scaling_factor; + std::get<2>(accumulators) += tmp_3; + // Contribution (4) + auto tmp_4 = accumulators_binary_limbs_3 - accumulators_binary_limbs_3_shift; + tmp_4 *= lagrange_even; + tmp_4 *= scaling_factor; + std::get<3>(accumulators) += tmp_4; + + // Contribution (5) (5-9 ensure that accumulator starts with zeroed-out limbs) + auto tmp_5 = accumulators_binary_limbs_0 * lagrange_second_to_last_in_minicircuit; + tmp_5 *= scaling_factor; + std::get<4>(accumulators) += tmp_5; + + // Contribution (6) + auto tmp_6 = accumulators_binary_limbs_1 * lagrange_second_to_last_in_minicircuit; + tmp_6 *= scaling_factor; + std::get<5>(accumulators) += tmp_6; + + // Contribution (7) + auto tmp_7 = accumulators_binary_limbs_2 * lagrange_second_to_last_in_minicircuit; + tmp_7 *= scaling_factor; + std::get<6>(accumulators) += tmp_7; + + // Contribution (8) + auto tmp_8 = accumulators_binary_limbs_3 * lagrange_second_to_last_in_minicircuit; + tmp_8 *= scaling_factor; + std::get<7>(accumulators) += tmp_8; + + // Contribution (9) (9-12 ensure the output is as stated, we basically use this to get the result out of the + // proof) + auto tmp_9 = (accumulators_binary_limbs_0 - relation_parameters.accumulated_result[0]) * lagrange_second; + tmp_9 *= scaling_factor; + std::get<8>(accumulators) += tmp_9; + + // Contribution (10) + auto tmp_10 = (accumulators_binary_limbs_1 - relation_parameters.accumulated_result[1]) * lagrange_second; + tmp_10 *= scaling_factor; + std::get<9>(accumulators) += tmp_10; + + // Contribution (11) + auto tmp_11 = (accumulators_binary_limbs_2 - relation_parameters.accumulated_result[2]) * lagrange_second; + tmp_11 *= scaling_factor; + std::get<10>(accumulators) += tmp_11; + + // Contribution (12) + auto tmp_12 = (accumulators_binary_limbs_3 - relation_parameters.accumulated_result[3]) * lagrange_second; + tmp_12 *= scaling_factor; + std::get<11>(accumulators) += tmp_12; + }; +}; +template +using GoblinTranslatorOpcodeConstraintRelation = Relation>; + +template +using GoblinTranslatorAccumulatorTransferRelation = Relation>; + +} // namespace proof_system diff --git a/barretenberg/cpp/src/barretenberg/proof_system/relations/goblin_translator_relation_consistency.test.cpp b/barretenberg/cpp/src/barretenberg/proof_system/relations/goblin_translator_relation_consistency.test.cpp index 486e37797d3..d404f7adf0a 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/relations/goblin_translator_relation_consistency.test.cpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/relations/goblin_translator_relation_consistency.test.cpp @@ -13,9 +13,11 @@ */ #include "barretenberg/ecc/curves/bn254/fr.hpp" #include "barretenberg/proof_system/relations/decomposition_relation.hpp" +#include "barretenberg/proof_system/relations/extra_relations.hpp" #include "barretenberg/proof_system/relations/gen_perm_sort_relation.hpp" #include "barretenberg/proof_system/relations/permutation_relation.hpp" #include "decomposition_relation.hpp" +#include "extra_relations.hpp" #include using namespace proof_system; @@ -905,4 +907,77 @@ TEST_F(GoblinTranslatorRelationConsistency, DecompositionRelation) run_test(/*random_inputs=*/true); }; +TEST_F(GoblinTranslatorRelationConsistency, OpcodeConstraintRelation) +{ + const auto run_test = [](bool random_inputs) { + using Relation = GoblinTranslatorOpcodeConstraintRelation; + using RelationValues = typename Relation::ArrayOfValuesOverSubrelations; + + const InputElements input_elements = random_inputs ? InputElements::get_random() : InputElements::get_special(); + const auto& op = input_elements.op; + + RelationValues expected_values; + + const auto parameters = RelationParameters::get_random(); + + // (Contribution 1) + auto contribution_1 = op * (op - FF(1)) * (op - FF(2)) * (op - FF(3)) * (op - FF(4)) * (op - FF(8)); + expected_values[0] = contribution_1; + + validate_relation_execution(expected_values, input_elements, parameters); + }; + run_test(/*random_inputs=*/false); + run_test(/*random_inputs=*/true); +}; + +TEST_F(GoblinTranslatorRelationConsistency, AccumulatorTransferRelation) +{ + const auto run_test = [](bool random_inputs) { + using Relation = GoblinTranslatorAccumulatorTransferRelation; + using RelationValues = typename Relation::ArrayOfValuesOverSubrelations; + + const InputElements input_elements = random_inputs ? InputElements::get_random() : InputElements::get_special(); + + const auto& lagrange_even = input_elements.lagrange_even; + const auto& lagrange_second = input_elements.lagrange_second; + const auto& lagrange_second_to_last_in_minicircuit = input_elements.lagrange_second_to_last_in_minicircuit; + const auto& accumulators_binary_limbs_0 = input_elements.accumulators_binary_limbs_0; + const auto& accumulators_binary_limbs_0_shift = input_elements.accumulators_binary_limbs_0_shift; + const auto& accumulators_binary_limbs_1 = input_elements.accumulators_binary_limbs_1; + const auto& accumulators_binary_limbs_1_shift = input_elements.accumulators_binary_limbs_1_shift; + const auto& accumulators_binary_limbs_2 = input_elements.accumulators_binary_limbs_2; + const auto& accumulators_binary_limbs_2_shift = input_elements.accumulators_binary_limbs_2_shift; + const auto& accumulators_binary_limbs_3 = input_elements.accumulators_binary_limbs_3; + const auto& accumulators_binary_limbs_3_shift = input_elements.accumulators_binary_limbs_3_shift; + + RelationValues expected_values; + + const auto parameters = RelationParameters::get_random(); + + const auto [accumulated_result_0, accumulated_result_1, accumulated_result_2, accumulated_result_3] = + parameters.accumulated_result; + + // Check transfer of accumulator at even indices + expected_values[0] = lagrange_even * (accumulators_binary_limbs_0 - accumulators_binary_limbs_0_shift); + expected_values[1] = lagrange_even * (accumulators_binary_limbs_1 - accumulators_binary_limbs_1_shift); + expected_values[2] = lagrange_even * (accumulators_binary_limbs_2 - accumulators_binary_limbs_2_shift); + expected_values[3] = lagrange_even * (accumulators_binary_limbs_3 - accumulators_binary_limbs_3_shift); + + // Check the accumulator starts as zero + expected_values[4] = accumulators_binary_limbs_0 * lagrange_second_to_last_in_minicircuit; + expected_values[5] = accumulators_binary_limbs_1 * lagrange_second_to_last_in_minicircuit; + expected_values[6] = accumulators_binary_limbs_2 * lagrange_second_to_last_in_minicircuit; + expected_values[7] = accumulators_binary_limbs_3 * lagrange_second_to_last_in_minicircuit; + + // Check the accumulator results in submitted value + expected_values[8] = (accumulators_binary_limbs_0 - accumulated_result_0) * lagrange_second; + expected_values[9] = (accumulators_binary_limbs_1 - accumulated_result_1) * lagrange_second; + expected_values[10] = (accumulators_binary_limbs_2 - accumulated_result_2) * lagrange_second; + expected_values[11] = (accumulators_binary_limbs_3 - accumulated_result_3) * lagrange_second; + validate_relation_execution(expected_values, input_elements, parameters); + }; + run_test(/*random_inputs=*/false); + run_test(/*random_inputs=*/true); +}; + } // namespace proof_system::ultra_relation_consistency_tests diff --git a/barretenberg/cpp/src/barretenberg/proof_system/relations/relation_parameters.hpp b/barretenberg/cpp/src/barretenberg/proof_system/relations/relation_parameters.hpp index cd6325587e1..4f218c0b709 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/relations/relation_parameters.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/relations/relation_parameters.hpp @@ -1,5 +1,5 @@ #pragma once - +#include namespace proof_system { /** @@ -8,6 +8,7 @@ namespace proof_system { * @tparam FF */ template struct RelationParameters { + static const int NUM_BINARY_LIMBS_IN_GOBLIN_TRANSLATOR = 4; FF eta = FF(0); // Lookup FF beta = FF(0); // Permutation + Lookup FF gamma = FF(0); // Permutation + Lookup @@ -18,6 +19,7 @@ template struct RelationParameters { // eccvm_set_permutation_delta is used in the set membership gadget in eccvm/ecc_set_relation.hpp // We can remove this by modifying the relation, but increases complexity FF eccvm_set_permutation_delta = 0; + std::array accumulated_result = { FF(0) }; // Goblin Translator static RelationParameters get_random() { @@ -32,6 +34,10 @@ template struct RelationParameters { result.eccvm_set_permutation_delta = result.gamma * (result.gamma + result.beta_sqr) * (result.gamma + result.beta_sqr + result.beta_sqr) * (result.gamma + result.beta_sqr + result.beta_sqr + result.beta_sqr); + result.accumulated_result = { + FF::random_element(), FF::random_element(), FF::random_element(), FF::random_element() + }; + return result; } };