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

[coord-e]

Follows #220, on top of #231. Three commits, each standing on its own:

4154ba3	move the formula-function lifting invariant! carried into formula_fn_lifting — no behaviour change
eeb87fb	name the rule that resolves a lifted function's receiver parameter, and read it from both the invariant and the ghost path
2d34fe7	thread the enclosing context into ghost!, plus tests

The gap

A ghost term is lifted 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

formula_fn_lifting holds what both macros need to lift a formula out of a body:

• 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, which the analyzer resolves back through annot_fn::lifted_param_source_name.

For ghost! the introduced value is parameter 0, so it passes through that 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.

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.

[Copilot]

🟡 Changes recommended

Macro matching can incorrectly rewrite unrelated macros named ghost.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Adds context-aware lifting so ghost! terms can reference generic and Self-typed variables.

Changes:

• Extracts shared formula-function lifting from invariant!.
• Threads enclosing context into ghost!.
• Adds analyzer support and paired UI tests.

File summaries

File	Description
thrust-macros/src/lib.rs	Registers lifting module and context-aware ghost macro.
thrust-macros/src/invariant.rs	Uses shared lifting logic.
thrust-macros/src/ghost.rs	Adds context-aware ghost expansion.
thrust-macros/src/formula_fn_lifting.rs	Implements shared formula lifting.
thrust-macros/src/context.rs	Injects context into ghost macros.
src/analyze/annot_fn.rs	Centralizes lifted parameter name resolution.
src/analyze/local_def.rs	Uses shared name resolution for invariants.
src/analyze/basic_block.rs	Resolves lifted ghost receiver names.
tests/ui/pass/ghost_self.rs	Tests valid Self-typed ghost terms.
tests/ui/fail/ghost_self.rs	Tests invalid Self-typed ghost behavior.
tests/ui/pass/ghost_generic.rs	Tests valid generic ghost terms.
tests/ui/fail/ghost_generic.rs	Tests invalid generic ghost behavior.

Review details

• Files reviewed: 12/12 changed files
• Comments generated: 1
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2d34fe77ae

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".