start work on governor

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) {}
+
+}

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) {}
+
+}

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) {}
+
+}

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) {}
+
+}

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) {}
+
+}

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) {}
+
+}

certora/scripts/Governor.sh

@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorHarness.sol \
+    --verify GovernorHarness:certora/specs/Privileged.spec

certora/scripts/GovernorCountingSimple.sh

@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorCountingSimpleHarness.sol \
+    --verify GovernorCountingSimpleHarness:certora/specs/Privileged.spec

certora/scripts/GovernorProposalThreshold.sh

@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorProposalThresholdHarness.sol \
+    --verify GovernorProposalThresholdHarness:certora/specs/Privileged.spec

certora/scripts/GovernorTimelockCompound.sh

@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorTimelockCompoundHarness.sol \
+    --verify GovernorTimelockCompoundHarness:certora/specs/Privileged.spec

certora/scripts/GovernorVotes.sh

@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorVotesHarness.sol \
+    --verify GovernorVotesHarness:certora/specs/Privileged.spec

certora/scripts/GovernorVotesQuorumFractionHarness.sh

@@ -0,0 +1,2 @@
+certoraRun certora/harnesses/GovernorVotesQuorumFractionHarness.sol \
+    --verify GovernorVotesQuorumFractionHarness:certora/specs/Privileged.spec

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 "$@"

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)

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";
+}