Match the receiver of pre!/post! to the closure's function type

[coord-e]

Fixes #206.

Problem

A closure's pre- and postcondition are over its upvars as its body receives them: a closure that mutates its upvars takes them behind a Mut, one that only reads them takes the upvars themselves. pre!(f(..)) / post!(f(..), r) applied them to whatever shape the specification names the closure by, so the two could disagree:

• a closure value (f: F) against a Mut<upvars> parameter — the mutating-capture case in Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with pre!/post!, has its pre/postcondition predicate declared at the FnMut receiver sort Mut<env> but applied at the bare env sort, so verification aborts with a solver sort mismatch #206;
• a &mut to a closure (f: &mut F) against a parameter that is the upvars themselves.

Either way the predicate variable was emitted at a sort other than its declaration, and the solver aborted before producing a verdict:

unknown constant p2 (A1_Tuple<Mut<Int>>)
declared: (declare-fun p2 (A2_Mut<Tuple<Mut<Int>>>) Bool)

Change

closure_receiver_term adapts the receiver term to the first parameter of the closure's rty::FunctionType: a closure value stands for upvars that the call leaves as they are (mut(t, t)), and a &mut to a closure contributes the upvars it holds on entry (mut_current(t)). Receivers that already match — including one built with Mut::new — pass through untouched.

Pinning the upvars on exit to the ones on entry keeps the system in the Horn fragment, which an existential or a universal over the prophecy would leave. It is the weaker reading, assumed by the callee and proven by the caller through the same term, so the only cost is that a bare pre!/post! cannot carry upvars whose value changes across calls. Naming the receiver with Mut::new(f, g) expresses that, for a closure held by value as much as for one held behind a &mut; the added test pins this down.

Tests

• closure_mut_capture_pre_post: the reproduction from Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with pre!/post!, has its pre/postcondition predicate declared at the FnMut receiver sort Mut<env> but applied at the bare env sort, so verification aborts with a solver sort mismatch #206, a FnMut closure mutating a capture through a by-value HOF.
• closure_ref_mut_pre_post: the opposite mismatch, a Fn closure named through &mut F.
• closure_receiver_mut_model_byval: two calls to a move closure whose upvars hold the counter, with the upvars between the calls named by Mut::new.

cargo test is green at 314 UI tests (308 before), as are cargo fmt --check and cargo clippy -D warnings.

The comment on closure_captures_fn_once explaining that pre!/post! strip a FnMut closure's upvars of their Mut no longer describes the behaviour, so it is updated to the reason that still holds.

🤖 Generated with Claude Code

https://claude.ai/code/session_0192XpBfrsKiGya1e3t3Cj84

[Copilot]

Pull request overview

This PR fixes an SMT sort-mismatch in pre!/post! for closures by adapting the “receiver term” passed to a closure’s contract so it matches the contract’s environment parameter (e.g., by-value vs &mut-named closures, and Fn vs FnMut capture shapes). This prevents malformed CHC/SMT output that previously caused the solver to abort before returning a verification verdict.

Changes:

• Add closure_receiver_term in AnnotFnTranslator and use it for closure pre/postcondition translation to reconcile receiver shape with the closure contract environment parameter.
• Add UI pass/fail test pairs covering the reported mismatch cases and the Mut::new “environment between calls” modeling case.
• Update an existing UI test comment to reflect the new closure capture/contract behavior.

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/analyze/annot_fn.rs	Introduces receiver-term adaptation logic and wires it into closure pre/postcondition translation.
tests/ui/pass/closure_mut_capture_pre_post.rs	Pass test reproducing the mutating-capture by-value HOF pre!/post! case from #206.
tests/ui/fail/closure_mut_capture_pre_post.rs	Fail counterpart asserting an incorrect postcondition for the same scenario.
tests/ui/pass/closure_ref_mut_pre_post.rs	Pass test for the opposite mismatch: Fn closure referenced via &mut in pre!/post!.
tests/ui/fail/closure_ref_mut_pre_post.rs	Fail counterpart with an incorrect assertion.
tests/ui/pass/closure_receiver_mut_model_byval.rs	Pass test pinning the intended modeling that Mut::new can carry environment across calls for by-value closures.
tests/ui/fail/closure_receiver_mut_model_byval.rs	Fail counterpart with an incorrect assertion.
tests/ui/pass/closure_captures_fn_once.rs	Updates a comment describing why the closure is kept FnOnce and what changes when it becomes FnMut.
tmp.LCvQPp73Qu.smt2	Appears to be an unintended, locally generated solver artifact added to the repo.

---

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

[coord-e]

Right, that file was never meant to be here — removed.

It comes from tests/thrust-pcsat-wrapper, which mktemp -p . a copy of the query and deletes it through a trap on exit. A solver run that gets killed on timeout never runs the trap, so the copy was left behind in the working tree and I swept it up. No fixture is needed; the tests generate their own queries.

---

Generated by Claude Code

[Copilot]

Pull request overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated no new comments.