Module creusot_contracts::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: GhostBox<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 GhostBox and ghost! for more details.

Structs

• GhostBox
  A type that can be used in ghost context.