Update tests

creusot/tests/should_fail/bad_law.stderr

@@ -4,8 +4,7 @@ error[creusot]: Laws cannot have additional generic parameters
 6 |     fn my_law<T>(x: T);
   |     ^^^^^^^^^^^^^^^^^^^
 
-Logic != Program
-error[creusot]: Expected `my_law` to be a program function as specified by the trait declaration
+error[creusot]: Expected `my_law` to be a logic function as specified by the trait declaration
   --> bad_law.rs:10:5
    |
 10 |     fn my_law<T>(_: T) {}

creusot/tests/should_fail/bug/222.rs

@@ -3,7 +3,7 @@ extern crate creusot_contracts;
 use creusot_contracts::{logic::Int, *};
 
 trait A {
-    #[ghost]
+    #[logic]
     fn mktrue() -> Int {
         pearlite! { 5 }
     }
@@ -17,7 +17,7 @@ trait A {
 }
 
 impl A for () {
-    #[ghost]
+    #[logic]
     fn mktrue() -> Int {
         pearlite! { 6 }
     }

creusot/tests/should_fail/bug/436_0.rs

@@ -2,16 +2,16 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 struct S {
-    g: Ghost<i32>,
+    g: Snapshot<i32>,
 }
 
-#[ghost]
+#[logic(prophetic)]
 fn prophecy(x: &mut S) -> i32 {
     pearlite! { *(^x).g }
 }
 
 pub fn f() {
-    let b = &mut S { g: gh! { 1i32 } };
-    b.g = gh! { prophecy(b) + 1i32 };
+    let b = &mut S { g: snapshot! { 1i32 } };
+    b.g = snapshot! { prophecy(b) + 1i32 };
     proof_assert! { false }
 }

creusot/tests/should_fail/bug/436_0.stderr

@@ -1,10 +1,8 @@
-error[creusot]: called Logic function in Ghost context "creusot_contracts::__stubs::fin"
-  --> 436_0.rs:10:5
+error[creusot]: called prophetic logic function "prophecy" in logic context
+  --> 436_0.rs:15:23
    |
-10 |     pearlite! { *(^x).g }
-   |     ^^^^^^^^^^^^^^^^^^^^^
-   |
-   = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)
+15 |     b.g = snapshot! { prophecy(b) + 1i32 };
+   |                       ^^^^^^^^
 
 error: aborting due to previous error
 

creusot/tests/should_fail/bug/436_1.rs

@@ -2,7 +2,7 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 struct S {
-    g: Ghost<bool>,
+    g: Snapshot<bool>,
 }
 
 #[predicate]
@@ -11,7 +11,7 @@ fn prophecy(x: &mut S) -> bool {
 }
 
 pub fn f() {
-    let b = &mut S { g: gh! { true } };
-    b.g = gh! { !prophecy(b) };
+    let b = &mut S { g: snapshot! { true } };
+    b.g = snapshot! { !prophecy(b) };
     proof_assert! { false }
 }

creusot/tests/should_fail/bug/436_1.stderr

@@ -1,8 +1,10 @@
-error[creusot]: called Logic function in Ghost context "prophecy"
-  --> 436_1.rs:15:18
+error[creusot]: called prophetic logic function "creusot_contracts::__stubs::fin" in logic context
+  --> 436_1.rs:10:5
    |
-15 |     b.g = gh! { !prophecy(b) };
-   |                  ^^^^^^^^
+10 |     pearlite! { *(^x).g }
+   |     ^^^^^^^^^^^^^^^^^^^^^
+   |
+   = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)
 
 error: aborting due to previous error
 

creusot/tests/should_fail/bug/436_2.rs

@@ -3,13 +3,13 @@ use creusot_contracts::*;
 
 enum Bad<'a> {
     None,
-    Some(Ghost<&'a mut Bad<'a>>),
+    Some(Snapshot<&'a mut Bad<'a>>),
 }
 
 pub fn test_bad() {
     let mut x = Bad::None;
     let m = &mut x;
-    let g = gh!(m);
+    let g = snapshot!(m);
     *m = Bad::Some(g);
     proof_assert!(*m == Bad::Some(g));
     proof_assert!(^*g == ^m);

creusot/tests/should_fail/bug/436_2.stderr

@@ -1,8 +1,8 @@
-error[creusot]: Illegal use of the Ghost type
+error[creusot]: Illegal use of the Snapshot type
  --> 436_2.rs:6:10
   |
-6 |     Some(Ghost<&'a mut Bad<'a>>),
-  |          ^^^^^^^^^^^^^^^^^^^^^^
+6 |     Some(Snapshot<&'a mut Bad<'a>>),
+  |          ^^^^^^^^^^^^^^^^^^^^^^^^^
 
 error: aborting due to previous error
 

creusot/tests/should_fail/bug/869.mlcfg

@@ -1,72 +1,72 @@
 
 module C869_Unsound
-  use prelude.Ghost
+  use prelude.Snapshot
   use prelude.Borrow
-  use prelude.Ghost
-  use prelude.Ghost
-  use prelude.Ghost
-  predicate resolve0 (self : borrowed (Ghost.ghost_ty bool)) =
+  use prelude.Snapshot
+  use prelude.Snapshot
+  use prelude.Snapshot
+  predicate resolve0 (self : borrowed (Snapshot.snap_ty bool)) =
     [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34]  ^ self =  * self
-  val resolve0 (self : borrowed (Ghost.ghost_ty bool)) : bool
+  val resolve0 (self : borrowed (Snapshot.snap_ty bool)) : bool
     ensures { result = resolve0 self }
 
-  use prelude.Ghost
+  use prelude.Snapshot
   let rec cfg unsound [#"../869.rs" 4 0 4 16] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : ()
    = [@vc:do_not_keep_trace] [@vc:sp]
   var _0 : ();
-  var x : Ghost.ghost_ty bool;
-  var xm : borrowed (Ghost.ghost_ty bool);
-  var _4 : borrowed (Ghost.ghost_ty bool);
-  var b : borrowed (Ghost.ghost_ty bool);
-  var _6 : borrowed (Ghost.ghost_ty bool);
-  var bg : Ghost.ghost_ty (borrowed (Ghost.ghost_ty bool));
-  var evil : borrowed (Ghost.ghost_ty bool);
-  var _12 : borrowed (Ghost.ghost_ty bool);
-  var _15 : Ghost.ghost_ty bool;
+  var x : Snapshot.snap_ty bool;
+  var xm : borrowed (Snapshot.snap_ty bool);
+  var _4 : borrowed (Snapshot.snap_ty bool);
+  var b : borrowed (Snapshot.snap_ty bool);
+  var _6 : borrowed (Snapshot.snap_ty bool);
+  var bg : Snapshot.snap_ty (borrowed (Snapshot.snap_ty bool));
+  var evil : borrowed (Snapshot.snap_ty bool);
+  var _12 : borrowed (Snapshot.snap_ty bool);
+  var _15 : Snapshot.snap_ty bool;
   {
     goto BB0
   }
   BB0 {
-    [#"../869.rs" 5 29 5 41] x <- ([#"../869.rs" 5 29 5 41] Ghost.new true);
+    [#"../869.rs" 5 32 5 50] x <- ([#"../869.rs" 5 32 5 50] Snapshot.new true);
     goto BB1
   }
   BB1 {
-    [#"../869.rs" 7 31 7 37] _4 <- Borrow.borrow_mut x;
-    [#"../869.rs" 7 31 7 37] x <-  ^ _4;
-    [#"../869.rs" 7 31 7 37] xm <- Borrow.borrow_final ( * _4) (Borrow.get_id _4);
-    [#"../869.rs" 7 31 7 37] _4 <- { _4 with current = ( ^ xm) ; };
+    [#"../869.rs" 7 34 7 40] _4 <- Borrow.borrow_mut x;
+    [#"../869.rs" 7 34 7 40] x <-  ^ _4;
+    [#"../869.rs" 7 34 7 40] xm <- Borrow.borrow_final ( * _4) (Borrow.get_id _4);
+    [#"../869.rs" 7 34 7 40] _4 <- { _4 with current = ( ^ xm) ; };
     assume { resolve0 _4 };
-    [#"../869.rs" 9 30 9 38] _6 <- Borrow.borrow_mut ( * xm);
-    [#"../869.rs" 9 30 9 38] xm <- { xm with current = ( ^ _6) ; };
-    [#"../869.rs" 9 30 9 38] b <- Borrow.borrow_final ( * _6) (Borrow.get_id _6);
-    [#"../869.rs" 9 30 9 38] _6 <- { _6 with current = ( ^ b) ; };
+    [#"../869.rs" 9 33 9 41] _6 <- Borrow.borrow_mut ( * xm);
+    [#"../869.rs" 9 33 9 41] xm <- { xm with current = ( ^ _6) ; };
+    [#"../869.rs" 9 33 9 41] b <- Borrow.borrow_final ( * _6) (Borrow.get_id _6);
+    [#"../869.rs" 9 33 9 41] _6 <- { _6 with current = ( ^ b) ; };
     assume { resolve0 b };
     assume { resolve0 _6 };
-    [#"../869.rs" 10 38 10 47] bg <- ([#"../869.rs" 10 38 10 47] Ghost.new b);
+    [#"../869.rs" 10 44 10 59] bg <- ([#"../869.rs" 10 44 10 59] Snapshot.new b);
     goto BB2
   }
   BB2 {
-    assert { [@expl:assertion] [#"../869.rs" 11 20 11 50] Ghost.inner ( * Ghost.inner bg) = true /\ Ghost.inner ( ^ Ghost.inner bg) = true };
-    [#"../869.rs" 13 33 13 41] _12 <- Borrow.borrow_final ( * xm) (Borrow.get_id xm);
-    [#"../869.rs" 13 33 13 41] xm <- { xm with current = ( ^ _12) ; };
-    [#"../869.rs" 13 33 13 41] evil <- Borrow.borrow_final ( * _12) (Borrow.get_id _12);
-    [#"../869.rs" 13 33 13 41] _12 <- { _12 with current = ( ^ evil) ; };
+    assert { [@expl:assertion] [#"../869.rs" 11 20 11 50] Snapshot.inner ( * Snapshot.inner bg) = true /\ Snapshot.inner ( ^ Snapshot.inner bg) = true };
+    [#"../869.rs" 13 36 13 44] _12 <- Borrow.borrow_final ( * xm) (Borrow.get_id xm);
+    [#"../869.rs" 13 36 13 44] xm <- { xm with current = ( ^ _12) ; };
+    [#"../869.rs" 13 36 13 44] evil <- Borrow.borrow_final ( * _12) (Borrow.get_id _12);
+    [#"../869.rs" 13 36 13 44] _12 <- { _12 with current = ( ^ evil) ; };
     assume { resolve0 _12 };
-    assert { [@expl:assertion] [#"../869.rs" 17 20 17 53] (evil = Ghost.inner bg) = (Ghost.inner ( ^ evil) = true) };
-    [#"../869.rs" 18 12 18 58] _15 <- ([#"../869.rs" 18 12 18 58] Ghost.new (if evil = Ghost.inner bg then
+    assert { [@expl:assertion] [#"../869.rs" 17 20 17 53] (evil = Snapshot.inner bg) = (Snapshot.inner ( ^ evil) = true) };
+    [#"../869.rs" 18 12 18 64] _15 <- ([#"../869.rs" 18 12 18 64] Snapshot.new (if evil = Snapshot.inner bg then
       false
     else
       true
     ));
     goto BB3
   }
   BB3 {
-    [#"../869.rs" 18 4 18 58] evil <- { evil with current = ([#"../869.rs" 18 4 18 58] _15) ; };
-    [#"../869.rs" 18 4 18 58] _15 <- any Ghost.ghost_ty bool;
+    [#"../869.rs" 18 4 18 64] evil <- { evil with current = ([#"../869.rs" 18 4 18 64] _15) ; };
+    [#"../869.rs" 18 4 18 64] _15 <- any Snapshot.snap_ty bool;
     assume { resolve0 evil };
     assume { resolve0 xm };
-    assert { [@expl:assertion] [#"../869.rs" 19 20 19 37] Ghost.inner ( * evil) = (not Ghost.inner ( ^ evil)) };
-    assert { [@expl:assertion] [#"../869.rs" 20 20 20 37] Ghost.inner ( * evil) = (not Ghost.inner ( * evil)) };
+    assert { [@expl:assertion] [#"../869.rs" 19 20 19 37] Snapshot.inner ( * evil) = (not Snapshot.inner ( ^ evil)) };
+    assert { [@expl:assertion] [#"../869.rs" 20 20 20 37] Snapshot.inner ( * evil) = (not Snapshot.inner ( * evil)) };
     [#"../869.rs" 4 17 21 1] _0 <- ([#"../869.rs" 4 17 21 1] ());
     return _0
   }

creusot/tests/should_fail/bug/869.rs

@@ -2,20 +2,20 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 pub fn unsound() {
-    let mut x: Ghost<bool> = gh! { true };
+    let mut x: Snapshot<bool> = snapshot! { true };
     //            id(xm)   = i1
-    let xm: &mut Ghost<bool> = &mut x;
+    let xm: &mut Snapshot<bool> = &mut x;
     // Not final: id(b)    = i2
-    let b: &mut Ghost<bool> = &mut *xm;
-    let bg: Ghost<&mut Ghost<bool>> = gh! { b };
+    let b: &mut Snapshot<bool> = &mut *xm;
+    let bg: Snapshot<&mut Snapshot<bool>> = snapshot! { b };
     proof_assert! { ***bg == true && *^*bg == true };
     // Final:     id(evil) = i1
-    let evil: &mut Ghost<bool> = &mut *xm;
+    let evil: &mut Snapshot<bool> = &mut *xm;
     // This proof_assert does not pass !
     // Indeed evil != *bg (because the id do not match), which causes the next line to put `true` inside `*evil`.
     // And thus *^evil == true, disproving the assertion.
     proof_assert! { (evil == *bg) == (*^evil == true) };
-    *evil = gh! { if evil == *bg { false } else { true } };
+    *evil = snapshot! { if evil == *bg { false } else { true } };
     proof_assert! { **evil == !*^evil };
     proof_assert! { **evil == !**evil };
 }

creusot/tests/should_fail/bug/borrowed_ghost.rs

@@ -2,9 +2,9 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 pub fn use_borrowed() {
-    let mut x = gh! { true };
-    let r = &mut x; // x = ?, r = (gh true, x)
-    *r = gh! { !x.inner() }; // r = (gh (not (inner x)), x)
-                             // resolve r: x = gh (not (inner x))
+    let mut x = snapshot! { true };
+    let r = &mut x; // x = ?, r = (snapshot true, x)
+    *r = snapshot! { !x.inner() }; // r = (snapshot (not (inner x)), x)
+                                   // resolve r: x = snapshot (not (inner x))
     proof_assert! { x.inner() == !x.inner() } // UNSOUND!
 }

creusot/tests/should_fail/bug/borrowed_ghost.stderr

@@ -1,10 +1,10 @@
 error[creusot]: Use of borrowed variable x
  --> borrowed_ghost.rs:7:10
   |
-7 |     *r = gh! { !x.inner() }; // r = (gh (not (inner x)), x)
-  |          ^^^^^^^^^^^^^^^^^^
+7 |     *r = snapshot! { !x.inner() }; // r = (snapshot (not (inner x)), x)
+  |          ^^^^^^^^^^^^^^^^^^^^^^^^
   |
-  = note: this error originates in the macro `gh` (in Nightly builds, run with -Z macro-backtrace for more info)
+  = note: this error originates in the macro `snapshot` (in Nightly builds, run with -Z macro-backtrace for more info)
 
 error: aborting due to previous error
 

creusot/tests/should_fail/builtin_with_contract.rs

@@ -1,7 +1,7 @@
 extern crate creusot_contracts;
 use creusot_contracts::*;
 
-#[ghost]
+#[logic]
 #[ensures(true && false)]
 #[creusot::builtins = "dummy_function"]
 fn builtin_with_contract() {}

creusot/tests/should_fail/ghost_mapping.rs

@@ -1,22 +1,22 @@
 extern crate creusot_contracts;
 use creusot_contracts::{logic::Mapping, *};
 
-#[logic]
+#[logic(prophetic)]
 fn f(x: &mut i32) -> Mapping<(), i32> {
     pearlite! { |_| ^x }
 }
 
-#[ghost]
+#[logic]
 fn g(x: &mut i32) -> Mapping<(), i32> {
     pearlite! { |_| ^x }
 }
 
-#[logic]
+#[logic(prophetic)]
 fn h(y: &mut i32) -> bool {
     pearlite! { forall<_x:Int> ^y == 1i32 }
 }
 
-#[ghost]
+#[logic]
 fn i(y: &mut i32) -> bool {
     pearlite! { forall<_x:Int> ^y == 1i32 }
 }

creusot/tests/should_fail/ghost_mapping.stderr

@@ -1,12 +1,12 @@
-error[creusot]: called Logic function in Ghost context "creusot_contracts::__stubs::fin"
+error[creusot]: called prophetic logic function "creusot_contracts::__stubs::fin" in logic context
   --> ghost_mapping.rs:11:5
    |
 11 |     pearlite! { |_| ^x }
    |     ^^^^^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error[creusot]: called Logic function in Ghost context "creusot_contracts::__stubs::fin"
+error[creusot]: called prophetic logic function "creusot_contracts::__stubs::fin" in logic context
   --> ghost_mapping.rs:21:5
    |
 21 |     pearlite! { forall<_x:Int> ^y == 1i32 }

creusot/tests/should_fail/impure_functions.rs

@@ -1,7 +1,7 @@
 extern crate creusot_contracts;
 use creusot_contracts::{logic::*, *};
 
-#[ghost]
+#[logic]
 fn x<T>(v: &Vec<T>) -> Int {
     pearlite! { v.len()@ }
 }

creusot/tests/should_fail/impure_functions.stderr

@@ -1,10 +1,10 @@
-error[creusot]: called Program function in Ghost context "std::vec::Vec::<T, A>::len"
+error[creusot]: called program function "std::vec::Vec::<T, A>::len" in logic context
  --> impure_functions.rs:6:19
   |
 6 |     pearlite! { v.len()@ }
   |                   ^^^
 
-error[creusot]: called Ghost function in Program context "x"
+error[creusot]: called logic function "x" in program context
   --> impure_functions.rs:10:13
    |
 10 |     let _ = x(&Vec::<()>::new());

creusot/tests/should_fail/logic_ghost_impl.rs → creusot/tests/should_fail/logic_prophetic_impl.rs

@@ -7,7 +7,7 @@ trait T {
 }
 
 impl T for () {
-    #[ghost]
+    #[logic(prophetic)]
     fn f() {
         ()
     }

creusot/tests/should_fail/logic_prophetic_impl.stderr

@@ -0,0 +1,8 @@
+error[creusot]: Expected `f` to be a logic function as specified by the trait declaration
+  --> logic_prophetic_impl.rs:11:5
+   |
+11 |     fn f() {
+   |     ^^^^^^
+
+error: aborting due to previous error
+