|
Barretenberg
The ZK-SNARK library at the core of Aztec
|
Log-derivative lookup argument relation for establishing lookup reads from tables with 3 or fewer columns. More...
#include <logderiv_lookup_relation.hpp>
Public Types | |
| using | FF = FF_ |
Static Public Member Functions | |
| template<typename AllEntities > | |
| static bool | skip (const AllEntities &in) |
| template<typename AllValues > | |
| static bool | operation_exists_at_row (const AllValues &row) |
| Does the provided row contain data relevant to table lookups; Used to determine whether the polynomial of inverses must be computed at a given row. | |
| template<typename AllEntities > | |
| static auto & | get_inverse_polynomial (AllEntities &in) |
| template<typename Accumulator , typename AllEntities > | |
| static Accumulator | compute_inverse_exists (const AllEntities &in) |
| Compute the Accumulator whose values indicate whether the inverse is computed or not. | |
| template<typename Accumulator , typename AllEntities , typename Parameters > | |
| static Accumulator | compute_write_term (const AllEntities &in, const Parameters ¶ms) |
| template<typename Accumulator , typename AllEntities , typename Parameters > | |
| static Accumulator | compute_read_term (const AllEntities &in, const Parameters ¶ms) |
| template<typename Polynomials > | |
| static void | compute_logderivative_inverse (Polynomials &polynomials, auto &relation_parameters, const size_t circuit_size) |
| Construct the polynomial I whose components are the inverse of the product of the read and write terms. | |
| template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters > | |
| static void | accumulate (ContainerOverSubrelations &accumulator, const AllEntities &in, const Parameters ¶ms, const FF &scaling_factor) |
| Accumulate the subrelation contributions for reads from a lookup table. | |
Static Public Attributes | |
| static constexpr size_t | WRITE_TERMS = 1 |
| static constexpr size_t | INVERSE_SUBRELATION_LENGTH = 5 |
| static constexpr size_t | LOOKUP_SUBRELATION_LENGTH = 5 |
| static constexpr size_t | BOOLEAN_CHECK_SUBRELATION_LENGTH |
| static constexpr std::array< size_t, 3 > | SUBRELATION_PARTIAL_LENGTHS |
| static constexpr std::array< bool, 3 > | SUBRELATION_LINEARLY_INDEPENDENT |
Log-derivative lookup argument relation for establishing lookup reads from tables with 3 or fewer columns.
lookup argument seeks to prove lookups from a column by establishing the following sum:
\sum_{i=0}^{n-1} q_{logderiv_lookup}_i * (1 / write_term_i) + read_count_i * (1 / read_term_i) = 0
where write_term = table_col_1 + \gamma + table_col_2 * \eta_1 + table_col_3 * \eta_2 + table_index * \eta_3 and read_term = derived_table_entry_1 + \gamma + derived_table_entry_2 * \eta_1 + derived_table_entry_3 * \eta_2
In practice, we must rephrase this expression in terms of polynomials, one of which is a polynomial I containing (indirectly) the rational functions in the above expression: I_i = 1/[(read_term_i) * (write_term_i)]. This leads to two subrelations. The first demonstrates that the inverse polynomial I is correctly formed. The second is the primary lookup identity, where the rational functions are replaced by the use of the inverse polynomial I. These two subrelations can be expressed as follows:
(1) I_i * (read_term_i) * (write_term_i) - 1 = 0
(2) \sum_{i=0}^{n-1} [q_{logderiv_lookup} * I_i * write_term_i + read_count_i * I_i * read_term_i] = 0
To not compute the inverse terms packed in I_i for indices not included in the sum we introduce a witness called inverse_exists, which is zero when either read_count_i is nonzero (a boolean called read_tag) or we have a read gate. This is represented by setting inverse_exists = 1- (1- read_tag)*(1- is_read_gate). Since is_read_gate is only dependent on selector values, we can assume that the verifier can check that it is boolean. However, if read_tag (which is a derived witness), is not constrained to be boolean, one can set the inverse_exists to 0, even when is_read_gate is 1, because inverse_exists is a linear function of read_tag then. Thus we have a third subrelation, that ensures that read_tag is a boolean value. (3) read_tag * read_tag - read_tag = 0 Further constraining of read_tags and read_counts is not required, since by tampering read_tags a malicious prover can only skip a write_term. This is disadvantagous for the cheating prover as it reduces the size of the lookup table. Hence, a malicious prover can not abuse this to prove an incorrect lookup. Note: Subrelation (2) is "linearly dependent" in the sense that it establishes that a sum across all rows of the exectution trace is zero, rather than that some expression holds independently at each row. Accordingly, this subrelation is not multiplied by a scaling factor at each accumulation step.
Definition at line 65 of file logderiv_lookup_relation.hpp.
| using bb::LogDerivLookupRelationImpl< FF_ >::FF = FF_ |
Definition at line 67 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Accumulate the subrelation contributions for reads from a lookup table.
Three subrelations are required per bus column, first to establish correctness of the precomputed inverses, second to establish the validity of the read, third establishes that read_tags is a boolean value.
| accumulator | transformed to evals + C(in(X)...)*scaling_factor |
| in | an std::array containing the fully extended Accumulator edges. |
| params | contains beta, gamma, and public_input_delta, .... |
| scaling_factor | optional term to scale the evaluation before adding to evals. |
Definition at line 256 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Compute the Accumulator whose values indicate whether the inverse is computed or not.
This is needed for efficiency since we don't need to compute the inverse unless the log derivative lookup relation is active at a given row. We skip the inverse computation for all the rows that read_count_i == 0 AND read_selector is 0
Definition at line 121 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Construct the polynomial I whose components are the inverse of the product of the read and write terms.
If the denominators of log derivative lookup relation are read_term and write_term, then I_i = (read_term_i*write_term_i)^{-1}.
Definition at line 216 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Definition at line 164 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Definition at line 141 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Definition at line 109 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Does the provided row contain data relevant to table lookups; Used to determine whether the polynomial of inverses must be computed at a given row.
In order to avoid unnecessary computation, the polynomial of inverses I is only computed for rows at which the lookup relation is "active". It is active if either (1) the present row contains a lookup gate (i.e. q_lookup == 1), or (2) the present row contains table data that has been looked up in this circuit (lookup_read_tags == 1, or equivalently, if the row in consideration has index i, the data in polynomials table_i has been utlized in the circuit).
Definition at line 102 of file logderiv_lookup_relation.hpp.
|
inlinestatic |
Definition at line 86 of file logderiv_lookup_relation.hpp.
|
staticconstexpr |
Definition at line 72 of file logderiv_lookup_relation.hpp.
|
staticconstexpr |
Definition at line 70 of file logderiv_lookup_relation.hpp.
|
staticconstexpr |
Definition at line 71 of file logderiv_lookup_relation.hpp.
|
staticconstexpr |
Definition at line 82 of file logderiv_lookup_relation.hpp.
|
staticconstexpr |
Definition at line 75 of file logderiv_lookup_relation.hpp.
|
staticconstexpr |
Definition at line 68 of file logderiv_lookup_relation.hpp.