fix: track MakeArray elements as Brillig call arguments in underconstrained check

compiler/noirc_evaluator/src/ssa/checks/check_for_missing_brillig_constraints.rs

@@ -47,6 +47,7 @@ use crate::ssa::ir::function::{Function, FunctionId};
 use crate::ssa::ir::instruction::{Instruction, InstructionId, Intrinsic};
 use crate::ssa::ir::value::{Value, ValueId};
 use crate::ssa::ssa_gen::Ssa;
+use crate::ssa::visit_once_deque::VisitOnceDeque;
 use noirc_artifacts::ssa::{InternalBug, SsaReport};
 use noirc_errors::Location;
 use rayon::prelude::*;
@@ -347,7 +348,12 @@ impl DependencyContext {
                         return;
                     }
 
-                    let current_tainted = BrilligTaintedIds::new(function, arguments, results);
+                    // Expand arguments through MakeArray chains so that
+                    // array element values are also tracked as call arguments
+                    // (e.g. for `v1 = make_array [v0]; call f(v1)`, track v0 too)
+                    let expanded_args = expand_args_through_make_array(function, arguments);
+
+                    let current_tainted = BrilligTaintedIds::new(function, &expanded_args, results);
 
                     // Record arguments/results for each Brillig call for the check.
                     //
@@ -366,7 +372,7 @@ impl DependencyContext {
                     if !wrapped_call_found {
                         // Record the current call, remember the argument values involved
                         self.tainted.insert(*instruction, current_tainted);
-                        arguments.iter().for_each(|value| {
+                        expanded_args.iter().for_each(|value| {
                             self.call_arguments.entry(*value).or_default().push(*instruction);
                         });
                     }
@@ -412,7 +418,10 @@ impl DependencyContext {
                                 // (fixes #10547)
                                 if matches!(
                                     &function.dfg[*instruction],
-                                    Instruction::Cast(..) | Instruction::Truncate { .. }
+                                    Instruction::Cast(..)
+                                        | Instruction::Truncate { .. }
+                                        | Instruction::MakeArray { .. }
+                                        | Instruction::ArraySet { .. }
                                 ) && let Some(tainted_ids) = self.tainted.get_mut(call)
                                 {
                                     tainted_ids.arguments.extend(&arguments);
@@ -538,6 +547,7 @@ impl DependencyContext {
                         self.update_children(&arguments, &results);
                     }
                     Instruction::ArraySet { .. }
+                    | Instruction::MakeArray { .. }
                     | Instruction::Binary(..)
                     | Instruction::Cast(..)
                     | Instruction::IfElse { .. }
@@ -550,7 +560,6 @@ impl DependencyContext {
                     Instruction::Allocate
                     | Instruction::DecrementRc { .. }
                     | Instruction::IncrementRc { .. }
-                    | Instruction::MakeArray { .. }
                     | Instruction::Noop => {}
                 }
             }
@@ -664,6 +673,38 @@ fn intersecting<T: Hash + Eq>(a: &HashSet<T>, b: &HashSet<T>) -> bool {
     a.intersection(b).next().is_some()
 }
 
+/// Expand a set of call arguments by tracing through MakeArray and ArraySet instructions.
+/// For example, if arguments contains v1 where `v1 = make_array [v0]`,
+/// the result will contain both v1 and v0. For `v2 = array_set v1, index .., value v3`,
+/// the result will contain v2, v3, and (recursively) the contents of v1.
+/// Works recursively for nested arrays and chained array_sets.
+fn expand_args_through_make_array(function: &Function, arguments: &[ValueId]) -> Vec<ValueId> {
+    let mut queue = VisitOnceDeque::default();
+    queue.extend(arguments.iter().copied());
+    let mut expanded = Vec::new();
+    while let Some(arg) = queue.pop_front() {
+        expanded.push(arg);
+        let Value::Instruction { instruction, .. } = &function.dfg[arg] else { continue };
+        match &function.dfg[*instruction] {
+            Instruction::MakeArray { elements, .. } => {
+                let non_constant_elements =
+                    elements.iter().copied().filter(|elem| !is_numeric_constant(function, *elem));
+                queue.extend(non_constant_elements);
+            }
+            Instruction::ArraySet { array, value, .. } => {
+                // Trace the source array (may be another ArraySet or MakeArray)
+                queue.push_back(*array);
+                // Trace the inserted value (contributes to the array content)
+                if !is_numeric_constant(function, *value) {
+                    queue.push_back(*value);
+                }
+            }
+            _ => {}
+        }
+    }
+    expanded
+}
+
 #[cfg(test)]
 mod tests {
     use crate::ssa::Ssa;
@@ -1209,22 +1250,45 @@ mod tests {
 
     #[test]
     #[traced_test]
-    #[should_panic = "Expected no warnings but found some."]
     fn constrain_on_array_element_links_to_input_array() {
         // Regression test for https://github.com/noir-lang/noir/issues/11807
         let program = r#"
         acir(inline) predicate_pure fn main f0 {
           b0(v0: Field):
             v1 = make_array [v0] : [Field; 1]
-            v3 = call f1(v1) -> [Field; 1]          // We pass v1 = [v0] to the Brillig function.
-            v5 = array_get v3, index u32 0 -> Field
-            constrain v5 == v0                      // We constrain the result directly against v0, which should clear the Brillig call.
+            v3 = call f1(v1) -> Field
+            constrain v3 == v0
             return v3
         }
         brillig(inline) predicate_pure fn helper_func f1 {
           b0(v0: [Field; 1]):
-            v2 = array_get v0, index u32 1 minus 1 -> Field
-            v3 = make_array [v2] : [Field; 1]
+            v2 = array_get v0, index u32 0 -> Field
+            return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true);
+        assert_eq!(ssa_level_warnings.len(), 0, "Expected no warnings but found some.");
+    }
+
+    #[test]
+    #[traced_test]
+    fn constrain_on_nested_array_element_links_to_input_array() {
+        // Nested array variant: [[Field; 1]; 1] wrapping v0
+        let program = r#"
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: Field):
+            v1 = make_array [v0] : [Field; 1]
+            v2 = make_array [v1] : [[Field; 1]; 1]
+            v4 = call f1(v2) -> Field
+            constrain v4 == v0
+            return v4
+        }
+        brillig(inline) predicate_pure fn helper_func f1 {
+          b0(v0: [[Field; 1]; 1]):
+            v2 = array_get v0, index u32 0 -> [Field; 1]
+            v3 = array_get v2, index u32 0 -> Field
             return v3
         }
         "#;
@@ -1233,4 +1297,98 @@ mod tests {
         let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true);
         assert_eq!(ssa_level_warnings.len(), 0, "Expected no warnings but found some.");
     }
+
+    #[test]
+    #[traced_test]
+    fn array_set_with_variable_index_constrain_against_set_value() {
+        // Array built from constants, then array_set with a non-constant index
+        // inserts v0. Brillig result constrained against v0.
+        let program = r#"
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: Field, v1: u32):
+            v2 = make_array [Field 0, Field 0] : [Field; 2]
+            v3 = array_set v2, index v1, value v0
+            v4 = call f1(v3) -> Field
+            constrain v4 == v0
+            return v4
+        }
+        brillig(inline) predicate_pure fn helper_func f1 {
+          b0(v0: [Field; 2]):
+            v2 = array_get v0, index u32 0 -> Field
+            return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true);
+        assert_eq!(
+            ssa_level_warnings.len(),
+            0,
+            "Expected no warnings: array_set value should be tracked as a call argument."
+        );
+    }
+
+    #[test]
+    #[traced_test]
+    fn array_set_on_param_array_constrain_against_original_element() {
+        // make_array [v0, v1], then array_set at non-constant index with v0.
+        // Brillig result constrained against v0 (which is both in the original
+        // make_array AND the array_set value).
+        let program = r#"
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: Field, v1: Field, v2: u32):
+            v3 = make_array [v0, v1] : [Field; 2]
+            v4 = array_set v3, index v2, value v0
+            v5 = call f1(v4) -> Field
+            constrain v5 == v0
+            return v5
+        }
+        brillig(inline) predicate_pure fn helper_func f1 {
+          b0(v0: [Field; 2]):
+            v2 = array_get v0, index u32 0 -> Field
+            return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true);
+        assert_eq!(
+            ssa_level_warnings.len(),
+            0,
+            "Expected no warnings: array_set on make_array with params, constrained against original element."
+        );
+    }
+
+    #[test]
+    #[traced_test]
+    fn array_set_constrain_result_array_elements() {
+        // Brillig returns an array. We array_get each element and constrain
+        // against the values used in the array_set. Since the Brillig call's
+        // result is an array, the checker uses array element tracking.
+        let program = r#"
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: Field, v1: Field, v2: u32):
+            v3 = make_array [v0, Field 0] : [Field; 2]
+            v4 = array_set v3, index v2, value v1
+            v5 = call f1(v4) -> [Field; 2]
+            v6 = array_get v5, index u32 0 -> Field
+            v7 = array_get v5, index u32 1 -> Field
+            constrain v6 == v0
+            constrain v7 == v1
+            return
+        }
+        brillig(inline) predicate_pure fn helper_func f1 {
+          b0(v0: [Field; 2]):
+            return v0
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true);
+        assert_eq!(
+            ssa_level_warnings.len(),
+            0,
+            "Expected no warnings: both array elements constrained against inputs."
+        );
+    }
 }