Incompleteness: a `&mut` stored in a `Vec` (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as `Unsat`

[coord-e]

Summary

When a &mut T is stored in a Vec<&mut T> (more generally, in any value whose model contains a Seq/Array), the reference's prophecy is never resolved — not even when the Vec is dropped. Env::dropping_formula_for_term walks &mut, Box (is_own), tuples, and enums to emit the final == current fact that closes out each live &mut's prophecy, but it has no arm for Type::Array (the sort that backs the Seq/Vec model), so the array's elements fall through to the empty else branch. The referent's prophecy variable is left unconstrained (havoc), and every subsequent assertion about the referent becomes unprovable ⇒ the program is rejected as Unsat even though it never panics.

This is an incompleteness bug (safe programs wrongly rejected) — not an unsoundness and not a panic.

Minimal reproducer

#[thrust::callable]
fn f(a: &mut i64) {
    let old = *a;
    {
        let mut v: Vec<&mut i64> = Vec::new();
        v.push(&mut *a);
    }               // `v` dropped here; `a` was never written through
    assert!(*a == old);
}
fn main() {}

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

a is never written (the &mut *a is only pushed into v, which is then dropped), so *a == old holds for every input and the program never panics. Thrust reports Unsat.

A write-through variant is rejected the same way and is likewise safe at runtime:

#[thrust::callable]
fn f(a: &mut i64) {
    {
        let mut v: Vec<&mut i64> = Vec::new();
        v.push(&mut *a);
        *v[0] = 5;
    }
    assert!(*a == 5);   // holds at runtime; Thrust: Unsat
}
fn main() {}

(Both programs were compiled with real rustc and executed over a range of inputs including i64::MIN/i64::MAX; neither ever panics.)

The gap is specific to the Seq/array-backed container

Every other container resolves the prophecy correctly on the identical shape — only the Vec case is rejected:

&mut i64 held in … then dropped without further writes	expected	Thrust
Vec<&mut i64>	SAFE	Unsat ❌
Box<&mut i64>	SAFE	SAFE ✓
(&mut i64,) (tuple)	SAFE	SAFE ✓
enum-variant payload	SAFE	SAFE ✓

And Vec<&mut _> is otherwise supported: pushing and reading/writing through the element before the Vec is dropped verifies correctly —

#[thrust::callable]
fn f(a: &mut i64) {
    let mut v: Vec<&mut i64> = Vec::new();
    v.push(&mut *a);
    *v[0] = 5;
    assert!(*v[0] == 5);   // SAFE
}
fn main() {}

— so it is only the drop-time prophecy resolution of the contained &mut that is missing. Wrapping the Vec in a tuple (let _w = (v, 0);) is rejected the same way, confirming the miss is inside the array walk, not at the top level.

Root cause

Env::dropping_formula_for_term (src/refine/env.rs:1112) emits the prophecy-closing fact for each &mut reachable in the dropped value's type:

if ty.is_mut() {
    term.clone().mut_final().equal_to(term.mut_current()).into()   // resolves the prophecy
} else if ty.is_own() {
    // recurse into Box payload
} else if let Some(tty) = ty.as_tuple() {
    // recurse into each tuple element
} else if let Some(ety) = ty.as_enum() {
    // recurse into each variant field (via a matcher predicate)
} else {
    chc::Body::default()   // <-- Type::Array (hence Seq/Vec) lands here: nothing emitted
}

There is no arm for Type::Array. The Vec/Seq model is Seq { array: Array<Int, T>, length: Int }, so dropping a Vec<&mut i64> recurses through the Seq struct into its array: Array<Int, &mut i64> field, which matches none of the arms and yields an empty body. The &mut elements' final == current facts are never emitted, the referent's prophecy stays free, and the post-drop assertion is unprovable.

Suggested direction

An Array arm would need to resolve the prophecy for every live element in [0, length), which — unlike the fixed-arity tuple/enum cases — requires a universally-quantified drop fact over the array index (analogous to how the enum arm introduces a matcher_pred, but ranging over 0 <= i < length). Until then, any &mut that flows through a Vec/slice/array and is dropped cannot be reasoned about after its container's scope ends.

Relation to existing issues

Distinct from the other drop/prophecy issues:

• 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 (&mut in Box): the box's prophecy is resolved at drop (the is_own arm handles it); 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 is about reading the referent before the box drops. Here the Vec's prophecy is never resolved at all.
• Incompleteness: dropping a recursively-defined ADT does not resolve &mut prophecies stored in its recursive-position field, so safe programs are wrongly rejected #173 / Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 (recursive user ADTs): those live in the recursive-variant field / stack-overflow of the as_enum arm; this is the missing Type::Array arm.
• Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121 / Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122 (partially-moved / partial-field-move aggregates): no move is involved here.

Notes

• No numerical-range / overflow concern.
• Not a panic — a clean Unsat verdict.

Environment

• branch main @ 6953863
• solver: Z3 (HORN / Spacer)