From 44113d58f5e1be5f3a4dcb9bbc6f51c6ef7a8f5e Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 17 Nov 2021 11:56:24 +0200 Subject: [PATCH] NewWizardHarness --- certora/harnesses/ERC20VotesHarness.sol | 5 + certora/harnesses/GovernorBasicHarness.sol | 21 ++- certora/harnesses/WizardHarness1.sol | 152 ++++++++++++++++++ certora/scripts/GovernorBasic.sh | 6 +- .../GovernorCountingSimple-counting.sh | 2 +- certora/scripts/WizardHarness1.sh | 8 + certora/specs/GovernorCountingSimple.spec | 1 + 7 files changed, 183 insertions(+), 12 deletions(-) create mode 100644 certora/harnesses/ERC20VotesHarness.sol create mode 100644 certora/harnesses/WizardHarness1.sol create mode 100644 certora/scripts/WizardHarness1.sh diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol new file mode 100644 index 000000000..c9f40b024 --- /dev/null +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -0,0 +1,5 @@ +import "../../contracts/token/ERC20/extensions/ERC20Votes.sol"; + +contract ERC20VotesHarness is ERC20Votes { + constructor(string memory name) ERC20Permit(name) {} +} \ No newline at end of file diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/GovernorBasicHarness.sol index 02846a137..8f5a9dfd6 100644 --- a/certora/harnesses/GovernorBasicHarness.sol +++ b/certora/harnesses/GovernorBasicHarness.sol @@ -33,16 +33,19 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes uint256 _votingDelay; - function votingDelay() public view override virtual returns (uint256) { + function votingDelay() public view override virtual returns (uint256) { // HARNESS: pure -> view return _votingDelay; } uint256 _votingPeriod; - function votingPeriod() public view override virtual returns (uint256) { + function votingPeriod() public view override virtual returns (uint256) { // HARNESS: pure -> view return _votingPeriod; } + function snapshot(uint256 proposalId) public view returns (uint64) { + return _proposals[proposalId].voteStart._deadline; + } mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; @@ -65,13 +68,15 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes return super.propose(targets, values, calldatas, ""); } - /* - mapping (address => mapping (uint256 => uint256)) _getVotes; - - function getVotesHarnness(address account, uint256 blockNumber) public { - _getVotes[account][blockNumber] = getVotes(account, blockNumber); + // Harness of castVoteWithReason to be able to impose requirement on the proposal ID. + uint256 public _pId_Harness; + function castVoteWithReason(uint256 proposalId, uint8 support, string calldata reason) + public + override(IGovernor, Governor) + returns (uint256) { + require(proposalId == _pId_Harness); + return super.castVoteWithReason(proposalId, support, reason); } - */ // The following functions are overrides required by Solidity. diff --git a/certora/harnesses/WizardHarness1.sol b/certora/harnesses/WizardHarness1.sol new file mode 100644 index 000000000..1c5ed9bcb --- /dev/null +++ b/certora/harnesses/WizardHarness1.sol @@ -0,0 +1,152 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../../contracts/governance/Governor.sol"; +import "../../contracts/governance/extensions/GovernorCountingSimple.sol"; +import "../../contracts/governance/extensions/GovernorVotes.sol"; +import "../../contracts/governance/extensions/GovernorVotesQuorumFraction.sol"; +import "../../contracts/governance/extensions/GovernorTimelockControl.sol"; +import "../../contracts/governance/extensions/GovernorProposalThreshold.sol"; + +/* +Wizard options: +ProposalThreshhold = 10 +ERC20Votes +TimelockCOntroller +*/ + +contract WizardHarness1 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 callPropose(address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas) public virtual returns (uint256) { + return super.propose(targets, values, calldatas, ""); + } + + function snapshot(uint256 proposalId) public view returns (uint64) { + return _proposals[proposalId].voteStart._deadline; + } + + + + // original code + + 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 + } + + // 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/scripts/GovernorBasic.sh b/certora/scripts/GovernorBasic.sh index 7b3db7077..f7d3cbf18 100644 --- a/certora/scripts/GovernorBasic.sh +++ b/certora/scripts/GovernorBasic.sh @@ -1,8 +1,8 @@ certoraRun certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \ - --solc solc8.0 \ - ---staging shelly/stringCVL \ + --solc solc8.2 \ + --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --rule unaffectedThreshhold \ + --rule allFunctionsRevertIfCanceled \ --msg "$1" \ No newline at end of file diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh index 6413e5694..ddd59baa2 100644 --- a/certora/scripts/GovernorCountingSimple-counting.sh +++ b/certora/scripts/GovernorCountingSimple-counting.sh @@ -1,7 +1,7 @@ certoraRun certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ - --staging alex/external-timeout-for-solvers \ + --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ --rule hasVotedCorrelation \ diff --git a/certora/scripts/WizardHarness1.sh b/certora/scripts/WizardHarness1.sh new file mode 100644 index 000000000..de0a038bb --- /dev/null +++ b/certora/scripts/WizardHarness1.sh @@ -0,0 +1,8 @@ +certoraRun certora/harnesses/WizardHarness1.sol \ + --verify WizardHarness1:certora/specs/GovernorBase.spec \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --rule allFunctionsRevertIfCanceled \ + --msg "$1" \ No newline at end of file diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index e2fc1fdf9..aa98ce493 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -274,6 +274,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f - // how to check executor()? // to make it public instead of internal is not best idea, I think. // currentContract gives a violation in +// maybe need harness implementation for one of the contracts rule privilegedOnly(method f){ env e; calldataarg arg;