Fix E0401 for invariant_context on trait methods

[coord-e]

#[thrust_macros::invariant_context] attached to a trait method fails to compile with E0401 ("can't use Self from outer item"):

#[thrust_macros::context]
trait Foo {
    #[thrust_macros::invariant_context]
    fn run(&mut self) {
        let mut x: i64 = 0;
        while x < 1 {
            thrust_macros::invariant!(|x: i64| x >= 0);
            x += 1;
        }
    }
}

Root cause

invariant_context rewrites each inner invariant! into a free-standing #[thrust::formula_fn] nested inside the method body. Inside that nested item, Self is out of scope, so any Self reaching it is rejected with E0401.

The macro already re-binds Self to a synthetic generic (__ThrustSelf, instantiated with the real Self via turbofish) — but it only did so when the closure mentioned Self. On a trait method, Self also reaches the generated function's where-clause through two paths that were never rewritten:

1. the host signature's own bounds (e.g. where Self: Sized), and
2. the Self: Model / <Self as Model>::Ty: PartialEq bounds a trait outer context contributes through model_where_predicates().

So for |x: i64| x >= 0 (no Self in the closure) those predicate-borne Selfs leaked through unbound. (The trait + Self-in-closure case was broken the same way.)

https://claude.ai/code/session_01UvhtewjXmse6vpHq7BJ81S

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR fixes a Rust E0401 compilation failure when #[thrust_macros::invariant_context] is applied to trait methods containing thrust_macros::invariant!(...), by ensuring Self is re-bound when it can leak into the generated nested #[thrust::formula_fn] via propagated where predicates (not only via the closure body).

Changes:

• Treat Self as “used” if it appears in propagated where-clause predicates (def_wheres), not just in the invariant closure tokens.
• Ensure trait-method invariants properly rewrite/bind Self even when the closure does not mention Self directly.
• Add UI tests covering both satisfiable and unsatisfiable loop-invariant cases in a trait method context.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
thrust-macros/src/invariant.rs	Expands the Self-usage detection to include propagated where predicates so nested formula fns don’t see unbound Self.
tests/ui/pass/loop_invariant_trait.rs	Adds a passing UI test for invariants in a trait method where Self only reaches generated bounds indirectly.
tests/ui/fail/loop_invariant_trait.rs	Adds a failing (Unsat) UI test for the same trait-method scenario to validate solver/reporting behavior.

---

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 21770e6a4b

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

Rewrite Self in copied generic parameter bounds

This detection still ignores Self that is copied through def_params, so trait methods with generic parameter bounds such as fn run<T: Marker<Self>>(&mut self) still expand to a nested formula function like fn _thrust_invariant_0<T: Marker<Self>, __ThrustSelf>(...), which triggers the same E0401 this change is trying to avoid. The branch rewrites parameters, the body, and def_wheres, but it never rewrites the generic parameter bounds already pushed into def_params; include those in the rewrite or move their bounds into the where-clause before rewriting.

Useful? React with 👍 / 👎.

[coord-e]

out of PR scope