Ghost code vs. exec code

The purpose of exec code is to manipulate physically real values — values that exist in physical electronic circuits when a program runs. The purpose of ghost code, on the other hand, is merely to talk about the values that exec code manipulates. In a sense, this gives ghost code supernatural abilities: ghost code can talk about things that could not be physically implemented at run-time. We’ve already seen one example of this with the types int and nat, which can only be used in ghost code. As another example, ghost code can talk about the result of division by zero:

fn divide_by_zero() {
    let x: u8 = 1;
    assert(x / 0 == x / 0); // succeeds in ghost code
    let y = x / 0; // FAILS in exec code
}

This simply reflects the SMT solver’s willingness to reason about the result of division by zero as an unspecified integer value. By contrast, Verus reports a verification failure if exec code attempts to divide by zero:

error: possible division by zero
    |
    |     let y = x / 0; // FAILS
    |             ^^^^^

Two particular abilities of ghost code¹ are worth keeping in mind:

• Ghost code can copy values of any type, even if the type doesn’t implement the Rust Copy trait.
• Ghost code can create a value of any type², even if the type has no public constructors (e.g. even if the type is struct whose fields are all private to another module).

For example, the following spec functions create and duplicate values of type S, defined in another module with private fields and without the Copy trait:

mod MA {
    // does not implement Copy
    // does not allow construction by other modules
    pub struct S {
        private_field: u8,
    }

}

mod MB {
    use builtin::*;
    use crate::MA::*;

    // construct a ghost S
    spec fn make_S() -> S;

    // duplicate an S
    spec fn duplicate_S(s: S) -> (S, S) {
        (s, s)
    }
}

These operations are not allowed in exec code. Furthermore, values from ghost code are not allowed to leak into exec code — what happens in ghost code stays in ghost code. Any attempt to use a value from ghost code in exec code will result in a compile-time error:

fn test(s: S) {
    let pair = duplicate_S(s); // FAILS
}

error: cannot call function with mode spec
    |
    |         let pair = duplicate_S(s); // FAILS
    |                    ^^^^^^^^^^^^^^

As an example of ghost code that uses these abilities, a call to the Verus Seq::index(...) function can duplicate a value from the sequence, if the index i is within bounds, and create a value out of thin air if i is out of bounds:

impl<A> Seq<A> {
...
    /// Gets the value at the given index `i`.
    ///
    /// If `i` is not in the range `[0, self.len())`, then the resulting value
    /// is meaningless and arbitrary.

    pub spec fn index(self, i: int) -> A
        recommends 0 <= i < self.len();
...
}