Verification with ghosts

(WIP)

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 _map(uint) returns uint;

‌with the hooks:

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

hook Sstore map[KEY uint k] uint v STORAGE {
    havoc _map assuming _map@new(k) == v &&
        (forall uint k2. k2 != k => _map@new(k2) == _map@old(k2));
}

‌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 array(uint) returns uint;ghost arrayLen() returns uint;

‌We also define the hooks. For array:

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

hook Sstore keys[INDEX uint index] uint n STORAGE {
    havoc array assuming array@new(index) == n &&
        (forall uint i. i != index => array@new(i) == array@old(i));
}

‌For arrayLen:

hook Sstore keys uint lenNew STORAGE {
    // the length of a solidity storage array is at the variable's slot
    havoc arrayLen assuming arrayLen@new() == lenNew;
}

Certora Prover Documentation

This documentation has been moved to https://docs.certora.com/

Verification with ghosts