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: Log-derivative based generic permutations for AVM #3428

Merged
merged 15 commits into from
Dec 7, 2023
4 changes: 2 additions & 2 deletions barretenberg/cpp/src/barretenberg/eccvm/eccvm_prover.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
#include "barretenberg/commitment_schemes/claim.hpp"
#include "barretenberg/commitment_schemes/commitment_key.hpp"
#include "barretenberg/common/ref_array.hpp"
#include "barretenberg/honk/proof_system/lookup_library.hpp"
#include "barretenberg/honk/proof_system/logderivative_library.hpp"
#include "barretenberg/honk/proof_system/permutation_library.hpp"
#include "barretenberg/honk/proof_system/power_polynomial.hpp"
#include "barretenberg/polynomials/polynomial.hpp"
Expand Down Expand Up @@ -183,7 +183,7 @@ template <ECCVMFlavor Flavor> void ECCVMProver_<Flavor>::execute_log_derivative_
gamma * (gamma + beta_sqr) * (gamma + beta_sqr + beta_sqr) * (gamma + beta_sqr + beta_sqr + beta_sqr);
relation_parameters.eccvm_set_permutation_delta = relation_parameters.eccvm_set_permutation_delta.invert();
// Compute inverse polynomial for our logarithmic-derivative lookup method
lookup_library::compute_logderivative_inverse<Flavor, typename Flavor::LookupRelation>(
logderivative_library::compute_logderivative_inverse<Flavor, typename Flavor::LookupRelation>(
prover_polynomials, relation_parameters, key->circuit_size);
transcript->send_to_verifier(commitment_labels.lookup_inverses, commitment_key->commit(key->lookup_inverses));
prover_polynomials.lookup_inverses = key->lookup_inverses;
Expand Down
376 changes: 376 additions & 0 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
@@ -1,7 +1,7 @@
#pragma once
#include <typeinfo>

namespace proof_system::honk::lookup_library {
namespace proof_system::honk::logderivative_library {

/**
* @brief Compute the inverse polynomial I(X) required for logderivative lookups
Expand Down Expand Up @@ -29,12 +29,12 @@ void compute_logderivative_inverse(Polynomials& polynomials, auto& relation_para
using Accumulator = typename Relation::ValueAccumulator0;
constexpr size_t READ_TERMS = Relation::READ_TERMS;
constexpr size_t WRITE_TERMS = Relation::WRITE_TERMS;
auto& inverse_polynomial = polynomials.lookup_inverses;

auto lookup_relation = Relation();
auto& inverse_polynomial = lookup_relation.template get_inverse_polynomial(polynomials);
for (size_t i = 0; i < circuit_size; ++i) {
auto row = polynomials.get_row(i);
bool has_inverse = lookup_relation.lookup_exists_at_row(row);
bool has_inverse = lookup_relation.operation_exists_at_row(row);
if (!has_inverse) {
continue;
}
Expand Down Expand Up @@ -97,7 +97,7 @@ void accumulate_logderivative_lookup_subrelation_contributions(ContainerOverSubr
using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>;
using View = typename Accumulator::View;

auto lookup_inverses = View(in.lookup_inverses);
auto lookup_inverses = View(lookup_relation.template get_inverse_polynomial(in));

constexpr size_t NUM_TOTAL_TERMS = READ_TERMS + WRITE_TERMS;
std::array<Accumulator, NUM_TOTAL_TERMS> lookup_terms;
Expand Down Expand Up @@ -153,4 +153,98 @@ void accumulate_logderivative_lookup_subrelation_contributions(ContainerOverSubr
});
}

} // namespace proof_system::honk::lookup_library
/**
* @brief Compute generic log-derivative set permutation subrelation accumulation
* @details The generic log-derivative lookup relation consistes of two subrelations. The first demonstrates that the
* inverse polynomial I, defined via I = 1/[(read_term) * (write_term)], has been computed correctly. The second
* establishes the correctness of the permutation itself based on the log-derivative argument. Note that the
* latter subrelation 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. The subrelation expressions are
* respectively:
*
* I * (read_term) * (write_term) - q_{permutation_enabler} = 0
*
* \sum_{i=0}^{n-1} [q_{write_enabler} * I * write_term + q_{read_enabler} * I * read_term] = 0
*
* The explicit expressions for read_term and write_term are dependent upon the particular structure of the permutation
* being performed and methods for computing them must be defined in the corresponding relation class. The entities
* which are used to determine the use of permutation (is it enabled, is the first "read" set enabled, is the second
* "write" set enabled) must be defined in the relation class.
*
* @tparam FF
* @tparam Relation
* @tparam ContainerOverSubrelations
* @tparam AllEntities
* @tparam Parameters
* @param accumulator
* @param in
* @param params
* @param scaling_factor
*/
template <typename FF, typename Relation, typename ContainerOverSubrelations, typename AllEntities, typename Parameters>
void accumulate_logderivative_permutation_subrelation_contributions(ContainerOverSubrelations& accumulator,
const AllEntities& in,
const Parameters& params,
const FF& scaling_factor)
{
constexpr size_t READ_TERMS = Relation::READ_TERMS;
constexpr size_t WRITE_TERMS = Relation::WRITE_TERMS;

// For now we only do simple permutations over tuples with 1 read and 1 write term
Copy link
Contributor

Choose a reason for hiding this comment

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

Could you make an issue to change this? I suspect we'll need to have more exotic lookups to fully support the AVM

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is just for permutations

static_assert(READ_TERMS == 1);
static_assert(WRITE_TERMS == 1);

auto permutation_relation = Relation();

using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>;
using View = typename Accumulator::View;

auto permutation_inverses = View(permutation_relation.template get_inverse_polynomial(in));

constexpr size_t NUM_TOTAL_TERMS = 2;
std::array<Accumulator, NUM_TOTAL_TERMS> permutation_terms;
std::array<Accumulator, NUM_TOTAL_TERMS> denominator_accumulator;

// The permutation relation = 1 / read_term - 1 / write_term
// To get the inverses (1 / read_term), (1 / write_term), we have a commitment to the product ofinver ses
// i.e. permutation_inverses = (1 / read_term) * (1 / write_term)
// The purpose of this next section is to derive individual inverse terms using `permutation_inverses`
// i.e. (1 / read_term) = permutation_inverses * write_term
// (1 / write_term) = permutation_inverses * read_term
permutation_terms[0] = permutation_relation.template compute_read_term<Accumulator, 0>(in, params);
permutation_terms[1] = permutation_relation.template compute_write_term<Accumulator, 0>(in, params);

barretenberg::constexpr_for<0, NUM_TOTAL_TERMS, 1>(
[&]<size_t i>() { denominator_accumulator[i] = permutation_terms[i]; });

barretenberg::constexpr_for<0, NUM_TOTAL_TERMS - 1, 1>(
[&]<size_t i>() { denominator_accumulator[i + 1] *= denominator_accumulator[i]; });

auto inverse_accumulator = Accumulator(permutation_inverses); // denominator_accumulator[NUM_TOTAL_TERMS - 1];

const auto inverse_exists = permutation_relation.template compute_inverse_exists<Accumulator>(in);

// Note: the lookup_inverses are computed so that the value is 0 if !inverse_exists
std::get<0>(accumulator) +=
(denominator_accumulator[NUM_TOTAL_TERMS - 1] * permutation_inverses - inverse_exists) * scaling_factor;

// After this algo, total degree of denominator_accumulator = NUM_TOTAL_TERMS
for (size_t i = 0; i < NUM_TOTAL_TERMS - 1; ++i) {
denominator_accumulator[NUM_TOTAL_TERMS - 1 - i] =
denominator_accumulator[NUM_TOTAL_TERMS - 2 - i] * inverse_accumulator;
inverse_accumulator = inverse_accumulator * permutation_terms[NUM_TOTAL_TERMS - 1 - i];
}
denominator_accumulator[0] = inverse_accumulator;

// each predicate is degree-1
// degree of relation at this point = NUM_TOTAL_TERMS + 1
std::get<1>(accumulator) +=
permutation_relation.template compute_read_term_predicate<Accumulator, 0>(in) * denominator_accumulator[0];

// each predicate is degree-1
// degree of relation = NUM_TOTAL_TERMS + 1
std::get<1>(accumulator) -=
permutation_relation.template compute_write_term_predicate<Accumulator, 0>(in) * denominator_accumulator[1];
}
} // namespace proof_system::honk::logderivative_library
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "barretenberg/ecc/curves/grumpkin/grumpkin.hpp"
#include "barretenberg/flavor/ecc_vm.hpp"
#include "barretenberg/honk/proof_system/lookup_library.hpp"
#include "barretenberg/honk/proof_system/logderivative_library.hpp"
#include "barretenberg/honk/proof_system/permutation_library.hpp"
#include "barretenberg/proof_system/op_queue/ecc_op_queue.hpp"
#include "barretenberg/relations/relation_parameters.hpp"
Expand Down Expand Up @@ -505,9 +505,9 @@ template <typename Flavor> class ECCVMCircuitBuilder {

auto polynomials = compute_polynomials();
const size_t num_rows = polynomials.get_polynomial_size();
proof_system::honk::lookup_library::compute_logderivative_inverse<Flavor,
honk::sumcheck::ECCVMLookupRelation<FF>>(
polynomials, params, num_rows);
proof_system::honk::logderivative_library::
compute_logderivative_inverse<Flavor, honk::sumcheck::ECCVMLookupRelation<FF>>(
polynomials, params, num_rows);

honk::permutation_library::compute_permutation_grand_product<Flavor, honk::sumcheck::ECCVMSetRelation<FF>>(
num_rows, polynomials, params);
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,163 @@
/**
* @file avm_template_circuit_builder.hpp
* @author Rumata888
* @brief A circuit builder for the AVM toy version used to showcase permutation and lookup mechanisms for PIL
*
*/
#pragma once

#include "barretenberg/common/constexpr_utils.hpp"
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "barretenberg/flavor/toy_avm.hpp"
#include "barretenberg/honk/proof_system/logderivative_library.hpp"
#include "barretenberg/relations/relation_parameters.hpp"
#include "barretenberg/relations/toy_avm/generic_permutation_relation.hpp"

namespace proof_system {

/**
* @brief Circuit builder for the ToyAVM that is used to explain generic permutation settings
*
* @tparam Flavor
*/
template <typename Flavor> class ToyAVMCircuitBuilder {
public:
using FF = typename Flavor::FF;
using Polynomial = typename Flavor::Polynomial;

static constexpr size_t NUM_POLYNOMIALS = Flavor::NUM_ALL_ENTITIES;
static constexpr size_t NUM_WIRES = Flavor::NUM_WIRES;

using AllPolynomials = typename Flavor::AllPolynomials;
size_t num_gates = 0;
std::array<std::vector<FF>, NUM_WIRES> wires;
ToyAVMCircuitBuilder() = default;

void add_row(const std::array<FF, NUM_WIRES> row)
{
for (size_t i = 0; i < NUM_WIRES; i++) {
wires[i].emplace_back(row[i]);
}
num_gates = wires[0].size();
}

/**
* @brief Compute the AVM Template flavor polynomial data required to generate a proof
*
* @return AllPolynomials
*/
AllPolynomials compute_polynomials()
{

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));

AllPolynomials polys;
for (auto& poly : polys.get_all()) {
poly = Polynomial(num_gates_pow2);
}

polys.lagrange_first[0] = 1;

for (size_t i = 0; i < num_gates; ++i) {
// Fill out the witness polynomials
polys.permutation_set_column_1[i] = wires[0][i];
polys.permutation_set_column_2[i] = wires[1][i];
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);
}
return polys;
}

/**
* @brief Check that the circuit is correct (proof should work)
*
*/
bool check_circuit()
{
// using FirstPermutationRelation = typename std::tuple_element_t<0, Flavor::Relations>;
// For now only gamma and beta are used
const FF gamma = FF::random_element();
const FF beta = FF::random_element();
proof_system::RelationParameters<typename Flavor::FF> params{
.eta = 0,
.beta = beta,
.gamma = gamma,
.public_input_delta = 0,
.lookup_grand_product_delta = 0,
.beta_sqr = 0,
.beta_cube = 0,
.eccvm_set_permutation_delta = 0,
};

// Compute polynomial values
auto polynomials = compute_polynomials();
const size_t num_rows = polynomials.get_polynomial_size();

// Check the tuple permutation relation
proof_system::honk::logderivative_library::compute_logderivative_inverse<
Flavor,
honk::sumcheck::GenericPermutationRelation<honk::sumcheck::ExampleTuplePermutationSettings, FF>>(
polynomials, params, num_rows);

using PermutationRelation =
honk::sumcheck::GenericPermutationRelation<honk::sumcheck::ExampleTuplePermutationSettings, FF>;
typename honk::sumcheck::GenericPermutationRelation<honk::sumcheck::ExampleTuplePermutationSettings,
typename Flavor::FF>::SumcheckArrayOfValuesOverSubrelations
permutation_result;
for (auto& r : permutation_result) {
r = 0;
}
for (size_t i = 0; i < num_rows; ++i) {
PermutationRelation::accumulate(permutation_result, polynomials.get_row(i), params, 1);
}
for (auto r : permutation_result) {
if (r != 0) {
info("Tuple GenericPermutationRelation failed.");
return false;
}
}
// Check the single permutation relation
proof_system::honk::logderivative_library::compute_logderivative_inverse<
Flavor,
honk::sumcheck::GenericPermutationRelation<honk::sumcheck::ExampleSameWirePermutationSettings, FF>>(
polynomials, params, num_rows);

using SameWirePermutationRelation =
honk::sumcheck::GenericPermutationRelation<honk::sumcheck::ExampleSameWirePermutationSettings, FF>;
typename honk::sumcheck::GenericPermutationRelation<honk::sumcheck::ExampleSameWirePermutationSettings,
typename Flavor::FF>::SumcheckArrayOfValuesOverSubrelations
second_permutation_result;
for (auto& r : second_permutation_result) {
r = 0;
}
for (size_t i = 0; i < num_rows; ++i) {
SameWirePermutationRelation::accumulate(second_permutation_result, polynomials.get_row(i), params, 1);
}
for (auto r : second_permutation_result) {
if (r != 0) {
info("Same wire GenericPermutationRelation failed.");
return false;
}
}
return true;
}

[[nodiscard]] size_t get_num_gates() const { return num_gates; }

[[nodiscard]] size_t get_circuit_subgroup_size(const size_t num_rows) const
{

const auto num_rows_log2 = static_cast<size_t>(numeric::get_msb64(num_rows));
size_t num_rows_pow2 = 1UL << (num_rows_log2 + (1UL << num_rows_log2 == num_rows ? 0 : 1));
return num_rows_pow2;
}
};
} // namespace proof_system
Loading