Implement loop invariant annotation

[coord-e]

Summary

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

fn f() {
    while cond {
        thrust_macros::invariant!(|x: i64, y: i64| x >= 1 && y >= 1);
        ...
    }
}

Scope: concrete (non-generic, non-Self) variable types only. Support for generic- and Self-typed variables — which requires extending #[thrust_macros::context] to thread the enclosing context into each invariant! — is split into a follow-up PR (#99).

Frontend (thrust-macros)

• invariant!(|x: T, ...| pred) expands into a #[thrust::formula_fn] over Model::Ty parameters and 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.
• An invariant naming Self is rejected with a clear message until the follow-up lands.

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.

Stacked

Generic- and Self-typed invariant variables (and the #[thrust_macros::context] extension that enables them): #99 — branch claude/loop-invariant-context-self-generics, based on this PR.

Test plan

• Pass/fail UI test pairs: basic, mutable reference, nested loops, method.
• cargo test --test ui (196 passed), cargo clippy --all-targets, cargo fmt --check all clean.

https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt

[Copilot]

Pull request overview

Adds a minimal Prusti-style thrust_macros::invariant!(|x: T, ...| pred) macro for declaring loop invariants inside loop bodies. The macro expands to a #[thrust::formula_fn] plus a marker call (thrust_models::__invariant_marker); the analyzer collects marker terminators, maps them to the enclosing loop header via the dominator tree, resolves named formula parameters to live MIR locals, and installs the formula as the header's precondition (replacing the inferred pvar). Multiple invariants at the same header are AND'd in source order. Scope is intentionally limited to concrete (non-generic, non-Self) variable types; generics/Self are deferred to #99.

Changes:

• New invariant! proc macro and shared helper reuse in thrust-macros.
• New __invariant_marker shim in std.rs plus annotation path and DefId cache entry.
• Analyzer support: marker collection, loop-header resolution via dominators, name→local resolution, formula→precondition translation, and marker terminator elaborated to Goto.

Reviewed changes

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

Show a summary per file

File	Description
thrust-macros/src/lib.rs	Registers the new invariant! proc macro entry point.
thrust-macros/src/invariant.rs	Parses the closure, rewrites params through Model::Ty, emits a formula_fn and the marker call.
std.rs	Adds the __invariant_marker shim annotated for analyzer lookup.
src/analyze/annot.rs	Adds invariant_marker_path() for annotation lookup.
src/analyze/did_cache.rs	Caches the marker's DefId.
src/analyze/annot_fn.rs	Exposes FormulaFn::formula() accessor.
src/analyze/basic_block.rs	Elaborates marker call terminator into a plain Goto.
src/analyze/local_def.rs	Collects markers, resolves loop headers and live locals, installs invariant as the header's precondition.
tests/ui/{pass,fail}/loop_invariant*.rs	Pass/fail UI test pairs covering basic, nested, mutable-ref, multi-invariant, and method cases.

---

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