Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
databus_lookup_relation.hpp
Go to the documentation of this file.
1// === AUDIT STATUS ===
2// internal: { status: Complete, auditors: [Sergei], commit: }
3// external_1: { status: not started, auditors: [], commit: }
4// external_2: { status: not started, auditors: [], commit: }
5// =====================
6
7#pragma once
8#include <array>
9#include <tuple>
10
15
16namespace bb {
17
77template <typename FF_> class DatabusLookupRelationImpl {
78 public:
79 using FF = FF_;
80 static constexpr size_t NUM_BUS_COLUMNS = 3; // calldata, return data
81 // the actual degree of this subrelation is 3, and requires a degree adjustment of 1.
82 // however as we reuse the accumulators used to compute this subrelation for the lookup subrelation, we set the
83 // degree to 4 which removes the need of having degree adjustments for folding.
84 static constexpr size_t INVERSE_SUBREL_LENGTH = 5; // deg + 1 of inverse correctness subrelation
85 static constexpr size_t INVERSE_SUBREL_LENGTH_ADJUSTMENT = 0;
86 // the max degree of this subrelation is 4
87 static constexpr size_t LOOKUP_SUBREL_LENGTH = 5; // deg + 1 of log-deriv lookup subrelation
88 static constexpr size_t LOOKUP_SUBREL_LENGTH_ADJUSTMENT = 0;
89 static constexpr size_t READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH =
90 3; // deg + 1 of the relation checking that read_tag_m is a boolean value
92 static constexpr size_t NUM_SUB_RELATION_PER_IDX = 3; // the number of subrelations per bus column
93
94 static constexpr std::array<size_t, NUM_SUB_RELATION_PER_IDX * NUM_BUS_COLUMNS> SUBRELATION_PARTIAL_LENGTHS{
95 INVERSE_SUBREL_LENGTH, // inverse polynomial correctness subrelation (bus_idx 0)
96 LOOKUP_SUBREL_LENGTH, // log-derivative lookup argument subrelation (bus_idx 0)
97 READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH, // read_tag_m* read_tag_m - read_tag_m (bus_idx 0)
98 INVERSE_SUBREL_LENGTH, // inverse polynomial correctness subrelation (bus_idx 1)
99 LOOKUP_SUBREL_LENGTH, // log-derivative lookup argument subrelation (bus_idx 1)
100 READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH, // read_tag_m* read_tag_m - read_tag_m (bus_idx 1)
101 INVERSE_SUBREL_LENGTH, // inverse polynomial correctness subrelation (bus_idx 2)
102 LOOKUP_SUBREL_LENGTH, // log-derivative lookup argument subrelation (bus_idx 2)
103 READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH, // read_tag_m* read_tag_m - read_tag_m (bus_idx 2)
104 };
105
106 static constexpr bool INVERSE_SUBREL_LIN_INDEPENDENT = true; // to be satisfied independently at each row
107 static constexpr bool LOOKUP_SUBREL_LIN_INDEPENDENT = false; // to be satisfied as a sum across all rows
108 static constexpr bool READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT = true; // to be satisfied independently at each row
109
110 // The lookup subrelations are "linearly dependent" in the sense that they establish the value of a sum across the
111 // entire execution trace rather than a per-row identity.
117
118 template <typename AllEntities> inline static bool skip([[maybe_unused]] const AllEntities& in)
119 {
120 // Ensure the input does not contain a read gate or data that is being read
121 return in.q_busread.is_zero() && in.calldata_read_counts.is_zero() &&
122 in.secondary_calldata_read_counts.is_zero() && in.return_data_read_counts.is_zero();
123 }
124
125 // Interface for easy access of databus components by column (bus_idx)
126 template <size_t bus_idx, typename AllEntities> struct BusData;
127
128 // Specialization for calldata (bus_idx = 0)
129 template <typename AllEntities> struct BusData</*bus_idx=*/0, AllEntities> {
130 static auto& values(const AllEntities& in) { return in.calldata; }
131 static auto& selector(const AllEntities& in) { return in.q_l; }
132 static auto& inverses(AllEntities& in) { return in.calldata_inverses; }
133 static auto& inverses(const AllEntities& in) { return in.calldata_inverses; } // const version
134 static auto& read_counts(const AllEntities& in) { return in.calldata_read_counts; }
135 static auto& read_tags(const AllEntities& in) { return in.calldata_read_tags; }
136 };
137
138 // Specialization for secondary_calldata (bus_idx = 1)
139 template <typename AllEntities> struct BusData</*bus_idx=*/1, AllEntities> {
140 static auto& values(const AllEntities& in) { return in.secondary_calldata; }
141 static auto& selector(const AllEntities& in) { return in.q_r; }
142 static auto& inverses(AllEntities& in) { return in.secondary_calldata_inverses; }
143 static auto& inverses(const AllEntities& in) { return in.secondary_calldata_inverses; } // const version
144 static auto& read_counts(const AllEntities& in) { return in.secondary_calldata_read_counts; }
145 static auto& read_tags(const AllEntities& in) { return in.secondary_calldata_read_tags; }
146 };
147
148 // Specialization for return data (bus_idx = 2)
149 template <typename AllEntities> struct BusData</*bus_idx=*/2, AllEntities> {
150 static auto& values(const AllEntities& in) { return in.return_data; }
151 static auto& selector(const AllEntities& in) { return in.q_o; }
152 static auto& inverses(AllEntities& in) { return in.return_data_inverses; }
153 static auto& inverses(const AllEntities& in) { return in.return_data_inverses; } // const version
154 static auto& read_counts(const AllEntities& in) { return in.return_data_read_counts; }
155 static auto& read_tags(const AllEntities& in) { return in.return_data_read_tags; }
156 };
157
166 template <size_t bus_idx, typename AllValues> static bool operation_exists_at_row(const AllValues& row)
167 {
168 auto read_selector = get_read_selector<FF, bus_idx>(row);
169 auto read_tag = BusData<bus_idx, AllValues>::read_tags(row);
170 return (read_selector == 1 || read_tag == 1);
171 }
172
184 template <typename Accumulator, size_t bus_idx, typename AllEntities>
185 static Accumulator compute_inverse_exists(const AllEntities& in)
186 {
187 using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
188
189 const auto is_read_gate = get_read_selector<Accumulator, bus_idx>(in); // is this a read gate
190 const auto read_tag_m =
191 CoefficientAccumulator(BusData<bus_idx, AllEntities>::read_tags(in)); // does row contain data being read
192 const Accumulator read_tag(read_tag_m);
193 // Relation checking: is_read_gate == 1 || read_tag == 1
194 // Important note: the relation written below assumes that is_read_gate and read_tag are boolean values, which
195 // is guaranteed by the boolean_check subrelation. If not, fixing one of the two, the return value is a linear
196 // function in the other variable and can be set to an arbitrary value independent of the fixed value. See the
197 // boolean_check subrelation for more explanation.
198 // degree 2(2) 1 2 (2) 1 // Degree 3 (3)
199 return is_read_gate + read_tag - (is_read_gate * read_tag); // Degree 3 (5)
200 }
201
209 template <typename Accumulator, size_t bus_idx, typename AllEntities>
210 static Accumulator get_read_selector(const AllEntities& in)
211 {
212 using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
213
214 auto q_busread = CoefficientAccumulator(in.q_busread);
215 auto column_selector = CoefficientAccumulator(BusData<bus_idx, AllEntities>::selector(in));
216
217 // degree 1 1 2 (2)
218 return Accumulator(q_busread * column_selector);
219 }
220
225 template <typename Accumulator, size_t bus_idx, typename AllEntities, typename Parameters>
226 static Accumulator compute_table_term(const AllEntities& in, const Parameters& params)
227 {
228 using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
229 using ParameterCoefficientAccumulator = typename Parameters::DataType::CoefficientAccumulator;
230
231 const auto& id = CoefficientAccumulator(in.databus_id);
232 const auto& value = CoefficientAccumulator(BusData<bus_idx, AllEntities>::values(in));
233 const auto& gamma = ParameterCoefficientAccumulator(params.gamma);
234 const auto& beta = ParameterCoefficientAccumulator(params.beta);
235
236 // Construct value_i + idx_i*\beta + \gamma
237 // degrees 1(0) 0(1) 1(1) 0(1)
238 return Accumulator(id * beta + value + gamma); // degree 1 (1)
239 }
240
246 template <typename Accumulator, typename AllEntities, typename Parameters>
247 static Accumulator compute_lookup_term(const AllEntities& in, const Parameters& params)
248 {
249 using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
250 using ParameterCoefficientAccumulator = typename Parameters::DataType::CoefficientAccumulator;
251
252 // Bus value stored in w_1, index into bus column stored in w_2
253 const auto& w_1 = CoefficientAccumulator(in.w_l);
254 const auto& w_2 = CoefficientAccumulator(in.w_r);
255 const auto& gamma = ParameterCoefficientAccumulator(params.gamma);
256 const auto& beta = ParameterCoefficientAccumulator(params.beta);
257
258 // Construct value + index*\beta + \gamma
259 return Accumulator((w_2 * beta) + w_1 + gamma); // degree 1 (2)
260 }
261
273 template <size_t bus_idx, typename Polynomials>
274 static void compute_logderivative_inverse(Polynomials& polynomials,
275 auto& relation_parameters,
276 const size_t circuit_size)
277 {
278 BB_BENCH_NAME("Databus::compute_logderivative_inverse");
279 auto& inverse_polynomial = BusData<bus_idx, Polynomials>::inverses(polynomials);
280
281 size_t min_iterations_per_thread = 1 << 6; // min number of iterations for which we'll spin up a unique thread
282 size_t num_threads = bb::calculate_num_threads(circuit_size, min_iterations_per_thread);
283
284 parallel_for(num_threads, [&](ThreadChunk chunk) {
285 bool is_read = false;
286 bool nonzero_read_count = false;
287 for (size_t i : chunk.range(circuit_size)) {
288 // Determine if the present row contains a databus operation
289 auto q_busread = polynomials.q_busread[i];
290 if constexpr (bus_idx == 0) { // calldata
291 is_read = q_busread == 1 && polynomials.q_l[i] == 1;
292 nonzero_read_count = polynomials.calldata_read_counts[i] > 0;
293 }
294 if constexpr (bus_idx == 1) { // secondary_calldata
295 is_read = q_busread == 1 && polynomials.q_r[i] == 1;
296 nonzero_read_count = polynomials.secondary_calldata_read_counts[i] > 0;
297 }
298 if constexpr (bus_idx == 2) { // return data
299 is_read = q_busread == 1 && polynomials.q_o[i] == 1;
300 nonzero_read_count = polynomials.return_data_read_counts[i] > 0;
301 }
302 // We only compute the inverse if this row contains a read gate or data that has been read
303 if (is_read || nonzero_read_count) {
304 // TODO(https://github.com/AztecProtocol/barretenberg/issues/940): avoid get_row if possible.
305 auto row = polynomials.get_row(i); // Note: this is a copy. use sparingly!
306 auto value = compute_lookup_term<FF>(row, relation_parameters) *
307 compute_table_term<FF, bus_idx>(row, relation_parameters);
308 inverse_polynomial.at(i) = value;
309 }
310 }
311 });
312
313 // Compute inverse polynomial I in place by inverting the product at each row
314 // Note: zeroes are ignored as they are not used anyway
315 FF::batch_invert(inverse_polynomial.coeffs());
316 };
317
328 template <typename FF,
329 size_t bus_idx,
330 typename ContainerOverSubrelations,
331 typename AllEntities,
332 typename Parameters>
333 static void accumulate_subrelation_contributions(ContainerOverSubrelations& accumulator,
334 const AllEntities& in,
335 const Parameters& params,
336 const FF& scaling_factor)
337 {
338 using Accumulator = typename std::tuple_element_t<4, ContainerOverSubrelations>;
339 using CoefficientAccumulator = typename Accumulator::CoefficientAccumulator;
341 const auto inverses_m = CoefficientAccumulator(BusData<bus_idx, AllEntities>::inverses(in)); // Degree 1
342 Accumulator inverses(inverses_m);
343 const auto read_counts_m = CoefficientAccumulator(BusData<bus_idx, AllEntities>::read_counts(in)); // Degree 1
344 const auto lookup_term = compute_lookup_term<Accumulator>(in, params); // Degree 1
345 const auto table_term = compute_table_term<Accumulator, bus_idx>(in, params); // Degree 1
346 const auto inverse_exists = compute_inverse_exists<Accumulator, bus_idx>(in); // Degree 3
347 const auto read_selector = get_read_selector<Accumulator, bus_idx>(in); // Degree 2
348
349 // Determine which pair of subrelations to update based on which bus column is being read
350 // The inverse relation subrelation index
351 constexpr size_t subrel_idx_1 = NUM_SUB_RELATION_PER_IDX * bus_idx;
352 // The lookup relation subrelation index
353 constexpr size_t subrel_idx_2 = NUM_SUB_RELATION_PER_IDX * bus_idx + 1;
354 // The read_tag boolean check subrelation index
355 constexpr size_t subrel_idx_3 = NUM_SUB_RELATION_PER_IDX * bus_idx + 2;
356
357 // Establish the correctness of the polynomial of inverses I. Note: inverses is computed so that the value
358 // is 0 if !inverse_exists. Degree 3
359 // degrees 3 = 1 1 1 3
360 std::get<subrel_idx_1>(accumulator) += (lookup_term * table_term * inverses - inverse_exists) * scaling_factor;
361
362 // Establish validity of the read. Note: no scaling factor here since this constraint is enforced across the
363 // entire trace, not on a per-row basis.
364
365 // degree 3 = 2 1
366 Accumulator tmp = read_selector * table_term;
367 // degree 2 = 1 1
368 tmp -= Accumulator(read_counts_m) * lookup_term;
369 // degree 1
370 tmp *= inverses;
371 std::get<subrel_idx_2>(accumulator) += tmp; // Deg 4 (4)
372
373 const auto read_tag_m = CoefficientAccumulator(BusData<bus_idx, AllEntities>::read_tags(in));
374 const auto read_tag = ShortAccumulator(read_tag_m);
375 // // this is done by row so we have to multiply by the scaling factor
376 // degree 1 1 1 = 2
377 std::get<subrel_idx_3>(accumulator) += (read_tag * read_tag - read_tag) * scaling_factor;
378 }
379
387 template <typename ContainerOverSubrelations, typename AllEntities, typename Parameters>
388 static void accumulate(ContainerOverSubrelations& accumulator,
389 const AllEntities& in,
390 const Parameters& params,
391 const FF& scaling_factor)
392 {
393 // Accumulate the subrelation contributions for each column of the databus
394 bb::constexpr_for<0, NUM_BUS_COLUMNS, 1>([&]<size_t bus_idx>() {
395 accumulate_subrelation_contributions<FF, bus_idx>(accumulator, in, params, scaling_factor);
396 });
397 }
398};
399
401
402} // namespace bb
#define BB_BENCH_NAME(name)
Definition bb_bench.hpp:225
Log-derivative lookup argument relation for establishing DataBus reads.
static constexpr bool READ_TAG_BOOLEAN_CHECK_LIN_INDEPENDENT
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.
static constexpr size_t NUM_SUB_RELATION_PER_IDX
static bool skip(const AllEntities &in)
static constexpr bool LOOKUP_SUBREL_LIN_INDEPENDENT
static constexpr size_t LOOKUP_SUBREL_LENGTH_ADJUSTMENT
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.
static constexpr std::array< size_t, NUM_SUB_RELATION_PER_IDX *NUM_BUS_COLUMNS > SUBRELATION_PARTIAL_LENGTHS
static void compute_logderivative_inverse(Polynomials &polynomials, auto &relation_parameters, const size_t circuit_size)
Construct the polynomial whose components are the inverse of the product of the read and write terms...
static constexpr size_t LOOKUP_SUBREL_LENGTH
static Accumulator compute_inverse_exists(const AllEntities &in)
static constexpr std::array< bool, NUM_SUB_RELATION_PER_IDX *NUM_BUS_COLUMNS > SUBRELATION_LINEARLY_INDEPENDENT
static Accumulator compute_lookup_term(const AllEntities &in, const Parameters &params)
Compute read term denominator in log derivative lookup argument.
static constexpr bool INVERSE_SUBREL_LIN_INDEPENDENT
static constexpr size_t READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH
static constexpr size_t INVERSE_SUBREL_LENGTH
static constexpr size_t READ_TAG_BOOLEAN_CHECK_SUBREL_LENGTH_ADJUSTMENT
static constexpr size_t INVERSE_SUBREL_LENGTH_ADJUSTMENT
static Accumulator get_read_selector(const AllEntities &in)
Compute scalar for read term in log derivative lookup argument.
static Accumulator compute_table_term(const AllEntities &in, const Parameters &params)
Compute write term denominator in log derivative lookup argument.
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 colu...
A wrapper for Relations to expose methods used by the Sumcheck prover or verifier to add the contribu...
Entry point for Barretenberg command-line interface.
Definition api.hpp:5
size_t calculate_num_threads(size_t num_iterations, size_t min_iterations_per_thread)
calculates number of threads to create based on minimum iterations per thread
Definition thread.cpp:233
void parallel_for(size_t num_iterations, const std::function< void(size_t)> &func)
Definition thread.cpp:111
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
auto range(size_t size, size_t offset=0) const
Definition thread.hpp:152
static void batch_invert(C &coeffs) noexcept
Batch invert a collection of field elements using Montgomery's trick.