No method of a trait `impl` can be specified: `requires`/`ensures`/`param`/`ret`/`sig` emit their `formula_fn` companions as items of the `impl`, so every trait-impl method dies with `E0407` — and the only alternative (spec on the trait) forces one spec on all impls

[coord-e]

Summary

Every surface annotation (#[thrust_macros::requires], ensures, param, ret, sig) expands to #[thrust::formula_fn] companion functions (plus, for requires/ensures, a _thrust_extern_spec_* wrapper) that are emitted in the annotated function's own item position, and to path statements that reference those companions by a prefix chosen from a heuristic rather than from where the item actually landed.

Inside an impl block that means the companions become associated items of that impl:

• in a trait impl (impl Op for Inc) Rust rejects them outright — E0407: method _thrust_requires_apply is not a member of trait Op. There is no workaround: #[thrust_macros::context] does not change where the items are emitted, and this affects requires, ensures, param, ret and sig alike.
• in an inherent impl the companions are legal, but the reference to them is unqualified in several cases, giving E0425: cannot find value _thrust_requires_<name> in this scope. For #[param]/#[ret]/#[sig] on an associated function without a receiver this too has no workaround.

The practical consequence is that a trait implementation cannot be given a specification. That is a core-logic limitation, not just a diagnostics problem: the only route left is to put the spec on the trait declaration, which then applies to every implementation of that trait (last repro below), so two impls with different behaviour cannot both be specified.

This is the same family as #252 (macro-emitted paths that do not resolve in the item's real scope), but a distinct root cause — item placement and the Self:: prefix inside impl blocks, rather than the thrust_models::… prefix.

Reproduction

All commands are cargo run -- -Adead_code -C debug-assertions=false <file>.

1. requires/ensures on a trait-impl method — E0407, no workaround

trait Op {
    fn apply(&self, x: i64) -> i64;
}

struct Inc;
impl thrust_models::Model for Inc { type Ty = Self; }

impl Op for Inc {
    #[thrust_macros::requires(true)]
    #[thrust_macros::ensures(result == x + 1)]
    fn apply(&self, x: i64) -> i64 { x + 1 }
}

fn main() {
    let a = Inc;
    assert!(a.apply(3) == 4);
}

error[E0407]: method `_thrust_requires_apply` is not a member of trait `Op`
  --> repro1.rs:10:5
   |
10 |     #[thrust_macros::ensures(result == x + 1)]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not a member of trait `Op`
   |
   = note: this error originates in the attribute macro `::thrust_macros::_requires_ensures`

error[E0407]: method `_thrust_ensures_apply` is not a member of trait `Op`
error[E0407]: method `_thrust_extern_spec_apply` is not a member of trait `Op`
error[E0425]: cannot find value `_thrust_requires_apply` in this scope

Adding #[thrust_macros::context] to the impl block does not help — the errors are identical. The same E0407 appears for #[thrust_macros::ret({ r: i64 | r > 0 })] (_thrust_refine_apply_ret), #[thrust_macros::param(x: { v: i64 | v > 0 })] (_thrust_refine_apply_p1) and #[thrust_macros::sig(..)] (_thrust_refine_make_p0, _thrust_refine_make_ret).

2. requires/ensures on an inherent-impl method without #[context] — E0425

struct Acc { n: i64 }
impl thrust_models::Model for Acc { type Ty = Self; }

impl Acc {
    #[thrust_macros::requires(true)]
    #[thrust_macros::ensures((!self).n == (*self).n + v)]
    fn add(&mut self, v: i64) { self.n += v; }
}

fn main() {
    let mut a = Acc { n: 0 };
    a.add(5);
    assert!(a.n == 5);
}

error[E0425]: cannot find value `_thrust_requires_add` in this scope
error[E0425]: cannot find value `_thrust_ensures_add` in this scope

Adding #[thrust_macros::context] to the impl makes this verify. Since context is documented as being about recovering generics and Self, needing it on a non-generic inherent impl just to make the expansion resolve is surprising, and the identifier named in the error is an internal one the user never wrote.

3. #[ret] on an associated function without a receiver — E0425, #[context] does not help

struct S { n: i64 }
impl thrust_models::Model for S { type Ty = Self; }

#[thrust_macros::context]
impl S {
    #[thrust_macros::ret({ r: i64 | r > 0 })]
    fn make() -> i64 { 1 }
}

fn main() { assert!(S::make() > 0); }

error[E0425]: cannot find value `_thrust_refine_make_ret` in this scope

Removing #[thrust_macros::context] gives the same error. The same annotation on a method that does take &self works.

4. Why "put the spec on the trait" is not a workaround

#[thrust_macros::context]
trait Op {
    #[thrust_macros::requires(true)]
    #[thrust_macros::ensures(result == x + 1)]
    fn apply(&self, x: i64) -> i64;
}

struct Inc;
struct Dbl;
impl thrust_models::Model for Inc { type Ty = Self; }
impl thrust_models::Model for Dbl { type Ty = Self; }

impl Op for Inc { fn apply(&self, x: i64) -> i64 { x + 1 } }
impl Op for Dbl { fn apply(&self, x: i64) -> i64 { x * 2 } }

fn main() {
    let a = Inc;
    let b = Dbl;
    assert!(a.apply(3) == 4);
    assert!(b.apply(3) == 6);
}

error: verification error: Unsat

Dbl::apply cannot satisfy the trait-level ensures, so the whole crate is rejected. With the spec on the trait declaration there is exactly one spec slot for all implementations; the per-impl spec that would fix this is what repro 1 shows is unwritable.

Current behaviour, by position

annotated item	requires/ensures	param/ret/sig
free function	ok	ok
trait declaration method	ok (#[context] on the trait)	ok
inherent impl, method with a receiver	E0425 without #[context], ok with it	ok
inherent impl, associated fn, no receiver	E0425 without #[context], ok with it	E0425, #[context] does not help
trait impl, any method	E0407, no workaround	E0407, no workaround

Root cause

Both defects come from the expansion emitting the companions next to the annotated fn and then guessing the path prefix.

Placement. spec.rs's ExpandedTokens::expand (thrust-macros/src/spec.rs:407) emits

quote! {
    #func
    #requires_fn
    #ensures_fn
    #[thrust::extern_spec_fn]
    fn #extern_spec_name … { … }
}

and rty.rs's expand_with_annotations (thrust-macros/src/rty.rs:200) emits #(#formula_fns)* #func. When the input is a FnItemWithSignature::ImplItemFn, all of those land inside the enclosing impl. That is legal for an inherent impl and illegal for a trait impl, which is exactly the E0407.

Prefix. ExpandedTokens::path_prefix (thrust-macros/src/spec.rs:377) emits Self:: only when an outer context was attached:

fn path_prefix(&self) -> Option<TokenStream2> {
    self.outer_context.as_ref()?;
    Some(quote!(Self::))
}

so without #[thrust_macros::context] the #[thrust::requires_path] statement — and the #path_prefix #name #turbofish(#call_args) call in the extern-spec wrapper — are unqualified even though the companion is an associated item. The condition that matters is whether the annotated fn is an impl item, not whether a context attribute was written.

rty.rs's build_refinement_path_stmt (thrust-macros/src/rty.rs:467) uses a different, equally partial heuristic:

let path_prefix = if func.sig().receiver().is_some() {
    quote!(Self::)
} else {
    quote!()
};

which is why repro 3 fails for an associated function with no receiver and cannot be fixed by #[context].

Suggested direction

Emit the companion formula_fns (and the _thrust_extern_spec_* wrapper) outside the enclosing impl — e.g. as free items, or into a separate inherent impl for the self type — and derive the path prefix in both spec.rs and rty.rs from the actual emission site rather than from outer_context presence or receiver presence. Emitting them outside the impl also removes the E0407 for trait impls, which is the case with no workaround today.

Environment

• thrust @ 2bf022d (clean tree)
• rustc 1.91.0-nightly (12eb345e5 2025-09-07) (nightly-2025-09-08, per rust-toolchain.toml)
• Z3 5.0.0 (x64-glibc-2.39, the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS