Add Certora's Governance verification rules (#2997)

Co-authored-by: Shelly Grossman <shelly@certora.com>
Co-authored-by: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Co-authored-by: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Co-authored-by: Aleksander Kryukov <firealexkryukov@gmail.com>

.gitignore

@@ -57,3 +57,8 @@ allFiredEvents
 # hardhat
 cache
 artifacts
+
+# Certora
+.certora*
+.last_confs
+certora_*

certora/Makefile

+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../contracts
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+

certora/README.md

+# Running the certora verification tool
+
+These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts.
+
+Documentation for CVT and the specification language are available
+[here](https://certora.atlassian.net/wiki/spaces/CPD/overview)
+
+## Running the verification
+
+The scripts in the `certora/scripts` directory are used to submit verification
+jobs to the Certora verification service. After the job is complete, the results will be available on
+[the Certora portal](https://vaas-stg.certora.com/).
+
+These scripts should be run from the root directory; for example by running
+
+```
+sh certora/scripts/verifyAll.sh <meaningful comment>
+```
+
+The most important of these is `verifyAll.sh`, which checks
+all of the harnessed contracts (`certora/harness/Wizard*.sol`) against all of
+the specifications (`certora/spec/*.spec`).
+
+The other scripts run a subset of the specifications or the contracts.  You can
+verify different contracts or specifications by changing the `--verify` option,
+and you can run a single rule or method with the `--rule` or `--method` option.
+
+For example, to verify the `WizardFirstPriority` contract against the
+`GovernorCountingSimple` specification, you could change the `--verify` line of
+the `WizardControlFirstPriortity.sh` script to:
+
+```
+--verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \
+```
+
+## Adapting to changes in the contracts
+
+Some of our rules require the code to be simplified in various ways. Our
+primary tool for performing these simplifications is to run verification on a
+contract that extends the original contracts and overrides some of the methods.
+These "harness" contracts can be found in the `certora/harness` directory.
+
+This pattern does require some modifications to the original code: some methods
+need to be made virtual or public, for example. These changes are handled by
+applying a patch to the code before verification.
+
+When one of the `verify` scripts is executed, it first applies the patch file
+`certora/applyHarness.patch` to the `contracts` directory, placing the output
+in the `certora/munged` directory. We then verify the contracts in the
+`certora/munged` directory.
+
+If the original contracts change, it is possible to create a conflict with the
+patch. In this case, the verify scripts will report an error message and output
+rejected changes in the `munged` directory. After merging the changes, run
+`make record` in the `certora` directory; this will regenerate the patch file,
+which can then be checked into git.

certora/applyHarness.patch

+diff -ruN .gitignore .gitignore
+--- .gitignore	1969-12-31 19:00:00.000000000 -0500
++++ .gitignore	2021-12-09 14:46:33.923637220 -0500
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol
+--- governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/compatibility/GovernorCompatibilityBravo.sol	2021-12-09 14:46:33.923637220 -0500
+@@ -245,7 +245,7 @@
+     /**
+      * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
+      */
+-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
++    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
+         ProposalDetails storage details = _proposalDetails[proposalId];
+         return quorum(proposalSnapshot(proposalId)) <= details.forVotes;
+     }
+@@ -253,7 +253,7 @@
+     /**
+      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
+      */
+-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
++    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
+         ProposalDetails storage details = _proposalDetails[proposalId];
+         return details.forVotes > details.againstVotes;
+     }
+diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
+--- governance/extensions/GovernorCountingSimple.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/extensions/GovernorCountingSimple.sol	2021-12-09 14:46:33.923637220 -0500
+@@ -64,7 +64,7 @@
+     /**
+      * @dev See {Governor-_quorumReached}.
+      */
+-    function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
++    function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
+         ProposalVote storage proposalvote = _proposalVotes[proposalId];
+ 
+         return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
+@@ -73,7 +73,7 @@
+     /**
+      * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
+      */
+-    function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
++    function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
+         ProposalVote storage proposalvote = _proposalVotes[proposalId];
+ 
+         return proposalvote.forVotes > proposalvote.againstVotes;
+diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol
+--- governance/extensions/GovernorTimelockControl.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/extensions/GovernorTimelockControl.sol	2021-12-09 14:46:33.923637220 -0500
+@@ -111,7 +111,7 @@
+         bytes[] memory calldatas,
+         bytes32 descriptionHash
+     ) internal virtual override {
+-        _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
++         _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
+     }
+ 
+     /**
+diff -ruN governance/Governor.sol governance/Governor.sol
+--- governance/Governor.sol	2021-12-03 15:24:56.523654357 -0500
++++ governance/Governor.sol	2021-12-09 14:46:56.411503587 -0500
+@@ -38,8 +38,8 @@
+ 
+     string private _name;
+ 
+-    mapping(uint256 => ProposalCore) private _proposals;
+-
++    mapping(uint256 => ProposalCore) public _proposals;
++ 
+     /**
+      * @dev Restrict access to governor executing address. Some module might override the _executor function to make
+      * sure this modifier is consistant with the execution model.
+@@ -167,12 +167,12 @@
+     /**
+      * @dev Amount of votes already cast passes the threshold limit.
+      */
+-    function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
++    function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+ 
+     /**
+      * @dev Is the proposal successful or not.
+      */
+-    function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
++    function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
+ 
+     /**
+      * @dev Register a vote with a given support and voting weight.
+diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
+--- token/ERC20/extensions/ERC20Votes.sol	2021-12-03 15:24:56.527654330 -0500
++++ token/ERC20/extensions/ERC20Votes.sol	2021-12-09 14:46:33.927637196 -0500
+@@ -84,7 +84,7 @@
+      *
+      * - `blockNumber` must have been already mined
+      */
+-    function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) {
++    function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) {
+         require(blockNumber < block.number, "ERC20Votes: block not yet mined");
+         return _checkpointsLookup(_checkpoints[account], blockNumber);
+     }

certora/harnesses/ERC20VotesHarness.sol

+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesHarness is ERC20Votes {
+    constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
+
+    mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
+
+    function _afterTokenTransfer(
+        address from,
+        address to,
+        uint256 amount
+    ) internal virtual override {
+        super._afterTokenTransfer(from, to, amount);
+        _getPastVotes[from][block.number] -= amount;
+        _getPastVotes[to][block.number] += amount;
+    }
+
+    /**
+     * @dev Change delegation for `delegator` to `delegatee`.
+     *
+     * Emits events {DelegateChanged} and {DelegateVotesChanged}.
+     */
+    function _delegate(address delegator, address delegatee) internal virtual override{
+        super._delegate(delegator, delegatee);
+        _getPastVotes[delegator][block.number] -= balanceOf(delegator);
+        _getPastVotes[delegatee][block.number] += balanceOf(delegator);
+    }
+}

certora/harnesses/WizardControlFirstPriority.sol

+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/governance/extensions/GovernorTimelockControl.sol";
+import "../munged/governance/extensions/GovernorProposalThreshold.sol";
+
+/* 
+Wizard options:
+ProposalThreshhold = 10
+ERC20Votes
+TimelockController
+*/
+
+contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
+    constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
+        Governor(name)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumFraction)
+        GovernorTimelockControl(_timelock)
+    {}
+
+    //HARNESS
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    uint256 _votingDelay;
+
+    uint256 _votingPeriod;
+
+    uint256 _proposalThreshold;
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason
+    ) internal override virtual returns (uint256) {
+        
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;        
+    }
+    
+    function snapshot(uint256 proposalId) public view returns (uint64) {
+        return _proposals[proposalId].voteStart._deadline;
+    }
+
+
+    function getExecutor() public view returns (address){
+        return _executor();
+    }
+
+    // original code, harnessed
+
+    function votingDelay() public view override returns (uint256) {     // HARNESS: pure -> view
+        return _votingDelay;                                            // HARNESS: parametric
+    }
+
+    function votingPeriod() public view override returns (uint256) {    // HARNESS: pure -> view
+        return _votingPeriod;                                           // HARNESS: parametric
+    }
+
+    function proposalThreshold() public view override returns (uint256) {   // HARNESS: pure -> view
+        return _proposalThreshold;                                          // HARNESS: parametric
+    }
+
+    // original code, not harnessed
+    // The following functions are overrides required by Solidity.
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function getVotes(address account, uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotes)
+        returns (uint256)
+    {
+        return super.getVotes(account, blockNumber);
+    }
+
+    function state(uint256 proposalId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (ProposalState)
+    {
+        return super.state(proposalId);
+    }
+
+    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
+        public
+        override(Governor, GovernorProposalThreshold, IGovernor)
+        returns (uint256)
+    {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockControl)
+    {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockControl)
+        returns (uint256)
+    {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor()
+        internal
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (address)
+    {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockControl)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/harnesses/WizardFirstTry.sol

+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/governance/extensions/GovernorTimelockCompound.sol";
+
+/* 
+Wizard options:
+ERC20Votes
+TimelockCompound
+*/
+
+contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
+    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
+        Governor(name)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumFraction)
+        GovernorTimelockCompound(_timelock)
+    {}
+
+    //HARNESS
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    function snapshot(uint256 proposalId) public view returns (uint64) {
+        return _proposals[proposalId].voteStart._deadline;
+    }
+
+    function getExecutor() public view returns (address){
+        return _executor();
+    }
+
+    uint256 _votingDelay;
+
+    uint256 _votingPeriod;
+
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason
+    ) internal override virtual returns (uint256) {
+        
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason);  //HARNESS
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
+
+        return deltaWeight;        
+    }
+
+    // original code, harnessed
+
+    function votingDelay() public view override virtual returns (uint256) {     // HARNESS: pure -> view
+        return _votingDelay;                                                    // HARNESS: parametric
+    }
+
+    function votingPeriod() public view override virtual returns (uint256) {    // HARNESS: pure -> view
+        return _votingPeriod;                                                   // HARNESS: parametric
+    }
+
+    // original code, not harnessed
+    // The following functions are overrides required by Solidity.
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(blockNumber);
+    }
+
+    function getVotes(address account, uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotes)
+        returns (uint256)
+    {
+        return super.getVotes(account, blockNumber);
+    }
+
+    function state(uint256 proposalId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (ProposalState)
+    {
+        return super.state(proposalId);
+    }
+
+    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
+        public
+        override(Governor, IGovernor)
+        returns (uint256)
+    {
+        return super.propose(targets, values, calldatas, description);
+    }
+
+    function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+    {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+        returns (uint256)
+    {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor()
+        internal
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (address)
+    {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/munged/.gitignore

+*
+!.gitignore

certora/scripts/Governor.sh

+make -C certora munged
+
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
+    --verify GovernorHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.0 \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule voteStartBeforeVoteEnd \
+    --msg "$1"

certora/scripts/GovernorCountingSimple-counting.sh

+make -C certora munged
+
+certoraRun  certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
+    --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
+    --solc solc8.2 \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule hasVotedCorrelation \
+    --msg "$1"

certora/scripts/WizardControlFirstPriority.sh

+make -C certora munged
+
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
+    --link WizardControlFirstPriority:token=ERC20VotesHarness \
+    --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --disableLocalTypeChecking \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule canVoteDuringVotingPeriod \
+    --msg "$1"

certora/scripts/WizardFirstTry.sh

+make -C certora munged
+
+certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
+    --verify WizardFirstTry:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --staging shelly/forSasha \
+    --optimistic_loop \
+    --disableLocalTypeChecking \
+    --settings -copyLoopUnroll=4 \
+    --msg "$1"

certora/scripts/sanity.sh

+make -C certora munged
+
+for f in certora/harnesses/Wizard*.sol
+do
+    echo "Processing $f"
+    file=$(basename $f)
+    echo ${file%.*}
+    certoraRun certora/harnesses/$file \
+    --verify ${file%.*}:certora/specs/sanity.spec "$@" \
+    --solc solc8.2 --staging shelly/forSasha \
+    --optimistic_loop \
+    --msg "checking sanity on ${file%.*}"
+    --settings -copyLoopUnroll=4
+done

certora/scripts/verifyAll.sh

+#!/bin/bash
+
+make -C certora munged
+
+for contract in certora/harnesses/Wizard*.sol;
+do
+    for spec in certora/specs/*.spec;
+    do      
+        contractFile=$(basename $contract)
+        specFile=$(basename $spec)
+        if [[ "${specFile%.*}" != "RulesInProgress" ]];
+        then
+            echo "Processing ${contractFile%.*} with $specFile"
+            if [[ "${contractFile%.*}" = *"WizardControl"* ]];
+            then
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --link ${contractFile%.*}:token=ERC20VotesHarness \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc8.2 \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            else
+                certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \
+                --verify ${contractFile%.*}:certora/specs/$specFile "$@" \
+                --solc solc8.2 \
+                --staging shelly/forSasha \
+                --disableLocalTypeChecking \
+                --optimistic_loop \
+                --settings -copyLoopUnroll=4 \
+                --send_only \
+                --msg "checking $specFile on ${contractFile%.*}"
+            fi
+        fi
+    done
+done

certora/specs/GovernorCountingSimple.spec

+import "GovernorBase.spec"
+
+using ERC20VotesHarness as erc20votes
+
+methods {
+    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
+
+    quorum(uint256) returns uint256
+    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
+
+    quorumNumerator() returns uint256
+    _executor() returns address
+
+    erc20votes._getPastVotes(address, uint256) returns uint256
+
+    getExecutor() returns address
+
+    timelock() returns address
+}
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// GHOSTS /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+//////////// ghosts to keep track of votes counting ////////////
+
+/*
+ * the sum of voting power of those who voted
+ */
+ghost sum_all_votes_power() returns uint256 {
+	init_state axiom sum_all_votes_power() == 0;
+}
+
+hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
+	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
+}
+
+/*
+ * sum of all votes casted per proposal
+ */
+ghost tracked_weight(uint256) returns uint256 {
+	init_state axiom forall uint256 p. tracked_weight(p) == 0;
+}
+
+/*
+ * sum of all votes casted
+ */
+ghost sum_tracked_weight() returns uint256 {
+	init_state axiom sum_tracked_weight() == 0;
+}
+
+/*
+ * getter for _proposalVotes.againstVotes
+ */
+ghost votesAgainst() returns uint256 {
+    init_state axiom votesAgainst() == 0;
+}
+
+/*
+ * getter for _proposalVotes.forVotes
+ */
+ghost votesFor() returns uint256 {
+    init_state axiom votesFor() == 0;
+}
+
+/*
+ * getter for _proposalVotes.abstainVotes
+ */
+ghost votesAbstain() returns uint256 {
+    init_state axiom votesAbstain() == 0;
+}
+
+hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
+	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
+	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
+	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
+    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
+}
+
+hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
+	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
+	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
+	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
+    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
+}
+
+hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
+	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
+	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
+	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
+    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
+}
+
+
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////// INVARIANTS ////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+/*
+ * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
+ */
+invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) 
+	tracked_weight(pId) == ghost_sum_vote_power_by_id(pId)
+
+
+/*
+ * sum of all votes casted is equal to the sum of voting power of those who voted
+ */
+invariant SumOfVotesCastEqualSumOfPowerOfVoted() 
+	sum_tracked_weight() == sum_all_votes_power()
+
+
+/*
+* sum of all votes casted is greater or equal to the sum of voting power of those who voted at a specific proposal
+*/
+invariant OneIsNotMoreThanAll(uint256 pId) 
+	sum_all_votes_power() >= tracked_weight(pId)
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// RULES //////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+/*
+ * Only sender's voting status can be changed by execution of any cast vote function
+ */
+// Checked for castVote only. all 3 castVote functions call _castVote, so the completness of the verification is counted on
+ // the fact that the 3 functions themselves makes no chages, but rather call an internal function to execute.
+ // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
+ // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
+ // We could check each function seperately and pass the rule, but that would have uglyfied the code with no concrete 
+ // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
+rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) {
+    env e; calldataarg args;
+
+    address voter = e.msg.sender;
+    address user;
+
+    bool hasVotedBefore_User = hasVoted(e, pId, user);
+
+    castVote@withrevert(e, pId, sup);
+    require(!lastReverted);
+
+    bool hasVotedAfter_User = hasVoted(e, pId, user);
+
+    assert user != voter => hasVotedBefore_User == hasVotedAfter_User;
+}
+
+
+/*
+* Total voting tally is monotonically non-decreasing in every operation 
+*/
+rule votingWeightMonotonicity(method f){
+    uint256 votingWeightBefore = sum_tracked_weight();
+
+    env e; 
+    calldataarg args;
+    f(e, args);
+
+    uint256 votingWeightAfter = sum_tracked_weight();
+
+    assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow";
+}
+
+
+/*
+* A change in hasVoted must be correlated with an non-decreasing of the vote supports (nondecrease because user can vote with weight 0)
+*/
+rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
+    address acc = e.msg.sender;
+    
+    uint256 againstBefore = votesAgainst();
+    uint256 forBefore = votesFor();
+    uint256 abstainBefore = votesAbstain();
+
+    bool hasVotedBefore = hasVoted(e, pId, acc);
+
+    helperFunctionsWithRevert(pId, f, e);
+    require(!lastReverted);
+
+    uint256 againstAfter = votesAgainst();
+    uint256 forAfter = votesFor();
+    uint256 abstainAfter = votesAbstain();
+    
+    bool hasVotedAfter = hasVoted(e, pId, acc);
+
+    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
+}
+
+
+/*
+* Only privileged users can execute privileged operations, e.g. change _quorumNumerator or _timelock
+*/
+rule privilegedOnlyNumerator(method f, uint256 newQuorumNumerator){
+    env e;
+    calldataarg arg;
+    uint256 quorumNumBefore = quorumNumerator(e);
+
+    f(e, arg);
+
+    uint256 quorumNumAfter = quorumNumerator(e);
+    address executorCheck = getExecutor(e);
+
+    assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non priveleged user changed quorum numerator";
+}
+
+rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){
+    env e;
+    calldataarg arg;
+    uint256 timelockBefore = timelock(e);
+
+    f(e, arg);
+
+    uint256 timelockAfter = timelock(e);
+
+    assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non priveleged user changed timelock";
+}

certora/specs/RulesInProgress.spec

+//////////////////////////////////////////////////////////////////////////////
+////////////// THIS SPEC IS A RESERVE FOR NOT IN PROGRESS //////////////
+//////////////////////////////////////////////////////////////////////////////
+
+import "GovernorBase.spec"
+
+using ERC20VotesHarness as erc20votes
+
+methods {
+    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
+
+    quorum(uint256) returns uint256
+    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
+
+    quorumNumerator() returns uint256
+    _executor() returns address
+
+    erc20votes._getPastVotes(address, uint256) returns uint256
+
+    getExecutor() returns address
+
+    timelock() returns address
+}
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// GHOSTS /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+//////////// ghosts to keep track of votes counting ////////////
+
+/*
+ * the sum of voting power of those who voted
+ */
+ghost sum_all_votes_power() returns uint256 {
+	init_state axiom sum_all_votes_power() == 0;
+}
+
+hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
+	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
+}
+
+/*
+ * sum of all votes casted per proposal
+ */
+ghost tracked_weight(uint256) returns uint256 {
+	init_state axiom forall uint256 p. tracked_weight(p) == 0;
+}
+
+/*
+ * sum of all votes casted
+ */
+ghost sum_tracked_weight() returns uint256 {
+	init_state axiom sum_tracked_weight() == 0;
+}
+
+/*
+ * getter for _proposalVotes.againstVotes
+ */
+ghost votesAgainst() returns uint256 {
+    init_state axiom votesAgainst() == 0;
+}
+
+/*
+ * getter for _proposalVotes.forVotes
+ */
+ghost votesFor() returns uint256 {
+    init_state axiom votesFor() == 0;
+}
+
+/*
+ * getter for _proposalVotes.abstainVotes
+ */
+ghost votesAbstain() returns uint256 {
+    init_state axiom votesAbstain() == 0;
+}
+
+hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
+	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
+	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
+	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
+    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
+}
+
+hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
+	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
+	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
+	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
+    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
+}
+
+hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
+	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
+	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
+	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
+    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
+}
+
+
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////// INVARIANTS ////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+
+//////////////////////////////////////////////////////////////////////////////
+///////////////////////////////// RULES //////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+
+//NOT FINISHED
+/*
+* the sum of voting power of those who voted is less or equal to the maximum possible votes, per each proposal
+*/
+rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
+
+    // add requireinvariant  for all i, j. i = i - 1 && i < j => checkpointlookup[i] < checkpointlookup[j];
+    require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId));
+
+    uint256 againstB;
+    uint256 forB;
+    uint256 absatinB;
+    againstB, forB, absatinB = proposalVotes(pId);
+
+    calldataarg args;
+    //f(e, args);
+
+    castVote(e, pId, sup);
+
+    uint256 against;
+    uint256 for;
+    uint256 absatin;
+    against, for, absatin = proposalVotes(pId);
+
+    uint256 ps = proposalSnapshot(pId);
+
+    assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
+}
\ No newline at end of file

certora/specs/sanity.spec

+/*
+This rule looks for a non-reverting execution path to each method, including those overridden in the harness.
+A method has such an execution path if it violates this rule.
+How it works:
+    - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails.
+    - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously.
+*/
+	
+rule sanity(method f) {
+    env e;
+    calldataarg arg;
+    f(e, arg);
+    assert false;
+}
\ No newline at end of file