Support Self and generic variables in loop invariants

[coord-e]

Summary

Extends thrust_macros::invariant! to invariants over generic- and Self-typed variables, by having #[thrust_macros::invariant_context] thread the enclosing context into each invariant!.

#[thrust_macros::invariant_context]
fn f(v: T) {
    while cond {
        thrust_macros::invariant!(|x: T, v: T| x == v);
        ...
    }
}

Frontend (thrust-macros)

The work is split so that invariant_context only injects context and invariant! does all the expansion — and the context rides on ordinary Rust syntax rather than any new bracket grammar.

• #[thrust_macros::invariant_context] accepts free functions, impl blocks, and trait definitions. It does not expand the invariants itself: for each invariant!(CLOSURE) it finds, it rewrites the macro input into a context-carrying form, and extends the host function's where clause with the Model/PartialEq bounds (which a function-like macro cannot add to its caller). The carried context reuses existing syntax — the enclosing function header (generics + where clause) is copied in as a fn header, and Self/outer generics ride on the existing #[thrust::_outer_context(impl/trait header)] attribute already used by #[thrust_macros::context] for requires/ensures:

  thrust_macros::invariant!(
      #[thrust::_outer_context(impl<T> Foo<T> where ..)]  // methods only
      fn _thrust_invariant_context<U>() where .. {
          |x: T, v: T| x == v
      }
  )

• invariant! performs the single, shared expansion for both the standalone concrete form and the threaded form. It re-declares the threaded generics (shadowing the enclosing ones) on the generated #[thrust::formula_fn] and instantiates it via turbofish; in methods, Self is re-declared as a synthetic type parameter and instantiated with the real Self (legal in expression position).

• The concrete, non-generic form from Implement loop invariant annotation #95 keeps working without invariant_context.

• The macro crate is organized into context, invariant, invariant_context, and spec modules; the root keeps only the proc-macro entry points and a few shared private helpers. The closure-parsing / formula_fn-synthesis / marker-call logic lives in exactly one place (invariant).

Test plan

• Pass/fail UI test pairs for the generic and Self cases (loop_invariant_generic, loop_invariant_self).
• cargo test --test ui, cargo clippy --all-targets, cargo fmt --check all clean.

Notes

• A struct used as an invariant variable must model structurally: its Model::Ty must mirror its fields (e.g. a one-field tuple struct models as a one-tuple). A mismatching model trips an existing subtyping panic unrelated to this PR.

https://claude.ai/code/session_01E4qhJALh9SAabEL1pQr6na

[Copilot]

Pull request overview

This PR extends loop invariant support in thrust-macros so thrust_macros::invariant! can reference generic-typed and Self-typed variables by threading the enclosing signature/outer context into each invariant expansion.

Changes:

• Adds #[thrust_macros::invariant_context] plus an internal _invariant_with_context! macro to carry the host signature (and outer impl/trait header) into invariant! calls.
• Updates the invariant expansion to (optionally) re-declare/instantiate in-scope generics via turbofish, and introduces helper utilities moved into lib.rs.
• Adds UI pass/fail tests covering generic and Self invariant variables (including a closure-typed generic param case).

Reviewed changes

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

Show a summary per file

File	Description
thrust-macros/src/spec.rs	Refactors to use shared crate::model_where_predicates / extract_outer_context helpers.
thrust-macros/src/lib.rs	Adds _invariant_with_context proc-macro, invariant_context attribute entrypoint, and shared helper functions.
thrust-macros/src/invariant.rs	Extends invariant expansion to accept threaded context and instantiate generics/Self.
thrust-macros/src/invariant_context.rs	New attribute macro to rewrite invariant! calls and add required Model bounds to the host function.
tests/ui/pass/loop_invariant_self.rs	New passing UI test for Self-typed invariant variables in a method.
tests/ui/pass/loop_invariant_generic.rs	New passing UI test for generic-typed invariant variables.
tests/ui/pass/loop_invariant_generic_closure.rs	New passing UI test ensuring closure-typed generics aren’t forced to implement Model.
tests/ui/fail/loop_invariant_self.rs	New failing UI test for an unsatisfiable Self-typed invariant.
tests/ui/fail/loop_invariant_generic.rs	New failing UI test for an unsatisfiable generic-typed invariant.

---

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