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

src/analyze/annot_fn.rs

@@ -19,6 +19,20 @@ pub struct FormulaFn<'tcx> {
     formula: chc::Formula<rty::FunctionParamIdx>,
 }
 
+/// The source name a parameter of a formula function lifted out of a function body
+/// (`invariant!`, `ghost!`) refers to.
+///
+/// The lifted function is free, where `self` is not a legal parameter name, so a formula
+/// naming the receiver gets a synthetic parameter instead. It stands for the value that
+/// debug info records as `self`.
+pub fn lifted_param_source_name(ident: rustc_span::symbol::Ident) -> rustc_span::Symbol {
+    if ident.name.as_str() == "__thrust_self" {
+        rustc_span::Symbol::intern("self")
+    } else {
+        ident.name
+    }
+}
+
 impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &FormulaFn<'_>
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,

src/analyze/basic_block.rs

@@ -1054,9 +1054,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             .skip(1)
             .map(|ident| {
                 let ident = ident.expect("ghost term parameters must be named");
-                let operand = self.operand_of_name(ident.name).unwrap_or_else(|| {
+                let name = analyze::annot_fn::lifted_param_source_name(ident);
+                let operand = self.operand_of_name(name).unwrap_or_else(|| {
                     self.tcx.dcx().fatal(format!(
-                        "ghost term refers to `{ident}`, which is not a live variable here"
+                        "ghost term refers to `{name}`, which is not a live variable here"
                     ))
                 });
                 self.operand_refined_type(operand)

src/analyze/local_def.rs

@@ -853,13 +853,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     .unwrap_or(*input_ty)
             };
 
-            // The synthetic `__thrust_self` parameter (emitted when an invariant refers to the receiver
-            // `self`) maps to the loop-carried receiver, which appears as `self` in debug info.
-            let name = if ident.name.as_str() == "__thrust_self" {
-                rustc_span::Symbol::intern("self")
-            } else {
-                ident.name
-            };
+            let name = analyze::annot_fn::lifted_param_source_name(ident);
 
             if input_ty
                 .ty_adt_def()

tests/ui/fail/ghost_generic.rs

@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::Ghost;
+
+#[thrust_macros::requires(g == v)]
+fn expect_same<T>(g: Ghost<T>, v: T) {
+    let _ = g;
+}
+
+#[thrust_macros::context]
+fn record<T: Copy>(a: T, b: T) {
+    let g = thrust_macros::ghost!(|b: T| -> T { b });
+    expect_same(g, a);
+}
+
+fn main() {
+    record(3_i64, 5_i64);
+}

tests/ui/fail/ghost_self.rs

@@ -0,0 +1,26 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+struct Counter {
+    count: i64,
+    seen: Ghost<Seq<Int>>,
+}
+
+impl thrust_models::Model for Counter {
+    type Ty = (Int, Seq<Int>);
+}
+
+#[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 });
+    }
+}
+
+fn main() {}

tests/ui/pass/ghost_generic.rs

@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::Ghost;
+
+#[thrust_macros::requires(g == v)]
+fn expect_same<T>(g: Ghost<T>, v: T) {
+    let _ = g;
+}
+
+#[thrust_macros::context]
+fn record<T: Copy>(a: T, b: T) {
+    let g = thrust_macros::ghost!(|a: T| -> T { a });
+    expect_same(g, a);
+}
+
+fn main() {
+    record(3_i64, 5_i64);
+}

tests/ui/pass/ghost_self.rs

@@ -0,0 +1,27 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+struct Counter {
+    count: i64,
+    seen: Ghost<Seq<Int>>,
+}
+
+impl thrust_models::Model for Counter {
+    type Ty = (Int, Seq<Int>);
+}
+
+#[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) });
+    }
+}
+
+fn main() {}

thrust-macros/src/context.rs

@@ -2,13 +2,13 @@
 //!
 //! Makes the enclosing context available to the specifications written inside an item.
 //!
-//! On a function, every `thrust_macros::invariant!(...)` in the body is rewritten into
-//! its context-carrying counterpart, carrying the host signature and, for a method, the
-//! enclosing `impl`/`trait` header, so an invariant may refer to generic- and
-//! `Self`-typed variables that the standalone macro cannot see. That also extends the
-//! function's where clause with the `Model` predicates for every in-scope type parameter
-//! (and for `Self` when used), since each injected marker call instantiates a
-//! `Model`-bounded formula function with the host's own generics.
+//! On a function, every `thrust_macros::invariant!(...)` and `thrust_macros::ghost!(...)`
+//! in the body is rewritten into its context-carrying counterpart, carrying the host
+//! signature and, for a method, the enclosing `impl`/`trait` header, so a formula may
+//! refer to generic- and `Self`-typed variables that the standalone macros cannot see.
+//! That also extends the function's where clause with the `Model` predicates for every
+//! in-scope type parameter (and for `Self` when used), since each injected marker call
+//! instantiates a `Model`-bounded formula function with the host's own generics.
 //!
 //! On an `impl`/`trait`, each method is stamped with the enclosing header — which is what
 //! method-level `requires`/`ensures` read to recover the outer generics — and with this
@@ -80,9 +80,9 @@ fn expand_outer(mut outer_item: FnOuterItem) -> TokenStream {
     outer_item.into_token_stream().into()
 }
 
-/// Rewrites each `invariant!` in the body into its context-carrying counterpart and
-/// extends the where clause with the `Model` predicates those calls need. A body naming
-/// no invariant — or a trait method that has no body at all — is left as it is.
+/// Rewrites each spec macro in the body into its context-carrying counterpart and extends
+/// the where clause with the `Model` predicates those calls need. A body naming no spec
+/// macro — or a trait method that has no body at all — is left as it is.
 fn expand_fn(mut func: FnItemWithSignature) -> TokenStream {
     let outer = match crate::extract_outer_context(func.attrs()) {
         Ok(outer) => outer,
@@ -146,19 +146,25 @@ impl ContextInjector<'_> {
 
 impl VisitMut for ContextInjector<'_> {
     fn visit_macro_mut(&mut self, mac: &mut syn::Macro) {
-        if !is_invariant_macro(&mac.path) {
+        let Some(with_context) = context_carrying_form(&mac.path) else {
             return;
-        }
+        };
         self.injected = true;
         if crate::tokens_contain_ident(&mac.tokens, "Self") {
             self.self_used = true;
         }
         mac.tokens = self.inject_context(&mac.tokens);
-        mac.path = syn::parse_quote!(::thrust_macros::_invariant_with_context);
+        mac.path = with_context;
     }
 }
 
-fn is_invariant_macro(path: &syn::Path) -> bool {
+/// The context-carrying counterpart of a spec macro that takes a formula over live
+/// variables, or `None` for any other macro.
+fn context_carrying_form(path: &syn::Path) -> Option<syn::Path> {
     // TODO: identify the macro precisely
-    path.segments.last().is_some_and(|s| s.ident == "invariant")
+    match path.segments.last()?.ident.to_string().as_str() {
+        "invariant" => Some(syn::parse_quote!(::thrust_macros::_invariant_with_context)),
+        "ghost" => Some(syn::parse_quote!(::thrust_macros::_ghost_with_context)),
+        _ => None,
+    }
 }