Don't drop partially-moved sub-places (fix #121, #122)

[coord-e]

Summary

Fixes #121 and #122, which share a single root cause.

moved_locals (src/analyze/basic_block/drop_point.rs) only excluded whole-local moves from the implicit-drop set. A local with a partial field move (e.g. move (_2.0)) was therefore still dropped wholesale once it became dead. Env::dropping_assumption (src/refine/env.rs) then walked the local's full type — including the part that was moved away — and resolved the &mut prophecy owned by the moved-out sub-place a second time, with a different current value. The two resolutions contradict (final = 1 ∧ final = 2), making the clause body unsatisfiable, after which any assertion — including false ones — "verifies."

Fix

• drop_point.rs: add partial_moved_places, which collects every partial field-move (move place with a non-empty projection) per local. Reference-typed moves are skipped for the same reason moved_locals skips them: ReborrowVisitor/RustCallVisitor turn them into reborrows, so the source still owns its prophecy and must be dropped normally.
• basic_block.rs: store that map on the analyzer (recomputed whenever body changes) and pass the relevant moved sub-places to the env when dropping a local.
• env.rs: dropping_assumption now takes the moved sub-places and short-circuits any subtree whose path matches a moved-out place (new Path::same_place structural comparison). drop_local_with_moved is the new entry point; drop_local delegates with an empty slice.

Tests

New pass/fail regression tests for both shapes:

• partial_move_drop.rs — Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121's partial-move-into-local (let b = s.0;).
• partial_move_field_call.rs — Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122's partial-move-into-call (owned (&mut i64,) field passed to a function).

Each false-assertion variant now reports Unsat (rejected) where it was previously accepted; the true-assertion companions still verify, confirming the drop is not over-suppressed.

Full UI suite passes with no regressions (pcsat solver via Docker).

Note on #122's literal reproduction

The exact Wrap { r: &'a mut i32 } example in #122 — where the moved field is itself &mut-typed — does not reach this drop on the current toolchain. In optimized MIR that field becomes a reborrow (deref_copy/copy), not an owned move, and analyzing apply panics earlier in an unrelated, pre-existing spot (reborrowing a &mut field out of a struct parameter). That panic is filed separately. This PR fixes the shared drop double-resolution; partial_move_field_call.rs exercises #122's intended shape using an owned aggregate field.

https://claude.ai/code/session_01Fovh1a8R5EtDd98ic9EJfR

---

Generated by Claude Code

[coord-e]

Possible uncovered sibling of this bug, found while adding the split_first_mut spec in #151.

Minimal call-site shape (with #151's extern spec relating the returned references to the receiver's current/final slice models):

let slice = two_element_mut_slice(); // modeled as [10, 20]
{
    let (first, _tail) = slice.split_first_mut().unwrap();
    *first = 11;
}
assert!(*slice.first().unwrap() == 12); // currently accepted

The relevant analyzer trace is:

_4 = Option::<(&mut i32, &mut [i32])>::unwrap(...)
_2 = move <synthetic reborrow of *(_4.0)>
_3 = move <synthetic reborrow of *(_4.1)>
implicitly dropped after statement local=_3
implicitly dropped after statement local=_4
(*_2) = 11

So the source tuple is dropped immediately after extracting its two &mut fields, while the synthetic reborrow in _2 is still live. The later mutation makes the path inconsistent/otherwise loses the required prophecy link, and the false assertion verifies vacuously.

This looks closely related to #121/#122, but PR #124 currently skips ref-typed partial moves because ReborrowVisitor turns them into reborrows. This case is exactly that excluded shape: the projected fields are themselves &mut, and the parent aggregate is dropped before the derived reborrows end.

I also checked simpler sized (&mut i64, &mut i64) tuple cases; they are rejected correctly, so the observed reproduction currently appears specific to the Option<(&mut T, &mut [T])>/unsized-tail path rather than all tuple destructuring.

[coord-e]

Superseded by #155. The same #121/#122 root cause is fixed there, but via the Place-based DropPoints from #154: instead of patching the env drop-walk (drop_local_with_moved / Path::same_place), #155 produces correct drop points by splitting a partially-moved local into its maximal still-owned sub-places, carving out the moved-out subtree. Your two regression tests (partial_move_drop, partial_move_field_call) are carried over and pass. Closing in favor of #155.

---

Generated by Claude Code