Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Generic Lookup Relations for AVM #3774

Closed
wants to merge 12 commits into from
184 changes: 134 additions & 50 deletions barretenberg/cpp/src/barretenberg/flavor/toy_avm.hpp

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -52,6 +52,12 @@ template <typename Flavor> class ToyAVMCircuitBuilder {
const auto num_gates_log2 = static_cast<size_t>(numeric::get_msb64(num_gates));
size_t num_gates_pow2 = 1UL << (num_gates_log2 + (1UL << num_gates_log2 == num_gates ? 0 : 1));

// We need at least 256 values for the range constraint
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why is this? do we have precomputed columns that have a minimum size of 256?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's just that in this implementation we add a table from 0-255 in compute_polynomials. It is not relation-generic, just for this concrete example.

num_gates_pow2 = num_gates_pow2 > 256 ? num_gates_pow2 : 256;

// We need at least 256 values for the range constraint
num_gates_pow2 = num_gates_pow2 > 256 ? num_gates_pow2 : 256;

ProverPolynomials polys;
for (Polynomial& poly : polys.get_all()) {
poly = Polynomial(num_gates_pow2);
@@ -66,12 +72,62 @@ template <typename Flavor> class ToyAVMCircuitBuilder {
polys.permutation_set_column_3[i] = wires[2][i];
polys.permutation_set_column_4[i] = wires[3][i];
polys.self_permutation_column[i] = wires[4][i];

// By default the permutation is over all rows where we place data
polys.enable_tuple_set_permutation[i] = 1;
// The same column permutation alternates between even and odd values
polys.enable_single_column_permutation[i] = 1;
polys.enable_first_set_permutation[i] = i & 1;
polys.enable_second_set_permutation[i] = 1 - (i & 1);

// Lookup-based range constraint related values

// Store the value
polys.range_constrained_column[i] = wires[5][i];
// Make range constrained
polys.lookup_is_range_constrained[i] = 1;
uint256_t constrained_value = wires[5][i];
// if the value is correct, update the appropriate counter
if (constrained_value < 256) {
polys.lookup_range_constraint_read_count[static_cast<size_t>(constrained_value.data[0])] =
polys.lookup_range_constraint_read_count[static_cast<size_t>(constrained_value.data[0])] + 1;
}

// Copy xor values
polys.lookup_xor_argument_1[i] = wires[6][i];
polys.lookup_xor_argument_2[i] = wires[7][i];
polys.lookup_xor_result[i] = wires[8][i];
polys.lookup_xor_accumulated_argument_1[i] = wires[9][i];
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what do lookup_xor_accumulated_argument_1 and lookup_xor_accumulated_argument_2 represent?

How many columns are we adding per distinct lookup?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We are trying to prove that lookup_xor_accumulated_argument_1 ^ lookup_xor_accumulated_argument_2 = lookup_xor_accumulated_result. However they are 8-bit, so we decompose them. The top 4 bits of lookup_xor_accumulated_argument_1 will be in lookup_xor_argument_1.

For this particular case we added 6 columns for arguments. 2 3-element tuples.

polys.lookup_xor_accumulated_argument_2[i] = wires[10][i];
polys.lookup_xor_accumulated_result[i] = wires[11][i];
// Enable xor
polys.lookup_is_xor_operation[i] = 1;

// Calculate index of this xor table entry
uint256_t xor_index = wires[6][i] * 16 + wires[7][i];
// if the value is correct, update the appropriate counter
if (xor_index < 256) {
polys.lookup_xor_read_count[static_cast<size_t>(xor_index.data[0])] =
polys.lookup_xor_read_count[static_cast<size_t>(xor_index.data[0])] + 1;
}
xor_index = (uint256_t(wires[9][i]) & 0xf) * 16 + (uint256_t(wires[10][i]) & 0xf);
// if the value is correct, update the appropriate counter
if (xor_index < 256) {
polys.lookup_xor_read_count[static_cast<size_t>(xor_index.data[0])] =
polys.lookup_xor_read_count[static_cast<size_t>(xor_index.data[0])] + 1;
}
}
for (size_t i = 0; i < 256; i++) {
// Fill range table
polys.lookup_is_range_table_entry[i] = FF(1);
polys.lookup_range_table_entries[i] = FF(i);

// Fill xor table
polys.lookup_is_xor_table_entry[i] = FF(1);
polys.lookup_xor_table_1[i] = FF(i >> 4);
polys.lookup_xor_table_2[i] = FF(i % 16);
polys.lookup_xor_table_3[i] = FF((i >> 4) ^ (i % 16));
polys.lookup_xor_shift[i] = FF(16);
}
return polys;
}
@@ -147,6 +203,56 @@ template <typename Flavor> class ToyAVMCircuitBuilder {
return false;
}
}

// Check the range constraint relation
proof_system::honk::logderivative_library::compute_logderivative_inverse<
Flavor,
honk::sumcheck::GenericLookupRelation<honk::sumcheck::ExampleLookupBasedRangeConstraintSettings, FF>>(
polynomials, params, num_rows);

using LookupRelation =
honk::sumcheck::GenericLookupRelation<honk::sumcheck::ExampleLookupBasedRangeConstraintSettings, FF>;
typename honk::sumcheck::GenericLookupRelation<honk::sumcheck::ExampleLookupBasedRangeConstraintSettings,
typename Flavor::FF>::SumcheckArrayOfValuesOverSubrelations
range_constraint_result;
for (auto& r : range_constraint_result) {
r = 0;
}
for (size_t i = 0; i < num_rows; ++i) {
LookupRelation::accumulate(range_constraint_result, polynomials.get_row(i), params, 1);
}
for (auto r : range_constraint_result) {
if (r != 0) {
info("RangeConstraintRelation failed.");
return false;
}
}

// Check the xor relation
proof_system::honk::logderivative_library::compute_logderivative_inverse<
Flavor,
honk::sumcheck::GenericLookupRelation<honk::sumcheck::ExampleXorLookupConstraintSettings, FF>>(
polynomials, params, num_rows);

using XorLookupRelation =
honk::sumcheck::GenericLookupRelation<honk::sumcheck::ExampleXorLookupConstraintSettings, FF>;
typename honk::sumcheck::GenericLookupRelation<honk::sumcheck::ExampleXorLookupConstraintSettings,
typename Flavor::FF>::SumcheckArrayOfValuesOverSubrelations
xor_constraint_result;
for (auto& r : xor_constraint_result) {
r = 0;
}
for (size_t i = 0; i < num_rows; ++i) {

XorLookupRelation::accumulate(xor_constraint_result, polynomials.get_row(i), params, 1);
}
for (auto r : xor_constraint_result) {
if (r != 0) {
info("Xor Constraint failed.");
return false;
}
}

return true;
}

Original file line number Diff line number Diff line change
@@ -35,10 +35,28 @@ TEST(ToyAVMCircuitBuilder, BaseCase)
column_2.emplace_back(FF::random_element());
}

std::vector<std::pair<uint8_t, uint8_t>> xor_arguments;

// Get xor arguments
for (size_t i = 0; i < circuit_size; i++) {
xor_arguments.emplace_back(engine.get_random_uint8(), engine.get_random_uint8());
}
for (size_t i = 0; i < circuit_size; i++) {
// We put the same tuple of values in the first 2 wires and in the next 2 to at different rows
// We also put the same value in the self_permutation column in 2 consecutive rows
circuit_builder.add_row({ column_0[i], column_1[i], column_0[15 - i], column_1[15 - i], column_2[i / 2] });
uint8_t xor_result = std::get<0>(xor_arguments[i]) ^ std::get<1>(xor_arguments[i]);
circuit_builder.add_row({ column_0[i], // Tuple 1 element 1
column_1[i], // Tuple 1 element 2
column_0[15 - i], // Tuple 2 element 1
column_1[15 - i], // Tuple 2 element 2
column_2[i / 2], // Self-permutation column
engine.get_random_uint8(), // Range constrained column
std::get<0>(xor_arguments[i]) >> 4, // Xor columns
std::get<1>(xor_arguments[i]) >> 4,
xor_result >> 4,
std::get<0>(xor_arguments[i]),
std::get<1>(xor_arguments[i]),
xor_result });
}

// Test that permutations with correct values work
@@ -63,8 +81,51 @@ TEST(ToyAVMCircuitBuilder, BaseCase)
EXPECT_EQ(result, true);

// Break single-column permutation
circuit_builder.wires[circuit_builder.wires.size() - 1][0] = FF::random_element();
tmp = circuit_builder.wires[4][0];
circuit_builder.wires[4][0] = FF::random_element();
result = circuit_builder.check_circuit();
EXPECT_EQ(result, false);

// Restore value
circuit_builder.wires[4][0] = tmp;
// Check circuit passes
result = circuit_builder.check_circuit();
EXPECT_EQ(result, true);

// Break range constraint

circuit_builder.wires[5][0] = 257;
result = circuit_builder.check_circuit();
EXPECT_EQ(result, false);

// Restore range constraint

circuit_builder.wires[5][0] = 255;
result = circuit_builder.check_circuit();
EXPECT_EQ(result, true);

// Break xor constraint

circuit_builder.wires[6][0] = 0;
circuit_builder.wires[7][0] = 0;
circuit_builder.wires[8][0] = 1;
result = circuit_builder.check_circuit();
EXPECT_EQ(result, false);

// Break scaled xor constraint

circuit_builder.wires[6][0] = 0;
circuit_builder.wires[7][0] = 0;
circuit_builder.wires[8][0] = 0;
circuit_builder.wires[9][0] = 1;
circuit_builder.wires[10][0] = 1;
circuit_builder.wires[11][0] = 1;
result = circuit_builder.check_circuit();
EXPECT_EQ(result, false);

// Restore xor constraint
circuit_builder.wires[11][0] = 0;
result = circuit_builder.check_circuit();
EXPECT_EQ(result, true);
}
} // namespace toy_avm_circuit_builder_tests
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
#include "generic_lookup_relation.hpp"
#include "barretenberg/flavor/relation_definitions_fwd.hpp"
#include "barretenberg/flavor/toy_avm.hpp"
#include "barretenberg/honk/proof_system/logderivative_library.hpp"
#include "relation_definer.hpp"

namespace proof_system::honk::sumcheck {

/**
* @brief Expression for generic log-derivative-based set permutation.
* @param accumulator transformed to `evals + C(in(X)...)*scaling_factor`
* @param in an std::array containing the fully extended Accumulator edges.
* @param relation_params contains beta, gamma, and public_input_delta, ....
* @param scaling_factor optional term to scale the evaluation before adding to evals.
*/
template <typename Settings, typename FF>
template <typename ContainerOverSubrelations, typename AllEntities, typename Parameters>
void GenericLookupRelationImpl<Settings, FF>::accumulate(ContainerOverSubrelations& accumulator,
const AllEntities& in,
const Parameters& params,
const FF& scaling_factor)
{
logderivative_library::
accumulate_logderivative_lookup_subrelation_contributions<FF, GenericLookupRelationImpl<Settings, FF>>(
accumulator, in, params, scaling_factor);
}

DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS(GenericLookupRelationImpl, flavor::ToyAVM);
} // namespace proof_system::honk::sumcheck
Loading