setup GovLateQuorum and add 3 rules for deadlines

certora/applyHarness.patch

@@ -1,6 +1,6 @@
 diff -ruN access/AccessControl.sol access/AccessControl.sol
---- access/AccessControl.sol	2022-03-02 09:14:55.000000000 -0800
-+++ access/AccessControl.sol	2022-04-08 17:31:22.000000000 -0700
+--- access/AccessControl.sol	2022-05-06 13:44:28.000000000 -0700
++++ access/AccessControl.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -93,7 +93,7 @@
       *
       * _Available since v4.6._
@@ -10,9 +10,21 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
          _checkRole(role, _msgSender());
      }
  
+diff -ruN governance/Governor.sol governance/Governor.sol
+--- governance/Governor.sol	2022-05-09 09:11:10.000000000 -0700
++++ governance/Governor.sol	2022-05-09 09:49:26.000000000 -0700
+@@ -42,7 +42,7 @@
+ 
+     string private _name;
+ 
+-    mapping(uint256 => ProposalCore) private _proposals;
++    mapping(uint256 => ProposalCore) internal _proposals;
+ 
+     // This queue keeps track of the governor operating on itself. Calls to functions protected by the
+     // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
 diff -ruN governance/TimelockController.sol governance/TimelockController.sol
---- governance/TimelockController.sol	2022-03-02 09:14:55.000000000 -0800
-+++ governance/TimelockController.sol	2022-04-08 17:31:22.000000000 -0700
+--- governance/TimelockController.sol	2022-05-06 13:44:28.000000000 -0700
++++ governance/TimelockController.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -24,10 +24,10 @@
      bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
@@ -32,9 +44,23 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
      }
 -}
 +} 
+diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
+--- governance/extensions/GovernorPreventLateQuorum.sol	2022-05-09 09:11:01.000000000 -0700
++++ governance/extensions/GovernorPreventLateQuorum.sol	2022-05-09 09:49:26.000000000 -0700
+@@ -21,8 +21,8 @@
+     using SafeCast for uint256;
+     using Timers for Timers.BlockNumber;
+ 
+-    uint64 private _voteExtension;
+-    mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines;
++    uint64 internal _voteExtension;
++    mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines;
+ 
+     /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
+     event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
 diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
---- governance/utils/Votes.sol	2022-03-02 09:14:55.000000000 -0800
-+++ governance/utils/Votes.sol	2022-04-08 17:44:19.000000000 -0700
+--- governance/utils/Votes.sol	2022-05-06 13:44:28.000000000 -0700
++++ governance/utils/Votes.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -35,7 +35,25 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -108,8 +134,8 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 +    function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
  }
 diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
---- token/ERC1155/ERC1155.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC1155/ERC1155.sol	2022-04-08 17:31:22.000000000 -0700
+--- token/ERC1155/ERC1155.sol	2022-05-06 13:44:28.000000000 -0700
++++ token/ERC1155/ERC1155.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -268,7 +268,7 @@
          uint256 id,
          uint256 amount,
@@ -165,8 +191,8 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
              try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
                  bytes4 response
 diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
---- token/ERC20/ERC20.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/ERC20.sol	2022-04-08 17:31:22.000000000 -0700
+--- token/ERC20/ERC20.sol	2022-05-06 13:44:28.000000000 -0700
++++ token/ERC20/ERC20.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -277,7 +277,7 @@
       * - `account` cannot be the zero address.
       * - `account` must have at least `amount` tokens.
@@ -186,8 +212,8 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
  
      /**
 diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
---- token/ERC20/extensions/ERC20FlashMint.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-04-08 17:31:22.000000000 -0700
+--- token/ERC20/extensions/ERC20FlashMint.sol	2022-05-06 13:44:28.000000000 -0700
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -40,9 +40,11 @@
          require(token == address(this), "ERC20FlashMint: wrong token");
          // silence warning about unused variable without the addition of bytecode.
@@ -202,8 +228,8 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
       * @dev Performs a flash loan. New tokens are minted and sent to the
       * `receiver`, who is required to implement the {IERC3156FlashBorrower}
 diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
---- token/ERC20/extensions/ERC20Votes.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/extensions/ERC20Votes.sol	2022-04-08 17:31:22.000000000 -0700
+--- token/ERC20/extensions/ERC20Votes.sol	2022-05-06 13:43:21.000000000 -0700
++++ token/ERC20/extensions/ERC20Votes.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -33,8 +33,8 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -335,8 +361,8 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
          return a + b;
      }
 diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
---- token/ERC20/extensions/ERC20Wrapper.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC20/extensions/ERC20Wrapper.sol	2022-04-08 17:31:22.000000000 -0700
+--- token/ERC20/extensions/ERC20Wrapper.sol	2022-05-06 13:44:28.000000000 -0700
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -44,7 +44,7 @@
       * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
       * function that can be exposed with access control if desired.
@@ -347,8 +373,8 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr
          _mint(account, value);
          return value;
 diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
---- token/ERC721/extensions/draft-ERC721Votes.sol	2022-03-02 09:14:55.000000000 -0800
-+++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-04-08 17:31:22.000000000 -0700
+--- token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-06 13:44:28.000000000 -0700
++++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-09 09:49:26.000000000 -0700
 @@ -34,7 +34,7 @@
      /**
       * @dev Returns the balance of `account`.

certora/harnesses/GovernorPreventLateQuorumHarness.sol

@@ -0,0 +1,159 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/governance/extensions/GovernorPreventLateQuorum.sol";
+import "../munged/governance/Governor.sol";
+import "../munged/governance/extensions/GovernorCountingSimple.sol";
+import "../munged/governance/extensions/GovernorVotes.sol";
+import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
+import "../munged/governance/extensions/GovernorTimelockControl.sol";
+import "../munged/token/ERC20/extensions/ERC20Votes.sol";
+
+contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl, GovernorPreventLateQuorum {
+    using SafeCast for uint256;
+    using Timers for Timers.BlockNumber;
+    constructor(IVotes _token, TimelockController _timelock, uint64 initialVoteExtension, uint256 quorumNumeratorValue)
+        Governor("Harness")
+        GovernorVotes(_token)
+        GovernorVotesQuorumFraction(quorumNumeratorValue)
+        GovernorTimelockControl(_timelock)
+        GovernorPreventLateQuorum(initialVoteExtension)
+    {}
+
+    // variable added to check when _castVote is called
+    uint256 public latestCastVoteCall;
+
+    // Harness from GovernorPreventLateQuorum //
+    
+    function getVoteExtension() public view returns(uint64) {
+        return _voteExtension;
+    }
+
+    function getExtendedDeadlineIsUnset(uint256 id) public view returns(bool) {
+        return _extendedDeadlines[id].isUnset();
+    }
+
+    function getExtendedDeadline(uint256 id) public view returns(uint64) {
+        return _extendedDeadlines[id].getDeadline();
+    }
+
+    // Harness from GovernorCountingSimple // 
+    
+    function  quorumReached(uint256 proposalId) public view returns(bool) {
+        return _quorumReached(proposalId);
+    }
+
+    // Harness from Governor //
+
+    function isExecuted(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].executed;
+    }
+    
+    function isCanceled(uint256 proposalId) public view returns (bool) {
+        return _proposals[proposalId].canceled;
+    }
+
+    // The following functions are overrides required by Solidity added by Certora. //
+
+    function proposalDeadline(uint256 proposalId) public view virtual override(Governor, GovernorPreventLateQuorum, IGovernor) returns (uint256) {
+        return super.proposalDeadline(proposalId);
+    }
+
+    function _castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason,
+        bytes memory params
+    ) internal virtual override(Governor, GovernorPreventLateQuorum) returns (uint256) {
+        latestCastVoteCall = block.number;
+        return super._castVote(proposalId, account, support, reason, params);
+    }
+
+    function castVote(
+        uint256 proposalId,
+        address account,
+        uint8 support,
+        string memory reason,
+        bytes memory params
+    ) public returns(uint256) {
+        return _castVote(proposalId, account, support, reason, params);
+    }
+
+    function lateQuorumVoteExtension() public view virtual override returns (uint64) {
+        return super.lateQuorumVoteExtension();
+    }
+
+    function setLateQuorumVoteExtension(uint64 newVoteExtension) public virtual override onlyGovernance {
+        super.setLateQuorumVoteExtension(newVoteExtension);
+    }
+
+    // The following functions are overrides required by Solidity added by OZ Wizard. //
+
+    function votingDelay() public pure override returns (uint256) {
+        return 1; // 1 block
+    }
+
+    function votingPeriod() public pure override returns (uint256) {
+        return 45818; // 1 week
+    }
+
+    function quorum(uint256 blockNumber)
+        public
+        view
+        override(IGovernor, GovernorVotesQuorumFraction)
+        returns (uint256)
+    {
+        return super.quorum(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, 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);
+    }
+}

certora/munged/governance/Governor.sol

@@ -42,7 +42,7 @@ abstract contract Governor is Context, ERC165, EIP712, IGovernor {
 
     string private _name;
 
-    mapping(uint256 => ProposalCore) private _proposals;
+    mapping(uint256 => ProposalCore) internal _proposals;
 
     // This queue keeps track of the governor operating on itself. Calls to functions protected by the
     // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},

certora/munged/governance/extensions/GovernorPreventLateQuorum.sol

@@ -21,8 +21,8 @@ abstract contract GovernorPreventLateQuorum is Governor {
     using SafeCast for uint256;
     using Timers for Timers.BlockNumber;
 
-    uint64 private _voteExtension;
-    mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines;
+    uint64 internal _voteExtension;
+    mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines;
 
     /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
     event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);

certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -0,0 +1,9 @@
+certoraRun \
+    certora/harnesses/ERC721VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    --solc solc \
+    --optimistic_loop \
+    --loop_iter 3 \
+    --cloud \
+    --rule $1 \
+    --msg "GovernorPreventLateQuorum $1"

certora/specs/GovernorPreventLateQuorum.spec

@@ -0,0 +1,115 @@
+//////////////////////////////////////////////////////////////////////////////
+///////////////////// Governor.sol base definitions //////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+using ERC721VotesHarness as erc20votes
+
+methods {
+    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
+    proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd
+    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
+    isExecuted(uint256) returns bool envfree
+    isCanceled(uint256) returns bool envfree
+    execute(address[], uint256[], bytes[], bytes32) returns uint256
+    hasVoted(uint256, address) returns bool
+    castVote(uint256, uint8) returns uint256
+    updateQuorumNumerator(uint256)
+    queue(address[], uint256[], bytes[], bytes32) returns uint256
+    quorumNumerator() returns uint256 envfree
+    quorumDenominator() returns uint256 envfree
+    votingPeriod() returns uint256 envfree
+    lateQuorumVoteExtension() returns uint64 envfree
+
+    // harness
+    getExtendedDeadlineIsUnset(uint256) returns bool envfree
+    getExtendedDeadline(uint256) returns uint64 envfree
+    quorumReached(uint256) returns bool envfree
+    latestCastVoteCall() returns uint256 envfree // more robust check than f.selector == _castVote(...).selector
+
+    // function summarization
+    proposalThreshold() returns uint256 envfree
+
+    getVotes(address, uint256) returns uint256 => DISPATCHER(true)
+
+    getPastTotalSupply(uint256 t) returns uint256      => PER_CALLEE_CONSTANT
+    getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT
+}
+
+//////////////////////////////////////////////////////////////////////////////
+//////////////////////////////// Definitions /////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
+
+// create definition for extended
+definition deadlineCanBeExtended(uint256 id) returns bool = 
+    getExtendedDeadlineIsUnset(id) &&
+    getExtendedDeadline(id) == 0 && 
+    !quorumReached(id);
+
+definition deadlineHasBeenExtended(uint256 id) returns bool = 
+    !getExtendedDeadlineIsUnset(id) &&
+    getExtendedDeadline(id) > 0 &&
+    quorumReached(id);
+
+
+
+// RULE deadline can only be extended once
+    // 1. if deadline changes then we have state transition from deadlineCanBeExtended to deadlineHasBeenExtended
+rule deadlineChangeEffects(method f) filtered {f -> !f.isView /* bottleneck, restrict for faster testing && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } {
+    env e; calldataarg args; uint256 id;
+
+    require (latestCastVoteCall() < e.block.number);
+    require (quorumNumerator() <= quorumDenominator());
+    require deadlineCanBeExtended(id);
+    require (proposalDeadline(id) < e.block.number 
+    && proposalDeadline(id) >= proposalSnapshot(id) + votingPeriod() 
+    && proposalSnapshot(id) > e.block.number); 
+    
+    uint256 deadlineBefore = proposalDeadline(id);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(id);
+    
+    assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(id));
+}
+
+    // 2. cant unextend
+rule deadlineCantBeUnextended(method f) filtered {f -> !f.isView /* && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } {
+    env e; calldataarg args; uint256 id;
+    require(deadlineHasBeenExtended(id));
+    f(e, args);
+    assert(deadlineHasBeenExtended(id));
+}
+
+    // 3. extended => can't change deadline
+        //@note if deadline changed, then it wasnt extended and castvote was called
+rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView /* && f.selector != propose(address[], uint256[], bytes[], string).selector*/ } {
+    env e; calldataarg args;
+    uint256 id;
+    require(deadlineHasBeenExtended(id)); // stays true
+    require (proposalDeadline(id) < e.block.number 
+    && proposalDeadline(id) >= proposalSnapshot(id) + votingPeriod() 
+    && proposalSnapshot(id) > e.block.number); 
+    uint256 deadlineBefore = proposalDeadline(id);
+    f(e, args);
+    uint256 deadlineAfter = proposalDeadline(id);
+    assert(deadlineBefore == deadlineAfter, "deadline can not be extended twice");
+}
+
+
+// RULE deadline can only extended if quorum reached w/ <= timeOfExtension left to vote
+// 3 rules
+    // 1. voting increases total votes
+    // 2. number of votes > quorum => quorum reached
+    // 3. deadline can only extended if quorum reached w/ <= timeOfExtension left to vote
+rule deadlineCanOnlyBeExtenededIfQuorumReached() {
+    env e; method f; calldataarg args;
+    uint256 id;
+    require(getExtendedDeadlineIsUnset(id));
+    f(e, args);
+    assert(false);
+}
+
+// RULE extendedDeadline is used iff quorum is reached w/ <= extensionTime left to vote
+
+// RULE extendedDeadlineField is set iff quroum is reached 
+
+// RULE if the deadline/extendedDeadline has not been reached, you can still vote (base)