Enable to write thrust_macros::{ensures,requires} inside impl

[coord-e]

This example:

#[thrust_macros::context]
impl<T> VecWrap<T> {
  #[thrust::trusted]
  #[thrust_macros::requires(index < (*self).1)]
  #[thrust_macros::ensures(*result == (*self).0[index])]
  fn get(&self, index: usize) -> &T {
      &self.inner[index]
  }
}

expands like the following:

impl<T> VecWrap<T> {
    #[thrust::ignored]
    #[thrust::_impl_context(impl < T > VecWrap < T > {})]
    fn len(&self) -> usize { self.inner.len() }
    #[allow(unused_variables)]
    #[allow(non_snake_case)]
    #[thrust::formula_fn]
    fn _thrust_requires_len(self_: <&Self as thrust_models::Model>::Ty)
        -> bool where T: thrust_models::Model,
        <T as thrust_models::Model>::Ty: PartialEq {
        true
    }
    #[allow(unused_variables)]
    #[allow(non_snake_case)]
    #[thrust::formula_fn]
    fn _thrust_ensures_len(result: <usize as thrust_models::Model>::Ty,
        self_: <&Self as thrust_models::Model>::Ty) -> bool where
        T: thrust_models::Model, <T as thrust_models::Model>::Ty: PartialEq {
        (true) && (result == (*self_).1)
    }
    #[thrust::extern_spec_fn]
    #[allow(path_statements)]
    fn _thrust_extern_spec_len(&self) -> usize where T: thrust_models::Model,
        <T as thrust_models::Model>::Ty: PartialEq {

        #[thrust::requires_path]
        Self::_thrust_requires_len;

        #[thrust::ensures_path]
        Self::_thrust_ensures_len;
        Self::len(self)
    }
}

• To expand formula_fn for methods of polymorphic ADT, the proc macro needs information of generics of the outer impl block. I've implemented thrust_macros::context which copies impl information to each inner items so that the inner proc macros can make use of it (via thrust::_impl_context attribute which is not used by backend)
• We can't simply copy formula expression in this case because self is now <&Self as Model>::Ty, not &Self. thrust_macros now renames the parameters and self in the formula expression accordingly to handle this

[Copilot]

Pull request overview

This PR enables thrust_macros::requires / thrust_macros::ensures to be used on methods inside impl blocks by propagating impl generics/context into each method and adjusting expansion details (notably self handling and Self:: path qualification) so the generated helper functions and extern-spec wrappers are well-formed in an impl context.

Changes:

• Added #[thrust_macros::context] to annotate impl blocks and inject a #[thrust::_impl_context(...)] marker onto contained methods for downstream macro expansion.
• Updated requires/ensures expansion to (a) consume impl generics for bounds generation, (b) rename self → self_ inside formula expressions when a receiver exists, and (c) qualify calls/paths with Self:: when expanding within an impl.
• Extended analyzer handling so #[thrust::extern_spec_fn] can be processed when attached to impl items (and trait items), plus improved annotated-path resolution via type checking.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
thrust-macros/src/lib.rs	Adds context macro, extracts impl context, rewrites self in formulas, and adjusts generated paths/where-clauses for impl-method expansions.
thrust-macros/Cargo.toml	Updates syn features for the new visitor-based implementation.
tests/ui/pass/annot_struct_impl.rs	Adds a passing UI test demonstrating requires/ensures on methods inside a generic impl wrapped with #[thrust_macros::context].
tests/ui/fail/annot_struct_impl.rs	Adds a failing UI test to ensure incorrect method postconditions are rejected in the new impl-annotation scenario.
src/analyze/local_def.rs	Allows extern_spec_fn target extraction for impl items (and trait items), not just top-level function items.
src/analyze.rs	Resolves annotated paths using typeck (qpath_res) instead of relying on syntactic QPath::Resolved.

---

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

[coord-e]

I am leaving unclear question to proceed for now