Enable to use thrust_macros::{ensures,requires} for trait method annotations

[coord-e]

The expansion of thrust_macros::{ensures, requires} remains mostly the same, but there’s a lot of plumbing involved to make this work. While the previous annotation mechanism directly attached attributes to the target def, thrust_macros::{ensures, requires} attaches annotations via extern_spec_fn. This made it difficult to fetch annotations using extract_{require, ensure}_annot. Instead, this PR’s implementation relies on def_ty_with_args to fetch the expected type of the trait method, which is given as an individual entry of defs (the previous implementation didn’t define the type of definition-side trait methods simply because they don’t have a body). See individual commits for details.

[Copilot]

Pull request overview

Enables using thrust_macros::{requires, ensures, predicate} on trait method declarations and trait impl methods by introducing an outer “context” mechanism and updating analysis/type-resolution to fetch expected trait-item types via def_ty_with_args.

Changes:

• Extend thrust_macros::context to wrap both impl blocks and trait definitions, and broaden macro parsing to handle free fns / impl methods / trait methods.
• Update analyzer logic to prefer trait-item refined types (via def_ty_with_args) when an impl method isn’t fully annotated, improving trait-method annotation support.
• Refresh UI tests to use thrust_macros::* annotations in traits/impls and adjust formulas to the current *x / !x pre/post-state notation.

Reviewed changes

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

Show a summary per file

File	Description
thrust-macros/src/lib.rs	Adds support for parsing/expanding annotations on trait methods and plumbs outer context into macro expansion.
src/analyze/local_def.rs	Uses trait-item expected types as a fallback when impl items aren’t fully annotated; refactors predicate-definition plumbing.
src/analyze/crate_.rs	Updates call site for refactored predicate-definition analysis.
src/analyze/basic_block.rs	Refactors fn-def type lookup into a helper that can resolve instances/shims when needed.
src/analyze/annot_fn.rs	Resolves predicate calls in formulas through Instance::resolve to get the correct DefId.
std.rs	Broadens several model wrapper types to ?Sized.
tests/ui/pass/iterators/annot_range_next.rs	Migrates iterator trait/impl annotations to thrust_macros::* and adds required outer context.
tests/ui/pass/iterators/annot_range_loop.rs	Same as above, for loop variant.
tests/ui/pass/annot_preds_trait.rs	Adds trait-level predicate/requires/ensures annotations using thrust_macros::*.
tests/ui/pass/annot_preds_trait_multi.rs	Same as above, covering multiple implementors.
tests/ui/fail/iterators/annot_range_next.rs	Updates failing UI test to new macro forms and context wrapping.
tests/ui/fail/iterators/annot_range_loop.rs	Updates failing UI test to new macro forms and context wrapping.
tests/ui/fail/annot_preds_trait.rs	Updates failing UI test to new macro forms and context wrapping.
tests/ui/fail/annot_preds_trait_multi.rs	Updates failing UI test to new macro forms and context wrapping.

Comments suppressed due to low confidence (4)

std.rs:77

• Mut was changed to Mut<T: ?Sized>, but the inherent/trait impls below still use impl<T> / impl<T, U>, which implicitly restricts them to T: Sized. This makes thrust_models::model::Mut<Unsized> lack PartialEq, Deref, and Not impls, which can break bounds like <T as Model>::Ty: PartialEq for T: ?Sized. Consider changing these impl headers to T: ?Sized and adding where T: Sized only on methods that truly require sized values (e.g., new).

        #[thrust::def::mut_model]
        pub struct Mut<T: ?Sized>(PhantomData<T>);

        impl<T> Mut<T> {
            #[allow(dead_code)]
            #[thrust::def::mut_new]
            #[thrust::ignored]
            pub fn new(_a: T, _b: T) -> Self {
                unimplemented!()
            }
        }

        impl<T, U> PartialEq<U> for Mut<T> where U: super::Model<Ty = Self> {

std.rs:122

• Box was changed to Box<T: ?Sized>, but the inherent/trait impls below are still impl<T> / impl<T, U>, so they only apply when T: Sized. This prevents thrust_models::model::Box<Unsized> from satisfying bounds like PartialEq that the macros can add for T: ?Sized. Update these impl headers to T: ?Sized and constrain only the by-value constructor (new) with T: Sized if needed.

        #[thrust::def::box_model]
        pub struct Box<T: ?Sized>(PhantomData<T>);

        impl<T> Box<T> {
            #[allow(dead_code)]
            #[thrust::def::box_new]
            #[thrust::ignored]
            pub fn new(_x: T) -> Self {
                unimplemented!()
            }
        }

        impl<T, U> PartialEq<U> for Box<T> where U: super::Model<Ty = Self> {
            #[thrust::ignored]
            fn eq(&self, _other: &U) -> bool {
                unimplemented!()
            }
        }

        impl<T> std::ops::Deref for Box<T> {
            type Target = T;

std.rs:154

• Array is now Array<I: ?Sized, T: ?Sized>, but the impls below (PartialEq, Index, and the inherent store) are still written as impl<I, T, ...> / impl<I, T>, which only cover Sized parameters. If I/T are intended to support ?Sized, update the relevant impl headers accordingly; otherwise, consider reverting the struct params back to Sized (especially I, which is taken by value in Index/store).

        #[thrust::def::array_model]
        pub struct Array<I: ?Sized, T: ?Sized>(PhantomData<I>, PhantomData<T>);

        impl<I, T, U> PartialEq<U> for Array<I, T> where U: super::Model<Ty = Self> {
            #[thrust::ignored]
            fn eq(&self, _other: &U) -> bool {
                unimplemented!()
            }
        }

        impl<I, T> std::ops::Index<I> for Array<I, T> {
            type Output = T;

            #[thrust::ignored]
            fn index(&self, _index: I) -> &Self::Output {
                unimplemented!()
            }
        }

        impl<I, T> Array<I, T> {
            #[allow(dead_code)]
            #[thrust::def::array_store]
            #[thrust::ignored]
            pub fn store(&self, _index: I, _value: T) -> Self {
                unimplemented!()

std.rs:166

• Vec was changed to Vec<T: ?Sized>, but the PartialEq impl below is still impl<T, U> PartialEq<U> for Vec<T>, which only applies for T: Sized. If Vec<T> is meant to be usable with unsized T (matching the struct definition), change this impl header to T: ?Sized.

        #[thrust::def::closure_model]
        pub struct Closure<T: ?Sized>(PhantomData<T>);

        pub struct Vec<T: ?Sized>(pub Array<Int, T>, pub Int);

        impl<T, U> PartialEq<U> for Vec<T> where U: super::Model<Ty = Self> {
            #[thrust::ignored]
            fn eq(&self, _other: &U) -> bool {
                unimplemented!()

---

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