Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Expand Up @@ -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);
Expand All @@ -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;
}
Expand Down Expand Up @@ -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;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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