[coord-e]

Fixes #121 and #122. Supersedes #124.

Dropping an aggregate after moving out a field can resolve that field's mutable-borrow prophecy twice. Contradictory resolutions can make false assertions verify. The drop must resolve only the parts still owned at that point on that execution path: a field moved in one branch remains owned in the other, and assigning a value back restores its drop obligation.

Implementation

• Track partial-move ownership after statements and on control-flow edges. Moving an owned place transfers its drop obligation; assigning to that place, a containing field, or the whole local restores ownership. Call destinations become initialized on the successful return edge. Reference moves retain the existing reborrow behavior.
• Specialize analysis MIR blocks when incoming ownership states differ, so each drop has a path-specific set of exclusions. Reuse existing block versions for loops and discard ownership history for locals no longer needed downstream. Projected assignments retain the state of untouched fields. Preserve loop-invariant associations across block specialization.
• Keep DropSet { drops, except }: drop targets are whole locals, and exclusions are moved-out MIR places. Include a parent local in the drop candidates after a direct field assignment. Whole-local move suppression remains keyed by the move's location.
• Use the existing MIR-place elaboration for exclusions, preserving real Box dereferences and inserting only the synthetic ownership dereferences. Match those paths against the refined type's drop traversal, including enum downcasts, to skip moved-out subtrees while resolving still-owned siblings.

Validation

• All 29 partial-move UI tests pass with thrust-fptprove-wrapper. They cover moves into locals and calls, siblings, conditional moves, field/parent/local reinitialization, enum payloads, loops with invariants, call-return initialization, sequential conditionals, and moves through Box values and boxed fields. Pass/fail pairs check both successful verification and rejection of false assertions.
• With thrust-fptprove-wrapper and a 180-second default solver limit, 409 UI tests pass; the two known timeout cases are excluded. The pass and fail variants of slice_split_first_mut_loop.rs previously timed out even with a 180-second limit. Their generated SMT constraints remain byte-for-byte identical before the ownership-tracking changes, after those changes, and after the Box fix. These two cases remain unverified; the entire 411-test suite is not reported as green.
• Unit tests (3), Cargo integration tests (2), and doc tests (2) pass. cargo fmt --all -- --check, cargo clippy -- -D warnings, and git diff --check pass.
• Three reviewers reviewed the entire branch diff and rechecked the fixes for loop-invariant handling, unnecessary block multiplication, enum exclusions, and Box dereferences. No additional findings remained in their final reviews.

Existing limitation

Writing through a field after reinitialization, for example let t = s.0; s.0 = t; *s.0.0 = 10;, can still panic with deref unbound var. This reproduces both before and after these changes and is separate from restoring the drop obligation.

[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.