Implement loop invariant annotation

[coord-e]

Summary

Adds Prusti-style loop invariant annotations. An invariant is written inside the loop body and refers to live variables by name:

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

Frontend (thrust-macros)

• invariant!(|x: T, ...| pred) expands into a #[thrust::formula_fn] over Model::Ty parameters plus a marker call (thrust_models::__invariant_marker) referencing it, so invariants reuse the exact static semantics of requires/ensures. The closure parameters name the live variables the invariant constrains.
• Because an in-body function-like macro cannot see the enclosing generics, the generated formula function re-declares the threaded generics (shadowing the enclosing ones) and is instantiated via turbofish. In methods, Self is re-declared as a synthetic type parameter and instantiated with the real Self the same way, so invariants may name generic- and Self-typed variables.
• #[thrust_macros::context] supplies that context: it stamps the enclosing impl/trait header onto each method (also used by method-level requires/ensures) and threads the in-scope generics/Self into every invariant!. It is general-purpose, not invariant-specific.
• invariant! also works without context for a concrete, non-generic invariant; one that names Self without context is rejected with a message pointing at the fix.
• The macro crate is reorganized into context, invariant, and spec modules; the crate root keeps only the proc-macro entry points and a few shared helpers.

Analyzer

• Collects invariant markers, maps each to its enclosing loop header (via the dominator tree), and turns the formula function into that header's precondition by binding each named formula parameter to the matching live basic-block parameter.
• Name→local resolution errors when several distinct live locals share a name (e.g. shadowing) instead of silently picking one. Resolving the intended shadow by lexical scope is left as future work.
• The marker terminator is elaborated to a plain goto so it is not type-checked as a real call.

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 change.

Test plan

• Pass/fail UI test pairs: basic, mutable-ref, nested loops, method, generic, Self, and no-context invariants.
• cargo test --test ui (201 passed), cargo clippy --all-targets, cargo fmt --check all clean.

https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt