Struct Ghost

pub struct Ghost<T>(/* private fields */);

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 Ghost<T> is an object of type T that resides in a special “ghost” heap. This heap is inaccessible from normal code, and Ghost values cannot be used to influence the behavior of normal code.

This box can be accessed in a ghost! block:

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

Implementations

impl<T> Ghost<T>

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

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

pure

ensures

**result == **self

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

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

pure

ensures

*result.inner_logic() == (*self).inner_logic()

ensures

^result.inner_logic() == (^self).inner_logic()

pub fn conjure() -> Self

Conjures a Ghost<T> out of thin air.

This would be unsound in verified code, hence the false precondition. This function is nevertheless useful to create a Ghost in “trusted” contexts, when axiomatizing an API that is believed to be sound for external reasons.

pure

requires

false

impl<T> Ghost<T>

pub fn new(x: T) -> Self

Creates a new ghost variable.

This function can only be called in ghost! code.

pure

ensures

*result == x

pub fn new_logic(x: T) -> Self

logic

Self(x)

ensures

*result == x

pub fn into_inner(self) -> T

Returns the inner value of the Ghost.

This function can only be called in ghost! context.

pure

ensures

result == *self

pub fn inner_logic(self) -> T

Returns the inner value of the Ghost.

You should prefer the dereference operator * instead.

logic

self.0

impl<T, U> Ghost<(T, U)>

pub fn split(self) -> (Ghost<T>, Ghost<U>)

pure

ensures

*self == (*result.0, *result.1)

Trait Implementations

impl<T: Clone> Clone for Ghost<T>

fn clone(&self) -> Self

ensures

result == *self

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

Performs copy-assignment from source.

impl<T> Deref for Ghost<T>

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

This function can only be called in ghost! context

pure

ensures

(*self).inner_logic() == *result

type Target = T

The resulting type after dereferencing.

impl<T> DerefMut for Ghost<T>

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

This function can only be called in ghost! context

pure

ensures

*result == (*self).inner_logic()

ensures

^result == (^self).inner_logic()

impl<T> Invariant for Ghost<T>

fn invariant(self) -> bool

logic(prophetic)

inv(self.inner_logic())

impl<T> Resolve for Ghost<T>

fn resolve(self) -> bool

logic(prophetic)

resolve(&self.inner_logic())

fn resolve_coherence(&self)

logic(prophetic)

{}

requires

structural_resolve(self)

ensures

(*self).resolve()

impl<T: View> View for Ghost<T>

fn view(self) -> Self::ViewTy

logic

(*self).view()

type ViewTy = <T as View>::ViewTy