PCell: interior mutability with ghost ownership

creusot-contracts/src/ghost.rs

@@ -45,7 +45,7 @@ pub struct GhostBox<T>(#[cfg(creusot)] Box<T>, #[cfg(not(creusot))] std::marker:
 where
     T: ?Sized;
 
-impl<T: ?Sized + Clone> Clone for GhostBox<T> {
+impl<T: Clone> Clone for GhostBox<T> {
     #[ensures(result == *self)]
     fn clone(&self) -> Self {
         #[cfg(creusot)]
@@ -107,14 +107,17 @@ impl<T: ?Sized> Resolve for GhostBox<T> {
     #[open]
     #[predicate(prophetic)]
     fn resolve(self) -> bool {
-        resolve(&self.0)
+        self.0.resolve()
     }
 
-    #[trusted]
     #[logic(prophetic)]
-    #[requires(structural_resolve(&self))]
+    #[open(self)]
+    #[requires(inv(self))]
+    #[requires(structural_resolve(self))]
     #[ensures((*self).resolve())]
-    fn resolve_coherence(&self) {}
+    fn resolve_coherence(&self) {
+        self.0.resolve_coherence();
+    }
 }
 
 impl<T: ?Sized> GhostBox<T> {
@@ -151,11 +154,12 @@ impl<T: ?Sized> GhostBox<T> {
     /// 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.
+    #[pure]
     #[requires(false)]
     pub fn conjure() -> Self {
         #[cfg(creusot)]
         {
-            loop {}
+            panic!()
         }
         #[cfg(not(creusot))]
         {
@@ -190,6 +194,13 @@ impl<T> GhostBox<T> {
         }
     }
 
+    #[logic]
+    #[open(self)]
+    #[ensures(*result.0 == x)]
+    pub fn new_logic(x: T) -> Self {
+        Self(Box::new(x))
+    }
+
     /// Returns the inner value of the `GhostBox`.
     ///
     /// This function can only be called in `ghost!` context.
@@ -217,3 +228,19 @@ impl<T> GhostBox<T> {
         *self.0
     }
 }
+
+impl<T, U> GhostBox<(T, U)> {
+    #[pure]
+    #[trusted]
+    #[ensures(*self == (*result.0, *result.1))]
+    pub fn split(self) -> (GhostBox<T>, GhostBox<U>) {
+        #[cfg(creusot)]
+        {
+            panic!()
+        }
+        #[cfg(not(creusot))]
+        {
+            (GhostBox(std::marker::PhantomData), GhostBox(std::marker::PhantomData))
+        }
+    }
+}

creusot-contracts/src/lib.rs

@@ -390,6 +390,7 @@ pub mod ghost;
 pub mod invariant;
 pub mod logic;
 pub mod model;
+pub mod pcell;
 pub mod ptr_own;
 pub mod resolve;
 pub mod snapshot;

creusot-contracts/src/logic/fmap.rs

@@ -238,7 +238,7 @@ impl<K, V: ?Sized> FMap<K, V> {
     #[ensures(result.is_empty())]
     #[allow(unreachable_code)]
     pub fn new() -> GhostBox<Self> {
-        ghost!(panic!())
+        GhostBox::conjure()
     }
 
     /// Returns the number of elements in the map.

creusot-contracts/src/pcell.rs

@@ -0,0 +1,266 @@
+//! Shared mutation with a ghost token
+//!
+//! This allows a form of interior mutability, using [ghost](mod@crate::ghost) code to keep
+//! track of the logical value.
+
+#[cfg(creusot)]
+use crate::util::SizedW;
+
+use crate::{GhostBox, *};
+use ::std::{cell::UnsafeCell, marker::PhantomData};
+
+/// A "permission" cell allowing interior mutability via a ghost token.
+///
+/// When writing/reading the cell, you need to explicitely pass a [`PCellOwn`] object.
+///
+/// # Safety
+///
+/// When using Creusot to verify the code, all methods should be safe to call. Indeed,
+/// Creusot ensures that every operation on the inner value uses the right [`PCellOwn`] object
+/// created by [`PCell::new`], ensuring safety in a manner similar to [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
+#[repr(transparent)]
+pub struct PCell<T: ?Sized>(UnsafeCell<T>);
+
+/// The id of a [`PCell`].
+///
+/// Most methods that manipulate `PCell`s require a permission with the same id.
+#[trusted]
+#[allow(dead_code)]
+pub struct Id(PhantomData<()>);
+
+impl Clone for Id {
+    #[pure]
+    #[ensures(result == *self)]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+impl Copy for Id {}
+
+/// Token that represents the ownership of a [`PCell`] object.
+///
+/// A `PCellOwn` only exists in the ghost world, and it must be used in conjunction with
+/// [`PCell`] in order to read or write the value.
+pub struct PCellOwn<T: ?Sized> {
+    /// Forbid construction
+    _private: PhantomData<()>,
+    pub id: Id,
+    pub val: Box<T>,
+}
+
+impl<T> View for PCellOwn<T> {
+    type ViewTy = T;
+
+    #[logic]
+    #[open]
+    fn view(self) -> Self::ViewTy {
+        *self.val
+    }
+}
+
+impl<T> PCellOwn<T>
+where
+    T: ?Sized,
+{
+    /// Returns the logical identity of the cell.
+    ///
+    /// To use a [`Pcell`], this and [`PCell::id`] must agree.
+    #[logic]
+    #[open]
+    pub fn id(self) -> Id {
+        self.id
+    }
+
+    /// Get the logical value.
+    #[logic]
+    #[open]
+    pub fn val(self) -> SizedW<T> {
+        self.val
+    }
+
+    /// If one owns two `PCellOwn`s in ghost code, then they have different ids.
+    #[trusted]
+    #[pure]
+    #[ensures(own1.id() != own2.id())]
+    #[ensures(*own1 == ^own1)]
+    #[allow(unused_variables)]
+    pub fn disjoint_lemma(own1: &mut PCellOwn<T>, own2: &PCellOwn<T>) {}
+}
+
+impl<T> PCell<T> {
+    /// Creates a new `PCell` containing the given value.
+    #[trusted]
+    #[ensures(result.0.id() == result.1.id())]
+    #[ensures((*result.1)@ == value)]
+    pub fn new(value: T) -> (Self, GhostBox<PCellOwn<T>>) {
+        let this = Self(UnsafeCell::new(value));
+        let perm = GhostBox::conjure();
+        (this, perm)
+    }
+
+    /// Sets the contained value.
+    ///
+    /// # Safety
+    ///
+    /// You must ensure that no other borrows to the inner value of `self` exists when calling
+    /// this function.
+    ///
+    /// Creusot will check that all calls to this function are indeed safe: see the
+    /// [type documentation](PCell).
+    #[trusted]
+    #[requires(self.id() == perm.id())]
+    #[ensures(val == (^perm.inner_logic())@)]
+    #[ensures(resolve(&(*perm.inner_logic())@))]
+    #[ensures(self.id() == (^perm.inner_logic()).id())]
+    pub unsafe fn set(&self, perm: GhostBox<&mut PCellOwn<T>>, val: T) {
+        let _ = perm;
+        unsafe {
+            *self.0.get() = val;
+        }
+    }
+
+    /// Replaces the contained value with `val`, and returns the old contained value.
+    ///
+    /// # Safety
+    ///
+    /// You must ensure that no other borrows to the inner value of `self` exists when calling
+    /// this function.
+    ///
+    /// Creusot will check that all calls to this function are indeed safe: see the
+    /// [type documentation](PCell).
+    #[trusted]
+    #[requires(self.id() == perm.id())]
+    #[ensures(val == (^perm.inner_logic())@)]
+    #[ensures(result == (*perm.inner_logic())@)]
+    #[ensures(self.id() == (^perm.inner_logic()).id())]
+    pub unsafe fn replace(&self, perm: GhostBox<&mut PCellOwn<T>>, val: T) -> T {
+        let _ = perm;
+        unsafe { std::ptr::replace(self.0.get(), val) }
+    }
+
+    /// Unwraps the value, consuming the cell.
+    #[trusted]
+    #[requires(self.id() == perm.id())]
+    #[ensures(result == perm@)]
+    pub fn into_inner(self, perm: GhostBox<PCellOwn<T>>) -> T {
+        let _ = perm;
+        self.0.into_inner()
+    }
+
+    /// Immutably borrows the wrapped value.
+    ///
+    /// The permission also acts as a guard, preventing writes to the underlying value
+    /// while it is borrowed.
+    ///
+    /// # Safety
+    ///
+    /// You must ensure that no mutable borrow to the inner value of `self` exists when calling
+    /// this function.
+    ///
+    /// Creusot will check that all calls to this function are indeed safe: see the
+    /// [type documentation](PCell).
+    #[trusted]
+    #[requires(self.id() == perm.id())]
+    #[ensures(*result == perm@)]
+    pub unsafe fn borrow<'a>(&'a self, perm: GhostBox<&'a PCellOwn<T>>) -> &'a T {
+        let _ = perm;
+        unsafe { &*self.0.get() }
+    }
+
+    /// Mutably borrows the wrapped value.
+    ///
+    /// The permission also acts as a guard, preventing accesses to the underlying value
+    /// while it is borrowed.
+    ///
+    /// # Safety
+    ///
+    /// You must ensure that no other borrows to the inner value of `self` exists when calling
+    /// this function.
+    ///
+    /// Creusot will check that all calls to this function are indeed safe: see the
+    /// [type documentation](PCell).
+    #[trusted]
+    #[requires(self.id() == perm.id())]
+    #[ensures(self.id() == (^perm.inner_logic()).id())]
+    #[ensures(*result == (*perm.inner_logic())@)]
+    #[ensures(^result == (^perm.inner_logic())@)]
+    pub unsafe fn borrow_mut<'a>(&'a self, perm: GhostBox<&'a mut PCellOwn<T>>) -> &'a mut T {
+        let _ = perm;
+        unsafe { &mut *self.0.get() }
+    }
+}
+
+impl<T> PCell<T>
+where
+    T: Copy,
+{
+    /// Returns a copy of the contained value.
+    ///
+    /// # Safety
+    ///
+    /// You must ensure that no mutable borrow to the inner value of `self` exists when calling
+    /// this function.
+    ///
+    /// Creusot will check that all calls to this function are indeed safe: see the
+    /// [type documentation](PCell).
+    #[trusted]
+    #[requires(self.id() == perm.id())]
+    #[ensures(result == (**perm)@)]
+    pub unsafe fn get(&self, perm: GhostBox<&PCellOwn<T>>) -> T {
+        let _ = perm;
+        unsafe { *self.0.get() }
+    }
+}
+
+impl<T> PCell<T> {
+    /// Returns the logical identity of the cell.
+    ///
+    /// This is used to guarantee that a [`PCellOwn`] is always used with the right [`PCell`].
+    #[logic]
+    #[trusted]
+    pub fn id(self) -> Id {
+        dead
+    }
+
+    /// Returns a raw pointer to the underlying data in this cell.
+    #[trusted]
+    #[ensures(true)]
+    pub fn as_ptr(&self) -> *mut T {
+        self.0.get()
+    }
+
+    /// Returns a `&PCell<T>` from a `&mut T`
+    #[trusted]
+    #[ensures(result.0.id() == result.1.inner_logic().id())]
+    #[ensures(^t == (^result.1.inner_logic())@)]
+    #[ensures(*t == (*result.1.inner_logic())@)]
+    pub fn from_mut(t: &mut T) -> (&PCell<T>, GhostBox<&mut PCellOwn<T>>) {
+        // SAFETY: `PCell` is layout-compatible with `Cell` and `T` because it is `repr(transparent)`.
+        // SAFETY: `&mut` ensures unique access
+        let cell: &PCell<T> = unsafe { &*(t as *mut T as *const Self) };
+        let perm = GhostBox::conjure();
+        (cell, perm)
+    }
+}
+
+impl<T> PCell<T>
+where
+    T: crate::std::default::Default,
+{
+    /// Takes the value of the cell, leaving `Default::default()` in its place.
+    ///
+    /// # Safety
+    ///
+    /// You must ensure that no other borrows to the inner value of `self` exists when calling
+    /// this function.
+    ///
+    /// Creusot will check that all calls to this function are indeed safe: see the
+    /// [type documentation](PCell).
+    #[requires(self.id() == perm.id())]
+    #[ensures(self.id() == (^perm.inner_logic()).id())]
+    #[ensures(result == (*perm.inner_logic())@)]
+    #[ensures((^perm.inner_logic())@.is_default())]
+    pub unsafe fn take(&self, perm: GhostBox<&mut PCellOwn<T>>) -> T {
+        self.replace(perm, T::default())
+    }
+}

creusot-contracts/src/ptr_own.rs

@@ -105,7 +105,5 @@ impl<T: ?Sized> PtrOwn<T> {
     #[ensures(own1.ptr().addr_logic() != own2.ptr().addr_logic())]
     #[ensures(*own1 == ^own1)]
     #[allow(unused_variables)]
-    pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &PtrOwn<T>) {
-        panic!()
-    }
+    pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &PtrOwn<T>) {}
 }