Skip to content

Commit

Permalink
feat: pil lookups w/ xor table example (AztecProtocol#3880)
Browse files Browse the repository at this point in the history
depends on : https://github.com/AztecProtocol/powdr/pull/37/files

Lookups allow us to assert that values in a set of columns equal some
values in another set of columns.


This approach uses the log derivative method to perform lookups, where
the lookup relation requires four extra columns ( as well as the read
and write columns ) to function.
- One selector column to initiate adding a value into the READ side of
the lookup table ( lhs in pil )
- One selector column to initiate adding a value into the WRITE side of
the lookup table ( rhs in pil ) - { adding to the table }
- One selector column to compute inverses - ( helper column )
- One column to store the number of times a WRITE term is read - (
helper column )

The selector columns will need to be defined manually - as in the
`ToyAvm` example.
The inverse column and the counts columns are automatically included by
the code gen. ( this means there are two extra columns per lookup (
which is a little bit inefficient; but will do for now ).

The name of the inverse column is decided by the attribute tag
`#[attribute]` above the lookup - which is required.
The name of the counts column is `${attribute}_counts`. 

Note: that in the circuit builder you are currently required to set the
counts column value manually.

syntax:
```pil
  #[lookup_xor] // attribute
    q_xor { xor_a, xor_b, xor_c } in q_xor_table { table_xor_a, table_xor_b, table_xor_c };
    // lhs selector, lhs columns        // rhs selector, rhs columns

```

closes: AztecProtocol#2995


Co-authored-by: Rumata888 <[email protected]>

---------

Co-authored-by: Jean M <[email protected]>
  • Loading branch information
Maddiaa0 and jeanmon authored Jan 9, 2024
1 parent 537630f commit 544d24e
Show file tree
Hide file tree
Showing 16 changed files with 984 additions and 134 deletions.
34 changes: 31 additions & 3 deletions barretenberg/cpp/pil/avm/toy_avm.pil
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,36 @@ namespace toy(256);
q_tuple_set { set_1_column_1, set_1_column_2 } is { set_2_column_1, set_2_column_2 };

// Relation not used -> we currently require a single relation for codegen
pol commit x;
x' - x = 0;
q_tuple_set * (1 - q_tuple_set) = 0;

// Also needs a fixed relation
pol fixed first = [1] + [0]*;
pol fixed first = [1] + [0]*;

// Lookup related stuff

// For each xor term we need:
// - The witness wire it is over
// - The column being lookuped
// - A shift of the column being lookuped
// - An accumulator for each of the tables

// constraint wires
pol commit xor_a;
pol commit xor_b;
pol commit xor_c;

// Precomputed tables
pol commit table_xor_a;
pol commit table_xor_b;
pol commit table_xor_c;

pol commit q_xor;
pol commit q_xor_table;

q_xor * (1 - q_xor) = 0;
q_xor_table * (1 - q_xor_table) = 0;

// Note - if no right hand side selector column is provided, then we will need to build the table ourselves
// Note - we can also take advantage of pil creating the lookup columns for us here -> I may be able to do some codegen here !
#[lookup_xor]
q_xor { xor_a, xor_b, xor_c } in q_xor_table { table_xor_a, table_xor_b, table_xor_c };
Original file line number Diff line number Diff line change
Expand Up @@ -202,10 +202,10 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_tag_shift,
memTrace_m_rw_shift,
memTrace_m_tag_shift,
memTrace_m_addr_shift,
memTrace_m_val_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift)

Expand Down Expand Up @@ -251,10 +251,10 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_tag_shift,
memTrace_m_rw_shift,
memTrace_m_tag_shift,
memTrace_m_addr_shift,
memTrace_m_val_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift };
};
Expand Down Expand Up @@ -303,15 +303,15 @@ class AvmMiniFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_val, memTrace_m_addr, memTrace_m_tag, memTrace_m_rw, avmMini_internal_return_ptr,
return { memTrace_m_rw, memTrace_m_tag, memTrace_m_addr, memTrace_m_val, avmMini_internal_return_ptr,
avmMini_pc };
};
RefVector<DataType> get_shifted()
{
return { memTrace_m_val_shift,
memTrace_m_addr_shift,
return { memTrace_m_rw_shift,
memTrace_m_tag_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift,
memTrace_m_val_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift };
};
Expand All @@ -326,7 +326,7 @@ class AvmMiniFlavor {

RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_val, memTrace_m_addr, memTrace_m_tag, memTrace_m_rw, avmMini_internal_return_ptr,
return { memTrace_m_rw, memTrace_m_tag, memTrace_m_addr, memTrace_m_val, avmMini_internal_return_ptr,
avmMini_pc };
};

Expand Down Expand Up @@ -637,6 +637,4 @@ class AvmMiniFlavor {
};

} // namespace flavor

namespace sumcheck {}
} // namespace proof_system::honk
105 changes: 80 additions & 25 deletions barretenberg/cpp/src/barretenberg/flavor/generated/Toy_flavor.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,11 @@ class ToyFlavor {
using VerifierCommitmentKey = pcs::VerifierCommitmentKey<Curve>;

static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 1;
static constexpr size_t NUM_WITNESS_ENTITIES = 7;
static constexpr size_t NUM_WITNESS_ENTITIES = 16;
static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
// We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for
// the unshifted and one for the shifted
static constexpr size_t NUM_ALL_ENTITIES = 9;
static constexpr size_t NUM_ALL_ENTITIES = 17;

using Relations = std::tuple<Toy_vm::toy_avm<FF>, sumcheck::two_column_perm_relation<FF>>;

Expand Down Expand Up @@ -81,13 +81,24 @@ class ToyFlavor {
toy_set_1_column_2,
toy_set_2_column_1,
toy_set_2_column_2,
toy_x,
two_column_perm)
toy_xor_a,
toy_xor_b,
toy_xor_c,
toy_table_xor_a,
toy_table_xor_b,
toy_table_xor_c,
toy_q_xor,
toy_q_xor_table,
two_column_perm,
lookup_xor,
lookup_xor_counts)

RefVector<DataType> get_wires()
{
return { toy_q_tuple_set, toy_set_1_column_1, toy_set_1_column_2, toy_set_2_column_1, toy_set_2_column_2,
toy_x, two_column_perm };
return { toy_q_tuple_set, toy_set_1_column_1, toy_set_1_column_2, toy_set_2_column_1,
toy_set_2_column_2, toy_xor_a, toy_xor_b, toy_xor_c,
toy_table_xor_a, toy_table_xor_b, toy_table_xor_c, toy_q_xor,
toy_q_xor_table, two_column_perm, lookup_xor, lookup_xor_counts };
};
RefVector<DataType> get_sorted_polynomials() { return {}; };
};
Expand All @@ -101,22 +112,34 @@ class ToyFlavor {
toy_set_1_column_2,
toy_set_2_column_1,
toy_set_2_column_2,
toy_x,
toy_xor_a,
toy_xor_b,
toy_xor_c,
toy_table_xor_a,
toy_table_xor_b,
toy_table_xor_c,
toy_q_xor,
toy_q_xor_table,
two_column_perm,
toy_x_shift)
lookup_xor,
lookup_xor_counts)

RefVector<DataType> get_wires()
{
return { toy_first, toy_q_tuple_set, toy_set_1_column_1, toy_set_1_column_2, toy_set_2_column_1,
toy_set_2_column_2, toy_x, two_column_perm, toy_x_shift };
return { toy_first, toy_q_tuple_set, toy_set_1_column_1, toy_set_1_column_2, toy_set_2_column_1,
toy_set_2_column_2, toy_xor_a, toy_xor_b, toy_xor_c, toy_table_xor_a,
toy_table_xor_b, toy_table_xor_c, toy_q_xor, toy_q_xor_table, two_column_perm,
lookup_xor, lookup_xor_counts };
};
RefVector<DataType> get_unshifted()
{
return { toy_first, toy_q_tuple_set, toy_set_1_column_1, toy_set_1_column_2, toy_set_2_column_1,
toy_set_2_column_2, toy_x, two_column_perm };
return { toy_first, toy_q_tuple_set, toy_set_1_column_1, toy_set_1_column_2, toy_set_2_column_1,
toy_set_2_column_2, toy_xor_a, toy_xor_b, toy_xor_c, toy_table_xor_a,
toy_table_xor_b, toy_table_xor_c, toy_q_xor, toy_q_xor_table, two_column_perm,
lookup_xor, lookup_xor_counts };
};
RefVector<DataType> get_to_be_shifted() { return { toy_x }; };
RefVector<DataType> get_shifted() { return { toy_x_shift }; };
RefVector<DataType> get_to_be_shifted() { return {}; };
RefVector<DataType> get_shifted() { return {}; };
};

public:
Expand All @@ -126,7 +149,7 @@ class ToyFlavor {
using Base = ProvingKey_<PrecomputedEntities<Polynomial>, WitnessEntities<Polynomial>>;
using Base::Base;

RefVector<DataType> get_to_be_shifted() { return { toy_x }; };
RefVector<DataType> get_to_be_shifted() { return {}; };

// The plookup wires that store plookup read data.
std::array<PolynomialHandle, 0> get_table_column_wires() { return {}; };
Expand Down Expand Up @@ -169,6 +192,8 @@ class ToyFlavor {
}
};

using RowPolynomials = AllEntities<FF>;

class PartiallyEvaluatedMultivariates : public AllEntities<Polynomial> {
public:
PartiallyEvaluatedMultivariates() = default;
Expand Down Expand Up @@ -206,8 +231,17 @@ class ToyFlavor {
Base::toy_set_1_column_2 = "TOY_SET_1_COLUMN_2";
Base::toy_set_2_column_1 = "TOY_SET_2_COLUMN_1";
Base::toy_set_2_column_2 = "TOY_SET_2_COLUMN_2";
Base::toy_x = "TOY_X";
Base::toy_xor_a = "TOY_XOR_A";
Base::toy_xor_b = "TOY_XOR_B";
Base::toy_xor_c = "TOY_XOR_C";
Base::toy_table_xor_a = "TOY_TABLE_XOR_A";
Base::toy_table_xor_b = "TOY_TABLE_XOR_B";
Base::toy_table_xor_c = "TOY_TABLE_XOR_C";
Base::toy_q_xor = "TOY_Q_XOR";
Base::toy_q_xor_table = "TOY_Q_XOR_TABLE";
Base::two_column_perm = "TWO_COLUMN_PERM";
Base::lookup_xor = "LOOKUP_XOR";
Base::lookup_xor_counts = "LOOKUP_XOR_COUNTS";
};
};

Expand All @@ -231,8 +265,17 @@ class ToyFlavor {
Commitment toy_set_1_column_2;
Commitment toy_set_2_column_1;
Commitment toy_set_2_column_2;
Commitment toy_x;
Commitment toy_xor_a;
Commitment toy_xor_b;
Commitment toy_xor_c;
Commitment toy_table_xor_a;
Commitment toy_table_xor_b;
Commitment toy_table_xor_c;
Commitment toy_q_xor;
Commitment toy_q_xor_table;
Commitment two_column_perm;
Commitment lookup_xor;
Commitment lookup_xor_counts;

std::vector<barretenberg::Univariate<FF, BATCHED_RELATION_PARTIAL_LENGTH>> sumcheck_univariates;
std::array<FF, NUM_ALL_ENTITIES> sumcheck_evaluations;
Expand All @@ -257,8 +300,17 @@ class ToyFlavor {
toy_set_1_column_2 = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_set_2_column_1 = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_set_2_column_2 = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_x = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_xor_a = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_xor_b = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_xor_c = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_table_xor_a = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_table_xor_b = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_table_xor_c = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_q_xor = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
toy_q_xor_table = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
two_column_perm = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
lookup_xor = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
lookup_xor_counts = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);

for (size_t i = 0; i < log_n; ++i) {
sumcheck_univariates.emplace_back(
Expand Down Expand Up @@ -287,8 +339,17 @@ class ToyFlavor {
serialize_to_buffer<Commitment>(toy_set_1_column_2, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_set_2_column_1, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_set_2_column_2, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_x, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_xor_a, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_xor_b, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_xor_c, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_table_xor_a, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_table_xor_b, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_table_xor_c, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_q_xor, Transcript::proof_data);
serialize_to_buffer<Commitment>(toy_q_xor_table, Transcript::proof_data);
serialize_to_buffer<Commitment>(two_column_perm, Transcript::proof_data);
serialize_to_buffer<Commitment>(lookup_xor, Transcript::proof_data);
serialize_to_buffer<Commitment>(lookup_xor_counts, Transcript::proof_data);

for (size_t i = 0; i < log_n; ++i) {
serialize_to_buffer(sumcheck_univariates[i], Transcript::proof_data);
Expand All @@ -307,10 +368,4 @@ class ToyFlavor {
};

} // namespace flavor

namespace sumcheck {

DECLARE_SUMCHECK_RELATION_CLASS(two_column_perm, flavor::ToyFlavor);

}
} // namespace proof_system::honk
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ void compute_logderivative_inverse(Polynomials& polynomials, auto& relation_para
constexpr size_t WRITE_TERMS = Relation::WRITE_TERMS;

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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "barretenberg/honk/proof_system/logderivative_library.hpp"
#include "barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp"
#include "barretenberg/relations/generic_lookup/generic_lookup_relation.hpp"
#include "barretenberg/relations/generic_permutation/generic_permutation_relation.hpp"

#include "barretenberg/flavor/generated/AvmMini_flavor.hpp"
Expand Down Expand Up @@ -59,10 +60,10 @@ template <typename FF> struct AvmMiniFullRow {
FF avmMini_mem_idx_b{};
FF avmMini_mem_idx_c{};
FF avmMini_last{};
FF memTrace_m_val_shift{};
FF memTrace_m_addr_shift{};
FF memTrace_m_tag_shift{};
FF memTrace_m_rw_shift{};
FF memTrace_m_tag_shift{};
FF memTrace_m_addr_shift{};
FF memTrace_m_val_shift{};
FF avmMini_internal_return_ptr_shift{};
FF avmMini_pc_shift{};
};
Expand Down Expand Up @@ -136,10 +137,10 @@ class AvmMiniCircuitBuilder {
polys.avmMini_last[i] = rows[i].avmMini_last;
}

polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted());
polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted());
polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted());
polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted());
polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted());
polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted());
polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted());
polys.avmMini_internal_return_ptr_shift = Polynomial(polys.avmMini_internal_return_ptr.shifted());
polys.avmMini_pc_shift = Polynomial(polys.avmMini_pc.shifted());

Expand Down
Loading

0 comments on commit 544d24e

Please sign in to comment.