Struct Ghost 

pub struct Ghost<T: ?Sized>(/* 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: ?Sized> Ghost<T>

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

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

erasure

_

ghost

ensures

**result == **self

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

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

erasure

_

ghost

ensures

*result == &mut **self

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.

erasure

_

ghost

requires

false

impl<T: ?Sized> Ghost<T>

pub fn new(x: T) -> Self

where T: Sized,

Creates a new ghost variable.

This function can only be called in ghost! code.

ghost

ensures

#[logic_alias(Self::new_logic)]

pub fn new_logic(_x: T) -> Self

where T: Sized,

logic

pub fn into_inner(self) -> T

where T: Sized,

Returns the inner value of the Ghost.

This function can only be called in ghost! context.

ghost

ensures

#[logic_alias(Self::inner_logic)]

pub fn inner_logic(self) -> T

where T: Sized,

Returns the inner value of the Ghost.

You should prefer the dereference operator * instead.

logic

impl<T, U: ?Sized> Ghost<(T, U)>

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

Transform a Ghost of a pair into a pair of Ghosts.

ghost

erasure

_

ensures

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

ensures

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

impl<T1, T2, T3> Ghost<(T1, T2, T3)>

pub fn split(self) -> (Ghost<T1>, Ghost<T2>, Ghost<T3>)

Transform a Ghost of tuple into a tuple of Ghosts.

ghost

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

impl<T1, T2, T3, T4> Ghost<(T1, T2, T3, T4)>

pub fn split(self) -> (Ghost<T1>, Ghost<T2>, Ghost<T3>, Ghost<T4>)

Transform a Ghost of tuple into a tuple of Ghosts.

ghost

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

impl<T1, T2, T3, T4, T5> Ghost<(T1, T2, T3, T4, T5)>

pub fn split(self) -> (Ghost<T1>, Ghost<T2>, Ghost<T3>, Ghost<T4>, Ghost<T5>)

Transform a Ghost of tuple into a tuple of Ghosts.

ghost

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

impl<T1, T2, T3, T4, T5, T6> Ghost<(T1, T2, T3, T4, T5, T6)>

pub fn split( self, ) -> (Ghost<T1>, Ghost<T2>, Ghost<T3>, Ghost<T4>, Ghost<T5>, Ghost<T6>)

Transform a Ghost of tuple into a tuple of Ghosts.

ghost

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

impl<T1, T2, T3, T4, T5, T6, T7> Ghost<(T1, T2, T3, T4, T5, T6, T7)>

pub fn split( self, ) -> (Ghost<T1>, Ghost<T2>, Ghost<T3>, Ghost<T4>, Ghost<T5>, Ghost<T6>, Ghost<T7>)

Transform a Ghost of tuple into a tuple of Ghosts.

ghost

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

impl<T1, T2, T3, T4, T5, T6, T7, T8> Ghost<(T1, T2, T3, T4, T5, T6, T7, T8)>

pub fn split( self, ) -> (Ghost<T1>, Ghost<T2>, Ghost<T3>, Ghost<T4>, Ghost<T5>, Ghost<T6>, Ghost<T7>, Ghost<T8>)

Transform a Ghost of tuple into a tuple of Ghosts.

ghost

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

ensures

(*self).$n == *result.$n

Trait Implementations

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

fn clone(&self) -> Self

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl<T: Copy> Copy for Ghost<T>

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

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

This function can only be called in ghost! context

ghost

requires

false

ensures

#[logic_alias(self.deref_logic())]

type Target = T

The resulting type after dereferencing.

impl<T: ?Sized> DerefLogic for Ghost<T>

fn deref_logic(&self) -> &T

logic

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

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

This function can only be called in ghost! context

ghost

requires

false

ensures

#[logic_alias(self.deref_mut_logic())]

impl<T: ?Sized> DerefMutLogic for Ghost<T>

fn deref_mut_logic(&mut self) -> &mut T

logic

impl<T: ?Sized + Fin> Fin for Ghost<T>

fn fin<'a>(self) -> &'a Self::Target

logic(open, prophetic, inline)

&^*self

type Target = <T as Fin>::Target

impl<T: ?Sized> Invariant for Ghost<T>

fn invariant(self) -> bool

logic(open, prophetic, inline)

inv(*self)

impl<'a, T: ?Sized> Resolve for Ghost<T>

fn resolve(self) -> bool

logic(open, prophetic, inline)

resolve(*self)

fn resolve_coherence(self)

logic

requires

structural_resolve(self)

ensures

self.resolve()