Inductive Properties

Task 3: Write a rule to verify the property

Property: sum of votes in favor and votes against equals total votes.

Tip

We want to prove that this rule always holds when you execute the functions of the contract, in this case vote(). We need to make sure the rule is inductive.

Your first attempt might be wrong

VotingWrongInvariantAsRule.spec

/// @title Total votes is sum of in favor and against - wrong rule
rule totalVotesIsSumWrong(env e) {

    bool isInFavor;
    vote(e, isInFavor);

    assert (
        votesInFavor() + votesAgainst() == totalVotes(),
        "totalVotes is sum of in favor and against"
    );
}

Why is this attempt wrong? It is NOT inductive. The prover assumes arbitrary states to begin with. This is called over-approximation of the set of reachable states. If we start in a state that violates the property, we will end up in a state that violates the property after executing vote(). Here we have to make sure that the prover knows which states are reachable before the execution of a contract function, that is, only states that do not already violate an inductive property.

Solution

An inductive rule

VotingBug2Invariant.spec

/// @title Total votes is sum of in favor and against
rule totalVotesIsSum(env e) {
    require votesInFavor() + votesAgainst() == totalVotes();

    bool isInFavor;
    vote(e, isInFavor);

    assert (
        votesInFavor() + votesAgainst() == totalVotes(),
        "totalVotes is sum of in favor and against"
    );
}

We require that the invariant holds before the execution of vote() and assert that it still holds after.

---

Inductive Invariants

The invariant keyword

CVL allows us to write the above rule in a simpler way that will check that the invariant holds on all external functions of a contract.

VotingInvariant.spec

/// @title Total votes is sum of in favor and against
invariant totalVotesIsSumInvariant()
    votesInFavor() + votesAgainst() == to_mathint(totalVotes());

Structural induction

Mathematically speaking, we induct on the structure of the contract.

Induction base

1. “Run” the constructor.

2. assert the invariant.

Induction step

1. require the invariant.

2. “Run” any function func() from the contract.

3. assert the invariant.

Task 4: Run the invariant spec

• The config is VotingInvariant.conf shown below.

  VotingInvariant.conf

  {
      "files": ["src/Voting.sol:Voting"],
      "verify": "Voting:certora/specs/VotingInvariant.spec",
      "msg": "A simple invariant example"
      // To use a specific Solidity compiler:
      // "solc": "<path-to-compiler>
      // Or add to the command line: --solc <path-to-compiler>,
      "server": "production"
  }
  

• To run the spec, execute the following command:

  certoraRun certora/confs/VotingInvariant.conf
  

• Results link: invariant report.

---

Another bug

Note

This contract also contains an injected bug.

Voting contract with injected bug

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

/// @title A simple voting contract
contract Voting {

    // `_hasVoted[user]` is true if the user voted.
    mapping(address => bool) public hasVoted;

    uint256 public votesInFavor;  // How many in favor
    uint256 public votesAgainst;  // How many opposed
    uint256 public totalVotes;  // Total number voted

    function vote(bool isInFavor) external {
        // The prover ignores reverted computation paths
        require(!hasVoted[msg.sender]);
        hasVoted[msg.sender] = true;

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

---

Exercises

Task 5: Find the second bug

1. Run the spec with the invariant and the rule on VotingBug2.sol. You can use:

   certoraRun certora/confs/VotingBug2.conf
   

2. Find the bug using the rule report.

3. Results link: rule report.

Task 6: Write a new bug

Inject a bug to the Voting contract that will be caught by the invariant totalVotesIsSumInvariant but not by the rule totalVotesIsSum.

Solution

Add a constructor and in it change one of the counters. Here is an example: solution report.

VotingConstructorBug.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

/// @title A simple voting contract
contract Voting {

    // `_hasVoted[user]` is true if the user voted.
    mapping(address => bool) public hasVoted;

    uint256 public votesInFavor;  // How many in favor
    uint256 public votesAgainst;  // How many opposed
    uint256 public totalVotes;  // Total number voted

    constructor() {
      votesInFavor = 1;  // NOTE: injected bug
    }

    function vote(bool isInFavor) external {
        // The prover ignores reverted computation paths
        require(!hasVoted[msg.sender]);
        hasVoted[msg.sender] = true;

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