Skip to content

Commit

Permalink
test(AVM): Negative unit tests for inter table relations (#5143)
Browse files Browse the repository at this point in the history 
Resolves #5033
  • Loading branch information
@jeanmon
jeanmon authored Mar 12, 2024
1 parent b2b0b93 commit a74dccb
Show file tree
Hide file tree
Showing 21 changed files with 702 additions and 336 deletions.
10 changes: 5 additions & 5 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
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

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
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
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

0 comments on commit a74dccb

Please sign in to comment.