Add a ghost! block for ghost code with ownership

creusot-contracts-dummy/src/lib.rs

@@ -33,6 +33,11 @@ pub fn snapshot(_: TS1) -> TS1 {
         .into()
 }
 
+#[proc_macro]
+pub fn ghost(_: TS1) -> TS1 {
+    quote::quote! { creusot_contracts::ghost::Ghost::from_fn(|| std::process::abort()) }.into()
+}
+
 #[proc_macro_attribute]
 pub fn logic(_: TS1, _: TS1) -> TS1 {
     TS1::new()

creusot-contracts-proc/src/lib.rs

@@ -421,6 +421,18 @@ pub fn snapshot(assertion: TS1) -> TS1 {
     })
 }
 
+#[proc_macro]
+pub fn ghost(body: TS1) -> TS1 {
+    let body = proc_macro2::TokenStream::from(body);
+    TS1::from(quote! {
+        {
+            ::creusot_contracts::__stubs::ghost_from_fn({
+                #[creusot::spec::ghost] || { #body }
+            })
+        }
+    })
+}
+
 struct LogicItem {
     vis: Visibility,
     defaultness: Option<Token![default]>,

creusot-contracts/src/ghost.rs

@@ -0,0 +1,32 @@
+use crate::*;
+
+// FIXME: better doc
+/// Any item that implements `Ghost` must **not** be able to break the ownership rules,
+/// be it in ghost or runtime code.
+///
+/// Additionnaly, it should be zero-sized, so that it's not possible to extract
+/// information from a ghost bloc and use it in normal code.
+#[rustc_diagnostic_item = "ghost_trait"]
+#[trusted]
+pub trait Ghost {}
+
+macro_rules! impl_ghost_tuple {
+    ($($ty_param:ident),*) => {
+        impl_ghost_tuple!{ @inner $($ty_param,)* || []; }
+    };
+    (@inner $ty_param:ident, $($rest:ident,)* || $( [ $($done:ident,)* ] ;)*) => {
+        impl_ghost_tuple! {
+            @inner $($rest,)* ||
+            [] ; $( [ $ty_param, $($done,)* ] ;)*
+        }
+    };
+    (@inner || $( [ $($done:ident,)* ] ;)*) => {
+        $(
+            impl<$($done : Ghost),*> Ghost for ($($done,)*) {}
+        )*
+    };
+}
+
+impl_ghost_tuple! { T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12 }
+
+impl<T> Ghost for Snapshot<T> {}

creusot-contracts/src/lib.rs

@@ -20,7 +20,7 @@ mod macros {
     /// A post-condition of a function or trait item
     pub use creusot_contracts_proc::ensures;
 
-    pub use creusot_contracts_proc::snapshot;
+    pub use creusot_contracts_proc::{ghost, snapshot};
 
     /// A loop invariant
     /// The first argument should be a name for the invariant
@@ -118,7 +118,7 @@ mod macros {
     /// A post-condition of a function or trait item
     pub use creusot_contracts_dummy::ensures;
 
-    pub use creusot_contracts_dummy::snapshot;
+    pub use creusot_contracts_dummy::{ghost, snapshot};
 
     /// A loop invariant
     /// The first argument should be a name for the invariant
@@ -220,9 +220,17 @@ pub mod std;
 #[cfg(creusot)]
 pub mod num_rational;
 
+#[cfg(creusot)]
+pub mod ghost;
+
 #[cfg(creusot)]
 pub mod snapshot;
 
+#[cfg(not(creusot))]
+pub mod ghost {
+    pub trait Ghost: std::ops::Deref {}
+}
+
 #[cfg(not(creusot))]
 pub mod snapshot {
     pub struct Snapshot<T>(std::marker::PhantomData<T>)
@@ -253,6 +261,7 @@ pub mod well_founded;
 
 // We add some common things at the root of the creusot-contracts library
 pub use crate::{
+    ghost::Ghost,
     logic::{IndexLogic as _, Int, OrdLogic, Seq},
     macros::*,
     model::{DeepModel, ShallowModel},

creusot-contracts/src/stubs.rs

@@ -63,6 +63,11 @@ pub fn snapshot_from_fn<T: ?Sized, F: Fn() -> crate::Snapshot<T>>(_: F) -> crate
     panic!()
 }
 
+#[rustc_diagnostic_item = "ghost_from_fn"]
+pub fn ghost_from_fn<T: crate::Ghost, F: FnOnce() -> T>(_: F) -> T {
+    panic!()
+}
+
 #[creusot::no_translate]
 #[creusot::builtins = "prelude.Mapping.from_fn"]
 pub fn mapping_from_fn<A, B, F: FnOnce(A) -> B>(_: F) -> crate::logic::Mapping<A, B> {

creusot/src/gather_spec_closures.rs

@@ -1,10 +1,9 @@
-use indexmap::{IndexMap, IndexSet};
-
 use crate::{
     ctx::TranslationCtx,
     pearlite::Term,
     util::{self, snapshot_closure_id},
 };
+use indexmap::{IndexMap, IndexSet};
 use rustc_data_structures::graph::WithSuccessors;
 use rustc_hir::def_id::DefId;
 use rustc_middle::{
@@ -24,6 +23,8 @@ pub(crate) struct SpecClosures<'tcx> {
     pub(crate) assertions: IndexMap<DefId, Term<'tcx>>,
     /// Closures generated by `snapshot!`
     pub(crate) snapshots: IndexMap<DefId, Term<'tcx>>,
+    /// Closures generated by `ghost!`
+    pub(crate) ghosts: IndexSet<DefId>,
 }
 
 impl<'tcx> SpecClosures<'tcx> {
@@ -33,16 +34,19 @@ impl<'tcx> SpecClosures<'tcx> {
 
         let mut assertions = IndexMap::new();
         let mut snapshots = IndexMap::new();
+        let mut ghosts = IndexSet::new();
         for clos in visitor.closures.into_iter() {
             if util::is_assertion(ctx.tcx, clos) {
                 let term = ctx.term(clos).unwrap().clone();
                 assertions.insert(clos, term);
             } else if util::is_snapshot_closure(ctx.tcx, clos) {
                 let term = ctx.term(clos).unwrap().clone();
                 snapshots.insert(clos, term);
+            } else if util::is_ghost_closure(ctx.tcx, clos) {
+                ghosts.insert(clos);
             }
         }
-        Self { assertions, snapshots }
+        Self { assertions, snapshots, ghosts }
     }
 }
 

creusot/src/translation/fmir.rs

@@ -222,8 +222,6 @@ pub type LocalDecls<'tcx> = IndexMap<Symbol, LocalDecl<'tcx>>;
 
 #[derive(Clone, Debug)]
 pub struct LocalDecl<'tcx> {
-    // Original MIR local
-    pub(crate) mir_local: Local,
     pub(crate) span: Span,
     pub(crate) ty: Ty<'tcx>,
     // Is this a MIR temporary?