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 ward<'a>(self) -> &'a C

Returns the underlying container that is managed by this permission.

(opaque)

pub fn val<'a>(self) -> &'a C::Value

Get the logical value contained by the container.

(opaque)

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

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

terminates

ghost

ensures

self.ward().is_disjoint(self.val(), other.ward(), other.val())

ensures

*self == ^self

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.

terminates

ensures

*result.1.ward() == result.0 && *result.1.val() == 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.

terminates

ensures

*result.1.ward() == result.0 && *result.1.val() == *val

erasure

Box::into_raw

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  // or *mut T (both are allowed)

terminates

ensures

*result.1.ward() == result.0

ensures

*result.1.val() == *r

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 *const T  // or *mut T (both are allowed)

terminates

ensures

*result.1.ward() == result.0

ensures

*result.1.val() == *r

ensures

*(^result.1.inner_logic()).val() == ^r

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

terminates

requires

ptr == *own.ward()

ensures

*result == *own.val()

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

terminates

requires

ptr as *const T == *own.ward()

ensures

*result == *own.val()

ensures

(^own).ward() == own.ward()

ensures

*(^own).val() == ^result

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.

terminates

requires

ptr as *const T == *own.ward()

ensures

*result == *own.val()

erasure

Box::from_raw

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.

terminates

requires

ptr as *const T == *own.ward()

pub fn ptr_is_aligned_lemma(&self)

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

terminates

ghost

ensures

self.ward().is_aligned_logic()

pub fn ptr_is_aligned_opaque(self) -> bool

Opaque wrapper around [std::ptr::is_aligned_logic]. We use this to hide alignment logic by default in invariant because it confuses SMT solvers sometimes. The underlying property is exposed by Perm::ptr_is_aligned_lemma.

(open(pub(self)))

Trait Implementations

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

fn invariant(self) -> bool

(open, prophetic)

pearlite! {
    !self.ward().is_null_logic()
        && self.ptr_is_aligned_opaque()
        && metadata_matches(*self.val(), metadata_logic(*self.ward()))
        // Allocations can never be larger than `isize` (source: https://doc.rust-lang.org/std/ptr/index.html#allocation)
        && size_of_val_logic(*self.val()) <= isize::MAX@
        // The allocation fits in the address space
        // (this is needed to verify (a `Perm` variant of) `<*const T>::add`, which checks this condition)
        && self.ward().addr_logic()@ + size_of_val_logic(*self.val()) <= usize::MAX@
        && inv(self.val())
}

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

fn invariant(self) -> bool

(open, prophetic, inline)

pearlite! { inv(self.val()) }

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

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.val())

fn resolve_coherence(self)

(prophetic)

requires

inv(self)

requires

structural_resolve(self)

ensures

self.resolve()

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

fn view(self) -> Self::ViewTy

(open, inline)

*self.val()

type ViewTy = <C as Container>::Value