FirstWizardHarness

certora/harnesses/GovernorBasicHarness.sol

@@ -0,0 +1,124 @@
+// 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/GovernorTimelockCompound.sol";
+
+/* 
+Wizard options:
+ERC20Votes
+TimelockCompound
+*/
+
+contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound {
+    constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction)
+        Governor(name)
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumFraction)
+        GovernorTimelockCompound(_timelock)
+    {}
+
+    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;
+
+    function votingDelay() public view override virtual returns (uint256) {
+        return _votingDelay;
+    }
+
+    uint256 _votingPeriod;
+
+    function votingPeriod() public view override virtual returns (uint256) {
+        return _votingPeriod;
+    }
+
+/*
+    function votingDelay() public pure override returns (uint256) {
+        return _votingDelay;
+    }
+
+
+    function votingPeriod() public pure override returns (uint256) {
+        return _votingPeriod;
+    }
+*/
+
+    // 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, GovernorTimelockCompound)
+        returns (ProposalState)
+    {
+        return super.state(proposalId);
+    }
+
+    function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
+        public
+        override(Governor, 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, GovernorTimelockCompound)
+    {
+        super._execute(proposalId, targets, values, calldatas, descriptionHash);
+    }
+
+    function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
+        internal
+        override(Governor, GovernorTimelockCompound)
+        returns (uint256)
+    {
+        return super._cancel(targets, values, calldatas, descriptionHash);
+    }
+
+    function _executor()
+        internal
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (address)
+    {
+        return super._executor();
+    }
+
+    function supportsInterface(bytes4 interfaceId)
+        public
+        view
+        override(Governor, GovernorTimelockCompound)
+        returns (bool)
+    {
+        return super.supportsInterface(interfaceId);
+    }
+}

certora/scripts/Governor.sh

@@ -4,5 +4,5 @@ certoraRun certora/harnesses/GovernorHarness.sol \
     --staging \
     --optimistic_loop \
     --settings -copyLoopUnroll=4 \
-    --rule noExecuteOrCancelBeforeStarting \
+    --rule voteStartBeforeVoteEnd \
     --msg "$1"

certora/scripts/GovernorBasic.sh

@@ -0,0 +1,8 @@
+certoraRun certora/harnesses/GovernorBasicHarness.sol \
+    --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \
+    --solc solc8.2 \
+    --staging \
+    --optimistic_loop \
+    --settings -copyLoopUnroll=4 \
+    --rule doubleVoting \
+    --msg "$1"

certora/specs/GovernorBase.spec

@@ -7,7 +7,7 @@ methods {
     hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
     isExecuted(uint256) returns bool envfree
     isCanceled(uint256) returns bool envfree
-    initialized(uint256) returns bool envfree
+    // initialized(uint256) returns bool envfree
 
     hasVoted(uint256, address) returns bool
 
@@ -176,3 +176,8 @@ rule doubleVoting(uint256 pId, uint8 sup) {
 
     assert reverted, "double voting accured";
 }
+
+/**
+* 
+*/
+//rule votingSumAndPower(uint256 pId, uint8 sup, method f) {}