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

_

terminates

ghost

ensures

**result == **self

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

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

erasure

_

terminates

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

_

terminates

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.

terminates

ghost

ensures

*result == x

pub fn new_logic(x: T) -> Self

(opaque)

ensures

*result == x

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.

terminates

ghost

ensures

result == *self

pub fn inner_logic(self) -> T

where T: Sized,

Returns the inner value of the Ghost.

You should prefer the dereference operator * instead.

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

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

terminates

ghost

erasure

_

ensures

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

ensures

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

Trait Implementations

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

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

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

terminates

ghost

requires

false

ensures

result == &**self

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

terminates

ghost

requires

false

ensures

result == &mut **self

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

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

(open, prophetic, inline)

pearlite! { &^*self }

type Target = <T as Fin>::Target

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

fn invariant(self) -> bool

(open, prophetic, inline)

inv(*self)

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

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

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

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

requires

<Ghost<&'a L> as LocalInvariantExt<'a>>::open.precondition((Ghost::new_logic(&**self), tokens, f))

ensures

<Ghost<&'a L> as LocalInvariantExt<'a>>::open.postcondition((Ghost::new_logic(&**self), tokens, f), result)

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

impl<'a, T: Protocol> LocalInvariantExt<'a> for Ghost<&'a LocalInvariant<T>>

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

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

requires

tokens.contains(self.namespace())

requires

forall<t: Ghost<&mut T>> (**t).protocol(self.public()) && inv(t) ==>
        f.precondition((t,)) &&
        // f must restore the invariant
        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public()))

ensures

exists<t: Ghost<&mut T>> t.protocol(self.public()) && f.postcondition_once((t,), result)

type Inner = T

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

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

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

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

requires

T::deref.precondition((*self,))

requires

forall<this> T::deref.postcondition((*self,), this) ==>
        <Ghost<&'a T::Target> as LocalInvariantExt<'a>>::open.precondition((Ghost::new_logic(this), tokens, f))

ensures

exists<this> T::deref.postcondition((*self,), this) &&
        <Ghost<&'a T::Target> as LocalInvariantExt<'a>>::open.postcondition((Ghost::new_logic(this), tokens, f), result)

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

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