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(avm): sequential lookup resolution and example #11769

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
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
3 changes: 3 additions & 0 deletions barretenberg/cpp/pil/vm2/alu.pil
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
namespace alu;

// Trace selector.
pol commit sel;

pol commit sel_op_add;
pol commit ia;
pol commit ib;
Expand Down
11 changes: 9 additions & 2 deletions barretenberg/cpp/pil/vm2/execution.pil
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@ pol commit last;
sel * (1 - sel) = 0;
last * (1 - last) = 0;

// Opcode selectors
pol commit sel_alu;

// If the current row is an execution row, then either
// the next row is an execution row, or the current row is marked as the last row.
// sel => (sel' v last) = 1 iff
Expand All @@ -46,12 +49,16 @@ sel * (1 - sel') * (1 - last) = 0;
#[LAST_IS_LAST]
last * sel' = 0;

// This is just an example of a sequential dynamic lookup.
// TODO: This might actually be a permutation, it depends.
// FIXME: This does not have all it needs.
#[LOOKUP_EXEC_ALU]
sel_alu {op1, op2, op3} in alu.sel {alu.ia_addr, alu.ib_addr, alu.dst_addr};

// These are needed to have a non-empty set of columns for each type.
pol public input;
#[LOOKUP_DUMMY_PRECOMPUTED]
sel {/*will be 1=OR*/ sel, clk, clk, clk} in
precomputed.sel_bitwise {precomputed.bitwise_op_id, precomputed.bitwise_input_a, precomputed.bitwise_input_b, precomputed.bitwise_output};
#[LOOKUP_DUMMY_DYNAMIC] // Just a self-lookup for now, for testing.
sel {op1, op2, op3, op4} in sel {op1, op2, op3, op4};
#[PERM_DUMMY_DYNAMIC] // Just a self-permutation for now, for testing.
sel {op1, op2, op3, op4} is sel {op1, op2, op3, op4};
8 changes: 4 additions & 4 deletions barretenberg/cpp/src/barretenberg/vm2/generated/columns.hpp

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions barretenberg/cpp/src/barretenberg/vm2/generated/flavor.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -76,12 +76,12 @@ class AvmFlavor {
static constexpr bool HasZK = false;

static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 16;
static constexpr size_t NUM_WITNESS_ENTITIES = 382;
static constexpr size_t NUM_WITNESS_ENTITIES = 384;
static constexpr size_t NUM_SHIFTED_ENTITIES = 68;
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 = 466;
static constexpr size_t NUM_ALL_ENTITIES = 468;

// Need to be templated for recursive verifier
template <typename FF_>
Expand All @@ -105,8 +105,8 @@ class AvmFlavor {
lookup_bitw_byte_lengths_relation<FF_>,
lookup_bitw_byte_operations_relation<FF_>,
lookup_bytecode_to_read_unary_relation<FF_>,
lookup_dummy_dynamic_relation<FF_>,
lookup_dummy_precomputed_relation<FF_>,
lookup_exec_alu_relation<FF_>,
lookup_rng_chk_diff_relation<FF_>,
lookup_rng_chk_is_r0_16_bit_relation<FF_>,
lookup_rng_chk_is_r1_16_bit_relation<FF_>,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,45 +10,44 @@

namespace bb::avm2 {

/////////////////// lookup_dummy_precomputed ///////////////////
/////////////////// lookup_exec_alu ///////////////////

class lookup_dummy_precomputed_lookup_settings {
class lookup_exec_alu_lookup_settings {
public:
static constexpr std::string_view NAME = "LOOKUP_DUMMY_PRECOMPUTED";
static constexpr std::string_view NAME = "LOOKUP_EXEC_ALU";

static constexpr size_t READ_TERMS = 1;
static constexpr size_t WRITE_TERMS = 1;
static constexpr size_t READ_TERM_TYPES[READ_TERMS] = { 0 };
static constexpr size_t WRITE_TERM_TYPES[WRITE_TERMS] = { 0 };
static constexpr size_t LOOKUP_TUPLE_SIZE = 4;
static constexpr size_t LOOKUP_TUPLE_SIZE = 3;
static constexpr size_t INVERSE_EXISTS_POLYNOMIAL_DEGREE = 4;
static constexpr size_t READ_TERM_DEGREE = 0;
static constexpr size_t WRITE_TERM_DEGREE = 0;

// Columns using the Column enum.
static constexpr Column SRC_SELECTOR = Column::execution_sel;
static constexpr Column DST_SELECTOR = Column::precomputed_sel_bitwise;
static constexpr Column COUNTS = Column::lookup_dummy_precomputed_counts;
static constexpr Column INVERSES = Column::lookup_dummy_precomputed_inv;
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> SRC_COLUMNS = {
Column::execution_sel, Column::execution_clk, Column::execution_clk, Column::execution_clk
};
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> DST_COLUMNS = { Column::precomputed_bitwise_op_id,
Column::precomputed_bitwise_input_a,
Column::precomputed_bitwise_input_b,
Column::precomputed_bitwise_output };
static constexpr Column SRC_SELECTOR = Column::execution_sel_alu;
static constexpr Column DST_SELECTOR = Column::alu_sel;
static constexpr Column COUNTS = Column::lookup_exec_alu_counts;
static constexpr Column INVERSES = Column::lookup_exec_alu_inv;
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> SRC_COLUMNS = { Column::execution_op1,
Column::execution_op2,
Column::execution_op3 };
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> DST_COLUMNS = { Column::alu_ia_addr,
Column::alu_ib_addr,
Column::alu_dst_addr };

template <typename AllEntities> static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in)
{
return (in._execution_sel() == 1 || in._precomputed_sel_bitwise() == 1);
return (in._execution_sel_alu() == 1 || in._alu_sel() == 1);
}

template <typename Accumulator, typename AllEntities>
static inline auto compute_inverse_exists(const AllEntities& in)
{
using View = typename Accumulator::View;
const auto is_operation = View(in._execution_sel());
const auto is_table_entry = View(in._precomputed_sel_bitwise());
const auto is_operation = View(in._execution_sel_alu());
const auto is_table_entry = View(in._alu_sel());
return (is_operation + is_table_entry - is_operation * is_table_entry);
}

Expand All @@ -64,33 +63,31 @@ class lookup_dummy_precomputed_lookup_settings {

template <typename AllEntities> static inline auto get_entities(AllEntities&& in)
{
return std::forward_as_tuple(in._lookup_dummy_precomputed_inv(),
in._lookup_dummy_precomputed_counts(),
in._execution_sel(),
in._precomputed_sel_bitwise(),
in._execution_sel(),
in._execution_clk(),
in._execution_clk(),
in._execution_clk(),
in._precomputed_bitwise_op_id(),
in._precomputed_bitwise_input_a(),
in._precomputed_bitwise_input_b(),
in._precomputed_bitwise_output());
return std::forward_as_tuple(in._lookup_exec_alu_inv(),
in._lookup_exec_alu_counts(),
in._execution_sel_alu(),
in._alu_sel(),
in._execution_op1(),
in._execution_op2(),
in._execution_op3(),
in._alu_ia_addr(),
in._alu_ib_addr(),
in._alu_dst_addr());
}
};

template <typename FF_>
class lookup_dummy_precomputed_relation : public GenericLookupRelation<lookup_dummy_precomputed_lookup_settings, FF_> {
class lookup_exec_alu_relation : public GenericLookupRelation<lookup_exec_alu_lookup_settings, FF_> {
public:
static constexpr std::string_view NAME = lookup_dummy_precomputed_lookup_settings::NAME;
static constexpr std::string_view NAME = lookup_exec_alu_lookup_settings::NAME;
};
template <typename FF_> using lookup_dummy_precomputed = GenericLookup<lookup_dummy_precomputed_lookup_settings, FF_>;
template <typename FF_> using lookup_exec_alu = GenericLookup<lookup_exec_alu_lookup_settings, FF_>;

/////////////////// lookup_dummy_dynamic ///////////////////
/////////////////// lookup_dummy_precomputed ///////////////////

class lookup_dummy_dynamic_lookup_settings {
class lookup_dummy_precomputed_lookup_settings {
public:
static constexpr std::string_view NAME = "LOOKUP_DUMMY_DYNAMIC";
static constexpr std::string_view NAME = "LOOKUP_DUMMY_PRECOMPUTED";

static constexpr size_t READ_TERMS = 1;
static constexpr size_t WRITE_TERMS = 1;
Expand All @@ -103,27 +100,28 @@ class lookup_dummy_dynamic_lookup_settings {

// Columns using the Column enum.
static constexpr Column SRC_SELECTOR = Column::execution_sel;
static constexpr Column DST_SELECTOR = Column::execution_sel;
static constexpr Column COUNTS = Column::lookup_dummy_dynamic_counts;
static constexpr Column INVERSES = Column::lookup_dummy_dynamic_inv;
static constexpr Column DST_SELECTOR = Column::precomputed_sel_bitwise;
static constexpr Column COUNTS = Column::lookup_dummy_precomputed_counts;
static constexpr Column INVERSES = Column::lookup_dummy_precomputed_inv;
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> SRC_COLUMNS = {
Column::execution_op1, Column::execution_op2, Column::execution_op3, Column::execution_op4
};
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> DST_COLUMNS = {
Column::execution_op1, Column::execution_op2, Column::execution_op3, Column::execution_op4
Column::execution_sel, Column::execution_clk, Column::execution_clk, Column::execution_clk
};
static constexpr std::array<Column, LOOKUP_TUPLE_SIZE> DST_COLUMNS = { Column::precomputed_bitwise_op_id,
Column::precomputed_bitwise_input_a,
Column::precomputed_bitwise_input_b,
Column::precomputed_bitwise_output };

template <typename AllEntities> static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in)
{
return (in._execution_sel() == 1 || in._execution_sel() == 1);
return (in._execution_sel() == 1 || in._precomputed_sel_bitwise() == 1);
}

template <typename Accumulator, typename AllEntities>
static inline auto compute_inverse_exists(const AllEntities& in)
{
using View = typename Accumulator::View;
const auto is_operation = View(in._execution_sel());
const auto is_table_entry = View(in._execution_sel());
const auto is_table_entry = View(in._precomputed_sel_bitwise());
return (is_operation + is_table_entry - is_operation * is_table_entry);
}

Expand All @@ -139,26 +137,26 @@ class lookup_dummy_dynamic_lookup_settings {

template <typename AllEntities> static inline auto get_entities(AllEntities&& in)
{
return std::forward_as_tuple(in._lookup_dummy_dynamic_inv(),
in._lookup_dummy_dynamic_counts(),
return std::forward_as_tuple(in._lookup_dummy_precomputed_inv(),
in._lookup_dummy_precomputed_counts(),
in._execution_sel(),
in._precomputed_sel_bitwise(),
in._execution_sel(),
in._execution_op1(),
in._execution_op2(),
in._execution_op3(),
in._execution_op4(),
in._execution_op1(),
in._execution_op2(),
in._execution_op3(),
in._execution_op4());
in._execution_clk(),
in._execution_clk(),
in._execution_clk(),
in._precomputed_bitwise_op_id(),
in._precomputed_bitwise_input_a(),
in._precomputed_bitwise_input_b(),
in._precomputed_bitwise_output());
}
};

template <typename FF_>
class lookup_dummy_dynamic_relation : public GenericLookupRelation<lookup_dummy_dynamic_lookup_settings, FF_> {
class lookup_dummy_precomputed_relation : public GenericLookupRelation<lookup_dummy_precomputed_lookup_settings, FF_> {
public:
static constexpr std::string_view NAME = lookup_dummy_dynamic_lookup_settings::NAME;
static constexpr std::string_view NAME = lookup_dummy_precomputed_lookup_settings::NAME;
};
template <typename FF_> using lookup_dummy_dynamic = GenericLookup<lookup_dummy_dynamic_lookup_settings, FF_>;
template <typename FF_> using lookup_dummy_precomputed = GenericLookup<lookup_dummy_precomputed_lookup_settings, FF_>;

} // namespace bb::avm2
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ void AluTraceBuilder::process(const simulation::EventEmitterInterface<simulation

trace.set(row,
{ {
{ C::alu_sel, 1 },
{ opcode_selector, 1 },
{ C::alu_op, static_cast<uint8_t>(event.operation) },
{ C::alu_ia, event.a },
Expand Down
15 changes: 15 additions & 0 deletions barretenberg/cpp/src/barretenberg/vm2/tracegen/execution_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@

#include "barretenberg/common/log.hpp"
#include "barretenberg/common/zip_view.hpp"
#include "barretenberg/vm2/common/opcodes.hpp"
#include "barretenberg/vm2/simulation/events/addressing_event.hpp"
#include "barretenberg/vm2/simulation/events/event_emitter.hpp"
#include "barretenberg/vm2/simulation/events/execution_event.hpp"
Expand All @@ -17,6 +18,19 @@ namespace {

constexpr size_t operand_columns = 4;

Column get_operation_selector(ExecutionOpCode operation)
{
switch (operation) {
case ExecutionOpCode::ADD:
return Column::execution_sel_alu;
default:
// TODO: Complete and remove this.
return Column::execution_sel;
// throw std::runtime_error("Unknown ALU operation");
break;
}
}

} // namespace

void ExecutionTraceBuilder::process(
Expand Down Expand Up @@ -47,6 +61,7 @@ void ExecutionTraceBuilder::process(
{ C::execution_sel, 1 }, // active execution trace
{ C::execution_clk, row }, // TODO: we may want this in the event
{ C::execution_ex_opcode, static_cast<size_t>(ex_event.opcode) },
{ get_operation_selector(ex_event.opcode), 1 },
{ C::execution_op1, static_cast<FF>(operands.at(0)) },
{ C::execution_op2, static_cast<FF>(operands.at(1)) },
{ C::execution_op3, static_cast<FF>(operands.at(2)) },
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include <array>
#include <bit>
#include <cstddef>
#include <cstdint>
#include <stdexcept>

#include "barretenberg/vm2/common/field.hpp"
Expand Down Expand Up @@ -54,9 +55,12 @@ template <typename LookupSettings_> class BaseLookupTraceBuilder : public Intera
// This class is used when the lookup is into a non-precomputed table.
// It calculates the counts by trying to find the tuple in the destination columns.
// It creates an index of the destination columns on init, and uses it to find the tuple efficiently.
template <typename LookupSettings_> class LookupIntoDynamicTable : public BaseLookupTraceBuilder<LookupSettings_> {
// This class should work for any lookup that is not precomputed.
// However, consider using a more specialized and faster class.
template <typename LookupSettings_>
class LookupIntoDynamicTableGeneric : public BaseLookupTraceBuilder<LookupSettings_> {
public:
virtual ~LookupIntoDynamicTable() = default;
virtual ~LookupIntoDynamicTableGeneric() = default;

protected:
using LookupSettings = LookupSettings_;
Expand Down Expand Up @@ -89,6 +93,57 @@ template <typename LookupSettings_> class LookupIntoDynamicTable : public BaseLo
unordered_flat_map<ArrayTuple, uint32_t> row_idx;
};

// This class is used when the lookup is into a non-precomputed table.
// It is optimized for the case when the source and destination tuples
// are expected to be in the same order (possibly with other tuples in the middle
// in the destination table).
// The approach is that for a given source row, you start sequentially looking at the
// destination rows until you find a match. Then you move to the next source row.
// Then you keep looking from the last destination row you found a match.
// WARNING: Do not use this class if you expect to "reuse" destination rows.
// In this case the two tables will likely not be in order.
template <typename LookupSettings> class LookupIntoDynamicTableSequential : public InteractionBuilderInterface {
public:
~LookupIntoDynamicTableSequential() override = default;

void process(TraceContainer& trace) override
{
uint32_t dst_row = 0;
uint32_t max_dst_row = trace.get_column_rows(LookupSettings::DST_SELECTOR);

trace.visit_column(LookupSettings::SRC_SELECTOR, [&](uint32_t row, const FF& src_sel_value) {
assert(src_sel_value == 1);
(void)src_sel_value; // Avoid GCC complaining of unused parameter when asserts are disabled.

auto src_values = trace.get_multiple(LookupSettings::SRC_COLUMNS, row);

// We set a dummy value in the inverse column so that the size of the column is right.
// The correct value will be set by the prover.
trace.set(LookupSettings::INVERSES, row, 0xdeadbeef);

// We find the first row in the destination columns where the values match.
while (dst_row < max_dst_row) {
// TODO: As an optimization, we could try to only walk the rows where the selector is active.
// We can't just do a visit because we cannot skip rows with that.
auto dst_selector = trace.get(LookupSettings::DST_SELECTOR, dst_row);
if (dst_selector == 1 && src_values == trace.get_multiple(LookupSettings::DST_COLUMNS, dst_row)) {
trace.set(LookupSettings::COUNTS, dst_row, trace.get(LookupSettings::COUNTS, dst_row) + 1);
return; // Done with this source row.
}
++dst_row;
}

throw std::runtime_error("Failed computing counts for " + std::string(LookupSettings::NAME) +
". Could not find tuple in destination.");
});

// We set a dummy value in the inverse column so that the size of the column is right.
// The correct value will be set by the prover.
trace.visit_column(LookupSettings::DST_SELECTOR,
[&](uint32_t row, const FF&) { trace.set(LookupSettings::INVERSES, row, 0xdeadbeef); });
}
};

} // namespace bb::avm2::tracegen

// Define a hash function for std::array so that it can be used as a key in a std::unordered_map.
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/src/barretenberg/vm2/tracegen_helper.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ TraceContainer AvmTraceGenHelper::generate_trace(EventsContainer&& events)
{
auto jobs_interactions = make_jobs<std::unique_ptr<InteractionBuilderInterface>>(
std::make_unique<LookupIntoBitwise<lookup_dummy_precomputed_lookup_settings>>(),
std::make_unique<LookupIntoDynamicTable<lookup_dummy_dynamic_lookup_settings>>(),
std::make_unique<LookupIntoDynamicTableSequential<lookup_exec_alu_lookup_settings>>(),
std::make_unique<PermutationBuilder<perm_dummy_dynamic_permutation_settings>>(),
std::make_unique<LookupIntoIndexedByClk<lookup_rng_chk_diff_lookup_settings>>(),
std::make_unique<LookupIntoIndexedByClk<lookup_rng_chk_pow_2_lookup_settings>>(),
Expand Down
Loading