fix: vector_push_front is PureWithPredicate

compiler/noirc_evaluator/src/ssa/ir/instruction.rs

@@ -265,13 +265,38 @@ impl Intrinsic {
             | Intrinsic::VectorInsert
             | Intrinsic::VectorPushBack => Purity::PureWithPredicate,
 
+            // Unlike the vector operations above, `vector_push_front` needs no
+            // non-emptiness assertion and its ACIR lowering does not read the
+            // side-effects variable. It still must not be fully `Pure`: in Brillig it
+            // may write through its vector argument in place when the argument's
+            // runtime reference count is 1, so a pass that moves `Pure` calls freely
+            // (e.g. loop-invariant code motion) could separate it from the `inc_rc`
+            // that makes the mutation unobservable, or execute it on a path where the
+            // source program never runs it. The same applies to any Brillig function
+            // wrapping it, which inherits this purity through `purity_analysis`.
+            Intrinsic::VectorPushFront => Purity::PureWithPredicate,
+
             Intrinsic::AssertConstant
             | Intrinsic::StaticAssert
             | Intrinsic::ApplyRangeConstraint
             | Intrinsic::AsWitness => Purity::PureWithPredicate,
 
-            _ if self.has_side_effects() => Purity::Impure,
-            _ => Purity::Pure,
+            // Reference counts are runtime state stored next to the array contents:
+            // reading one is ordering-dependent on the rc traffic around it, so these
+            // calls cannot be moved or deduplicated.
+            Intrinsic::ArrayRefCount | Intrinsic::VectorRefCount => Purity::Impure,
+
+            // Deliberately opaque to the optimizer.
+            Intrinsic::Hint(Hint::BlackBox) => Purity::Impure,
+
+            Intrinsic::ArrayLen
+            | Intrinsic::ArrayAsStrUnchecked
+            | Intrinsic::AsVector
+            | Intrinsic::StrAsBytes
+            | Intrinsic::IsUnconstrained
+            | Intrinsic::DerivePedersenGenerators
+            | Intrinsic::FieldLessThan
+            | Intrinsic::BlackBox(_) => Purity::Pure,
         }
     }
 

compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs

@@ -2905,6 +2905,49 @@ mod tests {
         assert_eq!(can_be_hoisted(&instruction, &function.dfg), result);
     }
 
+    #[test]
+    fn hoisting_vector_mutator_out_of_loop_drops_refcount_guard() {
+        // Reproduction for the AST fuzzer `pass_vs_prev` failure on seed 0xb6bc8e1f00100000,
+        // bisected to the Loop Invariant Code Motion pass.
+        //
+        // Brillig arrays are copy-on-write: `vector_push_front` writes through its input vector in
+        // place once the operand's reference count is 1. Inside the loop the operand `v1` is
+        // protected by the `inc_rc v1` immediately before the call, because `v1` is still read by
+        // the `array_get` in `b3`. The `inc_rc` guard is never hoisted, so the call must not be
+        // hoisted either: separated from its guard, the hoisted push would mutate `v1` in place
+        // and corrupt the value `b3` reads. `vector_push_front` is `PureWithPredicate` exactly so
+        // that LICM leaves it in the loop body, behind the guard.
+        //
+        // `assert_pass_does_not_affect_execution` interprets before and after LICM and panics when
+        // the results differ.
+        let src = r#"
+        brillig(inline) impure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [v0, u1 1] : [u1]
+            v2 = call f1(u32 2, v1) -> u1
+            return v2
+        }
+        brillig(inline) impure fn foo f1 {
+          b0(v0: u32, v1: [u1]):
+            jmp b1(u32 0)
+          b1(v2: u32):
+            v3 = lt v2, u32 2
+            jmpif v3 then: b2(), else: b3()
+          b2():
+            inc_rc v1
+            v4, v5 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
+            v6 = unchecked_add v2, u32 1
+            jmp b1(v6)
+          b3():
+            v7 = array_get v1, index u32 0 -> u1
+            return v7
+        }
+        "#;
+        let ssa = Ssa::from_str(src).unwrap();
+        let input = vec![crate::ssa::interpreter::value::Value::bool(true)];
+        let _ = assert_pass_does_not_affect_execution(ssa, input, Ssa::loop_invariant_code_motion);
+    }
+
     #[test]
     fn inserts_inc_rc_for_hoisted_array_set() {
         // The SSA below has been captured during the pre-processing of functions in the following:

test_programs/execution_success/regression_licm_vector_mutator/Nargo.toml

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

test_programs/execution_success/regression_licm_vector_mutator/Prover.toml

@@ -0,0 +1,3 @@
+x = true
+n = 1
+return = true

test_programs/execution_success/regression_licm_vector_mutator/src/main.nr

@@ -0,0 +1,33 @@
+// Regression test for loop-invariant code motion hoisting a Brillig vector
+// mutator (`vector_push_front`) into the loop pre-header while the `inc_rc`
+// guarding its vector operand stays behind in the loop body. Separated from
+// its guard, the hoisted push finds the vector at refcount 1 and mutates it
+// in place, corrupting `v` for the read after the loop.
+// See https://github.com/noir-lang/noir-claude/issues/244.
+//
+// Each piece below defeats a mechanism that otherwise masks the bug:
+// - `v`'s length must be dynamic (the `0..n` push loop), otherwise the vector
+//   intrinsics are constant-folded away before LICM runs.
+// - `v` must reach the second loop with spare capacity and refcount 1: a push
+//   only reuses its operand's storage when the new size fits the capacity.
+//   `as_vector()` gives capacity == size, so with `n = 0` the hoisted push
+//   harmlessly reallocates; the reallocating `push_back` (with `n = 1`)
+//   doubles the capacity, letting the next push mutate in place.
+// - `v` must not be used between the two loops: any use there would emit a
+//   clone (`inc_rc`) in the pre-header, accidentally guarding the hoisted push.
+// - The `0..2` loop is guaranteed to execute (a requirement for hoisting the
+//   call) and `acc` keeps the push alive through dead instruction elimination.
+unconstrained fn main(x: bool, n: u32) -> pub bool {
+    let mut v = [x].as_vector();
+    for _ in 0..n {
+        v = v.push_back(x);
+    }
+    let mut acc = 0;
+    for _ in 0..2 {
+        acc += v.push_front(false).len();
+    }
+    assert(acc > 0);
+    // `push_front` returns a new vector, so `v` itself must be unchanged.
+    assert(v[0] == x);
+    v[0]
+}

test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Nargo.toml

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

test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml

@@ -0,0 +1,4 @@
+x = true
+n = 1
+m = 0
+return = true

test_programs/execution_success/regression_licm_vector_mutator_empty_loop/src/main.nr

@@ -0,0 +1,13 @@
+unconstrained fn main(x: bool, n: u32, m: u32) -> pub bool {
+    let mut v = [x].as_vector();
+    for _ in 0..n {
+        v = v.push_back(x);
+    }
+    let mut acc = 0;
+    for _ in 0..m {
+        acc += v.push_front(false).len();
+    }
+    assert(acc == 0);
+    assert(v[0] == x);
+    v[0]
+}

test_programs/execution_success/regression_licm_vector_mutator_wrapper/Nargo.toml

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

test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml

@@ -0,0 +1,3 @@
+x = true
+n = 1
+return = true

test_programs/execution_success/regression_licm_vector_mutator_wrapper/src/main.nr

@@ -0,0 +1,22 @@
+fn helper(v: [bool]) -> Field {
+    let mut len = v.push_front(false).len() as Field;
+    for _ in 0..10 {
+        len = len * 3 + 1;
+    }
+    len
+}
+
+unconstrained fn main(x: bool, n: u32) -> pub bool {
+    let mut v = [x].as_vector();
+    for _ in 0..n {
+        v = v.push_back(x);
+    }
+    let mut acc = 0;
+    for _ in 0..2 {
+        acc += helper(v);
+    }
+    assert(acc != 0);
+    assert(helper(v) != 0);
+    assert(v[0] == x);
+    v[0]
+}