This documentation has been moved to https://docs.certora.com/
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;
}