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.

Sign up for GitHub

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

Jump to bottom

test(AVM): Negative unit tests for inter table relations #5143

Merged
merged 5 commits into from
Mar 12, 2024
Merged

test(AVM): Negative unit tests for inter table relations #5143

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
719f508
5033 - rename permutation and inclusion checks
jeanmon Mar 7, 2024
6b5f1a2
5033 - refactoring and cleaning up some namespaces use
jeanmon Mar 8, 2024
393cf05
5033 - unit tests for the permutation between ALU and MAIN
jeanmon Mar 8, 2024
d521918
5033 - add negative unit test on not copying the error tag to the main
jeanmon Mar 11, 2024
3e6a78b
5033 - other inter table negative unit tests
jeanmon Mar 11, 2024
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
10 changes: 5 additions & 5 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,15 +190,15 @@ namespace avm_main(256);

// Inter-table Constraints

#[equiv_tag_err]
#[INCL_MAIN_TAG_ERR]
avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk};

// Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1,
// the operation is not copied to the ALU table.
// TODO: when division is moved to the alu, we will need to add the selector in the list below:
alu_sel = (sel_op_add + sel_op_sub + sel_op_mul + sel_op_not + sel_op_eq) * (1 - tag_err);

#[equiv_inter_reg_alu]
#[PERM_MAIN_ALU]
alu_sel {clk, ia, ib, ic,
sel_op_add, sel_op_sub, sel_op_mul, sel_op_eq,
sel_op_not, in_tag}
Expand All @@ -207,17 +207,17 @@ namespace avm_main(256);
avm_alu.alu_op_add, avm_alu.alu_op_sub, avm_alu.alu_op_mul, avm_alu.alu_op_eq,
avm_alu.alu_op_not, avm_alu.alu_in_tag};

#[equiv_main_mem_a]
#[PERM_MAIN_MEM_A]
mem_op_a {clk, mem_idx_a, ia, rwa, in_tag}
is
avm_mem.m_op_a {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag};

#[equiv_main_mem_b]
#[PERM_MAIN_MEM_B]
mem_op_b {clk, mem_idx_b, ib, rwb, in_tag}
is
avm_mem.m_op_b {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag};

#[equiv_main_mem_c]
#[PERM_MAIN_MEM_C]
mem_op_c {clk, mem_idx_c, ic, rwc, in_tag}
is
avm_mem.m_op_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag};
214 changes: 107 additions & 107 deletions barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp
View file
Open in desktop

Large diffs are not rendered by default.

98 changes: 49 additions & 49 deletions ...nberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/avm_circuit_builder.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@
#include "barretenberg/relations/generated/avm/avm_alu.hpp"
#include "barretenberg/relations/generated/avm/avm_main.hpp"
#include "barretenberg/relations/generated/avm/avm_mem.hpp"
#include "barretenberg/relations/generated/avm/equiv_inter_reg_alu.hpp"
#include "barretenberg/relations/generated/avm/equiv_main_mem_a.hpp"
#include "barretenberg/relations/generated/avm/equiv_main_mem_b.hpp"
#include "barretenberg/relations/generated/avm/equiv_main_mem_c.hpp"
#include "barretenberg/relations/generated/avm/equiv_tag_err.hpp"
#include "barretenberg/relations/generated/avm/incl_main_tag_err.hpp"
#include "barretenberg/relations/generated/avm/perm_main_alu.hpp"
#include "barretenberg/relations/generated/avm/perm_main_mem_a.hpp"
#include "barretenberg/relations/generated/avm/perm_main_mem_b.hpp"
#include "barretenberg/relations/generated/avm/perm_main_mem_c.hpp"

namespace bb {

Expand Down Expand Up @@ -101,26 +101,26 @@ template <typename FF> struct AvmFullRow {
FF avm_main_mem_idx_b{};
FF avm_main_mem_idx_c{};
FF avm_main_last{};
FF equiv_inter_reg_alu{};
FF equiv_main_mem_a{};
FF equiv_main_mem_b{};
FF equiv_main_mem_c{};
FF equiv_tag_err{};
FF equiv_tag_err_counts{};
FF avm_main_pc_shift{};
FF avm_main_internal_return_ptr_shift{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_alu_alu_u16_r3_shift{};
FF avm_alu_alu_u16_r0_shift{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_u16_r2_shift{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF perm_main_alu{};
FF perm_main_mem_a{};
FF perm_main_mem_b{};
FF perm_main_mem_c{};
FF incl_main_tag_err{};
FF incl_main_tag_err_counts{};
FF avm_mem_m_tag_shift{};
FF avm_mem_m_addr_shift{};
FF avm_mem_m_val_shift{};
FF avm_mem_m_rw_shift{};
FF avm_mem_m_addr_shift{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_u16_r3_shift{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_u16_r0_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_alu_alu_u16_r2_shift{};
FF avm_main_pc_shift{};
FF avm_main_internal_return_ptr_shift{};
};

class AvmCircuitBuilder {
Expand Down Expand Up @@ -227,28 +227,28 @@ class AvmCircuitBuilder {
polys.avm_main_mem_idx_b[i] = rows[i].avm_main_mem_idx_b;
polys.avm_main_mem_idx_c[i] = rows[i].avm_main_mem_idx_c;
polys.avm_main_last[i] = rows[i].avm_main_last;
polys.equiv_inter_reg_alu[i] = rows[i].equiv_inter_reg_alu;
polys.equiv_main_mem_a[i] = rows[i].equiv_main_mem_a;
polys.equiv_main_mem_b[i] = rows[i].equiv_main_mem_b;
polys.equiv_main_mem_c[i] = rows[i].equiv_main_mem_c;
polys.equiv_tag_err[i] = rows[i].equiv_tag_err;
polys.equiv_tag_err_counts[i] = rows[i].equiv_tag_err_counts;
polys.perm_main_alu[i] = rows[i].perm_main_alu;
polys.perm_main_mem_a[i] = rows[i].perm_main_mem_a;
polys.perm_main_mem_b[i] = rows[i].perm_main_mem_b;
polys.perm_main_mem_c[i] = rows[i].perm_main_mem_c;
polys.incl_main_tag_err[i] = rows[i].incl_main_tag_err;
polys.incl_main_tag_err_counts[i] = rows[i].incl_main_tag_err_counts;
}

polys.avm_main_pc_shift = Polynomial(polys.avm_main_pc.shifted());
polys.avm_main_internal_return_ptr_shift = Polynomial(polys.avm_main_internal_return_ptr.shifted());
polys.avm_alu_alu_u16_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted());
polys.avm_alu_alu_u16_r3_shift = Polynomial(polys.avm_alu_alu_u16_r3.shifted());
polys.avm_alu_alu_u16_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.shifted());
polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted());
polys.avm_alu_alu_u16_r2_shift = Polynomial(polys.avm_alu_alu_u16_r2.shifted());
polys.avm_alu_alu_u16_r5_shift = Polynomial(polys.avm_alu_alu_u16_r5.shifted());
polys.avm_alu_alu_u16_r4_shift = Polynomial(polys.avm_alu_alu_u16_r4.shifted());
polys.avm_alu_alu_u16_r6_shift = Polynomial(polys.avm_alu_alu_u16_r6.shifted());
polys.avm_mem_m_tag_shift = Polynomial(polys.avm_mem_m_tag.shifted());
polys.avm_mem_m_addr_shift = Polynomial(polys.avm_mem_m_addr.shifted());
polys.avm_mem_m_val_shift = Polynomial(polys.avm_mem_m_val.shifted());
polys.avm_mem_m_rw_shift = Polynomial(polys.avm_mem_m_rw.shifted());
polys.avm_mem_m_addr_shift = Polynomial(polys.avm_mem_m_addr.shifted());
polys.avm_alu_alu_u16_r5_shift = Polynomial(polys.avm_alu_alu_u16_r5.shifted());
polys.avm_alu_alu_u16_r3_shift = Polynomial(polys.avm_alu_alu_u16_r3.shifted());
polys.avm_alu_alu_u16_r4_shift = Polynomial(polys.avm_alu_alu_u16_r4.shifted());
polys.avm_alu_alu_u16_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted());
polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted());
polys.avm_alu_alu_u16_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.shifted());
polys.avm_alu_alu_u16_r6_shift = Polynomial(polys.avm_alu_alu_u16_r6.shifted());
polys.avm_alu_alu_u16_r2_shift = Polynomial(polys.avm_alu_alu_u16_r2.shifted());
polys.avm_main_pc_shift = Polynomial(polys.avm_main_pc.shifted());
polys.avm_main_internal_return_ptr_shift = Polynomial(polys.avm_main_internal_return_ptr.shifted());

return polys;
}
Expand Down Expand Up @@ -313,39 +313,39 @@ class AvmCircuitBuilder {
}
for (auto r : lookup_result) {
if (r != 0) {
info("Lookup ", lookup_name, " failed.");
throw_or_abort(format("Lookup ", lookup_name, " failed."));
return false;
}
}
return true;
};

if (!evaluate_relation.template operator()<Avm_vm::avm_main<FF>>("avm_main",
Avm_vm::get_relation_label_avm_main)) {
if (!evaluate_relation.template operator()<Avm_vm::avm_mem<FF>>("avm_mem",
Avm_vm::get_relation_label_avm_mem)) {
return false;
}
if (!evaluate_relation.template operator()<Avm_vm::avm_alu<FF>>("avm_alu",
Avm_vm::get_relation_label_avm_alu)) {
return false;
}
if (!evaluate_relation.template operator()<Avm_vm::avm_mem<FF>>("avm_mem",
Avm_vm::get_relation_label_avm_mem)) {
if (!evaluate_relation.template operator()<Avm_vm::avm_main<FF>>("avm_main",
Avm_vm::get_relation_label_avm_main)) {
return false;
}

if (!evaluate_logderivative.template operator()<equiv_inter_reg_alu_relation<FF>>("equiv_inter_reg_alu")) {
if (!evaluate_logderivative.template operator()<perm_main_alu_relation<FF>>("PERM_MAIN_ALU")) {
return false;
}
if (!evaluate_logderivative.template operator()<equiv_main_mem_a_relation<FF>>("equiv_main_mem_a")) {
if (!evaluate_logderivative.template operator()<perm_main_mem_a_relation<FF>>("PERM_MAIN_MEM_A")) {
return false;
}
if (!evaluate_logderivative.template operator()<equiv_main_mem_b_relation<FF>>("equiv_main_mem_b")) {
if (!evaluate_logderivative.template operator()<perm_main_mem_b_relation<FF>>("PERM_MAIN_MEM_B")) {
return false;
}
if (!evaluate_logderivative.template operator()<equiv_main_mem_c_relation<FF>>("equiv_main_mem_c")) {
if (!evaluate_logderivative.template operator()<perm_main_mem_c_relation<FF>>("PERM_MAIN_MEM_C")) {
return false;
}
if (!evaluate_logderivative.template operator()<equiv_tag_err_relation<FF>>("equiv_tag_err")) {
if (!evaluate_logderivative.template operator()<incl_main_tag_err_relation<FF>>("INCL_MAIN_TAG_ERR")) {
return false;
}

Expand Down
74 changes: 37 additions & 37 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,57 +7,48 @@
namespace bb::Avm_vm {

template <typename FF> struct Avm_aluRow {
FF avm_alu_alu_op_eq{};
FF avm_alu_alu_u16_r5{};
FF avm_alu_alu_op_sub{};
FF avm_alu_alu_ff_tag{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_u16_r4{};
FF avm_alu_alu_ib{};
FF avm_alu_alu_u64_r0{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_alu_alu_op_eq{};
FF avm_alu_alu_u16_r7{};
FF avm_alu_alu_u8_tag{};
FF avm_alu_alu_cf{};
FF avm_alu_alu_u16_r2{};
FF avm_alu_alu_u16_r3_shift{};
FF avm_alu_alu_u16_r0_shift{};
FF avm_alu_alu_u64_r0{};
FF avm_alu_alu_ia{};
FF avm_alu_alu_u32_tag{};
FF avm_alu_alu_op_not{};
FF avm_alu_alu_op_mul{};
FF avm_alu_alu_sel{};
FF avm_alu_alu_u64_tag{};
FF avm_alu_alu_in_tag{};
FF avm_alu_alu_u16_r1{};
FF avm_alu_alu_u16_r3{};
FF avm_alu_alu_u16_r5{};
FF avm_alu_alu_u16_r2{};
FF avm_alu_alu_u128_tag{};
FF avm_alu_alu_u16_r0{};
FF avm_alu_alu_sel{};
FF avm_alu_alu_ff_tag{};
FF avm_alu_alu_op_eq_diff_inv{};
FF avm_alu_alu_ic{};
FF avm_alu_alu_op_mul{};
FF avm_alu_alu_cf{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r6{};
FF avm_alu_alu_ib{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_alu_alu_op_add{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_u16_r2_shift{};
FF avm_alu_alu_ic{};
FF avm_alu_alu_u8_r0{};
FF avm_alu_alu_op_not{};
FF avm_alu_alu_u16_tag{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_op_add{};
FF avm_alu_alu_u16_r0{};
FF avm_alu_alu_u16_r7{};
FF avm_alu_alu_u128_tag{};
FF avm_alu_alu_op_eq_diff_inv{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r1{};
FF avm_alu_alu_u16_r0_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_alu_alu_u64_tag{};
FF avm_alu_alu_u8_r1{};
FF avm_alu_alu_u16_r3{};
FF avm_alu_alu_u16_r2_shift{};
};

inline std::string get_relation_label_avm_alu(int index)
{
switch (index) {
case 10:
return "ALU_ADD_SUB_2";

case 12:
return "ALU_MUL_COMMON_1";

case 13:
return "ALU_MUL_COMMON_2";

case 18:
return "ALU_OP_NOT";

Expand All @@ -67,17 +58,26 @@ inline std::string get_relation_label_avm_alu(int index)
case 9:
return "ALU_ADD_SUB_1";

case 17:
return "ALU_FF_NOT_XOR";
case 10:
return "ALU_ADD_SUB_2";

case 16:
return "ALU_MULTIPLICATION_OUT_U128";
case 13:
return "ALU_MUL_COMMON_2";

case 20:
return "ALU_OP_EQ";

case 17:
return "ALU_FF_NOT_XOR";

case 11:
return "ALU_MULTIPLICATION_FF";

case 12:
return "ALU_MUL_COMMON_1";

case 16:
return "ALU_MULTIPLICATION_OUT_U128";
}
return std::to_string(index);
}
Expand Down
Loading
Loading