Incompleteness: an explicit `invariant!` on a loop that writes through a `&mut` drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it)

[coord-e]

Summary

When a while loop that mutates a referent through a &mut carries a user-supplied thrust_macros::invariant!, the reference's prophecy (final-value) link to its referent is dropped across the loop. The invariant can still constrain the current value *p (and that constraint survives the loop — a read of *p after the loop verifies fine), but when the borrow ends and the referent's value is reconstructed from the prophecy, that value is left unconstrained (havoc'd). Any assertion about the original variable after the loop then fails to verify, even though it provably cannot panic.

This is an incompleteness / accepts-safe-rejects direction (false positive), not a soundness hole — the value is left unconstrained, not set to a wrong value (both assert!(x >= 1) and assert!(x < 1) are rejected, while the tautology assert!(x >= 1 || x < 1) verifies).

Crucially it is distinct from #186 and has no workaround:

• Incompleteness: an explicit invariant! havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs #186 is about live locals the loop does not modify, not restated in the invariant. Here the loop does modify *p, and p is mentioned in the invariant — so Incompleteness: an explicit invariant! havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs #186's trigger ("a live, non-singleton local not modified by the loop") and its suggested fix ("frame live locals that the loop body does not assign") do not cover this case.
• The affected quantity is the prophecy of a mutated &mut, which cannot be restated in the invariant: neither *p nor !p in the invariant repairs it (see the controls table). The relationship that is lost is the aliasing/prophecy link x == !p, which the surface invariant syntax cannot express.
• The inference path (no explicit invariant!) handles the identical program correctly (safe).

Minimal reproduction

repro.rs:

//@compile-flags: -C debug-assertions=false

#[thrust_macros::requires(true)]
#[thrust_macros::ensures(true)]
#[thrust::trusted]
fn rand() -> i64 { unimplemented!() }

fn main() {
    let mut x = 1_i64;
    {
        let p = &mut x;
        while rand() == 0 {
            thrust_macros::invariant!(|p: &mut i64| *p >= 1);
            *p = *p + 1;
        }
    } // borrow of x ends here; x == final *p, which the invariant keeps >= 1
    assert!(x >= 1); // always true at runtime
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs && echo safe
error: verification error: Unsat

error: aborting due to 1 previous error

Expected: safe. The invariant *p >= 1 is inductive (entry *p == 1; preserved because *p + 1 >= 2 >= 1), so on loop exit *p >= 1; when the borrow of x ends, x equals the final *p, hence x >= 1.
Actual: rejected as Unsat.

Ground truth (runnable variant)

A bounded, fully-deterministic version (no rand) that real rustc runs to completion and which Thrust still rejects — confirming the program is genuinely safe:

fn main() {
    let mut x = 5_i64;
    let p = &mut x;
    let mut k = 0_i64;
    while k < 3 {
        thrust_macros::invariant!(|p: &mut i64, k: i64| *p >= 5 && k >= 0 && k <= 3);
        *p = *p + 1;
        k = k + 1;
    }
    let _last = *p;
    assert!(x >= 5); // x == 8 at runtime
}

$ rustc -Adead_code --edition 2021 -o real bounded.rs && ./real ; echo "exit=$?"
exit=0                                  # runs cleanly, x == 8, assert holds
$ cargo run -q -- -Adead_code -C debug-assertions=false bounded.rs
error: verification error: Unsat        # <- WRONG: this program cannot panic

Isolation

All rows use the rand-driven loop above and differ only in the marked line. Each was cross-checked so the diagnosis (x is havoc'd, not miscomputed) is unambiguous.

Case	Verdict	Correct?
assert on the referent after the borrow ends: … } assert!(x >= 1);	Unsat	❌ bug
assert on the current value instead: … assert!(*p >= 1); (last use inside scope)	safe	✅
read current value first: let v = *p; assert!(v >= 1);	safe	✅
no explicit invariant (inference): while rand()==0 { *p = *p + 1; } let _ = *p; assert!(x >= 1);	safe	✅
restate current value: invariant!(|p: &mut i64| *p >= 1) … assert!(x >= 1)	Unsat	❌ (no workaround)
restate prophecy too: invariant!(|p: &mut i64| *p >= 1 && !p >= 1) … assert!(x >= 1)	Unsat	❌ (no workaround)
no loop at all: let p = &mut x; *p = *p + 1; let _ = *p; assert!(x >= 1);	safe	✅
flipped assert: … assert!(x < 1);	Unsat	✅ (havoc)
tautology: … assert!(x >= 1 || x < 1);	safe	✅ (confirms x is havoc'd, not miscomputed)

So the trigger is precisely: a while loop with an explicit invariant! that writes through a &mut, followed by a read of the referent after the borrow ends. The current value *p is preserved through the loop; the prophecy link from *p to the referent x is not, and cannot be restated in the invariant.

Likely root cause

Same locus as the general "user invariant replaces the inferred precondition" mechanism noted in #186 — src/analyze/local_def.rs:938-953: when a header has user invariants, the block type is built from live_locals and its precondition is set to only the conjunction of the invariant!s (rty::Refinement::top() conjoined with each invariant), discarding the inference template entirely:

if let Some(invariants) = loop_invariants.get(&bb) {
    let mut bty = self.type_builder.build_basic_block(&self.body, live_locals, ret_ty);
    let mut inv = rty::Refinement::top();
    for &(formula_def_id, generic_args) in invariants {
        inv.push_conj(self.build_invariant_precondition(formula_def_id, generic_args, &bty));
    }
    bty.set_precondition(inv);
    ...
} else if analyze::basic_block::needs_own_precondition(&self.body, bb) {
    // inference: build_basic_block(...).for_template(...) — a precondition pvar over *all*
    // live locals, which preserves the &mut's (current, prophecy) structure and its link
    // to the referent
    ...
}

But the manifestation here is distinct from #186's (which is about unmodified sibling locals): for a live p: &mut i64, the invariant precondition constrains only the current component *p. The prophecy component !p — and, more importantly, the environment fact establishing the aliasing link x == !p created when p = &mut x before the loop — is not carried into the invariant precondition and is not expressible in the invariant closure. So at the loop header the reference is rebuilt with a fresh, unconstrained prophecy, and when the borrow of x ends (prophecy resolution at the reference's liveness-death) x is set to that unconstrained value → x >= 1 cannot be discharged.

Because the loop assigns *p, #186's suggested fix (frame only the live locals the loop body does not assign) would not repair this case. A fix here needs to also frame the prophecy component and the referent-aliasing relationship of a &mut that the loop mutates — i.e., reproduce, on the explicit-invariant path, the full (current, prophecy) framing that the inference-template path already provides.

Scope / when it bites

The pattern "borrow a variable mutably, run a loop that updates it under an explicit invariant!, then use the original variable after the loop" is common (e.g. a &mut accumulator updated in a while loop, read afterwards). Any such program is currently unverifiable unless the explicit invariant is dropped in favor of Thrust's inference. Not a numeric-range/overflow/unsigned issue — the constants are small (1, 5, 8) and the discrepancy is purely about the reference's prophecy link surviving the loop.

Environment

• thrust @ a148b9d
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration
• Uses only supported features (i64, &mut, while + invariant!, assert!); distinct from the listed known issues (in particular Incompleteness: an explicit invariant! havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs #186, whose trigger is a loop-unmodified local, and Incompleteness: a &mut stored in a Box has its prophecy resolved only at the Box's drop, so reading the referent before the box is dropped wrongly rejects safe programs #175, which requires a Box with a late drop).