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

@@ -13,6 +13,9 @@ use crate::rty;
 #[derive(Debug, Clone)]
 pub struct FormulaFn<'tcx> {
     params: IndexVec<rty::FunctionParamIdx, mir_ty::Ty<'tcx>>,
+    // TODO: remove once we stop relying on debug info to map parameters
+    // `None` for a parameter bound by a pattern, as the closure upvars tuple is.
+    param_idents: IndexVec<rty::FunctionParamIdx, Option<rustc_span::symbol::Ident>>,
     formula: chc::Formula<rty::FunctionParamIdx>,
 }
 
@@ -43,6 +46,16 @@ impl<'tcx> FormulaFn<'tcx> {
         &self.formula
     }
 
+    pub fn params(&self) -> &IndexVec<rty::FunctionParamIdx, mir_ty::Ty<'tcx>> {
+        &self.params
+    }
+
+    pub fn param_idents(
+        &self,
+    ) -> &IndexVec<rty::FunctionParamIdx, Option<rustc_span::symbol::Ident>> {
+        &self.param_idents
+    }
+
     pub fn to_require_formula(&self) -> chc::Formula<rty::FunctionParamIdx> {
         self.formula.clone()
     }
@@ -382,8 +395,15 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
             .skip_binder()
             .inputs()
             .to_vec();
+        let param_idents = self
+            .tcx
+            .fn_arg_idents(self.local_def_id.to_def_id())
+            .iter()
+            .copied()
+            .collect();
         FormulaFn {
             params: IndexVec::from_raw(params),
+            param_idents,
             formula,
         }
     }

src/analyze/basic_block.rs

@@ -9,7 +9,7 @@ use rustc_middle::mir::{
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 use rustc_span::def_id::{DefId, LocalDefId};
 
-use crate::analyze;
+use crate::analyze::{self, annot_fn::FormulaFn};
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{
@@ -968,6 +968,105 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
     }
 
+    /// The formula function a ghost marker call carries, or `None` for any other call.
+    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))
+    }
+
+    /// Forges an operand for a live variable named `name` using var_debug_info
+    ///
+    /// Shadowing can leave several entries sharing a name, and debug info does not say
+    /// which one the source that named it meant, so this refuses to guess.
+    fn operand_of_name(&self, name: rustc_span::Symbol) -> Option<Operand<'tcx>> {
+        let mut found: Option<Operand<'tcx>> = None;
+        for vdi in self
+            .body
+            .var_debug_info
+            .iter()
+            .filter(|vdi| vdi.name == name)
+        {
+            let operand = match &vdi.value {
+                mir::VarDebugInfoContents::Place(place) => {
+                    if !place.projection.is_empty() || !self.is_defined(place.local) {
+                        continue;
+                    }
+                    Operand::Copy(*place)
+                }
+                mir::VarDebugInfoContents::Const(constant) => {
+                    Operand::Constant(Box::new(*constant))
+                }
+            };
+            match &found {
+                None => found = Some(operand),
+                Some(prev) if *prev == operand => {}
+                Some(_) => self.tcx.dcx().fatal(format!(
+                    "ghost term refers to `{name}`, which is ambiguous here: multiple live \
+                     variables share this name (e.g. through shadowing). Rename the variables \
+                     to disambiguate."
+                )),
+            }
+        }
+
+        found
+    }
+
+    /// Types the introduction of a ghost value as a call to the function the ghost term
+    /// denotes: one from the live variables it names to a value refined by the term.
+    fn type_ghost_value(&mut self, formula_fn: FormulaFn<'tcx>, expected: &rty::RefinedType<Var>) {
+        let (value_ty, param_tys) = formula_fn
+            .params()
+            .raw
+            .split_first()
+            .expect("ghost formula function takes the ghost value as its first parameter");
+        let mut params: IndexVec<_, _> = param_tys
+            .iter()
+            .map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous())
+            .collect();
+        if params.is_empty() {
+            // elaboration: we need at least one predicate variable in parameter
+            params.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous());
+        }
+        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 args = formula_fn
+            .param_idents()
+            .iter()
+            .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(|| {
+                    self.tcx.dcx().fatal(format!(
+                        "ghost term refers to `{ident}`, which is not a live variable here"
+                    ))
+                });
+                self.operand_refined_type(operand)
+            })
+            .collect();
+
+        let clauses = self.relate_fn_sub_type(func_ty, args, expected.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 +1327,19 @@ 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) {
+                let formula_fn = self
+                    .ctx
+                    .formula_fn_with_args(formula_def_id, generic_args)
+                    .expect("ghost formula function is not registered");
+                self.type_ghost_value(formula_fn, &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/analyze/local_def.rs

@@ -836,15 +836,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             .ctx
             .formula_fn_with_args(formula_def_id, generic_args)
             .expect("invariant formula function is not registered");
-        let idents = self.tcx.fn_arg_idents(formula_def_id.to_def_id());
+        let idents = formula_fn.param_idents();
         let sig = self
             .tcx
             .fn_sig(formula_def_id.to_def_id())
             .instantiate(self.tcx, generic_args);
 
         let mut mapping: Vec<rty::FunctionParamIdx> = Vec::with_capacity(idents.len());
-        for (ident_opt, input_ty) in idents.iter().zip(sig.skip_binder().inputs()) {
-            let name = ident_opt.expect("invariant parameters must be named").name;
+        for (ident, input_ty) in idents.iter().zip(sig.skip_binder().inputs()) {
+            let ident = ident.expect("invariant parameters must be named");
             let input_ty = {
                 let typing_env =
                     mir_ty::TypingEnv::post_analysis(self.tcx, formula_def_id.to_def_id());
@@ -855,10 +855,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
             // 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 name.as_str() == "__thrust_self" {
+            let name = if ident.name.as_str() == "__thrust_self" {
                 rustc_span::Symbol::intern("self")
             } else {
-                name
+                ident.name
             };
 
             if input_ty

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());
 
+        // Refinements live on MIR locals, and `RemoveZsts` rewrites reads of zero-sized
+        // locals into constants, losing 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,32 @@ mod thrust_models {
         unimplemented!()
     }
 
+    /// Proof-only data, introduced by `thrust_macros::ghost!`. In the logic it is its
+    /// content, so a specification refers to a `Ghost<T>` as if it were a `T`.
+    #[allow(dead_code)]
+    pub struct Ghost<T: ?Sized>(std::marker::PhantomData<T>);
+
+    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;
+    }
+
+    #[doc(hidden)]
+    #[thrust::def::ghost_marker]
+    #[thrust::ignored]
+    #[inline(never)]
+    pub fn __ghost_marker<F, T: ?Sized>(_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_const.rs

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

tests/ui/fail/ghost_field.rs

@@ -0,0 +1,23 @@
+//@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::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_const.rs

@@ -0,0 +1,15 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+use thrust_models::model::{Int, Seq};
+use thrust_models::Ghost;
+
+#[thrust_macros::requires(s.len() == 0)]
+fn expect_empty(s: Ghost<Seq<Int>>) {
+    let _ = s;
+}
+
+fn main() {
+    let s = thrust_macros::ghost!(|| -> Seq<Int> { Seq::empty() });
+    expect_empty(s);
+}

tests/ui/pass/ghost_field.rs

@@ -0,0 +1,23 @@
+//@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::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() {}