Struct creusot_contracts::ghost::GhostBox

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

A type that can be used in ghost context.

This type may be used to make more complicated proofs possible. In particular, some proof may need a notion of non-duplicable token to carry around.

Conceptually, a GhostBox<T> is a pointer to an item of type T that resides in a special “ghost” heap. This heap is inaccessible from normal code, and GhostBox values cannot be used to influence the behavior of normal code.

This box can be dereferenced in a ghost block:

let b: GhostBox<i32> = GhostBox::new(1);
ghost! {
    let value: i32 = *b;
    // use value here
}
let value: i32 = *b; // compile error !

Implementations

impl<T: ?Sized> GhostBox<T>

pub fn borrow(&self) -> GhostBox<&T>

Transforms a &GhostBox<T> into GhostBox<&T>.

pure

ensures

*result.0 == &*self.0

pub fn borrow_mut(&mut self) -> GhostBox<&mut T>

Transforms a &mut GhostBox<T> into a GhostBox<&mut T>.

pure

ensures

*result.0 == &mut *self.0

pub fn conjure() -> Self

Conjures a GhostBox<T> out of thin air. This would be unsound in verified code, hence the false precondition. 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.

requires

false

impl<T> GhostBox<T>

pub fn new(x: T) -> Self

Creates a new ghost variable.

This function can only be called in ghost! code.

pure

ensures

*result.0 == x

pub fn into_inner(self) -> T

Returns the inner value of the GhostBox.

This function can only be called in ghost! context.

pure

ensures

result == *self.0

pub fn inner_logic(self) -> T

Returns the inner value of the GhostBox.

You should prefer the dereference operator * instead.

logic

*self.0

Trait Implementations

impl<T: ?Sized + Clone> Clone for GhostBox<T>

fn clone(&self) -> Self

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T: ?Sized> Deref for GhostBox<T>

fn deref(&self) -> &Self::Target

This function can only be called in ghost! context

pure

ensures

*(*self).0 == *result

type Target = T

The resulting type after dereferencing.

impl<T: ?Sized> DerefMut for GhostBox<T>

fn deref_mut(&mut self) -> &mut Self::Target

This function can only be called in ghost! context

pure

ensures

result == &mut *self.0

impl<T: ?Sized> Resolve for GhostBox<T>

fn resolve(self) -> bool

logic(prophetic)

resolve(&self.0)

fn resolve_coherence(&self)

logic(prophetic)

requires

structural_resolve(&self)

ensures

(*self).resolve()

impl<T: View + ?Sized> View for GhostBox<T>

fn view(self) -> Self::ViewTy

logic

self.0.view()

type ViewTy = <T as View>::ViewTy