From b0b6e6781930457f14bce96d2a999b9ae766a444 Mon Sep 17 00:00:00 2001 From: Ary Borenszweig Date: Thu, 13 Aug 2026 15:02:57 -0300 Subject: [PATCH 1/2] chore(test): add failing regression tests for killed-set loss across while-condition break/continue A break or continue written in a nested while loop's condition targets the ENCLOSING loop, so it can skip a reassignment below it. The break/continue arm clears the killed set to record exactly that, but find_last_uses_in_loop_body moves the enclosing killed set aside (std::mem::take) before traversing the body and condition and restores it unconditionally afterwards, discarding the clear. Loop-exit truncation then wrongly exempts the variable, its use is classified as a move, and the required clone is never emitted: a release nargo silently returns [9, 9] instead of [1, 9], and a debug build rejects the program via the rc_invariant validator. Red tests only (residual of noir#13153, reported in noir-claude#1702): two execution_success programs (break and continue spellings) and two ownership unit tests whose snapshots record the buggy move decision. Co-Authored-By: Claude Fable 5 --- .../noirc_frontend/src/ownership/tests.rs | 109 ++++++++++++++++++ .../Nargo.toml | 6 + .../Prover.toml | 3 + .../src/main.nr | 34 ++++++ .../Nargo.toml | 6 + .../Prover.toml | 3 + .../src/main.nr | 33 ++++++ 7 files changed, 194 insertions(+) create mode 100644 test_programs/execution_success/regression_while_condition_break_killed/Nargo.toml create mode 100644 test_programs/execution_success/regression_while_condition_break_killed/Prover.toml create mode 100644 test_programs/execution_success/regression_while_condition_break_killed/src/main.nr create mode 100644 test_programs/execution_success/regression_while_condition_continue_killed/Nargo.toml create mode 100644 test_programs/execution_success/regression_while_condition_continue_killed/Prover.toml create mode 100644 test_programs/execution_success/regression_while_condition_continue_killed/src/main.nr diff --git a/compiler/noirc_frontend/src/ownership/tests.rs b/compiler/noirc_frontend/src/ownership/tests.rs index cbc9b945121..2202be08909 100644 --- a/compiler/noirc_frontend/src/ownership/tests.rs +++ b/compiler/noirc_frontend/src/ownership/tests.rs @@ -2280,3 +2280,112 @@ fn closure_captured_array_used_twice_clones_first_use() { } "); } + +#[test] +fn break_in_nested_while_condition_clears_killed() { + // The `break` in the inner `while`'s condition targets the OUTER loop, so it can skip + // the reassignment `x = [v, v, v]`. `x`'s old value is then still live after the loop, + // so its use in `let mut y = x` must be cloned, not moved: `x` may not stay in the + // `killed` set that exempts it from loop-exit truncation. + // + // This snapshot currently records the WRONG decision (`let mut y$l5 = x$l2;`, a move): + // the `killed.clear()` performed by the `break` lands on the loop-local set and is + // discarded when the enclosing set is restored at the loop boundary. Once fixed, the + // snapshot must show `let mut y$l5 = x$l2.clone();`. + let src = " + unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { + let mut x = [v, v, v]; + let mut z = [0, 0, 0]; + let mut i = 0; + while i < n { + let mut y = x; + y[0] = 9; + z = y; + let mut j = 0; + while ({ if i == 1 { break; } j < 3 }) { j = j + 1; } + x = [v, v, v]; + i = i + 1; + } + [x[0], z[0]] + } + "; + + let program = get_monomorphized(src).unwrap(); + insta::assert_snapshot!(program, @r" + unconstrained fn main$f0(v$l0: Field, n$l1: u32) -> pub [Field; 2] { + let mut x$l2 = [v$l0, v$l0, v$l0]; + let mut z$l3 = [0, 0, 0]; + let mut i$l4 = 0; + while (i$l4 < n$l1) { + let mut y$l5 = x$l2; + y$l5[0] = 9; + z$l3 = y$l5; + let mut j$l6 = 0; + while { + if (i$l4 == 1) { + break + }; + (j$l6 < 3) + } { + j$l6 = (j$l6 + 1) + }; + x$l2 = [v$l0, v$l0, v$l0]; + i$l4 = (i$l4 + 1) + }; + [x$l2[0], z$l3[0]] + } + "); +} + +#[test] +fn continue_in_nested_while_condition_clears_killed() { + // The `continue` spelling of `break_in_nested_while_condition_clears_killed`: it also + // targets the outer loop and can also skip the reassignment `x = [v, v, v]`, so the use + // of `x` in `let mut y = x` must be cloned, not moved. + // + // This snapshot currently records the WRONG decision (`let mut y$l5 = x$l2;`, a move). + // Once fixed, the snapshot must show `let mut y$l5 = x$l2.clone();`. + let src = " + unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { + let mut x = [v, v, v]; + let mut z = [0, 0, 0]; + let mut i = 0; + while i < n { + let mut y = x; + y[0] = 9; + z = y; + i = i + 1; + let mut j = 0; + while ({ if i == n { continue; } j < 3 }) { j = j + 1; } + x = [v, v, v]; + } + [x[0], z[0]] + } + "; + + let program = get_monomorphized(src).unwrap(); + insta::assert_snapshot!(program, @r" + unconstrained fn main$f0(v$l0: Field, n$l1: u32) -> pub [Field; 2] { + let mut x$l2 = [v$l0, v$l0, v$l0]; + let mut z$l3 = [0, 0, 0]; + let mut i$l4 = 0; + while (i$l4 < n$l1) { + let mut y$l5 = x$l2; + y$l5[0] = 9; + z$l3 = y$l5; + i$l4 = (i$l4 + 1); + let mut j$l6 = 0; + while { + if (i$l4 == n$l1) { + continue + }; + (j$l6 < 3) + } { + j$l6 = (j$l6 + 1) + }; + x$l2 = [v$l0, v$l0, v$l0] + }; + [x$l2[0], z$l3[0]] + } + "); +} diff --git a/test_programs/execution_success/regression_while_condition_break_killed/Nargo.toml b/test_programs/execution_success/regression_while_condition_break_killed/Nargo.toml new file mode 100644 index 00000000000..8462f549899 --- /dev/null +++ b/test_programs/execution_success/regression_while_condition_break_killed/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "regression_while_condition_break_killed" +type = "bin" +authors = [""] + +[dependencies] diff --git a/test_programs/execution_success/regression_while_condition_break_killed/Prover.toml b/test_programs/execution_success/regression_while_condition_break_killed/Prover.toml new file mode 100644 index 00000000000..18fd5c1c916 --- /dev/null +++ b/test_programs/execution_success/regression_while_condition_break_killed/Prover.toml @@ -0,0 +1,3 @@ +v = "1" +n = "5" +return = ["1", "9"] diff --git a/test_programs/execution_success/regression_while_condition_break_killed/src/main.nr b/test_programs/execution_success/regression_while_condition_break_killed/src/main.nr new file mode 100644 index 00000000000..c99bfe12235 --- /dev/null +++ b/test_programs/execution_success/regression_while_condition_break_killed/src/main.nr @@ -0,0 +1,34 @@ +// Regression for the `killed` set being restored across a loop boundary, discarding the +// `killed.clear()` performed by a `break` in a nested `while` condition. +// +// The `break` in the inner `while`'s condition targets the OUTER loop, so it can skip the +// reassignment `x = [v, v, v]`. The old value of `x` is then still live after the loop, so +// `let mut y = x` must clone rather than move: otherwise `y` aliases `x` and `y[0] = 9` +// corrupts the value read afterwards. `z = y` keeps the in-place `array_set` from being +// optimized away. With `v = 1` and `n = 5` the `break` fires on the last executed iteration +// (`i == 1`), so nothing repairs the corruption: the correct result is `[1, 9]`; the missing +// clone produces `[9, 9]` (or fails SSA validation in a debug build). +unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { + let mut x = [v, v, v]; + let mut z = [0, 0, 0]; + let mut i = 0; + while i < n { + let mut y = x; + y[0] = 9; + z = y; + let mut j = 0; + while ( + { + if i == 1 { + break; + } + j < 3 + } + ) { + j = j + 1; + } + x = [v, v, v]; + i = i + 1; + } + [x[0], z[0]] +} diff --git a/test_programs/execution_success/regression_while_condition_continue_killed/Nargo.toml b/test_programs/execution_success/regression_while_condition_continue_killed/Nargo.toml new file mode 100644 index 00000000000..50e81948fc8 --- /dev/null +++ b/test_programs/execution_success/regression_while_condition_continue_killed/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "regression_while_condition_continue_killed" +type = "bin" +authors = [""] + +[dependencies] diff --git a/test_programs/execution_success/regression_while_condition_continue_killed/Prover.toml b/test_programs/execution_success/regression_while_condition_continue_killed/Prover.toml new file mode 100644 index 00000000000..18fd5c1c916 --- /dev/null +++ b/test_programs/execution_success/regression_while_condition_continue_killed/Prover.toml @@ -0,0 +1,3 @@ +v = "1" +n = "5" +return = ["1", "9"] diff --git a/test_programs/execution_success/regression_while_condition_continue_killed/src/main.nr b/test_programs/execution_success/regression_while_condition_continue_killed/src/main.nr new file mode 100644 index 00000000000..3ce30a6e278 --- /dev/null +++ b/test_programs/execution_success/regression_while_condition_continue_killed/src/main.nr @@ -0,0 +1,33 @@ +// The `continue` spelling of `regression_while_condition_break_killed`: a `continue` in a +// nested `while` condition also targets the OUTER loop and also clears the `killed` set, +// and that clear must survive the loop boundary just like for `break`. +// +// `i` is incremented before the inner `while`, so when the `continue` fires (`i == n`, the +// final iteration) it jumps to the outer condition, which is now false: the loop exits with +// the reassignment `x = [v, v, v]` skipped. The old value of `x` is still live after the +// loop, so `let mut y = x` must clone rather than move. The correct result is `[1, 9]`; the +// missing clone produces `[9, 9]` (or fails SSA validation in a debug build). +unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { + let mut x = [v, v, v]; + let mut z = [0, 0, 0]; + let mut i = 0; + while i < n { + let mut y = x; + y[0] = 9; + z = y; + i = i + 1; + let mut j = 0; + while ( + { + if i == n { + continue; + } + j < 3 + } + ) { + j = j + 1; + } + x = [v, v, v]; + } + [x[0], z[0]] +} From f2c12346824eed253682f0e1cc7f14ab501b5578 Mon Sep 17 00:00:00 2001 From: Ary Borenszweig Date: Thu, 13 Aug 2026 15:22:22 -0300 Subject: [PATCH 2/2] fix(ownership): apply a while-condition break/continue's kill-clearing to the enclosing loop's killed set MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A variable is exempt from loop-exit clone-forcing only while its in-loop reassignment is unconditional; a reachable break/continue voids that, which the Break/Continue arm records with killed.clear(). But find_last_uses_in_loop_body saves the enclosing killed set away (std::mem::take) while traversing the body and condition, so a break/continue in a while condition — which targets the enclosing loop — cleared the loop-local set, and the stale enclosing kills were restored afterwards. The variable then stayed exempt, its use was classified as a move, and the required clone was never emitted. Mirror the existing has_break propagation: when the condition contained a break/continue, clear the restored killed set too. Fixes noir-lang/noir-claude#1702 (residual of noir#13153). Co-Authored-By: Claude Fable 5 --- .../noirc_frontend/src/ownership/last_uses.rs | 5 ++++ .../noirc_frontend/src/ownership/tests.rs | 15 ++++-------- .../execute__tests__expanded.snap | 24 +++++++++++++++++++ .../execute__tests__stdout.snap | 5 ++++ .../execute__tests__expanded.snap | 24 +++++++++++++++++++ .../execute__tests__stdout.snap | 5 ++++ 6 files changed, 67 insertions(+), 11 deletions(-) create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__expanded.snap create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__stdout.snap create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__expanded.snap create mode 100644 tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__stdout.snap diff --git a/compiler/noirc_frontend/src/ownership/last_uses.rs b/compiler/noirc_frontend/src/ownership/last_uses.rs index c5f4bcfa96e..21ce54b227a 100644 --- a/compiler/noirc_frontend/src/ownership/last_uses.rs +++ b/compiler/noirc_frontend/src/ownership/last_uses.rs @@ -311,6 +311,11 @@ impl LastUseContext { } } self.killed = saved_killed; + // A `break`/`continue` in the condition targets the enclosing loop, so its + // `killed.clear()` must apply to the enclosing set we just restored. + if condition_has_break { + self.killed.clear(); + } self.has_break = saved_has_break || condition_has_break; } diff --git a/compiler/noirc_frontend/src/ownership/tests.rs b/compiler/noirc_frontend/src/ownership/tests.rs index 2202be08909..1dea23d9aa1 100644 --- a/compiler/noirc_frontend/src/ownership/tests.rs +++ b/compiler/noirc_frontend/src/ownership/tests.rs @@ -2286,12 +2286,8 @@ fn break_in_nested_while_condition_clears_killed() { // The `break` in the inner `while`'s condition targets the OUTER loop, so it can skip // the reassignment `x = [v, v, v]`. `x`'s old value is then still live after the loop, // so its use in `let mut y = x` must be cloned, not moved: `x` may not stay in the - // `killed` set that exempts it from loop-exit truncation. - // - // This snapshot currently records the WRONG decision (`let mut y$l5 = x$l2;`, a move): - // the `killed.clear()` performed by the `break` lands on the loop-local set and is - // discarded when the enclosing set is restored at the loop boundary. Once fixed, the - // snapshot must show `let mut y$l5 = x$l2.clone();`. + // `killed` set that exempts it from loop-exit truncation, even though that set is + // saved away while the inner loop (and its condition) is traversed. let src = " unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { let mut x = [v, v, v]; @@ -2317,7 +2313,7 @@ fn break_in_nested_while_condition_clears_killed() { let mut z$l3 = [0, 0, 0]; let mut i$l4 = 0; while (i$l4 < n$l1) { - let mut y$l5 = x$l2; + let mut y$l5 = x$l2.clone(); y$l5[0] = 9; z$l3 = y$l5; let mut j$l6 = 0; @@ -2342,9 +2338,6 @@ fn continue_in_nested_while_condition_clears_killed() { // The `continue` spelling of `break_in_nested_while_condition_clears_killed`: it also // targets the outer loop and can also skip the reassignment `x = [v, v, v]`, so the use // of `x` in `let mut y = x` must be cloned, not moved. - // - // This snapshot currently records the WRONG decision (`let mut y$l5 = x$l2;`, a move). - // Once fixed, the snapshot must show `let mut y$l5 = x$l2.clone();`. let src = " unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { let mut x = [v, v, v]; @@ -2370,7 +2363,7 @@ fn continue_in_nested_while_condition_clears_killed() { let mut z$l3 = [0, 0, 0]; let mut i$l4 = 0; while (i$l4 < n$l1) { - let mut y$l5 = x$l2; + let mut y$l5 = x$l2.clone(); y$l5[0] = 9; z$l3 = y$l5; i$l4 = (i$l4 + 1); diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__expanded.snap new file mode 100644 index 00000000000..aee1df933fb --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__expanded.snap @@ -0,0 +1,24 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: expanded_code +--- +unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { + let mut x: [Field; 3] = [v, v, v]; + let mut z: [Field; 3] = [0_Field, 0_Field, 0_Field]; + let mut i: u32 = 0_u32; + while i < n { + let mut y: [Field; 3] = x; + y[0_u32] = 9_Field; + z = y; + let mut j: u32 = 0_u32; + while { + if i == 1_u32 { break; }; + j < 3_u32 + } { + j = j + 1_u32; + } + x = [v, v, v]; + i = i + 1_u32; + } + [x[0_u32], z[0_u32]] +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__stdout.snap new file mode 100644 index 00000000000..f18e9117a9c --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_break_killed/execute__tests__stdout.snap @@ -0,0 +1,5 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: stdout +--- +[regression_while_condition_break_killed] Circuit output: [0x01, 0x09] diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__expanded.snap new file mode 100644 index 00000000000..801ba217a15 --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__expanded.snap @@ -0,0 +1,24 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: expanded_code +--- +unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] { + let mut x: [Field; 3] = [v, v, v]; + let mut z: [Field; 3] = [0_Field, 0_Field, 0_Field]; + let mut i: u32 = 0_u32; + while i < n { + let mut y: [Field; 3] = x; + y[0_u32] = 9_Field; + z = y; + i = i + 1_u32; + let mut j: u32 = 0_u32; + while { + if i == n { continue; }; + j < 3_u32 + } { + j = j + 1_u32; + } + x = [v, v, v]; + } + [x[0_u32], z[0_u32]] +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__stdout.snap new file mode 100644 index 00000000000..5947045edf5 --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_while_condition_continue_killed/execute__tests__stdout.snap @@ -0,0 +1,5 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: stdout +--- +[regression_while_condition_continue_killed] Circuit output: [0x01, 0x09]