Struct Perm 

pub struct Perm<C: ?Sized + Container>(/* private fields */);

Token that represents the ownership of the contents of a container object. The container is either an interrior mutable type (e.g., Perm or atomic types) or a raw pointer.

A Perm only exists in the ghost world, and it must be used in conjunction with its container in order to read or write the value.

Permissions are made unsized to guarantee that they cannot be replaced in a mutable reference. This would allow the permission to outlive the reference it has been placed in. This makes it easier to specify splitting a mutable reference of a permission to a slice, and makes it possible to specify functions such as Perm::from_mut.

Pointer permissions

A particular case of permissions is the case of permissions for raw pointers (i.e., C is *const T). In this case, the permission represents the ownership of the memory cell.

A warning regarding memory leaks: dropping a Perm<*const T> cannot deallocate the memory corresponding to the pointer because it is a ghost value. One must thus remember to explicitly call drop in order to free the memory tracked by a Perm<*const T> token.

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 Perm object created by Perm::new, ensuring safety in a manner similar to ghost_cell.

#[check(terminates)]

Perm<*const T> methods, particularly constructors (new, from_box, from_ref, from_mut), are marked check(terminates) rather than check(ghost) to prevent two things from happening in ghost code:

1. running out of pointer addresses;
2. allocating too large objects.

Note that we already can’t guard against these issues in program code. But preventing them in ghost code is even more imperative to ensure soundness.

Specifically, creating too many pointers contradicts the Perm::disjoint_lemma, and allocating too large objects contradicts the [Perm::invariant] that allocations have size at most isize::MAX.

Implementations

impl<C: ?Sized + Container> Perm<C>

pub fn disjoint_lemma(&mut self, other: &Self)

If one owns two permissions in ghost code, then they correspond to different containers.

impl<T: ?Sized> Perm<*const T>

pub fn new(v: T) -> (*mut T, Ghost<Box<Perm<*const T>>>)

where T: Sized,

Creates a new Perm<*const T> and associated *const by allocating a new memory cell initialized with v.

pub fn from_box(val: Box<T>) -> (*mut T, Ghost<Box<Perm<*const T>>>)

Creates a ghost Perm<*const T> and associated *const from an existing Box.

pub fn from_ref(r: &T) -> (*const T, Ghost<&Perm<*const T>>)

Decompose a shared reference into a raw pointer and a ghost Perm<*const T>.

Erasure

This function erases to a raw reborrow of a reference.

Perm::from_ref(r)
// erases to
r as *const T

pub fn from_mut(r: &mut T) -> (*mut T, Ghost<&mut Perm<*const T>>)

Decompose a mutable reference into a raw pointer and a ghost Perm<*const T>.

Erasure

This function erases to a raw reborrow of a reference.

Perm::from_mut(r)
// erases to
r as *mut T

pub unsafe fn as_ref(ptr: *const T, own: Ghost<&Perm<*const T>>) -> &T

Immutably borrows the underlying T.

Safety

Safety requirements are the same as a direct dereference: &*ptr.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

Erasure

This function erases to a cast from raw pointer to shared reference.

Perm::as_ref(ptr, own)
// erases to
& *ptr

pub unsafe fn as_mut(ptr: *mut T, own: Ghost<&mut Perm<*const T>>) -> &mut T

Mutably borrows the underlying T.

Safety

Safety requirements are the same as a direct dereference: &mut *ptr.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

Erasure

This function erases to a cast from raw pointer to mutable reference.

Perm::as_mut(ptr, own)
// erases to
&mut *ptr

pub unsafe fn to_box(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) -> Box<T>

Transfers ownership of own back into a Box.

Safety

Safety requirements are the same as Box::from_raw.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

pub unsafe fn drop(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>)

Deallocates the memory pointed by ptr.

Safety

Safety requirements are the same as Box::from_raw.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

pub fn ptr_is_aligned_lemma(&self)

The pointer of a Perm<*const T> is always aligned.

Trait Implementations

impl<C: ?Sized + Container<Value: Sized>> View for Perm<C>

type ViewTy = <C as Container>::Value

impl<T: ?Sized> Invariant for Perm<*const T>

impl<T: Sized> Invariant for Perm<PermCell<T>>

impl<C: ?Sized + Container> Resolve for Perm<C>