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

invariant

Define atomic and non-atomic invariants.

perm

Generic permissions for accessing memory pointed to by pointers or within an interior mutable type.

resource

Resource algebras

Structs

Committer

Wrapper around a single atomic operation, where multiple ghost steps can be performed.

Ghost

A type that can be used in ghost! context.

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.