Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
bb::LogDerivLookupRelationImpl< FF_ > Class Template Reference

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.
 
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_table_term (const AllEntities &in, const Parameters &params)
 Compute the table term.
 
template<typename Accumulator , typename AllEntities , typename Parameters >
static Accumulator compute_lookup_term (const AllEntities &in, const Parameters &params)
 
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 &params, const FF &scaling_factor)
 Accumulate the subrelation contributions for reads from a lookup table.
 

Static Public Attributes

static constexpr size_t TABLE_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
 

Detailed Description

template<typename FF_>
class bb::LogDerivLookupRelationImpl< FF_ >

Log-derivative lookup argument relation for establishing lookup reads from tables with 3 or fewer columns.

The lookup argument seeks to prove lookups from a column by establishing the following sum:

\[ \sum_{i=0}^{n-1} q_{\text{logderiv_lookup},i} \cdot \frac{1}{\text{lookup_term}_i} - \text{read_count}_i \cdot \frac{1}{\text{table_term}_i} = 0 \]

where

\[ \text{table_term} = \text{table_col}_1 + \gamma + \text{table_col}_2 \cdot \beta + \text{table_col}_3 \cdot \beta^2 + \text{table_index} \cdot \beta^3 \]

and

\[ \text{lookup_term} = \text{derived_table_entry}_1 + \gamma + \text{derived_table_entry}_2 \cdot \beta + \text{derived_table_entry}_3 \cdot \beta^2 + \text{table_index} \cdot \beta^3 \]

with

\[ \text{derived_table_entry}_i = w_i - \text{col_step_size}_i \cdot w_{i,\text{shift}} \]

(read note for explanation).

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).

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/[(\text{lookup_term}_i) \cdot (\text{table_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:

Subrelation 1 (Inverse correctness):

\[ I_i \cdot (\text{lookup_term}_i) \cdot (\text{table_term}_i) - 1 = 0 \]

Subrelation 2 (Lookup identity):

\[ \sum_{i=0}^{n-1} [q_{\text{logderiv_lookup}} \cdot I_i \cdot \text{table_term}_i - \text{read_count}_i \cdot I_i \cdot \text{lookup_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 \(\text{inverse_exists} = 1 - (1 - \text{read_tag}) \cdot (1 - \text{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 any value when is_read_gate = 0, because inverse_exists is a linear function of read_tag then. Thus we have a third subrelation that ensures read_tag is a boolean value.

Subrelation 3 (Boolean check):

\[ \text{read_tag} \cdot \text{read_tag} - \text{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 table_term. This is disadvantageous for the cheating prover as it reduces the size of the lookup table. Hence, a malicious prover cannot 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 execution 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.
The "real" table entries must be 'derived' from wire values since instead of storing actual values in wires we store successive accumulators, the differences of which are equal to entries in a table. This is an efficiency trick for the case where entries of the "real" table correspond to limbs of a value too large to be supported by the lookup table. This way we avoid using additional gates to reconstruct full size values from the limbs contained in tables. See the documentation in method bb::plookup::get_lookup_accumulators().

IMPORTANT: γ and β must be independent challenges for soundness.

Definition at line 95 of file logderiv_lookup_relation.hpp.

Member Typedef Documentation

◆ FF

template<typename FF_ >
using bb::LogDerivLookupRelationImpl< FF_ >::FF = FF_

Definition at line 97 of file logderiv_lookup_relation.hpp.

Member Function Documentation

◆ accumulate()

template<typename FF_ >
template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters >
static void bb::LogDerivLookupRelationImpl< FF_ >::accumulate ( ContainerOverSubrelations &  accumulator,
const AllEntities &  in,
const Parameters &  params,
const FF scaling_factor 
)
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.

Parameters
accumulatortransformed to evals + C(in(X)...)*scaling_factor
inan std::array containing the fully extended Accumulator edges.
paramscontains beta, gamma, and public_input_delta, ....
scaling_factoroptional term to scale the evaluation before adding to evals.

Definition at line 307 of file logderiv_lookup_relation.hpp.

◆ compute_inverse_exists()

template<typename FF_ >
template<typename Accumulator , typename AllEntities >
static Accumulator bb::LogDerivLookupRelationImpl< FF_ >::compute_inverse_exists ( const AllEntities &  in)
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 \(\text{read_count}_i = 0\) AND read_selector is 0.

Note
read_tag is constructed such that \(\text{read_tag}_i \in \{0, 1\}\). We add a subrelation to check that read_tag is a boolean value.
Template Parameters
AccumulatorAccumulator type for polynomial evaluations
AllEntitiesType containing all polynomial entities
Parameters
inAll entities
Returns
Accumulator indicating whether inverse should be computed

Definition at line 158 of file logderiv_lookup_relation.hpp.

◆ compute_logderivative_inverse()

template<typename FF_ >
template<typename Polynomials >
static void bb::LogDerivLookupRelationImpl< FF_ >::compute_logderivative_inverse ( Polynomials &  polynomials,
auto &  relation_parameters,
const size_t  circuit_size 
)
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 lookup_term and table_term, then \(I_i = (\text{lookup_term}_i \cdot \text{table_term}_i)^{-1}\).

Note
Importantly, \(I_i = 0\) for rows \(i\) at which there is no read or write, so the cost of this method is proportional to the actual number of lookups.

Definition at line 270 of file logderiv_lookup_relation.hpp.

◆ compute_lookup_term()

template<typename FF_ >
template<typename Accumulator , typename AllEntities , typename Parameters >
static Accumulator bb::LogDerivLookupRelationImpl< FF_ >::compute_lookup_term ( const AllEntities &  in,
const Parameters &  params 
)
inlinestatic

Definition at line 215 of file logderiv_lookup_relation.hpp.

◆ compute_table_term()

template<typename FF_ >
template<typename Accumulator , typename AllEntities , typename Parameters >
static Accumulator bb::LogDerivLookupRelationImpl< FF_ >::compute_table_term ( const AllEntities &  in,
const Parameters &  params 
)
inlinestatic

Compute the table term.

Computes \(\text{table}_1 + \gamma + \text{table}_2 \cdot \beta + \text{table}_3 \cdot \beta^2 + \text{table}_4 \cdot \beta^3\), where table \(_{1,2,3}\) correspond to the (maximum) three columns of the lookup table and table \(_4\) is the unique identifier of the lookup table (table_index).

Template Parameters
AccumulatorAccumulator type for polynomial evaluations
AllEntitiesType containing all polynomial entities
ParametersType containing relation parameters
Parameters
inAll entities
paramsRelation parameters (gamma, eta, eta_two, eta_three)
Returns
Accumulator containing the computed table term

Definition at line 192 of file logderiv_lookup_relation.hpp.

◆ get_inverse_polynomial()

template<typename FF_ >
template<typename AllEntities >
static auto & bb::LogDerivLookupRelationImpl< FF_ >::get_inverse_polynomial ( AllEntities &  in)
inlinestatic

Definition at line 140 of file logderiv_lookup_relation.hpp.

◆ operation_exists_at_row()

template<typename FF_ >
template<typename AllValues >
static bool bb::LogDerivLookupRelationImpl< FF_ >::operation_exists_at_row ( const AllValues &  row)
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_{\text{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 utilized in the circuit).

Definition at line 133 of file logderiv_lookup_relation.hpp.

◆ skip()

template<typename FF_ >
template<typename AllEntities >
static bool bb::LogDerivLookupRelationImpl< FF_ >::skip ( const AllEntities &  in)
inlinestatic

Definition at line 116 of file logderiv_lookup_relation.hpp.

Member Data Documentation

◆ BOOLEAN_CHECK_SUBRELATION_LENGTH

template<typename FF_ >
constexpr size_t bb::LogDerivLookupRelationImpl< FF_ >::BOOLEAN_CHECK_SUBRELATION_LENGTH
staticconstexpr
Initial value:
=
3

Definition at line 102 of file logderiv_lookup_relation.hpp.

◆ INVERSE_SUBRELATION_LENGTH

template<typename FF_ >
constexpr size_t bb::LogDerivLookupRelationImpl< FF_ >::INVERSE_SUBRELATION_LENGTH = 5
staticconstexpr

Definition at line 100 of file logderiv_lookup_relation.hpp.

◆ LOOKUP_SUBRELATION_LENGTH

template<typename FF_ >
constexpr size_t bb::LogDerivLookupRelationImpl< FF_ >::LOOKUP_SUBRELATION_LENGTH = 5
staticconstexpr

Definition at line 101 of file logderiv_lookup_relation.hpp.

◆ SUBRELATION_LINEARLY_INDEPENDENT

template<typename FF_ >
constexpr std::array<bool, 3> bb::LogDerivLookupRelationImpl< FF_ >::SUBRELATION_LINEARLY_INDEPENDENT
staticconstexpr
Initial value:
= { true ,
false ,
true }

Definition at line 112 of file logderiv_lookup_relation.hpp.

◆ SUBRELATION_PARTIAL_LENGTHS

template<typename FF_ >
constexpr std::array<size_t, 3> bb::LogDerivLookupRelationImpl< FF_ >::SUBRELATION_PARTIAL_LENGTHS
staticconstexpr

◆ TABLE_TERMS

template<typename FF_ >
constexpr size_t bb::LogDerivLookupRelationImpl< FF_ >::TABLE_TERMS = 1
staticconstexpr

Definition at line 98 of file logderiv_lookup_relation.hpp.


The documentation for this class was generated from the following file: