Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out `&mut` borrows

[coord-e]

Summary

moved_locals in src/analyze/basic_block/drop_point.rs only treats a move operand as an ownership transfer when the moved place is a whole local (place.projection.is_empty()). When a value is moved out of a projection (a partial move, e.g. let b = s.0;), the source local is still considered dead-and-droppable at the move site, so the analyzer emits an implicit drop for it.

Env::drop_local → dropping_assumption (src/refine/env.rs) then walks the local's full type — including the part that was just moved away — and emits the prophecy-resolving assumption mut_final(t) = mut_current(t) for a mutable reference whose ownership (and drop obligation) actually transferred to the destination of the move. When the program later writes through the moved reference, its prophecy is resolved a second time to a different value, making the environment assumptions inconsistent (1 = 2), after which any assertion verifies.

The result is that Thrust verifies programs that panic at runtime.

Reproduction

fn main() {
    let mut a = 1_i64;
    let s = ((&mut a,),);
    let b = s.0;     // partial move: `(&mut a,)` moves out of `s`
    *b.0 = 2;
    assert!(a == 1); // false at runtime: a == 2
}

This program panics when compiled with plain rustc:

$ rustc -C debug-assertions=off partial_move.rs && ./partial_move
thread 'main' panicked at partial_move.rs:6:5:
assertion failed: a == 1

but Thrust (at 1d85b18, z3 4.13.4) accepts it:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false partial_move.rs && echo verified safe
verified safe

Control: the whole-local move is handled correctly

Replacing the partial move with a whole-local move (which is recorded by moved_locals) makes Thrust reject the program as expected:

fn main() {
    let mut a = 1_i64;
    let s = ((&mut a,),);
    let b = s;       // whole-local move: drop of `s` correctly suppressed
    *(b.0).0 = 2;
    assert!(a == 1);
}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false whole_move.rs
error: verification error: Unsat

The only difference between the two programs is whether the move operand has a projection.

Analysis

The optimized MIR of the reproducer is:

bb0: {
    _1 = const 1_i64;            // a
    _4 = &mut _1;
    _3 = (move _4,);
    _2 = (move _3,);             // s
    _5 = move (_2.0: (&mut i64,)); // b — partial move out of s
    _8 = deref_copy (_5.0: &mut i64);
    (*_8) = const 2_i64;
    _6 = copy _1;
    switchInt(move _6) -> [1: bb2, otherwise: bb1];
}

With RUST_LOG=info, the analyzer logs:

implicitly dropped after statement local=_2 stmt_idx=4

i.e. s (_2) is implicitly dropped immediately after the partial move _5 = move (_2.0).

Two pieces interact:

1. moved_locals (src/analyze/basic_block/drop_point.rs, in fn moved_locals):

   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);
           }
       }
   }

   move (_2.0) has a non-empty projection, so _2 is not recorded as moved. Since _2 is dead after this statement (per MaybeLiveLocals), it lands in the implicit-drop set for stmt_idx = 4. The doc comment above this function even states the invariant being violated: a moved local's "drop obligation (including resolving any mutable-borrow prophecies it owns) moves to the destination and it must not be dropped at the move site" — but this is only enforced for whole-local moves.

2. dropping_assumption (src/refine/env.rs) is type-driven and walks the entire current type of the dropped local. For s it recurses tuple → own → tuple → own → mut and reaches the &mut i64 that was just moved into b, emitting:

   builder.push_formula(term.clone().mut_final().equal_to(term.mut_current()));

   i.e. final(a-borrow) = current(a-borrow) = 1. Because the environment binding for the moved-out field still points at the same temp-var chain that b's binding was derived from, the later assignment *b.0 = 2 resolves the same prophecy to 2. The CHC body now contains both final = 1 and final = 2, so the clause body is unsatisfiable and the false assertion a == 1 is "verified".

Note that the more common partial-move shape let b = s.0; where the field type is &mut T itself is not affected, because ReborrowVisitor::visit_operand turns moves of Ref-typed operands into reborrows. The hole is reachable whenever the moved projection's type is a non-reference type that (transitively) owns a mutable borrow — e.g. a tuple/struct field of type (&mut T,), Box<&mut T>, or a struct containing a &mut.

Expected behavior

A local that is partially moved must not have a dropping assumption emitted for the moved-out portion (or, conservatively, for any portion). Either:

• record partially-moved locals in moved_locals (possibly tracking which projection was moved, so the remaining fields can still be dropped soundly), or
• make dropping_assumption skip subtrees whose ownership has been transferred away.

Environment

• thrust @ 1d85b18 ("Resolve named struct fields in formula translation (Resolve named struct fields in formula translation #118)")
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.13.4, default solver configuration