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.

Re-exports

pub use self::perm::PermTarget;

Modules

invariant

Resource invariants.

lifetime_logic

Encoding of Rustbelt’s lifetime logic in Creusot.

perm

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

resource

Resource algebras

Structs

Ghost

A type that can be used in ghost! context.

GhostShared

A type for sharing ghost data immutably.

NotObjective

A guard for potentially subjective types

Traits

FnGhost

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

Objective

An assertion whose meaning is independent of this thread’s view.

Plain

A trait for types that can be extracted from snapshots in ghost code.