Module ghost 

Definitions for ghost code

Ghost code is code that will be erased during the normal compilation of the program. To use ghost code in creusot, you must use the ghost! macro:

let x: Ghost<i32> = ghost!(1);
ghost! {
    let y: i32 = *x;
    assert!(y == 1);
};

There are restrictions on the values that can enter/exit a ghost! block: see Ghost and ghost! for more details.

Modules

local_invariant

Define local invariants.

resource

Resource algebras

Structs

Ghost

A type that can be used in ghost! context.

PtrOwn

Token that represents the ownership of a memory cell

Traits

FnGhost

Marker trait for functions that are #[check(ghost)].

Plain

A marker trait for types that can be extracted from snapshots in ghost code. These are type that only contain plain data and whose onership does not convey any additional information.