Verification With Ghosts

(WIP)

In the last section, we presented the idea of ghosts for proving the invariant:

$$∀x.(map(x)≠0⟺∃i.0≤i≤keys.length∧keys[i]=x)$$

And we have already defined a ghost for the underlying map:

ghost mapping(uint => uint) _map;

with the hooks:

hook Sload uint v map[KEY uint k] {
    require _map[k] == v;
}

hook Sstore map[KEY uint k] uint v {
    _map[k] = v;
}

We continue with defining two additional ghosts: one capturing the length of the array, and the second for remembering the elements of the array:

ghost mapping(uint => uint) array; ghost uint arrayLen;

We also define the hooks. For array:

hook Sload uint n keys[INDEX uint index] {
    require array[index] == n;
}

hook Sstore keys[INDEX uint index] uint n {
    array[index] = n;
}

For arrayLen:

hook Sstore keys uint lenNew {
    // the length of a solidity storage array is at the variable's slot
    arrayLen = lenNew;
}