Merge branch 'master' into update-coma

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 `Ghost<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

@@ -28,8 +28,9 @@ pub fn proof_assert(_: TS1) -> TS1 {
 }
 
 #[proc_macro]
-pub fn gh(_: TS1) -> TS1 {
-    quote::quote! { creusot_contracts::ghost::Ghost::from_fn(|| std::process::abort()) }.into()
+pub fn snapshot(_: TS1) -> TS1 {
+    quote::quote! { creusot_contracts::snapshot::Snapshot::from_fn(|| std::process::abort()) }
+        .into()
 }
 
 #[proc_macro_attribute]
@@ -42,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/invariant.rs

@@ -144,16 +144,16 @@ fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
 
     quote! { {
         let mut #it = ::std::iter::IntoIterator::into_iter(#iter);
-        let #iter_old = gh! { #it };
-        let mut #produced = gh! { ::creusot_contracts::logic::Seq::EMPTY };
+        let #iter_old = snapshot! { #it };
+        let mut #produced = snapshot! { ::creusot_contracts::logic::Seq::EMPTY };
         #(#invariants;)*
         #(#outer)*
         #lbl
         loop {
             #(#inner)*
             match ::std::iter::Iterator::next(&mut #it) {
                 Some(#elem) => {
-                    #produced = gh! { #produced.inner().concat(::creusot_contracts::logic::Seq::singleton(#elem)) };
+                    #produced = snapshot! { #produced.inner().concat(::creusot_contracts::logic::Seq::singleton(#elem)) };
                     let #pat = #elem;
                     #body
                 },

creusot-contracts-proc/src/lib.rs

@@ -405,17 +405,17 @@ pub fn proof_assert(assertion: TS1) -> TS1 {
 }
 
 #[proc_macro]
-pub fn gh(assertion: TS1) -> TS1 {
+pub fn snapshot(assertion: TS1) -> TS1 {
     let assert = parse_macro_input!(assertion as Assertion);
     let assert_body = pretyping::encode_block(&assert.0).unwrap();
 
     TS1::from(quote! {
         {
-            ::creusot_contracts::__stubs::ghost_from_fn(
+            ::creusot_contracts::__stubs::snapshot_from_fn(
                 #[creusot::no_translate]
                 #[creusot::spec]
-                #[creusot::spec::ghost]
-                || { ::creusot_contracts::ghost::Ghost::new (#assert_body) }
+                #[creusot::spec::snapshot]
+                || { ::creusot_contracts::snapshot::Snapshot::new (#assert_body) }
             )
         }
     })
@@ -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