Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy

[coord-e]

Summary

When a &mut-bearing field is moved out of an aggregate (e.g. passed to a call) and the parent local is later dropped, the parent is dropped wholesale. This re-touches the already-moved field and resolves its mutable-borrow prophecy a second time, with a different current value. The two resolutions contradict each other, so the constraint system becomes vacuously satisfiable and the verifier accepts false assertions.

Reproduction (no closures involved)

struct Wrap<'a> {
    r: &'a mut i32,
}

fn bump(r: &mut i32) {
    *r += 1;
}

fn apply(w: Wrap) {
    bump(w.r); // moves `w.r` out into the call; `w` is then dropped wholesale
}

fn main() {
    let mut x = 1;
    let w = Wrap { r: &mut x };
    apply(w);
    assert!(x == 999); // actually x == 2, but this is accepted
}

assert!(x == 999) (and even assert!(false)-style asserts) are accepted, confirming the constraints are contradictory rather than merely under-constrained.

Root cause

moved_locals in src/analyze/basic_block/drop_point.rs only excludes a local from the implicit drop set when it is moved as a whole local:

fn visit_operand(&mut self, operand: &mir::Operand<'tcx>, _location: mir::Location) {
    if let mir::Operand::Move(place) = operand {
        if place.projection.is_empty() && !self.body.local_decls[place.local].ty.is_ref() {
            self.locals.insert(place.local);
        }
    }
}

In apply, the relevant MIR is roughly:

_2 = move (_1.0)            // move the field out
bump(move _2) / call(...)   // _2 consumed by the call
// _1 is now dead and gets dropped wholesale

Because move (_1.0) has a non-empty projection, _1 is never registered in moved_locals, so the drop-point analysis still schedules a wholesale drop of _1. Dropping _1 walks into field 0 — which was already moved out — and resolves its &mut prophecy again. For owned/immutable fields this wholesale drop is harmless (no prophecy), which is why it only surfaces with a &mut-bearing field.

Relationship to #46 / #120

Found while reviewing #120 (FnMut-closure-via-FnOnce). The same shape shows up when an FnMut closure is stored in a struct and called via (h.f)(..), since the closure environment owns a captured &mut. That nesting is out of scope for #46 (whose example is the direct apply(closure) case, which #120 handles soundly and completely), and the bug is independent of closures as the reproduction above shows. On main the struct-field-closure variant panics in the unimplemented case 3 rather than reaching this drop, so this is a distinct, pre-existing issue.

Possible direction

Track partial field-moves so the parent aggregate is not dropped wholesale once a field has been moved out — i.e. drop only the still-initialized sub-places, mirroring rustc's drop elaboration / move-path bookkeeping rather than moved_locals' whole-local-only check.