4.4. Ghosts and hooks¶

Ghost variables¶

Ghost variables are variables defined in CVL that behave like the storage data of the contract being verified. 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 before 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 before the constructor, the boolean condition is true. So, this is only used when preparing to prove an invariant relative to the constructor. An init_state axiom for a ghost variable does not constrain the ghost variable’s possible values when the Prover evaluates a rule nor an invariant relative to any non-constructor function.

Important

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

Here is another simple example that initializes a variable to false:

ghost bool boolGhost {
    init_state axiom !boolGhost;
}

The example below sets the initial value of map(x) to be x when x is even:

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

Important

It may be tempting to copy the boolean condition from an init_state axiom to a require statement in a rule or preserved block to constrain the initial states. But, this is not a good idea because it would exclude all states that include post-constructor changes to the ghost. Some of those states may be valid (i.e. reachable), so excluding them weakens the property and may prevent it from catching a bug. It would be safer to prove a new invariant about the valid states of the ghost and then use requireInvariant wherever needed.

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 been stored in _hasVoted.