From 2c08f85744a18a2cd631b71c6719e48674ae9088 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sun, 26 Sep 2021 00:21:08 +0300 Subject: [PATCH] start work on governor --- .../GovernorCountingSimpleHarness.sol | 29 +++++++ certora/harnesses/GovernorHarness.sol | 58 ++++++++++++++ .../GovernorProposalThresholdHarness.sol | 58 ++++++++++++++ .../GovernorTimelockCompoundHarness.sol | 58 ++++++++++++++ certora/harnesses/GovernorVotesHarness.sol | 52 ++++++++++++ .../GovernorVotesQuorumFractionHarness.sol | 46 +++++++++++ certora/scripts/Governor.sh | 2 + certora/scripts/GovernorCountingSimple.sh | 2 + certora/scripts/GovernorProposalThreshold.sh | 2 + certora/scripts/GovernorTimelockCompound.sh | 2 + certora/scripts/GovernorVotes.sh | 2 + .../GovernorVotesQuorumFractionHarness.sh | 2 + certora/scripts/check.sh | 7 ++ certora/specs/GovernorBase.spec | 79 +++++++++++++++++++ certora/specs/Privileged.spec | 31 ++++++++ 15 files changed, 430 insertions(+) create mode 100644 certora/harnesses/GovernorCountingSimpleHarness.sol create mode 100644 certora/harnesses/GovernorHarness.sol create mode 100644 certora/harnesses/GovernorProposalThresholdHarness.sol create mode 100644 certora/harnesses/GovernorTimelockCompoundHarness.sol create mode 100644 certora/harnesses/GovernorVotesHarness.sol create mode 100644 certora/harnesses/GovernorVotesQuorumFractionHarness.sol create mode 100755 certora/scripts/Governor.sh create mode 100755 certora/scripts/GovernorCountingSimple.sh create mode 100755 certora/scripts/GovernorProposalThreshold.sh create mode 100755 certora/scripts/GovernorTimelockCompound.sh create mode 100755 certora/scripts/GovernorVotes.sh create mode 100755 certora/scripts/GovernorVotesQuorumFractionHarness.sh create mode 100755 certora/scripts/check.sh create mode 100644 certora/specs/GovernorBase.spec create mode 100644 certora/specs/Privileged.spec diff --git a/certora/harnesses/GovernorCountingSimpleHarness.sol b/certora/harnesses/GovernorCountingSimpleHarness.sol new file mode 100644 index 000000000..52e980a81 --- /dev/null +++ b/certora/harnesses/GovernorCountingSimpleHarness.sol @@ -0,0 +1,29 @@ +import "../../contracts/governance/extensions/GovernorCountingSimple.sol"; + +contract GovernorCountingSimpleHarness is GovernorCountingSimple { + + mapping(uint256 => uint256) _quorum; + + function quorum(uint256 blockNumber) public view override virtual returns (uint256) { + return _quorum[blockNumber]; + } + + mapping (address => mapping (uint256 => uint256)) _getVotes; + + function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) { + return _getVotes[account][blockNumber]; + } + + uint256 _votingDelay; + function votingDelay() public view override virtual returns (uint256) { + return _votingDelay; + } + + uint256 _votingPeriod; + function votingPeriod() public view override virtual returns (uint256) { + return _votingPeriod; + } + + constructor(string memory name) Governor(name) {} + +} \ No newline at end of file diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol new file mode 100644 index 000000000..d2df3d450 --- /dev/null +++ b/certora/harnesses/GovernorHarness.sol @@ -0,0 +1,58 @@ +import "../../contracts/governance/Governor.sol"; + +contract GovernorHarness is Governor { + + mapping(uint256 => uint256) _quorum; + + function quorum(uint256 blockNumber) public view override virtual returns (uint256) { + return _quorum[blockNumber]; + } + + mapping (address => mapping (uint256 => uint256)) _getVotes; + + function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) { + return _getVotes[account][blockNumber]; + } + + mapping (uint256 => bool) __quoromReached; + function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + return __quoromReached[proposalId]; + } + + mapping (uint256 => bool) __voteSucceeded; + function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + return __voteSucceeded[proposalId]; + } + + //string _COUNTING_MODE; + function COUNTING_MODE() public pure override virtual returns (string memory) { + return "dummy"; + } + + mapping(uint256 => mapping(address => bool)) _hasVoted; + function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) { + return _hasVoted[proposalId][account]; + } + + uint256 _votingDelay; + function votingDelay() public view override virtual returns (uint256) { + return _votingDelay; + } + + uint256 _votingPeriod; + function votingPeriod() public view override virtual returns (uint256) { + return _votingPeriod; + } + + function _countVote( + uint256 proposalId, + address account, + uint8 support, + uint256 weight + ) internal override virtual { + // havoc something + } + + constructor(string memory name) Governor(name) {} + +} \ No newline at end of file diff --git a/certora/harnesses/GovernorProposalThresholdHarness.sol b/certora/harnesses/GovernorProposalThresholdHarness.sol new file mode 100644 index 000000000..8301a76d8 --- /dev/null +++ b/certora/harnesses/GovernorProposalThresholdHarness.sol @@ -0,0 +1,58 @@ +import "../../contracts/governance/extensions/GovernorProposalThreshold.sol"; + +contract GovernorProposalThresholdHarness is GovernorProposalThreshold { + + mapping(uint256 => uint256) _quorum; + + function quorum(uint256 blockNumber) public view override virtual returns (uint256) { + return _quorum[blockNumber]; + } + + mapping (address => mapping (uint256 => uint256)) _getVotes; + + function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) { + return _getVotes[account][blockNumber]; + } + + mapping (uint256 => bool) __quoromReached; + function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + return __quoromReached[proposalId]; + } + + mapping (uint256 => bool) __voteSucceeded; + function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + return __voteSucceeded[proposalId]; + } + + //string _COUNTING_MODE; + function COUNTING_MODE() public pure override virtual returns (string memory) { + return "dummy"; + } + + mapping(uint256 => mapping(address => bool)) _hasVoted; + function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) { + return _hasVoted[proposalId][account]; + } + + uint256 _votingDelay; + function votingDelay() public view override virtual returns (uint256) { + return _votingDelay; + } + + uint256 _votingPeriod; + function votingPeriod() public view override virtual returns (uint256) { + return _votingPeriod; + } + + function _countVote( + uint256 proposalId, + address account, + uint8 support, + uint256 weight + ) internal override virtual { + // havoc something + } + + constructor(string memory name) Governor(name) {} + +} \ No newline at end of file diff --git a/certora/harnesses/GovernorTimelockCompoundHarness.sol b/certora/harnesses/GovernorTimelockCompoundHarness.sol new file mode 100644 index 000000000..5513546ab --- /dev/null +++ b/certora/harnesses/GovernorTimelockCompoundHarness.sol @@ -0,0 +1,58 @@ +import "../../contracts/governance/extensions/GovernorTimelockCompound.sol"; + +contract GovernorTimelockCompoundHarness is GovernorTimelockCompound { + + mapping(uint256 => uint256) _quorum; + + function quorum(uint256 blockNumber) public view override virtual returns (uint256) { + return _quorum[blockNumber]; + } + + mapping (address => mapping (uint256 => uint256)) _getVotes; + + function getVotes(address account, uint256 blockNumber) public view override virtual returns (uint256) { + return _getVotes[account][blockNumber]; + } + + mapping (uint256 => bool) __quoromReached; + function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + return __quoromReached[proposalId]; + } + + mapping (uint256 => bool) __voteSucceeded; + function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + return __voteSucceeded[proposalId]; + } + + //string _COUNTING_MODE; + function COUNTING_MODE() public pure override virtual returns (string memory) { + return "dummy"; + } + + mapping(uint256 => mapping(address => bool)) _hasVoted; + function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) { + return _hasVoted[proposalId][account]; + } + + uint256 _votingDelay; + function votingDelay() public view override virtual returns (uint256) { + return _votingDelay; + } + + uint256 _votingPeriod; + function votingPeriod() public view override virtual returns (uint256) { + return _votingPeriod; + } + + function _countVote( + uint256 proposalId, + address account, + uint8 support, + uint256 weight + ) internal override virtual { + // havoc something + } + + constructor(string memory name, ICompoundTimelock timelock) Governor(name) GovernorTimelockCompound(timelock) {} + +} \ No newline at end of file diff --git a/certora/harnesses/GovernorVotesHarness.sol b/certora/harnesses/GovernorVotesHarness.sol new file mode 100644 index 000000000..65a095156 --- /dev/null +++ b/certora/harnesses/GovernorVotesHarness.sol @@ -0,0 +1,52 @@ +import "../../contracts/governance/extensions/GovernorVotes.sol"; + +contract GovernorVotesHarness is GovernorVotes { + + mapping(uint256 => uint256) _quorum; + + function quorum(uint256 blockNumber) public view override virtual returns (uint256) { + return _quorum[blockNumber]; + } + + mapping (uint256 => bool) __quoromReached; + function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + return __quoromReached[proposalId]; + } + + mapping (uint256 => bool) __voteSucceeded; + function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + return __voteSucceeded[proposalId]; + } + + //string _COUNTING_MODE; + function COUNTING_MODE() public pure override virtual returns (string memory) { + return "dummy"; + } + + mapping(uint256 => mapping(address => bool)) _hasVoted; + function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) { + return _hasVoted[proposalId][account]; + } + + uint256 _votingDelay; + function votingDelay() public view override virtual returns (uint256) { + return _votingDelay; + } + + uint256 _votingPeriod; + function votingPeriod() public view override virtual returns (uint256) { + return _votingPeriod; + } + + function _countVote( + uint256 proposalId, + address account, + uint8 support, + uint256 weight + ) internal override virtual { + // havoc something + } + + constructor(string memory name) Governor(name) {} + +} \ No newline at end of file diff --git a/certora/harnesses/GovernorVotesQuorumFractionHarness.sol b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol new file mode 100644 index 000000000..3c7015eb9 --- /dev/null +++ b/certora/harnesses/GovernorVotesQuorumFractionHarness.sol @@ -0,0 +1,46 @@ +import "../../contracts/governance/extensions/GovernorVotesQuorumFractionGovernor.sol"; + +contract GovernorVotesQuorumFractionHarness is GovernorVotesQuorumFraction { + + mapping (uint256 => bool) __quoromReached; + function _quorumReached(uint256 proposalId) internal view override virtual returns (bool) { + return __quoromReached[proposalId]; + } + + mapping (uint256 => bool) __voteSucceeded; + function _voteSucceeded(uint256 proposalId) internal view override virtual returns (bool) { + return __voteSucceeded[proposalId]; + } + + //string _COUNTING_MODE; + function COUNTING_MODE() public pure override virtual returns (string memory) { + return "dummy"; + } + + mapping(uint256 => mapping(address => bool)) _hasVoted; + function hasVoted(uint256 proposalId, address account) public view override virtual returns (bool) { + return _hasVoted[proposalId][account]; + } + + uint256 _votingDelay; + function votingDelay() public view override virtual returns (uint256) { + return _votingDelay; + } + + uint256 _votingPeriod; + function votingPeriod() public view override virtual returns (uint256) { + return _votingPeriod; + } + + function _countVote( + uint256 proposalId, + address account, + uint8 support, + uint256 weight + ) internal override virtual { + // havoc something + } + + constructor(string memory name) Governor(name) {} + +} \ No newline at end of file diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh new file mode 100755 index 000000000..4caada718 --- /dev/null +++ b/certora/scripts/Governor.sh @@ -0,0 +1,2 @@ +certoraRun certora/harnesses/GovernorHarness.sol \ + --verify GovernorHarness:certora/specs/Privileged.spec \ No newline at end of file diff --git a/certora/scripts/GovernorCountingSimple.sh b/certora/scripts/GovernorCountingSimple.sh new file mode 100755 index 000000000..95c2c2551 --- /dev/null +++ b/certora/scripts/GovernorCountingSimple.sh @@ -0,0 +1,2 @@ +certoraRun certora/harnesses/GovernorCountingSimpleHarness.sol \ + --verify GovernorCountingSimpleHarness:certora/specs/Privileged.spec \ No newline at end of file diff --git a/certora/scripts/GovernorProposalThreshold.sh b/certora/scripts/GovernorProposalThreshold.sh new file mode 100755 index 000000000..cb10572fc --- /dev/null +++ b/certora/scripts/GovernorProposalThreshold.sh @@ -0,0 +1,2 @@ +certoraRun certora/harnesses/GovernorProposalThresholdHarness.sol \ + --verify GovernorProposalThresholdHarness:certora/specs/Privileged.spec \ No newline at end of file diff --git a/certora/scripts/GovernorTimelockCompound.sh b/certora/scripts/GovernorTimelockCompound.sh new file mode 100755 index 000000000..9cbdd1ea0 --- /dev/null +++ b/certora/scripts/GovernorTimelockCompound.sh @@ -0,0 +1,2 @@ +certoraRun certora/harnesses/GovernorTimelockCompoundHarness.sol \ + --verify GovernorTimelockCompoundHarness:certora/specs/Privileged.spec \ No newline at end of file diff --git a/certora/scripts/GovernorVotes.sh b/certora/scripts/GovernorVotes.sh new file mode 100755 index 000000000..1dc476445 --- /dev/null +++ b/certora/scripts/GovernorVotes.sh @@ -0,0 +1,2 @@ +certoraRun certora/harnesses/GovernorVotesHarness.sol \ + --verify GovernorVotesHarness:certora/specs/Privileged.spec \ No newline at end of file diff --git a/certora/scripts/GovernorVotesQuorumFractionHarness.sh b/certora/scripts/GovernorVotesQuorumFractionHarness.sh new file mode 100755 index 000000000..239339ade --- /dev/null +++ b/certora/scripts/GovernorVotesQuorumFractionHarness.sh @@ -0,0 +1,2 @@ +certoraRun certora/harnesses/GovernorVotesQuorumFractionHarness.sol \ + --verify GovernorVotesQuorumFractionHarness:certora/specs/Privileged.spec \ No newline at end of file diff --git a/certora/scripts/check.sh b/certora/scripts/check.sh new file mode 100755 index 000000000..0cb980dc3 --- /dev/null +++ b/certora/scripts/check.sh @@ -0,0 +1,7 @@ +echo "Usage: Contract Spec" +echo "e.g. GovernorVotes Privileged" +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 diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec new file mode 100644 index 000000000..58c07582f --- /dev/null +++ b/certora/specs/GovernorBase.spec @@ -0,0 +1,79 @@ +// Governor.sol base definitions +methods { + proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart +} +ghost proposalVoteStart(uint256) returns uint64 { + init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0; +} +ghost proposalVoteEnd(uint256) returns uint64 { + init_state axiom forall uint256 pId. proposalVoteEnd(pId) == 0; +} +ghost proposalExecuted(uint256) returns bool { + init_state axiom forall uint256 pId. !proposalExecuted(pId); +} +ghost proposalCanceled(uint256) returns bool { + init_state axiom forall uint256 pId. !proposalCanceled(pId); +} + +hook Sstore _proposals[KEY uint256 pId].(offset 0) uint64 newValue STORAGE { + havoc proposalVoteStart assuming ( + proposalVoteStart@new(pId) == newValue + && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2)) + ); +} + +hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0) STORAGE { + require proposalVoteStart(pId) == value; +} + + +hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE { + havoc proposalVoteEnd assuming ( + proposalVoteEnd@new(pId) == newValue + && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2)) + ); +} + +hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE { + require proposalVoteEnd(pId) == value; +} + +rule sanityCheckVoteStart(method f, uint256 pId) { + uint64 preGhost = proposalVoteStart(pId); + uint256 pre = proposalSnapshot(pId); + + env e; + calldataarg arg; + f(e, arg); + + uint64 postGhost = proposalVoteStart(pId); + uint256 post = proposalSnapshot(pId); + + assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes"; + assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end"; +} + +rule sanityCheckVoteEnd(method f, uint256 pId) { + uint64 preGhost = proposalVoteEnd(pId); + uint256 pre = proposalSnapshot(pId); + + env e; + calldataarg arg; + f(e, arg); + + uint64 postGhost = proposalVoteEnd(pId); + uint256 post = proposalSnapshot(pId); + + assert preGhost == postGhost <=> pre == post, "ghost changes are correlated with getter changes"; + assert pre == preGhost => post == postGhost, "if correlated at the beginning should be correlated at the end"; +} + +/** + * A proposal cannot end unless it started. + */ +invariant voteStartBeforeVoteEnd(uint256 pId) proposalVoteStart(pId) < proposalVoteEnd(pId) + +/** + * A proposal cannot be both executed and canceled. + */ +invariant noBothExecutedAndCanceled(uint256 pId) !proposalExecuted(pId) || !proposalCanceled(pId) \ No newline at end of file diff --git a/certora/specs/Privileged.spec b/certora/specs/Privileged.spec new file mode 100644 index 000000000..f9615a619 --- /dev/null +++ b/certora/specs/Privileged.spec @@ -0,0 +1,31 @@ +definition knownAsNonPrivileged(method f) returns bool = false +/* ( f.selector == isWhitelistedOtoken(address).selector || + f.selector == isWhitelistedProduct(address,address,address,bool).selector || + f.selector == owner().selector || + f.selector == isWhitelistedCallee(address).selector || + f.selector == whitelistOtoken(address).selector || + f.selector == addressBook().selector || + f.selector == isWhitelistedCollateral(address).selector )*/; + + + +rule privilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require !knownAsNonPrivileged(f); + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != privileged; + invoke f(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "${f.selector} can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +}