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)
	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 &params)
	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 &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 std::array< size_t, NUM_SUB_RELATION_PER_IDX *NUM_BUS_COLUMNS >	TOTAL_LENGTH_ADJUSTMENTS

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_{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

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

Note: that the latter subrelation 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 52 of file databus_lookup_relation.hpp.

Member Typedef Documentation

◆ FF

template<typename FF_ >

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

Definition at line 54 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.

Each databus column requires three subrelations. the last relation is to make sure that the read_tag is a boolean value. check the logderiv_lookup_relation.hpp for more details.

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

Two subrelations are required per bus column, one to establish correctness of the precomputed inverses and one to establish the validity of the read.

Parameters

accumulator
in
params
scaling_factor

Definition at line 313 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

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.

Note: read_counts is constructed such that read_count_i <= 1 and is thus treated as boolean.

Definition at line 169 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 read_term and write_term, then I_i = (read_term_i*write_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 251 of file databus_lookup_relation.hpp.

◆ compute_read_term()

template<typename FF_ >

template<typename Accumulator , typename AllEntities , typename Parameters >

static Accumulator bb::DatabusLookupRelationImpl< FF_ >::compute_read_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 225 of file databus_lookup_relation.hpp.

◆ compute_write_term()

template<typename FF_ >

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

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

inlinestatic

Compute write term denominator in log derivative lookup argument.

Definition at line 203 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_busread * q_j, j = 1,2,3

Definition at line 187 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 154 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 65 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 67 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 100 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 70 of file databus_lookup_relation.hpp.

◆ TOTAL_LENGTH_ADJUSTMENTS

template<typename FF_ >

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

staticconstexpr

Initial value:

{
        INVERSE_SUBREL_LENGTH_ADJUSTMENT,
        LOOKUP_SUBREL_LENGTH_ADJUSTMENT,
        READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT,
        INVERSE_SUBREL_LENGTH_ADJUSTMENT,
        LOOKUP_SUBREL_LENGTH_ADJUSTMENT,
        READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT,
        INVERSE_SUBREL_LENGTH_ADJUSTMENT,
        LOOKUP_SUBREL_LENGTH_ADJUSTMENT,
        READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT
    }

Definition at line 82 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_read_term()

◆ compute_write_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

◆ TOTAL_LENGTH_ADJUSTMENTS