From 4b61feb9f64765bb5d1de2ff7aa9ed576e040d09 Mon Sep 17 00:00:00 2001 From: AztecBot Date: Wed, 8 Jul 2026 12:20:03 +0000 Subject: [PATCH] fix(ssa): accept array_set on transitively-fresh swapped loop sibling --- .../ssa/validation/rc_invariant/array_set.rs | 224 ++++++++++++++++++ .../src/ssa/validation/rc_invariant/mod.rs | 159 +++++++++++-- 2 files changed, 367 insertions(+), 16 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/array_set.rs b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/array_set.rs index fdc8ef83dbf..aa722499549 100644 --- a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/array_set.rs +++ b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/array_set.rs @@ -468,6 +468,230 @@ mod tests { assert_verifier_rejects(src); } + /// **Transitively-fresh swapped sibling through a nested loop header.** + /// Reduced from AST-fuzzer seed `0xfe6bbee600100000` + /// (`comptime_vs_brillig_direct`). The mutated array `v105` (outer header + /// `b21`) is rebound on its back-edge (`b25: jmp b21(v74, v106)`) to the + /// *inner*-loop header parameter `v106` (`b24`) — not a sibling parameter of + /// its own header. `v106` mixes two sources: a fresh `make_array` (`v71`) on + /// its own back-edge (`b28: jmp b24(v71, v40)`) and a forward-edge alias of + /// the mutated `v105` (`b22: jmp b24(v105, u32 0)`). The mutating branch + /// `b23` is only reachable after the inner loop has re-defined the + /// loop-carried value from its fresh back-edge source, so the value `v105` + /// mutates is a distinct per-iteration allocation and every `array_get v106` + /// read happened on a prior iteration over different fresh storage. Sound — + /// the swap exclusion must follow the sibling transitively across the nested + /// header's fresh back-edge and drop `v106` from `v105`'s alias-set. + #[test] + fn accepts_array_set_on_transitively_fresh_swapped_sibling() { + let src = r#" + brillig(inline_always) fn func_1 f0 { + b0(v0: [[u8; 2]; 3], v2: [[u8; 2]; 3], v4: &mut u32): + jmp b1(u128 8302379352820642275318148290232816646, v0, v2) + b1(v7: u128, v95: [[u8; 2]; 3], v96: [[u8; 2]; 3]): + v9 = lt v7, u128 8302379352820642275318148290232816647 + jmpif v9 then: b2(), else: b3() + b2(): + jmp b4(v95, v96, u32 0) + b3(): + v90 = make_array b"GO" + v92 = make_array b"GD" + v93 = make_array b"LO" + v94 = make_array [v90, v92, v93] : [[u8; 2]; 3] + return v94 + b4(v97: [[u8; 2]; 3], v98: [[u8; 2]; 3], v99: u32): + jmpif u1 0 then: b5(), else: b6() + b5(): + v14 = eq v99, u32 1 + jmpif v14 then: b7(), else: b8() + b6(): + v86 = cast v7 as Field + v88 = unchecked_add v7, u128 1 + jmp b1(v88, v97, v98) + b7(): + jmp b6() + b8(): + v16 = add v99, u32 1 + jmp b10(v97, v98, u32 0) + b9(): + jmp b4(v100, v101, v16) + b10(v100: [[u8; 2]; 3], v101: [[u8; 2]; 3], v102: u32): + v20 = eq v102, u32 2 + jmpif v20 then: b12(), else: b13() + b11(): + jmp b9() + b12(): + jmp b11() + b13(): + v22 = add v102, u32 1 + jmp b15(v101, u32 0) + b14(): + jmp b10(v82, v100, v22) + b15(v103: [[u8; 2]; 3], v104: u32): + jmpif u1 1 then: b16(), else: b17() + b16(): + v26 = eq v104, u32 0 + jmpif v26 then: b18(), else: b19() + b17(): + v81 = array_get v103, index u32 1 -> [u8; 2] + inc_rc v81 + inc_rc v81 + v82 = make_array [v81, v81, v81] : [[u8; 2]; 3] + jmp b14() + b18(): + jmp b17() + b19(): + v28 = add v104, u32 1 + jmp b21(u16 0, v103) + b20(): + jmp b15(v79, v28) + b21(v34: u16, v105: [[u8; 2]; 3]): + v35 = eq v34, u16 0 + jmpif v35 then: b22(), else: b23() + b22(): + jmp b24(v105, u32 0) + b23(): + v77 = make_array b"CG" + v79 = array_set v105, index u32 2, value v77 + jmp b20() + b24(v106: [[u8; 2]; 3], v107: u32): + v38 = eq v107, u32 2 + jmpif v38 then: b26(), else: b27() + b25(): + v72 = cast v7 as Field + v74 = unchecked_add v34, u16 1 + jmp b21(v74, v106) + b26(): + jmp b25() + b27(): + v40 = add v107, u32 1 + v62 = make_array b"{\"kind\":\"unsignedinteger\",\"width\":128}" + call print(u1 1, v7, v62, u1 0) + v65 = array_get v106, index u32 1 -> [u8; 2] + inc_rc v65 + v67 = array_get v106, index u32 2 -> [u8; 2] + inc_rc v67 + v70 = make_array b"SL" + v71 = make_array [v65, v67, v70] : [[u8; 2]; 3] + jmp b28() + b28(): + jmp b24(v71, v40) + } + "#; + assert_verifier_accepts_because( + src, + "v105's outer back-edge rebinds it to the inner-loop header param v106, whose \ + loop-carried definition v71 is an iteration-local make_array — so v106 is a \ + distinct per-iteration storage and the swap exclusion drops it from v105's alias-set", + ); + } + + /// **Nested-swap soundness canary — the inner loop must re-freshen the + /// swapped-in sibling.** Same outer-back-edge swap `v105 ← v106` as + /// [`Self::accepts_array_set_on_transitively_fresh_swapped_sibling`], but the + /// inner loop threads `v106` back onto its own back-edge **unchanged** + /// (`b28: jmp b24(v106, v40)`) instead of a fresh `make_array`. Now `v106` + /// is loop-invariant storage that stays equal to the entry `v105`, so the + /// in-loop `array_get v106` reads the very storage the outer + /// `array_set v105` mutates in place. The transitive-freshness relaxation + /// must **not** fire (the inner back-edge arg is not iteration-local fresh), + /// and the verifier must reject. Guards the load-bearing freshening + /// requirement of the nested extension. + #[test] + fn end_to_end_nested_swap_without_inner_freshening_is_rejected() { + let src = r#" + brillig(inline_always) fn func_1 f0 { + b0(v0: [[u8; 2]; 3], v2: [[u8; 2]; 3], v4: &mut u32): + jmp b1(u128 8302379352820642275318148290232816646, v0, v2) + b1(v7: u128, v95: [[u8; 2]; 3], v96: [[u8; 2]; 3]): + v9 = lt v7, u128 8302379352820642275318148290232816647 + jmpif v9 then: b2(), else: b3() + b2(): + jmp b4(v95, v96, u32 0) + b3(): + v90 = make_array b"GO" + v92 = make_array b"GD" + v93 = make_array b"LO" + v94 = make_array [v90, v92, v93] : [[u8; 2]; 3] + return v94 + b4(v97: [[u8; 2]; 3], v98: [[u8; 2]; 3], v99: u32): + jmpif u1 0 then: b5(), else: b6() + b5(): + v14 = eq v99, u32 1 + jmpif v14 then: b7(), else: b8() + b6(): + v86 = cast v7 as Field + v88 = unchecked_add v7, u128 1 + jmp b1(v88, v97, v98) + b7(): + jmp b6() + b8(): + v16 = add v99, u32 1 + jmp b10(v97, v98, u32 0) + b9(): + jmp b4(v100, v101, v16) + b10(v100: [[u8; 2]; 3], v101: [[u8; 2]; 3], v102: u32): + v20 = eq v102, u32 2 + jmpif v20 then: b12(), else: b13() + b11(): + jmp b9() + b12(): + jmp b11() + b13(): + v22 = add v102, u32 1 + jmp b15(v101, u32 0) + b14(): + jmp b10(v82, v100, v22) + b15(v103: [[u8; 2]; 3], v104: u32): + jmpif u1 1 then: b16(), else: b17() + b16(): + v26 = eq v104, u32 0 + jmpif v26 then: b18(), else: b19() + b17(): + v81 = array_get v103, index u32 1 -> [u8; 2] + inc_rc v81 + inc_rc v81 + v82 = make_array [v81, v81, v81] : [[u8; 2]; 3] + jmp b14() + b18(): + jmp b17() + b19(): + v28 = add v104, u32 1 + jmp b21(u16 0, v103) + b20(): + jmp b15(v79, v28) + b21(v34: u16, v105: [[u8; 2]; 3]): + v35 = eq v34, u16 0 + jmpif v35 then: b22(), else: b23() + b22(): + jmp b24(v105, u32 0) + b23(): + v77 = make_array b"CG" + v79 = array_set v105, index u32 2, value v77 + jmp b20() + b24(v106: [[u8; 2]; 3], v107: u32): + v38 = eq v107, u32 2 + jmpif v38 then: b26(), else: b27() + b25(): + v72 = cast v7 as Field + v74 = unchecked_add v34, u16 1 + jmp b21(v74, v106) + b26(): + jmp b25() + b27(): + v40 = add v107, u32 1 + v65 = array_get v106, index u32 1 -> [u8; 2] + inc_rc v65 + v67 = array_get v106, index u32 2 -> [u8; 2] + inc_rc v67 + jmp b28() + b28(): + jmp b24(v106, v40) + } + "#; + assert_verifier_rejects(src); + } + /// ACIR functions are skipped: `inc_rc` / `dec_rc` are no-ops in ACIR and /// `array_set` always produces a fresh array. #[test] diff --git a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs index 552330de971..a7914e1cfc3 100644 --- a/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs +++ b/compiler/noirc_evaluator/src/ssa/validation/rc_invariant/mod.rs @@ -337,6 +337,19 @@ struct Context<'f> { /// swapped into `P` would make `P_k = Q_{k-1} = Q_k` and genuinely /// alias. /// + /// **Nested swap.** `Q` need not be a sibling parameter of `P`'s own + /// header: it may instead be the loop-carried parameter of a *nested* loop + /// header that re-freshens it every iteration (the back-edge `P ← Q` + /// threads out the inner loop's exit value). The freshening requirement + /// then applies to the *inner* loop's back-edge, and the back-edge-only + /// entry guard is replaced by a structural one — the inner loop is exited + /// only through its header's branch and the header does not read `Q`, so + /// the value threaded out is a header-entry value never read on its own + /// iteration. See `is_transitively_fresh_sibling` in [`Context::new`]. + /// Because such a `Q` also carries a forward-edge alias of `P` into its own + /// loop, [`Context::find_reachable_aliased_use`] additionally marks it + /// *protected* so the forward walk never re-adds it. + /// /// **Forward propagation.** After recording, exclusions are pushed /// forward across non-back-edge parameter edges to a fixed point: on a /// forward edge `R ← P`, `R` *is* `P` within the same iteration, so `R` @@ -499,11 +512,103 @@ impl<'f> Context<'f> { let fresh_array_values: HashSet = make_array_values.union(&call_result_values).copied().collect(); + // Index each loop's block set by its header so the nested-sibling + // relaxation below can find the loop a swapped-in value heads. + let mut loops_by_header: HashMap>> = + HashMap::default(); + for l in &loops.yet_to_unroll { + loops_by_header.entry(l.header).or_default().push(&l.blocks); + } + + // Whether `sibling` is a *distinct per-iteration storage* by virtue of + // being the loop-carried parameter of a **nested** loop header that + // re-freshens it every iteration — the transitive analog of the + // same-header freshening the swap exclusion already recognizes. It lets + // an outer back-edge swap `source ← sibling` drop `sibling` even though + // `sibling` is a parameter of a *different* header (and may itself carry + // a forward-edge alias of `source` into its own loop). + // + // All three conditions must hold: + // + // 1. `sibling` is a parameter (at `sib_pos`) of some loop header + // `sib_header`, and on **every** back-edge into `sib_header` the arg + // threaded into `sib_pos` is an iteration-local fresh allocation — so + // each completed inner iteration rebinds `sibling` to distinct + // storage. + // 2. The inner loop's only exit is its header's own branch (no loop + // block other than `sib_header` has an edge leaving the loop). Then + // the value threaded out of the loop is always a *header-entry* value + // of the exiting iteration — the one on which the body did **not** + // run. + // 3. `sib_header` itself does not read `sibling`. Combined with (2), + // that header-entry exit value was never read on its own iteration, + // while every in-loop read of `sibling` saw a distinct earlier + // allocation (by (1)). So the storage the outer `array_set` later + // mutates in place — the swapped-in exit value — has no live aliased + // read, exactly as the same-header case guarantees. + let is_transitively_fresh_sibling = |sibling: ValueId| -> bool { + let Some((sib_header, sib_pos)) = loops_by_header.keys().find_map(|&h| { + function + .dfg + .block_parameters(h) + .iter() + .position(|&p| p == sibling) + .map(|pos| (h, pos)) + }) else { + return false; + }; + + // (1) Every back-edge re-freshens `sibling`. + let mut saw_back_edge = false; + for &(bs, h) in &back_edges { + if h != sib_header { + continue; + } + saw_back_edge = true; + let Some(args) = incoming_edges + .get(&sib_header) + .and_then(|edges| edges.iter().find(|(pred, _)| *pred == bs)) + .map(|(_, args)| args) + else { + return false; + }; + if !args.get(sib_pos).is_some_and(|a| iteration_local_fresh.contains(a)) { + return false; + } + } + if !saw_back_edge { + return false; + } + + // (2) The loop is exited only through its header's branch. + for blocks in loops_by_header.get(&sib_header).into_iter().flatten() { + for &b in *blocks { + if b != sib_header && cfg.successors(b).any(|s| !blocks.contains(&s)) { + return false; + } + } + } + + // (3) The header does not read `sibling` (terminator args aside — + // those are the legitimate threading mechanism). + for &inst_id in function.dfg[sib_header].instructions() { + let mut reads_sibling = false; + function.dfg[inst_id].for_each_value(|v| reads_sibling |= v == sibling); + if reads_sibling { + return false; + } + } + + true + }; + // Swap exclusions. For every loop back-edge `be_start → header`, // inspect each array-typed header parameter at `source_pos`: if - // the back-edge rebinds it to a *sibling* header parameter - // (`source ← sibling`) whose own back-edge arg is an - // iteration-local fresh allocation, and the source and sibling + // the back-edge rebinds it to a *sibling* freshly-reallocated + // per-iteration storage (`source ← sibling`) — either a sibling + // header parameter freshened on its own back-edge, or a nested loop + // header's loop-carried parameter (see + // `is_transitively_fresh_sibling`) — and the source and sibling // receive distinct storage on every forward edge into the header, // record the sibling as excluded from the source's alias-set. See // [`Context::swap_excluded_aliases`]. @@ -527,13 +632,23 @@ impl<'f> Context<'f> { if sibling == source_param { continue; } - let Some(sibling_pos) = params.iter().position(|&pp| pp == sibling) else { - continue; + // The swapped-in sibling must be a *distinct per-iteration + // storage*. Two shapes qualify: + // - **Same-header swap** (the #12929 relaxation): `sibling` is + // another parameter of `header` whose own back-edge arg is an + // iteration-local fresh allocation (the `c3 = [..]` / + // `c3 = f()` half of the swap). + // - **Nested swap**: `sibling` is the loop-carried parameter of + // a *nested* loop header, re-freshened on that inner loop's + // back-edge — see `is_transitively_fresh_sibling`. + let sibling_pos = params.iter().position(|&pp| pp == sibling); + let sibling_is_fresh = match sibling_pos { + Some(pos) => { + be_args.get(pos).is_some_and(|a| iteration_local_fresh.contains(a)) + } + None => is_transitively_fresh_sibling(sibling), }; - // The sibling's own back-edge arg must be an - // iteration-local fresh allocation (the `c3 = [..]` or - // `c3 = f()` half of the swap). - if !be_args.get(sibling_pos).is_some_and(|a| iteration_local_fresh.contains(a)) { + if !sibling_is_fresh { continue; } // Loop-entry guard. On every *forward* edge into the @@ -564,12 +679,14 @@ impl<'f> Context<'f> { if source_forward_aliases.contains(&sibling) { return true; } - args.get(sibling_pos).is_some_and(|&sibling_forward_arg| { - let sibling_forward_aliases = backward_set(sibling_forward_arg); - source_forward_aliases - .iter() - .any(|x| sibling_forward_aliases.contains(x)) - }) + sibling_pos.and_then(|sp| args.get(sp)).is_some_and( + |&sibling_forward_arg| { + let sibling_forward_aliases = backward_set(sibling_forward_arg); + source_forward_aliases + .iter() + .any(|x| sibling_forward_aliases.contains(x)) + }, + ) }); if entry_aliased { continue; @@ -1152,7 +1269,7 @@ impl<'f> Context<'f> { // the loop-header parameter on the back-edge, since the value // threaded back is this protected participant rather than a // still-live alias. - let protected: im::HashSet = alias_set + let mut protected: im::HashSet = alias_set .iter() .copied() .filter(|&v| { @@ -1161,6 +1278,16 @@ impl<'f> Context<'f> { && self.back_edge_participants.contains(&v) }) .collect(); + // A swap-excluded sibling is a distinct per-iteration storage + // ([`Context::swap_excluded_aliases`]); besides being dropped from the + // seed alias-set in [`Context::alias_set_for`], it must never be + // *re-added* to the use-set by the forward walk's add-rule when the + // source flows into it on a forward edge (the nested swap feeds + // `sibling ← source` on the inner loop's entry edge). Marking it + // protected keeps it out for the whole walk. + if let Some(excluded) = self.swap_excluded_aliases.get(&source) { + protected.extend(excluded.iter().copied()); + } let use_set: im::HashSet = alias_set.iter().copied().filter(|v| !protected.contains(v)).collect();