Weaken closure parameter for FnMut closures called via FnOnce

[coord-e]

Fixes #46 (the remaining reopened case: calling an FnMut closure via FnOnce::call_once).

Problem

Calling an FnMut closure through FnOnce::call_once resolves to the closure function taking &mut {closure}, while the caller's MIR passes the closure environment by value. This hit the unimplemented!() "case 3" in RustCallVisitor.

The draft patch in the issue comment fixed the panic but lost completeness: after rewriting the call to pass &mut {closure}, the environment local stays live in the caller, yet the drop-point analysis (computed on the original MIR, where the local was moved into the call) never schedules a drop for it. The prophecies of its captured mutable borrows were therefore never resolved (final = current), leaving the captures' final values unconstrained.

Fix

• RustCallVisitor case 3: insert a mutable borrow of the closure environment and pass it as the argument. Since FnOnce::call_once consumes the closure, schedule both the borrow and the environment local to be dropped right after the call, which resolves the prophecies of the captured mutable borrows and restores completeness.
• DropPoints: the scheduled drops are stored next to the liveness-derived sets, behind DropPoints::insert_after_terminator and an Analyzer::drop_after_terminator helper. They are kept as a Vec because the locals are created during elaboration and lie outside the bitset domains sized to the original body's locals.
• reassign_local_mutabilities: mark the closure argument of a FnOnce::call_once call as mutable when the closure's kind is FnMut (implementing the TODO from the issue comment by checking the closure kind instead of the resolved signature), so the environment is boxed in the refinement environment and can be mutably borrowed.

Tests

• New tests/ui/{pass,fail}/closure_param_weaken_3.rs with the example from the issue: assert!(result == 3 && x == 2) is now proven (the issue's draft patch could not), and the incorrect variant (x == 1) is rejected with Unsat.
• Full cargo test passes locally (230/230 UI tests, including the pcsat/COAR-based ones), as do cargo fmt --check and cargo clippy.

https://claude.ai/code/session_012451PZJH2QqdqE5Zyxna5y

[Copilot]

Pull request overview

This PR addresses an incompleteness/panic when an FnMut closure is invoked through FnOnce::call_once, by rewriting the call to introduce an implicit mutable borrow of the closure environment and ensuring the corresponding drop obligations are recorded even though the locals are created during elaboration (outside the original MIR liveness domains).

Changes:

• Add a RustCallVisitor “case 3” transform to handle {closure} -> &mut {closure} for FnOnce::call_once, and schedule implicit drops after the call.
• Extend DropPoints with an “extra after-terminator drops” list to support elaboration-created locals.
• Update local mutability inference so FnOnce::call_once receiving an FnMut closure treats the closure argument as mutable, enabling boxing/borrowing as needed.
• Add new UI pass/fail tests covering the reopened scenario from issue #46.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/ui/pass/closure_param_weaken_3.rs	Adds a passing UI test exercising FnMut closure called via FnOnce::call_once.
tests/ui/fail/closure_param_weaken_3.rs	Adds a failing UI test variant expected to be Unsat.
src/analyze/local_def.rs	Marks closure arguments as mutable for FnOnce::call_once when the closure kind is FnMut.
src/analyze/basic_block/visitor/rust_call.rs	Implements the previously unimplemented!() rust-call “case 3” rewrite and schedules drops after the call.
src/analyze/basic_block/drop_point.rs	Adds support for “extra” after-terminator drops (for locals introduced during elaboration).
src/analyze/basic_block.rs	Wires the new after-terminator drop list into terminator typing and adds an analyzer helper to schedule those drops.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.