fix(acir): guard empty vector pop/remove on the semantic length

compiler/noirc_evaluator/src/acir/call/intrinsics/vector_ops.rs

@@ -386,8 +386,14 @@ impl Context<'_> {
         let vector_type = dfg.type_of_value(vector_contents_id);
         self.check_vector_result_count("vector_pop_back", result_ids, &vector_type)?;
 
-        // Check if we're trying to pop from a known empty vector.
-        if self.has_zero_length(vector_contents_id, dfg) {
+        let vector_length_var = vector_length_value.clone().into_var()?;
+
+        // Check if we're trying to pop from a known empty vector: one whose backing store
+        // is empty, or one whose semantic length is known to be zero (its backing store may
+        // still be non-empty padding in that case).
+        if self.has_zero_length(vector_contents_id, dfg)
+            || self.vector_length_is_known_zero(dfg, vector_length_id, vector_length_var)
+        {
             // Make sure this code is disabled, or fail with the empty-vector pop message.
             let msg = "Attempt to pop from an empty vector".to_string();
             self.acir_context.assert_zero_var(self.current_side_effects_enabled_var, msg)?;
@@ -451,6 +457,25 @@ impl Context<'_> {
         Ok(results)
     }
 
+    /// Whether the vector's semantic length is known to be zero at this point: either the
+    /// SSA value is the constant zero, or its ACIR expression has folded to zero (which
+    /// happens when the side-effects predicate it was multiplied by collapsed to a
+    /// constant). The backing store cannot answer this question — merging branch arms of
+    /// unequal lengths pads the shorter arm, so a semantically empty vector may still have
+    /// a non-empty backing store, and `has_zero_length` inspects that backing store.
+    fn vector_length_is_known_zero(
+        &self,
+        dfg: &DataFlowGraph,
+        vector_length_id: ValueId,
+        vector_length_var: AcirVar,
+    ) -> bool {
+        let length_const = dfg.get_numeric_constant(vector_length_id).or_else(|| {
+            let expr = self.acir_context.var_to_expression(vector_length_var).ok()?;
+            expr.to_const().copied()
+        });
+        length_const.is_some_and(|length| length.is_zero())
+    }
+
     /// Compute the new vector length after popping one value from it.
     ///
     /// Assumes that we already handled the constant zero case.
@@ -547,8 +572,14 @@ impl Context<'_> {
         self.check_vector_result_count("vector_pop_front", result_ids, &vector_type)?;
         let element_size = vector_type.element_size();
 
-        // Check if we're trying to pop from a known empty vector.
-        if self.has_zero_length(vector_contents_id, dfg) {
+        let vector_length_var = vector_length_value.clone().into_var()?;
+
+        // Check if we're trying to pop from a known empty vector: one whose backing store
+        // is empty, or one whose semantic length is known to be zero (its backing store may
+        // still be non-empty padding in that case).
+        if self.has_zero_length(vector_contents_id, dfg)
+            || self.vector_length_is_known_zero(dfg, vector_length_id, vector_length_var)
+        {
             // Make sure this code is disabled, or fail with the empty-vector pop message.
             let msg = "Attempt to pop from an empty vector".to_string();
             self.acir_context.assert_zero_var(self.current_side_effects_enabled_var, msg)?;
@@ -873,8 +904,13 @@ impl Context<'_> {
         let vector_typ = dfg.type_of_value(vector_contents);
         self.check_vector_result_count("vector_remove", result_ids, &vector_typ)?;
 
-        // Check if we're trying to remove from an empty vector
-        if self.has_zero_length(vector_contents, dfg) {
+        // Check if we're trying to remove from a known empty vector: one whose backing store
+        // is empty, or one whose semantic length is known to be zero (its backing store may
+        // still be non-empty padding in that case). Without the semantic-length check a length
+        // that has folded to zero reaches the `sub_var(length, 1)` below and produces `p - 1`.
+        if self.has_zero_length(vector_contents, dfg)
+            || self.vector_length_is_known_zero(dfg, arguments[0], vector_length)
+        {
             // Make sure this code is disabled, or fail with "Index out of bounds".
             let msg = "Index out of bounds, vector has size 0".to_string();
             self.acir_context.assert_zero_var(self.current_side_effects_enabled_var, msg)?;

test_programs/execution_success/vector_ops_collapsed_predicate/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "vector_ops_collapsed_predicate"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/vector_ops_collapsed_predicate/Prover.toml

@@ -0,0 +1,4 @@
+g0 = true
+d = false
+i = 0
+return = 0

test_programs/execution_success/vector_ops_collapsed_predicate/src/main.nr

@@ -0,0 +1,23 @@
+// Popping from a statically-empty slice inside a conditional collapses the branch
+// predicate to a constant zero at the ACIR level (the empty-pop assertion pins it),
+// which in turn folds the length of an unrelated, still-live slice to a constant zero.
+// A subsequent `remove` on that slice must not turn the folded length into `0 - 1` in
+// the field: `push_back` consumes the result as a `u32` length, and the compiler must
+// not crash converting it. With `g0 = true` the branch is inactive and `main` returns 0.
+fn main(g0: bool, d: bool, i: u32) -> pub Field {
+    let v = @[1];
+    let mut w = @[1];
+    if d {
+        w = w.push_back(5);
+    }
+    let mut out = 0;
+    if !g0 {
+        let (v2, _a) = v.remove(i);
+        let (_v3, _b) = v2.pop_back();
+        let (w2, _c) = w.pop_back();
+        let (w3, _e) = w2.remove(i);
+        let w4 = w3.push_back(9);
+        out = w4[0];
+    }
+    out
+}