From 9e4222087e9bfdd6dcd8e693798096d17e002e60 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Mon, 11 Dec 2023 22:57:44 +0000 Subject: [PATCH 01/11] wip --- .../cpp/src/barretenberg/flavor/toy_avm.hpp | 103 ++++---- .../toy_avm/generic_lookup_relation.cpp | 29 +++ .../toy_avm/generic_lookup_relation.hpp | 230 ++++++++++++++++++ .../toy_avm/generic_permutation_relation.cpp | 7 +- .../toy_avm/generic_permutation_relation.hpp | 2 +- .../relations/toy_avm/relation_definer.hpp | 77 +++++- 6 files changed, 394 insertions(+), 54 deletions(-) create mode 100644 barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp create mode 100644 barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp diff --git a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp index b781e842d3ec..b95f3c0a385c 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp @@ -7,6 +7,7 @@ #include "barretenberg/polynomials/univariate.hpp" #include "barretenberg/relations/relation_parameters.hpp" #include "barretenberg/relations/relation_types.hpp" +#include "barretenberg/relations/toy_avm/generic_lookup_relation.hpp" #include "barretenberg/relations/toy_avm/generic_permutation_relation.hpp" #include "barretenberg/relations/toy_avm/relation_definer.hpp" #include "relation_definitions_fwd.hpp" @@ -85,7 +86,9 @@ class ToyAVM { enable_tuple_set_permutation, // column 1 enable_single_column_permutation, // column 2 enable_first_set_permutation, // column 3 - enable_second_set_permutation) // column 4 + enable_second_set_permutation, // column 4 + lookup_is_range_constrained, // column 5 + lookup_is_table_entry) // column 6 RefVector get_selectors() { @@ -93,7 +96,9 @@ class ToyAVM { enable_tuple_set_permutation, enable_single_column_permutation, enable_first_set_permutation, - enable_second_set_permutation }; + enable_second_set_permutation, + lookup_is_range_constrained, + lookup_is_table_entry }; }; RefVector get_sigma_polynomials() { return {}; }; RefVector get_id_polynomials() { return {}; }; @@ -108,21 +113,22 @@ class ToyAVM { template class WitnessEntities { public: DEFINE_FLAVOR_MEMBERS(DataType, - permutation_set_column_1, // Column 0 - permutation_set_column_2, // Column 1 - permutation_set_column_3, // Column 2 - permutation_set_column_4, // Column 3 - self_permutation_column, // Column 4 - tuple_permutation_inverses, // Column 5 - single_permutation_inverses) // Column 6 + permutation_set_column_1, // Column 0 + permutation_set_column_2, // Column 1 + permutation_set_column_3, // Column 2 + permutation_set_column_4, // Column 3 + self_permutation_column, // Column 4 + lookup_range_constraint_read_count, + range_constrained_column, + tuple_permutation_inverses, // Column 5 + single_permutation_inverses, + lookup_range_constraint_inverses) // Column 6 RefVector get_wires() { - return { permutation_set_column_1, - permutation_set_column_2, - permutation_set_column_3, - permutation_set_column_4, - self_permutation_column }; + return { permutation_set_column_1, permutation_set_column_2, permutation_set_column_3, + permutation_set_column_4, self_permutation_column, lookup_range_constraint_read_count, + range_constrained_column }; }; }; @@ -139,39 +145,51 @@ class ToyAVM { template class AllEntities { public: DEFINE_FLAVOR_MEMBERS(DataType, - lagrange_first, // Column 0 - enable_tuple_set_permutation, // Column 1 - enable_single_column_permutation, // Column 2 - enable_first_set_permutation, // Column 3 - enable_second_set_permutation, // Column 4 - permutation_set_column_1, // Column 5 - permutation_set_column_2, // Column 6 - permutation_set_column_3, // Column 7 - permutation_set_column_4, // Column 8 - self_permutation_column, // Column 9 - tuple_permutation_inverses, // Column 10 - single_permutation_inverses) // Column 11 + lagrange_first, // column 0 + enable_tuple_set_permutation, // column 1 + enable_single_column_permutation, // column 2 + enable_first_set_permutation, // column 3 + enable_second_set_permutation, // column 4 + lookup_is_range_constrained, // column 5 + lookup_is_table_entry, // column 6 + permutation_set_column_1, // Column 0 + permutation_set_column_2, // Column 1 + permutation_set_column_3, // Column 2 + permutation_set_column_4, // Column 3 + self_permutation_column, // Column 4 + lookup_range_constraint_read_count, + range_constrained_column, + tuple_permutation_inverses, // Column 5 + single_permutation_inverses, + lookup_range_constraint_inverses) // Column 11 RefVector get_wires() { - return { - permutation_set_column_1, permutation_set_column_2, permutation_set_column_3, permutation_set_column_4 - }; + return { permutation_set_column_1, permutation_set_column_2, permutation_set_column_3, + permutation_set_column_4, self_permutation_column, lookup_range_constraint_read_count, + range_constrained_column }; }; RefVector get_unshifted() { - return { lagrange_first, - enable_tuple_set_permutation, - enable_single_column_permutation, - enable_first_set_permutation, - enable_second_set_permutation, - permutation_set_column_1, - permutation_set_column_2, - permutation_set_column_3, - permutation_set_column_4, - self_permutation_column, - tuple_permutation_inverses, - single_permutation_inverses }; + return { lagrange_first, // column 0 + enable_tuple_set_permutation, // column 1 + enable_single_column_permutation, // column 2 + enable_first_set_permutation, // column 3 + enable_second_set_permutation, // column 4 + lookup_is_range_constrained, // column 5 + lookup_is_table_entry, // column 6 + permutation_set_column_1, // Column 0 + permutation_set_column_2, // Column 1 + permutation_set_column_3, // Column 2 + permutation_set_column_4, // Column 3 + self_permutation_column, // Column 4 + lookup_range_constraint_read_count, + range_constrained_column, + tuple_permutation_inverses, // Column 5 + single_permutation_inverses, + lookup_range_constraint_inverses + + }; }; RefVector get_to_be_shifted() { return {}; }; RefVector get_shifted() { return {}; }; @@ -354,7 +372,8 @@ class ToyAVM { } // namespace flavor namespace sumcheck { -DECLARE_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericPermutationRelationImpl, flavor::ToyAVM) +DECLARE_PERMUTATION_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericPermutationRelationImpl, flavor::ToyAVM) +DECLARE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericLookupRelationImpl, flavor::ToyAVM) } // namespace sumcheck } // namespace proof_system::honk diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp new file mode 100644 index 000000000000..8b53274d63fb --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp @@ -0,0 +1,29 @@ +#include "generic_lookup_relation.hpp" +#include "barretenberg/flavor/relation_definitions_fwd.hpp" +#include "barretenberg/flavor/toy_avm.hpp" +#include "barretenberg/honk/proof_system/logderivative_library.hpp" +#include "relation_definer.hpp" + +namespace proof_system::honk::sumcheck { + +/** + * @brief Expression for generic log-derivative-based set permutation. + * @param accumulator transformed to `evals + C(in(X)...)*scaling_factor` + * @param in an std::array containing the fully extended Accumulator edges. + * @param relation_params contains beta, gamma, and public_input_delta, .... + * @param scaling_factor optional term to scale the evaluation before adding to evals. + */ +template +template +void GenericLookupRelationImpl::accumulate(ContainerOverSubrelations& accumulator, + const AllEntities& in, + const Parameters& params, + const FF& scaling_factor) +{ + logderivative_library::accumulate_logderivative_permutation_subrelation_contributions< + FF, + GenericPermutationRelationImpl>(accumulator, in, params, scaling_factor); +} + +// DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericLookupRelationImpl, flavor::ToyAVM); +} // namespace proof_system::honk::sumcheck diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp new file mode 100644 index 000000000000..b6d00f66cf95 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -0,0 +1,230 @@ +/** + * @file generic_lookup_relation.hpp + * @author Rumata888 + * @brief This file contains the template for the generic lookup that can be specialized to enforce various + * lookups (for explanation on how to define them, see "relation_definer.hpp") + * + * @details Lookup is a mechanism to ensure that a particular value or tuple of values (these can be values of + * witnesses, selectors or function of these) is contained withing a particular set. It is a relative of set + * permutation, but has a one-to-many relationship beween elements that are being looked up and the table of values they + * are being looked up from. In this relation template we use the following terminology: + * + READ - the action of looking up the value in the table + * + WRITE - the action of adding the value to the lookup table + * + * TODO(@Rumata888): Talk to Zac why "lookup_read_count" refers to the count of the looked up element in the multiset. + * (The value is applied to the write predicate, so it is confusing). + */ +#pragma once +#include +#include + +#include "barretenberg/common/constexpr_utils.hpp" +#include "barretenberg/polynomials/polynomial.hpp" +#include "barretenberg/polynomials/univariate.hpp" +#include "barretenberg/relations/relation_types.hpp" + +namespace proof_system::honk::sumcheck { +/** + * @brief Specifies positions of elements in the tuple of entities received from methods in the Settings class + * + */ + +template class GenericLookupRelationImpl { + public: + using FF = FF_; + // Read and write terms counts should stay set to 1 unless we want to permute several columns at once as accumulated + // sets (not as tuples). + static constexpr size_t READ_TERMS = Settings::READ_TERMS; + static constexpr size_t WRITE_TERMS = Settings::WRITE_TERMS; + + static constexpr size_t LOOKUP_TUPLE_SIZE = Settings::LOOKUP_TUPLE_SIZE; + // 1 + polynomial degree of this relation + static constexpr size_t LENGTH = READ_TERMS + WRITE_TERMS + 3; // 5 + + static constexpr size_t INVERSE_POLYNOMIAL_INDEX = 0; + static constexpr size_t LOOKUP_READ_COUNT_START_POLYNOMIAL_INDEX = 1; + static constexpr size_t LOOKUP_READ_TERM_PREDICATE_START_POLYNOMIAL_INDEX = + LOOKUP_READ_COUNT_START_POLYNOMIAL_INDEX + WRITE_TERMS; + static constexpr size_t LOOKUP_WRITE_TERM_PREDICATE_START_POLYNOMIAL_INDEX = + LOOKUP_READ_TERM_PREDICATE_START_POLYNOMIAL_INDEX + READ_TERMS; + static constexpr size_t LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX = + LOOKUP_WRITE_TERM_PREDICATE_START_POLYNOMIAL_INDEX + WRITE_TERMS; + + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + LENGTH, // inverse polynomial correctness sub-relation + LENGTH // log-derived terms subrelation + }; + + /** + * @brief We apply the power polynomial only to the first subrelation + * + *@details The first subrelation establishes correspondence between the inverse polynomial elements and the terms. + *The second relation computes the inverses of individual terms, which are then summed up with sumcheck + * + */ + static constexpr std::array SUBRELATION_LINEARLY_INDEPENDENT = { true, false }; + + /** + * @brief Check if we need to compute the inverse polynomial element value for this row + * @details This proxies to a method in the Settings class + * + * @param row All values at row + */ + template static bool operation_exists_at_row(const AllValues& row) + + { + return Settings::inverse_polynomial_is_computed_at_row(row); + } + + /** + * @brief Get the inverse permutation polynomial (needed to compute its value) + * + */ + template static auto& get_inverse_polynomial(AllEntities& in) + { + // WIRE containing the inverse of the product of terms at this row. Used to reconstruct individual inversed + // terms + return std::get(Settings::get_nonconst_entities(in)); + } + + /** + * @brief Get selector/wire switching on(1) or off(0) inverse computation + * + */ + template + static Accumulator compute_inverse_exists(const AllEntities& in) + { + + // A lookup could be enabled by one of several selectors or witnesses, so we want to give as much freedom as + // possible to the implementor + return Settings::template compute_inverse_exists(in); + } + + /** + * @brief Returns the number of times a particular value is written (how many times it is being looked up) + * + * @details Lookup read counts should be independent columns, so there is no need to call a separate function + * + * @tparam Accumulator + * @tparam index The index of the write predicate to which this count belongs + * @tparam AllEntities + * @param in + * @return Accumulator + */ + template + static Accumulator lookup_read_counts(const AllEntities& in) + { + + static_assert(index < WRITE_TERMS); + using View = typename Accumulator::View; + + return Accumulator( + View(std::get(Settings::get_const_entities(in)))); + } + /** + * @brief Compute if the value from the first set exists in this row + * + * @tparam read_index Kept for compatibility with lookups, behavior doesn't change + */ + template + static Accumulator compute_read_term_predicate(const AllEntities& in) + + { + static_assert(read_index < READ_TERMS); + using View = typename Accumulator::View; + + // The selector/wire value that determines that an element from the first set needs to be included. Can be + // different from the wire used in the write part. + return Accumulator(View(std::get( + Settings::get_const_entities(in)))); + } + + /** + * @brief Compute if the value from the second set exists in this row + * + * @tparam write_index Kept for compatibility with lookups, behavior doesn't change + */ + template + static Accumulator compute_write_term_predicate(const AllEntities& in) + { + + static_assert(write_index < WRITE_TERMS); + using View = typename Accumulator::View; + + // The selector/wire value that determines that an element from the first set needs to be included. Can be + // different from the wire used in the write part. + return Accumulator(View(std::get( + Settings::get_const_entities(in)))); + } + + /** + * @brief Compute the value of a single item in the set + * + * @details Computes the polynomial \gamma + \sum_{i=0}^{num_columns}(column_i*\beta^i), so the tuple of columns is + * in the first set + * + * @tparam read_index The chosen polynomial relation + * + * @param params Used for beta and gamma + */ + template + static Accumulator compute_read_term(const AllEntities& in, const Parameters& params) + { + using View = typename Accumulator::View; + + static_assert(read_index < READ_TERMS); + + // Retrieve all polynomials used + const auto all_polynomials = Settings::get_const_entities(in); + + auto result = Accumulator(0); + + // Iterate over tuple and sum as a polynomial over beta + barretenberg::constexpr_for( + [&]() { result = result * params.beta + View(std::get(all_polynomials)); }); + + const auto& gamma = params.gamma; + return result + gamma; + } + + /** + * @brief Compute the value of a single item in the set + * + * @details Computes the polynomial \gamma + \sum_{i=0}^{num_columns}(column_i*\beta^i), so the tuple of columns is + * in the second set + * + * @tparam write_index Kept for compatibility with lookups, behavior doesn't change + * + * @param params Used for beta and gamma + */ + template + static Accumulator compute_write_term(const AllEntities& in, const Parameters& params) + { + + static_assert(write_index < WRITE_TERMS); + + // Sometimes we construct lookup tables on the fly from intermediate + return Settings::template compute_write_term(in, params); + } + + /** + * @brief Expression for generic log-derivative-based set permutation. + * @param accumulator transformed to `evals + C(in(X)...)*scaling_factor` + * @param in an std::array containing the fully extended Accumulator edges. + * @param relation_params contains beta, gamma, and public_input_delta, .... + * @param scaling_factor optional term to scale the evaluation before adding to evals. + */ + template + static void accumulate(ContainerOverSubrelations& accumulator, + const AllEntities& in, + const Parameters& params, + const FF& scaling_factor); +}; + +template +using GenericLookupRelation = Relation>; + +} // namespace proof_system::honk::sumcheck diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.cpp index 1822c388c4e7..248bea80cfe2 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.cpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.cpp @@ -25,10 +25,5 @@ void GenericPermutationRelationImpl::accumulate(ContainerOverSubre GenericPermutationRelationImpl>(accumulator, in, params, scaling_factor); } -// template class GenericPermutationRelationImpl; -// template -// using GenericPermutationRelationExampleSettingsImpl = GenericPermutationRelationImpl; DEFINE_SUMCHECK_RELATION_CLASS(GenericPermutationRelationExampleSettingsImpl, flavor::AVMTemplate); - -DEFINE_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericPermutationRelationImpl, flavor::ToyAVM); +DEFINE_PERMUTATION_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericPermutationRelationImpl, flavor::ToyAVM); } // namespace proof_system::honk::sumcheck diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.hpp index d4246a423f5c..0f91ee55ad4f 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_permutation_relation.hpp @@ -101,7 +101,7 @@ template class GenericPermutationRelationImpl static Accumulator compute_read_term_predicate(const AllEntities& in) { - static_assert(read_index < WRITE_TERMS); + static_assert(read_index < READ_TERMS); using View = typename Accumulator::View; // The selector/wire value that determines that an element from the first set needs to be included. Can be diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index 4771c1260b7d..0d7a466e6f15 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -193,21 +193,88 @@ class ExampleSameWirePermutationSettings { } }; +class ExampleLookupBasedRangeConstraintSettings { + public: + static constexpr size_t READ_TERMS = 1; + static constexpr size_t WRITE_TERMS = 1; + static constexpr size_t LOOKUP_TUPLE_SIZE = 1; + + /** + * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the + * value needs to be set to zero. + * + * @details If this is true then the lookup takes place in this row + * + */ + template static inline bool inverse_polynomial_is_computed_at_row(const AllEntities& in) + { + return (in.lookup_is_range_constrained == 1) || (in.lookup_is_table_entry == 1); + } + + template + static Accumulator compute_inverse_exists(const AllEntities& in) + { + + using View = Accumulator::View; + const auto is_constrained = View(in.lookup_is_range_constrained); + const auto is_table_entry = View(in.lookup_is_table_entry); + return (is_constrained + is_table_entry + is_constrained * is_table_entry); + } + template + static Accumulator compute_write_term(const AllEntities& in, const Parameters& params) + { + + static_assert(write_index < WRITE_TERMS); + + using View = typename Accumulator::View; + return Accumulator(View(in.lookup_range_table_entries) + View(params.gamma)); + } + template static inline auto get_const_entities(const AllEntities& in) + { + + return std::forward_as_tuple( + in.lookup_range_constraint_inverses, /* The polynomial containing the inverse product*/ + in.lookup_range_constraint_read_count, /* The polynomial enabling the product check subrelation */ + in.lookup_is_range_constrained, /* Enables adding first set to the sum */ + in.lookup_is_table_entry, /* Enables adding second set to the sum */ + in.range_constrained_column /* The first set column */ + ); + } + template static inline auto get_nonconst_entities(AllEntities& in) + { + + return std::forward_as_tuple( + in.lookup_range_constraint_inverses, /* The polynomial containing the inverse product*/ + in.lookup_range_constraint_read_count, /* The polynomial enabling the product check subrelation */ + in.lookup_is_range_constrained, /* Enables adding first set to the sum */ + in.lookup_is_table_entry, /* Enables adding second set to the sum */ + in.range_constrained_column /* The first set column */ + ); + } +}; + #define DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, Settings) \ template class RelationImplementation; \ template using RelationImplementation##Settings = RelationImplementation; \ DEFINE_SUMCHECK_RELATION_CLASS(RelationImplementation##Settings, flavor); -#define DEFINE_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ - DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleTuplePermutationSettings); \ - DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleSameWirePermutationSettings); - #define DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, Settings) \ extern template class RelationImplementation; \ template using RelationImplementation##Settings = RelationImplementation; \ DECLARE_SUMCHECK_RELATION_CLASS(RelationImplementation##Settings, flavor); -#define DECLARE_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ +#define DEFINE_PERMUTATION_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ + DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleTuplePermutationSettings); \ + DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleSameWirePermutationSettings); + +#define DECLARE_PERMUTATION_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleTuplePermutationSettings); \ DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleSameWirePermutationSettings); + +#define DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ + DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleLookupBasedRangeConstraintSettings); + +#define DECLARE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ + DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleLookupBasedRangeConstraintSettings); + } // namespace proof_system::honk::sumcheck \ No newline at end of file From e145fc7753a2728e114bd125066418b0f2741bbe Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Wed, 13 Dec 2023 23:51:21 +0000 Subject: [PATCH 02/11] Range constraint works. Horribly --- .../cpp/src/barretenberg/flavor/toy_avm.hpp | 36 +++++++------- .../toy_avm/toy_avm_circuit_builder.hpp | 48 +++++++++++++++++++ .../toy_avm/toy_avm_circuit_builder.test.cpp | 9 +++- .../toy_avm/generic_lookup_relation.cpp | 8 ++-- .../toy_avm/generic_lookup_relation.hpp | 6 +-- .../relations/toy_avm/relation_definer.hpp | 5 +- 6 files changed, 85 insertions(+), 27 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp index b95f3c0a385c..22f7e350fae7 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp @@ -44,17 +44,17 @@ class ToyAVM { // The number of wires is 5. The set of tuples (permutation_set_column_1,permutation_set_column_2) should be // equivalent to (permutation_set_column_3, permutation_set_column_4) and the self_permutation_column contains 2 // subsets which are permutations of each other - static constexpr size_t NUM_WIRES = 5; + static constexpr size_t NUM_WIRES = 6; // The number of multivariate polynomials on which a sumcheck prover sumcheck operates (including shifts). We often // need containers of this size to hold related data, so we choose a name more agnostic than `NUM_POLYNOMIALS`. // Note: this number does not include the individual sorted list polynomials. - static constexpr size_t NUM_ALL_ENTITIES = 12; + static constexpr size_t NUM_ALL_ENTITIES = 18; // The number of polynomials precomputed to describe a circuit and to aid a prover in constructing a satisfying // assignment of witnesses. We again choose a neutral name. - static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 5; + static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 8; // The total number of witness entities not including shifts. - static constexpr size_t NUM_WITNESS_ENTITIES = 7; + static constexpr size_t NUM_WITNESS_ENTITIES = 10; // define the tuple of Relations that comprise the Sumcheck relation using Relations = std::tuple>; @@ -88,7 +88,8 @@ class ToyAVM { enable_first_set_permutation, // column 3 enable_second_set_permutation, // column 4 lookup_is_range_constrained, // column 5 - lookup_is_table_entry) // column 6 + lookup_is_table_entry, // column 6 + lookup_range_table_entries) // column 7 RefVector get_selectors() { @@ -98,7 +99,8 @@ class ToyAVM { enable_first_set_permutation, enable_second_set_permutation, lookup_is_range_constrained, - lookup_is_table_entry }; + lookup_is_table_entry, + lookup_range_table_entries }; }; RefVector get_sigma_polynomials() { return {}; }; RefVector get_id_polynomials() { return {}; }; @@ -152,11 +154,12 @@ class ToyAVM { enable_second_set_permutation, // column 4 lookup_is_range_constrained, // column 5 lookup_is_table_entry, // column 6 - permutation_set_column_1, // Column 0 - permutation_set_column_2, // Column 1 - permutation_set_column_3, // Column 2 - permutation_set_column_4, // Column 3 - self_permutation_column, // Column 4 + lookup_range_table_entries, + permutation_set_column_1, // Column 0 + permutation_set_column_2, // Column 1 + permutation_set_column_3, // Column 2 + permutation_set_column_4, // Column 3 + self_permutation_column, // Column 4 lookup_range_constraint_read_count, range_constrained_column, tuple_permutation_inverses, // Column 5 @@ -178,11 +181,12 @@ class ToyAVM { enable_second_set_permutation, // column 4 lookup_is_range_constrained, // column 5 lookup_is_table_entry, // column 6 - permutation_set_column_1, // Column 0 - permutation_set_column_2, // Column 1 - permutation_set_column_3, // Column 2 - permutation_set_column_4, // Column 3 - self_permutation_column, // Column 4 + lookup_range_table_entries, + permutation_set_column_1, // Column 0 + permutation_set_column_2, // Column 1 + permutation_set_column_3, // Column 2 + permutation_set_column_4, // Column 3 + self_permutation_column, // Column 4 lookup_range_constraint_read_count, range_constrained_column, tuple_permutation_inverses, // Column 5 diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp index 93199a9dda0c..9c4d2db765b5 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp @@ -52,6 +52,12 @@ template class ToyAVMCircuitBuilder { const auto num_gates_log2 = static_cast(numeric::get_msb64(num_gates)); size_t num_gates_pow2 = 1UL << (num_gates_log2 + (1UL << num_gates_log2 == num_gates ? 0 : 1)); + // We need at least 256 values for the range constraint + num_gates_pow2 = num_gates_pow2 > 256 ? num_gates_pow2 : 256; + + // We need at least 256 values for the range constraint + num_gates_pow2 = num_gates_pow2 > 256 ? num_gates_pow2 : 256; + ProverPolynomials polys; for (Polynomial& poly : polys.get_all()) { poly = Polynomial(num_gates_pow2); @@ -66,12 +72,30 @@ template class ToyAVMCircuitBuilder { polys.permutation_set_column_3[i] = wires[2][i]; polys.permutation_set_column_4[i] = wires[3][i]; polys.self_permutation_column[i] = wires[4][i]; + // By default the permutation is over all rows where we place data polys.enable_tuple_set_permutation[i] = 1; // The same column permutation alternates between even and odd values polys.enable_single_column_permutation[i] = 1; polys.enable_first_set_permutation[i] = i & 1; polys.enable_second_set_permutation[i] = 1 - (i & 1); + + // Lookup-based range constraint related values + + // Store the value + polys.range_constrained_column[i] = wires[5][i]; + // Make range constrained + polys.lookup_is_range_constrained[i] = 1; + uint256_t constrained_value = wires[5][i]; + // If the value is correct, update the appropriate counter + if (constrained_value < 256) { + polys.lookup_range_constraint_read_count[static_cast(constrained_value.data[0])] = + polys.lookup_range_constraint_read_count[static_cast(constrained_value.data[0])] + 1; + } + } + for (size_t i = 0; i < 256; i++) { + polys.lookup_is_table_entry[i] = FF(1); + polys.lookup_range_table_entries[i] = FF(i); } return polys; } @@ -147,6 +171,30 @@ template class ToyAVMCircuitBuilder { return false; } } + + // Check the range constraint relation + proof_system::honk::logderivative_library::compute_logderivative_inverse< + Flavor, + honk::sumcheck::GenericLookupRelation>( + polynomials, params, num_rows); + + using LookupRelation = + honk::sumcheck::GenericLookupRelation; + typename honk::sumcheck::GenericLookupRelation::SumcheckArrayOfValuesOverSubrelations + range_constraint_result; + for (auto& r : range_constraint_result) { + r = 0; + } + for (size_t i = 0; i < num_rows; ++i) { + LookupRelation::accumulate(range_constraint_result, polynomials.get_row(i), params, 1); + } + for (auto r : range_constraint_result) { + if (r != 0) { + info("RangeConstraintRelation failed."); + return false; + } + } return true; } diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp index 62b2e4d83c3b..c55e503d9c64 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp @@ -38,7 +38,12 @@ TEST(ToyAVMCircuitBuilder, BaseCase) for (size_t i = 0; i < circuit_size; i++) { // We put the same tuple of values in the first 2 wires and in the next 2 to at different rows // We also put the same value in the self_permutation column in 2 consecutive rows - circuit_builder.add_row({ column_0[i], column_1[i], column_0[15 - i], column_1[15 - i], column_2[i / 2] }); + circuit_builder.add_row({ column_0[i], + column_1[i], + column_0[15 - i], + column_1[15 - i], + column_2[i / 2], + engine.get_random_uint8() }); } // Test that permutations with correct values work @@ -63,7 +68,7 @@ TEST(ToyAVMCircuitBuilder, BaseCase) EXPECT_EQ(result, true); // Break single-column permutation - circuit_builder.wires[circuit_builder.wires.size() - 1][0] = FF::random_element(); + circuit_builder.wires[4][0] = FF::random_element(); result = circuit_builder.check_circuit(); EXPECT_EQ(result, false); } diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp index 8b53274d63fb..2bc40089a75b 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.cpp @@ -20,10 +20,10 @@ void GenericLookupRelationImpl::accumulate(ContainerOverSubrelatio const Parameters& params, const FF& scaling_factor) { - logderivative_library::accumulate_logderivative_permutation_subrelation_contributions< - FF, - GenericPermutationRelationImpl>(accumulator, in, params, scaling_factor); + logderivative_library:: + accumulate_logderivative_lookup_subrelation_contributions>( + accumulator, in, params, scaling_factor); } -// DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericLookupRelationImpl, flavor::ToyAVM); +DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericLookupRelationImpl, flavor::ToyAVM); } // namespace proof_system::honk::sumcheck diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp index b6d00f66cf95..4e1516ca8bc0 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -181,10 +181,9 @@ template class GenericLookupRelationImpl { // Iterate over tuple and sum as a polynomial over beta barretenberg::constexpr_for( - [&]() { result = result * params.beta + View(std::get(all_polynomials)); }); + [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); const auto& gamma = params.gamma; return result + gamma; @@ -207,6 +206,7 @@ template class GenericLookupRelationImpl { static_assert(write_index < WRITE_TERMS); // Sometimes we construct lookup tables on the fly from intermediate + return Settings::template compute_write_term(in, params); } diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index 0d7a466e6f15..8b7c557d5187 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -218,7 +218,7 @@ class ExampleLookupBasedRangeConstraintSettings { using View = Accumulator::View; const auto is_constrained = View(in.lookup_is_range_constrained); const auto is_table_entry = View(in.lookup_is_table_entry); - return (is_constrained + is_table_entry + is_constrained * is_table_entry); + return (is_constrained + is_table_entry - is_constrained * is_table_entry); } template static Accumulator compute_write_term(const AllEntities& in, const Parameters& params) @@ -227,7 +227,8 @@ class ExampleLookupBasedRangeConstraintSettings { static_assert(write_index < WRITE_TERMS); using View = typename Accumulator::View; - return Accumulator(View(in.lookup_range_table_entries) + View(params.gamma)); + info("Write value: ", View(in.lookup_range_table_entries)); + return Accumulator(View(in.lookup_range_table_entries) + params.gamma); } template static inline auto get_const_entities(const AllEntities& in) { From bb8625db273c5658ca55d7a39b8b8d2d8ead4b58 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Wed, 13 Dec 2023 23:53:43 +0000 Subject: [PATCH 03/11] Goodbye stray info --- .../cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp | 1 - 1 file changed, 1 deletion(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index 8b7c557d5187..2b84789b1f74 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -227,7 +227,6 @@ class ExampleLookupBasedRangeConstraintSettings { static_assert(write_index < WRITE_TERMS); using View = typename Accumulator::View; - info("Write value: ", View(in.lookup_range_table_entries)); return Accumulator(View(in.lookup_range_table_entries) + params.gamma); } template static inline auto get_const_entities(const AllEntities& in) From 88fe516f1fa180611c619570105f1eb43f1251dd Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Mon, 18 Dec 2023 17:28:42 +0000 Subject: [PATCH 04/11] Generic stuff works, cleaning up --- .../toy_avm/generic_lookup_relation.hpp | 106 +++++++++++++++--- .../relations/toy_avm/relation_definer.hpp | 11 +- 2 files changed, 96 insertions(+), 21 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp index 4e1516ca8bc0..1538197d4712 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -41,6 +41,28 @@ template class GenericLookupRelationImpl { // 1 + polynomial degree of this relation static constexpr size_t LENGTH = READ_TERMS + WRITE_TERMS + 3; // 5 + // The structure of polynomial tuple returned from Settings' functions get_const_entities and get_nonconst_entities + // is the following: + // 1) 1 Polynomial used to contain the inverse product from which we reconstruct individual inverses + // used in the sum + // 2) WRITE_TERMS number of polynomials representing how much each write term has been read + // 3) READ_TERMS number of polynomials enabling the addition of a particular read term in this row (should we lookup + // or not) + // 4) WRITE_TERMS number of polynomials enabling a particular write term in this row (should we add it to + // the lookup table or not) + // 5) Depending on the type of read terms (BASIC_TUPLE, SCALED_TUPLE or ARBITRARY): + // 1. In case of basic tuple READ_TERMS polynomials the combination of whose values in a row is supposed to + // represent the looked up entry + // 2. In case of scaled tuple there are READ_TERMS previous accumulator polynomials, READ_TERMS + // scaling polynomials and READ_TERMS current accumulator polynomials. The tuple is comprised of values + // (current_accumulator-scale*previous_accumulator) + // 3. In the arbitrary case the are no additional read_term + // polynomials, because the logic is completely decided in the settings + // 6) Depending on the type of read terms (BASIC_TUPLE or ARBITRARY): + // 1. In case of basic tuple WRITE_TERNS polynomials the combination of whose values in a row is supposed to + // represent the entry written into the lookup table + // 2. In the arbitrary case the are no additional write term polynomials, + // because the logic is completely decided in the settings static constexpr size_t INVERSE_POLYNOMIAL_INDEX = 0; static constexpr size_t LOOKUP_READ_COUNT_START_POLYNOMIAL_INDEX = 1; static constexpr size_t LOOKUP_READ_TERM_PREDICATE_START_POLYNOMIAL_INDEX = @@ -173,20 +195,43 @@ template class GenericLookupRelationImpl { using View = typename Accumulator::View; static_assert(read_index < READ_TERMS); - - // Retrieve all polynomials used - const auto all_polynomials = Settings::get_const_entities(in); - - auto result = Accumulator(0); - - // Iterate over tuple and sum as a polynomial over beta - barretenberg::constexpr_for( - [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); - - const auto& gamma = params.gamma; - return result + gamma; + static_assert(Settings::READ_TERM_TYPE < 3); + static_assert(Settings::READ_TERM_TYPE >= 0); + enum READ_TERM_TYPES { BASIC_TUPLE = 0, SCALED_TUPLE, ARBITRARY }; + + if constexpr (Settings::READ_TERM_TYPE == BASIC_TUPLE) { + // Retrieve all polynomials used + const auto all_polynomials = Settings::get_const_entities(in); + + auto result = Accumulator(0); + + // Iterate over tuple and sum as a polynomial over beta + barretenberg::constexpr_for( + [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); + const auto& gamma = params.gamma; + return result + gamma; + } else if constexpr (Settings::READ_TERM_TYPE == SCALED_TUPLE) { + // Retrieve all polynomials used + const auto all_polynomials = Settings::get_const_entities(in); + + auto result = Accumulator(0); + // Iterate over tuple and sum as a polynomial over beta + barretenberg::constexpr_for< + LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + read_index * 3 * LOOKUP_TUPLE_SIZE, + LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + (read_index * 3 + 1) * LOOKUP_TUPLE_SIZE, + 1>([&]() { + result = (result * params.beta) + View(std::get(all_polynomials)) - + View(std::get(all_polynomials)) * View(std::get(all_polynomials)); + }); + const auto& gamma = params.gamma; + return result + gamma; + } else { + + return Settings::template compute_read_term(in, params); + } } /** @@ -204,10 +249,37 @@ template class GenericLookupRelationImpl { { static_assert(write_index < WRITE_TERMS); + static_assert(Settings::WRITE_TERM_TYPE < 2); + static_assert(Settings::WRITE_TERM_TYPE >= 0); + static_assert(Settings::READ_TERM_TYPE < 3); + static_assert(Settings::READ_TERM_TYPE >= 0); + enum READ_TERM_TYPES { BASIC_TUPLE = 0, SCALED_TUPLE, ARBITRARY }; + enum WRITE_TERM_TYPES { WRITE_BASIC_TUPLE = 0, WRITE_ARBITRARY }; - // Sometimes we construct lookup tables on the fly from intermediate - - return Settings::template compute_write_term(in, params); + using View = typename Accumulator::View; + // Write term offset is dependet on which read term computation method is used + constexpr size_t WRITE_TERMS_OFFSET = LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + + (Settings::READ_TERM_TYPE == BASIC_TUPLE ? LOOKUP_TUPLE_SIZE + : Settings::READ_TERM_TYPE == SCALED_TUPLE ? LOOKUP_TUPLE_SIZE * 3 + : 0); + if constexpr (Settings::WRITE_TERM_TYPE == WRITE_BASIC_TUPLE) { + // Retrieve all polynomials used + const auto all_polynomials = Settings::get_const_entities(in); + + auto result = Accumulator(0); + + // Iterate over tuple and sum as a polynomial over beta + barretenberg::constexpr_for( + [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); + const auto& gamma = params.gamma; + return result + gamma; + } else { + // Sometimes we construct lookup tables on the fly from intermediate + + return Settings::template compute_write_term(in, params); + } } /** diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index 2b84789b1f74..e20f17f29def 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -195,9 +195,12 @@ class ExampleSameWirePermutationSettings { class ExampleLookupBasedRangeConstraintSettings { public: + static constexpr size_t READ_TERM_TYPE = 0; + static constexpr size_t WRITE_TERM_TYPE = 0; static constexpr size_t READ_TERMS = 1; static constexpr size_t WRITE_TERMS = 1; static constexpr size_t LOOKUP_TUPLE_SIZE = 1; + static constexpr size_t INVERSE_EXISTS_COMPLEXITY = 2; /** * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the @@ -237,8 +240,8 @@ class ExampleLookupBasedRangeConstraintSettings { in.lookup_range_constraint_read_count, /* The polynomial enabling the product check subrelation */ in.lookup_is_range_constrained, /* Enables adding first set to the sum */ in.lookup_is_table_entry, /* Enables adding second set to the sum */ - in.range_constrained_column /* The first set column */ - ); + in.range_constrained_column, /* The first set column */ + in.lookup_range_table_entries); } template static inline auto get_nonconst_entities(AllEntities& in) { @@ -248,8 +251,8 @@ class ExampleLookupBasedRangeConstraintSettings { in.lookup_range_constraint_read_count, /* The polynomial enabling the product check subrelation */ in.lookup_is_range_constrained, /* Enables adding first set to the sum */ in.lookup_is_table_entry, /* Enables adding second set to the sum */ - in.range_constrained_column /* The first set column */ - ); + in.range_constrained_column, /* The first set column */ + in.lookup_range_table_entries); } }; From 3027f163bc444a079b3497c8efceff7c917fcad0 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Tue, 26 Dec 2023 21:11:44 +0000 Subject: [PATCH 05/11] More comments --- .../toy_avm/generic_lookup_relation.hpp | 47 ++++++-- .../relations/toy_avm/relation_definer.hpp | 114 ++++++++++++++++-- 2 files changed, 140 insertions(+), 21 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp index 1538197d4712..62ba32401177 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -5,7 +5,7 @@ * lookups (for explanation on how to define them, see "relation_definer.hpp") * * @details Lookup is a mechanism to ensure that a particular value or tuple of values (these can be values of - * witnesses, selectors or function of these) is contained withing a particular set. It is a relative of set + * witnesses, selectors or a function of these) is contained within a particular set. It is a relative of set * permutation, but has a one-to-many relationship beween elements that are being looked up and the table of values they * are being looked up from. In this relation template we use the following terminology: * + READ - the action of looking up the value in the table @@ -32,12 +32,40 @@ namespace proof_system::honk::sumcheck { template class GenericLookupRelationImpl { public: using FF = FF_; - // Read and write terms counts should stay set to 1 unless we want to permute several columns at once as accumulated - // sets (not as tuples). + + // Read terms specified how many maximum lookups can be performed in 1 row static constexpr size_t READ_TERMS = Settings::READ_TERMS; + + // Looked up entries can be a basic tuple, a scaled tuple or completely arbitrary + enum READ_TERM_TYPES { READ_BASIC_TUPLE = 0, READ_SCALED_TUPLE, READ_ARBITRARY }; + + // Write terms specifies how many insertions into the lookup table can be performed in 1 row static constexpr size_t WRITE_TERMS = Settings::WRITE_TERMS; + // Entries put into the table are ever defined as a tuple or constructed arbitrarily + enum WRITE_TERM_TYPES { WRITE_BASIC_TUPLE = 0, WRITE_ARBITRARY }; + + // Lookup tuple size specifies how many values are bundled together to represent a single entry in the lookup table. + // For example, it would be 1 for a range constraint lookup, or 3 for XOR lookup static constexpr size_t LOOKUP_TUPLE_SIZE = Settings::LOOKUP_TUPLE_SIZE; + + // Compute the length of the inverse polynomial correctness sub-relation MAX(product of terms * inverse, inverse + // exists polynomial) + 1; + static constexpr size_t FIRST_SUBRELATION_LENGTH = + std::max((READ_TERMS + WRITE_TERMS + 1), Settings::INVERSE_EXISTS_POLYNOMIAL_DEGREE) + 1; + + // Read term degree is dependent on what type of read term we use + static constexpr size_t READ_TERM_DEGREE = Settings::READ_TERM_TYPE == READ_BASIC_TUPLE ? 1 + : Settings::READ_TERM_TYPE == READ_SCALED_TUPLE + ? 2 + : Settings::READ_TERM_DEGREE; + static_assert(READ_TERM_DEGREE != 0); + + // Write term degree is dependent on what type of write term we use + static constexpr size_t WRITE_TERM_DEGREE = + Settings::WRITE_TERM_TYPE == WRITE_BASIC_TUPLE ? 1 : Settings::WRITE_TERM_DEGREE; + // Compute the length of the log-derived term subrelation + static constexpr size_t SECOND_SUBRELATION_LENGTH = std::max(READ_TERM_DEGREE + 1, WRITE_TERM_DEGREE + 2) + 1; // 1 + polynomial degree of this relation static constexpr size_t LENGTH = READ_TERMS + WRITE_TERMS + 3; // 5 @@ -197,9 +225,8 @@ template class GenericLookupRelationImpl { static_assert(read_index < READ_TERMS); static_assert(Settings::READ_TERM_TYPE < 3); static_assert(Settings::READ_TERM_TYPE >= 0); - enum READ_TERM_TYPES { BASIC_TUPLE = 0, SCALED_TUPLE, ARBITRARY }; - if constexpr (Settings::READ_TERM_TYPE == BASIC_TUPLE) { + if constexpr (Settings::READ_TERM_TYPE == READ_BASIC_TUPLE) { // Retrieve all polynomials used const auto all_polynomials = Settings::get_const_entities(in); @@ -213,7 +240,7 @@ template class GenericLookupRelationImpl { [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); const auto& gamma = params.gamma; return result + gamma; - } else if constexpr (Settings::READ_TERM_TYPE == SCALED_TUPLE) { + } else if constexpr (Settings::READ_TERM_TYPE == READ_SCALED_TUPLE) { // Retrieve all polynomials used const auto all_polynomials = Settings::get_const_entities(in); @@ -253,15 +280,13 @@ template class GenericLookupRelationImpl { static_assert(Settings::WRITE_TERM_TYPE >= 0); static_assert(Settings::READ_TERM_TYPE < 3); static_assert(Settings::READ_TERM_TYPE >= 0); - enum READ_TERM_TYPES { BASIC_TUPLE = 0, SCALED_TUPLE, ARBITRARY }; - enum WRITE_TERM_TYPES { WRITE_BASIC_TUPLE = 0, WRITE_ARBITRARY }; using View = typename Accumulator::View; // Write term offset is dependet on which read term computation method is used constexpr size_t WRITE_TERMS_OFFSET = LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + - (Settings::READ_TERM_TYPE == BASIC_TUPLE ? LOOKUP_TUPLE_SIZE - : Settings::READ_TERM_TYPE == SCALED_TUPLE ? LOOKUP_TUPLE_SIZE * 3 - : 0); + (Settings::READ_TERM_TYPE == READ_BASIC_TUPLE ? LOOKUP_TUPLE_SIZE + : Settings::READ_TERM_TYPE == READ_SCALED_TUPLE ? LOOKUP_TUPLE_SIZE * 3 + : 0); if constexpr (Settings::WRITE_TERM_TYPE == WRITE_BASIC_TUPLE) { // Retrieve all polynomials used const auto all_polynomials = Settings::get_const_entities(in); diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index e20f17f29def..de781ce9ccfa 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -193,18 +193,86 @@ class ExampleSameWirePermutationSettings { } }; +/** + * @brief This class contains an example of how to set LookupSettings classes used by the + * GenericLookupRelationImpl class to specify a concrete permutation + * + * @details To create your own lookup: + * 1) Create a copy of this class and rename it + * 2) Update all the values with the ones needed for your permutation + * 3) Update "DECLARE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS" and "DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS" to + * include the new settings + * 4) Add the relation with the chosen settings to Relations in the flavor (for example,"` + * using Relations = std::tuple>;)` + * + */ class ExampleLookupBasedRangeConstraintSettings { public: + /** + * @brief The type of the READ_TERM (lookup operation) that we are using + * + * @details 0 stands for basic tuple lookup, where we simply lookup a tuple of values from given entities + * 1 stands for scaled tuple lookup, which uses a tuple of (current_accumulator - previous_accumulator * shift) + * values + * 2 means arbitrary expression that requires the settings to have a specific method and set the READ_TERM_DEGREE to + * the degree of the expression + * + */ static constexpr size_t READ_TERM_TYPE = 0; + /** + * @brief The type of the WRITE_TERM (lookup table entry addition) that we are using + * + * @details 0 stands for basic tuple lookup, where we simply lookup a tuple of values from given entities + * 1 means an arbitrary expression, evaluated through a method defines in these settings. In this case + * WRITE_TERM_DEGREE has to be set to the degree of the expression + * + */ static constexpr size_t WRITE_TERM_TYPE = 0; + + /** + * @brief The number of read terms (how many lookups we perform) in each row + * + */ static constexpr size_t READ_TERMS = 1; + /** + * @brief The number of write terms (how many additions to the lookup table we make) in each row + * + */ static constexpr size_t WRITE_TERMS = 1; + + /** + * @brief How many values represent a single lookup object. This value is used by the automatic read term + * implementation in the relation in case the lookup is a basic or scaled tuple and in the write term if it's a + * basic tuple + * + */ static constexpr size_t LOOKUP_TUPLE_SIZE = 1; - static constexpr size_t INVERSE_EXISTS_COMPLEXITY = 2; /** - * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the - * value needs to be set to zero. + * @brief The polynomial degree of the relation telling us if the inverse polynomial value needs to be computed + * + */ + static constexpr size_t INVERSE_EXISTS_POLYNOMIAL_DEGREE = 2; + + /** + * @brief The degree of the read term if implemented arbitrarily. This value is not used by basic and scaled read + * terms, but will cause compilation error if not defined + * + */ + static constexpr size_t READ_TERM_DEGREE = 0; + + /** + * @brief The degree of the write term if implemented arbitrarily. This value is not used by the basic write + * term, but will cause compilation error if not defined + * + */ + + static constexpr size_t WRITE_TERM_DEGREE = 0; + + /** + * @brief If this method returns true on a row of values, then the inverse polynomial exists at this index. + * Otherwise the value needs to be set to zero. * * @details If this is true then the lookup takes place in this row * @@ -214,6 +282,15 @@ class ExampleLookupBasedRangeConstraintSettings { return (in.lookup_is_range_constrained == 1) || (in.lookup_is_table_entry == 1); } + /** + * @brief Subprocedure for computing the value deciding if the inverse polynomial value needs to be checked in this + * row + * + * @tparam Accumulator Type specified by the lookup relation + * @tparam AllEntities Values/Univariates of all entities row + * @param in Value/Univariate of all entities at row/edge + * @return Accumulator + */ template static Accumulator compute_inverse_exists(const AllEntities& in) { @@ -223,15 +300,24 @@ class ExampleLookupBasedRangeConstraintSettings { const auto is_table_entry = View(in.lookup_is_table_entry); return (is_constrained + is_table_entry - is_constrained * is_table_entry); } - template - static Accumulator compute_write_term(const AllEntities& in, const Parameters& params) - { - static_assert(write_index < WRITE_TERMS); + /** + * @brief Get all the entities for the lookup when need to update them + * + * @details The generic structure of this tuple is described in ./generic_lookup_relation.hpp . The following is + description for the current case: - using View = typename Accumulator::View; - return Accumulator(View(in.lookup_range_table_entries) + params.gamma); - } + The entities are returned as a tuple of references in the following order (this is for ): + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that specifies how many times the lookup table entry at this row has been looked up + * - The entity/polynomial that enables the lookup operation at this row + * - The entity/polynomial that enables adding an entry to the lookup table in this row + * - The entity/polynomial a value from which is being looked up (since there is one entry, it simply checks if it's + contained in the set) + * - The entity/polynomial a value from which is being added to the table + * + * @return All the entities needed for the lookup + */ template static inline auto get_const_entities(const AllEntities& in) { @@ -243,6 +329,14 @@ class ExampleLookupBasedRangeConstraintSettings { in.range_constrained_column, /* The first set column */ in.lookup_range_table_entries); } + /** + * @brief Get all the entities for the lookup when only need to read them + * @details Same as in get_const_entities, but nonconst + * + * @tparam AllEntities + * @param in + * @return auto + */ template static inline auto get_nonconst_entities(AllEntities& in) { From c2ba5eed285b80899e6b477fcf8b044daecfe8bd Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Sun, 31 Dec 2023 17:36:47 +0000 Subject: [PATCH 06/11] Mini update --- .../relations/toy_avm/relation_definer.hpp | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index de781ce9ccfa..a5a2360ee09a 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -323,11 +323,11 @@ class ExampleLookupBasedRangeConstraintSettings { return std::forward_as_tuple( in.lookup_range_constraint_inverses, /* The polynomial containing the inverse product*/ - in.lookup_range_constraint_read_count, /* The polynomial enabling the product check subrelation */ - in.lookup_is_range_constrained, /* Enables adding first set to the sum */ - in.lookup_is_table_entry, /* Enables adding second set to the sum */ - in.range_constrained_column, /* The first set column */ - in.lookup_range_table_entries); + in.lookup_range_constraint_read_count, /* The polynomial containing number of reads of each table entry */ + in.lookup_is_range_constrained, /* Enables lookup action in this row */ + in.lookup_is_table_entry, /* Enables adding an entry to the table */ + in.range_constrained_column, /* Column being looked up */ + in.lookup_range_table_entries); /* Column containing table entries*/ } /** * @brief Get all the entities for the lookup when only need to read them @@ -339,14 +339,13 @@ class ExampleLookupBasedRangeConstraintSettings { */ template static inline auto get_nonconst_entities(AllEntities& in) { - return std::forward_as_tuple( in.lookup_range_constraint_inverses, /* The polynomial containing the inverse product*/ - in.lookup_range_constraint_read_count, /* The polynomial enabling the product check subrelation */ - in.lookup_is_range_constrained, /* Enables adding first set to the sum */ - in.lookup_is_table_entry, /* Enables adding second set to the sum */ - in.range_constrained_column, /* The first set column */ - in.lookup_range_table_entries); + in.lookup_range_constraint_read_count, /* The polynomial containing number of reads of each table entry */ + in.lookup_is_range_constrained, /* Enables lookup action in this row */ + in.lookup_is_table_entry, /* Enables adding an entry to the table */ + in.range_constrained_column, /* Column being looked up */ + in.lookup_range_table_entries); /* Column containing table entries*/ } }; From 4cbc1f4be242c587c87e3132825decc70eb6344c Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Tue, 2 Jan 2024 13:20:05 +0000 Subject: [PATCH 07/11] Before cleanup --- .../cpp/src/barretenberg/flavor/toy_avm.hpp | 113 ++++++-- .../toy_avm/toy_avm_circuit_builder.hpp | 62 ++++- .../toy_avm/toy_avm_circuit_builder.test.cpp | 68 ++++- .../toy_avm/generic_lookup_relation.hpp | 244 ++++++++++++++---- .../relations/toy_avm/relation_definer.hpp | 226 ++++++++++++++-- 5 files changed, 606 insertions(+), 107 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp index 22f7e350fae7..f370767fba68 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp @@ -41,20 +41,17 @@ class ToyAVM { using CommitmentKey = pcs::CommitmentKey; using VerifierCommitmentKey = pcs::VerifierCommitmentKey; - // The number of wires is 5. The set of tuples (permutation_set_column_1,permutation_set_column_2) should be - // equivalent to (permutation_set_column_3, permutation_set_column_4) and the self_permutation_column contains 2 - // subsets which are permutations of each other - static constexpr size_t NUM_WIRES = 6; + static constexpr size_t NUM_WIRES = 12; // The number of multivariate polynomials on which a sumcheck prover sumcheck operates (including shifts). We often // need containers of this size to hold related data, so we choose a name more agnostic than `NUM_POLYNOMIALS`. // Note: this number does not include the individual sorted list polynomials. - static constexpr size_t NUM_ALL_ENTITIES = 18; + static constexpr size_t NUM_ALL_ENTITIES = 32; // The number of polynomials precomputed to describe a circuit and to aid a prover in constructing a satisfying // assignment of witnesses. We again choose a neutral name. - static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 8; + static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 14; // The total number of witness entities not including shifts. - static constexpr size_t NUM_WITNESS_ENTITIES = 10; + static constexpr size_t NUM_WITNESS_ENTITIES = 18; // define the tuple of Relations that comprise the Sumcheck relation using Relations = std::tuple>; @@ -88,8 +85,14 @@ class ToyAVM { enable_first_set_permutation, // column 3 enable_second_set_permutation, // column 4 lookup_is_range_constrained, // column 5 - lookup_is_table_entry, // column 6 - lookup_range_table_entries) // column 7 + lookup_is_range_table_entry, // column 6 + lookup_range_table_entries, // column 7 + lookup_is_xor_operation, // column 8 + lookup_is_xor_table_entry, // column 9 + lookup_xor_shift, // column 10 + lookup_xor_table_1, + lookup_xor_table_2, + lookup_xor_table_3) RefVector get_selectors() { @@ -99,8 +102,14 @@ class ToyAVM { enable_first_set_permutation, enable_second_set_permutation, lookup_is_range_constrained, - lookup_is_table_entry, - lookup_range_table_entries }; + lookup_is_range_table_entry, + lookup_range_table_entries, + lookup_is_xor_operation, + lookup_is_xor_table_entry, + lookup_xor_shift, + lookup_xor_table_1, + lookup_xor_table_2, + lookup_xor_table_3 }; }; RefVector get_sigma_polynomials() { return {}; }; RefVector get_id_polynomials() { return {}; }; @@ -122,15 +131,33 @@ class ToyAVM { self_permutation_column, // Column 4 lookup_range_constraint_read_count, range_constrained_column, - tuple_permutation_inverses, // Column 5 + lookup_xor_read_count, + lookup_xor_argument_1, + lookup_xor_argument_2, + lookup_xor_result, + lookup_xor_accumulated_argument_1, + lookup_xor_accumulated_argument_2, + lookup_xor_accumulated_result, + + tuple_permutation_inverses, single_permutation_inverses, - lookup_range_constraint_inverses) // Column 6 + lookup_range_constraint_inverses, + lookup_xor_inverses) RefVector get_wires() { - return { permutation_set_column_1, permutation_set_column_2, permutation_set_column_3, - permutation_set_column_4, self_permutation_column, lookup_range_constraint_read_count, - range_constrained_column }; + return { permutation_set_column_1, + permutation_set_column_2, + permutation_set_column_3, + permutation_set_column_4, + self_permutation_column, + range_constrained_column, + lookup_xor_argument_1, + lookup_xor_argument_2, + lookup_xor_result, + lookup_xor_accumulated_argument_1, + lookup_xor_accumulated_argument_2, + lookup_xor_accumulated_result }; }; }; @@ -153,7 +180,13 @@ class ToyAVM { enable_first_set_permutation, // column 3 enable_second_set_permutation, // column 4 lookup_is_range_constrained, // column 5 - lookup_is_table_entry, // column 6 + lookup_is_range_table_entry, // column 6 + lookup_is_xor_operation, + lookup_is_xor_table_entry, + lookup_xor_shift, + lookup_xor_table_1, + lookup_xor_table_2, + lookup_xor_table_3, lookup_range_table_entries, permutation_set_column_1, // Column 0 permutation_set_column_2, // Column 1 @@ -162,15 +195,33 @@ class ToyAVM { self_permutation_column, // Column 4 lookup_range_constraint_read_count, range_constrained_column, + lookup_xor_read_count, + lookup_xor_argument_1, + lookup_xor_argument_2, + lookup_xor_result, + lookup_xor_accumulated_argument_1, + lookup_xor_accumulated_argument_2, + lookup_xor_accumulated_result, + tuple_permutation_inverses, // Column 5 single_permutation_inverses, - lookup_range_constraint_inverses) // Column 11 + lookup_range_constraint_inverses, + lookup_xor_inverses) // Column 11 RefVector get_wires() { - return { permutation_set_column_1, permutation_set_column_2, permutation_set_column_3, - permutation_set_column_4, self_permutation_column, lookup_range_constraint_read_count, - range_constrained_column }; + return { permutation_set_column_1, + permutation_set_column_2, + permutation_set_column_3, + permutation_set_column_4, + self_permutation_column, + range_constrained_column, + lookup_xor_argument_1, + lookup_xor_argument_2, + lookup_xor_result, + lookup_xor_accumulated_argument_1, + lookup_xor_accumulated_argument_2, + lookup_xor_accumulated_result }; }; RefVector get_unshifted() { @@ -180,7 +231,10 @@ class ToyAVM { enable_first_set_permutation, // column 3 enable_second_set_permutation, // column 4 lookup_is_range_constrained, // column 5 - lookup_is_table_entry, // column 6 + lookup_is_range_table_entry, // column 6 + lookup_is_xor_operation, + lookup_is_xor_table_entry, + lookup_xor_shift, lookup_range_table_entries, permutation_set_column_1, // Column 0 permutation_set_column_2, // Column 1 @@ -189,9 +243,20 @@ class ToyAVM { self_permutation_column, // Column 4 lookup_range_constraint_read_count, range_constrained_column, + lookup_xor_read_count, + lookup_xor_argument_1, + lookup_xor_argument_2, + lookup_xor_result, + lookup_xor_accumulated_argument_1, + lookup_xor_accumulated_argument_2, + lookup_xor_accumulated_result, + lookup_xor_table_1, + lookup_xor_table_2, + lookup_xor_table_3, tuple_permutation_inverses, // Column 5 single_permutation_inverses, - lookup_range_constraint_inverses + lookup_range_constraint_inverses, + lookup_xor_inverses }; }; @@ -304,6 +369,7 @@ class ToyAVM { CommitmentLabels() : AllEntities() { + // TODO: fill out labels Base::permutation_set_column_1 = "PERMUTATION_SET_COLUMN_1"; Base::permutation_set_column_2 = "PERMUTATION_SET_COLUMN_2"; Base::permutation_set_column_3 = "PERMUTATION_SET_COLUMN_3"; @@ -325,6 +391,7 @@ class ToyAVM { public: VerifierCommitments(const std::shared_ptr& verification_key) { + // TODO: fill out commitments lagrange_first = verification_key->lagrange_first; enable_tuple_set_permutation = verification_key->enable_tuple_set_permutation; enable_single_column_permutation = verification_key->enable_single_column_permutation; diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp index 9c4d2db765b5..45bfb7b0badf 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.hpp @@ -87,15 +87,47 @@ template class ToyAVMCircuitBuilder { // Make range constrained polys.lookup_is_range_constrained[i] = 1; uint256_t constrained_value = wires[5][i]; - // If the value is correct, update the appropriate counter + // if the value is correct, update the appropriate counter if (constrained_value < 256) { polys.lookup_range_constraint_read_count[static_cast(constrained_value.data[0])] = polys.lookup_range_constraint_read_count[static_cast(constrained_value.data[0])] + 1; } + + // Copy xor values + polys.lookup_xor_argument_1[i] = wires[6][i]; + polys.lookup_xor_argument_2[i] = wires[7][i]; + polys.lookup_xor_result[i] = wires[8][i]; + polys.lookup_xor_accumulated_argument_1[i] = wires[9][i]; + polys.lookup_xor_accumulated_argument_2[i] = wires[10][i]; + polys.lookup_xor_accumulated_result[i] = wires[11][i]; + // Enable xor + polys.lookup_is_xor_operation[i] = 1; + + // Calculate index of this xor table entry + uint256_t xor_index = wires[6][i] * 16 + wires[7][i]; + // if the value is correct, update the appropriate counter + if (xor_index < 256) { + polys.lookup_xor_read_count[static_cast(xor_index.data[0])] = + polys.lookup_xor_read_count[static_cast(xor_index.data[0])] + 1; + } + xor_index = (uint256_t(wires[9][i]) & 0xf) * 16 + (uint256_t(wires[10][i]) & 0xf); + // if the value is correct, update the appropriate counter + if (xor_index < 256) { + polys.lookup_xor_read_count[static_cast(xor_index.data[0])] = + polys.lookup_xor_read_count[static_cast(xor_index.data[0])] + 1; + } } for (size_t i = 0; i < 256; i++) { - polys.lookup_is_table_entry[i] = FF(1); + // Fill range table + polys.lookup_is_range_table_entry[i] = FF(1); polys.lookup_range_table_entries[i] = FF(i); + + // Fill xor table + polys.lookup_is_xor_table_entry[i] = FF(1); + polys.lookup_xor_table_1[i] = FF(i >> 4); + polys.lookup_xor_table_2[i] = FF(i % 16); + polys.lookup_xor_table_3[i] = FF((i >> 4) ^ (i % 16)); + polys.lookup_xor_shift[i] = FF(16); } return polys; } @@ -195,6 +227,32 @@ template class ToyAVMCircuitBuilder { return false; } } + + // Check the xor relation + proof_system::honk::logderivative_library::compute_logderivative_inverse< + Flavor, + honk::sumcheck::GenericLookupRelation>( + polynomials, params, num_rows); + + using XorLookupRelation = + honk::sumcheck::GenericLookupRelation; + typename honk::sumcheck::GenericLookupRelation::SumcheckArrayOfValuesOverSubrelations + xor_constraint_result; + for (auto& r : xor_constraint_result) { + r = 0; + } + for (size_t i = 0; i < num_rows; ++i) { + + XorLookupRelation::accumulate(xor_constraint_result, polynomials.get_row(i), params, 1); + } + for (auto r : xor_constraint_result) { + if (r != 0) { + info("Xor Constraint failed."); + return false; + } + } + return true; } diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp index c55e503d9c64..8231a5c2c901 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/toy_avm/toy_avm_circuit_builder.test.cpp @@ -35,15 +35,28 @@ TEST(ToyAVMCircuitBuilder, BaseCase) column_2.emplace_back(FF::random_element()); } + std::vector> xor_arguments; + + // Get xor arguments + for (size_t i = 0; i < circuit_size; i++) { + xor_arguments.emplace_back(engine.get_random_uint8(), engine.get_random_uint8()); + } for (size_t i = 0; i < circuit_size; i++) { // We put the same tuple of values in the first 2 wires and in the next 2 to at different rows // We also put the same value in the self_permutation column in 2 consecutive rows - circuit_builder.add_row({ column_0[i], - column_1[i], - column_0[15 - i], - column_1[15 - i], - column_2[i / 2], - engine.get_random_uint8() }); + uint8_t xor_result = std::get<0>(xor_arguments[i]) ^ std::get<1>(xor_arguments[i]); + circuit_builder.add_row({ column_0[i], // Tuple 1 element 1 + column_1[i], // Tuple 1 element 2 + column_0[15 - i], // Tuple 2 element 1 + column_1[15 - i], // Tuple 2 element 2 + column_2[i / 2], // Self-permutation column + engine.get_random_uint8(), // Range constrained column + std::get<0>(xor_arguments[i]) >> 4, // Xor columns + std::get<1>(xor_arguments[i]) >> 4, + xor_result >> 4, + std::get<0>(xor_arguments[i]), + std::get<1>(xor_arguments[i]), + xor_result }); } // Test that permutations with correct values work @@ -68,8 +81,51 @@ TEST(ToyAVMCircuitBuilder, BaseCase) EXPECT_EQ(result, true); // Break single-column permutation + tmp = circuit_builder.wires[4][0]; circuit_builder.wires[4][0] = FF::random_element(); result = circuit_builder.check_circuit(); EXPECT_EQ(result, false); + + // Restore value + circuit_builder.wires[4][0] = tmp; + // Check circuit passes + result = circuit_builder.check_circuit(); + EXPECT_EQ(result, true); + + // Break range constraint + + circuit_builder.wires[5][0] = 257; + result = circuit_builder.check_circuit(); + EXPECT_EQ(result, false); + + // Restore range constraint + + circuit_builder.wires[5][0] = 255; + result = circuit_builder.check_circuit(); + EXPECT_EQ(result, true); + + // Break xor constraint + + circuit_builder.wires[6][0] = 0; + circuit_builder.wires[7][0] = 0; + circuit_builder.wires[8][0] = 1; + result = circuit_builder.check_circuit(); + EXPECT_EQ(result, false); + + // Break scaled xor constraint + + circuit_builder.wires[6][0] = 0; + circuit_builder.wires[7][0] = 0; + circuit_builder.wires[8][0] = 0; + circuit_builder.wires[9][0] = 1; + circuit_builder.wires[10][0] = 1; + circuit_builder.wires[11][0] = 1; + result = circuit_builder.check_circuit(); + EXPECT_EQ(result, false); + + // Restore xor constraint + circuit_builder.wires[11][0] = 0; + result = circuit_builder.check_circuit(); + EXPECT_EQ(result, true); } } // namespace toy_avm_circuit_builder_tests \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp index 62ba32401177..d2997278a4e3 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -49,25 +49,117 @@ template class GenericLookupRelationImpl { // For example, it would be 1 for a range constraint lookup, or 3 for XOR lookup static constexpr size_t LOOKUP_TUPLE_SIZE = Settings::LOOKUP_TUPLE_SIZE; - // Compute the length of the inverse polynomial correctness sub-relation MAX(product of terms * inverse, inverse - // exists polynomial) + 1; - static constexpr size_t FIRST_SUBRELATION_LENGTH = - std::max((READ_TERMS + WRITE_TERMS + 1), Settings::INVERSE_EXISTS_POLYNOMIAL_DEGREE) + 1; + /** + * @brief Compute the maximum degree of read terms + * + *@details We need this to evaluate the length of the subrelations correctly + * @return constexpr size_t + */ + static constexpr size_t compute_maximum_read_term_degree() + { + size_t maximum_degree = 0; + for (size_t i = 0; i < READ_TERMS; i++) { + size_t current_degree = 0; + if (Settings::READ_TERM_TYPES[i] == READ_BASIC_TUPLE) { + current_degree = 1; + } else if (Settings::READ_TERM_TYPES[i] == READ_SCALED_TUPLE) { + current_degree = 2; + } else { + current_degree = Settings::READ_TERM_DEGREE; + } + maximum_degree = std::max(current_degree, maximum_degree); + } + return maximum_degree; + } + + /** + * @brief Compute the maximum degree of write terms + * + *@details We need this to evaluate the length of the subrelations correctly + * @return constexpr size_t + */ + static constexpr size_t compute_maximum_write_term_degree() + { + size_t maximum_degree = 0; + for (size_t i = 0; i < WRITE_TERMS; i++) { + size_t current_degree = 0; + if (Settings::WRITE_TERM_TYPES[i] == WRITE_BASIC_TUPLE) { + current_degree = 1; + } else { + current_degree = Settings::WRITE_TERM_DEGREE; + } + maximum_degree = std::max(current_degree, maximum_degree); + } + return maximum_degree; + } + + /** + * @brief Compute the degree of of the product of read terms + * + * @details The degree of the inverse polynomial check subrelation is dependent on this value + * + * @return constexpr size_t + */ + static constexpr size_t compute_read_term_product_degree() + { + size_t accumulated_degree = 0; + for (size_t i = 0; i < READ_TERMS; i++) { + size_t current_degree = 0; + if (Settings::READ_TERM_TYPES[i] == READ_BASIC_TUPLE) { + current_degree = 1; + } else if (Settings::READ_TERM_TYPES[i] == READ_SCALED_TUPLE) { + current_degree = 2; + } else { + current_degree = Settings::READ_TERM_DEGREE; + } + accumulated_degree += current_degree; + } + return accumulated_degree; + } + + /** + * @brief Compute the degree of of the product of write terms + * + * @details The degree of the inverse polynomial check subrelation is dependent on this value + * + * @return constexpr size_t + */ + static constexpr size_t compute_write_term_product_degree() + { + size_t accumulated_degree = 0; + for (size_t i = 0; i < WRITE_TERMS; i++) { + size_t current_degree = 0; + if (Settings::WRITE_TERM_TYPES[i] == WRITE_BASIC_TUPLE) { + current_degree = 1; + } else { + current_degree = Settings::WRITE_TERM_DEGREE; + } + accumulated_degree += current_degree; + } + return accumulated_degree; + } // Read term degree is dependent on what type of read term we use - static constexpr size_t READ_TERM_DEGREE = Settings::READ_TERM_TYPE == READ_BASIC_TUPLE ? 1 - : Settings::READ_TERM_TYPE == READ_SCALED_TUPLE - ? 2 - : Settings::READ_TERM_DEGREE; + static constexpr size_t READ_TERM_DEGREE = compute_maximum_read_term_degree(); static_assert(READ_TERM_DEGREE != 0); // Write term degree is dependent on what type of write term we use - static constexpr size_t WRITE_TERM_DEGREE = - Settings::WRITE_TERM_TYPE == WRITE_BASIC_TUPLE ? 1 : Settings::WRITE_TERM_DEGREE; - // Compute the length of the log-derived term subrelation - static constexpr size_t SECOND_SUBRELATION_LENGTH = std::max(READ_TERM_DEGREE + 1, WRITE_TERM_DEGREE + 2) + 1; + static constexpr size_t WRITE_TERM_DEGREE = compute_maximum_write_term_degree(); + + static_assert(WRITE_TERM_DEGREE != 0); + + // Compute the length of the inverse polynomial correctness sub-relation MAX(product of terms * inverse, inverse + // exists polynomial) + 1; + static constexpr size_t FIRST_SUBRELATION_LENGTH = + std::max((compute_read_term_product_degree() + compute_write_term_product_degree() + 1), + Settings::INVERSE_EXISTS_POLYNOMIAL_DEGREE) + + 1; + + // Compute the length of the log-derived term subrelation MAX(read term * enable read, write term * write count * + // enable write) + static constexpr size_t SECOND_SUBRELATION_LENGTH = std::max(READ_TERM_DEGREE + 1, WRITE_TERM_DEGREE + 2); // 1 + polynomial degree of this relation - static constexpr size_t LENGTH = READ_TERMS + WRITE_TERMS + 3; // 5 + static constexpr size_t LENGTH = std::max(FIRST_SUBRELATION_LENGTH, SECOND_SUBRELATION_LENGTH); // The structure of polynomial tuple returned from Settings' functions get_const_entities and get_nonconst_entities // is the following: @@ -78,16 +170,16 @@ template class GenericLookupRelationImpl { // or not) // 4) WRITE_TERMS number of polynomials enabling a particular write term in this row (should we add it to // the lookup table or not) - // 5) Depending on the type of read terms (BASIC_TUPLE, SCALED_TUPLE or ARBITRARY): - // 1. In case of basic tuple READ_TERMS polynomials the combination of whose values in a row is supposed to + // 5) For each read term depending on its type (READ_BASIC_TUPLE, READ_SCALED_TUPLE or READ_ARBITRARY): + // 1. In case of basic tuple LOOKUP_TUPLE_SIZE polynomials the combination of whose values in a row is supposed to // represent the looked up entry - // 2. In case of scaled tuple there are READ_TERMS previous accumulator polynomials, READ_TERMS - // scaling polynomials and READ_TERMS current accumulator polynomials. The tuple is comprised of values + // 2. In case of scaled tuple there are LOOKUP_TUPLE_SIZE previous accumulator polynomials, LOOKUP_TUPLE_SIZE + // scaling polynomials and LOOKUP_TUPLE_SIZE current accumulator polynomials. The tuple is comprised of values // (current_accumulator-scale*previous_accumulator) - // 3. In the arbitrary case the are no additional read_term + // 3. In the arbitrary case the are no additional // polynomials, because the logic is completely decided in the settings - // 6) Depending on the type of read terms (BASIC_TUPLE or ARBITRARY): - // 1. In case of basic tuple WRITE_TERNS polynomials the combination of whose values in a row is supposed to + // 6) For each write term depending on its type (READ_BASIC_TUPLE or READ_ARBITRARY): + // 1. In case of basic tuple LOOKUP_TUPLE_SIZE polynomials the combination of whose values in a row is supposed to // represent the entry written into the lookup table // 2. In the arbitrary case the are no additional write term polynomials, // because the logic is completely decided in the settings @@ -104,7 +196,6 @@ template class GenericLookupRelationImpl { LENGTH, // inverse polynomial correctness sub-relation LENGTH // log-derived terms subrelation }; - /** * @brief We apply the power polynomial only to the first subrelation * @@ -207,6 +298,74 @@ template class GenericLookupRelationImpl { Settings::get_const_entities(in)))); } + /** + * @brief Compute where the polynomials defining a particular read term are located + * + *@details We pass polynomials involved in read an write terms from settings as a tuple of references. However, + *depending on the type of read term different number of polynomials can be used to compute it. So we need to + *compute the offset in the tuple iteratively + * + * @param read_index Index of the read term + * @return constexpr size_t + */ + static constexpr size_t compute_read_term_polynomial_offset(size_t read_index) + { + // If it's the starting index, then there is nothing to compute, just get the starting index + if (read_index == 0) { + return LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX; + } + + // If the previous term used basic tuple lookup, add lookup tuple size (it was using just a linear combination + // of polynomials) + if (Settings::READ_TERM_TYPES[read_index - 1] == READ_BASIC_TUPLE) { + return compute_read_term_polynomial_offset(read_index - 1) + LOOKUP_TUPLE_SIZE; + } + + // If the previous term used scaled tuple lookup, add lookup tuple size x 3 (it was using just a linear + // combination of differences (current - previous⋅scale)) + + if (Settings::READ_TERM_TYPES[read_index - 1] == READ_SCALED_TUPLE) { + return compute_read_term_polynomial_offset(read_index - 1) + 3 * LOOKUP_TUPLE_SIZE; + } + // In case of arbitrary read term, no polynomials from the tuple are being used + if (Settings::READ_TERM_TYPES[read_index - 1] == READ_ARBITRARY) { + return compute_read_term_polynomial_offset(read_index - 1); + } + throw std::logic_error("Should never reach this part"); + return SIZE_MAX; + } + + /** + * @brief Compute where the polynomials defining a particular write term are located + * + *@details We pass polynomials involved in read an write terms from settings as a tuple of references. However, + *depending on the type of term different number of polynomials can be used to compute it. So we need to + *compute the offset in the tuple iteratively + * + * @param write_index Index of the write term + * @return constexpr size_t + */ + static constexpr size_t compute_write_term_polynomial_offset(size_t write_index) + { + // If it's the starting index, then we need to find out how many polynomials were taken by read terms + if (write_index == 0) { + return compute_read_term_polynomial_offset(READ_TERMS); + } + + // If the previous term used basic tuple lookup, add lookup tuple size (it was using just a linear combination + // of polynomials) + if (Settings::WRITE_TERM_TYPES[write_index - 1] == WRITE_BASIC_TUPLE) { + return compute_write_term_polynomial_offset(write_index - 1) + LOOKUP_TUPLE_SIZE; + } + + // In case of arbitrary write term, no polynomials from the tuple are being used + if (Settings::WRITE_TERM_TYPES[write_index - 1] == WRITE_ARBITRARY) { + return compute_write_term_polynomial_offset(write_index - 1); + } + throw std::logic_error("Should never reach this part"); + return SIZE_MAX; + } + /** * @brief Compute the value of a single item in the set * @@ -223,36 +382,30 @@ template class GenericLookupRelationImpl { using View = typename Accumulator::View; static_assert(read_index < READ_TERMS); - static_assert(Settings::READ_TERM_TYPE < 3); - static_assert(Settings::READ_TERM_TYPE >= 0); - - if constexpr (Settings::READ_TERM_TYPE == READ_BASIC_TUPLE) { + constexpr size_t start_polynomial_index = compute_read_term_polynomial_offset(read_index); + if constexpr (Settings::READ_TERM_TYPES[read_index] == READ_BASIC_TUPLE) { // Retrieve all polynomials used const auto all_polynomials = Settings::get_const_entities(in); auto result = Accumulator(0); // Iterate over tuple and sum as a polynomial over beta - barretenberg::constexpr_for( + barretenberg::constexpr_for( [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); const auto& gamma = params.gamma; return result + gamma; - } else if constexpr (Settings::READ_TERM_TYPE == READ_SCALED_TUPLE) { + } else if constexpr (Settings::READ_TERM_TYPES[read_index] == READ_SCALED_TUPLE) { // Retrieve all polynomials used const auto all_polynomials = Settings::get_const_entities(in); auto result = Accumulator(0); // Iterate over tuple and sum as a polynomial over beta - barretenberg::constexpr_for< - LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + read_index * 3 * LOOKUP_TUPLE_SIZE, - LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + (read_index * 3 + 1) * LOOKUP_TUPLE_SIZE, - 1>([&]() { - result = (result * params.beta) + View(std::get(all_polynomials)) - - View(std::get(all_polynomials)) * View(std::get(all_polynomials)); - }); + barretenberg::constexpr_for( + [&]() { + result = + (result * params.beta) + View(std::get(all_polynomials)) - + View(std::get(all_polynomials)) * View(std::get(all_polynomials)); + }); const auto& gamma = params.gamma; return result + gamma; } else { @@ -276,27 +429,18 @@ template class GenericLookupRelationImpl { { static_assert(write_index < WRITE_TERMS); - static_assert(Settings::WRITE_TERM_TYPE < 2); - static_assert(Settings::WRITE_TERM_TYPE >= 0); - static_assert(Settings::READ_TERM_TYPE < 3); - static_assert(Settings::READ_TERM_TYPE >= 0); using View = typename Accumulator::View; - // Write term offset is dependet on which read term computation method is used - constexpr size_t WRITE_TERMS_OFFSET = LOOKUP_READ_PREDICATE_START_POLYNOMIAL_INDEX + - (Settings::READ_TERM_TYPE == READ_BASIC_TUPLE ? LOOKUP_TUPLE_SIZE - : Settings::READ_TERM_TYPE == READ_SCALED_TUPLE ? LOOKUP_TUPLE_SIZE * 3 - : 0); - if constexpr (Settings::WRITE_TERM_TYPE == WRITE_BASIC_TUPLE) { + constexpr size_t start_polynomial_index = compute_write_term_polynomial_offset(write_index); + + if constexpr (Settings::WRITE_TERM_TYPES[write_index] == WRITE_BASIC_TUPLE) { // Retrieve all polynomials used const auto all_polynomials = Settings::get_const_entities(in); auto result = Accumulator(0); // Iterate over tuple and sum as a polynomial over beta - barretenberg::constexpr_for( + barretenberg::constexpr_for( [&]() { result = (result * params.beta) + View(std::get(all_polynomials)); }); const auto& gamma = params.gamma; return result + gamma; diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index a5a2360ee09a..ecc2fea1811d 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -195,7 +195,7 @@ class ExampleSameWirePermutationSettings { /** * @brief This class contains an example of how to set LookupSettings classes used by the - * GenericLookupRelationImpl class to specify a concrete permutation + * GenericLookupRelationImpl class to specify a range constraint * * @details To create your own lookup: * 1) Create a copy of this class and rename it @@ -210,37 +210,27 @@ class ExampleSameWirePermutationSettings { class ExampleLookupBasedRangeConstraintSettings { public: /** - * @brief The type of the READ_TERM (lookup operation) that we are using - * - * @details 0 stands for basic tuple lookup, where we simply lookup a tuple of values from given entities - * 1 stands for scaled tuple lookup, which uses a tuple of (current_accumulator - previous_accumulator * shift) - * values - * 2 means arbitrary expression that requires the settings to have a specific method and set the READ_TERM_DEGREE to - * the degree of the expression + * @brief The number of read terms (how many lookups we perform) in each row * */ - static constexpr size_t READ_TERM_TYPE = 0; + static constexpr size_t READ_TERMS = 1; /** - * @brief The type of the WRITE_TERM (lookup table entry addition) that we are using - * - * @details 0 stands for basic tuple lookup, where we simply lookup a tuple of values from given entities - * 1 means an arbitrary expression, evaluated through a method defines in these settings. In this case - * WRITE_TERM_DEGREE has to be set to the degree of the expression + * @brief The number of write terms (how many additions to the lookup table we make) in each row * */ - static constexpr size_t WRITE_TERM_TYPE = 0; + static constexpr size_t WRITE_TERMS = 1; /** - * @brief The number of read terms (how many lookups we perform) in each row + * @brief The type of READ_TERM used for each read index * */ - static constexpr size_t READ_TERMS = 1; + static constexpr size_t READ_TERM_TYPES[READ_TERMS] = { 0 }; + /** - * @brief The number of write terms (how many additions to the lookup table we make) in each row + * @brief They type of WRITE_TERM used for each write index * */ - static constexpr size_t WRITE_TERMS = 1; - + static constexpr size_t WRITE_TERM_TYPES[WRITE_TERMS] = { 0 }; /** * @brief How many values represent a single lookup object. This value is used by the automatic read term * implementation in the relation in case the lookup is a basic or scaled tuple and in the write term if it's a @@ -279,7 +269,7 @@ class ExampleLookupBasedRangeConstraintSettings { */ template static inline bool inverse_polynomial_is_computed_at_row(const AllEntities& in) { - return (in.lookup_is_range_constrained == 1) || (in.lookup_is_table_entry == 1); + return (in.lookup_is_range_constrained == 1) || (in.lookup_is_range_table_entry == 1); } /** @@ -297,7 +287,7 @@ class ExampleLookupBasedRangeConstraintSettings { using View = Accumulator::View; const auto is_constrained = View(in.lookup_is_range_constrained); - const auto is_table_entry = View(in.lookup_is_table_entry); + const auto is_table_entry = View(in.lookup_is_range_table_entry); return (is_constrained + is_table_entry - is_constrained * is_table_entry); } @@ -325,7 +315,7 @@ class ExampleLookupBasedRangeConstraintSettings { in.lookup_range_constraint_inverses, /* The polynomial containing the inverse product*/ in.lookup_range_constraint_read_count, /* The polynomial containing number of reads of each table entry */ in.lookup_is_range_constrained, /* Enables lookup action in this row */ - in.lookup_is_table_entry, /* Enables adding an entry to the table */ + in.lookup_is_range_table_entry, /* Enables adding an entry to the table */ in.range_constrained_column, /* Column being looked up */ in.lookup_range_table_entries); /* Column containing table entries*/ } @@ -343,12 +333,194 @@ class ExampleLookupBasedRangeConstraintSettings { in.lookup_range_constraint_inverses, /* The polynomial containing the inverse product*/ in.lookup_range_constraint_read_count, /* The polynomial containing number of reads of each table entry */ in.lookup_is_range_constrained, /* Enables lookup action in this row */ - in.lookup_is_table_entry, /* Enables adding an entry to the table */ + in.lookup_is_range_table_entry, /* Enables adding an entry to the table */ in.range_constrained_column, /* Column being looked up */ in.lookup_range_table_entries); /* Column containing table entries*/ } }; +/** + * @brief This class contains an example of how to set LookupSettings classes used by the + * GenericLookupRelationImpl class to specify a scaled lookup + * + * @details To create your own lookup: + * 1) Create a copy of this class and rename it + * 2) Update all the values with the ones needed for your permutation + * 3) Update "DECLARE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS" and "DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS" to + * include the new settings + * 4) Add the relation with the chosen settings to Relations in the flavor (for example,"` + * using Relations = std::tuple>;)` + * + */ +class ExampleXorLookupConstraintSettings { + public: + /** + * @brief The number of read terms (how many lookups we perform) in each row + * + */ + static constexpr size_t READ_TERMS = 2; + /** + * @brief The number of write terms (how many additions to the lookup table we make) in each row + * + */ + static constexpr size_t WRITE_TERMS = 1; + + /** + * @brief The type of READ_TERM used for each read index (basic and scaled) + * + */ + static constexpr size_t READ_TERM_TYPES[READ_TERMS] = { 0, 1 }; + + /** + * @brief They type of WRITE_TERM used for each write index + * + */ + static constexpr size_t WRITE_TERM_TYPES[WRITE_TERMS] = { 0 }; + /** + * @brief How many values represent a single lookup object. This value is used by the automatic read term + * implementation in the relation in case the lookup is a basic or scaled tuple and in the write term if it's a + * basic tuple + * + */ + static constexpr size_t LOOKUP_TUPLE_SIZE = 3; + + /** + * @brief The polynomial degree of the relation telling us if the inverse polynomial value needs to be computed + * + */ + static constexpr size_t INVERSE_EXISTS_POLYNOMIAL_DEGREE = 2; + + /** + * @brief The degree of the read term if implemented arbitrarily. This value is not used by basic and scaled read + * terms, but will cause compilation error if not defined + * + */ + static constexpr size_t READ_TERM_DEGREE = 0; + + /** + * @brief The degree of the write term if implemented arbitrarily. This value is not used by the basic write + * term, but will cause compilation error if not defined + * + */ + + static constexpr size_t WRITE_TERM_DEGREE = 0; + + /** + * @brief If this method returns true on a row of values, then the inverse polynomial exists at this index. + * Otherwise the value needs to be set to zero. + * + * @details If this is true then the lookup takes place in this row + * + */ + template static inline bool inverse_polynomial_is_computed_at_row(const AllEntities& in) + { + return (in.lookup_is_xor_operation == 1) || (in.lookup_is_xor_table_entry == 1); + } + + /** + * @brief Subprocedure for computing the value deciding if the inverse polynomial value needs to be checked in this + * row + * + * @tparam Accumulator Type specified by the lookup relation + * @tparam AllEntities Values/Univariates of all entities row + * @param in Value/Univariate of all entities at row/edge + * @return Accumulator + */ + template + static Accumulator compute_inverse_exists(const AllEntities& in) + { + + using View = Accumulator::View; + const auto is_xor_operation = View(in.lookup_is_xor_operation); + const auto is_xor_table_entry = View(in.lookup_is_xor_table_entry); + return (is_xor_operation + is_xor_table_entry - is_xor_operation * is_xor_table_entry); + } + + /** + * @brief Get all the entities for the lookup when need to update them + * + * @details The generic structure of this tuple is described in ./generic_lookup_relation.hpp . The following is + description for the current case: + + The entities are returned as a tuple of references in the following order (this is for ): + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that specifies how many times the lookup table entry at this row has been looked up + * - READ_TERMS entities/polynomials that enable individual lookup operations + * - The entity/polynomial that enables adding an entry to the lookup table in this row + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the basic tuple being looked up as the first read term + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the previous accumulators in the second read term + (scaled tuple) + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the shifts in the second read term (scaled tuple) + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the current accumulators in the second read term + (scaled tuple) + * - LOOKUP_TUPLE_SIZE entities/polynomials representing basic tuples added to the table + * + * @return All the entities needed for the lookup + */ + template static inline auto get_const_entities(const AllEntities& in) + { + + return std::forward_as_tuple( + in.lookup_xor_inverses, /* The polynomial containing the inverse product*/ + in.lookup_xor_read_count, /* The polynomial containing number of reads of each table entry */ + in.lookup_is_xor_operation, /* Enables 1st lookup action in this row */ + in.lookup_is_xor_operation, /* Enables 2nd lookup action in this row */ + in.lookup_is_xor_table_entry, /* Enables adding an entry to the table */ + in.lookup_xor_argument_1, /* 1st element of the 1st read term (basic tuple) being looked up */ + in.lookup_xor_argument_2, /* 2nd element of the 1st read term (basic tuple) being looked up */ + in.lookup_xor_result, /* 3rd element of the 1st read term (basic tuple) being looked up */ + in.lookup_xor_argument_1, /* Previous accumulator of the 1st element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_argument_2, /* Previous accumulator of the 2nd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_result, /* Previous accumulator of the 3rd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_shift, /* Shift of the 1st element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_shift, /* Shift of the 2nd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_shift, /* Shift of the 3rd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_accumulated_argument_1, /* Current accumulator of the 1st element in the 2nd read term (scaled + tuple)*/ + in.lookup_xor_accumulated_argument_2, /* Current accumulator of the 2nd element in the 2nd read term (scaled + tuple)*/ + in.lookup_xor_accumulated_result, /* Current accumulator of the 3rd element in the 2nd read term (scaled + tuple)*/ + in.lookup_xor_table_1, /* 1st element of the write term (basic tuple)*/ + in.lookup_xor_table_2, /* 2nd element of the write term (basic tuple)*/ + in.lookup_xor_table_3); /* 3rd element of the write term (basic tuple)*/ + } + /** + * @brief Get all the entities for the lookup when only need to read them + * @details Same as in get_const_entities, but nonconst + * + * @return All the entities needed for the lookup + */ + template static inline auto get_nonconst_entities(AllEntities& in) + { + return std::forward_as_tuple( + in.lookup_xor_inverses, /* The polynomial containing the inverse product*/ + in.lookup_xor_read_count, /* The polynomial containing number of reads of each table entry */ + in.lookup_is_xor_operation, /* Enables 1st lookup action in this row */ + in.lookup_is_xor_operation, /* Enables 2nd lookup action in this row */ + in.lookup_is_xor_table_entry, /* Enables adding an entry to the table */ + in.lookup_xor_argument_1, /* 1st element of the 1st read term (basic tuple) being looked up */ + in.lookup_xor_argument_2, /* 2nd element of the 1st read term (basic tuple) being looked up */ + in.lookup_xor_result, /* 3rd element of the 1st read term (basic tuple) being looked up */ + in.lookup_xor_argument_1, /* Previous accumulator of the 1st element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_argument_2, /* Previous accumulator of the 2nd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_result, /* Previous accumulator of the 3rd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_shift, /* Shift of the 1st element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_shift, /* Shift of the 2nd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_shift, /* Shift of the 3rd element in the 2nd read term (scaled tuple)*/ + in.lookup_xor_accumulated_argument_1, /* Current accumulator of the 1st element in the 2nd read term (scaled + tuple)*/ + in.lookup_xor_accumulated_argument_2, /* Current accumulator of the 2nd element in the 2nd read term (scaled + tuple)*/ + in.lookup_xor_accumulated_result, /* Current accumulator of the 3rd element in the 2nd read term (scaled + tuple)*/ + in.lookup_xor_table_1, /* 1st element of the write term (basic tuple)*/ + in.lookup_xor_table_2, /* 2nd element of the write term (basic tuple)*/ + in.lookup_xor_table_3); /* 3rd element of the write term (basic tuple)*/ + } +}; + #define DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, Settings) \ template class RelationImplementation; \ template using RelationImplementation##Settings = RelationImplementation; \ @@ -368,9 +540,11 @@ class ExampleLookupBasedRangeConstraintSettings { DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleSameWirePermutationSettings); #define DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ - DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleLookupBasedRangeConstraintSettings); + DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleLookupBasedRangeConstraintSettings); \ + DEFINE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleXorLookupConstraintSettings); #define DECLARE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(RelationImplementation, flavor) \ - DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleLookupBasedRangeConstraintSettings); + DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleLookupBasedRangeConstraintSettings); \ + DECLARE_IMPLEMENTATIONS_FOR_SETTINGS(RelationImplementation, flavor, ExampleXorLookupConstraintSettings); } // namespace proof_system::honk::sumcheck \ No newline at end of file From 048f932056afd49b87d40e7dfa18385451e80a9c Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Tue, 2 Jan 2024 13:27:46 +0000 Subject: [PATCH 08/11] Cleanup --- .../cpp/src/barretenberg/flavor/toy_avm.hpp | 166 +++++++++--------- 1 file changed, 80 insertions(+), 86 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp index f370767fba68..a10ebaaf1a4c 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp @@ -90,9 +90,9 @@ class ToyAVM { lookup_is_xor_operation, // column 8 lookup_is_xor_table_entry, // column 9 lookup_xor_shift, // column 10 - lookup_xor_table_1, - lookup_xor_table_2, - lookup_xor_table_3) + lookup_xor_table_1, // column 11 + lookup_xor_table_2, // column 12 + lookup_xor_table_3) // column 13 RefVector get_selectors() { @@ -124,25 +124,24 @@ class ToyAVM { template class WitnessEntities { public: DEFINE_FLAVOR_MEMBERS(DataType, - permutation_set_column_1, // Column 0 - permutation_set_column_2, // Column 1 - permutation_set_column_3, // Column 2 - permutation_set_column_4, // Column 3 - self_permutation_column, // Column 4 - lookup_range_constraint_read_count, - range_constrained_column, - lookup_xor_read_count, - lookup_xor_argument_1, - lookup_xor_argument_2, - lookup_xor_result, - lookup_xor_accumulated_argument_1, - lookup_xor_accumulated_argument_2, - lookup_xor_accumulated_result, - - tuple_permutation_inverses, - single_permutation_inverses, - lookup_range_constraint_inverses, - lookup_xor_inverses) + permutation_set_column_1, // Column 0 + permutation_set_column_2, // Column 1 + permutation_set_column_3, // Column 2 + permutation_set_column_4, // Column 3 + self_permutation_column, // Column 4 + lookup_range_constraint_read_count, // column 5 + range_constrained_column, // column 6 + lookup_xor_read_count, // column 7 + lookup_xor_argument_1, // column 8 + lookup_xor_argument_2, // column 9 + lookup_xor_result, // column 10 + lookup_xor_accumulated_argument_1, // column 11 + lookup_xor_accumulated_argument_2, // column 12 + lookup_xor_accumulated_result, // column 13 + tuple_permutation_inverses, // column 14 + single_permutation_inverses, // column 15 + lookup_range_constraint_inverses, // column 16 + lookup_xor_inverses) // column 17 RefVector get_wires() { @@ -174,39 +173,38 @@ class ToyAVM { template class AllEntities { public: DEFINE_FLAVOR_MEMBERS(DataType, - lagrange_first, // column 0 - enable_tuple_set_permutation, // column 1 - enable_single_column_permutation, // column 2 - enable_first_set_permutation, // column 3 - enable_second_set_permutation, // column 4 - lookup_is_range_constrained, // column 5 - lookup_is_range_table_entry, // column 6 - lookup_is_xor_operation, - lookup_is_xor_table_entry, - lookup_xor_shift, - lookup_xor_table_1, - lookup_xor_table_2, - lookup_xor_table_3, - lookup_range_table_entries, - permutation_set_column_1, // Column 0 - permutation_set_column_2, // Column 1 - permutation_set_column_3, // Column 2 - permutation_set_column_4, // Column 3 - self_permutation_column, // Column 4 - lookup_range_constraint_read_count, - range_constrained_column, - lookup_xor_read_count, - lookup_xor_argument_1, - lookup_xor_argument_2, - lookup_xor_result, - lookup_xor_accumulated_argument_1, - lookup_xor_accumulated_argument_2, - lookup_xor_accumulated_result, - - tuple_permutation_inverses, // Column 5 - single_permutation_inverses, - lookup_range_constraint_inverses, - lookup_xor_inverses) // Column 11 + lagrange_first, // column 0 + enable_tuple_set_permutation, // column 1 + enable_single_column_permutation, // column 2 + enable_first_set_permutation, // column 3 + enable_second_set_permutation, // column 4 + lookup_is_range_constrained, // column 5 + lookup_is_range_table_entry, // column 6 + lookup_is_xor_operation, // column 7 + lookup_is_xor_table_entry, // column 8 + lookup_xor_shift, // column 9 + lookup_xor_table_1, // column 10 + lookup_xor_table_2, // column 11 + lookup_xor_table_3, // column 12 + lookup_range_table_entries, // column 13 + permutation_set_column_1, // column 14 + permutation_set_column_2, // column 15 + permutation_set_column_3, // column 16 + permutation_set_column_4, // column 17 + self_permutation_column, // column 18 + lookup_range_constraint_read_count, // column 19 + range_constrained_column, // column 20 + lookup_xor_read_count, // column 21 + lookup_xor_argument_1, // column 22 + lookup_xor_argument_2, // column 23 + lookup_xor_result, // column 24 + lookup_xor_accumulated_argument_1, // column 25 + lookup_xor_accumulated_argument_2, // column 26 + lookup_xor_accumulated_result, // column 27 + tuple_permutation_inverses, // column 28 + single_permutation_inverses, // column 29 + lookup_range_constraint_inverses, // column 30 + lookup_xor_inverses) // column 31 RefVector get_wires() { @@ -225,22 +223,22 @@ class ToyAVM { }; RefVector get_unshifted() { - return { lagrange_first, // column 0 - enable_tuple_set_permutation, // column 1 - enable_single_column_permutation, // column 2 - enable_first_set_permutation, // column 3 - enable_second_set_permutation, // column 4 - lookup_is_range_constrained, // column 5 - lookup_is_range_table_entry, // column 6 + return { lagrange_first, + enable_tuple_set_permutation, + enable_single_column_permutation, + enable_first_set_permutation, + enable_second_set_permutation, + lookup_is_range_constrained, + lookup_is_range_table_entry, lookup_is_xor_operation, lookup_is_xor_table_entry, lookup_xor_shift, lookup_range_table_entries, - permutation_set_column_1, // Column 0 - permutation_set_column_2, // Column 1 - permutation_set_column_3, // Column 2 - permutation_set_column_4, // Column 3 - self_permutation_column, // Column 4 + permutation_set_column_1, + permutation_set_column_2, + permutation_set_column_3, + permutation_set_column_4, + self_permutation_column, lookup_range_constraint_read_count, range_constrained_column, lookup_xor_read_count, @@ -253,7 +251,7 @@ class ToyAVM { lookup_xor_table_1, lookup_xor_table_2, lookup_xor_table_3, - tuple_permutation_inverses, // Column 5 + tuple_permutation_inverses, single_permutation_inverses, lookup_range_constraint_inverses, lookup_xor_inverses @@ -367,23 +365,10 @@ class ToyAVM { public: CommitmentLabels() - : AllEntities() - { - // TODO: fill out labels - Base::permutation_set_column_1 = "PERMUTATION_SET_COLUMN_1"; - Base::permutation_set_column_2 = "PERMUTATION_SET_COLUMN_2"; - Base::permutation_set_column_3 = "PERMUTATION_SET_COLUMN_3"; - Base::permutation_set_column_4 = "PERMUTATION_SET_COLUMN_4"; - Base::self_permutation_column = "SELF_PERMUTATION_COLUMN"; - Base::tuple_permutation_inverses = "TUPLE_PERMUTATION_INVERSES"; - Base::single_permutation_inverses = "SINGLE_PERMUTATION_INVERSES"; - // The ones beginning with "__" are only used for debugging - Base::lagrange_first = "__LAGRANGE_FIRST"; - Base::enable_tuple_set_permutation = "__ENABLE_SET_PERMUTATION"; - Base::enable_single_column_permutation = "__ENABLE_SINGLE_COLUMN_PERMUTATION"; - Base::enable_first_set_permutation = "__ENABLE_FIRST_SET_PERMUTATION"; - Base::enable_second_set_permutation = "__ENABLE_SECOND_SET_PERMUTATION"; - }; + : AllEntities(){ + // TODO: fill out labels when the proving system is involved + // Base::permutation_set_column_1 = "PERMUTATION_SET_COLUMN_1"; + }; }; class VerifierCommitments : public AllEntities { @@ -391,12 +376,21 @@ class ToyAVM { public: VerifierCommitments(const std::shared_ptr& verification_key) { - // TODO: fill out commitments + lagrange_first = verification_key->lagrange_first; enable_tuple_set_permutation = verification_key->enable_tuple_set_permutation; enable_single_column_permutation = verification_key->enable_single_column_permutation; enable_first_set_permutation = verification_key->enable_first_set_permutation; enable_second_set_permutation = verification_key->enable_second_set_permutation; + lookup_is_range_constrained = verification_key->lookup_is_range_constrained; + lookup_is_range_table_entry = verification_key->lookup_is_range_table_entry; + lookup_range_table_entries = verification_key->lookup_range_table_entries; + lookup_is_xor_operation = verification_key->lookup_is_xor_operation; + lookup_is_xor_table_entry = verification_key->lookup_is_xor_table_entry; + lookup_xor_shift = verification_key->lookup_xor_shift; + lookup_xor_table_1 = verification_key->lookup_xor_table_1; + lookup_xor_table_2 = verification_key->lookup_xor_table_2; + lookup_xor_table_3 = verification_key->lookup_xor_table_3; } }; From e2ec451285213c623df868a545f3813a1232ea64 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Tue, 2 Jan 2024 13:33:43 +0000 Subject: [PATCH 09/11] Minifix --- .../src/barretenberg/relations/toy_avm/relation_definer.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp index ecc2fea1811d..c01ecccda502 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/relation_definer.hpp @@ -285,7 +285,7 @@ class ExampleLookupBasedRangeConstraintSettings { static Accumulator compute_inverse_exists(const AllEntities& in) { - using View = Accumulator::View; + using View = typename Accumulator::View; const auto is_constrained = View(in.lookup_is_range_constrained); const auto is_table_entry = View(in.lookup_is_range_table_entry); return (is_constrained + is_table_entry - is_constrained * is_table_entry); @@ -431,7 +431,7 @@ class ExampleXorLookupConstraintSettings { static Accumulator compute_inverse_exists(const AllEntities& in) { - using View = Accumulator::View; + using View = typename Accumulator::View; const auto is_xor_operation = View(in.lookup_is_xor_operation); const auto is_xor_table_entry = View(in.lookup_is_xor_table_entry); return (is_xor_operation + is_xor_table_entry - is_xor_operation * is_xor_table_entry); From 2bab277bb50fb90a73893747c12e9443e20691e3 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Tue, 2 Jan 2024 13:44:10 +0000 Subject: [PATCH 10/11] Fix --- .../barretenberg/relations/toy_avm/generic_lookup_relation.hpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp index d2997278a4e3..bc510620fba3 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -331,7 +331,6 @@ template class GenericLookupRelationImpl { if (Settings::READ_TERM_TYPES[read_index - 1] == READ_ARBITRARY) { return compute_read_term_polynomial_offset(read_index - 1); } - throw std::logic_error("Should never reach this part"); return SIZE_MAX; } @@ -362,7 +361,6 @@ template class GenericLookupRelationImpl { if (Settings::WRITE_TERM_TYPES[write_index - 1] == WRITE_ARBITRARY) { return compute_write_term_polynomial_offset(write_index - 1); } - throw std::logic_error("Should never reach this part"); return SIZE_MAX; } From 3793b63a1a3a0e32e834fe5cc7d636479e1a9085 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Thu, 4 Jan 2024 14:50:22 +0000 Subject: [PATCH 11/11] Fixed second subrelation length --- .../toy_avm/generic_lookup_relation.hpp | 32 ++++++++++++++++--- 1 file changed, 27 insertions(+), 5 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp index bc510620fba3..96a4c4b334e8 100644 --- a/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/toy_avm/generic_lookup_relation.hpp @@ -11,8 +11,6 @@ * + READ - the action of looking up the value in the table * + WRITE - the action of adding the value to the lookup table * - * TODO(@Rumata888): Talk to Zac why "lookup_read_count" refers to the count of the looked up element in the multiset. - * (The value is applied to the write predicate, so it is confusing). */ #pragma once #include @@ -92,6 +90,27 @@ template class GenericLookupRelationImpl { } return maximum_degree; } + /** + * @brief Compute the minimum degree of write terms + * + *@details We need this to evaluate the length of the subrelations correctly (specifically the logderivative + *relation) + * @return constexpr size_t + */ + static constexpr size_t compute_minimum_write_term_degree() + { + size_t minimum_degree = SIZE_MAX; + for (size_t i = 0; i < WRITE_TERMS; i++) { + size_t current_degree = 0; + if (Settings::WRITE_TERM_TYPES[i] == WRITE_BASIC_TUPLE) { + current_degree = 1; + } else { + current_degree = Settings::WRITE_TERM_DEGREE; + } + minimum_degree = std::min(current_degree, minimum_degree); + } + return minimum_degree; + } /** * @brief Compute the degree of of the product of read terms @@ -155,9 +174,12 @@ template class GenericLookupRelationImpl { Settings::INVERSE_EXISTS_POLYNOMIAL_DEGREE) + 1; - // Compute the length of the log-derived term subrelation MAX(read term * enable read, write term * write count * - // enable write) - static constexpr size_t SECOND_SUBRELATION_LENGTH = std::max(READ_TERM_DEGREE + 1, WRITE_TERM_DEGREE + 2); + // Compute the length of the seconds subrelation (inverse_polynomial⋅ ∏read_terms ⋅ ∏(write_terms other than + // current)⋅ enable_write⋅ lookup_read_count). + + static constexpr size_t SECOND_SUBRELATION_LENGTH = compute_read_term_product_degree() + + compute_write_term_product_degree() - + compute_minimum_write_term_degree() + 2; // 1 + polynomial degree of this relation static constexpr size_t LENGTH = std::max(FIRST_SUBRELATION_LENGTH, SECOND_SUBRELATION_LENGTH);