From 8843cec04bed45ee071046d8c67d090e000635fc Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 18 Apr 2024 12:12:35 +0000 Subject: [PATCH] 5466: Add PIL relation to prevent overlap in second row of CAST and 128-bit multiplication in ALU trace --- barretenberg/cpp/pil/avm/avm_alu.pil | 12 +- .../relations/generated/avm/avm_alu.hpp | 31 ++-- .../relations/generated/avm/declare_views.hpp | 1 + .../vm/generated/avm_circuit_builder.hpp | 4 +- .../barretenberg/vm/generated/avm_flavor.hpp | 151 +++++++++++++----- 5 files changed, 140 insertions(+), 59 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 2150542e686..cc39ef9ca7e 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -497,11 +497,6 @@ 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; @@ -509,4 +504,9 @@ namespace avm_alu(256); 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; \ No newline at end of file + 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; \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp index ea21fba5789..ac09315024a 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -12,6 +12,7 @@ template 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{}; @@ -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); } @@ -201,7 +202,7 @@ template class avm_aluImpl { static constexpr std::array 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 @@ -763,14 +764,6 @@ template 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) + @@ -791,13 +784,21 @@ template 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; } @@ -805,7 +806,7 @@ template class avm_aluImpl { { 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; } diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp index 5531e8131b0..e427a1bf7be 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -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); \ diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp index 221702456b1..4bfaa9fa499 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -268,6 +268,7 @@ template 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{}; @@ -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 rows; @@ -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()); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index fbd3f58d4c8..bcdaabdbd6c 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp @@ -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_bin_relation, @@ -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, @@ -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, @@ -1338,37 +1340,84 @@ class AvmFlavor { }; RefVector 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 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 }; }; }; @@ -1382,15 +1431,43 @@ class AvmFlavor { RefVector 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 }; };