Allow user-specified closure pre/post via closure! macro by coord-e · Pull Request #189 · coord-e/thrust

coord-e · 2026-07-23T11:30:06Z

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

Copilot

Pull request overview

This PR introduces a new thrust_macros::closure! proc-macro to let users explicitly pin a closure’s requires / ensures conditions (optionally), instead of always inferring them as pvar templates, and adds UI tests validating the behavior.

Changes:

Add closure! proc-macro entry point in thrust-macros and implement its expansion logic.
Expand closure bodies to include #[thrust::formula_fn] companions plus #[thrust::requires_path] / #[thrust::ensures_path] markers when clauses are provided.
Add passing/failing UI test pairs for requires-only, ensures-only, and both clauses.

Reviewed changes

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

Show a summary per file

File	Description
thrust-macros/src/lib.rs	Exposes the new `closure!` proc macro from the macros crate.
thrust-macros/src/closure.rs	Implements parsing + expansion for closure pre/post specifications via injected formula fns and path markers.
tests/ui/pass/closure_requires_only.rs	Pass case: `requires` pinned, `ensures` inferred.
tests/ui/pass/closure_requires_ensures.rs	Pass case: both `requires` and `ensures` pinned.
tests/ui/pass/closure_ensures_only.rs	Pass case: `ensures` pinned, `requires` inferred.
tests/ui/fail/closure_requires_only.rs	Fail case: violates pinned `requires`.
tests/ui/fail/closure_requires_ensures.rs	Fail case: pinned `ensures` hides exact result.
tests/ui/fail/closure_ensures_only.rs	Fail case: pinned `ensures` hides exact result.

Suppressed comments (1)

thrust-macros/src/closure.rs:148

Same as above for the ensures marker: the injected _thrust_closure_ensures; is a path statement and can trigger the path_statements lint in user code. Add #[allow(path_statements)] to suppress the warning for this marker statement.

            _thrust_closure_ensures;
        });
    }

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

coord-e · 2026-08-06T12:15:23Z

+            #[thrust::requires_path]
+            _thrust_closure_requires;
+        });


The lint does not fire here, so I'm leaving this as is.

path_statements is suppressed for spans coming from a macro defined in another crate, and closure! lives in thrust-macros. Checked against a build of this branch:

closure! expansion, default lints: no path_statements diagnostic

same, with -W path-statements and with -D warnings: still nothing

same file with a crate-level #[deny(path_statements)]: still nothing

positive control — a hand-written marker; statement in that same file, same invocation: error: path statement with no effect

So the lint is active and reaching the file; it just doesn't apply to the injected statements.

The #[allow(path_statements)] in spec.rs sits on fn items that the macro re-emits, which is a different shape from these statements; I'd rather not copy an attribute over without a case that needs it.

Generated by Claude Code

Closure pre-/post-conditions were always inferred as predicate-variable templates. Add `thrust_macros::closure!(requires(..), ensures(..), |x: T| -> R { .. })` so a user can pin them explicitly, mirroring Prusti's `closure!`. The macro 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-fn specs. Each clause is optional; an omitted side stays inferred (a pvar). A closure's parameters are `[env, arg1, .., argN]` while a clause names only the arguments, so the companions declare a dummy leading parameter standing in for the environment. Their parameter positions then line up with the closure's, and the plugin needs no closure-specific handling. Adds UI test pairs for all three clause combinations. Each declares a spec that inference would not produce, so the failing side of every pair fails only because the spec is pinned: a precondition the call site violates, and a postcondition weaker than the body. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BTDWVnDzef1Kx97mHWUsTU

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: d02e7552cd

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

chatgpt-codex-connector · 2026-08-06T13:02:53Z

+    // a dummy parameter in the environment's place to keep the positions aligned.
+    let mut fn_params: Vec<FnArg> = vec![syn::parse_quote!(_thrust_closure_env: ())];
+    for param in &closure.inputs {
+        let syn::Pat::Type(pt) = param else {


Reject unsupported closure parameter patterns

When a specified closure uses a valid typed pattern that FormulaFn cannot translate, such as closure!(requires(true), |_: i32| 1) or a tuple containing _, this check accepts it and copies the pattern into the generated formula function. analyze::annot_fn::build_env_from_pat only handles bindings and tuple patterns, so verification panics with unsupported pattern in formula rather than reporting a diagnostic. Validate the inner pattern recursively or lower unsupported patterns to analyzer-compatible bindings.

Useful? React with 👍 / 👎.

i think it is an obligation of analyze::annot_fn::build_env_from_pat and macros should not care

chatgpt-codex-connector · 2026-08-06T13:02:53Z

+    // A closure's parameters are `[env, arg1, .., argN]`, the environment being the
+    // closure value itself. A clause names only the arguments, so the companions take
+    // a dummy parameter in the environment's place to keep the positions aligned.
+    let mut fn_params: Vec<FnArg> = vec![syn::parse_quote!(_thrust_closure_env: ())];


Make generated closure identifiers collision-proof

The synthetic environment binding uses a call-site-visible fixed name, so a valid closure parameter named _thrust_closure_env produces a generated helper with that identifier bound twice and fails with E0415. The fixed helper item names have the same hygiene problem when the original body declares _thrust_closure_requires or _thrust_closure_ensures; generate collision-proof identifiers instead of reserving undocumented user names.

Useful? React with 👍 / 👎.

coord-e force-pushed the claude/closure-pre-post-flexibility-67si3w branch 2 times, most recently from e5a6b1e to 7a5f9b6 Compare August 6, 2026 11:55

coord-e requested a lite review from Copilot August 6, 2026 11:57

Copilot started reviewing on behalf of coord-e August 6, 2026 11:57 View session

coord-e force-pushed the claude/closure-pre-post-flexibility-67si3w branch from 7a5f9b6 to eae27ff Compare August 6, 2026 11:59

Copilot AI reviewed Aug 6, 2026

View reviewed changes

coord-e force-pushed the claude/closure-pre-post-flexibility-67si3w branch from eae27ff to 852e7f9 Compare August 6, 2026 12:15

coord-e force-pushed the claude/closure-pre-post-flexibility-67si3w branch from 852e7f9 to d02e755 Compare August 6, 2026 12:47

coord-e marked this pull request as ready for review August 6, 2026 12:52

chatgpt-codex-connector Bot reviewed Aug 6, 2026

View reviewed changes

coord-e merged commit a148b9d into main Aug 6, 2026
9 checks passed

coord-e deleted the claude/closure-pre-post-flexibility-67si3w branch August 6, 2026 14:02

Navigation Menu

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

Allow user-specified closure pre/post via closure! macro#189
coord-e merged 1 commit into
mainfrom
claude/closure-pre-post-flexibility-67si3w

coord-e commented Jul 23, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

coord-e Aug 6, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Aug 6, 2026

Uh oh!

coord-e Aug 6, 2026

Uh oh!

chatgpt-codex-connector Bot Aug 6, 2026

Uh oh!

coord-e Aug 6, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

coord-e commented Jul 23, 2026

Summary

How it works

Tests

Out of scope (follow-ups)

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

coord-e Aug 6, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Aug 6, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Aug 6, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Aug 6, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Aug 6, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants