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>

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

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

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.

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.

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.

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

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

Trait Implementations

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

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

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

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

This function can only be called in ghost! context

type Target = T

The resulting type after dereferencing.

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

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

This function can only be called in ghost! context

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

type Target = <T as Fin>::Target

impl<'a, L> NonAtomicInvariantExt<'a> for &'a Ghost<L>

where Ghost<&'a L>: NonAtomicInvariantExt<'a>,

type Inner = <Ghost<&'a L> as NonAtomicInvariantExt<'a>>::Inner

fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A

where F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,

Alias for NonAtomicInvariant::open, to use method call syntax (inv.open(...)).

impl<'a, T: Protocol> NonAtomicInvariantExt<'a> for Ghost<&'a NonAtomicInvariant<T>>

type Inner = T

fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A

where F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,

Alias for NonAtomicInvariant::open, to use method call syntax (inv.open(...)).

impl<'a, T> NonAtomicInvariantExt<'a> for Ghost<&'a T>

where T: Deref, Ghost<&'a T::Target>: NonAtomicInvariantExt<'a>,

type Inner = <Ghost<&'a <T as Deref>::Target> as NonAtomicInvariantExt<'a>>::Inner

fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A

where F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,

Alias for NonAtomicInvariant::open, to use method call syntax (inv.open(...)).

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

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