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: HashSet<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 place 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 place, 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: 298 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