Log-derivative lookup argument relation for establishing DataBus reads. More...

#include <databus_lookup_relation.hpp>

Classes
struct	BusData

struct	BusData< 0, AllEntities >

struct	BusData< 1, AllEntities >

struct	BusData< 2, AllEntities >

Public Types
using	FF = FF_

Static Public Member Functions
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)

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_table_term (const AllEntities &in, const Parameters &params)
	Compute write term denominator in log derivative lookup argument.

template<typename Accumulator , typename AllEntities , typename Parameters >
static Accumulator	compute_lookup_term (const AllEntities &in, const Parameters &params)
	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 &params, 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 &params, const FF &scaling_factor)
	Accumulate the log derivative databus lookup argument subrelation contributions for each databus column.

Static Public Attributes
static constexpr size_t	NUM_BUS_COLUMNS = 3

static constexpr size_t	INVERSE_SUBREL_LENGTH = 5

static constexpr size_t	INVERSE_SUBREL_LENGTH_ADJUSTMENT = 0

static constexpr size_t	LOOKUP_SUBREL_LENGTH = 5

static constexpr size_t	LOOKUP_SUBREL_LENGTH_ADJUSTMENT = 0

static constexpr size_t	READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH

static constexpr size_t	READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT = 0

static constexpr size_t	NUM_SUB_RELATION_PER_IDX = 3

static constexpr std::array< size_t, NUM_SUB_RELATION_PER_IDX *NUM_BUS_COLUMNS >	SUBRELATION_PARTIAL_LENGTHS

static constexpr bool	INVERSE_SUBREL_LIN_INDEPENDENT = true

static constexpr bool	LOOKUP_SUBREL_LIN_INDEPENDENT = false

static constexpr bool	READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT = true

static constexpr std::array< bool, NUM_SUB_RELATION_PER_IDX *NUM_BUS_COLUMNS >	SUBRELATION_LINEARLY_INDEPENDENT

Detailed Description

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_{\text{logderiv_lookup},i} \cdot \frac{1}{\text{lookup_term}_i} - \text{read_count}_i \cdot \frac{1}{\text{table_term}_i} = 0 \]

where the lookup and table terms are both of the form $\text{value}_i + \text{idx}_i \cdot \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 table term, the (idx, value) pair comes from the "table" (bus column), and for the lookup term the (idx, value) pair comes from wires 1 and 2 which should contain a valid entry in the table.

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 \]

In reality this relation is $I_i \cdot (\text{lookup_term}_i) \cdot (\text{table_term}_i) - \text{inverse_exists} = 0$, i.e. it is only checked for active gates (more explanation below).

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 \]

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_{\text{busread}} \cdot q_j$ (j = 1,2,...).

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 $\text{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 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 that read_tag is a boolean value.

Subrelation 3 (Boolean check):

\[ \text{read_tag} \cdot \text{read_tag} - \text{read_tag} = 0 \]

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.

Definition at line 77 of file databus_lookup_relation.hpp.

Member Typedef Documentation

◆ FF

template<typename FF_ >

using bb::DatabusLookupRelationImpl< FF_ >::FF = FF_

Definition at line 79 of file databus_lookup_relation.hpp.

Member Function Documentation

◆ accumulate()

template<typename FF_ >

template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters >

static void bb::DatabusLookupRelationImpl< FF_ >::accumulate	(	ContainerOverSubrelations &	accumulator,
		const AllEntities &	in,
		const Parameters &	params,
		const FF &	scaling_factor
	)

inlinestatic

Accumulate the log derivative databus lookup argument subrelation contributions for each databus column.

Parameters

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 388 of file databus_lookup_relation.hpp.

◆ accumulate_subrelation_contributions()

template<typename FF_ >

template<typename FF , size_t bus_idx, typename ContainerOverSubrelations , typename AllEntities , typename Parameters >

static void bb::DatabusLookupRelationImpl< FF_ >::accumulate_subrelation_contributions	(	ContainerOverSubrelations &	accumulator,
		const AllEntities &	in,
		const Parameters &	params,
		const FF &	scaling_factor
	)

inlinestatic

Accumulate the subrelation contributions for reads from a single databus column.

Three subrelations are required per bus column, one to establish correctness of the precomputed inverses, one to establish the validity of the read, and one to ensure read_tags is a boolean value

Parameters

accumulator
in
params
scaling_factor

Definition at line 333 of file databus_lookup_relation.hpp.

◆ compute_inverse_exists()

template<typename FF_ >

template<typename Accumulator , size_t bus_idx, typename AllEntities >

static Accumulator bb::DatabusLookupRelationImpl< FF_ >::compute_inverse_exists ( const AllEntities & in )

inlinestatic

$. We add a subrelation to check that $\text{read_tag}$ is a boolean value.

Definition at line 185 of file databus_lookup_relation.hpp.

◆ compute_logderivative_inverse()

template<typename FF_ >

template<size_t bus_idx, typename Polynomials >

static void bb::DatabusLookupRelationImpl< 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 databus usage.

Definition at line 274 of file databus_lookup_relation.hpp.

◆ compute_lookup_term()

template<typename FF_ >

template<typename Accumulator , typename AllEntities , typename Parameters >

static Accumulator bb::DatabusLookupRelationImpl< FF_ >::compute_lookup_term	(	const AllEntities &	in,
		const Parameters &	params
	)

inlinestatic

Compute read term denominator in log derivative lookup argument.

Note: No bus_idx required here since inputs to a read are of the same form regardless the bus column

Definition at line 247 of file databus_lookup_relation.hpp.

◆ compute_table_term()

template<typename FF_ >

template<typename Accumulator , size_t bus_idx, typename AllEntities , typename Parameters >

static Accumulator bb::DatabusLookupRelationImpl< FF_ >::compute_table_term	(	const AllEntities &	in,
		const Parameters &	params
	)

inlinestatic

Compute write term denominator in log derivative lookup argument.

Definition at line 226 of file databus_lookup_relation.hpp.

◆ get_read_selector()

template<typename FF_ >

template<typename Accumulator , size_t bus_idx, typename AllEntities >

static Accumulator bb::DatabusLookupRelationImpl< FF_ >::get_read_selector ( const AllEntities & in )

inlinestatic

Compute scalar for read term in log derivative lookup argument.

The selector indicating read from bus column $j$ is given by $q_{\text{busread}} \cdot q_j$, where $j \in \{1, 2, 3\}$.

Definition at line 210 of file databus_lookup_relation.hpp.

◆ operation_exists_at_row()

template<typename FF_ >

template<size_t bus_idx, typename AllValues >

static bool bb::DatabusLookupRelationImpl< FF_ >::operation_exists_at_row ( const AllValues & row )

inlinestatic

Determine whether the inverse I needs to be computed at a given row for a given bus column.

The value of the inverse polynomial I(X) only needs to be computed when the databus lookup gate is "active". Otherwise it is set to 0. This method allows for determination of when the inverse should be computed.

Template Parameters

AllValues

Parameters

row

Definition at line 166 of file databus_lookup_relation.hpp.

◆ skip()

template<typename FF_ >

template<typename AllEntities >

template<typename FF_ >

constexpr size_t bb::DatabusLookupRelationImpl< FF_ >::READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH

staticconstexpr

Initial value:

=

3

Definition at line 89 of file databus_lookup_relation.hpp.

◆ READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT

template<typename FF_ >

constexpr size_t bb::DatabusLookupRelationImpl< FF_ >::READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT = 0

staticconstexpr

Definition at line 91 of file databus_lookup_relation.hpp.

◆ SUBRELATION_LINEARLY_INDEPENDENT

template<typename FF_ >

constexpr std::array<bool, NUM_SUB_RELATION_PER_IDX * NUM_BUS_COLUMNS> bb::DatabusLookupRelationImpl< FF_ >::SUBRELATION_LINEARLY_INDEPENDENT

staticconstexpr

Initial value:

= {
        INVERSE_SUBREL_LIN_INDEPENDENT, LOOKUP_SUBREL_LIN_INDEPENDENT, READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT,
        INVERSE_SUBREL_LIN_INDEPENDENT, LOOKUP_SUBREL_LIN_INDEPENDENT, READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT,
        INVERSE_SUBREL_LIN_INDEPENDENT, LOOKUP_SUBREL_LIN_INDEPENDENT, READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT
    }

Definition at line 112 of file databus_lookup_relation.hpp.

◆ SUBRELATION_PARTIAL_LENGTHS

template<typename FF_ >

constexpr std::array<size_t, NUM_SUB_RELATION_PER_IDX * NUM_BUS_COLUMNS> bb::DatabusLookupRelationImpl< FF_ >::SUBRELATION_PARTIAL_LENGTHS

staticconstexpr

Initial value:

{
        INVERSE_SUBREL_LENGTH,                
        LOOKUP_SUBREL_LENGTH,                 
        READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH, 
        INVERSE_SUBREL_LENGTH,                
        LOOKUP_SUBREL_LENGTH,                 
        READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH, 
        INVERSE_SUBREL_LENGTH,                
        LOOKUP_SUBREL_LENGTH,                 
        READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH, 
    }

Definition at line 94 of file databus_lookup_relation.hpp.

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

src/barretenberg/relations/databus_lookup_relation.hpp

Classes

Public Types

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ FF

Member Function Documentation

◆ accumulate()

◆ accumulate_subrelation_contributions()

◆ compute_inverse_exists()

◆ compute_logderivative_inverse()

◆ compute_lookup_term()

◆ compute_table_term()

◆ get_read_selector()

◆ operation_exists_at_row()

◆ skip()

Member Data Documentation

◆ INVERSE_SUBREL_LENGTH

◆ INVERSE_SUBREL_LENGTH_ADJUSTMENT

◆ INVERSE_SUBREL_LIN_INDEPENDENT

◆ LOOKUP_SUBREL_LENGTH

◆ LOOKUP_SUBREL_LENGTH_ADJUSTMENT

◆ LOOKUP_SUBREL_LIN_INDEPENDENT

◆ NUM_BUS_COLUMNS

◆ NUM_SUB_RELATION_PER_IDX

◆ READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT

◆ READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH

◆ READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT

◆ SUBRELATION_LINEARLY_INDEPENDENT

◆ SUBRELATION_PARTIAL_LENGTHS