From 21c2eafb2dbbe9f589b6f2fa75a8f55fabd2b193 Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Mon, 3 Aug 2026 13:38:59 +0000
Subject: [PATCH 01/12] chore: reproduce LICM miscompiling a hoisted Brillig
 vector mutator (AST fuzzer)

---
 .../src/ssa/opt/loop_invariant.rs             | 45 +++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index 0795542f9bc..c83047c6a34 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -2905,6 +2905,51 @@ mod tests {
         assert_eq!(can_be_hoisted(&instruction, &function.dfg), result);
     }
 
+    #[test]
+    #[should_panic(expected = "SSA pass has resulted in a different execution result")]
+    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`. `vector_push_front` is `PureWithPredicate`, so LICM hoists the
+        // call into the pre-header — but the `inc_rc` guard is a separate instruction that is never
+        // hoisted. Separated from its guard, the hoisted push mutates `v1` in place and corrupts the
+        // value `b3` reads, so the pass changes the program's result.
+        //
+        // `assert_pass_does_not_affect_execution` interprets before and after LICM and panics when
+        // they differ, which they do on `master`. Once LICM re-establishes the `inc_rc` on hoisted
+        // vector-mutator operands the results match and the `#[should_panic]` should be removed.
+        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:

From 2a75f196d569d5ab8aaf4e2fa80e4af5dde33eef Mon Sep 17 00:00:00 2001
From: Ary Borenszweig <asterite@gmail.com>
Date: Mon, 3 Aug 2026 12:21:48 -0300
Subject: [PATCH 02/12] chore: add failing source-level regression test for the
 LICM vector mutator hoist

The miscompilation is reachable from plain Noir source, not just
hand-written SSA: with x = true, n = 1 the program returns false on the
base commit because the hoisted vector_push_front mutates v in place.
The test asserts the correct semantics, so it stays red until LICM keeps
(or re-establishes) the inc_rc guard on the hoisted mutator's operands.

Reaching the bug from source requires defeating three masking
mechanisms, documented in the test: a dynamic vector length (constant
lengths fold before LICM), spare capacity with refcount 1 at the
pre-header (a fresh as_vector() reallocates harmlessly), and no use of
the vector between the loops (which would emit a guarding inc_rc clone
in the pre-header).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .../regression_licm_vector_mutator/Nargo.toml |  6 ++++
 .../Prover.toml                               |  2 ++
 .../src/main.nr                               | 33 +++++++++++++++++++
 3 files changed, 41 insertions(+)
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator/Nargo.toml
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator/Prover.toml
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator/src/main.nr

diff --git a/test_programs/execution_success/regression_licm_vector_mutator/Nargo.toml b/test_programs/execution_success/regression_licm_vector_mutator/Nargo.toml
new file mode 100644
index 00000000000..d234f126aa7
--- /dev/null
+++ b/test_programs/execution_success/regression_licm_vector_mutator/Nargo.toml
@@ -0,0 +1,6 @@
+[package]
+name = "regression_licm_vector_mutator"
+type = "bin"
+authors = [""]
+
+[dependencies]
diff --git a/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml b/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml
new file mode 100644
index 00000000000..13547c55a3d
--- /dev/null
+++ b/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml
@@ -0,0 +1,2 @@
+x = true
+n = 1
diff --git a/test_programs/execution_success/regression_licm_vector_mutator/src/main.nr b/test_programs/execution_success/regression_licm_vector_mutator/src/main.nr
new file mode 100644
index 00000000000..e87c425186e
--- /dev/null
+++ b/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]
+}

From fd8540b71c4f5a3ebf5395de42ac0bbb31e752dc Mon Sep 17 00:00:00 2001
From: Ary Borenszweig <asterite@gmail.com>
Date: Mon, 3 Aug 2026 12:38:09 -0300
Subject: [PATCH 03/12] chore: add failing regression test for the LICM hoist
 of a pure wrapper around a vector mutator

Source-level variant of the user-function-wrapper bypass described in
https://gist.github.com/AztecBot/b4b227ffacd5e2cc17e703255e98c22b: LICM
hoists calls to user functions by recorded callee purity, so a fix that
only guards hoisted intrinsic calls would leave this test red.

Under low inliner aggressiveness (exercised by the CI inliner matrix)
the wrapper survives to LICM as a real call and is hoisted away from
its inc_rc guard; under high aggressiveness it inlines and reduces to
the direct-intrinsic case. Keeping the wrapper alive from source needs
a loop in its body (defeats simple-function inlining), two call sites
(defeats always-inline-when-called-once), and Field arithmetic (checked
u32 ops would make it PureWithPredicate, whose hoisting path is blocked
by the preceding side-effecting inc_rc; only fully-pure callees hoist
unconditionally).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .../Nargo.toml                                |  6 +++++
 .../Prover.toml                               |  2 ++
 .../src/main.nr                               | 22 +++++++++++++++++++
 3 files changed, 30 insertions(+)
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator_wrapper/Nargo.toml
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator_wrapper/src/main.nr

diff --git a/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Nargo.toml b/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Nargo.toml
new file mode 100644
index 00000000000..57a4baa8c3d
--- /dev/null
+++ b/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]
diff --git a/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml b/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml
new file mode 100644
index 00000000000..13547c55a3d
--- /dev/null
+++ b/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml
@@ -0,0 +1,2 @@
+x = true
+n = 1
diff --git a/test_programs/execution_success/regression_licm_vector_mutator_wrapper/src/main.nr b/test_programs/execution_success/regression_licm_vector_mutator_wrapper/src/main.nr
new file mode 100644
index 00000000000..2be8d1aecf7
--- /dev/null
+++ b/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]
+}

From c103e047ec3a245d784095ac0c410287948b1e37 Mon Sep 17 00:00:00 2001
From: Ary Borenszweig <asterite@gmail.com>
Date: Mon, 3 Aug 2026 13:03:50 -0300
Subject: [PATCH 04/12] chore: add failing regression test for LICM
 speculatively hoisting a vector mutator out of an empty loop

Third source-level shape of the miscompilation, distinct from the
stranded-guard cases: with m = 0 the push_front loop never executes,
yet v is still corrupted. The fully-Pure branch of can_hoist_invariant
checks neither does_execute nor block impurity, so the hoisted mutator
runs once in the pre-header of a zero-iteration loop; assert(acc == 0)
passes while assert(v[0] == x) fails.

This also pins down that inserting a pre-header inc_rc alone is not a
sufficient fix for the Pure path: the hoisted push must not execute
speculatively at all (today a copying push is only harmless because
its result is dead).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .../Nargo.toml                                      |  6 ++++++
 .../Prover.toml                                     |  3 +++
 .../src/main.nr                                     | 13 +++++++++++++
 3 files changed, 22 insertions(+)
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Nargo.toml
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml
 create mode 100644 test_programs/execution_success/regression_licm_vector_mutator_empty_loop/src/main.nr

diff --git a/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Nargo.toml b/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Nargo.toml
new file mode 100644
index 00000000000..4c768feb8b5
--- /dev/null
+++ b/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]
diff --git a/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml b/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml
new file mode 100644
index 00000000000..750db086b2a
--- /dev/null
+++ b/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml
@@ -0,0 +1,3 @@
+x = true
+n = 1
+m = 0
diff --git a/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/src/main.nr b/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/src/main.nr
new file mode 100644
index 00000000000..d0903b7c796
--- /dev/null
+++ b/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]
+}

From 62280b8b8a4b2daf24719de81a270c71bdc5e9d8 Mon Sep 17 00:00:00 2001
From: Ary Borenszweig <asterite@gmail.com>
Date: Mon, 3 Aug 2026 14:22:11 -0300
Subject: [PATCH 05/12] fix(ssa): classify vector_push_front as
 PureWithPredicate so LICM keeps it behind its inc_rc guard

vector_push_front was the only vector mutator classified fully Pure: it
needs no non-emptiness assertion and its ACIR lowering does not read the
side-effects variable, so it fell through purity()'s catch-all. But in
Brillig it can write through its vector argument in place when the
argument's runtime reference count is 1, and the fully-Pure hoisting
path in loop-invariant code motion checks neither block impurity nor
whether the loop executes. LICM therefore hoisted the call into the
pre-header, away from the inc_rc guarding its operand (or into a path
the source program never executes), mutating a still-live vector in
place.

Classifying it PureWithPredicate routes it through the predicated
hoisting path, which refuses to move it past the side-effecting inc_rc
the ownership pass emits directly before it and refuses to hoist it out
of loops that may not execute. Functions wrapping the intrinsic inherit
the classification through purity analysis, closing the pure-wrapper
bypass as well.

Also replaces purity()'s catch-all arms with an exhaustive enumeration
so future intrinsics require an explicit purity decision.

The regression test loses its #[should_panic]: interpreting before and
after LICM now agrees. The three execution_success programs
(regression_licm_vector_mutator{,_wrapper,_empty_loop}) turn green,
including the wrapper variant under minimum inliner aggressiveness,
where the wrapper survives to LICM as a real call.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .../noirc_evaluator/src/ssa/ir/instruction.rs | 29 +++++++++++++++++--
 .../src/ssa/opt/loop_invariant.rs             | 12 ++++----
 2 files changed, 32 insertions(+), 9 deletions(-)

diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs
index f6ef839faf8..8f5a9ab8a0a 100644
--- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs
+++ b/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,
         }
     }
 
diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index c83047c6a34..2fec8bee5bf 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -2906,7 +2906,6 @@ mod tests {
     }
 
     #[test]
-    #[should_panic(expected = "SSA pass has resulted in a different execution result")]
     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.
@@ -2914,14 +2913,13 @@ mod tests {
         // 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`. `vector_push_front` is `PureWithPredicate`, so LICM hoists the
-        // call into the pre-header — but the `inc_rc` guard is a separate instruction that is never
-        // hoisted. Separated from its guard, the hoisted push mutates `v1` in place and corrupts the
-        // value `b3` reads, so the pass changes the program's result.
+        // 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
-        // they differ, which they do on `master`. Once LICM re-establishes the `inc_rc` on hoisted
-        // vector-mutator operands the results match and the `#[should_panic]` should be removed.
+        // the results differ.
         let src = r#"
         brillig(inline) impure fn main f0 {
           b0(v0: u1):

From b26cee3138d1eedcebac5ae0e7a0122d725e5efb Mon Sep 17 00:00:00 2001
From: Ary Borenszweig <asterite@gmail.com>
Date: Mon, 3 Aug 2026 14:55:44 -0300
Subject: [PATCH 06/12] Snapshots and Prover.toml return value

---
 .../Prover.toml                               |  1 +
 .../Prover.toml                               |  1 +
 .../Prover.toml                               |  1 +
 .../execute__tests__expanded.snap             | 20 +++++++++++++
 .../execute__tests__stdout.snap               |  5 ++++
 .../execute__tests__expanded.snap             | 20 +++++++++++++
 .../execute__tests__stdout.snap               |  5 ++++
 .../execute__tests__expanded.snap             | 29 +++++++++++++++++++
 .../execute__tests__stdout.snap               |  5 ++++
 9 files changed, 87 insertions(+)
 create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__expanded.snap
 create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__stdout.snap
 create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__expanded.snap
 create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__stdout.snap
 create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__expanded.snap
 create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__stdout.snap

diff --git a/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml b/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml
index 13547c55a3d..9337e2fdb6d 100644
--- a/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml
+++ b/test_programs/execution_success/regression_licm_vector_mutator/Prover.toml
@@ -1,2 +1,3 @@
 x = true
 n = 1
+return = true
diff --git a/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml b/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml
index 750db086b2a..e1dcebdee86 100644
--- a/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml
+++ b/test_programs/execution_success/regression_licm_vector_mutator_empty_loop/Prover.toml
@@ -1,3 +1,4 @@
 x = true
 n = 1
 m = 0
+return = true
diff --git a/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml b/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml
index 13547c55a3d..9337e2fdb6d 100644
--- a/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml
+++ b/test_programs/execution_success/regression_licm_vector_mutator_wrapper/Prover.toml
@@ -1,2 +1,3 @@
 x = true
 n = 1
+return = true
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__expanded.snap
new file mode 100644
index 00000000000..07f60204b83
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__expanded.snap
@@ -0,0 +1,20 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: expanded_code
+---
+unconstrained fn main(x: bool, n: u32) -> pub bool {
+    let mut v: [bool] = [x].as_vector();
+    for _ in 0_u32..n {
+        v = v.push_back(x);
+    }
+    let mut acc: u32 = 0_u32;
+    for _ in 0_u32..2_u32 {
+        {
+            let op_rhs_0: u32 = v.push_front(false).len();
+            acc = acc + op_rhs_0;
+        }
+    }
+    assert(acc > 0_u32);
+    assert(v[0_u32] == x);
+    v[0_u32]
+}
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__stdout.snap
new file mode 100644
index 00000000000..e54a80a2e37
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator/execute__tests__stdout.snap
@@ -0,0 +1,5 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: stdout
+---
+[regression_licm_vector_mutator] Circuit output: true
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__expanded.snap
new file mode 100644
index 00000000000..da167d2e86f
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__expanded.snap
@@ -0,0 +1,20 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: expanded_code
+---
+unconstrained fn main(x: bool, n: u32, m: u32) -> pub bool {
+    let mut v: [bool] = [x].as_vector();
+    for _ in 0_u32..n {
+        v = v.push_back(x);
+    }
+    let mut acc: u32 = 0_u32;
+    for _ in 0_u32..m {
+        {
+            let op_rhs_0: u32 = v.push_front(false).len();
+            acc = acc + op_rhs_0;
+        }
+    }
+    assert(acc == 0_u32);
+    assert(v[0_u32] == x);
+    v[0_u32]
+}
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__stdout.snap
new file mode 100644
index 00000000000..2098c8b56e3
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_empty_loop/execute__tests__stdout.snap
@@ -0,0 +1,5 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: stdout
+---
+[regression_licm_vector_mutator_empty_loop] Circuit output: true
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__expanded.snap
new file mode 100644
index 00000000000..79580adf318
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__expanded.snap
@@ -0,0 +1,29 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: expanded_code
+---
+fn helper(v: [bool]) -> Field {
+    let mut len: Field = v.push_front(false).len() as Field;
+    for _ in 0_u32..10_u32 {
+        len = (len * 3_Field) + 1_Field;
+    }
+    len
+}
+
+unconstrained fn main(x: bool, n: u32) -> pub bool {
+    let mut v: [bool] = [x].as_vector();
+    for _ in 0_u32..n {
+        v = v.push_back(x);
+    }
+    let mut acc: Field = 0_Field;
+    for _ in 0_u32..2_u32 {
+        {
+            let op_rhs_0: Field = helper(v);
+            acc = acc + op_rhs_0;
+        }
+    }
+    assert(acc != 0_Field);
+    assert(helper(v) != 0_Field);
+    assert(v[0_u32] == x);
+    v[0_u32]
+}
diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__stdout.snap
new file mode 100644
index 00000000000..0d23702fee7
--- /dev/null
+++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_licm_vector_mutator_wrapper/execute__tests__stdout.snap
@@ -0,0 +1,5 @@
+---
+source: tooling/nargo_cli/tests/execute.rs
+expression: stdout
+---
+[regression_licm_vector_mutator_wrapper] Circuit output: true

From 177d4e97922ab1e8b55238cc1239768e3ebde023 Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Wed, 5 Aug 2026 14:55:47 +0000
Subject: [PATCH 07/12] update PR #13445

---
 .../src/ssa/opt/loop_invariant.rs             | 40 ++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index 2fec8bee5bf..492632d39e2 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -2918,6 +2918,17 @@ mod tests {
         // and corrupt the value `b3` reads. `vector_push_front` is `PureWithPredicate` exactly so
         // that LICM leaves it in the loop body, behind the guard.
         //
+        // `PureWithPredicate` is necessary but not sufficient on its own: `can_be_hoisted` maps it
+        // to `WithPredicate`, and `BlockContext::can_hoist_control_dependent_instruction` still
+        // hoists such an instruction out of a loop that is guaranteed to execute — which `b1`'s
+        // `0..2` bounds are. What stops the hoist here is the third condition of that check,
+        // `!is_impure`: the `inc_rc` guard itself is side-effecting, so it marks `b2` impure
+        // before the call is considered. In other words the guard protects the mutator by being
+        // in front of it, not merely by existing. Both halves are load-bearing, so this test
+        // asserts on the SSA as well as on the execution result: were `vector_push_front` `Pure`
+        // again, or were rc instructions to stop marking a block impure, the call below would
+        // move into `b0` and the snapshot would change.
+        //
         // `assert_pass_does_not_affect_execution` interprets before and after LICM and panics when
         // the results differ.
         let src = r#"
@@ -2945,7 +2956,34 @@ mod tests {
         "#;
         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);
+        let (ssa, _) =
+            assert_pass_does_not_affect_execution(ssa, input, Ssa::loop_invariant_code_motion);
+
+        // Nothing is hoisted: the pre-header `b0` of `f1` stays empty and the call stays in `b2`,
+        // immediately after the `inc_rc` that guards its vector operand.
+        assert_ssa_snapshot!(ssa, @r"
+        brillig(inline) impure fn main f0 {
+          b0(v0: u1):
+            v2 = make_array [v0, u1 1] : [u1]
+            v5 = call f1(u32 2, v2) -> u1
+            return v5
+        }
+        brillig(inline) impure fn foo f1 {
+          b0(v0: u32, v1: [u1]):
+            jmp b1(u32 0)
+          b1(v2: u32):
+            v5 = lt v2, u32 2
+            jmpif v5 then: b2(), else: b3()
+          b2():
+            inc_rc v1
+            v8, v9 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
+            v11 = unchecked_add v2, u32 1
+            jmp b1(v11)
+          b3():
+            v12 = array_get v1, index u32 0 -> u1
+            return v12
+        }
+        ");
     }
 
     #[test]

From f634283da1c4c28293365650284cfdd26c3fcaf1 Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Wed, 5 Aug 2026 15:28:47 +0000
Subject: [PATCH 08/12] update PR #13445

---
 .../noirc_evaluator/src/ssa/ir/instruction.rs |  18 ++
 .../src/ssa/opt/loop_invariant.rs             | 182 ++++++++++++++++++
 2 files changed, 200 insertions(+)

diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs
index 8f5a9ab8a0a..06c7ebfa61e 100644
--- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs
+++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs
@@ -243,6 +243,24 @@ impl Intrinsic {
         )
     }
 
+    /// Returns true if this intrinsic may write through its vector operand in place in Brillig,
+    /// i.e. when that operand's copy-on-write reference count is 1.
+    ///
+    /// This is the subset of [`Self::unsafe_for_clone_elision_in_brillig`] that actually mutates:
+    /// `StrAsBytes` and `ArrayAsStrUnchecked` are unsafe to elide a clone around because their
+    /// result aliases their operand, not because they write to it.
+    pub(crate) fn mutates_array_operand_in_brillig(&self) -> bool {
+        matches!(
+            self,
+            Intrinsic::VectorPushBack
+                | Intrinsic::VectorPushFront
+                | Intrinsic::VectorPopBack
+                | Intrinsic::VectorPopFront
+                | Intrinsic::VectorInsert
+                | Intrinsic::VectorRemove
+        )
+    }
+
     pub(crate) fn purity(&self) -> Purity {
         match self {
             // These apply a constraint in the form of ACIR opcodes, but they can be deduplicated
diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index 492632d39e2..e716bf59f84 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -426,6 +426,27 @@ impl<'f> LoopInvariantContext<'f> {
                     self.can_hoist_invariant(&loop_context, &block_context, instruction_id);
 
                 if hoist_invariant {
+                    // If we are hoisting an instruction which can write through one of its array
+                    // operands in place, that operand needs an `inc_rc` of its own in the
+                    // pre-header, ahead of the hoisted instruction. See
+                    // `mutable_array_operands` for why this cannot be left to the guard the
+                    // ownership pass already emits in the loop body.
+                    let guards =
+                        self.unprotected_mutable_array_operands(instruction_id, pre_header);
+                    if !guards.is_empty() {
+                        let call_stack = self
+                            .inserter
+                            .function
+                            .dfg
+                            .get_instruction_call_stack_id(instruction_id);
+                        for operand in guards {
+                            let inc_rc = Instruction::IncrementRc { value: operand };
+                            self.inserter.function.dfg.insert_instruction_and_results(
+                                inc_rc, pre_header, None, call_stack,
+                            );
+                        }
+                    }
+
                     self.inserter.push_instruction(instruction_id, pre_header, false);
 
                     // If we are hoisting an instruction which returns a new array,
@@ -661,6 +682,85 @@ impl<'f> LoopInvariantContext<'f> {
         }
     }
 
+    /// The array operands of `instruction_id` that it may write through in place, and which
+    /// therefore need an `inc_rc` in the pre-header when the instruction is hoisted.
+    ///
+    /// Brillig arrays are copy-on-write: `array_set` and the vector mutator intrinsics write
+    /// through their array operand once that operand's reference count is 1, and clone otherwise.
+    /// The ownership pass keeps that safe by emitting an `inc_rc` on any operand still live after
+    /// the mutation — but that `inc_rc` is a separate instruction which `can_be_hoisted`
+    /// classifies `No`, so it stays in the loop body. A mutator hoisted out from in front of its
+    /// guard would find the operand at reference count 1 and corrupt it (noir-lang/noir-claude#244).
+    ///
+    /// Today nothing reaches that state: the guard is side-effecting, so it marks the block impure
+    /// and `BlockContext::can_hoist_control_dependent_instruction` refuses the hoist. That is an
+    /// accident of instruction order rather than a property of this pass — it holds only because
+    /// the guard happens to sit in the same block, ahead of the mutator, and it evaporates the
+    /// moment rc traffic stops counting towards `is_impure`. Emitting the guard alongside the
+    /// hoisted instruction makes the motion safe on its own terms instead.
+    ///
+    /// This deliberately does not cover the other two entries of
+    /// `Intrinsic::unsafe_for_clone_elision_in_brillig`, `StrAsBytes` and `ArrayAsStrUnchecked`:
+    /// they alias their operand rather than write through it, and the shared buffer is already
+    /// covered by the `inc_rc` inserted on the hoisted instruction's *results*.
+    ///
+    /// Calls to user-defined functions need no entry here either: a Brillig function that can
+    /// mutate an array parameter in place is `Purity::Impure` (see `Function::is_pure`), so
+    /// `can_be_hoisted` never lets it out of the loop in the first place.
+    ///
+    /// An operand the pre-header already bumps is skipped: it is protected at the position the
+    /// instruction is being hoisted to, so a second bump would only force a copy. That is the
+    /// shape `inserts_inc_rc_for_hoisted_array_set` captures, and the reason this pass can go on
+    /// hoisting a Brillig `array_set` whose operand is cloned before the loop.
+    fn unprotected_mutable_array_operands(
+        &self,
+        instruction_id: InstructionId,
+        pre_header: BasicBlockId,
+    ) -> Vec<ValueId> {
+        let operands = self.mutable_array_operands(instruction_id);
+        if operands.is_empty() {
+            return operands;
+        }
+
+        let dfg = &self.inserter.function.dfg;
+        let bumped_in_pre_header: HashSet<ValueId> = dfg[pre_header]
+            .instructions()
+            .iter()
+            .filter_map(|instruction| match dfg[*instruction] {
+                Instruction::IncrementRc { value } => Some(self.inserter.resolve(value)),
+                _ => None,
+            })
+            .collect();
+
+        operands.into_iter().filter(|operand| !bumped_in_pre_header.contains(operand)).collect()
+    }
+
+    /// The array operands of `instruction_id` that it may write through in place, whether or not
+    /// they are already protected. See [`Self::unprotected_mutable_array_operands`].
+    fn mutable_array_operands(&self, instruction_id: InstructionId) -> Vec<ValueId> {
+        let dfg = &self.inserter.function.dfg;
+        if !dfg.runtime().is_brillig() {
+            return Vec::new();
+        }
+
+        let operands = match &dfg[instruction_id] {
+            Instruction::ArraySet { array, .. } => vec![*array],
+            Instruction::Call { func, arguments } => match dfg[*func] {
+                Value::Intrinsic(intrinsic) if intrinsic.mutates_array_operand_in_brillig() => {
+                    arguments
+                        .iter()
+                        .copied()
+                        .filter(|argument| dfg.type_of_value(*argument).is_array())
+                        .collect()
+                }
+                _ => Vec::new(),
+            },
+            _ => Vec::new(),
+        };
+
+        operands.into_iter().map(|operand| self.inserter.resolve(operand)).collect()
+    }
+
     /// Decide if an in instruction can be hoisted into the pre-header of the loop.
     ///
     /// Returns 2 flags:
@@ -2986,6 +3086,88 @@ mod tests {
         ");
     }
 
+    #[test]
+    fn hoisted_vector_mutator_guards_its_own_array_operand() {
+        // The companion of `hoisting_vector_mutator_out_of_loop_drops_refcount_guard` with the
+        // `inc_rc v1` guard removed from `b2`. `v1` is still read by the `array_get` in `b3`, so
+        // the mutation must not be observable — but with nothing side-effecting ahead of it, `b2`
+        // is pure, the loop is guaranteed to execute and the call *is* hoisted.
+        //
+        // That is the case the purity classification alone does not cover: it is only the guard's
+        // side effect that keeps the mutator in the loop in the other test, so as soon as the
+        // guard is not sitting in front of the call the hoist goes ahead. LICM therefore has to
+        // re-establish the protection itself, by emitting `inc_rc v1` into the pre-header ahead of
+        // the hoisted call, which puts `v1` at reference count 2 and forces the push to clone.
+        //
+        // The frontend does not emit this shape today (the ownership pass always places the clone
+        // beside the mutating use), so this is hardening rather than a reachable miscompilation —
+        // but nothing in the pass was enforcing it.
+        let src = r#"
+        brillig(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [v0, u1 1] : [u1]
+            v2 = call f1(u32 2, v1) -> u1
+            return v2
+        }
+        brillig(inline) predicate_pure 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():
+            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
+        }
+        "#;
+        // `assert_pass_does_not_affect_execution` is deliberately not used here: the input is
+        // ill-formed, so its pre-LICM interpretation is already the corrupted one. Interpreting
+        // this SSA before the pass yields `0` — the loop mutates `v1` in place at reference count
+        // 1 on every iteration, and `b3` reads the pushed `u1 0` back. Its SSA-level meaning is
+        // `1`: `vector_push_front` returns a new vector and leaves `v1` alone. The pass must land
+        // on the latter.
+        let ssa = Ssa::from_str(src).unwrap();
+        let input = vec![crate::ssa::interpreter::value::Value::bool(true)];
+        let ssa = ssa.loop_invariant_code_motion();
+        assert_eq!(
+            ssa.interpret(crate::ssa::interpreter::value::Value::snapshot_args(&input)),
+            Ok(vec![crate::ssa::interpreter::value::Value::bool(true)]),
+            "the hoisted push must not be observable through `v1`",
+        );
+
+        // The call is hoisted into `b0`, preceded by the `inc_rc v1` that LICM inserted to protect
+        // the operand it can write through, and followed by the pre-existing `inc_rc` on its
+        // array result.
+        assert_ssa_snapshot!(ssa, @r"
+        brillig(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v2 = make_array [v0, u1 1] : [u1]
+            v5 = call f1(u32 2, v2) -> u1
+            return v5
+        }
+        brillig(inline) predicate_pure fn foo f1 {
+          b0(v0: u32, v1: [u1]):
+            inc_rc v1
+            v5, v6 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
+            jmp b1(u32 0)
+          b1(v2: u32):
+            v9 = lt v2, u32 2
+            jmpif v9 then: b2(), else: b3()
+          b2():
+            inc_rc v6
+            v11 = unchecked_add v2, u32 1
+            jmp b1(v11)
+          b3():
+            v12 = array_get v1, index u32 0 -> u1
+            return v12
+        }
+        ");
+    }
+
     #[test]
     fn inserts_inc_rc_for_hoisted_array_set() {
         // The SSA below has been captured during the pre-processing of functions in the following:

From f21be293f793dbf821b1ff72220e89485d5a2551 Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Wed, 5 Aug 2026 15:46:56 +0000
Subject: [PATCH 09/12] update PR #13445

---
 .../src/ssa/opt/loop_invariant.rs             | 91 ++++++++++---------
 1 file changed, 48 insertions(+), 43 deletions(-)

diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index e716bf59f84..e3d0d8c1418 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -3088,80 +3088,85 @@ mod tests {
 
     #[test]
     fn hoisted_vector_mutator_guards_its_own_array_operand() {
-        // The companion of `hoisting_vector_mutator_out_of_loop_drops_refcount_guard` with the
-        // `inc_rc v1` guard removed from `b2`. `v1` is still read by the `array_get` in `b3`, so
-        // the mutation must not be observable — but with nothing side-effecting ahead of it, `b2`
-        // is pure, the loop is guaranteed to execute and the call *is* hoisted.
+        // The companion of `hoisting_vector_mutator_out_of_loop_drops_refcount_guard`, with the
+        // `inc_rc v1` guard moved out of the loop body and into the entry block. The SSA is
+        // well-formed either way — `v1` is read by the `array_get` in `b4` and the entry bump
+        // dominates every mutation of it — but the two shapes hoist differently.
         //
-        // That is the case the purity classification alone does not cover: it is only the guard's
-        // side effect that keeps the mutator in the loop in the other test, so as soon as the
-        // guard is not sitting in front of the call the hoist goes ahead. LICM therefore has to
-        // re-establish the protection itself, by emitting `inc_rc v1` into the pre-header ahead of
-        // the hoisted call, which puts `v1` at reference count 2 and forces the push to clone.
+        // With the guard in the loop body its side effect marks the block impure and the call
+        // stays put. Here the loop body has nothing side-effecting ahead of the call, so the
+        // block is pure, the `0..2` loop is guaranteed to execute, and the call is hoisted. The
+        // purity classification does not distinguish these two cases at all; only the guard's
+        // accidental position does. So LICM has to re-establish the protection at the point it
+        // moves the mutator to, by emitting `inc_rc v1` into the pre-header ahead of the hoisted
+        // call. `Ssa::interpret` models copy-on-write faithfully, so the returned value is what
+        // catches a guard emitted in the wrong place: `b4` reads `v1[0]` after the push.
         //
-        // The frontend does not emit this shape today (the ownership pass always places the clone
-        // beside the mutating use), so this is hardening rather than a reachable miscompilation —
-        // but nothing in the pass was enforcing it.
+        // The bump is redundant here, since the entry block already protects `v1` — the
+        // pre-header scan in `unprotected_mutable_array_operands` is deliberately local, and
+        // `inserts_inc_rc_for_hoisted_array_set` pins the case it does recognise. Conservative in
+        // this direction costs one rc bump; conservative in the other direction is a
+        // miscompilation.
         let src = r#"
-        brillig(inline) predicate_pure fn main f0 {
+        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) predicate_pure fn foo f1 {
+        brillig(inline) impure fn foo f1 {
           b0(v0: u32, v1: [u1]):
-            jmp b1(u32 0)
-          b1(v2: u32):
+            inc_rc v1
+            jmp b1()
+          b1():
+            jmp b2(u32 0)
+          b2(v2: u32):
             v3 = lt v2, u32 2
-            jmpif v3 then: b2(), else: b3()
-          b2():
+            jmpif v3 then: b3(), else: b4()
+          b3():
             v4, v5 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
             v6 = unchecked_add v2, u32 1
-            jmp b1(v6)
-          b3():
+            jmp b2(v6)
+          b4():
             v7 = array_get v1, index u32 0 -> u1
             return v7
         }
         "#;
-        // `assert_pass_does_not_affect_execution` is deliberately not used here: the input is
-        // ill-formed, so its pre-LICM interpretation is already the corrupted one. Interpreting
-        // this SSA before the pass yields `0` — the loop mutates `v1` in place at reference count
-        // 1 on every iteration, and `b3` reads the pushed `u1 0` back. Its SSA-level meaning is
-        // `1`: `vector_push_front` returns a new vector and leaves `v1` alone. The pass must land
-        // on the latter.
         let ssa = Ssa::from_str(src).unwrap();
         let input = vec![crate::ssa::interpreter::value::Value::bool(true)];
-        let ssa = ssa.loop_invariant_code_motion();
-        assert_eq!(
-            ssa.interpret(crate::ssa::interpreter::value::Value::snapshot_args(&input)),
-            Ok(vec![crate::ssa::interpreter::value::Value::bool(true)]),
-            "the hoisted push must not be observable through `v1`",
-        );
+        let (ssa, result) =
+            assert_pass_does_not_affect_execution(ssa, input, Ssa::loop_invariant_code_motion);
 
-        // The call is hoisted into `b0`, preceded by the `inc_rc v1` that LICM inserted to protect
-        // the operand it can write through, and followed by the pre-existing `inc_rc` on its
-        // array result.
+        // `main` returns `v1[0]`, i.e. the argument it was given: the hoisted push must not be
+        // observable through `v1`.
+        assert_eq!(result, Ok(vec![crate::ssa::interpreter::value::Value::bool(true)]));
+
+        // The call is hoisted into the pre-header `b1`, preceded by the `inc_rc v1` LICM inserted
+        // to protect the operand it can write through, and followed by the pre-existing `inc_rc`
+        // on its array result.
         assert_ssa_snapshot!(ssa, @r"
-        brillig(inline) predicate_pure fn main f0 {
+        brillig(inline) impure fn main f0 {
           b0(v0: u1):
             v2 = make_array [v0, u1 1] : [u1]
             v5 = call f1(u32 2, v2) -> u1
             return v5
         }
-        brillig(inline) predicate_pure fn foo f1 {
+        brillig(inline) impure fn foo f1 {
           b0(v0: u32, v1: [u1]):
+            inc_rc v1
+            jmp b1()
+          b1():
             inc_rc v1
             v5, v6 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
-            jmp b1(u32 0)
-          b1(v2: u32):
+            jmp b2(u32 0)
+          b2(v2: u32):
             v9 = lt v2, u32 2
-            jmpif v9 then: b2(), else: b3()
-          b2():
+            jmpif v9 then: b3(), else: b4()
+          b3():
             inc_rc v6
             v11 = unchecked_add v2, u32 1
-            jmp b1(v11)
-          b3():
+            jmp b2(v11)
+          b4():
             v12 = array_get v1, index u32 0 -> u1
             return v12
         }

From 55d071022b09cfc646db3b7ea9a23f7645f23a57 Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Wed, 5 Aug 2026 15:57:35 +0000
Subject: [PATCH 10/12] update PR #13445

---
 .../src/ssa/opt/loop_invariant.rs             | 52 +++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index e3d0d8c1418..b2f4392004b 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -3173,6 +3173,58 @@ mod tests {
         ");
     }
 
+    #[test]
+    fn hoisted_vector_mutator_guard_prevents_operand_corruption() {
+        // The output-guarding half of `hoisted_vector_mutator_guards_its_own_array_operand`.
+        //
+        // That test keeps the SSA well-formed, which means the entry block already protects `v1`
+        // and the `inc_rc` LICM emits is redundant: revert the guard and the program still
+        // returns the same value, so only its snapshot notices. That is not a gap in the test but
+        // a property of the fix — on SSA that honours the ownership contract a live array operand
+        // is always already protected on every path to the mutator, so the guard can never change
+        // a result. The only inputs where it can are ones that violate the contract, and this is
+        // one: `v1` is read by the `array_get` in `b3` with nothing bumping it anywhere.
+        //
+        // `assert_pass_does_not_affect_execution` cannot express this. Interpreting the input
+        // before the pass already yields the corrupted `0`: the loop mutates `v1` in place at
+        // reference count 1 and `b3` reads the pushed `u1 0` back. The pass is *supposed* to
+        // change that, by hoisting the push behind a guard it emits itself, landing on the
+        // SSA-level meaning of `1` — `vector_push_front` returns a new vector and leaves `v1`
+        // alone. Without the guard the hoisted push mutates in place exactly as before and the
+        // assertion below sees `false`.
+        let src = r#"
+        brillig(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [v0, u1 1] : [u1]
+            v2 = call f1(u32 2, v1) -> u1
+            return v2
+        }
+        brillig(inline) predicate_pure 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():
+            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 ssa = ssa.loop_invariant_code_motion();
+
+        assert_eq!(
+            ssa.interpret(crate::ssa::interpreter::value::Value::snapshot_args(&input)),
+            Ok(vec![crate::ssa::interpreter::value::Value::bool(true)]),
+            "the hoisted push must not be observable through `v1`",
+        );
+    }
+
     #[test]
     fn inserts_inc_rc_for_hoisted_array_set() {
         // The SSA below has been captured during the pre-processing of functions in the following:

From cb357d7c0ec947b8f427e2868b0249d66735d742 Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Wed, 5 Aug 2026 16:21:05 +0000
Subject: [PATCH 11/12] update PR #13445

---
 .../src/ssa/opt/loop_invariant.rs             | 33 ++++++++++++-------
 1 file changed, 22 insertions(+), 11 deletions(-)

diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index b2f4392004b..2848f82db74 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -692,12 +692,20 @@ impl<'f> LoopInvariantContext<'f> {
     /// classifies `No`, so it stays in the loop body. A mutator hoisted out from in front of its
     /// guard would find the operand at reference count 1 and corrupt it (noir-lang/noir-claude#244).
     ///
-    /// Today nothing reaches that state: the guard is side-effecting, so it marks the block impure
-    /// and `BlockContext::can_hoist_control_dependent_instruction` refuses the hoist. That is an
-    /// accident of instruction order rather than a property of this pass — it holds only because
-    /// the guard happens to sit in the same block, ahead of the mutator, and it evaporates the
-    /// moment rc traffic stops counting towards `is_impure`. Emitting the guard alongside the
-    /// hoisted instruction makes the motion safe on its own terms instead.
+    /// That state is reachable from Noir source: it is exactly what
+    /// `test_programs/execution_success/regression_licm_vector_mutator` compiled to before
+    /// `vector_push_front` was reclassified `PureWithPredicate`. The guard the ownership pass
+    /// emits sits in the loop body, so it is not protection *at the pre-header*, and hoisting the
+    /// push past it corrupted the vector. Emitting the guard here fixes those three regression
+    /// programs on its own, without the purity change — the two are independent remedies for the
+    /// same defect, and this one fixes the whole class rather than one intrinsic.
+    ///
+    /// With the reclassification also in place, no vector mutator is hoisted at all, so nothing
+    /// in the test corpus reaches this code any more (919 packages compiled: zero hits). What
+    /// still holds the other route shut is that the guard is side-effecting, so it marks the
+    /// block impure and `BlockContext::can_hoist_control_dependent_instruction` refuses the
+    /// hoist — an accident of instruction order rather than a property of this pass, which
+    /// evaporates the moment rc traffic stops counting towards `is_impure`.
     ///
     /// This deliberately does not cover the other two entries of
     /// `Intrinsic::unsafe_for_clone_elision_in_brillig`, `StrAsBytes` and `ArrayAsStrUnchecked`:
@@ -3179,11 +3187,14 @@ mod tests {
         //
         // That test keeps the SSA well-formed, which means the entry block already protects `v1`
         // and the `inc_rc` LICM emits is redundant: revert the guard and the program still
-        // returns the same value, so only its snapshot notices. That is not a gap in the test but
-        // a property of the fix — on SSA that honours the ownership contract a live array operand
-        // is always already protected on every path to the mutator, so the guard can never change
-        // a result. The only inputs where it can are ones that violate the contract, and this is
-        // one: `v1` is read by the `array_get` in `b3` with nothing bumping it anywhere.
+        // returns the same value, so only its snapshot notices. This one is the complement, on
+        // SSA where `v1` is read by the `array_get` in `b3` with nothing bumping it anywhere, so
+        // the guard is the only thing standing between the hoisted push and a corrupted result.
+        //
+        // A hand-written input is needed only because `vector_push_front` is now
+        // `PureWithPredicate` and so is never hoisted. Reclassify it `Pure` again and the three
+        // `regression_licm_vector_mutator*` programs reach this same path from ordinary Noir
+        // source — and pass, on the strength of this guard alone.
         //
         // `assert_pass_does_not_affect_execution` cannot express this. Interpreting the input
         // before the pass already yields the corrupted `0`: the loop mutates `v1` in place at

From 15228647aad96a7d755ffff418c5223c59c323bd Mon Sep 17 00:00:00 2001
From: AztecBot <tech@aztec-labs.com>
Date: Wed, 5 Aug 2026 16:33:24 +0000
Subject: [PATCH 12/12] update PR #13445

---
 .../src/ssa/opt/loop_invariant.rs             | 203 ++++++++++--------
 1 file changed, 118 insertions(+), 85 deletions(-)

diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
index 2848f82db74..3be0398d6a8 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs
@@ -3013,32 +3013,30 @@ mod tests {
         assert_eq!(can_be_hoisted(&instruction, &function.dfg), result);
     }
 
+    /// Regression for noir-claude#244, found by the AST fuzzer `pass_vs_prev` on seed
+    /// `0xb6bc8e1f00100000` and bisected to this pass. LICM hoisted a Brillig vector mutator out
+    /// of a loop and left the `inc_rc` guarding its operand behind, so the hoisted push mutated a
+    /// still-live vector in place and the program returned the wrong answer with no error.
+    ///
+    /// Brillig arrays are copy-on-write: `vector_push_front` writes through its input vector in
+    /// place once the operand's reference count is 1. Here 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`. That guard is classified `CanBeHoistedResult::No` and stays in the loop body, so the
+    /// call must stay with it.
+    ///
+    /// The assertions prove both halves of what keeps it there. `vector_push_front` being
+    /// `PureWithPredicate` is necessary but not sufficient: `can_be_hoisted` maps that to
+    /// `WithPredicate`, and `BlockContext::can_hoist_control_dependent_instruction` still hoists
+    /// out of a loop guaranteed to execute — which `b1`'s `0..2` bounds are. What stops it is the
+    /// third condition of that check, `!is_impure`: the guard is itself side-effecting, so it
+    /// marks `b2` impure before the call is considered. The guard protects the mutator by being
+    /// in front of it, not merely by existing. Reclassify the intrinsic `Pure`, or stop counting
+    /// rc traffic towards `is_impure`, and the call moves into `b0` — which the snapshot catches
+    /// and, on the corrupted read, the returned value does too.
     #[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.
-        //
-        // `PureWithPredicate` is necessary but not sufficient on its own: `can_be_hoisted` maps it
-        // to `WithPredicate`, and `BlockContext::can_hoist_control_dependent_instruction` still
-        // hoists such an instruction out of a loop that is guaranteed to execute — which `b1`'s
-        // `0..2` bounds are. What stops the hoist here is the third condition of that check,
-        // `!is_impure`: the `inc_rc` guard itself is side-effecting, so it marks `b2` impure
-        // before the call is considered. In other words the guard protects the mutator by being
-        // in front of it, not merely by existing. Both halves are load-bearing, so this test
-        // asserts on the SSA as well as on the execution result: were `vector_push_front` `Pure`
-        // again, or were rc instructions to stop marking a block impure, the call below would
-        // move into `b0` and the snapshot would change.
-        //
-        // `assert_pass_does_not_affect_execution` interprets before and after LICM and panics when
-        // the results differ.
+        use crate::ssa::interpreter::value::Value;
+
         let src = r#"
         brillig(inline) impure fn main f0 {
           b0(v0: u1):
@@ -3053,6 +3051,7 @@ mod tests {
             v3 = lt v2, u32 2
             jmpif v3 then: b2(), else: b3()
           b2():
+            // `v1` is guarded here because `b3` still reads it.
             inc_rc v1
             v4, v5 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
             v6 = unchecked_add v2, u32 1
@@ -3063,12 +3062,17 @@ mod tests {
         }
         "#;
         let ssa = Ssa::from_str(src).unwrap();
-        let input = vec![crate::ssa::interpreter::value::Value::bool(true)];
-        let (ssa, _) =
-            assert_pass_does_not_affect_execution(ssa, input, Ssa::loop_invariant_code_motion);
+        let (ssa, result) = assert_pass_does_not_affect_execution(
+            ssa,
+            vec![Value::bool(true)],
+            Ssa::loop_invariant_code_motion,
+        );
 
-        // Nothing is hoisted: the pre-header `b0` of `f1` stays empty and the call stays in `b2`,
-        // immediately after the `inc_rc` that guards its vector operand.
+        // Behavior: `main` returns `v1[0]`, i.e. the argument it was given.
+        assert_eq!(result, Ok(vec![Value::bool(true)]));
+
+        // Shape: nothing is hoisted. The pre-header `b0` of `f1` stays empty and the call stays
+        // in `b2`, immediately after the `inc_rc` that guards its vector operand.
         assert_ssa_snapshot!(ssa, @r"
         brillig(inline) impure fn main f0 {
           b0(v0: u1):
@@ -3094,27 +3098,30 @@ mod tests {
         ");
     }
 
+    /// Companion of [`hoisting_vector_mutator_out_of_loop_drops_refcount_guard`] for
+    /// noir-claude#244, with the `inc_rc v1` guard moved out of the loop body and into the entry
+    /// block. The SSA is well-formed either way — `v1` is read by the `array_get` in `b4` and the
+    /// entry bump dominates every mutation of it — but the two shapes hoist differently.
+    ///
+    /// With the guard in the loop body its side effect marks the block impure and the call stays
+    /// put. Here the loop body has nothing side-effecting ahead of the call, so the block is
+    /// pure, the `0..2` loop is guaranteed to execute, and the call *is* hoisted. The purity
+    /// classification does not distinguish the two cases at all; only the guard's position does.
+    /// So LICM has to re-establish the protection at the point it moves the mutator to, by
+    /// emitting `inc_rc v1` into the pre-header ahead of the hoisted call — which the snapshot
+    /// asserts. `Ssa::interpret` models copy-on-write faithfully, so the returned value is what
+    /// would catch a guard emitted in the wrong place: `b4` reads `v1[0]` after the push.
+    ///
+    /// The bump is redundant in this particular shape, since the entry block already protects
+    /// `v1`: the pre-header scan in `unprotected_mutable_array_operands` is deliberately local,
+    /// and [`inserts_inc_rc_for_hoisted_array_set`] pins the case it does recognise. Conservative
+    /// in this direction costs one rc bump; conservative in the other is a miscompilation. See
+    /// [`hoisted_vector_mutator_guard_prevents_operand_corruption`] for the shape where the guard
+    /// changes the result.
     #[test]
     fn hoisted_vector_mutator_guards_its_own_array_operand() {
-        // The companion of `hoisting_vector_mutator_out_of_loop_drops_refcount_guard`, with the
-        // `inc_rc v1` guard moved out of the loop body and into the entry block. The SSA is
-        // well-formed either way — `v1` is read by the `array_get` in `b4` and the entry bump
-        // dominates every mutation of it — but the two shapes hoist differently.
-        //
-        // With the guard in the loop body its side effect marks the block impure and the call
-        // stays put. Here the loop body has nothing side-effecting ahead of the call, so the
-        // block is pure, the `0..2` loop is guaranteed to execute, and the call is hoisted. The
-        // purity classification does not distinguish these two cases at all; only the guard's
-        // accidental position does. So LICM has to re-establish the protection at the point it
-        // moves the mutator to, by emitting `inc_rc v1` into the pre-header ahead of the hoisted
-        // call. `Ssa::interpret` models copy-on-write faithfully, so the returned value is what
-        // catches a guard emitted in the wrong place: `b4` reads `v1[0]` after the push.
-        //
-        // The bump is redundant here, since the entry block already protects `v1` — the
-        // pre-header scan in `unprotected_mutable_array_operands` is deliberately local, and
-        // `inserts_inc_rc_for_hoisted_array_set` pins the case it does recognise. Conservative in
-        // this direction costs one rc bump; conservative in the other direction is a
-        // miscompilation.
+        use crate::ssa::interpreter::value::Value;
+
         let src = r#"
         brillig(inline) impure fn main f0 {
           b0(v0: u1):
@@ -3124,6 +3131,7 @@ mod tests {
         }
         brillig(inline) impure fn foo f1 {
           b0(v0: u32, v1: [u1]):
+            // The guard dominates every mutation of `v1`, but is not in the pre-header `b1`.
             inc_rc v1
             jmp b1()
           b1():
@@ -3141,17 +3149,19 @@ mod tests {
         }
         "#;
         let ssa = Ssa::from_str(src).unwrap();
-        let input = vec![crate::ssa::interpreter::value::Value::bool(true)];
-        let (ssa, result) =
-            assert_pass_does_not_affect_execution(ssa, input, Ssa::loop_invariant_code_motion);
+        let (ssa, result) = assert_pass_does_not_affect_execution(
+            ssa,
+            vec![Value::bool(true)],
+            Ssa::loop_invariant_code_motion,
+        );
 
-        // `main` returns `v1[0]`, i.e. the argument it was given: the hoisted push must not be
-        // observable through `v1`.
-        assert_eq!(result, Ok(vec![crate::ssa::interpreter::value::Value::bool(true)]));
+        // Behavior: `main` returns `v1[0]`, i.e. the argument it was given — the hoisted push is
+        // not observable through `v1`.
+        assert_eq!(result, Ok(vec![Value::bool(true)]));
 
-        // The call is hoisted into the pre-header `b1`, preceded by the `inc_rc v1` LICM inserted
-        // to protect the operand it can write through, and followed by the pre-existing `inc_rc`
-        // on its array result.
+        // Shape: the call is hoisted into the pre-header `b1`, preceded by the `inc_rc v1` LICM
+        // inserted to protect the operand it can write through, and followed by the pre-existing
+        // `inc_rc` on its array result.
         assert_ssa_snapshot!(ssa, @r"
         brillig(inline) impure fn main f0 {
           b0(v0: u1):
@@ -3181,28 +3191,27 @@ mod tests {
         ");
     }
 
+    /// The result-changing half of [`hoisted_vector_mutator_guards_its_own_array_operand`], for
+    /// noir-claude#244. That test keeps the entry block's bump, so the guard LICM emits is
+    /// redundant and only its snapshot notices when the guard is removed. Here `v1` is read by
+    /// the `array_get` in `b3` with nothing bumping it anywhere, so the guard is the only thing
+    /// between the hoisted push and a corrupted result: without it the assertion below sees
+    /// `false`.
+    ///
+    /// A hand-written input is needed only because `vector_push_front` is now `PureWithPredicate`
+    /// and so is never hoisted. Reclassify it `Pure` and the three
+    /// `test_programs/execution_success/regression_licm_vector_mutator*` programs reach this same
+    /// path from ordinary Noir source — and pass, on the strength of this guard alone.
+    ///
+    /// `assert_pass_does_not_affect_execution` deliberately does not apply: this input violates
+    /// the ownership pass's contract, so interpreting it *before* LICM already yields the
+    /// corrupted `0` — the loop mutates `v1` in place at reference count 1 and `b3` reads the
+    /// pushed `u1 0` back. The pass is supposed to change that result, landing on the SSA-level
+    /// meaning of `1`, where `vector_push_front` returns a new vector and leaves `v1` alone.
     #[test]
     fn hoisted_vector_mutator_guard_prevents_operand_corruption() {
-        // The output-guarding half of `hoisted_vector_mutator_guards_its_own_array_operand`.
-        //
-        // That test keeps the SSA well-formed, which means the entry block already protects `v1`
-        // and the `inc_rc` LICM emits is redundant: revert the guard and the program still
-        // returns the same value, so only its snapshot notices. This one is the complement, on
-        // SSA where `v1` is read by the `array_get` in `b3` with nothing bumping it anywhere, so
-        // the guard is the only thing standing between the hoisted push and a corrupted result.
-        //
-        // A hand-written input is needed only because `vector_push_front` is now
-        // `PureWithPredicate` and so is never hoisted. Reclassify it `Pure` again and the three
-        // `regression_licm_vector_mutator*` programs reach this same path from ordinary Noir
-        // source — and pass, on the strength of this guard alone.
-        //
-        // `assert_pass_does_not_affect_execution` cannot express this. Interpreting the input
-        // before the pass already yields the corrupted `0`: the loop mutates `v1` in place at
-        // reference count 1 and `b3` reads the pushed `u1 0` back. The pass is *supposed* to
-        // change that, by hoisting the push behind a guard it emits itself, landing on the
-        // SSA-level meaning of `1` — `vector_push_front` returns a new vector and leaves `v1`
-        // alone. Without the guard the hoisted push mutates in place exactly as before and the
-        // assertion below sees `false`.
+        use crate::ssa::interpreter::value::Value;
+
         let src = r#"
         brillig(inline) predicate_pure fn main f0 {
           b0(v0: u1):
@@ -3217,6 +3226,7 @@ mod tests {
             v3 = lt v2, u32 2
             jmpif v3 then: b2(), else: b3()
           b2():
+            // No `inc_rc v1` anywhere, even though `b3` reads `v1`.
             v4, v5 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
             v6 = unchecked_add v2, u32 1
             jmp b1(v6)
@@ -3225,15 +3235,38 @@ mod tests {
             return v7
         }
         "#;
-        let ssa = Ssa::from_str(src).unwrap();
-        let input = vec![crate::ssa::interpreter::value::Value::bool(true)];
-        let ssa = ssa.loop_invariant_code_motion();
+        let input = vec![Value::bool(true)];
+        let ssa = Ssa::from_str(src).unwrap().loop_invariant_code_motion();
 
-        assert_eq!(
-            ssa.interpret(crate::ssa::interpreter::value::Value::snapshot_args(&input)),
-            Ok(vec![crate::ssa::interpreter::value::Value::bool(true)]),
-            "the hoisted push must not be observable through `v1`",
-        );
+        // Behavior: the hoisted push must not be observable through `v1`.
+        assert_eq!(ssa.interpret(Value::snapshot_args(&input)), Ok(vec![Value::bool(true)]),);
+
+        // Shape: the `inc_rc v1` LICM emitted is what makes that true, by putting `v1` at
+        // reference count 2 before the hoisted push and forcing it to clone.
+        assert_ssa_snapshot!(ssa, @r"
+        brillig(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v2 = make_array [v0, u1 1] : [u1]
+            v5 = call f1(u32 2, v2) -> u1
+            return v5
+        }
+        brillig(inline) predicate_pure fn foo f1 {
+          b0(v0: u32, v1: [u1]):
+            inc_rc v1
+            v5, v6 = call vector_push_front(v0, v1, u1 0) -> (u32, [u1])
+            jmp b1(u32 0)
+          b1(v2: u32):
+            v9 = lt v2, u32 2
+            jmpif v9 then: b2(), else: b3()
+          b2():
+            inc_rc v6
+            v11 = unchecked_add v2, u32 1
+            jmp b1(v11)
+          b3():
+            v12 = array_get v1, index u32 0 -> u1
+            return v12
+        }
+        ");
     }
 
     #[test]