Introduce ghost variables

src/analyze/annot.rs

@@ -202,6 +202,14 @@ pub fn invariant_marker_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn ghost_marker_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("ghost_marker"),
+    ]
+}
+
 pub fn fn_param_wrapper_path() -> [Symbol; 3] {
     [
         Symbol::intern("thrust"),

src/analyze/annot_fn.rs

@@ -43,6 +43,10 @@ impl<'tcx> FormulaFn<'tcx> {
         &self.formula
     }
 
+    pub fn params(&self) -> &IndexVec<rty::FunctionParamIdx, mir_ty::Ty<'tcx>> {
+        &self.params
+    }
+
     pub fn to_require_formula(&self) -> chc::Formula<rty::FunctionParamIdx> {
         self.formula.clone()
     }

src/analyze/basic_block.rs

@@ -968,6 +968,99 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
     }
 
+    /// The formula function a ghost marker call carries, or `None` for any other call.
+    ///
+    /// The marker's argument is the formula function item `thrust_macros::ghost!`
+    /// introduces, whose parameter `0` is the ghost value and whose remaining parameters
+    /// name the live variables the ghost term refers to.
+    fn ghost_marker_formula_fn(
+        &self,
+        func: &Operand<'tcx>,
+        args: &[rustc_span::source_map::Spanned<Operand<'tcx>>],
+    ) -> Option<(LocalDefId, mir_ty::GenericArgsRef<'tcx>)> {
+        let (def_id, _) = func.const_fn_def()?;
+        if Some(def_id) != self.ctx.def_ids().ghost_marker() {
+            return None;
+        }
+
+        let arg_ty = args[0].node.ty(&self.local_decls, self.tcx);
+        let mir_ty::TyKind::FnDef(formula_def_id, generic_args) = arg_ty.kind() else {
+            panic!("ghost marker argument must be a formula function item");
+        };
+        let formula_def_id = formula_def_id
+            .as_local()
+            .expect("ghost formula function must be local");
+        Some((formula_def_id, generic_args))
+    }
+
+    /// Resolves the value a ghost term refers to by source variable name.
+    ///
+    /// A variable whose value is a constant is held in the debug info itself rather than
+    /// in a local of its own, so both forms are read back here.
+    fn operand_of_name(&self, name: rustc_span::Symbol) -> Option<Operand<'tcx>> {
+        self.body
+            .var_debug_info
+            .iter()
+            .filter(|vdi| vdi.name == name)
+            .find_map(|vdi| match &vdi.value {
+                mir::VarDebugInfoContents::Place(place) => (place.projection.is_empty()
+                    && self.is_defined(place.local))
+                .then_some(Operand::Copy(*place)),
+                mir::VarDebugInfoContents::Const(constant) => {
+                    Some(Operand::Constant(Box::new(*constant)))
+                }
+            })
+    }
+
+    /// Types the introduction of a ghost value: the value is the one its term denotes in
+    /// the current environment.
+    ///
+    /// A ghost term is a formula function laid out like an `ensures` — parameter `0` is
+    /// the value, the rest are free — so it reads as the return refinement of a function
+    /// over the live variables it names, and the introduction as a call to that function.
+    fn type_ghost_value(
+        &mut self,
+        formula_def_id: LocalDefId,
+        generic_args: mir_ty::GenericArgsRef<'tcx>,
+        expected_value: &rty::RefinedType<Var>,
+    ) {
+        let formula_fn = self
+            .ctx
+            .formula_fn_with_args(formula_def_id, generic_args)
+            .expect("ghost formula function is not registered");
+        let (value_ty, param_tys) = formula_fn
+            .params()
+            .raw
+            .split_first()
+            .expect("ghost formula function takes the ghost value as its first parameter");
+        let params = param_tys
+            .iter()
+            .map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous())
+            .collect();
+        let value_ty = self.type_builder.build(*value_ty);
+        let func_ty = rty::FunctionType::new(
+            params,
+            rty::RefinedType::new(value_ty.vacuous(), formula_fn.to_refinement()),
+        );
+
+        let idents = self.tcx.fn_arg_idents(formula_def_id.to_def_id()).to_vec();
+        let args = idents[1..]
+            .iter()
+            .map(|ident| {
+                let name = ident.expect("ghost term parameters must be named").name;
+                let operand = self.operand_of_name(name).unwrap_or_else(|| {
+                    self.tcx.dcx().fatal(format!(
+                        "ghost term refers to `{name}`, which is not a live variable here"
+                    ))
+                });
+                self.operand_refined_type(operand)
+            })
+            .collect();
+
+        let clauses = self.relate_fn_sub_type(func_ty, args, expected_value.clone());
+        self.ctx.extend_clauses(clauses);
+    }
+
     fn elaborate_place(&self, place: &mir::Place<'tcx>) -> mir::Place<'tcx> {
         let mut projection = Vec::new();
         if self.is_mut_local(place.local) {
@@ -1228,11 +1321,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 .for_template(&mut self.ctx)
                 .with_scope(&self.env)
                 .build_refined(decl.ty);
-            self.type_call(
-                func.clone(),
-                args.clone().iter().map(|a| a.node.clone()),
-                &rty,
-            );
+            if let Some((formula_def_id, generic_args)) = self.ghost_marker_formula_fn(func, args) {
+                self.type_ghost_value(formula_def_id, generic_args, &rty);
+            } else {
+                self.type_call(
+                    func.clone(),
+                    args.clone().iter().map(|a| a.node.clone()),
+                    &rty,
+                );
+            }
             self.bind_local(destination, rty);
         }
     }

src/analyze/did_cache.rs

@@ -35,6 +35,7 @@ struct DefIds {
     forall: OnceCell<Option<DefId>>,
     implies: OnceCell<Option<DefId>>,
     invariant_marker: OnceCell<Option<DefId>>,
+    ghost_marker: OnceCell<Option<DefId>>,
 
     fn_param_wrapper: OnceCell<Option<DefId>>,
     fn_param_at_entry: OnceCell<Option<DefId>>,
@@ -256,6 +257,13 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::invariant_marker_path()))
     }
 
+    pub fn ghost_marker(&self) -> Option<DefId> {
+        *self
+            .def_ids
+            .ghost_marker
+            .get_or_init(|| self.annotated_def(&crate::analyze::annot::ghost_marker_path()))
+    }
+
     pub fn fn_param_wrapper(&self) -> Option<DefId> {
         *self
             .def_ids

src/main.rs

@@ -19,6 +19,15 @@ impl Callbacks for CompilerCalls {
         attrs.push("feature(register_tool)".to_owned());
         attrs.push("register_tool(thrust)".to_owned());
 
+        // Thrust refines values, which it tracks through MIR locals. `RemoveZsts` rewrites
+        // reads of zero-sized locals into constants, which loses the refinement of every
+        // value whose type carries no runtime data -- the model types and `Ghost<T>`.
+        config
+            .opts
+            .unstable_opts
+            .mir_enable_passes
+            .push(("RemoveZsts".to_owned(), false));
+
         config.override_queries = Some(|_sess, providers| {
             providers.mir_borrowck = thrust::mir_borrowck_skip_formula_fn;
         });

std.rs

@@ -412,6 +412,36 @@ mod thrust_models {
         unimplemented!()
     }
 
+    /// Proof-only data, introduced by `thrust_macros::ghost!`.
+    ///
+    /// A `Ghost<T>` has no runtime representation, and program code cannot observe its
+    /// content: the only operations on it are moving and copying it around. In the logic
+    /// it *is* its content, so a specification refers to it as if it were a `T`.
+    #[allow(dead_code)]
+    pub struct Ghost<T: ?Sized>(std::marker::PhantomData<T>);
+
+    // `PhantomData` is `Copy` whatever `T` is, so these are unconditional; deriving them
+    // would demand `T: Copy`.
+    impl<T: ?Sized> Clone for Ghost<T> {
+        #[thrust::ignored]
+        fn clone(&self) -> Self {
+            *self
+        }
+    }
+
+    impl<T: ?Sized> Copy for Ghost<T> {}
+
+    impl<T: ?Sized> Model for Ghost<T> where T: Model {
+        type Ty = <T as Model>::Ty;
+    }
+
+    #[thrust::def::ghost_marker]
+    #[thrust::ignored]
+    #[inline(never)]
+    pub fn __ghost_marker<F, T>(_f: F) -> Ghost<T> {
+        Ghost(std::marker::PhantomData)
+    }
+
     #[allow(dead_code)]
     #[thrust::def::fn_param_wrapper]
     pub struct FnParam<T>(std::marker::PhantomData<T>);

tests/ui/fail/ghost_field.rs

@@ -0,0 +1,24 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+/// Counts how many values were recorded, and remembers them in a ghost field.
+struct Counter {
+    count: i64,
+    seen: Ghost<Seq<Int>>,
+}
+
+impl thrust_models::Model for Counter {
+    type Ty = (Int, Seq<Int>);
+}
+
+#[thrust_macros::requires((*c).1.len() == (*c).0)]
+#[thrust_macros::ensures((!c).1.len() == (!c).0)]
+fn record(c: &mut Counter, x: i64) {
+    c.count += 1;
+    c.seen = thrust_macros::ghost!(|c: &mut Counter, x: i64| -> Seq<Int> { (*c).1 });
+}
+
+fn main() {}

tests/ui/fail/ghost_local.rs

@@ -0,0 +1,16 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+#[thrust_macros::requires(s.len() == 1)]
+fn expect_len_one(s: Ghost<Seq<Int>>) {
+    let _ = s;
+}
+
+fn main() {
+    let x: i64 = 3;
+    let s = thrust_macros::ghost!(|x: i64| -> Seq<Int> { Seq::singleton(x).push(x) });
+    expect_len_one(s);
+}

tests/ui/pass/ghost_field.rs

@@ -0,0 +1,24 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+/// Counts how many values were recorded, and remembers them in a ghost field.
+struct Counter {
+    count: i64,
+    seen: Ghost<Seq<Int>>,
+}
+
+impl thrust_models::Model for Counter {
+    type Ty = (Int, Seq<Int>);
+}
+
+#[thrust_macros::requires((*c).1.len() == (*c).0)]
+#[thrust_macros::ensures((!c).1.len() == (!c).0)]
+fn record(c: &mut Counter, x: i64) {
+    c.count += 1;
+    c.seen = thrust_macros::ghost!(|c: &mut Counter, x: i64| -> Seq<Int> { (*c).1.push(x) });
+}
+
+fn main() {}

tests/ui/pass/ghost_local.rs

@@ -0,0 +1,16 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off -A unused-variables
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+#[thrust_macros::requires(s.len() == 1)]
+fn expect_len_one(s: Ghost<Seq<Int>>) {
+    let _ = s;
+}
+
+fn main() {
+    let x: i64 = 3;
+    let s = thrust_macros::ghost!(|x: i64| -> Seq<Int> { Seq::singleton(x) });
+    expect_len_one(s);
+}

thrust-macros/src/ghost.rs

@@ -0,0 +1,93 @@
+//! Expansion of `thrust_macros::ghost!`.
+//!
+//! A ghost expression is a logical term over the live variables it names, so it expands
+//! into a `#[thrust::formula_fn]` relating the introduced value to that term, laid out
+//! like an `ensures` formula function (parameter `0` is the value), plus a marker call
+//! the analyzer intercepts to bind the value:
+//!
+//! ```ignore
+//! ghost!(|s: Ghost<Seq<Int>>, x: i64| -> Seq<Int> { s.push(x) })
+//! ```
+//!
+//! becomes
+//!
+//! ```ignore
+//! {
+//!     #[thrust::formula_fn]
+//!     fn _thrust_ghost_0(
+//!         result: <Seq<Int> as Model>::Ty,
+//!         s: <Ghost<Seq<Int>> as Model>::Ty,
+//!         x: <i64 as Model>::Ty,
+//!     ) -> bool {
+//!         result == (s.push(x))
+//!     }
+//!     thrust_models::__ghost_marker::<_, Seq<Int>>(_thrust_ghost_0)
+//! }
+//! ```
+//!
+//! The parameters name the live variables the term refers to, with their types, exactly
+//! as in [`crate::invariant`]; the return type names the logical type of the introduced
+//! value.
+
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+use proc_macro::TokenStream;
+use quote::{format_ident, ToTokens};
+use syn::FnArg;
+
+use crate::FormulaFnTypeLowering;
+
+static COUNTER: AtomicUsize = AtomicUsize::new(0);
+
+pub fn expand(input: TokenStream) -> TokenStream {
+    let input = crate::formula::wrap_closure_body(input.into());
+    let closure = match syn::parse2::<syn::ExprClosure>(input) {
+        Ok(closure) => closure,
+        Err(e) => return e.to_compile_error().into(),
+    };
+    match expand_ghost(&closure) {
+        Ok(expr) => expr.into_token_stream().into(),
+        Err(e) => e.to_compile_error().into(),
+    }
+}
+
+fn expand_ghost(closure: &syn::ExprClosure) -> syn::Result<syn::Expr> {
+    let syn::ReturnType::Type(_, value_ty) = &closure.output else {
+        return Err(syn::Error::new_spanned(
+            closure,
+            "ghost expression must have an explicit type, e.g. `|x: i64| -> Seq<Int> { .. }`",
+        ));
+    };
+
+    // Parameter `0` is the introduced value, named `result` as in an `ensures` formula.
+    let mut fn_params: Vec<FnArg> = vec![syn::parse_quote!(result: #value_ty)];
+    for param in &closure.inputs {
+        let syn::Pat::Type(pt) = param else {
+            return Err(syn::Error::new_spanned(
+                param,
+                "ghost expression parameters must have explicit types, e.g. `|x: i64| ...`",
+            ));
+        };
+        let pat = &pt.pat;
+        let ty = &pt.ty;
+        fn_params.push(syn::parse_quote!(#pat: #ty));
+    }
+
+    let dummy_sig = syn::parse_quote!(fn f());
+    let model_ty_params = FormulaFnTypeLowering::new(&dummy_sig).lower_params(&fn_params);
+
+    let body = &closure.body;
+    let id = COUNTER.fetch_add(1, Ordering::Relaxed);
+    let name = format_ident!("_thrust_ghost_{}", id);
+
+    Ok(syn::parse_quote!({
+        #[allow(unused_variables)]
+        #[allow(non_snake_case)]
+        #[thrust::formula_fn]
+        fn #name(#model_ty_params) -> bool {
+            result == (#body)
+        }
+
+        thrust_models::__ghost_marker::<_, #value_ty>(#name)
+    }))
+}