Skip to content

Commit

Permalink
fix: more comments
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed Mar 26, 2024
1 parent a3dea9e commit 7afb529
Show file tree
Hide file tree
Showing 12 changed files with 295 additions and 293 deletions.
19 changes: 11 additions & 8 deletions barretenberg/cpp/pil/avm/avm_binary.pil
Original file line number Diff line number Diff line change
Expand Up @@ -29,16 +29,17 @@ namespace avm_binary(256);
#[OP_ID_REL]
(op_id' - op_id) * mem_tag_ctr = 0;

// Little Endian bitwise decomposition, constrained to be U8 given the lookup the avm_byte_lookup
// Little Endian bitwise decomposition of accumulators (which are processed top-down),
// constrained to be U8 given by the lookup to the avm_byte_lookup
pol commit bin_ia_bytes;
pol commit bin_ib_bytes;
pol commit bin_ic_bytes;

pol commit start; // Identifies when we want to capture the output to the main tracssssss
pol commit start; // Identifies when we want to capture the output to the main trace.


// To support dynamically sized memory operands we use a counter against a lookup
// This counter goes from [0, MEM_TAG] where MEM_TAG is the number of bytes in the
// This decrementing counter goes from [MEM_TAG, 0] where MEM_TAG is the number of bytes in the
// corresponding integer. i.e. MEM_TAG is between 1 (U8) and 16(U128).
// Consistency can be achieved with a lookup table between the instr_tag and bytes_length
pol commit mem_tag_ctr;
Expand All @@ -50,14 +51,16 @@ namespace avm_binary(256);
pol commit mem_tag_ctr_inv;

// bin_sel is set to 1 when mem_tag_ctr != 0, and 0 otherwise.
// we constrain it such that bin_sel = mem_tag * mem_tag_ctr_inv unless mem_tag = 0 the bin_sel = 0
// we constrain it such that bin_sel = mem_tag_ctr * mem_tag_ctr_inv unless mem_tag_ctr = 0 the bin_sel = 0
// In here we use the consolidated equality relation because it doesnt require us to enforce
// this additional relation: mem_tag_ctr_inv = 1 when mem_tag_ctr = 0.
// this additional relation: mem_tag_ctr_inv = 1 when mem_tag_ctr = 0. (allows default zero value in trace)
#[BIN_SEL_CTR_REL]
mem_tag_ctr * ((1 - bin_sel) * (1 - mem_tag_ctr_inv) + mem_tag_ctr_inv) - bin_sel = 0;

(1 - bin_sel) * acc_ia = 0; // Forces accumulator to start at zero when mem_tag_ctr == 0
(1 - bin_sel) * acc_ib = 0; // Forces accumulator to start at zero when mem_tag_ctr == 0
// Forces accumulator to start at zero when mem_tag_ctr == 0
(1 - bin_sel) * acc_ia = 0;
(1 - bin_sel) * acc_ib = 0;
(1 - bin_sel) * acc_ic = 0;

#[LOOKUP_BYTE_LENGTHS]
start {in_tag, mem_tag_ctr}
Expand All @@ -67,7 +70,7 @@ namespace avm_binary(256);
#[LOOKUP_BYTE_OPERATIONS]
bin_sel {op_id, bin_ia_bytes, bin_ib_bytes, bin_ic_bytes}
in
avm_byte_lookup.bin_sel {avm_byte_lookup.table_op_id, avm_byte_lookup.table_input_a,avm_byte_lookup.table_input_b, avm_byte_lookup.table_output};
avm_byte_lookup.bin_sel {avm_byte_lookup.table_op_id, avm_byte_lookup.table_input_a, avm_byte_lookup.table_input_b, avm_byte_lookup.table_output};

#[ACC_REL_A]
(acc_ia - bin_ia_bytes - 256 * acc_ia') * mem_tag_ctr = 0;
Expand Down
4 changes: 3 additions & 1 deletion barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -261,8 +261,10 @@ namespace avm_main(256);
bin_op_id = sel_op_or + 2 * sel_op_xor; // sel_op_and excluded since op_id = 0 for op_and

// Only 1 of the binary selectors should be set (i.e. Mutual Exclusivity)
// Bin_sel is not explicitly constrained to be boolean, however this is enforced through
// the operation decomposition step during bytecode unpacking.
#[BIN_SEL_2]
bin_sel = (sel_op_and + sel_op_or + sel_op_xor);
bin_sel = sel_op_and + sel_op_or + sel_op_xor;

#[PERM_MAIN_BIN]
bin_sel {ia, ib, ic, bin_op_id, in_tag}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,75 +7,75 @@
namespace bb::Avm_vm {

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

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

case 13:
return "ALU_MUL_COMMON_2";

case 16:
return "ALU_MULTIPLICATION_OUT_U128";

case 20:
return "ALU_OP_EQ";

case 18:
return "ALU_OP_NOT";

case 13:
return "ALU_MUL_COMMON_2";
case 19:
return "ALU_RES_IS_BOOL";

case 11:
return "ALU_MULTIPLICATION_FF";

case 12:
return "ALU_MUL_COMMON_1";

case 19:
return "ALU_RES_IS_BOOL";
case 9:
return "ALU_ADD_SUB_1";

case 17:
return "ALU_FF_NOT_XOR";

case 11:
return "ALU_MULTIPLICATION_FF";

case 10:
return "ALU_ADD_SUB_2";
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,43 +7,43 @@
namespace bb::Avm_vm {

template <typename FF> struct Avm_binaryRow {
FF avm_binary_acc_ic{};
FF avm_binary_acc_ib_shift{};
FF avm_binary_bin_sel{};
FF avm_binary_acc_ib{};
FF avm_binary_mem_tag_ctr{};
FF avm_binary_bin_ic_bytes{};
FF avm_binary_acc_ic_shift{};
FF avm_binary_acc_ia{};
FF avm_binary_op_id_shift{};
FF avm_binary_acc_ia_shift{};
FF avm_binary_acc_ib{};
FF avm_binary_op_id{};
FF avm_binary_bin_ib_bytes{};
FF avm_binary_op_id_shift{};
FF avm_binary_bin_ia_bytes{};
FF avm_binary_mem_tag_ctr_shift{};
FF avm_binary_bin_ic_bytes{};
FF avm_binary_acc_ic_shift{};
FF avm_binary_acc_ic{};
FF avm_binary_bin_ia_bytes{};
FF avm_binary_bin_ib_bytes{};
FF avm_binary_mem_tag_ctr_inv{};
FF avm_binary_mem_tag_ctr{};
FF avm_binary_bin_sel{};
FF avm_binary_acc_ib_shift{};
};

inline std::string get_relation_label_avm_binary(int index)
{
switch (index) {
case 8:
return "ACC_REL_C";

case 2:
return "MEM_TAG_REL";

case 3:
return "BIN_SEL_CTR_REL";

case 1:
return "OP_ID_REL";

case 6:
case 7:
return "ACC_REL_A";

case 7:
case 8:
return "ACC_REL_B";

case 9:
return "ACC_REL_C";

case 3:
return "BIN_SEL_CTR_REL";

case 2:
return "MEM_TAG_REL";
}
return std::to_string(index);
}
Expand All @@ -52,8 +52,8 @@ template <typename FF_> class avm_binaryImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 9> SUBRELATION_PARTIAL_LENGTHS{
3, 3, 3, 4, 3, 3, 4, 4, 4,
static constexpr std::array<size_t, 10> SUBRELATION_PARTIAL_LENGTHS{
3, 3, 3, 4, 3, 3, 3, 4, 4, 4,
};

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -118,16 +118,15 @@ template <typename FF_> class avm_binaryImpl {
{
Avm_DECLARE_VIEWS(6);

auto tmp = (((avm_binary_acc_ia - avm_binary_bin_ia_bytes) - (avm_binary_acc_ia_shift * FF(256))) *
avm_binary_mem_tag_ctr);
auto tmp = ((-avm_binary_bin_sel + FF(1)) * avm_binary_acc_ic);
tmp *= scaling_factor;
std::get<6>(evals) += tmp;
}
// Contribution 7
{
Avm_DECLARE_VIEWS(7);

auto tmp = (((avm_binary_acc_ib - avm_binary_bin_ib_bytes) - (avm_binary_acc_ib_shift * FF(256))) *
auto tmp = (((avm_binary_acc_ia - avm_binary_bin_ia_bytes) - (avm_binary_acc_ia_shift * FF(256))) *
avm_binary_mem_tag_ctr);
tmp *= scaling_factor;
std::get<7>(evals) += tmp;
Expand All @@ -136,11 +135,20 @@ template <typename FF_> class avm_binaryImpl {
{
Avm_DECLARE_VIEWS(8);

auto tmp = (((avm_binary_acc_ic - avm_binary_bin_ic_bytes) - (avm_binary_acc_ic_shift * FF(256))) *
auto tmp = (((avm_binary_acc_ib - avm_binary_bin_ib_bytes) - (avm_binary_acc_ib_shift * FF(256))) *
avm_binary_mem_tag_ctr);
tmp *= scaling_factor;
std::get<8>(evals) += tmp;
}
// Contribution 9
{
Avm_DECLARE_VIEWS(9);

auto tmp = (((avm_binary_acc_ic - avm_binary_bin_ic_bytes) - (avm_binary_acc_ic_shift * FF(256))) *
avm_binary_mem_tag_ctr);
tmp *= scaling_factor;
std::get<9>(evals) += tmp;
}
}
};

Expand Down
Loading

0 comments on commit 7afb529

Please sign in to comment.