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