Struct PCell

pub struct PCell<T: ?Sized>(/* private fields */);

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.

Implementations

impl<T> PCell<T>

pub fn new(value: T) -> (Self, Ghost<PCellOwn<T>>)

Creates a new PCell containing the given value.

ensures

result.0.id() == result.1.id()

ensures

(*result.1)@ == value

pub unsafe fn set(&self, perm: Ghost<&mut PCellOwn<T>>, val: T)

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.

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 replace(&self, perm: Ghost<&mut PCellOwn<T>>, val: T) -> T

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.

requires

self.id() == perm.id()

ensures

val == (^perm.inner_logic())@

ensures

result == (*perm.inner_logic())@

ensures

self.id() == (^perm.inner_logic()).id()

pub fn into_inner(self, perm: Ghost<PCellOwn<T>>) -> T

Unwraps the value, consuming the cell.

requires

self.id() == perm.id()

ensures

result == perm@

pub unsafe fn borrow<'a>(&'a self, perm: Ghost<&'a PCellOwn<T>>) -> &'a T

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.

requires

self.id() == perm.id()

ensures

*result == perm@

pub unsafe fn borrow_mut<'a>( &'a self, perm: Ghost<&'a mut PCellOwn<T>>, ) -> &'a mut T

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.

requires

self.id() == perm.id()

ensures

self.id() == (^perm.inner_logic()).id()

ensures

*result == (*perm.inner_logic())@

ensures

^result == (^perm.inner_logic())@

impl<T> PCell<T>

where T: Copy,

pub unsafe fn get(&self, perm: Ghost<&PCellOwn<T>>) -> T

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.

requires

self.id() == perm.id()

ensures

result == (**perm)@

impl<T> PCell<T>

pub fn id(self) -> Id

Returns the logical identity of the cell.

This is used to guarantee that a PCellOwn is always used with the right PCell.

logic

pub fn as_ptr(&self) -> *mut T

Returns a raw pointer to the underlying data in this cell.

ensures

true

pub fn from_mut(t: &mut T) -> (&PCell<T>, Ghost<&mut PCellOwn<T>>)

Returns a &PCell<T> from a &mut T

ensures

result.0.id() == result.1.inner_logic().id()

ensures

^t == (^result.1.inner_logic())@

ensures

*t == (*result.1.inner_logic())@

impl<T> PCell<T>

where T: Default,

pub unsafe fn take(&self, perm: Ghost<&mut PCellOwn<T>>) -> T

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.

requires

self.id() == perm.id()

ensures

self.id() == (^perm.inner_logic()).id()

ensures

result == (*perm.inner_logic())@

ensures

(^perm.inner_logic())@.is_default()