Macro creusot_contracts::macros::ghost

ghost!() { /* proc-macro */ }

Opens a ‘ghost block’.

Ghost blocks are used to execute ghost code: code that will be erased in the normal execution of the program, but could influence the proof.

Note that ghost blocks are subject to some constraints, that ensure the behavior of the code stays the same with and without ghost blocks:

• They may not contain code that crashes or runs indefinitely. In other words, they can only call pure functions.
• All variables that are read in the ghost block must either be Copy, or a GhostBox.
• All variables that are modified in the ghost block must be GhostBoxs.
• The variable returned by the ghost block will automatically be wrapped in a GhostBox.

Example

let x = 1;
let mut g = ghost!(Seq::new()); // g is a zero-sized variable at runtime
ghost! {
    g.push_back_ghost(x);
};