Skip to content

Commit

Permalink
feat(avm): enable main -> mem clk lookups (#4591)
Browse files Browse the repository at this point in the history 
Enables lookup for tag err, adds test case for permutation check with
two selectors.
Edits the permutation check active constraint to be active when either
lhs / rhs are active, rather than a third selector.

Co-authored-by: jeanmon <[email protected]>
  • Loading branch information
@Maddiaa0 @jeanmon
Maddiaa0 and jeanmon authored Feb 14, 2024
1 parent f5592b8 commit 0e503c1
Show file tree
Hide file tree
Showing 26 changed files with 1,019 additions and 244 deletions.
4 changes: 3 additions & 1 deletion barretenberg/cpp/pil/avm/avm_main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,8 @@ namespace avm_main(256);

// Inter-table Constraints

// TODO: tag_err {clk} IS avm_mem.m_tag_err {avm_mem.m_clk}
#[equiv_tag_err]
avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk};

// TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}
19 changes: 17 additions & 2 deletions barretenberg/cpp/pil/avm/toy_avm.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,18 @@ namespace toy(256);
pol commit set_2_column_1;
pol commit set_2_column_2;

// This is a column based tuple lookup
// This is a column based tuple lookup, one selector
#[two_column_perm] // the name of the inverse
q_tuple_set { set_1_column_1, set_1_column_2 } is { set_2_column_1, set_2_column_2 };


// Column based lookup, two selectors
pol commit sparse_column_1, sparse_column_2;
pol commit sparse_lhs, sparse_rhs;

#[two_column_sparse_perm] // the name of the inverse
sparse_lhs { sparse_column_1 } is sparse_rhs { sparse_column_2 };

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

Expand Down Expand Up @@ -45,4 +53,11 @@ namespace toy(256);
// 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 };
q_xor { xor_a, xor_b, xor_c } in q_xor_table { table_xor_a, table_xor_b, table_xor_c };

// Minimum repro testing multiple lookups
pol commit q_err, q_err_check;
pol commit clk, m_clk;

#[lookup_err]
q_err_check {m_clk} in q_err {clk};
129 changes: 63 additions & 66 deletions barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,13 +37,13 @@ class AvmFlavor {
using RelationSeparator = FF;

static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2;
static constexpr size_t NUM_WITNESS_ENTITIES = 69;
static constexpr size_t NUM_WITNESS_ENTITIES = 71;
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 = 85;
static constexpr size_t NUM_ALL_ENTITIES = 87;

using Relations = std::tuple<Avm_vm::avm_mem<FF>, Avm_vm::avm_main<FF>, Avm_vm::avm_alu<FF>>;
using Relations = std::tuple<Avm_vm::avm_mem<FF>, Avm_vm::avm_alu<FF>, Avm_vm::avm_main<FF>>;

static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length<Relations>();

Expand Down Expand Up @@ -145,7 +145,9 @@ class AvmFlavor {
avm_main_mem_idx_a,
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last)
avm_main_last,
equiv_tag_err,
equiv_tag_err_counts)

RefVector<DataType> get_wires()
{
Expand Down Expand Up @@ -217,7 +219,9 @@ class AvmFlavor {
avm_main_mem_idx_a,
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last };
avm_main_last,
equiv_tag_err,
equiv_tag_err_counts };
};
RefVector<DataType> get_sorted_polynomials() { return {}; };
};
Expand Down Expand Up @@ -296,20 +300,22 @@ class AvmFlavor {
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last,
equiv_tag_err,
equiv_tag_err_counts,
avm_mem_m_rw_shift,
avm_mem_m_tag_shift,
avm_mem_m_val_shift,
avm_mem_m_addr_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r0_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r4_shift)
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r3_shift,
avm_main_pc_shift,
avm_main_internal_return_ptr_shift)

RefVector<DataType> get_wires()
{
Expand Down Expand Up @@ -384,20 +390,22 @@ class AvmFlavor {
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last,
equiv_tag_err,
equiv_tag_err_counts,
avm_mem_m_rw_shift,
avm_mem_m_tag_shift,
avm_mem_m_val_shift,
avm_mem_m_addr_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r0_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r4_shift };
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r3_shift,
avm_main_pc_shift,
avm_main_internal_return_ptr_shift };
};
RefVector<DataType> get_unshifted()
{
Expand Down Expand Up @@ -471,41 +479,29 @@ class AvmFlavor {
avm_main_mem_idx_a,
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last };
avm_main_last,
equiv_tag_err,
equiv_tag_err_counts };
};
RefVector<DataType> get_to_be_shifted()
{
return { avm_mem_m_rw,
avm_mem_m_tag,
avm_mem_m_val,
avm_mem_m_addr,
avm_main_internal_return_ptr,
avm_main_pc,
avm_alu_alu_u16_r6,
avm_alu_alu_u16_r0,
avm_alu_alu_u16_r2,
avm_alu_alu_u16_r7,
avm_alu_alu_u16_r3,
avm_alu_alu_u16_r1,
avm_alu_alu_u16_r5,
avm_alu_alu_u16_r4 };
return { avm_mem_m_rw, avm_mem_m_addr,
avm_mem_m_val, avm_mem_m_tag,
avm_alu_alu_u16_r2, avm_alu_alu_u16_r1,
avm_alu_alu_u16_r5, avm_alu_alu_u16_r0,
avm_alu_alu_u16_r7, avm_alu_alu_u16_r6,
avm_alu_alu_u16_r4, avm_alu_alu_u16_r3,
avm_main_pc, avm_main_internal_return_ptr };
};
RefVector<DataType> get_shifted()
{
return { avm_mem_m_rw_shift,
avm_mem_m_tag_shift,
avm_mem_m_val_shift,
avm_mem_m_addr_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r4_shift };
return { avm_mem_m_rw_shift, avm_mem_m_addr_shift,
avm_mem_m_val_shift, avm_mem_m_tag_shift,
avm_alu_alu_u16_r2_shift, avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift, avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r7_shift, avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r4_shift, avm_alu_alu_u16_r3_shift,
avm_main_pc_shift, avm_main_internal_return_ptr_shift };
};
};

Expand All @@ -518,20 +514,13 @@ class AvmFlavor {

RefVector<DataType> get_to_be_shifted()
{
return { avm_mem_m_rw,
avm_mem_m_tag,
avm_mem_m_val,
avm_mem_m_addr,
avm_main_internal_return_ptr,
avm_main_pc,
avm_alu_alu_u16_r6,
avm_alu_alu_u16_r0,
avm_alu_alu_u16_r2,
avm_alu_alu_u16_r7,
avm_alu_alu_u16_r3,
avm_alu_alu_u16_r1,
avm_alu_alu_u16_r5,
avm_alu_alu_u16_r4 };
return { avm_mem_m_rw, avm_mem_m_addr,
avm_mem_m_val, avm_mem_m_tag,
avm_alu_alu_u16_r2, avm_alu_alu_u16_r1,
avm_alu_alu_u16_r5, avm_alu_alu_u16_r0,
avm_alu_alu_u16_r7, avm_alu_alu_u16_r6,
avm_alu_alu_u16_r4, avm_alu_alu_u16_r3,
avm_main_pc, avm_main_internal_return_ptr };
};

// The plookup wires that store plookup read data.
Expand Down Expand Up @@ -679,6 +668,8 @@ class AvmFlavor {
Base::avm_main_mem_idx_b = "AVM_MAIN_MEM_IDX_B";
Base::avm_main_mem_idx_c = "AVM_MAIN_MEM_IDX_C";
Base::avm_main_last = "AVM_MAIN_LAST";
Base::equiv_tag_err = "EQUIV_TAG_ERR";
Base::equiv_tag_err_counts = "EQUIV_TAG_ERR_COUNTS";
};
};

Expand Down Expand Up @@ -767,6 +758,8 @@ class AvmFlavor {
Commitment avm_main_mem_idx_b;
Commitment avm_main_mem_idx_c;
Commitment avm_main_last;
Commitment equiv_tag_err;
Commitment equiv_tag_err_counts;

std::vector<bb::Univariate<FF, BATCHED_RELATION_PARTIAL_LENGTH>> sumcheck_univariates;
std::array<FF, NUM_ALL_ENTITIES> sumcheck_evaluations;
Expand Down Expand Up @@ -855,6 +848,8 @@ class AvmFlavor {
avm_main_mem_idx_b = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
avm_main_mem_idx_c = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
avm_main_last = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
equiv_tag_err = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);
equiv_tag_err_counts = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_frs_read);

for (size_t i = 0; i < log_n; ++i) {
sumcheck_univariates.emplace_back(
Expand Down Expand Up @@ -947,6 +942,8 @@ class AvmFlavor {
serialize_to_buffer<Commitment>(avm_main_mem_idx_b, Transcript::proof_data);
serialize_to_buffer<Commitment>(avm_main_mem_idx_c, Transcript::proof_data);
serialize_to_buffer<Commitment>(avm_main_last, Transcript::proof_data);
serialize_to_buffer<Commitment>(equiv_tag_err, Transcript::proof_data);
serialize_to_buffer<Commitment>(equiv_tag_err_counts, Transcript::proof_data);

for (size_t i = 0; i < log_n; ++i) {
serialize_to_buffer(sumcheck_univariates[i], Transcript::proof_data);
Expand Down
Loading

0 comments on commit 0e503c1

Please sign in to comment.