Skip to content

Commit

Permalink
4613 - remove constrain on intermediate registers set to zero in case of
Browse files Browse the repository at this point in the history 
     memory tag mismatch. Add unit tests. Adapt witness generation to
not add an antry in ALU table in case of memory tag mismatch.
  • Loading branch information
@jeanmon
jeanmon committed Mar 5, 2024
1 parent 0363b8e commit 02ae497
Show file tree
Hide file tree
Showing 9 changed files with 266 additions and 251 deletions.
5 changes: 0 additions & 5 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,11 +107,6 @@ namespace avm_main(256);

// TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6

// Set intermediate registers to 0 whenever tag_err occurs
tag_err * ia = 0;
tag_err * ib = 0;
tag_err * ic = 0;

// Relation for division over the finite field
// If tag_err == 1 in a division, then ib == 0 and op_err == 1.
#[SUBOP_DIVISION_FF]
Expand Down
112 changes: 56 additions & 56 deletions barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ class AvmFlavor {
static constexpr size_t NUM_ALL_ENTITIES = 90;

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

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

Expand Down Expand Up @@ -313,20 +313,20 @@ class AvmFlavor {
equiv_inter_reg_alu,
equiv_tag_err,
equiv_tag_err_counts,
avm_mem_m_addr_shift,
avm_mem_m_rw_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r7_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift)
avm_alu_alu_u16_r6_shift,
avm_mem_m_addr_shift,
avm_mem_m_rw_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift)

RefVector<DataType> get_wires()
{
Expand Down Expand Up @@ -406,20 +406,20 @@ class AvmFlavor {
equiv_inter_reg_alu,
equiv_tag_err,
equiv_tag_err_counts,
avm_mem_m_addr_shift,
avm_mem_m_rw_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r7_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift };
avm_alu_alu_u16_r6_shift,
avm_mem_m_addr_shift,
avm_mem_m_rw_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift };
};
RefVector<DataType> get_unshifted()
{
Expand Down Expand Up @@ -502,37 +502,37 @@ class AvmFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return { avm_mem_m_addr,
avm_mem_m_rw,
avm_mem_m_val,
avm_mem_m_tag,
return { avm_main_internal_return_ptr,
avm_main_pc,
avm_alu_alu_u16_r7,
avm_alu_alu_u16_r3,
avm_alu_alu_u16_r0,
avm_alu_alu_u16_r2,
avm_alu_alu_u16_r1,
avm_alu_alu_u16_r5,
avm_alu_alu_u16_r6,
avm_alu_alu_u16_r2,
avm_alu_alu_u16_r3,
avm_alu_alu_u16_r4,
avm_alu_alu_u16_r0,
avm_alu_alu_u16_r7,
avm_main_internal_return_ptr,
avm_main_pc };
avm_alu_alu_u16_r6,
avm_mem_m_addr,
avm_mem_m_rw,
avm_mem_m_val,
avm_mem_m_tag };
};
RefVector<DataType> get_shifted()
{
return { avm_mem_m_addr_shift,
avm_mem_m_rw_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift,
return { avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r1_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r7_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift };
avm_alu_alu_u16_r6_shift,
avm_mem_m_addr_shift,
avm_mem_m_rw_shift,
avm_mem_m_val_shift,
avm_mem_m_tag_shift };
};
};

Expand All @@ -545,20 +545,20 @@ class AvmFlavor {

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

// The plookup wires that store plookup read data.
Expand Down
48 changes: 24 additions & 24 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 @@ -97,20 +97,20 @@ template <typename FF> struct AvmFullRow {
FF equiv_inter_reg_alu{};
FF equiv_tag_err{};
FF equiv_tag_err_counts{};
FF avm_main_internal_return_ptr_shift{};
FF avm_main_pc_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_r2_shift{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_mem_m_addr_shift{};
FF avm_mem_m_rw_shift{};
FF avm_mem_m_val_shift{};
FF avm_mem_m_tag_shift{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_alu_alu_u16_r2_shift{};
FF avm_alu_alu_u16_r3_shift{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r0_shift{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_main_internal_return_ptr_shift{};
FF avm_main_pc_shift{};
};

class AvmCircuitBuilder {
Expand Down Expand Up @@ -218,20 +218,20 @@ class AvmCircuitBuilder {
polys.equiv_tag_err_counts[i] = rows[i].equiv_tag_err_counts;
}

polys.avm_main_internal_return_ptr_shift = Polynomial(polys.avm_main_internal_return_ptr.shifted());
polys.avm_main_pc_shift = Polynomial(polys.avm_main_pc.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_r2_shift = Polynomial(polys.avm_alu_alu_u16_r2.shifted());
polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.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_addr_shift = Polynomial(polys.avm_mem_m_addr.shifted());
polys.avm_mem_m_rw_shift = Polynomial(polys.avm_mem_m_rw.shifted());
polys.avm_mem_m_val_shift = Polynomial(polys.avm_mem_m_val.shifted());
polys.avm_mem_m_tag_shift = Polynomial(polys.avm_mem_m_tag.shifted());
polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted());
polys.avm_alu_alu_u16_r5_shift = Polynomial(polys.avm_alu_alu_u16_r5.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_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_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.shifted());
polys.avm_alu_alu_u16_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted());
polys.avm_main_internal_return_ptr_shift = Polynomial(polys.avm_main_internal_return_ptr.shifted());
polys.avm_main_pc_shift = Polynomial(polys.avm_main_pc.shifted());

return polys;
}
Expand Down Expand Up @@ -303,16 +303,16 @@ class AvmCircuitBuilder {
return true;
};

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_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_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;
}

Expand Down
80 changes: 40 additions & 40 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,42 +7,42 @@
namespace bb::Avm_vm {

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

inline std::string get_relation_label_avm_alu(int index)
Expand All @@ -54,29 +54,29 @@ inline std::string get_relation_label_avm_alu(int index)
case 11:
return "ALU_MUL_COMMON_2";

case 16:
return "ALU_OP_NOT";
case 14:
return "ALU_MULTIPLICATION_OUT_U128";

case 10:
return "ALU_MUL_COMMON_1";

case 9:
return "ALU_MULTIPLICATION_FF";

case 17:
return "ALU_RES_IS_BOOL";

case 18:
return "ALU_OP_EQ";

case 8:
return "ALU_ADD_SUB_2";

case 15:
return "ALU_FF_NOT_XOR";

case 8:
return "ALU_ADD_SUB_2";
case 17:
return "ALU_RES_IS_BOOL";

case 14:
return "ALU_MULTIPLICATION_OUT_U128";
case 9:
return "ALU_MULTIPLICATION_FF";

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

0 comments on commit 02ae497

Please sign in to comment.