Verify generic functions' bodies against requires/ensures contracts

[coord-e]

Fixes#103.

Problem

Generic functions carrying #[thrust_macros::requires]/#[thrust_macros::ensures] had their bodies skipped during verification — the declared contract was trusted rather than checked against the implementation. Non-generic functions were verified correctly, so a wrong contract on a generic function was silently accepted. This was unsound, and it also made higher-order functions' contracts (generic over the closure type) trusted summaries.

Root cause

The requires/ensures macro routes the contract through an #[thrust::extern_spec_fn] wrapper whose tail-call target is the annotated function. For a generic function, this wrapper was registered as a deferred def with NoAnalyze, so the target's body was never run through the analyzer (def_ty_with_args gates body analysis on mode.should_analyze()).

Two roles were also conflated in the deferred def: the spec source (the wrapper, which carries the contract via expected_ty) and the body to verify (the wrapper's target). They are different defs for an extern-spec wrapper.

Non-generic functions were unaffected because they go through register_def (Concrete) + analyze_local_defs, which runs the body against the contract.

Fix

The change is behavioral, not a data-model change — DeferredDefTy { local_def_id, cache, mode } is unchanged, where local_def_id is the spec source and mode is Analyze/NoAnalyze:

• def_ty_with_args: when mode is Analyze, verify the body of the keyed def (def_id — i.e. the extern-spec target, or the function itself for a plain generic fn) against the spec, instead of running local_def_id (the spec source / wrapper). The analysis runs per-instantiation using the call site's concrete generic args, which sidesteps the constrained-type-parameter limitation of placeholder_generic_args.
• refine_fn_def: register_deferred_def now takes the target key explicitly, and a generic extern-spec wrapper whose target is local, has MIR, and isn't in skip_analysis is registered Analyze (was unconditionally NoAnalyze). Targets that must stay trusted keep NoAnalyze: non-local extern fns (e.g. std::mem::take), bodyless trait method declarations (no MIR), and trusted/ignored targets (#[thrust::trusted], whose macro expansion marks the original #[thrust::ignored]).

Known limitation: an uncalled generic function is never instantiated, so its body is never analyzed — a wrong contract on an uncalled generic function still wouldn't be caught, consistent with the per-instantiation approach. (A TODO notes that the criteria for which extern-spec'd target is analyzed could be made clearer.)

Tests

• tests/ui/pass/fn_poly_annot_2.rs — a generic id<T>(x, _t) -> i32 whose body (x * 1) satisfies ensures(result == x); verifies.
• tests/ui/fail/fn_poly_annot_2.rs — the same shape with a wrong body (x + 1) and a caller that asserts nothing about the result. Before the fix the body was never checked so this was silently accepted; now it's Unsat.

Verification

• Full UI suite: 205 passed, 0 failed (z3 4.13.0 + dockerd + pinned COAR image for the pcsat-based tests).
• A clean-baseline comparison confirmed the previously-trusted method/trait cases (annot_struct_impl, annot_preds_trait*, adt_poly_fn_poly) still pass once their bodies are actually verified.
• cargo fmt --check and cargo clippy -- -D warnings are clean.

https://claude.ai/code/session_01VTACey3vnA23ug9Pm5hMSF

[Copilot]

Pull request overview

Fixes an unsoundness in Thrust’s verifier where generic functions annotated with #[thrust_macros::requires] / #[thrust_macros::ensures] were not having their bodies checked, causing their contracts to be treated as trusted summaries (including for higher-order/generic-over-closure functions). The change updates deferred-definition registration and instantiation-time typing so that, when appropriate, the target function body is analyzed against the spec source’s expected type.

Changes:

• Update deferred-def registration for generic functions so extern-spec wrapper targets are eligible for Analyze when local MIR is available and not skipped.
• Change def_ty_with_args so Analyze mode verifies the keyed def’s body (the actual target) against the spec-providing wrapper’s expected_ty.
• Add UI tests covering generic requires/ensures where the body does and does not satisfy the contract.

Reviewed changes

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

File	Description
tests/ui/pass/fn_poly_annot_2.rs	New passing UI test ensuring a generic function body is checked against its contract.
tests/ui/fail/fn_poly_annot_2.rs	New failing UI test proving a wrong generic body now triggers Unsat.
src/analyze/crate_.rs	Registers deferred defs for generic extern-spec targets with Analyze when the target is local/analyzable.
src/analyze.rs	Ensures deferred instantiations in Analyze mode run body analysis on the keyed def rather than the spec wrapper.

---

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