[kasimte]

move_storagelive_call_to_loophead copies a loop-body local's initializer up to the loop head, so CBMC can infer a nested loop's assigns clause (#4179). It was copying in cases that don't need it or can't support it. Two fixes, each only skips a copy it used to make:

• Copy only when an inner loop writes the local. A single loop never needs the copy, so the initializer is no longer lifted to the loop head, where the values it reads aren't defined yet. This unblocks a loop-invariant proof of a binary-search loop (no kani::unwind). (for-loop iterator setup still copies unconditionally.)
• Copy only when the block can move. Re-targeting a moved group's terminator only works when it has a single target. A branching SwitchInt (let x = if c { f() } else { g() }) does not, and used to panic (Loop contracts: ICE "Kani can only insert instructions after terminators that have a target field" when a loop-local is initialized through branching control flow #4959). It is now left in place.

Skipping a copy can leave a false failure at the loop head, but never a false VERIFICATION SUCCESSFUL. Known gap: a write through &mut isn't counted as an inner-loop write, so that copy is skipped too. The copied code's own side effects are pre-existing, tracked in #4982.

Resolves #4911. Resolves #4949. Resolves #4959.

Testing: the #4911/#4949 and #4959 reproducers fail on main and verify here. The nested-loop cases that must still be copied still verify (nested_loop_local_var_func_call.rs).

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Copilot review overview

🟡 Changes recommended

Projected writes are incorrectly treated as definitions of their base locals, causing both unsafe copies and unnecessary skipped copies.

Review effort: Balanced
Findings: 1

Open (1)

• Projection writes incorrectly define their base locals · New

What changed in this PR

Prevents unsafe loop-body initialization copies that read loop-local state or contain unsupported control flow.

Changes:

• Adds loop-local dependency and splice-shape checks.
• Adds positive, negative, and branching regression tests.

File	Description
kani-compiler/​src/​kani_middle/​transform/​loop_contracts.rs	Adds copy eligibility analysis.
tests/​expected/​loop-contract/​loop_local_var_branching_init.rs	Tests loop-local branching initialization.
tests/​expected/​loop-contract/​loop_local_var_branching_init.expected	Records successful verification.
tests/​expected/​loop-contract/​loop_local_var_branching_init_external_cond.rs	Tests externally controlled branching.
tests/​expected/​loop-contract/​loop_local_var_branching_init_external_cond.expected	Records successful verification.
tests/​expected/​loop-contract/​loop_head_call_computed_index.rs	Tests computed-index calls.
tests/​expected/​loop-contract/​loop_head_call_computed_index.expected	Records successful harness results.
tests/​expected/​loop-contract/​loop_head_call_computed_index_fail.rs	Tests genuine bounds failure.
tests/​expected/​loop-contract/​loop_head_call_computed_index_fail.expected	Records expected verification failure.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Thanks for splitting this into two independent fixes, and for writing down the known limitations. Both fixes do what the description says. #4911's check_with_closure verifies, both #4959 reproducers verify instead of panicking, and the three tests that should fail on main do. The loop-contract expected suite passes (67/0/6) with this branch merged on current main.

I'm requesting changes because the gate refuses copies that main needs for nested-loop assigns inference (#4179), so programs that verify today start failing Check assigns clause inclusion. 039c19513 fixed the projection-write case from Copilot's thread: my *acc = j reproducer verifies again. Two ways in remain, each with a reproducer inline:

1. Rvalue::CheckedBinaryOp is not modeled, so any initializer with checked arithmetic, e.g. let mut j = sum_pair(t1 + 1, t2);, is refused. This is the one most users will hit.
2. Locals the pass has already copied to the same head are still classified as dead there (let a = f(t1); let mut j = g(a);).

These are spurious failures, not unsound results. I also checked the other direction and found no case where refusing a copy hides a real failure. A MirVisitor with visit_local and PlaceContext would fix 1 and remove the arm list, and it would give you the read/write order the question on line 962 is about. Adding a nested-loop test that needs the copy would keep this from regressing again.

Separately, while trying to break the copy, I found that liveness isn't the only problem with it. Because the copy runs once before the loop, a call with side effects, a kani::assume in the callee, or a panic on a path where the body never runs can each make Kani report SUCCESSFUL for a program whose assertion fails natively, and the for-loop machinery computes a nested iterator once from a stale outer value. All of that is on main today and none of it comes from this PR, so I don't want to block on it here. Please open a GitHub issue with the reproducers above (one issue, or two: side effects, assume and panics in the head copy, and the stale nested iterator), and make the comment at line 1055 say that the gate covers liveness only.

What I didn't run: -Z uninit-checks, coverage, and the full regression script (CI covered the last one on 9f9b2274d and was green; it hasn't run on 039c19513 yet).

[kasimte]

Thanks for the review. Just updated with four commits:

• 41df310b0: an ordered MirVisitor walk replaces the arm list, so nothing is refused as unanalyzable now.
• 3993ddddd: track locals an earlier move to the head already made live.
• 12e1235ba: drop call destinations from the fallback's definition sites.
• 96ef9934a: scope the comments to live storage, linking #4982.

loop-contract suite 67/0/6. nested_loop_local_var_func_call.rs covers all five shapes (checked arithmetic, a call-initialized local, a reference, a &mut write, the #4179 move). Also resolves #4949, which verifies with and without an explicit loop_modifies.

Fork CI: Format Check and Cargo Deny pass. Kani CI is red only on zerocopy 0.8.60 failing to compile in the cargo-kani regression, not from this PR and hitting any fresh Kani build. The loop-contract suite passes there, and the three failures are all zerocopy-dependent.

[feliperodri]

Thanks for working through round 1 so thoroughly. The MirVisitor walk and the per-head live set fix both regressions I reported. #4982 has the reproducers. Every new harness passes, and the three tests that should fail on main still do. With this branch merged on current main, the loop-contract suite passes (76/0/4), and fmt and both clippy gates are clean.

I'm still requesting changes, for two reasons, each with a reproducer inline:

1. The gate still refuses copies that #4179 needs. In Kani's MIR a plain let start = i + 1; has no StorageLive, so the fallback counts it as dead, and let mut j = f(start); in front of an inner loop stops being copied. That program verifies on main and fails Check assigns clause inclusion here, at every MIR opt level I tried except 0. Writing id(i + 1) instead makes it verify, which says the rule tracks how a local was computed, not whether it exists at the head. The flip side is that #4911 with let mid = add(base, half); still fails.
2. When a nested for iterator group can't be retargeted, the copy is skipped but the body's kani_into_iter call is still replaced with a goto. The iterator is then uninitialized: main panics on these programs, and this branch reports an overflow inside KaniIter::len instead.

Both are spurious failures. I checked the other direction (wrong invariants, wrong assertions, loop_modifies violations, loop, while let, closures, generics, on_entry, opt levels 1 and 2), and refusing a copy never hid a real failure.

For 1, I think the gate should ask whether the copy is needed rather than whether its reads are live. The copy exists only so CBMC can infer an inner loop's assigns clause. I prototyped "copy only when an inner loop writes the local" (snippet on line 955). It passes the suite and all of your tests, fixes both cases in 1, and also fixes the single-loop reproducers in #4982. If you see a reason that rule is wrong, I'd like to hear it. Fixing 2 means tracking which kaniiter groups were moved.

The branch also conflicts with main after #4946 (head_live versus decreases_bindings in move_storagelive_assign_to_loophead); keeping both works.

What I didn't run: -Z uninit-checks, coverage, and the full regression script. CI has only run Auto Label on this head.

One more thing, not caused by this PR: could you open an issue for a soundness hole I hit while probing? At -Zmir-opt-level=2 and above, a loop that writes a variable missing from its loop_modifies clause verifies, on main as well as here (I raised the same thing on #4947). Nothing reads the kani_loop_modifies binding, so MIR optimizations remove it and CBMC infers the write set instead. This reproduces it with RUSTFLAGS=-Zmir-opt-level=2 kani file.rs -Z loop-contracts (it fails Check that hidden is assignable at level 1):

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]

#[kani::proof]
fn opt2_modifies_ignored() {
    let mut i: u32 = 0;
    let mut hidden: u32 = 0;
    #[kani::loop_invariant(i <= 5)]
    #[kani::loop_modifies(&i)]
    while i < 5 {
        hidden = i;
        i = i + 1;
    }
    assert!(i == 5);
    std::hint::black_box(hidden);
}

The #[inline(never)] keep-alive that #4946 uses for the decreases binding fixes it in my test.

[kasimte]

@feliperodri Thanks for looking again and the detailed review.

I rebased and addressed comments. Filed the mir-opt-2 loop_modifies hole as #5053. Re-requesting review.