Skip to content

Commit

Permalink
fix: address comments
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed Feb 14, 2024
1 parent 8378489 commit 6ea5658
Show file tree
Hide file tree
Showing 9 changed files with 194 additions and 190 deletions.
16 changes: 10 additions & 6 deletions barretenberg/cpp/pil/avm/avm_alu.pil
Original file line number Diff line number Diff line change
Expand Up @@ -225,14 +225,18 @@ namespace avm_alu(256);
alu_op_not * (alu_ia + alu_ic - UINT_MAX) = 0;

// ========= EQUALITY Operation Constraints ===============================
// TODO: Note this method differs from the approach taken for "equality to zero" checks
// in handling the error tags found in avm_main and avm_mem files. The predicted relation difference
// is minor and when we optimise we will harmonise the methods based on actual performance.

// Equality of two elements is found by performing an "equality to zero" check.
// This relies on the fact than the inverse of a field element exists for all elements except zero
// 1) Given two values a & b, find the difference c = a - b
// 2) If a & b are equal, c == 0 otherwise c != 0
// This relies on the fact that the inverse of a field element exists for all elements except zero
// 1) Given two values x & y, find the difference z = x - y
// 2) If x & y are equal, z == 0 otherwise z != 0
// 3) Field equality to zero can be done as follows
// a) c(e(1 - y) + y) - 1 + e = 0;
// b) where y = c^-1 and e is a boolean value indicating if c == 0
// c) if e == 0; cy = 1 && c has an inverse. if e ==1; c = 0 and we set c_inv = 0;
// a) z(e(x - w) + w) - 1 + e = 0;
// b) where w = z^-1 and e is a boolean value indicating if z == 0
// c) if e == 0; zw = 1 && z has an inverse. If e == 1; z == 0 and we set w = 0;

// Registers Ia and Ib hold the values that equality is to be tested on
pol DIFF = alu_ia - alu_ib;
Expand Down
87 changes: 30 additions & 57 deletions barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ class AvmFlavor {
// the unshifted and one for the shifted
static constexpr size_t NUM_ALL_ENTITIES = 85;

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

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

Expand Down Expand Up @@ -296,19 +296,19 @@ class AvmFlavor {
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r1_shift,
avm_mem_m_val_shift,
avm_mem_m_rw_shift,
avm_alu_alu_u16_r6_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_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 @@ -384,19 +384,19 @@ class AvmFlavor {
avm_main_mem_idx_b,
avm_main_mem_idx_c,
avm_main_last,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r1_shift,
avm_mem_m_val_shift,
avm_mem_m_rw_shift,
avm_alu_alu_u16_r6_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_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 @@ -475,37 +475,19 @@ class AvmFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return { avm_main_internal_return_ptr,
avm_main_pc,
avm_alu_alu_u16_r2,
avm_alu_alu_u16_r6,
avm_alu_alu_u16_r7,
avm_alu_alu_u16_r4,
avm_alu_alu_u16_r5,
avm_alu_alu_u16_r3,
avm_alu_alu_u16_r0,
avm_alu_alu_u16_r1,
avm_mem_m_val,
avm_mem_m_rw,
avm_mem_m_addr,
avm_mem_m_tag };
return { avm_alu_alu_u16_r2, avm_alu_alu_u16_r7, avm_alu_alu_u16_r3,
avm_alu_alu_u16_r4, avm_alu_alu_u16_r0, avm_alu_alu_u16_r5,
avm_alu_alu_u16_r1, avm_alu_alu_u16_r6, avm_main_internal_return_ptr,
avm_main_pc, avm_mem_m_addr, avm_mem_m_rw,
avm_mem_m_val, avm_mem_m_tag };
};
RefVector<DataType> get_shifted()
{
return { avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_alu_alu_u16_r2_shift,
avm_alu_alu_u16_r6_shift,
avm_alu_alu_u16_r7_shift,
avm_alu_alu_u16_r4_shift,
avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r0_shift,
avm_alu_alu_u16_r1_shift,
avm_mem_m_val_shift,
avm_mem_m_rw_shift,
avm_mem_m_addr_shift,
avm_mem_m_tag_shift };
return { avm_alu_alu_u16_r2_shift, avm_alu_alu_u16_r7_shift, avm_alu_alu_u16_r3_shift,
avm_alu_alu_u16_r4_shift, avm_alu_alu_u16_r0_shift, avm_alu_alu_u16_r5_shift,
avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r6_shift, avm_main_internal_return_ptr_shift,
avm_main_pc_shift, avm_mem_m_addr_shift, avm_mem_m_rw_shift,
avm_mem_m_val_shift, avm_mem_m_tag_shift };
};
};

Expand All @@ -518,20 +500,11 @@ class AvmFlavor {

RefVector<DataType> get_to_be_shifted()
{
return { avm_main_internal_return_ptr,
avm_main_pc,
avm_alu_alu_u16_r2,
avm_alu_alu_u16_r6,
avm_alu_alu_u16_r7,
avm_alu_alu_u16_r4,
avm_alu_alu_u16_r5,
avm_alu_alu_u16_r3,
avm_alu_alu_u16_r0,
avm_alu_alu_u16_r1,
avm_mem_m_val,
avm_mem_m_rw,
avm_mem_m_addr,
avm_mem_m_tag };
return { avm_alu_alu_u16_r2, avm_alu_alu_u16_r7, avm_alu_alu_u16_r3,
avm_alu_alu_u16_r4, avm_alu_alu_u16_r0, avm_alu_alu_u16_r5,
avm_alu_alu_u16_r1, avm_alu_alu_u16_r6, avm_main_internal_return_ptr,
avm_main_pc, 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
Original file line number Diff line number Diff line change
Expand Up @@ -90,19 +90,19 @@ template <typename FF> struct AvmFullRow {
FF avm_main_mem_idx_b{};
FF avm_main_mem_idx_c{};
FF avm_main_last{};
FF avm_main_internal_return_ptr_shift{};
FF avm_main_pc_shift{};
FF avm_alu_alu_u16_r2_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_alu_alu_u16_r4_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_r0_shift{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_mem_m_val_shift{};
FF avm_mem_m_rw_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_main_internal_return_ptr_shift{};
FF avm_main_pc_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{};
};

Expand Down Expand Up @@ -206,19 +206,19 @@ class AvmCircuitBuilder {
polys.avm_main_last[i] = rows[i].avm_main_last;
}

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_r2_shift = Polynomial(polys.avm_alu_alu_u16_r2.shifted());
polys.avm_alu_alu_u16_r6_shift = Polynomial(polys.avm_alu_alu_u16_r6.shifted());
polys.avm_alu_alu_u16_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted());
polys.avm_alu_alu_u16_r4_shift = Polynomial(polys.avm_alu_alu_u16_r4.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_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.shifted());
polys.avm_alu_alu_u16_r5_shift = Polynomial(polys.avm_alu_alu_u16_r5.shifted());
polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.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_alu_alu_u16_r6_shift = Polynomial(polys.avm_alu_alu_u16_r6.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());
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());

return polys;
Expand Down Expand Up @@ -257,14 +257,14 @@ class AvmCircuitBuilder {
return true;
};

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)) {
return false;
}
if (!evaluate_relation.template operator()<Avm_vm::avm_mem<FF>>("avm_mem",
Avm_vm::get_relation_label_avm_mem)) {
return false;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,72 +7,72 @@
namespace bb::Avm_vm {

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

inline std::string get_relation_label_avm_alu(int index)
{
switch (index) {
case 6:
return "ALU_ADD_SUB_1";

case 9:
return "ALU_MUL_COMMON_1";

case 17:
return "ALU_OP_EQ";

case 7:
return "ALU_ADD_SUB_2";

case 15:
return "ALU_OP_NOT";

case 6:
return "ALU_ADD_SUB_1";

case 13:
return "ALU_MULTIPLICATION_OUT_U128";

case 10:
return "ALU_MUL_COMMON_2";

case 16:
return "ALU_RES_IS_BOOL";

case 17:
return "ALU_OP_EQ";

case 14:
return "ALU_FF_NOT_XOR";

case 10:
return "ALU_MUL_COMMON_2";
case 15:
return "ALU_OP_NOT";

case 8:
return "ALU_MULTIPLICATION_FF";
Expand Down
Loading

0 comments on commit 6ea5658

Please sign in to comment.