Bridge the rust-call receiver in pre!/post!

[coord-e]

Fixes #206.

Problem

A specification holds a closure as its signature says, while the closure body takes it as its rust-call receiver: a closure that mutates its upvars takes them behind a Mut, one that only reads them takes them behind a &, one that consumes them takes them as they are. pre!(f(..)) / post!(f(..), r) applied the closure's pre- and postcondition to the receiver as the specification names it, so the two could disagree:

• a closure value (f: F) against a body taking &mut {closure} — 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 body taking &{closure}.

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 takes the receiver term through the same three steps RustCallVisitor performs on the argument of a call:

• a closure value borrowed as &{closure};
• a closure value borrowed as &mut {closure};
• a &mut {closure} reborrowed as &{closure}.

A receiver the body already takes as it stands is left alone. In particular a receiver that carries a Mut for a body that takes one keeps it, and with it the upvars the call leaves behind — which is what Mut::new(f, g) is for.

The mutable borrow of a closure value ends the call holding the upvars it started with. That is as much as a specification naming the closure by value can say about them, and it keeps the system in the Horn fragment, which an existential or a universal over the prophecy would leave. A specification that needs the upvars a call leaves behind names the receiver with Mut::new(f, g), 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 other 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.

[coord-e]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: e3ec5b3dea

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".