Skip to content

Commit

Permalink
feat: Log-derivative based generic permutations for AVM (AztecProtoco…
Browse files Browse the repository at this point in the history
…l#3428)

Introduces a relation for constructing generic permutations that needs
to be templated for PIL for AVM.
Renames lookup_library to logderivative_library
  • Loading branch information
Rumata888 authored Dec 7, 2023
1 parent 080230c commit 379b5ad
Show file tree
Hide file tree
Showing 15 changed files with 1,201 additions and 24 deletions.
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
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

0 comments on commit 379b5ad

Please sign in to comment.