Specs for raw pointers & ghost ownership for pointers

creusot-contracts/src/ghost.rs

@@ -129,6 +129,23 @@ impl<T: ?Sized> GhostBox<T> {
         }
     }
 
+    /// Conjures a `GhostBox<T>` out of thin air.
+    /// This would be unsound in verified code, hence the `false` precondition.
+    /// This function is nevertheless useful to create a `GhostBox` in "trusted"
+    /// contexts, when axiomatizing an API that is believed to be sound for
+    /// external reasons.
+    #[requires(false)]
+    pub fn conjure() -> Self {
+        #[cfg(creusot)]
+        {
+            loop {}
+        }
+        #[cfg(not(creusot))]
+        {
+            GhostBox(std::marker::PhantomData)
+        }
+    }
+
     // Internal function to easily create a GhostBox in non-creusot mode.
     #[cfg(not(creusot))]
     #[doc(hidden)]

creusot-contracts/src/lib.rs

@@ -216,9 +216,9 @@ pub mod snapshot {
     impl<T: ?Sized> Copy for Snapshot<T> {}
 }
 
-pub mod ghost_ptr;
 pub mod invariant;
 pub mod model;
+pub mod ptr_own;
 pub mod resolve;
 pub mod util;
 pub mod well_founded;
@@ -251,6 +251,7 @@ mod base_prelude {
     pub use crate::std::{
         iter::{SkipExt as _, TakeExt as _},
         ops::{FnExt as _, FnMutExt as _, FnOnceExt as _, RangeInclusiveExt as _},
+        ptr::PointerExt as _,
         slice::SliceExt as _,
     };
 }