|
| template<typename AllEntities > |
| static bool | skip (const AllEntities &in) |
| |
| template<size_t bus_idx, typename AllValues > |
| static bool | operation_exists_at_row (const AllValues &row) |
| | Determine whether the inverse I needs to be computed at a given row for a given bus column.
|
| |
| template<typename Accumulator , size_t bus_idx, 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 , size_t bus_idx, typename AllEntities > |
| static Accumulator | get_read_selector (const AllEntities &in) |
| | Compute scalar for read term in log derivative lookup argument.
|
| |
| template<typename Accumulator , size_t bus_idx, typename AllEntities , typename Parameters > |
| static Accumulator | compute_write_term (const AllEntities &in, const Parameters ¶ms) |
| | Compute write term denominator in log derivative lookup argument.
|
| |
| template<typename Accumulator , typename AllEntities , typename Parameters > |
| static Accumulator | compute_read_term (const AllEntities &in, const Parameters ¶ms) |
| | Compute read term denominator in log derivative lookup argument.
|
| |
| template<size_t bus_idx, 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 FF , size_t bus_idx, typename ContainerOverSubrelations , typename AllEntities , typename Parameters > |
| static void | accumulate_subrelation_contributions (ContainerOverSubrelations &accumulator, const AllEntities &in, const Parameters ¶ms, const FF &scaling_factor) |
| | Accumulate the subrelation contributions for reads from a single databus column.
|
| |
| template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters > |
| static void | accumulate (ContainerOverSubrelations &accumulator, const AllEntities &in, const Parameters ¶ms, const FF &scaling_factor) |
| | Accumulate the log derivative databus lookup argument subrelation contributions for each databus column.
|
| |
template<typename FF_>
class bb::DatabusLookupRelationImpl< FF_ >
Log-derivative lookup argument relation for establishing DataBus reads.
Each column of the databus can be thought of as a table from which we can look up values. The log-derivative 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 the read and write terms are both of the form value_i + idx_i*\beta + \gamma. This expression is motivated by taking the derivative of the log of a more conventional grand product style set equivalence argument (see e.g. https://eprint.iacr.org/2022/1530.pdf for details). For the write term, the (idx, value) pair comes from the "table" (bus column), and for the read term the (idx, value) pair comes from wires 1 and 2 which should contain a valid entry in the table. (Note: the meaning of "read" here is clear: the inputs are an (index, value) pair that we want to read from the table. Here "write" refers to data that is present in the "table", i.e. the bus column. There is no gate associated with a write, the data is simply populated in the corresponding column and committed to when constructing a proof).
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 In reality this relation is I_i * (read_term_i) * (write_term_i) - inverse_exists = 0, i.e. it is only checked for active gates (more explanation below).
(2) \sum_{i=0}^{n-1} [q_{logderiv_lookup} * I_i * write_term_i + read_count_i * I_i * read_term_i] = 0
Each column of the DataBus requires its own pair of subrelations. The column being read is selected via a unique product, i.e. a lookup from bus column j is selected via q_busread * q_j (j = 1,2,...).
To not compute the inverse terms packed in I_i for indices that 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 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 Note: that 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 62 of file databus_lookup_relation.hpp.
1.9.8