Let a ghost term name generic- and Self-typed variables

[coord-e]

Follows #220. Stacked on #231 — review that one first; this branch's own change is the second commit.

ghost! lifts its term into a free #[thrust::formula_fn], which inherits neither the enclosing function's generics nor Self, so a term could only name variables of concrete type — the last of #220's known gaps. #[thrust_macros::context] already threads that context into invariant!; it now threads it into ghost! too.

#[thrust_macros::context]
impl Counter {
    #[thrust_macros::requires((*self).1.len() == (*self).0)]
    #[thrust_macros::ensures((!self).1.len() == (!self).0)]
    fn record(&mut self, x: i64) {
        self.count += 1;
        self.seen = thrust_macros::ghost!(|self: &mut Self, x: i64| -> Seq<Int> { (*self).1.push(x) });
    }
}

#[thrust_macros::context]
fn record<T: Copy>(a: T, b: T) {
    let g = thrust_macros::ghost!(|a: T| -> T { a });
    expect_same(g, a);
}

How it works

The context handling invariant! carried moves to a new formula_fn_lifting module, which both macros now build their formula function with:

• the in-scope generics are re-declared on the formula function and instantiated via turbofish;
• Self is rewritten to the impl's self type, or to a synthetic type parameter instantiated with the real Self in a trait;
• the receiver self is renamed to a __thrust_self parameter.

For ghost! the introduced value is parameter 0, so it passes through the same lifting as an ordinary parameter: a value type naming Self or a generic is rewritten along with the rest, while the __ghost_marker::<_, T> turbofish keeps the type as written, since the marker call stays in the host's scope.

On the analyzer side the ghost path resolves __thrust_self back to the receiver the way the invariant path already does; the shared rule is annot_fn::lifted_param_source_name.

Tests

ghost_self	ghost field of a struct updated by a method whose term names self
ghost_generic	ghost value of a generic type, from a term naming a generic-typed live variable

Each as a pass/fail pair; in both, the fail file differs only in which live variable the term names.

Known gaps

• Self in a generic or trait impl is unsupported, unchanged from invariant! — both now go through the same TODO, so a fix covers them together.

---

Generated by Claude Code