Michael D. George
3 years ago
committed by
GitHub
commit
1c3b17826e
@ -1,4 +1,4 @@ |
||||
contact_links: |
||||
- name: Support request |
||||
- name: Questions & Support Requests |
||||
url: https://forum.openzeppelin.com/c/support/contracts/18 |
||||
about: Ask the community in the Community Forum |
||||
about: Ask in the OpenZeppelin Forum |
||||
|
||||
@ -0,0 +1,25 @@ |
||||
name: Build Docs |
||||
|
||||
on: |
||||
push: |
||||
branches: [release-v*] |
||||
|
||||
jobs: |
||||
build: |
||||
runs-on: ubuntu-latest |
||||
steps: |
||||
- uses: actions/checkout@v2 |
||||
- uses: actions/setup-node@v3 |
||||
with: |
||||
node-version: 12.x |
||||
- uses: actions/cache@v2 |
||||
id: cache |
||||
with: |
||||
path: '**/node_modules' |
||||
key: npm-v2-${{ hashFiles('**/package-lock.json') }} |
||||
restore-keys: npm-v2- |
||||
- run: npm ci |
||||
if: steps.cache.outputs.cache-hit != 'true' |
||||
- run: bash scripts/git-user-config.sh |
||||
- run: node scripts/update-docs-branch.js |
||||
- run: git push --all origin |
||||
@ -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)
|
||||
|
||||
@ -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 <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. |
||||
@ -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);
|
||||
}
|
||||
@ -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); |
||||
} |
||||
} |
||||
@ -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); |
||||
} |
||||
} |
||||
@ -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); |
||||
} |
||||
} |
||||
@ -0,0 +1,2 @@ |
||||
* |
||||
!.gitignore |
||||
@ -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" |
||||
@ -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" |
||||
@ -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" |
||||
@ -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" |
||||
@ -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 |
||||
@ -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 |
||||
@ -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"); |
||||
} |
||||
|
||||
@ -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"; |
||||
} |
||||
@ -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"; |
||||
} |
||||
@ -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; |
||||
} |
||||
@ -0,0 +1,61 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
// OpenZeppelin Contracts (last updated v4.5.0) (governance/utils/IVotes.sol) |
||||
pragma solidity ^0.8.0; |
||||
|
||||
/** |
||||
* @dev Common interface for {ERC20Votes}, {ERC721Votes}, and other {Votes}-enabled contracts. |
||||
* |
||||
* _Available since v4.5._ |
||||
*/ |
||||
interface IVotes { |
||||
/** |
||||
* @dev Emitted when an account changes their delegate. |
||||
*/ |
||||
event DelegateChanged(address indexed delegator, address indexed fromDelegate, address indexed toDelegate); |
||||
|
||||
/** |
||||
* @dev Emitted when a token transfer or delegate change results in changes to a delegate's number of votes. |
||||
*/ |
||||
event DelegateVotesChanged(address indexed delegate, uint256 previousBalance, uint256 newBalance); |
||||
|
||||
/** |
||||
* @dev Returns the current amount of votes that `account` has. |
||||
*/ |
||||
function getVotes(address account) external view returns (uint256); |
||||
|
||||
/** |
||||
* @dev Returns the amount of votes that `account` had at the end of a past block (`blockNumber`). |
||||
*/ |
||||
function getPastVotes(address account, uint256 blockNumber) external view returns (uint256); |
||||
|
||||
/** |
||||
* @dev Returns the total supply of votes available at the end of a past block (`blockNumber`). |
||||
* |
||||
* NOTE: This value is the sum of all available votes, which is not necessarily the sum of all delegated votes. |
||||
* Votes that have not been delegated are still part of total supply, even though they would not participate in a |
||||
* vote. |
||||
*/ |
||||
function getPastTotalSupply(uint256 blockNumber) external view returns (uint256); |
||||
|
||||
/** |
||||
* @dev Returns the delegate that `account` has chosen. |
||||
*/ |
||||
function delegates(address account) external view returns (address); |
||||
|
||||
/** |
||||
* @dev Delegates votes from the sender to `delegatee`. |
||||
*/ |
||||
function delegate(address delegatee) external; |
||||
|
||||
/** |
||||
* @dev Delegates votes from signer to `delegatee`. |
||||
*/ |
||||
function delegateBySig( |
||||
address delegatee, |
||||
uint256 nonce, |
||||
uint256 expiry, |
||||
uint8 v, |
||||
bytes32 r, |
||||
bytes32 s |
||||
) external; |
||||
} |
||||
@ -0,0 +1,211 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
// OpenZeppelin Contracts (last updated v4.5.0) (governance/utils/Votes.sol) |
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../../utils/Context.sol"; |
||||
import "../../utils/Counters.sol"; |
||||
import "../../utils/Checkpoints.sol"; |
||||
import "../../utils/cryptography/draft-EIP712.sol"; |
||||
import "./IVotes.sol"; |
||||
|
||||
/** |
||||
* @dev This is a base abstract contract that tracks voting units, which are a measure of voting power that can be |
||||
* transferred, and provides a system of vote delegation, where an account can delegate its voting units to a sort of |
||||
* "representative" that will pool delegated voting units from different accounts and can then use it to vote in |
||||
* decisions. In fact, voting units _must_ be delegated in order to count as actual votes, and an account has to |
||||
* delegate those votes to itself if it wishes to participate in decisions and does not have a trusted representative. |
||||
* |
||||
* This contract is often combined with a token contract such that voting units correspond to token units. For an |
||||
* example, see {ERC721Votes}. |
||||
* |
||||
* The full history of delegate votes is tracked on-chain so that governance protocols can consider votes as distributed |
||||
* at a particular block number to protect against flash loans and double voting. The opt-in delegate system makes the |
||||
* cost of this history tracking optional. |
||||
* |
||||
* When using this module the derived contract must implement {_getVotingUnits} (for example, make it return |
||||
* {ERC721-balanceOf}), and can use {_transferVotingUnits} to track a change in the distribution of those units (in the |
||||
* previous example, it would be included in {ERC721-_beforeTokenTransfer}). |
||||
* |
||||
* _Available since v4.5._ |
||||
*/ |
||||
abstract contract Votes is IVotes, Context, EIP712 { |
||||
using Checkpoints for Checkpoints.History; |
||||
using Counters for Counters.Counter; |
||||
|
||||
bytes32 private constant _DELEGATION_TYPEHASH = |
||||
keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); |
||||
|
||||
mapping(address => address) private _delegation; |
||||
mapping(address => Checkpoints.History) private _delegateCheckpoints; |
||||
Checkpoints.History private _totalCheckpoints; |
||||
|
||||
mapping(address => Counters.Counter) private _nonces; |
||||
|
||||
/** |
||||
* @dev Returns the current amount of votes that `account` has. |
||||
*/ |
||||
function getVotes(address account) public view virtual override returns (uint256) { |
||||
return _delegateCheckpoints[account].latest(); |
||||
} |
||||
|
||||
/** |
||||
* @dev Returns the amount of votes that `account` had at the end of a past block (`blockNumber`). |
||||
* |
||||
* Requirements: |
||||
* |
||||
* - `blockNumber` must have been already mined |
||||
*/ |
||||
function getPastVotes(address account, uint256 blockNumber) public view virtual override returns (uint256) { |
||||
return _delegateCheckpoints[account].getAtBlock(blockNumber); |
||||
} |
||||
|
||||
/** |
||||
* @dev Returns the total supply of votes available at the end of a past block (`blockNumber`). |
||||
* |
||||
* NOTE: This value is the sum of all available votes, which is not necessarily the sum of all delegated votes. |
||||
* Votes that have not been delegated are still part of total supply, even though they would not participate in a |
||||
* vote. |
||||
* |
||||
* Requirements: |
||||
* |
||||
* - `blockNumber` must have been already mined |
||||
*/ |
||||
function getPastTotalSupply(uint256 blockNumber) public view virtual override returns (uint256) { |
||||
require(blockNumber < block.number, "Votes: block not yet mined"); |
||||
return _totalCheckpoints.getAtBlock(blockNumber); |
||||
} |
||||
|
||||
/** |
||||
* @dev Returns the current total supply of votes. |
||||
*/ |
||||
function _getTotalSupply() internal view virtual returns (uint256) { |
||||
return _totalCheckpoints.latest(); |
||||
} |
||||
|
||||
/** |
||||
* @dev Returns the delegate that `account` has chosen. |
||||
*/ |
||||
function delegates(address account) public view virtual override returns (address) { |
||||
return _delegation[account]; |
||||
} |
||||
|
||||
/** |
||||
* @dev Delegates votes from the sender to `delegatee`. |
||||
*/ |
||||
function delegate(address delegatee) public virtual override { |
||||
address account = _msgSender(); |
||||
_delegate(account, delegatee); |
||||
} |
||||
|
||||
/** |
||||
* @dev Delegates votes from signer to `delegatee`. |
||||
*/ |
||||
function delegateBySig( |
||||
address delegatee, |
||||
uint256 nonce, |
||||
uint256 expiry, |
||||
uint8 v, |
||||
bytes32 r, |
||||
bytes32 s |
||||
) public virtual override { |
||||
require(block.timestamp <= expiry, "Votes: signature expired"); |
||||
address signer = ECDSA.recover( |
||||
_hashTypedDataV4(keccak256(abi.encode(_DELEGATION_TYPEHASH, delegatee, nonce, expiry))), |
||||
v, |
||||
r, |
||||
s |
||||
); |
||||
require(nonce == _useNonce(signer), "Votes: invalid nonce"); |
||||
_delegate(signer, delegatee); |
||||
} |
||||
|
||||
/** |
||||
* @dev Delegate all of `account`'s voting units to `delegatee`. |
||||
* |
||||
* Emits events {DelegateChanged} and {DelegateVotesChanged}. |
||||
*/ |
||||
function _delegate(address account, address delegatee) internal virtual { |
||||
address oldDelegate = delegates(account); |
||||
_delegation[account] = delegatee; |
||||
|
||||
emit DelegateChanged(account, oldDelegate, delegatee); |
||||
_moveDelegateVotes(oldDelegate, delegatee, _getVotingUnits(account)); |
||||
} |
||||
|
||||
/** |
||||
* @dev Transfers, mints, or burns voting units. To register a mint, `from` should be zero. To register a burn, `to` |
||||
* should be zero. Total supply of voting units will be adjusted with mints and burns. |
||||
*/ |
||||
function _transferVotingUnits( |
||||
address from, |
||||
address to, |
||||
uint256 amount |
||||
) internal virtual { |
||||
if (from == address(0)) { |
||||
_totalCheckpoints.push(_add, amount); |
||||
} |
||||
if (to == address(0)) { |
||||
_totalCheckpoints.push(_subtract, amount); |
||||
} |
||||
_moveDelegateVotes(delegates(from), delegates(to), amount); |
||||
} |
||||
|
||||
/** |
||||
* @dev Moves delegated votes from one delegate to another. |
||||
*/ |
||||
function _moveDelegateVotes( |
||||
address from, |
||||
address to, |
||||
uint256 amount |
||||
) private { |
||||
if (from != to && amount > 0) { |
||||
if (from != address(0)) { |
||||
(uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_subtract, amount); |
||||
emit DelegateVotesChanged(from, oldValue, newValue); |
||||
} |
||||
if (to != address(0)) { |
||||
(uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_add, amount); |
||||
emit DelegateVotesChanged(to, oldValue, newValue); |
||||
} |
||||
} |
||||
} |
||||
|
||||
function _add(uint256 a, uint256 b) private pure returns (uint256) { |
||||
return a + b; |
||||
} |
||||
|
||||
function _subtract(uint256 a, uint256 b) private pure returns (uint256) { |
||||
return a - b; |
||||
} |
||||
|
||||
/** |
||||
* @dev Consumes a nonce. |
||||
* |
||||
* Returns the current value and increments nonce. |
||||
*/ |
||||
function _useNonce(address owner) internal virtual returns (uint256 current) { |
||||
Counters.Counter storage nonce = _nonces[owner]; |
||||
current = nonce.current(); |
||||
nonce.increment(); |
||||
} |
||||
|
||||
/** |
||||
* @dev Returns an address nonce. |
||||
*/ |
||||
function nonces(address owner) public view virtual returns (uint256) { |
||||
return _nonces[owner].current(); |
||||
} |
||||
|
||||
/** |
||||
* @dev Returns the contract's {EIP712} domain separator. |
||||
*/ |
||||
// solhint-disable-next-line func-name-mixedcase |
||||
function DOMAIN_SEPARATOR() external view returns (bytes32) { |
||||
return _domainSeparatorV4(); |
||||
} |
||||
|
||||
/** |
||||
* @dev Must return the voting units held by an account. |
||||
*/ |
||||
function _getVotingUnits(address) internal virtual returns (uint256); |
||||
} |
||||
@ -0,0 +1,20 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
// OpenZeppelin Contracts (last updated v4.5.0) (interfaces/draft-IERC1822.sol) |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
/** |
||||
* @dev ERC1822: Universal Upgradeable Proxy Standard (UUPS) documents a method for upgradeability through a simplified |
||||
* proxy whose upgrades are fully controlled by the current implementation. |
||||
*/ |
||||
interface IERC1822Proxiable { |
||||
/** |
||||
* @dev Returns the storage slot that the proxiable contract assumes is being used to store the implementation |
||||
* address. |
||||
* |
||||
* IMPORTANT: A proxy pointing at a proxiable contract should not be considered proxiable itself, because this risks |
||||
* bricking a proxy that upgrades to it, by delegating to itself until out of gas. Thus it is critical that this |
||||
* function revert if invoked through a proxy. |
||||
*/ |
||||
function proxiableUUID() external view returns (bytes32); |
||||
} |
||||
@ -0,0 +1,11 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../utils/Base64.sol"; |
||||
|
||||
contract Base64Mock { |
||||
function encode(bytes memory value) external pure returns (string memory) { |
||||
return Base64.encode(value); |
||||
} |
||||
} |
||||
@ -0,0 +1,23 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../utils/Checkpoints.sol"; |
||||
|
||||
contract CheckpointsImpl { |
||||
using Checkpoints for Checkpoints.History; |
||||
|
||||
Checkpoints.History private _totalCheckpoints; |
||||
|
||||
function latest() public view returns (uint256) { |
||||
return _totalCheckpoints.latest(); |
||||
} |
||||
|
||||
function getAtBlock(uint256 blockNumber) public view returns (uint256) { |
||||
return _totalCheckpoints.getAtBlock(blockNumber); |
||||
} |
||||
|
||||
function push(uint256 value) public returns (uint256, uint256) { |
||||
return _totalCheckpoints.push(value); |
||||
} |
||||
} |
||||
@ -0,0 +1,58 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../utils/structs/DoubleEndedQueue.sol"; |
||||
|
||||
// Bytes32Deque |
||||
contract Bytes32DequeMock { |
||||
using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque; |
||||
|
||||
event OperationResult(bytes32 value); |
||||
|
||||
DoubleEndedQueue.Bytes32Deque private _vector; |
||||
|
||||
function pushBack(bytes32 value) public { |
||||
_vector.pushBack(value); |
||||
} |
||||
|
||||
function pushFront(bytes32 value) public { |
||||
_vector.pushFront(value); |
||||
} |
||||
|
||||
function popFront() public returns (bytes32) { |
||||
bytes32 value = _vector.popFront(); |
||||
emit OperationResult(value); |
||||
return value; |
||||
} |
||||
|
||||
function popBack() public returns (bytes32) { |
||||
bytes32 value = _vector.popBack(); |
||||
emit OperationResult(value); |
||||
return value; |
||||
} |
||||
|
||||
function front() public view returns (bytes32) { |
||||
return _vector.front(); |
||||
} |
||||
|
||||
function back() public view returns (bytes32) { |
||||
return _vector.back(); |
||||
} |
||||
|
||||
function at(uint256 i) public view returns (bytes32) { |
||||
return _vector.at(i); |
||||
} |
||||
|
||||
function clear() public { |
||||
_vector.clear(); |
||||
} |
||||
|
||||
function length() public view returns (uint256) { |
||||
return _vector.length(); |
||||
} |
||||
|
||||
function empty() public view returns (bool) { |
||||
return _vector.empty(); |
||||
} |
||||
} |
||||
@ -0,0 +1,33 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../token/ERC721/extensions/ERC721Royalty.sol"; |
||||
|
||||
contract ERC721RoyaltyMock is ERC721Royalty { |
||||
constructor(string memory name, string memory symbol) ERC721(name, symbol) {} |
||||
|
||||
function setTokenRoyalty( |
||||
uint256 tokenId, |
||||
address recipient, |
||||
uint96 fraction |
||||
) public { |
||||
_setTokenRoyalty(tokenId, recipient, fraction); |
||||
} |
||||
|
||||
function setDefaultRoyalty(address recipient, uint96 fraction) public { |
||||
_setDefaultRoyalty(recipient, fraction); |
||||
} |
||||
|
||||
function mint(address to, uint256 tokenId) public { |
||||
_mint(to, tokenId); |
||||
} |
||||
|
||||
function burn(uint256 tokenId) public { |
||||
_burn(tokenId); |
||||
} |
||||
|
||||
function deleteDefaultRoyalty() public { |
||||
_deleteDefaultRoyalty(); |
||||
} |
||||
} |
||||
@ -0,0 +1,25 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../token/ERC721/extensions/draft-ERC721Votes.sol"; |
||||
|
||||
contract ERC721VotesMock is ERC721Votes { |
||||
constructor(string memory name, string memory symbol) ERC721(name, symbol) EIP712(name, "1") {} |
||||
|
||||
function getTotalSupply() public view returns (uint256) { |
||||
return _getTotalSupply(); |
||||
} |
||||
|
||||
function mint(address account, uint256 tokenId) public { |
||||
_mint(account, tokenId); |
||||
} |
||||
|
||||
function burn(uint256 tokenId) public { |
||||
_burn(tokenId); |
||||
} |
||||
|
||||
function getChainId() external view returns (uint256) { |
||||
return block.chainid; |
||||
} |
||||
} |
||||
@ -0,0 +1,41 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../governance/extensions/GovernorCountingSimple.sol"; |
||||
import "../governance/extensions/GovernorVotes.sol"; |
||||
|
||||
contract GovernorVoteMocks is GovernorVotes, GovernorCountingSimple { |
||||
constructor(string memory name_, IVotes token_) Governor(name_) GovernorVotes(token_) {} |
||||
|
||||
function quorum(uint256) public pure override returns (uint256) { |
||||
return 0; |
||||
} |
||||
|
||||
function votingDelay() public pure override returns (uint256) { |
||||
return 4; |
||||
} |
||||
|
||||
function votingPeriod() public pure override returns (uint256) { |
||||
return 16; |
||||
} |
||||
|
||||
function cancel( |
||||
address[] memory targets, |
||||
uint256[] memory values, |
||||
bytes[] memory calldatas, |
||||
bytes32 salt |
||||
) public returns (uint256 proposalId) { |
||||
return _cancel(targets, values, calldatas, salt); |
||||
} |
||||
|
||||
function getVotes(address account, uint256 blockNumber) |
||||
public |
||||
view |
||||
virtual |
||||
override(IGovernor, GovernorVotes) |
||||
returns (uint256) |
||||
{ |
||||
return super.getVotes(account, blockNumber); |
||||
} |
||||
} |
||||
@ -0,0 +1,23 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../utils/math/SignedMath.sol"; |
||||
|
||||
contract SignedMathMock { |
||||
function max(int256 a, int256 b) public pure returns (int256) { |
||||
return SignedMath.max(a, b); |
||||
} |
||||
|
||||
function min(int256 a, int256 b) public pure returns (int256) { |
||||
return SignedMath.min(a, b); |
||||
} |
||||
|
||||
function average(int256 a, int256 b) public pure returns (int256) { |
||||
return SignedMath.average(a, b); |
||||
} |
||||
|
||||
function abs(int256 n) public pure returns (uint256) { |
||||
return SignedMath.abs(n); |
||||
} |
||||
} |
||||
@ -0,0 +1,58 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "./UUPSUpgradeableMock.sol"; |
||||
|
||||
// This contract implements the pre-4.5 UUPS upgrade function with a rollback test. |
||||
// It's used to test that newer UUPS contracts are considered valid upgrades by older UUPS contracts. |
||||
contract UUPSUpgradeableLegacyMock is UUPSUpgradeableMock { |
||||
// Inlined from ERC1967Upgrade |
||||
bytes32 private constant _ROLLBACK_SLOT = 0x4910fdfa16fed3260ed0e7147f7cc6da11a60208b5b9406d12a635614ffd9143; |
||||
|
||||
// ERC1967Upgrade._setImplementation is private so we reproduce it here. |
||||
// An extra underscore prevents a name clash error. |
||||
function __setImplementation(address newImplementation) private { |
||||
require(Address.isContract(newImplementation), "ERC1967: new implementation is not a contract"); |
||||
StorageSlot.getAddressSlot(_IMPLEMENTATION_SLOT).value = newImplementation; |
||||
} |
||||
|
||||
function _upgradeToAndCallSecureLegacyV1( |
||||
address newImplementation, |
||||
bytes memory data, |
||||
bool forceCall |
||||
) internal { |
||||
address oldImplementation = _getImplementation(); |
||||
|
||||
// Initial upgrade and setup call |
||||
__setImplementation(newImplementation); |
||||
if (data.length > 0 || forceCall) { |
||||
Address.functionDelegateCall(newImplementation, data); |
||||
} |
||||
|
||||
// Perform rollback test if not already in progress |
||||
StorageSlot.BooleanSlot storage rollbackTesting = StorageSlot.getBooleanSlot(_ROLLBACK_SLOT); |
||||
if (!rollbackTesting.value) { |
||||
// Trigger rollback using upgradeTo from the new implementation |
||||
rollbackTesting.value = true; |
||||
Address.functionDelegateCall( |
||||
newImplementation, |
||||
abi.encodeWithSignature("upgradeTo(address)", oldImplementation) |
||||
); |
||||
rollbackTesting.value = false; |
||||
// Check rollback was effective |
||||
require(oldImplementation == _getImplementation(), "ERC1967Upgrade: upgrade breaks further upgrades"); |
||||
// Finally reset to the new implementation and log the upgrade |
||||
_upgradeTo(newImplementation); |
||||
} |
||||
} |
||||
|
||||
// hooking into the old mechanism |
||||
function upgradeTo(address newImplementation) external virtual override { |
||||
_upgradeToAndCallSecureLegacyV1(newImplementation, bytes(""), false); |
||||
} |
||||
|
||||
function upgradeToAndCall(address newImplementation, bytes memory data) external payable virtual override { |
||||
_upgradeToAndCallSecureLegacyV1(newImplementation, data, false); |
||||
} |
||||
} |
||||
@ -0,0 +1,40 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../governance/utils/Votes.sol"; |
||||
|
||||
contract VotesMock is Votes { |
||||
mapping(address => uint256) private _balances; |
||||
mapping(uint256 => address) private _owners; |
||||
|
||||
constructor(string memory name) EIP712(name, "1") {} |
||||
|
||||
function getTotalSupply() public view returns (uint256) { |
||||
return _getTotalSupply(); |
||||
} |
||||
|
||||
function delegate(address account, address newDelegation) public { |
||||
return _delegate(account, newDelegation); |
||||
} |
||||
|
||||
function _getVotingUnits(address account) internal virtual override returns (uint256) { |
||||
return _balances[account]; |
||||
} |
||||
|
||||
function mint(address account, uint256 voteId) external { |
||||
_balances[account] += 1; |
||||
_owners[voteId] = account; |
||||
_transferVotingUnits(address(0), account, 1); |
||||
} |
||||
|
||||
function burn(uint256 voteId) external { |
||||
address owner = _owners[voteId]; |
||||
_balances[owner] -= 1; |
||||
_transferVotingUnits(owner, address(0), 1); |
||||
} |
||||
|
||||
function getChainId() external view returns (uint256) { |
||||
return block.chainid; |
||||
} |
||||
} |
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in new issue