From 712b62b90c0da63f2a23842e11bfdb15f896b34a Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Thu, 28 Nov 2024 14:39:40 +0100 Subject: [PATCH] Add a `PCell` type for interior mutability with ghost code --- creusot-contracts/src/ghost.rs | 2 +- creusot-contracts/src/lib.rs | 1 + creusot-contracts/src/pcell.rs | 199 +++++++++++++++++++++++++++++++++ 3 files changed, 201 insertions(+), 1 deletion(-) create mode 100644 creusot-contracts/src/pcell.rs diff --git a/creusot-contracts/src/ghost.rs b/creusot-contracts/src/ghost.rs index c9c6797202..4630b51fa8 100644 --- a/creusot-contracts/src/ghost.rs +++ b/creusot-contracts/src/ghost.rs @@ -45,7 +45,7 @@ pub struct GhostBox(#[cfg(creusot)] Box, #[cfg(not(creusot))] std::marker: where T: ?Sized; -impl Clone for GhostBox { +impl Clone for GhostBox { #[ensures(result == *self)] fn clone(&self) -> Self { #[cfg(creusot)] diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs index 9e1152e72b..2d110103d8 100644 --- a/creusot-contracts/src/lib.rs +++ b/creusot-contracts/src/lib.rs @@ -387,6 +387,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; diff --git a/creusot-contracts/src/pcell.rs b/creusot-contracts/src/pcell.rs new file mode 100644 index 0000000000..0558eb61d4 --- /dev/null +++ b/creusot-contracts/src/pcell.rs @@ -0,0 +1,199 @@ +//! 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. + +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. +#[repr(transparent)] +pub struct PCell(UnsafeCell); + +/// The id of a [`PCell`]. +#[trusted] +#[allow(dead_code)] +pub struct Id(PhantomData<()>); + +impl Clone for Id { + 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. +#[trusted] +pub struct PCellOwn(PhantomData); + +impl View for PCellOwn { + type ViewTy = T; + + #[logic] + #[trusted] + fn view(self) -> Self::ViewTy { + dead + } +} + +impl PCellOwn +where + T: ?Sized, +{ + /// Returns the logical identity of the cell. + /// + /// To use a [`Pcell`], this and [`PCell::id`] must agree. + #[logic] + #[trusted] + pub fn id(self) -> Id { + dead + } +} + +impl PCellOwn { + /// Get the logical value. + #[logic] + #[open] + pub fn val(self) -> T { + self.view() + } +} + +impl PCell { + /// Creates a new `PCell` containing the given value. + #[trusted] + #[ensures(result.0.id() == result.1.id())] + #[ensures((*result.1)@ == value)] + #[allow(unreachable_code)] + pub fn new(value: T) -> (Self, GhostBox>) { + let this = Self(UnsafeCell::new(value)); + let perm = ghost!(panic!()); + (this, perm) + } + + /// Sets the contained value. + #[trusted] + #[requires(self.id() == perm.id())] + #[ensures(val == (^perm.inner_logic()).val())] + #[ensures(resolve(&(*perm.inner_logic()).val()))] + #[ensures(self.id() == (^perm.inner_logic()).id())] + pub fn set(&self, perm: GhostBox<&mut PCellOwn>, val: T) { + let _ = perm; + unsafe { + *self.0.get() = val; + } + } + + /// Replaces the contained value with `val`, and returns the old contained value. + #[trusted] + #[requires(self.id() == perm.id())] + #[ensures(val == (^perm.inner_logic()).val())] + #[ensures(result == (*perm.inner_logic()).val())] + #[ensures(self.id() == (^perm.inner_logic()).id())] + pub fn replace(&self, perm: GhostBox<&mut PCellOwn>, 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.val())] + pub fn into_inner(self, perm: GhostBox>) -> 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. + #[trusted] + #[requires(self.id() == perm.id())] + #[ensures(*result == perm.val())] + pub fn borrow<'a>(&'a self, perm: GhostBox<&'a PCellOwn>) -> &'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. + #[trusted] + #[requires(self.id() == perm.id())] + #[ensures(self.id() == (^perm.inner_logic()).id())] + #[ensures(*result == (*perm.inner_logic()).val())] + #[ensures(^result == (^perm.inner_logic()).val())] + pub fn borrow_mut<'a>(&'a self, perm: GhostBox<&'a mut PCellOwn>) -> &'a mut T { + let _ = perm; + unsafe { &mut *self.0.get() } + } +} + +impl PCell +where + T: Copy, +{ + /// Returns a copy of the contained value. + #[trusted] + #[requires(self.id() == perm.id())] + #[ensures(result == (**perm)@)] + pub fn get(&self, perm: GhostBox<&PCellOwn>) -> T { + let _ = perm; + unsafe { *self.0.get() } + } +} + +impl PCell +where + T: ?Sized, +{ + /// 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` from a `&mut T` + #[trusted] + #[ensures(result.0.id() == result.1.inner_logic().id())] + // TODO: #[ensures(^t == (^result.1.inner_logic()).val())] + #[allow(unreachable_code)] + pub fn from_mut(t: &mut T) -> (&PCell, GhostBox<&mut PCellOwn>) { + // SAFETY: `PCell` is layout-compatible with `Cell` and `T` because it is `repr(transparent)`. + // SAFETY: `&mut` ensures unique access + let cell: &PCell = unsafe { &*(t as *mut T as *const Self) }; + let perm = ghost!(panic!()); + (cell, perm) + } +} + +impl PCell +where + T: crate::std::default::Default, +{ + /// Takes the value of the cell, leaving `Default::default()` in its place. + #[requires(self.id() == perm.id())] + #[ensures(self.id() == (^perm.inner_logic()).id())] + #[ensures(result == (*perm.inner_logic()).val())] + #[ensures((^perm.inner_logic()).val().is_default())] + pub fn take(&self, perm: GhostBox<&mut PCellOwn>) -> T { + self.replace(perm, T::default()) + } +}