Skip to content

Commit

Permalink
5466: Add PIL relation to prevent overlap in second row of CAST and
Browse files Browse the repository at this point in the history 
      128-bit multiplication in ALU trace
  • Loading branch information
@jeanmon
jeanmon committed Apr 18, 2024
1 parent d1400ac commit 8843cec
Show file tree
Hide file tree
Showing 5 changed files with 140 additions and 59 deletions.
12 changes: 6 additions & 6 deletions barretenberg/cpp/pil/avm/avm_alu.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -497,16 +497,16 @@ namespace avm_alu(256);
#[OP_CAST_PREV_LINE]
op_cast_prev' = op_cast;

// TODO: If a lookup selector with value > 1 is enabled, then we do not need this constraint.
// Otherwise, melding two op_cast with a common row might lead to disabling
#[OP_CAST_PREV_MUT_EXCL]
op_cast_prev * op_cast = 0;

#[ALU_OP_CAST]
op_cast * (SUM_TAG + ff_tag * ia - ic) = 0;

#[OP_CAST_RNG_CHECK_P_SUB_A_LOW]
op_cast * (a_lo' - p_sub_a_lo) = 0;

#[OP_CAST_RNG_CHECK_P_SUB_A_HIGH]
op_cast * (a_hi' - p_sub_a_hi) = 0;
op_cast * (a_hi' - p_sub_a_hi) = 0;

// 128-bit multiplication and CAST need two rows in ALU trace. We need to ensure
// that another ALU operation does not start in the second row.
#[TWO_LINE_OP_NO_OVERLAP]
(op_mul * ff_tag + op_cast) * alu_sel' = 0;
31 changes: 16 additions & 15 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 @@ -12,6 +12,7 @@ template <typename FF> struct Avm_aluRow {
FF avm_alu_a_lo{};
FF avm_alu_a_lo_shift{};
FF avm_alu_alu_sel{};
FF avm_alu_alu_sel_shift{};
FF avm_alu_b_hi{};
FF avm_alu_b_hi_shift{};
FF avm_alu_b_lo{};
Expand Down Expand Up @@ -181,16 +182,16 @@ inline std::string get_relation_label_avm_alu(int index)
return "OP_CAST_PREV_LINE";

case 50:
return "OP_CAST_PREV_MUT_EXCL";
return "ALU_OP_CAST";

case 51:
return "ALU_OP_CAST";
return "OP_CAST_RNG_CHECK_P_SUB_A_LOW";

case 52:
return "OP_CAST_RNG_CHECK_P_SUB_A_LOW";
return "OP_CAST_RNG_CHECK_P_SUB_A_HIGH";

case 53:
return "OP_CAST_RNG_CHECK_P_SUB_A_HIGH";
return "TWO_LINE_OP_NO_OVERLAP";
}
return std::to_string(index);
}
Expand All @@ -201,7 +202,7 @@ template <typename FF_> class avm_aluImpl {

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

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -763,14 +764,6 @@ template <typename FF_> class avm_aluImpl {
{
Avm_DECLARE_VIEWS(50);

auto tmp = (avm_alu_op_cast_prev * avm_alu_op_cast);
tmp *= scaling_factor;
std::get<50>(evals) += tmp;
}
// Contribution 51
{
Avm_DECLARE_VIEWS(51);

auto tmp =
(avm_alu_op_cast *
(((((((avm_alu_u8_tag * avm_alu_u8_r0) +
Expand All @@ -791,21 +784,29 @@ template <typename FF_> class avm_aluImpl {
(avm_alu_ff_tag * avm_alu_ia)) -
avm_alu_ic));
tmp *= scaling_factor;
std::get<50>(evals) += tmp;
}
// Contribution 51
{
Avm_DECLARE_VIEWS(51);

auto tmp = (avm_alu_op_cast * (avm_alu_a_lo_shift - avm_alu_p_sub_a_lo));
tmp *= scaling_factor;
std::get<51>(evals) += tmp;
}
// Contribution 52
{
Avm_DECLARE_VIEWS(52);

auto tmp = (avm_alu_op_cast * (avm_alu_a_lo_shift - avm_alu_p_sub_a_lo));
auto tmp = (avm_alu_op_cast * (avm_alu_a_hi_shift - avm_alu_p_sub_a_hi));
tmp *= scaling_factor;
std::get<52>(evals) += tmp;
}
// Contribution 53
{
Avm_DECLARE_VIEWS(53);

auto tmp = (avm_alu_op_cast * (avm_alu_a_hi_shift - avm_alu_p_sub_a_hi));
auto tmp = (((avm_alu_op_mul * avm_alu_ff_tag) + avm_alu_op_cast) * avm_alu_alu_sel_shift);
tmp *= scaling_factor;
std::get<53>(evals) += tmp;
}
Expand Down
1 change: 1 addition & 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 @@ -219,6 +219,7 @@
[[maybe_unused]] auto lookup_u16_14_counts = View(new_term.lookup_u16_14_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); \
Expand Down
4 changes: 3 additions & 1 deletion barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -268,6 +268,7 @@ template <typename FF> struct AvmFullRow {
FF lookup_u16_14_counts{};
FF avm_alu_a_hi_shift{};
FF avm_alu_a_lo_shift{};
FF avm_alu_alu_sel_shift{};
FF avm_alu_b_hi_shift{};
FF avm_alu_b_lo_shift{};
FF avm_alu_cmp_rng_ctr_shift{};
Expand Down Expand Up @@ -315,7 +316,7 @@ class AvmCircuitBuilder {
using Polynomial = Flavor::Polynomial;
using ProverPolynomials = Flavor::ProverPolynomials;

static constexpr size_t num_fixed_columns = 252;
static constexpr size_t num_fixed_columns = 253;
static constexpr size_t num_polys = 215;
std::vector<Row> rows;

Expand Down Expand Up @@ -520,6 +521,7 @@ class AvmCircuitBuilder {

polys.avm_alu_a_hi_shift = Polynomial(polys.avm_alu_a_hi.shifted());
polys.avm_alu_a_lo_shift = Polynomial(polys.avm_alu_a_lo.shifted());
polys.avm_alu_alu_sel_shift = Polynomial(polys.avm_alu_alu_sel.shifted());
polys.avm_alu_b_hi_shift = Polynomial(polys.avm_alu_b_hi.shifted());
polys.avm_alu_b_lo_shift = Polynomial(polys.avm_alu_b_lo.shifted());
polys.avm_alu_cmp_rng_ctr_shift = Polynomial(polys.avm_alu_cmp_rng_ctr.shifted());
Expand Down
151 changes: 114 additions & 37 deletions barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ class AvmFlavor {
static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
// We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for
// the unshifted and one for the shifted
static constexpr size_t NUM_ALL_ENTITIES = 252;
static constexpr size_t NUM_ALL_ENTITIES = 253;

using GrandProductRelations = std::tuple<perm_main_alu_relation<FF>,
perm_main_bin_relation<FF>,
Expand Down Expand Up @@ -827,6 +827,7 @@ class AvmFlavor {
lookup_u16_14_counts,
avm_alu_a_hi_shift,
avm_alu_a_lo_shift,
avm_alu_alu_sel_shift,
avm_alu_b_hi_shift,
avm_alu_b_lo_shift,
avm_alu_cmp_rng_ctr_shift,
Expand Down Expand Up @@ -1082,6 +1083,7 @@ class AvmFlavor {
lookup_u16_14_counts,
avm_alu_a_hi_shift,
avm_alu_a_lo_shift,
avm_alu_alu_sel_shift,
avm_alu_b_hi_shift,
avm_alu_b_lo_shift,
avm_alu_cmp_rng_ctr_shift,
Expand Down Expand Up @@ -1338,37 +1340,84 @@ class AvmFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return { avm_alu_a_hi, avm_alu_a_lo, avm_alu_b_hi, avm_alu_b_lo,
avm_alu_cmp_rng_ctr, avm_alu_cmp_sel, avm_alu_op_add, avm_alu_op_cast_prev,
avm_alu_op_cast, avm_alu_op_mul, avm_alu_op_sub, avm_alu_p_sub_a_hi,
avm_alu_p_sub_a_lo, avm_alu_p_sub_b_hi, avm_alu_p_sub_b_lo, avm_alu_rng_chk_lookup_selector,
avm_alu_rng_chk_sel, avm_alu_u16_r0, avm_alu_u16_r1, avm_alu_u16_r2,
avm_alu_u16_r3, avm_alu_u16_r4, avm_alu_u16_r5, avm_alu_u16_r6,
avm_alu_u8_r0, avm_alu_u8_r1, avm_binary_acc_ia, avm_binary_acc_ib,
avm_binary_acc_ic, avm_binary_mem_tag_ctr, avm_binary_op_id, avm_main_internal_return_ptr,
avm_main_pc, avm_mem_addr, avm_mem_rw, avm_mem_tag,
return { avm_alu_a_hi,
avm_alu_a_lo,
avm_alu_alu_sel,
avm_alu_b_hi,
avm_alu_b_lo,
avm_alu_cmp_rng_ctr,
avm_alu_cmp_sel,
avm_alu_op_add,
avm_alu_op_cast_prev,
avm_alu_op_cast,
avm_alu_op_mul,
avm_alu_op_sub,
avm_alu_p_sub_a_hi,
avm_alu_p_sub_a_lo,
avm_alu_p_sub_b_hi,
avm_alu_p_sub_b_lo,
avm_alu_rng_chk_lookup_selector,
avm_alu_rng_chk_sel,
avm_alu_u16_r0,
avm_alu_u16_r1,
avm_alu_u16_r2,
avm_alu_u16_r3,
avm_alu_u16_r4,
avm_alu_u16_r5,
avm_alu_u16_r6,
avm_alu_u8_r0,
avm_alu_u8_r1,
avm_binary_acc_ia,
avm_binary_acc_ib,
avm_binary_acc_ic,
avm_binary_mem_tag_ctr,
avm_binary_op_id,
avm_main_internal_return_ptr,
avm_main_pc,
avm_mem_addr,
avm_mem_rw,
avm_mem_tag,
avm_mem_val };
};
RefVector<DataType> get_shifted()
{
return { avm_alu_a_hi_shift, avm_alu_a_lo_shift,
avm_alu_b_hi_shift, avm_alu_b_lo_shift,
avm_alu_cmp_rng_ctr_shift, avm_alu_cmp_sel_shift,
avm_alu_op_add_shift, avm_alu_op_cast_prev_shift,
avm_alu_op_cast_shift, avm_alu_op_mul_shift,
avm_alu_op_sub_shift, avm_alu_p_sub_a_hi_shift,
avm_alu_p_sub_a_lo_shift, avm_alu_p_sub_b_hi_shift,
avm_alu_p_sub_b_lo_shift, avm_alu_rng_chk_lookup_selector_shift,
avm_alu_rng_chk_sel_shift, avm_alu_u16_r0_shift,
avm_alu_u16_r1_shift, avm_alu_u16_r2_shift,
avm_alu_u16_r3_shift, avm_alu_u16_r4_shift,
avm_alu_u16_r5_shift, avm_alu_u16_r6_shift,
avm_alu_u8_r0_shift, avm_alu_u8_r1_shift,
avm_binary_acc_ia_shift, avm_binary_acc_ib_shift,
avm_binary_acc_ic_shift, avm_binary_mem_tag_ctr_shift,
avm_binary_op_id_shift, avm_main_internal_return_ptr_shift,
avm_main_pc_shift, avm_mem_addr_shift,
avm_mem_rw_shift, avm_mem_tag_shift,
return { avm_alu_a_hi_shift,
avm_alu_a_lo_shift,
avm_alu_alu_sel_shift,
avm_alu_b_hi_shift,
avm_alu_b_lo_shift,
avm_alu_cmp_rng_ctr_shift,
avm_alu_cmp_sel_shift,
avm_alu_op_add_shift,
avm_alu_op_cast_prev_shift,
avm_alu_op_cast_shift,
avm_alu_op_mul_shift,
avm_alu_op_sub_shift,
avm_alu_p_sub_a_hi_shift,
avm_alu_p_sub_a_lo_shift,
avm_alu_p_sub_b_hi_shift,
avm_alu_p_sub_b_lo_shift,
avm_alu_rng_chk_lookup_selector_shift,
avm_alu_rng_chk_sel_shift,
avm_alu_u16_r0_shift,
avm_alu_u16_r1_shift,
avm_alu_u16_r2_shift,
avm_alu_u16_r3_shift,
avm_alu_u16_r4_shift,
avm_alu_u16_r5_shift,
avm_alu_u16_r6_shift,
avm_alu_u8_r0_shift,
avm_alu_u8_r1_shift,
avm_binary_acc_ia_shift,
avm_binary_acc_ib_shift,
avm_binary_acc_ic_shift,
avm_binary_mem_tag_ctr_shift,
avm_binary_op_id_shift,
avm_main_internal_return_ptr_shift,
avm_main_pc_shift,
avm_mem_addr_shift,
avm_mem_rw_shift,
avm_mem_tag_shift,
avm_mem_val_shift };
};
};
Expand All @@ -1382,15 +1431,43 @@ class AvmFlavor {

RefVector<DataType> get_to_be_shifted()
{
return { avm_alu_a_hi, avm_alu_a_lo, avm_alu_b_hi, avm_alu_b_lo,
avm_alu_cmp_rng_ctr, avm_alu_cmp_sel, avm_alu_op_add, avm_alu_op_cast_prev,
avm_alu_op_cast, avm_alu_op_mul, avm_alu_op_sub, avm_alu_p_sub_a_hi,
avm_alu_p_sub_a_lo, avm_alu_p_sub_b_hi, avm_alu_p_sub_b_lo, avm_alu_rng_chk_lookup_selector,
avm_alu_rng_chk_sel, avm_alu_u16_r0, avm_alu_u16_r1, avm_alu_u16_r2,
avm_alu_u16_r3, avm_alu_u16_r4, avm_alu_u16_r5, avm_alu_u16_r6,
avm_alu_u8_r0, avm_alu_u8_r1, avm_binary_acc_ia, avm_binary_acc_ib,
avm_binary_acc_ic, avm_binary_mem_tag_ctr, avm_binary_op_id, avm_main_internal_return_ptr,
avm_main_pc, avm_mem_addr, avm_mem_rw, avm_mem_tag,
return { avm_alu_a_hi,
avm_alu_a_lo,
avm_alu_alu_sel,
avm_alu_b_hi,
avm_alu_b_lo,
avm_alu_cmp_rng_ctr,
avm_alu_cmp_sel,
avm_alu_op_add,
avm_alu_op_cast_prev,
avm_alu_op_cast,
avm_alu_op_mul,
avm_alu_op_sub,
avm_alu_p_sub_a_hi,
avm_alu_p_sub_a_lo,
avm_alu_p_sub_b_hi,
avm_alu_p_sub_b_lo,
avm_alu_rng_chk_lookup_selector,
avm_alu_rng_chk_sel,
avm_alu_u16_r0,
avm_alu_u16_r1,
avm_alu_u16_r2,
avm_alu_u16_r3,
avm_alu_u16_r4,
avm_alu_u16_r5,
avm_alu_u16_r6,
avm_alu_u8_r0,
avm_alu_u8_r1,
avm_binary_acc_ia,
avm_binary_acc_ib,
avm_binary_acc_ic,
avm_binary_mem_tag_ctr,
avm_binary_op_id,
avm_main_internal_return_ptr,
avm_main_pc,
avm_mem_addr,
avm_mem_rw,
avm_mem_tag,
avm_mem_val };
};

Expand Down

0 comments on commit 8843cec

Please sign in to comment.