From e81037926227b4778fee7710eb8daafc5781ba15 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com> Date: Wed, 3 Nov 2021 17:05:06 +0200 Subject: [PATCH] sanity rule preparations --- .../harnesses/GovernorProposalThresholdHarness.sol | 9 +++++++-- .../harnesses/GovernorTimelockCompoundHarness.sol | 4 ++-- certora/harnesses/GovernorVotesHarness.sol | 7 +++---- .../GovernorVotesQuorumFractionHarness.sol | 6 +++--- certora/scripts/check.sh | 4 +++- certora/scripts/sanity.sh | 9 +++++++++ certora/specs/sanity.spec | 14 ++++++++++++++ contracts/governance/Governor.sol | 4 ++-- .../extensions/GovernorCountingSimple.sol | 4 ++-- 9 files changed, 45 insertions(+), 16 deletions(-) create mode 100644 certora/scripts/sanity.sh create mode 100644 certora/specs/sanity.spec diff --git a/certora/harnesses/GovernorProposalThresholdHarness.sol b/certora/harnesses/GovernorProposalThresholdHarness.sol index 8301a76d8..1d0559a60 100644 --- a/certora/harnesses/GovernorProposalThresholdHarness.sol +++ b/certora/harnesses/GovernorProposalThresholdHarness.sol @@ -15,12 +15,12 @@ contract GovernorProposalThresholdHarness is GovernorProposalThreshold { } mapping (uint256 => bool) __quoromReached; - function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + function _quorumReached(uint256 proposalId) public view override virtual returns (bool) { return __quoromReached[proposalId]; } mapping (uint256 => bool) __voteSucceeded; - function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) { return __voteSucceeded[proposalId]; } @@ -53,6 +53,11 @@ contract GovernorProposalThresholdHarness is GovernorProposalThreshold { // havoc something } + uint256 _proposalThreshold; + function proposalThreshold() public view override virtual returns (uint256) { + return _proposalThreshold; + } + constructor(string memory name) Governor(name) {} } \ No newline at end of file diff --git a/certora/harnesses/GovernorTimelockCompoundHarness.sol b/certora/harnesses/GovernorTimelockCompoundHarness.sol index 5513546ab..f8a85e53f 100644 --- a/certora/harnesses/GovernorTimelockCompoundHarness.sol +++ b/certora/harnesses/GovernorTimelockCompoundHarness.sol @@ -15,12 +15,12 @@ contract GovernorTimelockCompoundHarness is GovernorTimelockCompound { } mapping (uint256 => bool) __quoromReached; - function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + function _quorumReached(uint256 proposalId) public view override virtual returns (bool) { return __quoromReached[proposalId]; } mapping (uint256 => bool) __voteSucceeded; - function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) { return __voteSucceeded[proposalId]; } diff --git a/certora/harnesses/GovernorVotesHarness.sol b/certora/harnesses/GovernorVotesHarness.sol index 65a095156..8ed638e41 100644 --- a/certora/harnesses/GovernorVotesHarness.sol +++ b/certora/harnesses/GovernorVotesHarness.sol @@ -9,12 +9,12 @@ contract GovernorVotesHarness is GovernorVotes { } mapping (uint256 => bool) __quoromReached; - function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + function _quorumReached(uint256 proposalId) public view override virtual returns (bool) { return __quoromReached[proposalId]; } mapping (uint256 => bool) __voteSucceeded; - function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) { return __voteSucceeded[proposalId]; } @@ -47,6 +47,5 @@ contract GovernorVotesHarness is GovernorVotes { // havoc something } - constructor(string memory name) Governor(name) {} - + constructor(ERC20Votes tokenAddr) GovernorVotes(tokenAddr) {} } \ No newline at end of file diff --git a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol index 3c7015eb9..65be741d4 100644 --- a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol +++ b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol @@ -1,14 +1,14 @@ -import "../../contracts/governance/extensions/GovernorVotesQuorumFractionGovernor.sol"; +import "../../contracts/governance/extensions/GovernorVotesQuorumFraction.sol"; contract GovernorVotesQuorumFractionHarness is GovernorVotesQuorumFraction { mapping (uint256 => bool) __quoromReached; - function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + function _quorumReached(uint256 proposalId) public view override virtual returns (bool) { return __quoromReached[proposalId]; } mapping (uint256 => bool) __voteSucceeded; - function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + function _voteSucceeded(uint256 proposalId) public view override virtual returns (bool) { return __voteSucceeded[proposalId]; } diff --git a/certora/scripts/check.sh b/certora/scripts/check.sh index 0cb980dc3..cdb356e90 100755 --- a/certora/scripts/check.sh +++ b/certora/scripts/check.sh @@ -4,4 +4,6 @@ Contract=$1 Spec=$2 shift 2 certoraRun certora/harnesses/${Contract}Harness.sol \ - --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@" \ No newline at end of file + --verify ${Contract}Harness:certora/specs/${Spec}.spec "$@" \ + --solc solc8.0 + \ No newline at end of file diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh new file mode 100644 index 000000000..4db90ebff --- /dev/null +++ b/certora/scripts/sanity.sh @@ -0,0 +1,9 @@ +for f in certora/harnesses/*.sol +do + echo "Processing $f" + file=$(basename $f) + echo ${file%.*} + certoraRun certora/harnesses/$file \ + --verify ${file%.*}:certora/specs/sanity.spec "$@" \ + --solc solc8.0 +done \ No newline at end of file diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec new file mode 100644 index 000000000..e08f68845 --- /dev/null +++ b/certora/specs/sanity.spec @@ -0,0 +1,14 @@ +/* +This rule looks for a non-reverting execution path to each method, including those overridden in the harness. +A method has such an execution path if it violates this rule. +How it works: + - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails. + - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously. +*/ + +rule sanity(method f) { + env e; + calldataarg arg; + f(e, arg); + assert false; +} \ No newline at end of file diff --git a/contracts/governance/Governor.sol b/contracts/governance/Governor.sol index f11287ca8..9f08dc2ad 100644 --- a/contracts/governance/Governor.sol +++ b/contracts/governance/Governor.sol @@ -154,12 +154,12 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor { /** * @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); /** * @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); /** * @dev Register a vote with a given support and voting weight. diff --git a/contracts/governance/extensions/GovernorCountingSimple.sol b/contracts/governance/extensions/GovernorCountingSimple.sol index 782c8a699..b8c72ed9e 100644 --- a/contracts/governance/extensions/GovernorCountingSimple.sol +++ b/contracts/governance/extensions/GovernorCountingSimple.sol @@ -64,7 +64,7 @@ abstract contract GovernorCountingSimple is Governor { /** * @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 @@ abstract contract GovernorCountingSimple is Governor { /** * @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;