Refer to closure pre-/post-conditions in specifications

[coord-e]

Implements #71: allow #[thrust_macros::requires] / #[thrust_macros::ensures] specifications to refer to the precondition and postcondition of a closure parameter f. This enables specifying higher-order functions in terms of the contracts of the closures passed to them.

Surface syntax

thrust_macros::pre!(f(x))// f's precondition holds for argument x
thrust_macros::post!(f(x), r)// r is a possible result of f(x)

Arity is handled automatically (pre!(f()), pre!(f(x)), pre!(f(x, y))), so there is no tuple noise. Example — Option::map:

#[requires(opt == None || exists(|i| opt == Some(i) && pre!(f(i))))]#[ensures((opt == None && result == None) || exists(|i| exists(|j| opt == Some(i) && post!(f(i), j) && result == Some(j))))]

What's included

• std.rs: marker functions thrust_models::model::closure_precondition(&f, args) and closure_postcondition(&f, args, result) (tagged #[thrust::def::…]), plus Option::map and Option::unwrap_or_else extern specs written with pre!/post!.
• thrust-macros: function-like macros pre! / post! (pre_post.rs) that desugar to those marker functions, tupling the call arguments. Pure surface sugar; the analyzer is unchanged.
• analyze: recognize the markers in the formula-function translator (annot_fn); resolve the referenced closure's FunctionType from the analyzer's already-known defs (known_function_ty_with_args), and expand a marker by substituting the supplied argument terms into the closure's parameter/return refinements.
• rty: FunctionType::{precondition,postcondition}_formula helpers — a positional substitution of parameter values into the closure's refinements (the closure value itself is the leading RustCall environment parameter).

Tests

New pass/fail ui tests, all verifying non-vacuously:

• closure_postcondition (+ closure_postcondition_generic, exercised through a generic wrapper) — a higher-order apply using pre!/post!.
• option_map, option_unwrap_or_else — exercise the new std specs (use the PCSat solver, like the existing annot_exists/iterators tests).

cargo test passes (214 tests, with the PCSat/COAR solver available); cargo fmt --check and cargo clippy -- -D warnings are clean.

Two commits

1. Refer to closure pre-/post-conditions in specifications — the marker functions, analyzer/rty support, std specs and tests (using the markers directly).
2. Add pre!/post! sugar — the pre!/post! macros, with std/tests switched to them.

Scope and #83 compatibility

pre!/post! wrap a call expression, which is the shape #83 needs ("the pre/post of a call to some def"). This PR is deliberately scoped to closures only — the markers lower to a closure's FunctionType. When #83 generalizes this to other defs (e.g. #82's <&T as PartialEq>::eq), the user-facing pre!/post! syntax stays the same and only the lowering grows.

Notes

• Builds on Verify generic functions' bodies against requires/ensures contracts #105 (generic functions' bodies are verified against their contracts) and Panic verifying a generic function whose closure argument has a generic parameter type #108 (generic HOF with a generic-typed closure argument); both are in main.
• The std combinators are trusted extern_spec_fns, so their specs surface the closure's precondition in requires (e.g. requires(pre!(f(x)))) so callers discharge it — otherwise a postcondition referring to that closure would be vacuous.

Closes#71

https://claude.ai/code/session_01NyPQne5pFDqo9g3rnpAUSS

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit:f36aff1b0f

ℹ️ 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]

Support function items in pre/post markers

When a higher-order spec using pre!(f(...)) or post!(f(...), ...) is instantiated with a function item instead of a closure (for example opt.map(i32::abs) or apply(x, some_fn)), expr_ty(receiver) normalizes to TyKind::FnDef, not TyKind::Closure. This branch returns None, and the caller immediately panics as “precondition used on a non-closure parameter”, even though precompute_callable_param_contracts already caches FnDef contracts and the public macro/docs describe closure/function support. Please handle TyKind::FnDef here (and avoid adding a closure environment argument for Rust ABI functions) so these valid FnOnce call sites don't crash verification.

Useful? React with 👍 / 👎.

[coord-e]

this requires more work beyond annot_fn.rs to support non-RustCall ABI; will be implemented in follow-up PR

[Copilot]

Pull request overview

Adds first-class support for referring to a closure argument’s contract from within #[thrust_macros::requires] / #[thrust_macros::ensures], enabling higher-order function specifications (e.g., Option::map, Option::unwrap_or_else) to be stated in terms of the passed closure’s pre/post-conditions.

Changes:

• Introduces thrust_macros::pre! / thrust_macros::post! proc-macros, desugaring to thrust_models::model::{closure_precondition, closure_postcondition} marker functions.
• Extends formula translation to recognize and expand these markers by substituting call arguments/results into the referenced closure’s FunctionType refinements.
• Adds new std extern specs and UI tests covering the new closure pre/post reference mechanism (pass + fail cases).

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
thrust-macros/src/pre_post.rs	Implements pre!/post! macro parsing + desugaring to marker functions.
thrust-macros/src/lib.rs	Exposes pre!/post! as proc-macros from the thrust-macros crate.
std.rs	Adds marker functions and writes Option::{map,unwrap_or_else} specs using pre!/post!.
src/rty.rs	Adds helpers to turn a FunctionType’s parameter/return refinements into instantiated CHC formulas.
src/analyze/local_def.rs	Eagerly precomputes callable parameter contracts so formula translation can read cached contracts.
src/analyze/did_cache.rs	Caches DefIds for the new marker functions.
src/analyze/annot.rs	Defines paths for #[thrust::def::closure_precondition] / closure_postcondition.
src/analyze/annot_fn.rs	Recognizes marker calls and expands them into formulas based on the referenced closure’s contract.
src/analyze.rs	Adds read-only accessors needed by formula translation to query cached function types and tcx.
tests/ui/pass/closure_postcondition.rs	Pass UI test for a HOF spec using pre!/post!.
tests/ui/pass/closure_postcondition_generic.rs	Pass UI test covering generic HOFs using pre!/post!.
tests/ui/pass/option_map.rs	Pass UI test exercising new Option::map extern spec.
tests/ui/pass/option_unwrap_or_else.rs	Pass UI test exercising new Option::unwrap_or_else extern spec.
tests/ui/fail/closure_postcondition.rs	Fail UI test ensuring contracts are non-vacuous.
tests/ui/fail/option_map.rs	Fail UI test ensuring Option::map spec is enforced.
tests/ui/fail/option_unwrap_or_else.rs	Fail UI test ensuring Option::unwrap_or_else spec is enforced.

---

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