rename ghost, logic and predicate functions

`#[ghost]` -> `#[logic]`
`#[logic]` -> `#[logic(prophetic)]`
`#[predicate]` -> `#[predicate]` and `#[predicate(prophetic)]`

ARCHITECTURE.md

@@ -151,7 +151,7 @@ Instead, we replace the `discriminant` / `switchInt` pair with a match directly
 
 ## Logical functions
 
-Logical functions are created by `#[ghost]`, `#[logic]`, or `#[predicate]`.
+Logical functions are created by `#[logic]` or `#[predicate]`.
 
 ## Specifications
 

README.md

@@ -152,15 +152,14 @@ Contracts and logic functions are written in Pearlite, a specification language
 - Logical Expressions: quantifiers (`forall` and `exists`), logical implication `==>`, *logical* equality `a == b`, labels
 - Rust specific logical expressions: access to the **final** value of a mutable reference `^`, access to the *model* of an object `@`
 
-We also provide three new attributes on Rust functions: `ghost`, `logic` and `predicate`.
-
-A ghost function is marked with `#[ghost]`. It can be used in ghost code, to assign ghost
-variables of the `Snapshot<T>` type.
+We also provide two new attributes on Rust functions: `logic` and `predicate`.
 
 Marked  `#[logic]` or `#[predicate]`, a function can be used in specs and other logical conditions (`requires`/`ensures` and `invariant`). They can use ghost functions.
 The two attributes have the following difference.
 - A `logic` function can freely have logical, non-executable operations, such as quantifiers, logic equalities, etc. Instead, this function can't be called in normal Rust code (the function body of a `logic` function is replaced with a panic).
   You can use pearlite syntax for any part in the logic function by marking that part with the `pearlite! { ... }` macro.
+
+  If you need to use the prophecy operator `^` on a mutable reference, you need to mark the function `#[logic(prophetic)]`.
 - A `predicate` is a logical function which returns a proposition (in practice, returns a boolean value).
 
 When you write *recursive* `ghost`, `logic` or `predicate` functions, you have to show that the function terminates.

creusot-contracts-dummy/src/lib.rs

@@ -43,11 +43,6 @@ pub fn pearlite(_: TS1) -> TS1 {
     TS1::new()
 }
 
-#[proc_macro_attribute]
-pub fn ghost(_: TS1, _: TS1) -> TS1 {
-    TS1::new()
-}
-
 #[proc_macro_attribute]
 pub fn predicate(_: TS1, _: TS1) -> TS1 {
     TS1::new()

creusot-contracts-proc/src/derive/deep_model.rs

@@ -47,7 +47,7 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
         impl #impl_generics ::creusot_contracts::DeepModel for #name #ty_generics #where_clause {
             type DeepModelTy = #deep_model_ty_name #ty_generics;
 
-            #[ghost]
+            #[logic]
             #open
             fn deep_model(self) -> Self::DeepModelTy {
                 #eq

creusot-contracts-proc/src/derive/resolve.rs

@@ -14,7 +14,7 @@ pub fn derive_resolve(input: proc_macro::TokenStream) -> proc_macro::TokenStream
     let expanded = quote! {
         #[::creusot_contracts::trusted]
         impl #impl_generics ::creusot_contracts::Resolve for #name #ty_generics #where_clause {
-            #[::creusot_contracts::predicate]
+            #[::creusot_contracts::predicate(prophetic)]
             #[::creusot_contracts::open]
             fn resolve(self) -> bool {
                 use ::creusot_contracts::Resolve;

creusot-contracts-proc/src/lib.rs

@@ -467,59 +467,35 @@ impl Parse for LogicInput {
 }
 
 #[proc_macro_attribute]
-pub fn ghost(_: TS1, tokens: TS1) -> TS1 {
-    let log = parse_macro_input!(tokens as LogicInput);
-    match log {
-        LogicInput::Item(log) => ghost_item(log),
-        LogicInput::Sig(sig) => ghost_sig(sig),
-    }
-}
-
-fn ghost_sig(sig: TraitItemSignature) -> TS1 {
-    let span = sig.span();
-    TS1::from(quote_spanned! {span=>
-        #[creusot::decl::ghost]
-        #sig
-    })
-}
-
-fn ghost_item(log: LogicItem) -> TS1 {
-    let span = log.sig.span();
-
-    let term = log.body;
-    let vis = log.vis;
-    let def = log.defaultness;
-    let sig = log.sig;
-    let attrs = log.attrs;
-    let req_body = pretyping::encode_block(&term.stmts).unwrap();
-
-    TS1::from(quote_spanned! {span=>
-        #[creusot::decl::ghost]
-        #(#attrs)*
-        #vis #def #sig {
-            #req_body
+pub fn logic(prophetic: TS1, tokens: TS1) -> TS1 {
+    let prophetic = if prophetic.is_empty() {
+        None
+    } else {
+        let t = parse_macro_input!(prophetic as Ident);
+        if t.to_string() == "prophetic" {
+            Some(quote!(#[creusot::decl::logic::prophetic]))
+        } else {
+            None
         }
-    })
-}
-
-#[proc_macro_attribute]
-pub fn logic(_: TS1, tokens: TS1) -> TS1 {
+    };
     let log = parse_macro_input!(tokens as LogicInput);
     match log {
-        LogicInput::Item(log) => logic_item(log),
-        LogicInput::Sig(sig) => logic_sig(sig),
+        LogicInput::Item(log) => logic_item(log, prophetic),
+        LogicInput::Sig(sig) => logic_sig(sig, prophetic),
     }
 }
 
-fn logic_sig(sig: TraitItemSignature) -> TS1 {
+fn logic_sig(sig: TraitItemSignature, prophetic: Option<TokenStream>) -> TS1 {
     let span = sig.span();
-    TS1::from(quote_spanned! {span=>
+
+    TS1::from(quote_spanned! {span =>
         #[creusot::decl::logic]
+        #prophetic
         #sig
     })
 }
 
-fn logic_item(log: LogicItem) -> TS1 {
+fn logic_item(log: LogicItem, prophetic: Option<TokenStream>) -> TS1 {
     let span = log.sig.span();
 
     let term = log.body;
@@ -529,8 +505,9 @@ fn logic_item(log: LogicItem) -> TS1 {
     let attrs = log.attrs;
     let req_body = pretyping::encode_block(&term.stmts).unwrap();
 
-    TS1::from(quote_spanned! {span=>
+    TS1::from(quote_spanned! {span =>
         #[creusot::decl::logic]
+        #prophetic
         #(#attrs)*
         #vis #def #sig {
             #req_body
@@ -550,7 +527,18 @@ pub fn law(_: TS1, tokens: TS1) -> TS1 {
 }
 
 #[proc_macro_attribute]
-pub fn predicate(_: TS1, tokens: TS1) -> TS1 {
+pub fn predicate(prophetic: TS1, tokens: TS1) -> TS1 {
+    let prophetic = if prophetic.is_empty() {
+        None
+    } else {
+        let t = parse_macro_input!(prophetic as Ident);
+        if t.to_string() == "prophetic" {
+            Some(quote!(#[creusot::decl::logic::prophetic]))
+        } else {
+            None
+        }
+    };
+
     let pred = parse_macro_input!(tokens as LogicInput);
 
     let sig = match &pred {
@@ -573,20 +561,21 @@ pub fn predicate(_: TS1, tokens: TS1) -> TS1 {
     };
 
     match pred {
-        LogicInput::Item(log) => predicate_item(log),
-        LogicInput::Sig(sig) => predicate_sig(sig),
+        LogicInput::Item(log) => predicate_item(log, prophetic),
+        LogicInput::Sig(sig) => predicate_sig(sig, prophetic),
     }
 }
 
-fn predicate_sig(sig: TraitItemSignature) -> TS1 {
+fn predicate_sig(sig: TraitItemSignature, prophetic: Option<TokenStream>) -> TS1 {
     let span = sig.span();
     TS1::from(quote_spanned! {span=>
         #[creusot::decl::predicate]
+        #prophetic
         #sig
     })
 }
 
-fn predicate_item(log: LogicItem) -> TS1 {
+fn predicate_item(log: LogicItem, prophetic: Option<TokenStream>) -> TS1 {
     let span = log.sig.span();
     let term = log.body;
     let vis = log.vis;
@@ -598,6 +587,7 @@ fn predicate_item(log: LogicItem) -> TS1 {
 
     TS1::from(quote_spanned! {span=>
         #[creusot::decl::predicate]
+        #prophetic
         #(#attrs)*
         #vis #def #sig {
             #req_body

creusot-contracts/src/ghost_ptr.rs

@@ -29,7 +29,7 @@ impl<T: ?Sized> ShallowModel for GhostPtrToken<T> {
     type ShallowModelTy = FMap<GhostPtr<T>, T>;
 
     #[trusted]
-    #[ghost]
+    #[logic]
     #[open(self)]
     fn shallow_model(self) -> Self::ShallowModelTy {
         absurd
@@ -131,7 +131,7 @@ impl<T: ?Sized> GhostPtrToken<T> {
 impl<T: ?Sized> GhostPtrExt<T> for GhostPtr<T> {
     #[trusted]
     #[open(self)]
-    #[ghost]
+    #[logic]
     #[ensures(forall<t: GhostPtrToken<T>> !t@.contains(result))]
     #[ensures(result.addr_logic() == 0)]
     #[ensures(forall<ptr: GhostPtr<T>> ptr.addr_logic() == result.addr_logic() ==> ptr == result)]
@@ -140,7 +140,7 @@ impl<T: ?Sized> GhostPtrExt<T> for GhostPtr<T> {
     }
 
     #[trusted]
-    #[ghost]
+    #[logic]
     #[open(self)]
     fn addr_logic(self) -> Int {
         absurd
@@ -151,7 +151,7 @@ impl<'a, T: ?Sized> ShallowModel for GhostPtrTokenRef<'a, T> {
     type ShallowModelTy = FMap<GhostPtr<T>, T>;
 
     #[trusted]
-    #[ghost]
+    #[logic]
     #[open(self)]
     fn shallow_model(self) -> Self::ShallowModelTy {
         absurd
@@ -174,14 +174,14 @@ impl<'a, T: ?Sized> GhostPtrTokenRef<'a, T> {
     #[requires(new_model.subset(self@))]
     #[ensures(result@ == *new_model)]
     #[allow(unused_variables)]
-    pub fn shrink_token_ref(self, new_model: Ghost<FMap<*const T, T>>) -> Self {
+    pub fn shrink_token_ref(self, new_model: Snapshot<FMap<*const T, T>>) -> Self {
         self
     }
 }
 
 impl<'a, T: ?Sized> GhostPtrTokenMut<'a, T> {
     #[trusted]
-    #[ghost]
+    #[logic]
     #[open(self)]
     pub fn cur(self) -> FMap<GhostPtr<T>, T> {
         absurd
@@ -265,9 +265,9 @@ impl<'a, T> Resolve for GhostPtrTokenMut<'a, T> {
 }
 
 pub trait GhostPtrExt<T: ?Sized>: Sized {
-    #[ghost]
+    #[logic]
     fn null_logic() -> Self;
-    #[ghost]
+    #[logic]
     fn addr_logic(self) -> Int;
 }
 

creusot-contracts/src/invariant.rs

@@ -1,7 +1,7 @@
 use crate::*;
 
 pub trait Invariant {
-    #[predicate]
+    #[predicate(prophetic)]
     #[open]
     #[rustc_diagnostic_item = "creusot_invariant_user"]
     fn invariant(self) -> bool {

creusot-contracts/src/lib.rs

@@ -32,20 +32,41 @@ mod macros {
     pub use creusot_contracts_proc::law;
 
     /// Declare a function as being a logical function, this declaration must be pure and
-    /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [pearlite] macro.
+    /// total. It cannot be called from Rust programs, but in exchange it can use logical
+    /// operations and syntax with the help of the [`pearlite!`] macro.
+    ///
+    /// # `prophetic`
+    ///
+    /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to
+    /// specify that the function is _prophetic_, like so:
+    /// ```ignore
+    /// #[logic(prophetic)]
+    /// fn uses_prophecies(x: &mut Int) -> Int {
+    ///     pearlite! { if ^x == 0 { 0 } else { 1 } }
+    /// }
+    /// ```
+    /// Such a logic function cannot be used in [`snapshot!`] anymore, and cannot be
+    /// called from a regular [`logic`] or [`predicate`] function.
     pub use creusot_contracts_proc::logic;
 
-    /// Declare a function as being a ghost function, this declaration must be pure and
-    /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [pearlite] macro.
-    /// Unlike functions marked with the `[logic]` attribute, `[ghost]` functions cannot
-    /// use the final value operator (^), nor call other `[predicate]` or `[logic]` functions.
-    pub use creusot_contracts_proc::ghost;
-
     /// Declare a function as being a logical function, this declaration must be pure and
     /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [pearlite] macro.
+    /// use logical operations and syntax with the help of the [`pearlite!`] macro.
+    ///
+    /// It **must** return a boolean.
+    ///
+    /// # `prophetic`
+    ///
+    /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to
+    /// specify that the function is _prophetic_, like so:
+    /// ```ignore
+    /// #[predicate(prophetic)]
+    /// fn uses_prophecies(x: &mut Int) -> bool {
+    ///     pearlite! { ^x == 0 }
+    /// }
+    /// ```
+    /// Such a predicate function cannot be used in [`snapshot!`] anymore, and cannot be
+    /// called from a regular [`logic`] or [`predicate`] function.
     pub use creusot_contracts_proc::predicate;
 
     /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime
@@ -109,20 +130,41 @@ mod macros {
     pub use creusot_contracts_dummy::law;
 
     /// Declare a function as being a logical function, this declaration must be pure and
-    /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [pearlite] macro.
+    /// total. It cannot be called from Rust programs, but in exchange it can use logical
+    /// operations and syntax with the help of the [`pearlite!`] macro.
+    ///
+    /// # `prophetic`
+    ///
+    /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to
+    /// specify that the function is _prophetic_, like so:
+    /// ```ignore
+    /// #[logic(prophetic)]
+    /// fn uses_prophecies(x: &mut Int) -> Int {
+    ///     pearlite! { if ^x == 0 { 0 } else { 1 } }
+    /// }
+    /// ```
+    /// Such a logic function cannot be used in [`snapshot!`] anymore, and cannot be
+    /// called from a regular [`logic`] or [`predicate`] function.
     pub use creusot_contracts_dummy::logic;
 
-    /// Declare a function as being a ghost function, this declaration must be pure and
-    /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [pearlite] macro.
-    /// Unlike functions marked with the `[logic]` attribute, `[ghost]` functions cannot
-    /// use the final value operator (^), nor call other `[predicate]` or `[logic]` functions.
-    pub use creusot_contracts_dummy::ghost;
-
     /// Declare a function as being a logical function, this declaration must be pure and
     /// total. It cannot be called from Rust programs as it is *ghost*, in exchange it can
-    /// use logical operations and syntax with the help of the [pearlite] macro.
+    /// use logical operations and syntax with the help of the [`pearlite!`] macro.
+    ///
+    /// It **must** return a boolean.
+    ///
+    /// # `prophetic`
+    ///
+    /// If you wish to use the `^` operator on mutable borrows to get the final value, you need to
+    /// specify that the function is _prophetic_, like so:
+    /// ```ignore
+    /// #[predicate(prophetic)]
+    /// fn uses_prophecies(x: &mut Int) -> bool {
+    ///     pearlite! { ^x == 0 }
+    /// }
+    /// ```
+    /// Such a predicate function cannot be used in [`snapshot!`] anymore, and cannot be
+    /// called from a regular [`logic`] or [`predicate`] function.
     pub use creusot_contracts_dummy::predicate;
 
     /// Inserts a *logical* assertion into the code. This assertion will not be checked at runtime