Power voting

Revisiting the Voting Contract

1. Each voter now has voting power according to their token balance (a multi contract setup).

2. To prevent the same funds being used in subsequent votes, the voter’s balance is transferred to the PowerVoting contract.

3. The funds will be released to the voter when voting is ended (to be implemented).

PowerVoting code

PowerVoting.sol

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

import {MinimalToken} from "./MinimalTokenFixed.sol";

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

    MinimalToken public token;

    bool public isVotingEnded;

    // How much was transferred when voting
    mapping(address => uint256) amountVoted;

    // `_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

    function totalVotes() public view returns (uint256) {
        return token.balanceOf(address(this));
    }

    function endVoting() public {
        require(!isVotingEnded, "Already ended");
        isVotingEnded = true;
    }

    function vote(bool isInFavor) external {
        require(!isVotingEnded, "Voting ended");
        require(!hasVoted[msg.sender]);
        require(msg.sender != address(this), "Self voting");
        hasVoted[msg.sender] = true;

        uint256 power = token.balanceOf(msg.sender);

        // Take the money to prevent voting twice with it
        token.transferFrom(msg.sender, address(this), power);
        amountVoted[msg.sender] += power;

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

---

Spec

• The spec is PowerVoting.spec.

• It contains two rules we’ve seen before.

• The CVL keyword using allows us to refer to instances of certain contracts. For example:

  using MinimalToken as token;
  
  rule (...) {
      ...
      assert token.balanceOf(user) >= 10;
  }
  

PowerVoting spec

PowerVoting.spec

/* Verification of the `PowerVoting` contract */

using MinimalToken as token;

methods {
    // Declares the getters for the public state variables as `envfree`
    function totalVotes() external returns (uint256) envfree;
    function votesInFavor() external returns (uint256) envfree;
    function votesAgainst() external returns (uint256) envfree;

    // Declares function so can be called from the spec via, `token.balanceOf(a)`
    function MinimalToken.balanceOf(address) external returns (uint256) envfree;
}


/// @title Integrity of vote
rule voteIntegrity(bool isInFavor) {
    uint256 votedBefore = totalVotes();

    env e;
    vote(e, isInFavor);

    assert (
        totalVotes() > votedBefore,
        "totalVotes increases after voting"
    );
}


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

---

Exercises

Task 8: Fixing voteIntegrity

• Use the config PowerVoting.conf.

• Results link: rule report.

1. Fix the voteIntegrity rule - it should consider all possible cases.

2. Rerun and check that both rules pass now.

Hints

• Use the implication logical operator =>, whose meaning is “if condition then …”.

• If a rule contains several assert clauses, then all of them must hold.

Solution

• The violation of the rule voteIntegrity occurs when the voter has a balance of zero. We can either require the voter’s balance to be non-zero, or assert that the total votes increase only if the voter’s balance is non-zero.

• To also handle the case where the voter’s balance is zero, we can divide into two cases:

  1. If the voter’s balance is zero then the total votes is unchanged.

  2. Otherwise the votes must increase.

Here is the report using the fixed spec: solution report.

Fixed spec

/* Verification of the `PowerVoting` contract */

using MinimalToken as token;

methods {
    // Declares the getters for the public state variables as `envfree`
    function totalVotes() external returns (uint256) envfree;
    function votesInFavor() external returns (uint256) envfree;
    function votesAgainst() external returns (uint256) envfree;

    // Declares function so can be called from the spec via, `token.balanceOf(a)`
    function MinimalToken.balanceOf(address) external returns (uint256) envfree;
}


/// @title Integrity of vote
rule voteIntegrity(bool isInFavor) {
    uint256 votedBefore = totalVotes();

    env e;
    uint256 voterBalance = token.balanceOf(e.msg.sender);
    vote(e, isInFavor);

    assert (
        (voterBalance > 0) => totalVotes() > votedBefore,
        "totalVotes increases after voting"
    );
    assert (
        (voterBalance == 0) => totalVotes() == votedBefore,
        "if voter has no funds then totalVotes is unchanged"
    );
}


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

Task 9: Advanced CVL constructs

• Rerun the spec removing the "parametric_contracts" field. This allows the Prover to use any function from any contract in the induction step of an invariant.

• The Prover will find violations in the totalVotesIsSumInvariant invariant, such as in unlimited parametric report.

1. What is the source of these violations?

2. Can you think of ways to fix them?

Solution

The violations occur in any function of MinimalToken that

• can transfer funds to the address of PowerVoting, i.e. donations, or

• when PowerVoting itself transfers funds to someone else.

There are multiple solutions to fix this issue. Under the assumption that PowerVoting is a safe contract that will not maliciously transfer funds to anyone, we can tell the prover to assume certain things about the program states it considers when verifying the invariant.

To this end, we use so-called preserved{} blocks that can include

• general assumptions for the execution of all functions or

• specific requirements on a per-method basis

Here is run link with the following solution:

PowerVotingAdvanced.spec

/// @title Total votes is sum of in favor and against
invariant totalVotesIsSumInvariant()
    votesInFavor() + votesAgainst() == to_mathint(totalVotes())
    {
        preserved with (env e) {
            // assumptions for the prover when "executing" any contract method
            require e.msg.sender != currentContract;
        }
        preserved token.transfer(address to, uint256 amount) with (env e) {
            // assumptions for the prover when "executing" a specific contract method
            require e.msg.sender != currentContract;
            require to != currentContract;
        }
        preserved token.transferFrom(address from, address to, uint256 amount) with (env e) {
            require from != currentContract;
            require to != currentContract;
        }
    }

Note

This example introduces a new CVL keyword currentContract. We can use this keyword to refer to the contract we’re verifying, specified in the conf file under verify. In this case, currentContract is PowerVoting.

"verify": "PowerVoting:certora/specs/PowerVotingSolution.spec"