Allow user-specified closure pre/post via closure! macro

[coord-e]

Summary

Closure pre-/post-conditions were always inferred as predicate-variable (pvar) templates. This adds a way to pin them explicitly:

let f = thrust_macros::closure!(
    requires(x > 0),
    ensures(result == x + 1),
    |x: i32| -> i32 { x + 1 },
);

Each clause is optional — omit one and that side stays inferred (a pvar). The surface mirrors Prusti's closure!, which shares thrust's constraint of per-item proc-macros on stable Rust (Verus-style in-signature clauses need a whole-program macro; Creusot-style attributes-on-closures need whole-body rewriting — neither fits).

How it works

Maximal reuse of the existing named-fn spec machinery:

• thrust-macros/src/closure.rs (new) — rewrites the closure body to carry #[thrust::formula_fn] companions plus #[thrust::requires_path] / #[thrust::ensures_path] path statements, the same markers the plugin already reads for named functions. Reuses FormulaFnTypeLowering and formula::expand. The closure header supplies parameter/return types, so nothing is restated.
• src/analyze/local_def.rs — expected_ty shifts a closure formula's argument indices by one to account for the environment parameter that leads a closure's FunctionType params ([env, arg1, .., argN]). This is the core plugin change; the existing installation path (param_refinement / ret_refinement) then swaps in the user formula in place of the inferred pvar.
• src/analyze/crate_.rs — refine_local_defs registers every formula fn in a pre-pass so a closure's spec companions (nested inside the closure body) resolve regardless of the order mir_keys yields them.

No change needed to FunctionType (pre/post are already the params'/return refinements) or to pre!/post! (callers still reference the now-fixed spec the same way). The injected path statements analyze cleanly without special skipping.

Tests

Adds passing/failing UI test pairs following the repo convention (//@check-pass vs //@error-in-other-file: Unsat):

• closure_requires_ensures — a closure with both clauses, plus a caller relying on the fixed spec.
• closure_ensures_only — only ensures given; requires stays inferred.

Verified end-to-end with z3 as the CHC solver. The full UI suite shows zero regressions — the failing set is identical to the base tree's pre-existing solver-limitation failures.

Out of scope (follow-ups)

• Generic / Self context threading (the invariant_context machinery): closures in generic contexts referring to generic-/Self-typed values aren't supported yet, matching invariant!'s initial capability.
• Environment exposure: naming captured state (e.g. FnMut before/after) in a closure spec — the env param plumbing exists, but the macro surface for it is left as a follow-up.

🤖 Generated with Claude Code

---

Generated by Claude Code