From 61b011869c4924abe835b87e4f659ff9152dbf1a Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 17 Nov 2021 16:00:16 +0200 Subject: [PATCH] AddedLinkAndFixingGhost --- certora/harnesses/ERC20VotesHarness.sol | 30 +++++++++++++++++++ .../GovernorCountingSimple-counting.sh | 2 +- certora/scripts/WizardHarness1.sh | 3 +- certora/specs/GovernorCountingSimple.spec | 19 ++++++------ .../token/ERC20/extensions/ERC20Votes.sol | 2 +- 5 files changed, 44 insertions(+), 12 deletions(-) diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index 6ef5934b7..366aa9304 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -2,4 +2,34 @@ import "../../contracts/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)) _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); + } + + function getPastVotes(address account, uint256 blockNumber) public view virtual override returns (uint256) { + uint256 gpv = super.getPastVotes(account, blockNumber); + require (_getPastVotes[account][blockNumber] == gpv); + return gpv; + } + } \ No newline at end of file diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh index c812f52e9..82b2c263e 100644 --- a/certora/scripts/GovernorCountingSimple-counting.sh +++ b/certora/scripts/GovernorCountingSimple-counting.sh @@ -1,4 +1,4 @@ -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ +certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ --staging shelly/forSasha \ diff --git a/certora/scripts/WizardHarness1.sh b/certora/scripts/WizardHarness1.sh index dd8816f35..64fd52d33 100644 --- a/certora/scripts/WizardHarness1.sh +++ b/certora/scripts/WizardHarness1.sh @@ -1,8 +1,9 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardHarness1.sol \ + --link WizardHarness1:token=ERC20VotesHarness \ --verify WizardHarness1:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --rule SumOfVotesCastEqualSumOfPowerOfVoted \ + --rule hasVotedCorrelation \ --msg "$1" \ No newline at end of file diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index e8ee21db5..8c17bc738 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -1,5 +1,7 @@ import "GovernorBase.spec" +using ERC20VotesHarness as erc20votes + methods { ghost_sum_vote_power_by_id(uint256) returns uint256 envfree // castVote(uint256, uint8) returns uint256 @@ -81,12 +83,11 @@ ghost totalVotesPossible(uint256) returns uint256 { } // Was done with _getVotes by mistake. Should check GovernorBasicHarness but _getVotes is from GovernorHarness -//hook Sstore _getVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE { -// havoc totalVotesPossible assuming forall uint256 bn. -// (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight) -// && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn)); -// -//} +hook Sstore erc20votes._getPastVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE { + havoc totalVotesPossible assuming forall uint256 bn. + (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight) + && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn)); +} @@ -118,8 +119,8 @@ invariant OneIsNotMoreThanAll(uint256 pId) /* * totalVotesPossible >= votePower(id) */ -//invariant possibleTotalVotes(uint256 pId) -// tracked_weight(pId) <= totalVotesPossible(snapshot(pId)) +invariant possibleTotalVotes(uint256 pId) + tracked_weight(pId) <= totalVotesPossible(snapshot(pId)) /* * totalVotesPossible >= votePower(id) @@ -255,7 +256,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f - uint256 votesAfter = getVotes(acc, bn); bool hasVotedAfter = hasVoted(e, pId, acc); - assert hasVotedBefore != hasVotedAfter => againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter, "no correlation"; + assert hasVotedBefore != hasVotedAfter => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation"; } diff --git a/contracts/token/ERC20/extensions/ERC20Votes.sol b/contracts/token/ERC20/extensions/ERC20Votes.sol index 5e176973e..06fd68831 100644 --- a/contracts/token/ERC20/extensions/ERC20Votes.sol +++ b/contracts/token/ERC20/extensions/ERC20Votes.sol @@ -84,7 +84,7 @@ abstract contract ERC20Votes is ERC20Permit { * * - `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); }