4.4. Ghosts and hooks

Ghost variables

Ghost variables are variables defined in CVL that behave like the verified contract’s storage data. For example, they revert when the storage reverts, and they can be set to specific values after the constructor. They can be directly accessed from the spec, both to read and to write.

Examples

Defining a ghost variables of different types

ghost mathint numVoted;
ghost mapping(address => uint256) balanceGhost;

Setting initial state

To set the initial value of a ghost variable (i.e. its value after the constructor), we use the following syntax:

Defining a ghost variable’s initial state as zero

ghost mathint someGhost {
    init_state axiom someGhost == 0;
}

The expression init_state axiom <boolean condition>; ensures that immediately after the constructor, the boolean condition would be true. Note, however, that at any other time its value is not constrained.

Important

The <boolean condition> expression may not contain calls to solidity functions.

Here is another simple example:

ghost bool boolGhost {
    init_state axiom !boolGhost;
}

The example below sets the value of func(x) to be x whenever x is even:

ghost mapping(uint256 => uint256) func {
    init_state axiom forall uint256 x. (x % 2 == 0) => (func(x) == x);
}

Storage hooks

Storage hooks allow us to inject CVL code whenever a storage variable is accessed, whether for read or write. The syntax is detailed in the Hooks documentation. One use for storage hooks is to update ghost variables.

Example

Consider the simple voting contract from Voting.sol shown below.

contract Voting {

  mapping(address => bool) internal _hasVoted;

  uint256 public votesInFavor;
  uint256 public votesAgainst;
  uint256 public totalVotes;

  function vote(bool isInFavor) public {
    require(!_hasVoted[msg.sender]);
    _hasVoted[msg.sender] = true;

    totalVotes += 1;
    if (isInFavor) {
      votesInFavor += 1;
    } else {
      votesAgainst += 1;
    }
  }

  function hasVoted(address voter) public view returns (bool) {
    return _hasVoted[voter];
  }
}

We want to prove that the number of times _hasVoted is updated equals totalVotes. To do this we define a ghost variable numVoted that is updated every time the _hasVoted mapping is modified. This allows us to count the number of times values in _hasVoted changed from false to true.

ghost mathint numVoted {
    // No votes at start
    init_state axiom numVoted == 0;
}

hook Sstore _hasVoted[KEY address voter]
    bool newVal (bool oldVal) {
    numVoted = numVoted + 1;
}

/// @title Total voted intergrity
invariant sumResultsEqualsTotalVotes()
     to_mathint(totalVotes()) == numVoted;

To be precise, the invariant sumResultsEqualsTotalVotes means that totalVotes equals the number of times a value has changed from false to true in _hasVoted.