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

[coord-e]

Summary

A &mut reference stored inside a Box has its prophecy resolved only at the Box's drop terminator, never at the reference's actual last use. Because a Box<&mut T> carries a real drop (to free its heap allocation), the drop terminator is scheduled at the end of the box's lexical scope — which, under NLL, can come after the referent is legitimately read again. Any read of the referent between the last write-through-the-box and the box's drop is therefore evaluated against an unresolved prophecy (the final value is still an unconstrained existential), so a provably-safe program is rejected as Unsat.

This is the incompleteness direction (a safe program is wrongly rejected). It is distinct from #173 (which is about recursive ADTs skipping their recursive tail field — that path emits WARN skipping recursive variant; this one does not) and is the mirror of the unsoundness in #121/#122 (those over-resolve a moved-out field's prophecy; this one under-resolves a boxed reference's prophecy by resolving it too late).

Reproduced on af7cd99 with z3 4.16.0.

Reproduction

fn main() {
    let mut x = 1_i64;
    let bx = Box::new(&mut x); // Box<&mut i64>
    **bx = 42;                 // write 42 through the boxed reference
    assert!(x == 42);          // always true at runtime
}

$ rustc -Adead_code --edition 2021 -o real box.rs && ./real ; echo "exit=$?"
exit=0                                  # runs cleanly; the assert always holds

$ cargo run -q -- -Adead_code -C debug-assertions=false box.rs
error: verification error: Unsat        # <- WRONG: this program cannot panic

The program has no inputs and is fully deterministic, so it is safe for all executions, yet Thrust reports a possible panic.

Controls — every close variant verifies correctly, isolating the trigger to Box's late drop

program	runtime	Thrust	correct?
Box<&mut i64>, read referent while box still in scope (above)	ok	Unsat	❌ bug
same, but box dropped in an inner scope before the read: { let bx = Box::new(&mut x); **bx = 42; } assert!(x == 42);	ok	safe	✅
bare &mut i64 (no box): let r = &mut x; *r = 42; assert!(x == 42);	ok	safe	✅
tuple of &mut: let t = (&mut x,); *t.0 = 42; assert!(x == 42);	ok	safe	✅
struct with &mut field: let w = W { r: &mut x }; *w.r = 42; assert!(x == 42);	ok	safe	✅

Only the Box case fails. The bare-reference, tuple, and struct cases have no drop terminator (references / aggregates of references are trivially dropped), so their prophecy is resolved at the borrow's liveness-death — which precedes the read — and they verify. The Box carries a real drop, which is where the discrepancy comes from.

Root cause

The optimized MIR of the reproduction:

bb1: {
    _7 = copy ((_2.0: Unique<&mut i64>).0: NonNull<&mut i64>) as *const &mut i64 (Transmute);
    _6 = deref_copy (*_7);
    (*_6) = const 42_i64;                                  // write through the boxed &mut
    _4 = copy _1;                                          // read x
    switchInt(move _4) -> [42: bb3, otherwise: bb2];       // assert!(x == 42)
}
bb2: { _5 = core::panicking::panic("assertion failed: x == 42") -> bb5; }
bb3: { drop(_2) -> [return: bb4, unwind continue]; }       // Box dropped AFTER the read

The referent _1 (x) is read in bb1, but the Box _2 is only dropped in bb3. Prophecy resolution for the boxed &mut happens in drop_local → dropping_assumption → dropping_formula_for_term (src/refine/env.rs:1112), whose is_own branch recurses into the box contents and emits !inner == *inner for the inner Mut:

} else if ty.is_own() {
    let inner = &ty.as_pointer().unwrap().elem.ty;
    self.dropping_formula_for_term(existentials, inner, term.box_current())
}

That assumption is only added when _2 is dropped (bb3). At the read in bb1 the inner prophecy is still unresolved, so x's value is the unconstrained final/prophecy variable and x == 42 cannot be discharged — hence Unsat. For a bare &mut there is no drop terminator, so Thrust resolves the prophecy at the reference's liveness-death (right after (*r) = 42, before copy x), which is why the otherwise-identical bare/tuple/struct forms verify.

Note this path never hits the recursive-variant skip of #173: there is no WARN skipping recursive variant, and Box<&mut i64> is not a recursively-defined ADT.

Expected vs. actual

• Expected: the reproduction verifies (safe) — after **bx = 42, x == 42 holds, and it is read only after the boxed reference's last use.
• Actual: rejected as Unsat, because the boxed &mut's prophecy is resolved only at the Box's drop terminator, which NLL schedules after the referent read.

Suggested direction

Resolve the prophecy of a &mut owned by a Box (Own) at the reference's last use (its NLL end-of-borrow), rather than deferring it to the owning box's drop terminator — matching how bare &mut locals are already resolved at liveness-death. Equivalently, a read of a referent whose only live borrow is reachable through an about-to-be-idle box should force that box's inner-prophecy resolution.

Environment

• thrust @ af7cd99
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.16.0, default solver configuration