From 915ca181baa8c284bd226509dfbd461999627a71 Mon Sep 17 00:00:00 2001 From: "Michael D. George" Date: Mon, 27 Dec 2021 17:11:59 -0500 Subject: [PATCH] Add Certora's Governance verification rules (#2997) Co-authored-by: Shelly Grossman 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 --- .gitignore | 5 + certora/Makefile | 24 ++ certora/README.md | 56 +++ certora/applyHarness.patch | 101 ++++++ certora/harnesses/ERC20VotesHarness.sol | 28 ++ .../harnesses/WizardControlFirstPriority.sol | 150 ++++++++ certora/harnesses/WizardFirstTry.sol | 141 ++++++++ certora/munged/.gitignore | 2 + certora/scripts/Governor.sh | 10 + .../GovernorCountingSimple-counting.sh | 10 + certora/scripts/WizardControlFirstPriority.sh | 12 + certora/scripts/WizardFirstTry.sh | 10 + certora/scripts/sanity.sh | 14 + certora/scripts/verifyAll.sh | 39 ++ certora/specs/GovernorBase.spec | 334 ++++++++++++++++++ certora/specs/GovernorCountingSimple.spec | 221 ++++++++++++ certora/specs/RulesInProgress.spec | 139 ++++++++ certora/specs/sanity.spec | 14 + 18 files changed, 1310 insertions(+) create mode 100644 certora/Makefile create mode 100644 certora/README.md create mode 100644 certora/applyHarness.patch create mode 100644 certora/harnesses/ERC20VotesHarness.sol create mode 100644 certora/harnesses/WizardControlFirstPriority.sol create mode 100644 certora/harnesses/WizardFirstTry.sol create mode 100644 certora/munged/.gitignore create mode 100755 certora/scripts/Governor.sh create mode 100644 certora/scripts/GovernorCountingSimple-counting.sh create mode 100644 certora/scripts/WizardControlFirstPriority.sh create mode 100644 certora/scripts/WizardFirstTry.sh create mode 100644 certora/scripts/sanity.sh create mode 100644 certora/scripts/verifyAll.sh create mode 100644 certora/specs/GovernorBase.spec create mode 100644 certora/specs/GovernorCountingSimple.spec create mode 100644 certora/specs/RulesInProgress.spec create mode 100644 certora/specs/sanity.spec diff --git a/.gitignore b/.gitignore index 0a62cf0b3..c60c5d945 100644 --- a/.gitignore +++ b/.gitignore @@ -57,3 +57,8 @@ allFiredEvents # hardhat cache artifacts + +# Certora +.certora* +.last_confs +certora_* diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 000000000..bbbddbcab --- /dev/null +++ b/certora/Makefile @@ -0,0 +1,24 @@ +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) + diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 000000000..55f84d42f --- /dev/null +++ b/certora/README.md @@ -0,0 +1,56 @@ +# 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 +``` + +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. diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch new file mode 100644 index 000000000..42b10fab5 --- /dev/null +++ b/certora/applyHarness.patch @@ -0,0 +1,101 @@ +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); + } diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol new file mode 100644 index 000000000..5067ecfba --- /dev/null +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -0,0 +1,28 @@ +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); + } +} diff --git a/certora/harnesses/WizardControlFirstPriority.sol b/certora/harnesses/WizardControlFirstPriority.sol new file mode 100644 index 000000000..5ae7fe066 --- /dev/null +++ b/certora/harnesses/WizardControlFirstPriority.sol @@ -0,0 +1,150 @@ +// 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); + } +} diff --git a/certora/harnesses/WizardFirstTry.sol b/certora/harnesses/WizardFirstTry.sol new file mode 100644 index 000000000..83fece04f --- /dev/null +++ b/certora/harnesses/WizardFirstTry.sol @@ -0,0 +1,141 @@ +// 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); + } +} diff --git a/certora/munged/.gitignore b/certora/munged/.gitignore new file mode 100644 index 000000000..d6b7ef32c --- /dev/null +++ b/certora/munged/.gitignore @@ -0,0 +1,2 @@ +* +!.gitignore diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh new file mode 100755 index 000000000..53ade5060 --- /dev/null +++ b/certora/scripts/Governor.sh @@ -0,0 +1,10 @@ +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" diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh new file mode 100644 index 000000000..9ed8fe34c --- /dev/null +++ b/certora/scripts/GovernorCountingSimple-counting.sh @@ -0,0 +1,10 @@ +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" diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/WizardControlFirstPriority.sh new file mode 100644 index 000000000..b815986ee --- /dev/null +++ b/certora/scripts/WizardControlFirstPriority.sh @@ -0,0 +1,12 @@ +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" diff --git a/certora/scripts/WizardFirstTry.sh b/certora/scripts/WizardFirstTry.sh new file mode 100644 index 000000000..fd5a32ab4 --- /dev/null +++ b/certora/scripts/WizardFirstTry.sh @@ -0,0 +1,10 @@ +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" diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh new file mode 100644 index 000000000..b6cdb4ec3 --- /dev/null +++ b/certora/scripts/sanity.sh @@ -0,0 +1,14 @@ +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 diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh new file mode 100644 index 000000000..90d76912c --- /dev/null +++ b/certora/scripts/verifyAll.sh @@ -0,0 +1,39 @@ +#!/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 diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec new file mode 100644 index 000000000..031b2680e --- /dev/null +++ b/certora/specs/GovernorBase.spec @@ -0,0 +1,334 @@ +////////////////////////////////////////////////////////////////////////////// +///////////////////// Governor.sol base definitions ////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +using ERC20VotesHarness as erc20votes + +methods { + proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart + proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd + hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree + isExecuted(uint256) returns bool envfree + isCanceled(uint256) returns bool envfree + execute(address[], uint256[], bytes[], bytes32) returns uint256 + hasVoted(uint256, address) returns bool + castVote(uint256, uint8) returns uint256 + updateQuorumNumerator(uint256) + queue(address[], uint256[], bytes[], bytes32) returns uint256 + + // internal functions made public in harness: + _quorumReached(uint256) returns bool + _voteSucceeded(uint256) returns bool envfree + + // function summarization + proposalThreshold() returns uint256 envfree + + getVotes(address, uint256) returns uint256 => DISPATCHER(true) + + getPastTotalSupply(uint256 t) returns uint256 => PER_CALLEE_CONSTANT + getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT + + //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true) + //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) +} + +////////////////////////////////////////////////////////////////////////////// +//////////////////////////////// Definitions ///////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + + +// proposal was created - relation proved in noStartBeforeCreation +definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0; + + +////////////////////////////////////////////////////////////////////////////// +///////////////////////////// Helper Functions /////////////////////////////// +////////////////////////////////////////////////////////////////////////////// + +function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { + address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash; + uint8 support; uint8 v; bytes32 r; bytes32 s; + if (f.selector == propose(address[], uint256[], bytes[], string).selector) { + uint256 result = propose@withrevert(e, targets, values, calldatas, reason); + require(result == proposalId); + } else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) { + uint256 result = execute@withrevert(e, targets, values, calldatas, descriptionHash); + require(result == proposalId); + } else if (f.selector == castVote(uint256, uint8).selector) { + castVote@withrevert(e, proposalId, support); + } else if (f.selector == castVoteWithReason(uint256, uint8, string).selector) { + castVoteWithReason@withrevert(e, proposalId, support, reason); + } else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) { + castVoteBySig@withrevert(e, proposalId, support, v, r, s); + } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) { + queue@withrevert(e, targets, values, calldatas, descriptionHash); + } else { + calldataarg args; + f@withrevert(e, args); + } +} + +/* + ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////// State Diagram ////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// + // // + // castVote(s)() // + // ------------- propose() ---------------------- time pass --------------- time passes ----------- // + // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() | // + // ------------- ---------------------- --------------- -> Executed/Canceled ----------- // + // ------------------------------------------------------------|---------------|-------------------------|--------------> // + // t start end timelock // + // // + ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +*/ + + +/////////////////////////////////////////////////////////////////////////////////////// +///////////////////////////////// Global Valid States ///////////////////////////////// +/////////////////////////////////////////////////////////////////////////////////////// + + +/* + * Start and end date are either initialized (non zero) or uninitialized (zero) simultaneously + * This invariant assumes that the block number cannot be 0 at any stage of the contract cycle + * This is very safe assumption as usually the 0 block is genesis block which is uploaded with data + * by the developers and will not be valid to raise proposals (at the current way that block chain is functioning) + */ + // To use env with general preserved block disable type checking [--disableLocalTypeChecking] +invariant startAndEndDatesNonZero(uint256 pId) + proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0 + { preserved with (env e){ + require e.block.number > 0; + }} + + +/* + * If a proposal is canceled it must have a start and an end date + */ + // To use env with general preserved block disable type checking [--disableLocalTypeChecking] +invariant canceledImplyStartAndEndDateNonZero(uint pId) + isCanceled(pId) => proposalSnapshot(pId) != 0 + {preserved with (env e){ + require e.block.number > 0; + }} + + +/* + * If a proposal is executed it must have a start and an end date + */ + // To use env with general preserved block disable type checking [--disableLocalTypeChecking] +invariant executedImplyStartAndEndDateNonZero(uint pId) + isExecuted(pId) => proposalSnapshot(pId) != 0 + { preserved with (env e){ + requireInvariant startAndEndDatesNonZero(pId); + require e.block.number > 0; + }} + + +/* + * A proposal starting block number must be less or equal than the proposal end date + */ +invariant voteStartBeforeVoteEnd(uint256 pId) + // from < to <= because snapshot and deadline can be the same block number if delays are set to 0 + // This is possible before the integration of GovernorSettings.sol to the system. + // After integration of GovernorSettings.sol the invariant expression should be changed from <= to < + (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) + // (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) + { preserved { + requireInvariant startAndEndDatesNonZero(pId); + }} + + +/* + * A proposal cannot be both executed and canceled simultaneously. + */ +invariant noBothExecutedAndCanceled(uint256 pId) + !isExecuted(pId) || !isCanceled(pId) + + +/* + * A proposal could be executed only if quorum was reached and vote succeeded + */ +rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){ + bool isExecutedBefore = isExecuted(pId); + bool quorumReachedBefore = _quorumReached(e, pId); + bool voteSucceededBefore = _voteSucceeded(pId); + + calldataarg args; + f(e, args); + + bool isExecutedAfter = isExecuted(pId); + assert (!isExecutedBefore && isExecutedAfter) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed"; +} + +/////////////////////////////////////////////////////////////////////////////////////// +////////////////////////////////// In-State Rules ///////////////////////////////////// +/////////////////////////////////////////////////////////////////////////////////////// + +//========================================== +//------------- Voting Period -------------- +//========================================== + +/* + * A user cannot vote twice + */ + // 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 doubleVoting(uint256 pId, uint8 sup, method f) { + env e; + address user = e.msg.sender; + bool votedCheck = hasVoted(e, pId, user); + + castVote@withrevert(e, pId, sup); + + assert votedCheck => lastReverted, "double voting accured"; +} + + +/////////////////////////////////////////////////////////////////////////////////////// +//////////////////////////// State Transitions Rules ////////////////////////////////// +/////////////////////////////////////////////////////////////////////////////////////// + +//=========================================== +//-------- Propose() --> End of Time -------- +//=========================================== + + +/* + * Once a proposal is created, voteStart and voteEnd are immutable + */ +rule immutableFieldsAfterProposalCreation(uint256 pId, method f) { + uint256 _voteStart = proposalSnapshot(pId); + uint256 _voteEnd = proposalDeadline(pId); + + require proposalCreated(pId); // startDate > 0 + + env e; calldataarg arg; + f(e, arg); + + uint256 voteStart_ = proposalSnapshot(pId); + uint256 voteEnd_ = proposalDeadline(pId); + assert _voteStart == voteStart_, "Start date was changed"; + assert _voteEnd == voteEnd_, "End date was changed"; +} + + +/* + * Voting cannot start at a block number prior to proposal’s creation block number + */ +rule noStartBeforeCreation(uint256 pId) { + uint256 previousStart = proposalSnapshot(pId); + // This line makes sure that we see only cases where start date is changed from 0, i.e. creation of proposal + // We proved in immutableFieldsAfterProposalCreation that once dates set for proposal, it cannot be changed + require !proposalCreated(pId); // previousStart == 0; + + env e; calldataarg args; + propose(e, args); + + uint256 newStart = proposalSnapshot(pId); + // if created, start is after current block number (creation block) + assert(newStart != previousStart => newStart >= e.block.number); +} + + +//============================================ +//--- End of Voting Period --> End of Time --- +//============================================ + + +/* + * A proposal can neither be executed nor canceled before it ends + */ + // By induction it cannot be executed nor canceled before it starts, due to voteStartBeforeVoteEnd +rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){ + require !isExecuted(pId) && !isCanceled(pId); + + env e; calldataarg args; + f(e, args); + + assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline"; +} + +//////////////////////////////////////////////////////////////////////////////// +////////////////////// Integrity Of Functions (Unit Tests) ///////////////////// +//////////////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////////////// +////////////////////////////// High Level Rules //////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////////////// +///////////////////////////// Not Categorized Yet ////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// + + +/* + * All proposal specific (non-view) functions should revert if proposal is executed + */ + // In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, + // non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc + // we connected the executed attribute to the execute() function, showing that only execute() can + // change it, and that it will always change it. +rule allFunctionsRevertIfExecuted(method f) filtered { f -> + !f.isView && !f.isFallback + && f.selector != updateTimelock(address).selector + && f.selector != updateQuorumNumerator(uint256).selector + && f.selector != queue(address[],uint256[],bytes[],bytes32).selector + && f.selector != relay(address,uint256,bytes).selector + && f.selector != 0xb9a61961 // __acceptAdmin() +} { + env e; calldataarg args; + uint256 pId; + require(isExecuted(pId)); + requireInvariant noBothExecutedAndCanceled(pId); + requireInvariant executedImplyStartAndEndDateNonZero(pId); + + helperFunctionsWithRevert(pId, f, e); + + assert(lastReverted, "Function was not reverted"); +} + +/* + * All proposal specific (non-view) functions should revert if proposal is canceled + */ +rule allFunctionsRevertIfCanceled(method f) filtered { + f -> !f.isView && !f.isFallback + && f.selector != updateTimelock(address).selector + && f.selector != updateQuorumNumerator(uint256).selector + && f.selector != queue(address[],uint256[],bytes[],bytes32).selector + && f.selector != relay(address,uint256,bytes).selector + && f.selector != 0xb9a61961 // __acceptAdmin() +} { + env e; calldataarg args; + uint256 pId; + require(isCanceled(pId)); + requireInvariant noBothExecutedAndCanceled(pId); + requireInvariant canceledImplyStartAndEndDateNonZero(pId); + + helperFunctionsWithRevert(pId, f, e); + + assert(lastReverted, "Function was not reverted"); +} + +/* + * Proposal can be switched to executed only via execute() function + */ +rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) { + env e; calldataarg args; + uint256 pId; + bool executedBefore = isExecuted(pId); + require(!executedBefore); + + helperFunctionsWithRevert(pId, f, e); + + bool executedAfter = isExecuted(pId); + assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method"); +} + diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec new file mode 100644 index 000000000..6d2d5fbb7 --- /dev/null +++ b/certora/specs/GovernorCountingSimple.spec @@ -0,0 +1,221 @@ +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"; +} diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/RulesInProgress.spec new file mode 100644 index 000000000..cbad3336e --- /dev/null +++ b/certora/specs/RulesInProgress.spec @@ -0,0 +1,139 @@ +////////////////////////////////////////////////////////////////////////////// +////////////// 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 diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec new file mode 100644 index 000000000..e08f68845 --- /dev/null +++ b/certora/specs/sanity.spec @@ -0,0 +1,14 @@ +/* +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