Skip to content

Commit

Permalink
fix: more constraints and tests
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed Mar 25, 2024
1 parent 3367500 commit a3dea9e
Show file tree
Hide file tree
Showing 13 changed files with 290 additions and 254 deletions.
16 changes: 5 additions & 11 deletions barretenberg/cpp/pil/avm/avm_binary.pil
Original file line number Diff line number Diff line change
Expand Up @@ -49,18 +49,12 @@ namespace avm_binary(256);
// This is checked by two relation conditions and utilising mem_tag_ctr_inv
pol commit mem_tag_ctr_inv;

// a) Bin_sel constrained to be a boolean
// b) When mem_tag_ctr != 0, bin_sel must be 1
// c) When mem_tag_ctr = 0, bin_sel must be 0.
// 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
// 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.
#[BIN_SEL_CTR_REL]
mem_tag_ctr * mem_tag_ctr_inv - bin_sel = 0;

// Must ensure that mem_tag_ctr_inv !=0 if mem_tag_ctr != 0,
// otherwise it is possible to set bin_sel = 0 when mem_tag_ctr != 0 in BIN_SEL_CTR_REL.
// a) When mem_tag_ctr == 0, bin_sel is 0 from BIN_SEL_CTR_REL.
// b) if bin_sel is 0, mem_tag_ctr_inv must be 1.
// c) if bin_sel is 1, mem_tag_ctr_inv constrained by BIN_SEL_CTR_REL.
(1 - bin_sel) * (mem_tag_ctr_inv - 1) = 0;
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
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_aluRow {
FF avm_alu_alu_u16_r4{};
FF avm_alu_alu_u16_r0_shift{};
FF avm_alu_alu_op_eq_diff_inv{};
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_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_u64_r0{};
FF avm_alu_alu_u16_r0{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_alu_alu_u16_r4_shift{};
FF avm_alu_alu_u16_r7{};
FF avm_alu_alu_u16_r2{};
FF avm_alu_alu_u8_tag{};
FF avm_alu_alu_u16_r2_shift{};
FF avm_alu_alu_u16_r6{};
FF avm_alu_alu_u16_r3{};
FF avm_alu_alu_u64_tag{};
FF avm_alu_alu_u128_tag{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_op_mul{};
FF avm_alu_alu_op_add{};
FF avm_alu_alu_op_not{};
FF avm_alu_alu_u64_tag{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_u16_r1{};
FF avm_alu_alu_in_tag{};
FF avm_alu_alu_u16_r3_shift{};
FF avm_alu_alu_u16_r6_shift{};
FF avm_alu_alu_op_sub{};
FF avm_alu_alu_u16_r5{};
FF avm_alu_alu_u8_r1{};
FF avm_alu_alu_u64_r0{};
FF avm_alu_alu_u16_r1_shift{};
FF avm_alu_alu_sel{};
FF avm_alu_alu_u16_r7_shift{};
FF avm_alu_alu_ib{};
FF avm_alu_alu_u16_r2{};
FF avm_alu_alu_u32_tag{};
FF avm_alu_alu_u16_tag{};
FF avm_alu_alu_u8_r0{};
FF avm_alu_alu_ia{};
FF avm_alu_alu_ic{};
FF avm_alu_alu_cf{};
FF avm_alu_alu_op_eq{};
FF avm_alu_alu_u16_r5_shift{};
FF avm_alu_alu_op_not{};
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{};
};

inline std::string get_relation_label_avm_alu(int index)
Expand All @@ -52,32 +52,32 @@ inline std::string get_relation_label_avm_alu(int index)
case 9:
return "ALU_ADD_SUB_1";

case 11:
return "ALU_MULTIPLICATION_FF";
case 16:
return "ALU_MULTIPLICATION_OUT_U128";

case 10:
return "ALU_ADD_SUB_2";
case 20:
return "ALU_OP_EQ";

case 18:
return "ALU_OP_NOT";

case 13:
return "ALU_MUL_COMMON_2";

case 12:
return "ALU_MUL_COMMON_1";

case 19:
return "ALU_RES_IS_BOOL";

case 17:
return "ALU_FF_NOT_XOR";

case 18:
return "ALU_OP_NOT";

case 16:
return "ALU_MULTIPLICATION_OUT_U128";

case 19:
return "ALU_RES_IS_BOOL";
case 11:
return "ALU_MULTIPLICATION_FF";

case 20:
return "ALU_OP_EQ";
case 10:
return "ALU_ADD_SUB_2";
}
return std::to_string(index);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,39 +7,43 @@
namespace bb::Avm_vm {

template <typename FF> struct Avm_binaryRow {
FF avm_binary_acc_ic_shift{};
FF avm_binary_acc_ib{};
FF avm_binary_bin_sel{};
FF avm_binary_acc_ib_shift{};
FF avm_binary_op_id{};
FF avm_binary_bin_ic_bytes{};
FF avm_binary_acc_ic{};
FF avm_binary_acc_ib_shift{};
FF avm_binary_acc_ia{};
FF avm_binary_mem_tag_ctr{};
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_acc_ia_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_mem_tag_ctr_inv{};
FF avm_binary_mem_tag_ctr{};
FF avm_binary_bin_sel{};
};

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 8:
return "ACC_REL_C";
case 3:
return "BIN_SEL_CTR_REL";

case 1:
return "OP_ID_REL";

case 6:
return "ACC_REL_A";

case 7:
return "ACC_REL_B";

case 1:
return "OP_ID_REL";
}
return std::to_string(index);
}
Expand All @@ -49,7 +53,7 @@ template <typename FF_> class avm_binaryImpl {
using FF = FF_;

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

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -87,7 +91,10 @@ template <typename FF_> class avm_binaryImpl {
{
Avm_DECLARE_VIEWS(3);

auto tmp = ((-avm_binary_bin_sel + FF(1)) * avm_binary_mem_tag_ctr);
auto tmp =
((avm_binary_mem_tag_ctr * (((-avm_binary_bin_sel + FF(1)) * (-avm_binary_mem_tag_ctr_inv + FF(1))) +
avm_binary_mem_tag_ctr_inv)) -
avm_binary_bin_sel);
tmp *= scaling_factor;
std::get<3>(evals) += tmp;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,82 +7,82 @@
namespace bb::Avm_vm {

template <typename FF> struct Avm_mainRow {
FF avm_main_tag_err{};
FF avm_main_sel_op_sub{};
FF avm_main_internal_return_ptr{};
FF avm_main_sel_op_and{};
FF avm_main_sel_op_div{};
FF avm_main_rwa{};
FF avm_main_ind_op_c{};
FF avm_main_sel_op_add{};
FF avm_main_sel_op_mul{};
FF avm_main_sel_internal_call{};
FF avm_main_sel_jump{};
FF avm_main_sel_mov{};
FF avm_main_mem_op_b{};
FF avm_main_sel_op_xor{};
FF avm_main_rwc{};
FF avm_main_internal_return_ptr{};
FF avm_main_first{};
FF avm_main_mem_op_a{};
FF avm_main_ind_op_c{};
FF avm_main_internal_return_ptr_shift{};
FF avm_main_ind_op_a{};
FF avm_main_inv{};
FF avm_main_bin_op_id{};
FF avm_main_sel_internal_return{};
FF avm_main_mem_op_c{};
FF avm_main_op_err{};
FF avm_main_rwb{};
FF avm_main_ic{};
FF avm_main_ia{};
FF avm_main_pc_shift{};
FF avm_main_sel_op_not{};
FF avm_main_mem_idx_b{};
FF avm_main_tag_err{};
FF avm_main_alu_sel{};
FF avm_main_bin_sel{};
FF avm_main_sel_mov{};
FF avm_main_sel_op_or{};
FF avm_main_ind_op_b{};
FF avm_main_mem_idx_a{};
FF avm_main_sel_op_sub{};
FF avm_main_inv{};
FF avm_main_pc{};
FF avm_main_op_err{};
FF avm_main_alu_sel{};
FF avm_main_sel_halt{};
FF avm_main_sel_op_or{};
FF avm_main_bin_sel{};
FF avm_main_sel_op_not{};
FF avm_main_sel_op_xor{};
FF avm_main_pc_shift{};
FF avm_main_ib{};
FF avm_main_first{};
FF avm_main_ic{};
FF avm_main_sel_op_div{};
FF avm_main_mem_op_b{};
FF avm_main_sel_internal_return{};
FF avm_main_rwc{};
FF avm_main_sel_op_mul{};
FF avm_main_internal_return_ptr_shift{};
FF avm_main_pc{};
FF avm_main_sel_op_eq{};
FF avm_main_ind_op_b{};
FF avm_main_rwa{};
FF avm_main_ia{};
FF avm_main_ind_op_a{};
FF avm_main_mem_idx_b{};
FF avm_main_mem_op_c{};
FF avm_main_sel_internal_call{};
FF avm_main_sel_jump{};
};

inline std::string get_relation_label_avm_main(int index)
{
switch (index) {
case 36:
return "RETURN_POINTER_DECREMENT";

case 43:
return "MOV_SAME_VALUE";

case 45:
return "BIN_SEL_1";

case 28:
return "SUBOP_ERROR_RELEVANT_OP";

case 25:
return "SUBOP_DIVISION_FF";

case 27:
return "SUBOP_DIVISION_ZERO_ERR2";
case 41:
return "PC_INCREMENT";

case 42:
return "INTERNAL_RETURN_POINTER_CONSISTENCY";

case 26:
return "SUBOP_DIVISION_ZERO_ERR1";
case 28:
return "SUBOP_ERROR_RELEVANT_OP";

case 43:
return "MOV_SAME_VALUE";

case 46:
return "BIN_SEL_2";

case 27:
return "SUBOP_DIVISION_ZERO_ERR2";

case 30:
return "RETURN_POINTER_INCREMENT";

case 41:
return "PC_INCREMENT";
case 36:
return "RETURN_POINTER_DECREMENT";

case 45:
return "BIN_SEL_1";

case 26:
return "SUBOP_DIVISION_ZERO_ERR1";
}
return std::to_string(index);
}
Expand Down
Loading

0 comments on commit a3dea9e

Please sign in to comment.