4.1. Simple invariants examples

Here are two simple examples of invariants. The second example Ball Game also highlights a subtle point of using invariants.

A simple example

In the folder simple_voting is a simple voting contract Voting.sol, shown below.

Voting contract

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];
  }
}

A simple invariant of this contract is: votesInFavor + votesAgainst == totalVotes, which we express as an invariant in Voting.spec. The spec also contains two translations of the invariant to a rule, one correct and the other wrong:

Invariant

invariant sumResultsEqualsTotalVotes()
    votesInFavor() + votesAgainst() == to_mathint(totalVotes());

Translation to a rule of the induction step of the invariant

rule sumResultsEqualsTotalVotesAsRule(method f) {
    // Precondition
    require votesInFavor() + votesAgainst() == to_mathint(totalVotes());

    env e;
    calldataarg args;
    f(e, args);
    
    assert (
        votesInFavor() + votesAgainst() == to_mathint(totalVotes()),
        "Sum of votes should equal total votes"
    );
}

Wrong translation of the invariant to a rule

rule sumResultsEqualsTotalVotesWrong() {
    assert (
        votesInFavor() + votesAgainst() == to_mathint(totalVotes()),
        "Sum of votes should equal total votes"
    );
}

Running the Certora Prover verifies the invariant, and also the rule sumResultsEqualsTotalVotesAsRule (which is the translation of the invariant’s induction step translation to a rule). While the naive translation to a rule in sumResultsEqualsTotalVotesWrong fails, since it doesn’t have the necessary precondition.

Note

The invariant has another advantage over the rule besides its brevity – it also verifies the invariant holds after the constructor. In contrast, a parametric rule will not checked for the case where the parametric method is the constructor.

Ball Game