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

[coord-e]

Fixes #121 and #122. Supersedes #124.

Bug

A local with a partial field move (e.g. move (_2.0)) was still dropped wholesale, so the drop walked into the moved-out sub-place and resolved the &mut prophecy it owns a second time. The two resolutions contradict (final = 1 ∧ final = 2), making the clause body unsatisfiable, after which any assertion — including false ones — "verifies".

Approach

All drop information lives in DropPoints; a dying local is dropped whole while its moved-out sub-places are skipped.

• drop_point.rs — Moves::collect gathers all non-reference moved operands in one body traversal: whole-local moves (keyed by location, where the local also dies) and, keyed by the parent local, the partial field moves. DropSet { drops, except } carries, per drop point, the whole locals to drop plus the moved-out sub-places to skip. Drop targets stay whole locals (drops: BTreeSet<Local>) — the closure environment restored by RustCallVisitor reaches its drop through a projection-less temporary.
• env.rs — dropping_formula_for_term threads the drop-walk path and except alongside the type/term walk (introduced in Fix enum-drop of aggregate mutable-reference fields #167) and returns early on any subtree matching an excepted path, so the drop resolves the still-owned siblings and skips the moved-out subtrees (which are resolved at the move destination). The fix is both sound and complete. The moved-out places are elaborated to the walk's form via Env::elaborated_path, which inserts the own-box Derefs the type elaboration introduces (mut/reborrowed locals, and every tuple field), so the comparison lines up exactly — without this a partially-moved local that gets box-elaborated (e.g. when a sibling is mutated through) would not be skipped, and the false assertion would verify vacuously. With Path::PlaceTy gone (Fix enum-drop of aggregate mutable-reference fields #167), Path now derives Eq, so the match is a plain ==.

Testing

New pass/fail regression tests:

• 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).
• partial_move_sibling.rs — a partially-moved local with a still-owned sibling: the sibling's prophecy must be resolved by the parent's drop (completeness), and — when the moved-out part is used and the sibling is reborrowed — the moved-out sub-place must not be resolved twice (soundness).

Each false-assertion variant reports Unsat (rejected); the true companions verify. Full UI suite on the rebased branch: 308 passed, 0 failed (pcsat via Docker, z3 4.15.4), plus doc-tests. cargo fmt --all -- --check, cargo clippy -- -D warnings, and git diff --check are clean.

Note on #154

#154 proposed migrating drop points to MIR Place to support projected drops. That turned out to be unnecessary: drop targets are always whole locals (the closure-environment case reaches its drop through a projection-less temporary), so this PR keeps Local drops and only tracks the moved-out sub-places as except.

🤖 Generated with Claude Code

[Copilot]

Pull request overview

Fixes prophecy double-resolution when partially moved locals are dropped.

Changes:

• Tracks moved sub-places as drop exceptions.
• Skips excepted paths during drop-formula generation.
• Adds pass/fail regression coverage for local, call, and sibling cases.

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/analyze/basic_block/drop_point.rs	Collects moves and builds exception-aware drop sets.
src/analyze/basic_block.rs	Applies drop sets during block analysis.
src/analyze/local_def.rs	Propagates lifetime-aware drop-point types.
src/refine/env.rs	Skips moved paths while generating drop formulas.
tests/ui/pass/partial_move_drop.rs	Tests a valid local partial move.
tests/ui/fail/partial_move_drop.rs	Rejects the unsound local variant.
tests/ui/pass/partial_move_field_call.rs	Tests a valid field move into a call.
tests/ui/fail/partial_move_field_call.rs	Rejects the unsound call variant.
tests/ui/pass/partial_move_sibling.rs	Tests correct sibling prophecy resolution.
tests/ui/fail/partial_move_sibling.rs	Guards against double-resolution with a sibling.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.