Skip to content

Commit

Permalink
chore: comments + execution
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed May 3, 2024
1 parent 44faa93 commit a079c7d
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 19 deletions.
9 changes: 5 additions & 4 deletions barretenberg/cpp/pil/avm/avm_alu.pil
Original file line number Diff line number Diff line change
Expand Up @@ -654,24 +654,25 @@ namespace avm_alu(256);
// To show this, we constrain ib - ia - 1 to be within 128-bits
// Since we need a range check we use the existing a_lo column that is range checked over 128-bits
op_div_a_lt_b * (a_lo - (ib - ia - 1)) = 0;
op_div_a_lt_b * ic * (ia - remainder) = 0;
op_div_a_lt_b * ic = 0; // ic = 0
op_div_a_lt_b * (ia - remainder) = 0; // remainder = a, might not be needed.


// ====== Handling ia > ib =====
pol commit op_div_std;
op_div_std * (1 - op_div_std) = 0;

pol PRODUCT = ib * ic; // This can be up to a 256-bit number
pol PRODUCT = ib * ic; // This number can be up to 256-bits long
// We need to check that this value has not overflowed the field.
// (1) Decompose ib * ic into two 128-bit limbs, we will re-use the a_lo and a_hi columns.
// (2) Perform a 128-bit range check, over these two limbs.
// (2) Perform a 128-bit range check, over these two limbs. Again re-using the a_lo and a_hi columns.
// (3) Perform the primality check, we re-use the p_sub_a_lo and p_sub_a_hi columns.

// Check that a_lo and a_hi correctly represent PRODUCT
#[ALU_PROD_DIV]
op_div_std * (PRODUCT - (a_lo + 2 ** 128 * a_hi)) = 0;
// Range checks already performed via a_lo and a_hi
// Primality checks already performed above p_sub_a_lo and p_sub_a_hi
// Primality checks already performed above via p_sub_a_lo and p_sub_a_hi

//Range check remainder < ib and put the value in b_lo, it has to fit into a 128-bit range check
// b_hi is zero, TODO: does it need to be enforced as zero?
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -234,16 +234,16 @@ inline std::string get_relation_label_avm_alu(int index)
case 64:
return "SHL_OUTPUT";

case 70:
case 71:
return "ALU_PROD_DIV";

case 71:
case 72:
return "REMAINDER_RANGE_CHK";

case 73:
case 74:
return "CMP_CTR_REL_3";

case 75:
case 76:
return "DIVISION_RELATION";
}
return std::to_string(index);
Expand All @@ -253,10 +253,10 @@ template <typename FF_> class avm_aluImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 76> SUBRELATION_PARTIAL_LENGTHS{
static constexpr std::array<size_t, 77> SUBRELATION_PARTIAL_LENGTHS{
2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 4, 4,
3, 4, 3, 3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 2, 5,
3, 3, 4, 4, 4, 4, 4, 3, 5, 5, 4, 5, 5, 2, 3, 3, 4, 3, 4, 3, 3, 3, 3, 4,
3, 3, 4, 4, 4, 4, 4, 3, 5, 5, 4, 5, 5, 2, 3, 3, 3, 3, 3, 4, 3, 3, 3, 3, 4,
};

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -1009,67 +1009,75 @@ template <typename FF_> class avm_aluImpl {
{
Avm_DECLARE_VIEWS(68);

auto tmp = ((avm_alu_op_div_a_lt_b * avm_alu_ic) * (avm_alu_ia - avm_alu_remainder));
auto tmp = (avm_alu_op_div_a_lt_b * avm_alu_ic);
tmp *= scaling_factor;
std::get<68>(evals) += tmp;
}
// Contribution 69
{
Avm_DECLARE_VIEWS(69);

auto tmp = (avm_alu_op_div_std * (-avm_alu_op_div_std + FF(1)));
auto tmp = (avm_alu_op_div_a_lt_b * (avm_alu_ia - avm_alu_remainder));
tmp *= scaling_factor;
std::get<69>(evals) += tmp;
}
// Contribution 70
{
Avm_DECLARE_VIEWS(70);

auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) -
(avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL })))));
auto tmp = (avm_alu_op_div_std * (-avm_alu_op_div_std + FF(1)));
tmp *= scaling_factor;
std::get<70>(evals) += tmp;
}
// Contribution 71
{
Avm_DECLARE_VIEWS(71);

auto tmp = (avm_alu_op_div_std * (avm_alu_b_lo - ((avm_alu_ib - avm_alu_remainder) - FF(1))));
auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) -
(avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL })))));
tmp *= scaling_factor;
std::get<71>(evals) += tmp;
}
// Contribution 72
{
Avm_DECLARE_VIEWS(72);

auto tmp = (avm_alu_op_div_std * avm_alu_b_hi);
auto tmp = (avm_alu_op_div_std * (avm_alu_b_lo - ((avm_alu_ib - avm_alu_remainder) - FF(1))));
tmp *= scaling_factor;
std::get<72>(evals) += tmp;
}
// Contribution 73
{
Avm_DECLARE_VIEWS(73);

auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(2)) * avm_alu_op_div_std);
auto tmp = (avm_alu_op_div_std * avm_alu_b_hi);
tmp *= scaling_factor;
std::get<73>(evals) += tmp;
}
// Contribution 74
{
Avm_DECLARE_VIEWS(74);

auto tmp = (avm_alu_rng_chk_sel * avm_alu_op_div_std);
auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(2)) * avm_alu_op_div_std);
tmp *= scaling_factor;
std::get<74>(evals) += tmp;
}
// Contribution 75
{
Avm_DECLARE_VIEWS(75);

auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) - (avm_alu_ia - avm_alu_remainder)));
auto tmp = (avm_alu_rng_chk_sel * avm_alu_op_div_std);
tmp *= scaling_factor;
std::get<75>(evals) += tmp;
}
// Contribution 76
{
Avm_DECLARE_VIEWS(76);

auto tmp = (avm_alu_op_div_std * ((avm_alu_ib * avm_alu_ic) - (avm_alu_ia - avm_alu_remainder)));
tmp *= scaling_factor;
std::get<76>(evals) += tmp;
}
}
};

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,12 @@ std::vector<Row> Execution::gen_trace(std::vector<Instruction> const& instructio
std::get<uint32_t>(inst.operands.at(2)),
std::get<uint32_t>(inst.operands.at(3)));
break;
case OpCode::DIV:
trace_builder.op_div(std::get<uint8_t>(inst.operands.at(0)),
std::get<uint32_t>(inst.operands.at(1)),
std::get<uint32_t>(inst.operands.at(2)),
std::get<uint32_t>(inst.operands.at(3)));
break;
// Compute - Comparators
case OpCode::EQ:
trace_builder.op_eq(std::get<uint8_t>(inst.operands.at(0)),
Expand Down

0 comments on commit a079c7d

Please sign in to comment.