Skip to content

Commit

Permalink
test: add div by zero
Browse files Browse the repository at this point in the history
  • Loading branch information
@IlyasRidhuan
IlyasRidhuan committed May 8, 2024
1 parent 5e7d92d commit 6022718
Show file tree
Hide file tree
Showing 21 changed files with 1,980 additions and 124 deletions.
14 changes: 10 additions & 4 deletions barretenberg/cpp/pil/avm/avm_alu.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -689,7 +689,7 @@ namespace avm_alu(256);
// Range checks already performed via a_lo and 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_hi, it has to fit into a 128-bit range check
//Range check remainder < ib and put the value in b_hi, it has to fit into a 128 bit range check
#[REMAINDER_RANGE_CHK]
op_div_std * (b_hi - (ib - remainder - 1)) = 0;

Expand All @@ -706,9 +706,15 @@ namespace avm_alu(256);
op_div_std * (PRODUCT - (ia - remainder)) = 0;

// === DIVISION 64 BIT RANGE CHECKS
// 64-bit decompositions and implicit 64-bit range checks for each limb,
// 64-bit decompositions and implicit 64 bit range checks for each limb,
// TODO: We need extra slice registers because we are performing an additional 64-bit bit range check in the same row, look into re-using old columns or refactoring
// range checks to be more modular.
// boolean to account for the division-specific 64 bit range checks.
pol commit div_rng_chk_selector;
div_rng_chk_selector * (1 - div_rng_chk_selector) = 0;
// div_rng_chk_selector && div_rng_chk_selector' = 1 if op_div_std = 1
div_rng_chk_selector * div_rng_chk_selector' = op_div_std;

pol commit div_u16_r0;
pol commit div_u16_r1;
pol commit div_u16_r2;
Expand All @@ -723,8 +729,8 @@ namespace avm_alu(256);
quotient_lo = op_div_std * (div_u16_r0' + div_u16_r1' * 2**16 + div_u16_r2' * 2**32 + div_u16_r3' * 2**48);
quotient_hi = op_div_std * (div_u16_r4' + div_u16_r5' * 2**16 + div_u16_r6' * 2**32 + div_u16_r7' * 2**48);

// We need an extra 128 bits to do 2 more 64 bit range checks. We use b_lo to store partial_prod_lo and partial_prod_hi.
// Use a shift to access the slices (b_lo is moved into the alu slice registers on the next row)
// We need an extra 128 bits to do 2 more 64 bit range checks. We use b_lo (128 bits) to store partial_prod_lo(64 bits) and partial_prod_hi(64 bits.
// Use a shift to access the slices (b_lo is moved into the alu slice registers on the next row anyways as part of the SHIFT_RELS_0 relations)
pol NEXT_SUM_64 = u8_r0' + u8_r1' * 2**8 + u16_r0' * 2**16 + u16_r1' * 2**32 + u16_r2' * 2**48;
pol NEXT_SUM_128 = u16_r3' + u16_r4' * 2**16 + u16_r5' * 2**32 + u16_r6' * 2**48;
partial_prod_lo = op_div_std * NEXT_SUM_64;
Expand Down
26 changes: 25 additions & 1 deletion barretenberg/cpp/pil/avm/avm_main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -323,7 +323,7 @@ namespace avm_main(256);

// Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1,
// the operation is not copied to the ALU table.
alu_sel = ALU_ALL_SEL * (1 - tag_err);
alu_sel = ALU_ALL_SEL * (1 - tag_err) * (1 - op_err);

// Dispatch the correct in_tag for alu
ALU_R_TAG_SEL * (alu_in_tag - r_in_tag) = 0;
Expand Down Expand Up @@ -473,3 +473,27 @@ namespace avm_main(256);
#[LOOKUP_U16_14]
avm_alu.rng_chk_lookup_selector {avm_alu.u16_r14 } in sel_rng_16 { clk };

// ==== Additional row range checks for division
#[LOOKUP_DIV_U16_0]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r0} in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_1]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r1 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_2]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r2 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_3]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r3 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_4]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r4 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_5]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r5 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_6]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r6 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_7]
avm_alu.div_rng_chk_selector {avm_alu.div_u16_r7 } in sel_rng_16 { clk };
54 changes: 36 additions & 18 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 @@ -23,6 +23,8 @@ template <typename FF> struct Avm_aluRow {
FF avm_alu_cmp_rng_ctr_shift{};
FF avm_alu_cmp_sel{};
FF avm_alu_cmp_sel_shift{};
FF avm_alu_div_rng_chk_selector{};
FF avm_alu_div_rng_chk_selector_shift{};
FF avm_alu_div_u16_r0{};
FF avm_alu_div_u16_r0_shift{};
FF avm_alu_div_u16_r1{};
Expand Down Expand Up @@ -275,10 +277,10 @@ template <typename FF_> class avm_aluImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 85> SUBRELATION_PARTIAL_LENGTHS{
static constexpr std::array<size_t, 87> 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, 3, 3, 3, 4, 4, 3, 5, 3, 3, 3, 5, 4, 4, 4, 4, 4, 4,
4, 3, 5, 5, 4, 5, 5, 2, 3, 3, 3, 3, 3, 4, 4, 3, 5, 3, 3, 3, 5, 3, 3, 4, 4, 4, 4, 4, 4,
};

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -1130,49 +1132,65 @@ template <typename FF_> class avm_aluImpl {
{
Avm_DECLARE_VIEWS(79);

auto tmp = (avm_alu_div_rng_chk_selector * (-avm_alu_div_rng_chk_selector + FF(1)));
tmp *= scaling_factor;
std::get<79>(evals) += tmp;
}
// Contribution 80
{
Avm_DECLARE_VIEWS(80);

auto tmp = ((avm_alu_div_rng_chk_selector * avm_alu_div_rng_chk_selector_shift) - avm_alu_op_div_std);
tmp *= scaling_factor;
std::get<80>(evals) += tmp;
}
// Contribution 81
{
Avm_DECLARE_VIEWS(81);

auto tmp =
(avm_alu_divisor_lo - (avm_alu_op_div_std * (((avm_alu_div_u16_r0 + (avm_alu_div_u16_r1 * FF(65536))) +
(avm_alu_div_u16_r2 * FF(4294967296UL))) +
(avm_alu_div_u16_r3 * FF(281474976710656UL)))));
tmp *= scaling_factor;
std::get<79>(evals) += tmp;
std::get<81>(evals) += tmp;
}
// Contribution 80
// Contribution 82
{
Avm_DECLARE_VIEWS(80);
Avm_DECLARE_VIEWS(82);

auto tmp =
(avm_alu_divisor_hi - (avm_alu_op_div_std * (((avm_alu_div_u16_r4 + (avm_alu_div_u16_r5 * FF(65536))) +
(avm_alu_div_u16_r6 * FF(4294967296UL))) +
(avm_alu_div_u16_r7 * FF(281474976710656UL)))));
tmp *= scaling_factor;
std::get<80>(evals) += tmp;
std::get<82>(evals) += tmp;
}
// Contribution 81
// Contribution 83
{
Avm_DECLARE_VIEWS(81);
Avm_DECLARE_VIEWS(83);

auto tmp = (avm_alu_quotient_lo -
(avm_alu_op_div_std * (((avm_alu_div_u16_r0_shift + (avm_alu_div_u16_r1_shift * FF(65536))) +
(avm_alu_div_u16_r2_shift * FF(4294967296UL))) +
(avm_alu_div_u16_r3_shift * FF(281474976710656UL)))));
tmp *= scaling_factor;
std::get<81>(evals) += tmp;
std::get<83>(evals) += tmp;
}
// Contribution 82
// Contribution 84
{
Avm_DECLARE_VIEWS(82);
Avm_DECLARE_VIEWS(84);

auto tmp = (avm_alu_quotient_hi -
(avm_alu_op_div_std * (((avm_alu_div_u16_r4_shift + (avm_alu_div_u16_r5_shift * FF(65536))) +
(avm_alu_div_u16_r6_shift * FF(4294967296UL))) +
(avm_alu_div_u16_r7_shift * FF(281474976710656UL)))));
tmp *= scaling_factor;
std::get<82>(evals) += tmp;
std::get<84>(evals) += tmp;
}
// Contribution 83
// Contribution 85
{
Avm_DECLARE_VIEWS(83);
Avm_DECLARE_VIEWS(85);

auto tmp =
(avm_alu_partial_prod_lo -
Expand All @@ -1181,18 +1199,18 @@ template <typename FF_> class avm_aluImpl {
(avm_alu_u16_r1_shift * FF(4294967296UL))) +
(avm_alu_u16_r2_shift * FF(281474976710656UL)))));
tmp *= scaling_factor;
std::get<83>(evals) += tmp;
std::get<85>(evals) += tmp;
}
// Contribution 84
// Contribution 86
{
Avm_DECLARE_VIEWS(84);
Avm_DECLARE_VIEWS(86);

auto tmp = (avm_alu_partial_prod_hi -
(avm_alu_op_div_std * (((avm_alu_u16_r3_shift + (avm_alu_u16_r4_shift * FF(65536))) +
(avm_alu_u16_r5_shift * FF(4294967296UL))) +
(avm_alu_u16_r6_shift * FF(281474976710656UL)))));
tmp *= scaling_factor;
std::get<84>(evals) += tmp;
std::get<86>(evals) += tmp;
}
}
};
Expand Down
21 changes: 11 additions & 10 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ template <typename FF_> class avm_mainImpl {

static constexpr std::array<size_t, 69> SUBRELATION_PARTIAL_LENGTHS{
3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
3, 3, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2,
3, 3, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 4, 4, 3, 3, 3, 3, 3, 4, 3, 3, 3, 2,
};

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -677,15 +677,16 @@ template <typename FF_> class avm_mainImpl {

auto tmp =
(avm_main_alu_sel -
(((((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_div) +
avm_main_sel_op_not) +
avm_main_sel_op_eq) +
avm_main_sel_op_lt) +
avm_main_sel_op_lte) +
avm_main_sel_op_shr) +
avm_main_sel_op_shl) +
avm_main_sel_op_cast) *
(-avm_main_tag_err + FF(1))));
((((((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_div) +
avm_main_sel_op_not) +
avm_main_sel_op_eq) +
avm_main_sel_op_lt) +
avm_main_sel_op_lte) +
avm_main_sel_op_shr) +
avm_main_sel_op_shl) +
avm_main_sel_op_cast) *
(-avm_main_tag_err + FF(1))) *
(-avm_main_op_err + FF(1))));
tmp *= scaling_factor;
std::get<64>(evals) += tmp;
}
Expand Down
18 changes: 18 additions & 0 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
[[maybe_unused]] auto avm_alu_clk = View(new_term.avm_alu_clk); \
[[maybe_unused]] auto avm_alu_cmp_rng_ctr = View(new_term.avm_alu_cmp_rng_ctr); \
[[maybe_unused]] auto avm_alu_cmp_sel = View(new_term.avm_alu_cmp_sel); \
[[maybe_unused]] auto avm_alu_div_rng_chk_selector = View(new_term.avm_alu_div_rng_chk_selector); \
[[maybe_unused]] auto avm_alu_div_u16_r0 = View(new_term.avm_alu_div_u16_r0); \
[[maybe_unused]] auto avm_alu_div_u16_r1 = View(new_term.avm_alu_div_u16_r1); \
[[maybe_unused]] auto avm_alu_div_u16_r2 = View(new_term.avm_alu_div_u16_r2); \
Expand Down Expand Up @@ -232,6 +233,14 @@
[[maybe_unused]] auto lookup_u16_12 = View(new_term.lookup_u16_12); \
[[maybe_unused]] auto lookup_u16_13 = View(new_term.lookup_u16_13); \
[[maybe_unused]] auto lookup_u16_14 = View(new_term.lookup_u16_14); \
[[maybe_unused]] auto lookup_div_u16_0 = View(new_term.lookup_div_u16_0); \
[[maybe_unused]] auto lookup_div_u16_1 = View(new_term.lookup_div_u16_1); \
[[maybe_unused]] auto lookup_div_u16_2 = View(new_term.lookup_div_u16_2); \
[[maybe_unused]] auto lookup_div_u16_3 = View(new_term.lookup_div_u16_3); \
[[maybe_unused]] auto lookup_div_u16_4 = View(new_term.lookup_div_u16_4); \
[[maybe_unused]] auto lookup_div_u16_5 = View(new_term.lookup_div_u16_5); \
[[maybe_unused]] auto lookup_div_u16_6 = View(new_term.lookup_div_u16_6); \
[[maybe_unused]] auto lookup_div_u16_7 = View(new_term.lookup_div_u16_7); \
[[maybe_unused]] auto lookup_byte_lengths_counts = View(new_term.lookup_byte_lengths_counts); \
[[maybe_unused]] auto lookup_byte_operations_counts = View(new_term.lookup_byte_operations_counts); \
[[maybe_unused]] auto incl_main_tag_err_counts = View(new_term.incl_main_tag_err_counts); \
Expand All @@ -257,13 +266,22 @@
[[maybe_unused]] auto lookup_u16_12_counts = View(new_term.lookup_u16_12_counts); \
[[maybe_unused]] auto lookup_u16_13_counts = View(new_term.lookup_u16_13_counts); \
[[maybe_unused]] auto lookup_u16_14_counts = View(new_term.lookup_u16_14_counts); \
[[maybe_unused]] auto lookup_div_u16_0_counts = View(new_term.lookup_div_u16_0_counts); \
[[maybe_unused]] auto lookup_div_u16_1_counts = View(new_term.lookup_div_u16_1_counts); \
[[maybe_unused]] auto lookup_div_u16_2_counts = View(new_term.lookup_div_u16_2_counts); \
[[maybe_unused]] auto lookup_div_u16_3_counts = View(new_term.lookup_div_u16_3_counts); \
[[maybe_unused]] auto lookup_div_u16_4_counts = View(new_term.lookup_div_u16_4_counts); \
[[maybe_unused]] auto lookup_div_u16_5_counts = View(new_term.lookup_div_u16_5_counts); \
[[maybe_unused]] auto lookup_div_u16_6_counts = View(new_term.lookup_div_u16_6_counts); \
[[maybe_unused]] auto lookup_div_u16_7_counts = View(new_term.lookup_div_u16_7_counts); \
[[maybe_unused]] auto avm_alu_a_hi_shift = View(new_term.avm_alu_a_hi_shift); \
[[maybe_unused]] auto avm_alu_a_lo_shift = View(new_term.avm_alu_a_lo_shift); \
[[maybe_unused]] auto avm_alu_alu_sel_shift = View(new_term.avm_alu_alu_sel_shift); \
[[maybe_unused]] auto avm_alu_b_hi_shift = View(new_term.avm_alu_b_hi_shift); \
[[maybe_unused]] auto avm_alu_b_lo_shift = View(new_term.avm_alu_b_lo_shift); \
[[maybe_unused]] auto avm_alu_cmp_rng_ctr_shift = View(new_term.avm_alu_cmp_rng_ctr_shift); \
[[maybe_unused]] auto avm_alu_cmp_sel_shift = View(new_term.avm_alu_cmp_sel_shift); \
[[maybe_unused]] auto avm_alu_div_rng_chk_selector_shift = View(new_term.avm_alu_div_rng_chk_selector_shift); \
[[maybe_unused]] auto avm_alu_div_u16_r0_shift = View(new_term.avm_alu_div_u16_r0_shift); \
[[maybe_unused]] auto avm_alu_div_u16_r1_shift = View(new_term.avm_alu_div_u16_r1_shift); \
[[maybe_unused]] auto avm_alu_div_u16_r2_shift = View(new_term.avm_alu_div_u16_r2_shift); \
Expand Down
Loading

0 comments on commit 6022718

Please sign in to comment.