Ghost code

Often, it is useful to introduce ghost state and ghost code, i.e., additional state and code that is used for specification and verification purposes, but which is not meant to be compiled and executed. Ghost code cannot change the visible behavior of a program, i.e., it cannot assign to non-ghost variables or cause the program to not terminate.

Ghost code is considered by Gobra but it is ignored during compilation. When writing Gobra annotations in Go source files, the syntax // @ makes it clear that the line is treated as a comment by Go and is not included in the program.

Ghost parameters

Consider the function Max that returns the maximum element of an array, with the signature:

// @ ensures forall i int :: 0 <= i && i < len(arr) ==> arr[i] <= res
// @ ensures exists i int :: 0 <= i && i < len(arr) ==> arr[i] == res
func Max(arr [10]int) (res int)

Verifying this function would be challenging because of the existential quantifier. Additionally, the postcondition gives clients only the maximal value.

With a ghost out parameter idx, we can return the index of the maximal value. The updated contract specifies, that the maximal value is at index idx. We update idx with a ghost statement to maintain the invariant that it is the index of the maximal value in the prefix of the array already iterated over. As Max has two out parameters now, clients must assign the ghost return value to a ghost location.

const N = 10

// @ ensures forall i int :: 0 <= i && i < len(arr) ==> arr[i] <= res
// @ ensures 0 <= idx && idx < len(arr) && arr[idx] == res
func Max(arr [N]int) (res int /*@ , ghost idx int @*/) {
    res = arr[0]
    // @ invariant 0 <= i0 && i0 <= N
    // @ invariant forall j int :: 0 <= j && j < i0 ==> arr[j] <= res
    // @ invariant 0 <= idx && idx < N && arr[idx] == res
    for i, a := range arr /*@ with i0 @*/ {
        if a > res {
            res = a
            // @ ghost idx = i
        }
    }
    return res /*@ , idx @*/
}

func client() {
    arr := [10]int{0, 2, 4, 8, 10, 1, 3, 5, 7, 9}
    // @ assert arr[4] == 10
    // @ ghost var idx int
    m, /*@ idx @*/ := Max(arr)
    // @ assert arr[idx] == m
    // @ assert m == 10
}

Ghost erasure property

Recall that ghost code cannot change the visible behavior of a program. Hence, ghost code cannot modify non-ghost locations. For example, the ghost statement x = 1 causes an error since x is a normal variable:

    var x int
    // @ ghost x = 1
    // ...

ERROR ghost error: only ghost locations can be assigned to in ghost code

To make a statement ghost, add ghost before it. Although not all statements can appear in ghost code. For example, there is no ghost return statement, because it can change the visible behavior of a program:

func loop() {
    // @ ghost return
    for {}
}

ERROR ghost error: expected ghostifiable statement

Termination of ghost functions

Ghost functions must be proven to terminate. Calling a non-terminating ghost function could change the visible behavior of a program. For example, the function boo does not terminate with ghost code but returns immediately without ghost code..

/*@
ghost
func inf() {
    for {}
}
@*/

// @ decreases
func boo() int {
    // @ ghost inf()
    return 42
}

ERROR loop occurring in ghost context does not have a termination measure
    for {}
 ^

More ghost entities

In general, Gobra allows marking the following entities as ghost:

• in and out parameters of functions and methods
• functions and methods where all in- and out-parameters are implicitly ghost
• variables ghost var x int = 42
• statements

We will continue using ghost code in the following chapters.