Fold invariant_context into context

[coord-e]

#[thrust_macros::context] stamped each method of an impl/trait with the enclosing header, while #[thrust_macros::invariant_context] threaded the same header — plus the host signature — into the invariant! calls in a function body. Two attributes for one question: what does the code inside this item see?

They become one. #[thrust_macros::context] now takes a function as well, and on an impl/trait it threads every method's body as it stamps it, so a method carrying a loop invariant no longer needs an attribute of its own:

#[thrust_macros::context]
impl Counter {
    fn run(&mut self) -> i64 {
        let init = *self;
        while rand() {
            thrust_macros::invariant!(|init: Self, self: &mut Self| init.value <= (*self).value);
            self.value += 1;
        }
        init.value
    }
}

A free function still opts in explicitly, with #[thrust_macros::context] in place of the old name.

Not extending a where clause nothing asked for

Threading a body that names no spec macro now leaves it alone. invariant_context extended the host's where clause with the Model predicates unconditionally, which was fine while it was opt-in per function; with every method of a #[context] item threaded, those bounds would otherwise land on methods that have no formula to justify them.

Changes

context.rs	takes a fn as well as an impl/trait; ContextInjector moves here from invariant_context.rs, which is deleted
tests/ui	17 files: free functions take #[thrust_macros::context], methods drop the attribute entirely

No behaviour change for the analyzer; the macro expansion each test produces is the same as before.

---

Generated by Claude Code