feat(avm)!: Remove some range checks in bc decomposition subtrace (#16453)

Range checks related to setting the boolean asserting "WINDOWS >
bytes_remaining" have been removed and replaced by "standard relations".
The newly introduced relations leverage on "bytes_remaining" column
being a decrementing counter.
We set the selector to be 0 at the row where "bytes_remaining ==
WINDOWS" and 1 for the next row (bytes_remaining == WINDOWS - 1) and
then propagate value 0 to the top and value 1 to the bottom.

Benchmarks after this PR:
```
bc_decomposition_acc                                        7.54 us         7.54 us        92926
bc_decomposition_interactions_acc                          0.351 us        0.351 us      1988845
```

Benchmarks before this PR:
```
bc_decomposition_acc                                        7.35 us         7.35 us        94833
bc_decomposition_interactions_acc                           1.15 us         1.15 us       610300
```

   NUM_WITNESS_ENTITIES went from 2922 to 2917;
   NUM_SHIFTED_ENTITIES wnet from 315 to 316;

Author: jeanmon

barretenberg/cpp/pil/vm2/bytecode/bc_decomposition.pil

@@ -132,37 +132,45 @@ pol commit bytes_pc_plus_1, bytes_pc_plus_2, bytes_pc_plus_3, bytes_pc_plus_4, b
 //   39 |               1 |             1 |   0xD | 0x0 | 0x0 | ...
 
 pol commit bytes_to_read;
-pol commit sel_overflow_correction_needed;
-sel_overflow_correction_needed * (1 - sel_overflow_correction_needed) = 0;
+pol commit sel_windows_gt_remaining;
+sel_windows_gt_remaining * (1 - sel_windows_gt_remaining) = 0;
 // We need to constrain bytes_to_read = min(WINDOW_SIZE, bytes_remaining) which is equal to
 // bytes_remaining if bytes_remaining <= WINDOW_SIZE and WINDOW_SIZE otherwise.
 
-// Absolute value of WINDOW_SIZE - bytes_remaining
-pol commit abs_diff;
-// Remark: The factor sel in relation below is only required to use the skippable mechanism.
-// sel_overflow_correction_needed = 1 if bytes_remaining < WINDOW_SIZE and
-// sel_overflow_correction_needed = 0 if bytes_remaining > WINDOW_SIZE
-#[BC_DEC_ABS_DIFF]
-sel * (2 * sel_overflow_correction_needed * (WINDOW_SIZE - bytes_remaining) - WINDOW_SIZE + bytes_remaining - abs_diff) = 0;
+pol commit is_windows_eq_remaining;
+pol commit windows_min_remaining_inv;
+is_windows_eq_remaining * (1 - is_windows_eq_remaining) = 0;
 
-// We prove that the abs_diff is positive (and therefore sel_overflow_correction_needed correct) over the integers
-// using a range check over 24 bits. We know that WINDOWS_SIZE fits into 16 bits and bytes_remaining cannot be larger
-// than the trace size 2^21 (and bytecode hashing/validation could not pass). This provides guarantee that
-// abs_diff cannot be the result of an underflow. This would be only possible for bytes_remaining being very close
-// to the field order.
+// bytes_remaining == WINDOW_SIZE <==> is_windows_eq_remaining == 1
+#[IS_WINDOWS_EQ_REMAINING]
+sel * ((WINDOW_SIZE - bytes_remaining) * (is_windows_eq_remaining * (1 - windows_min_remaining_inv) + windows_min_remaining_inv) + is_windows_eq_remaining - 1) = 0;
 
-pol commit abs_diff_lo;
-pol commit abs_diff_hi;
-abs_diff = abs_diff_hi * 2**16 + abs_diff_lo;
 
-#[ABS_DIFF_LO_IS_U16]
-sel { abs_diff_lo } in precomputed.sel_range_16 { precomputed.clk };
-
-#[ABS_DIFF_HI_IS_U8]
-sel { abs_diff_hi } in precomputed.sel_range_8 { precomputed.clk };
-
-#[BC_DEC_OVERFLOW_CORRECTION_VALUE]
-sel * ((1 - sel_overflow_correction_needed) * (bytes_to_read - WINDOW_SIZE) + sel_overflow_correction_needed * (bytes_to_read - bytes_remaining)) = 0;
+// We want to constrain sel_windows_gt_remaining as follows:
+// sel_windows_gt_remaining = 1 if bytes_remaining < WINDOW_SIZE and
+// sel_windows_gt_remaining = 0 if bytes_remaining >= WINDOW_SIZE
+//
+// Instead of using range-checks/GT gadget to show an inequality, we leverage on the fact that bytes_remaining
+// is a decrementing counter.
+// So the pattern for sel_windows_gt_remaining bottom-up is: 1, 1, 1, ..., 1, 0, 0, 0, ...
+// where first 0 entry is at the row where bytes_remaining == WINDOW_SIZE.
+//
+// We initialize sel_windows_gt_remaining = 1 on last row of the bytecode
+// and propagate the boolean value to the above row whenever bytes_remaining != WINDOW_SIZE.
+// If we encounter the row where bytes_remaining == WINDOW_SIZE, we swap the boolean value.
+// Whenever the bytecode is smaller than WINDOW_SIZE, we exclusively propagate the value 1.
+
+// Set sel_windows_gt_remaining = 1 on the last row of the bytecode.
+#[SEL_WINDOWS_GT_REMAINING_INIT]
+last_of_contract * (1 - sel_windows_gt_remaining) = 0;
+
+// If we reach is_windows_eq_remaining == 1, we pass from 1 to 0. (Decrement a single time.)
+// sel_windows_gt_remaining = sel_windows_gt_remaining' - is_windows_eq_remaining
+#[SEL_WINDOWS_GT_REMAINING_PROPAGATION]
+(1 - FIRST_OR_LAST_CONTRACT) * (sel_windows_gt_remaining' - is_windows_eq_remaining - sel_windows_gt_remaining) = 0;
+
+#[SET_BYTES_TO_READ]
+sel * ((1 - sel_windows_gt_remaining) * (bytes_to_read - WINDOW_SIZE) + sel_windows_gt_remaining * (bytes_to_read - bytes_remaining)) = 0;
 
 // Constrain shifted columns.
 // We need to guard with (1 - FIRST_OR_LAST_CONTRACT) because otherwise we would need to copy value

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/bc_decomposition.test.cpp

@@ -21,6 +21,7 @@ namespace {
 using testing::random_bytes;
 using testing::random_contract_class;
 using tracegen::BytecodeTraceBuilder;
+using tracegen::DECOMPOSE_WINDOW_SIZE;
 using tracegen::TestTraceContainer;
 
 using FF = AvmFlavorSettings::FF;
@@ -256,21 +257,102 @@ TEST(BytecodeDecompositionConstrainingTest, NegativeMutateBytecodeId)
                               "BC_DEC_ID_CONSTANT");
 }
 
+// Both positive and negative tests for sel_windows_gt_remaining initialization
+TEST(BytecodeDecompositionConstrainingTest, SelWindowsGtRemainingInitialization)
+{
+    TestTraceContainer trace = TestTraceContainer::from_rows({
+        {
+            .bc_decomposition_last_of_contract = 1,
+            .bc_decomposition_sel = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 1,
+        },
+    });
+
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_INIT);
+
+    trace.set(C::bc_decomposition_sel_windows_gt_remaining, 0, 0); // Mutate to wrong value
+    EXPECT_THROW_WITH_MESSAGE(
+        check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_INIT),
+        "SEL_WINDOWS_GT_REMAINING_INIT");
+}
+
+// Both positive and negative tests for sel_windows_gt_remaining propagation without mutation.
+TEST(BytecodeDecompositionConstrainingTest, SelWindowsGtRemainingPropagation)
+{
+    TestTraceContainer trace = TestTraceContainer::from_rows({
+        {
+            .bc_decomposition_sel = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 1,
+        },
+        {
+            .bc_decomposition_last_of_contract = 1,
+            .bc_decomposition_sel = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 1,
+        },
+    });
+
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION);
+
+    trace.set(C::bc_decomposition_sel_windows_gt_remaining, 0, 0); // Mutate to wrong value at the top
+    EXPECT_THROW_WITH_MESSAGE(
+        check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION),
+        "SEL_WINDOWS_GT_REMAINING_PROPAGATION");
+
+    // Reset to correct value
+    trace.set(C::bc_decomposition_sel_windows_gt_remaining, 0, 1);
+
+    trace.set(C::bc_decomposition_sel_windows_gt_remaining, 1, 0); // Mutate to wrong value at the bottom
+    EXPECT_THROW_WITH_MESSAGE(
+        check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION),
+        "SEL_WINDOWS_GT_REMAINING_PROPAGATION");
+
+    // Test propagattion of 0 instead of 1
+    trace.set(C::bc_decomposition_sel_windows_gt_remaining, 0, 0); // Mutate to correct value
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION);
+}
+
+// Both positive and negative tests for sel_windows_gt_remaining propagation with mutation.
+TEST(BytecodeDecompositionConstrainingTest, SelWindowsGtRemainingPropagationWithMutation)
+{
+    TestTraceContainer trace = TestTraceContainer::from_rows({
+        {
+            .bc_decomposition_is_windows_eq_remaining = 1,
+            .bc_decomposition_sel = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 0,
+        },
+        {
+            .bc_decomposition_sel = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 1,
+        },
+        {
+            .bc_decomposition_last_of_contract = 1,
+            .bc_decomposition_sel = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 1,
+        },
+    });
+
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION);
+
+    trace.set(C::bc_decomposition_sel_windows_gt_remaining, 0, 1); // Mutate to wrong value
+    EXPECT_THROW_WITH_MESSAGE(
+        check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION),
+        "SEL_WINDOWS_GT_REMAINING_PROPAGATION");
+}
+
 TEST(BytecodeDecompositionConstrainingTest, NegativeWrongBytesToReadNoCorrection)
 {
     TestTraceContainer trace = TestTraceContainer::from_rows({
         {
             .bc_decomposition_bytes_remaining = 75,
-            .bc_decomposition_bytes_to_read = tracegen::DECOMPOSE_WINDOW_SIZE,
+            .bc_decomposition_bytes_to_read = DECOMPOSE_WINDOW_SIZE,
             .bc_decomposition_sel = 1,
         },
     });
 
-    check_relation<bc_decomposition>(trace, bc_decomposition::SR_BC_DEC_OVERFLOW_CORRECTION_VALUE);
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SET_BYTES_TO_READ);
     trace.set(C::bc_decomposition_bytes_to_read, 0, 75); // Mutate to wrong value (bytes_remaining)
-    EXPECT_THROW_WITH_MESSAGE(
-        check_relation<bc_decomposition>(trace, bc_decomposition::SR_BC_DEC_OVERFLOW_CORRECTION_VALUE),
-        "BC_DEC_OVERFLOW_CORRECTION_VALUE");
+    EXPECT_THROW_WITH_MESSAGE(check_relation<bc_decomposition>(trace, bc_decomposition::SR_SET_BYTES_TO_READ),
+                              "SET_BYTES_TO_READ");
 }
 
 TEST(BytecodeDecompositionConstrainingTest, NegativeWrongBytesToReadWithCorrection)
@@ -280,16 +362,14 @@ TEST(BytecodeDecompositionConstrainingTest, NegativeWrongBytesToReadWithCorrecti
             .bc_decomposition_bytes_remaining = 13,
             .bc_decomposition_bytes_to_read = 13,
             .bc_decomposition_sel = 1,
-            .bc_decomposition_sel_overflow_correction_needed = 1,
+            .bc_decomposition_sel_windows_gt_remaining = 1,
         },
     });
 
-    check_relation<bc_decomposition>(trace, bc_decomposition::SR_BC_DEC_OVERFLOW_CORRECTION_VALUE);
-    trace.set(
-        C::bc_decomposition_bytes_to_read, 0, tracegen::DECOMPOSE_WINDOW_SIZE); // Mutate to wrong value (WINDOWS_SIZE)
-    EXPECT_THROW_WITH_MESSAGE(
-        check_relation<bc_decomposition>(trace, bc_decomposition::SR_BC_DEC_OVERFLOW_CORRECTION_VALUE),
-        "BC_DEC_OVERFLOW_CORRECTION_VALUE");
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SET_BYTES_TO_READ);
+    trace.set(C::bc_decomposition_bytes_to_read, 0, DECOMPOSE_WINDOW_SIZE); // Mutate to wrong value
+    EXPECT_THROW_WITH_MESSAGE(check_relation<bc_decomposition>(trace, bc_decomposition::SR_SET_BYTES_TO_READ),
+                              "SET_BYTES_TO_READ");
 }
 
 TEST(BytecodeDecompositionConstrainingTest, NegativeWrongPacking)

barretenberg/cpp/src/barretenberg/vm2/generated/columns.hpp

@@ -129,10 +129,10 @@ namespace bb::avm2 {
 
 struct AvmFlavorVariables {
     static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 133;
-    static constexpr size_t NUM_WITNESS_ENTITIES = 2924;
-    static constexpr size_t NUM_SHIFTED_ENTITIES = 315;
+    static constexpr size_t NUM_WITNESS_ENTITIES = 2919;
+    static constexpr size_t NUM_SHIFTED_ENTITIES = 316;
     static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
-    static constexpr size_t NUM_ALL_ENTITIES = 3372;
+    static constexpr size_t NUM_ALL_ENTITIES = 3368;
 
     // Need to be templated for recursive verifier
     template <typename FF_>
@@ -243,8 +243,6 @@ struct AvmFlavorVariables {
         lookup_alu_range_check_trunc_mid_relation<FF_>,
         lookup_alu_register_tag_value_relation<FF_>,
         lookup_alu_tag_max_bits_value_relation<FF_>,
-        lookup_bc_decomposition_abs_diff_hi_is_u8_relation<FF_>,
-        lookup_bc_decomposition_abs_diff_lo_is_u16_relation<FF_>,
         lookup_bc_decomposition_bytes_are_bytes_relation<FF_>,
         lookup_bc_hashing_get_packed_field_relation<FF_>,
         lookup_bc_hashing_iv_is_len_relation<FF_>,

barretenberg/cpp/src/barretenberg/vm2/generated/flavor_variables.hpp

@@ -14,10 +14,10 @@ template <typename FF_> class bc_decompositionImpl {
   public:
     using FF = FF_;
 
-    static constexpr std::array<size_t, 52> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 4, 4, 5, 3, 4, 4, 3, 3, 4, 2, 4,
-                                                                            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, 3, 3 };
+    static constexpr std::array<size_t, 54> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 4, 4, 5, 3, 4, 4, 3, 3, 3, 5, 3, 3,
+                                                                            4, 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, 3, 3 };
 
     template <typename AllEntities> inline static bool skip(const AllEntities& in)
     {
@@ -54,13 +54,17 @@ template <typename FF> class bc_decomposition : public Relation<bc_decomposition
             return "BC_DEC_BYTES_REMAINING_DECREMENT";
         case 8:
             return "BC_DEC_ID_CONSTANT";
-        case 10:
-            return "BC_DEC_ABS_DIFF";
+        case 11:
+            return "IS_WINDOWS_EQ_REMAINING";
         case 12:
-            return "BC_DEC_OVERFLOW_CORRECTION_VALUE";
-        case 50:
+            return "SEL_WINDOWS_GT_REMAINING_INIT";
+        case 13:
+            return "SEL_WINDOWS_GT_REMAINING_PROPAGATION";
+        case 14:
+            return "SET_BYTES_TO_READ";
+        case 52:
             return "SEL_TOGGLED_AT_PACKED";
-        case 51:
+        case 53:
             return "BC_DECOMPOSITION_REPACKING";
         }
         return std::to_string(index);
@@ -74,10 +78,12 @@ template <typename FF> class bc_decomposition : public Relation<bc_decomposition
     static constexpr size_t SR_BC_DEC_PC_INCREMENT = 6;
     static constexpr size_t SR_BC_DEC_BYTES_REMAINING_DECREMENT = 7;
     static constexpr size_t SR_BC_DEC_ID_CONSTANT = 8;
-    static constexpr size_t SR_BC_DEC_ABS_DIFF = 10;
-    static constexpr size_t SR_BC_DEC_OVERFLOW_CORRECTION_VALUE = 12;
-    static constexpr size_t SR_SEL_TOGGLED_AT_PACKED = 50;
-    static constexpr size_t SR_BC_DECOMPOSITION_REPACKING = 51;
+    static constexpr size_t SR_IS_WINDOWS_EQ_REMAINING = 11;
+    static constexpr size_t SR_SEL_WINDOWS_GT_REMAINING_INIT = 12;
+    static constexpr size_t SR_SEL_WINDOWS_GT_REMAINING_PROPAGATION = 13;
+    static constexpr size_t SR_SET_BYTES_TO_READ = 14;
+    static constexpr size_t SR_SEL_TOGGLED_AT_PACKED = 52;
+    static constexpr size_t SR_BC_DECOMPOSITION_REPACKING = 53;
 };
 
 } // namespace bb::avm2