Support FnParam for closure-typed function parameters in invariants

[coord-e]

Problem

Referring to a closure-typed function parameter through thrust_models::FnParam<F> in a loop invariant failed to compile:

error[E0308]: mismatched types
   |  fn_[0] == f.at_entry()
   |            ^^^^^^^^^^^^ expected `Closure<F>`, found associated type
   = note: expected struct `Closure<F>`
             found associated type `<F as Model>::Ty`

The invariant macro rewrites a closure type parameter F to Closure<F>, but only for a bare F — it never descended into the generic arguments of composite path types, so FnParam<F> was left untouched and f.at_entry() produced <F as Model>::Ty instead of Closure<F>.

Changes

• macro (formula_fn_type_lowering.rs): lower_closure_type_params_in_ty now recurses into a path type's generic arguments (and qualified self), so FnParam<F> becomes FnParam<Closure<F>> and f.at_entry() recovers the modeled closure.

• analyzer (annot_fn.rs): a capture-free closure models to a null (singleton) sort. Ordinary singleton parameters are already collapsed to their canonical value in build_env_from_params so they never appear as a variable in a formula, but FnParam<Inner> wrappers were excluded from that handling (the wrapper type does not build to a meaningful sort). A singleton closure passed via FnParam therefore kept a param-variable reference and later ICE'd during clause building. The wrapped parameter is now classified by its Inner sort, so a singleton closure collapses like any other singleton and no singleton value var reaches a refinement.

Tests

Adds a pass/fail pair loop_invariant_fn_param_closure:

• last_apply proves a postcondition from an invariant relating the accumulator to the entry closure's postcondition via post!(f.at_entry()) (capturing closure).
• unchanged covers the null-sort closure-identity case.

Known limitations (not addressed here)

• For an FnMut closure, post!(f.at_entry()(..)) hits a sort mismatch: the closure-contract predicate takes the environment as Mut<Tuple> while f.at_entry() yields a plain Tuple.
• The closure-history-array pattern (exists(|fn_: Array<Int, Closure<F>>| fn_[0] == f.at_entry())) type-checks and no longer ICEs, but the solver returns unknown on the existential over an array of closures.

🤖 Generated with Claude Code

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR fixes closure-typed function parameters referenced via thrust_models::FnParam<F> inside invariants by ensuring closure type parameters are correctly lowered when nested in generic path arguments, and by preventing singleton (null-sort) closures wrapped in FnParam from reaching clause building as variables.

Changes:

• Macro: recurse into syn::Type::Path generic arguments (and qself) so FnParam<F> becomes FnParam<Closure<F>> during invariant type lowering.
• Analyzer: classify FnParam<Inner> parameters by their Inner type for singleton detection/collapsing to avoid ICEs when the wrapped closure is singleton-sorted.
• Tests: add pass/fail UI coverage for both capturing-closure postcondition reasoning via f.at_entry() and capture-free (null-sort) closure identity comparisons.

Reviewed changes

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

File	Description
thrust-macros/src/formula_fn_type_lowering.rs	Extends closure type-param lowering to descend into path generic arguments / qualified self.
src/analyze/annot_fn.rs	Treats FnParam<Inner> parameters as Inner for singleton collapsing to prevent ICEs.
tests/ui/pass/loop_invariant_fn_param_closure.rs	New passing UI test exercising FnParam<F> with a capturing closure in an invariant.
tests/ui/fail/loop_invariant_fn_param_closure.rs	New failing UI test ensuring the scenario is checked under Unsat expectations and avoids ICE.

---

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1865775859

ℹ️ 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".