Verification With Ghosts


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


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;