Ghost code

Sometimes, you may need code that will be used only in the proofs/specification, that yet still obeys the typing rules of Rust. In this case, snapshots are not enough, since they don't have lifetimes or ownership.

This is why there exists a separate mechanism: ghost code.

ghost! and GhostBox<T> are the counterparts of snapshot! and Snapshot<T>.

ghost! blocks

At any point in the code, you may open a ghost! block:

#![allow(unused)]
fn main() {
ghost! {
    // code here
}
}

In ghost! block, you may write any kind of Rust code, with the following restrictions :

• ghost code must terminate (see termination for details)
• all functions called must have the #[pure] attribute
• When reading an outer variable, the variable must be a GhostBox<T>, or implement Copy
• When writing an outer variable, the variable must be a GhostBox<T>
• The output of the ghost! block will automatically be wrapped in GhostBox::new

Those restriction exists to ensure that ghost code is erasable: its presence or absence does not affect the semantics of the actual running program, only the proofs.

GhostBox<T>

The GhostBox<T> type is the type of "ghost data". In Creusot, it acts like a Box<T>, while in normal running code, it is an empty type. It has the same View as the underlying type, meaning you can use the @ operator directly.

The only restriction of GhostBox<T> is that it may not be dereferenced nor created in non-ghost code.

Examples

• Creating and modifying a ghost variable:

#![allow(unused)]
fn main() {
let mut g = ghost!(50);
ghost! {
    *g *= 2;
};
proof_assert!(g@ == 100);
}

• Calling a function in ghost code:

#![allow(unused)]
fn main() {
#[pure]
#[requires(*g < i32::MAX)]
#[ensures((^g)@ == (*g)@ + 1)]
fn add_one(g: &mut i32) {
    *g += 1;
}

let mut g = ghost!(41);
ghost! {
    add_one(&mut *g);
};
proof_assert!(g@ == 42);
}

• Using a ghost access token:

#![allow(unused)]
fn main() {
struct Token;

struct Data {
    // ...
}

impl Data {
    fn new() -> (Data, GhostBox<Token>) { /* */ }
    fn read(&self, token: &GhostBox<Token>) -> T { /* */ }
    fn write(&self, t: T, token: &mut GhostBox<Token>) { /* */ }
}
}