finalize fist 3 rules; fix old governor spec

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "solidity.compileUsingRemoteVersion": "v0.8.2+commit.661d1103"
+}

certora/applyHarness.patch

@@ -1,6 +1,6 @@
 diff -ruN access/AccessControl.sol access/AccessControl.sol
 --- access/AccessControl.sol	2022-05-06 13:44:28.000000000 -0700
-+++ access/AccessControl.sol	2022-05-09 09:49:26.000000000 -0700
++++ access/AccessControl.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -93,7 +93,7 @@
       *
       * _Available since v4.6._
@@ -12,7 +12,7 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
  
 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
++++ governance/Governor.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -42,7 +42,7 @@
  
      string private _name;
@@ -24,7 +24,7 @@ diff -ruN governance/Governor.sol governance/Governor.sol
      // {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-05-06 13:44:28.000000000 -0700
-+++ governance/TimelockController.sol	2022-05-09 09:49:26.000000000 -0700
++++ governance/TimelockController.sol	2022-05-12 19:13:19.000000000 -0700
 @@ -24,10 +24,10 @@
      bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE");
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
@@ -38,7 +38,22 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
  
      /**
       * @dev Emitted when a call is scheduled as part of operation `id`.
-@@ -353,4 +353,4 @@
+@@ -332,10 +332,11 @@
+         uint256 value,
+         bytes calldata data
+     ) private {
+-        (bool success, ) = target.call{value: value}(data);
+-        require(success, "TimelockController: underlying transaction reverted");
++        return; // can't deal with external calls
++        // (bool success, ) = target.call{value: value}(data);
++        // require(success, "TimelockController: underlying transaction reverted");
+ 
+-        emit CallExecuted(id, index, target, value, data);
++        // emit CallExecuted(id, index, target, value, data);
+     }
+ 
+     /**
+@@ -353,4 +354,4 @@
          emit MinDelayChange(_minDelay, newDelay);
          _minDelay = newDelay;
      }
@@ -46,7 +61,7 @@ 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
++++ governance/extensions/GovernorPreventLateQuorum.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -21,8 +21,8 @@
      using SafeCast for uint256;
      using Timers for Timers.BlockNumber;
@@ -60,7 +75,7 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi
      event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
 diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 --- governance/utils/Votes.sol	2022-05-06 13:44:28.000000000 -0700
-+++ governance/utils/Votes.sol	2022-05-09 09:49:26.000000000 -0700
++++ governance/utils/Votes.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -35,7 +35,25 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -135,7 +150,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
  }
 diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
 --- token/ERC1155/ERC1155.sol	2022-05-06 13:44:28.000000000 -0700
-+++ token/ERC1155/ERC1155.sol	2022-05-09 09:49:26.000000000 -0700
++++ token/ERC1155/ERC1155.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -268,7 +268,7 @@
          uint256 id,
          uint256 amount,
@@ -192,7 +207,7 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
                  bytes4 response
 diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
 --- token/ERC20/ERC20.sol	2022-05-06 13:44:28.000000000 -0700
-+++ token/ERC20/ERC20.sol	2022-05-09 09:49:26.000000000 -0700
++++ token/ERC20/ERC20.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -277,7 +277,7 @@
       * - `account` cannot be the zero address.
       * - `account` must have at least `amount` tokens.
@@ -213,7 +228,7 @@ 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-05-06 13:44:28.000000000 -0700
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-05-09 09:49:26.000000000 -0700
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -40,9 +40,11 @@
          require(token == address(this), "ERC20FlashMint: wrong token");
          // silence warning about unused variable without the addition of bytecode.
@@ -229,7 +244,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
       * `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-05-06 13:43:21.000000000 -0700
-+++ token/ERC20/extensions/ERC20Votes.sol	2022-05-09 09:49:26.000000000 -0700
++++ token/ERC20/extensions/ERC20Votes.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -33,8 +33,8 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -362,7 +377,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
      }
 diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
 --- 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
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-05-11 11:17:20.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.
@@ -374,7 +389,7 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr
          return value;
 diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
 --- 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
++++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-11 11:17:20.000000000 -0700
 @@ -34,7 +34,7 @@
      /**
       * @dev Returns the balance of `account`.
@@ -384,3 +399,14 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/
          return balanceOf(account);
      }
  }
+diff -ruN utils/Address.sol utils/Address.sol
+--- utils/Address.sol	2022-05-06 13:43:21.000000000 -0700
++++ utils/Address.sol	2022-05-15 10:58:38.000000000 -0700
+@@ -131,6 +131,7 @@
+         uint256 value,
+         string memory errorMessage
+     ) internal returns (bytes memory) {
++        return "";
+         require(address(this).balance >= value, "Address: insufficient balance for call");
+         require(isContract(target), "Address: call to non-contract");
+ 

certora/harnesses/GovernorPreventLateQuorumHarness.sol

@@ -20,6 +20,8 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
         GovernorPreventLateQuorum(initialVoteExtension)
     {}
 
+    mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
+
     // variable added to check when _castVote is called
     uint256 public latestCastVoteCall;
 
@@ -39,12 +41,29 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
 
     // Harness from GovernorCountingSimple // 
     
-    function  quorumReached(uint256 proposalId) public view returns(bool) {
+    function quorumReached(uint256 proposalId) public view returns(bool) {
         return _quorumReached(proposalId);
     }
 
+    function voteSucceeded(uint256 proposalId) public view returns(bool) {
+        return _voteSucceeded(proposalId);
+    }
+
+    function countVote(uint256 proposalId,
+        address account,
+        uint8 support,
+        uint256 weight,
+        bytes memory // params
+        ) public view {
+        return _countVote(proposalId,account,support,weight,"");
+    }
+
     // Harness from Governor //
 
+    function getExecutor() public view returns (address){
+        return _executor();
+    }
+
     function isExecuted(uint256 proposalId) public view returns (bool) {
         return _proposals[proposalId].executed;
     }
@@ -66,10 +85,16 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
         string memory reason,
         bytes memory params
     ) internal virtual override(Governor, GovernorPreventLateQuorum) returns (uint256) {
+        // flag for when _castVote is called
         latestCastVoteCall = block.number;
-        return super._castVote(proposalId, account, support, reason, params);
-    }
 
+        // added to run GovernorCountingSimple.spec
+        uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params);
+        ghost_sum_vote_power_by_id[proposalId] += deltaWeight; 
+
+        return deltaWeight;
+    }
+    /*
     function castVote(
         uint256 proposalId,
         address account,
@@ -79,6 +104,7 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
     ) public returns(uint256) {
         return _castVote(proposalId, account, support, reason, params);
     }
+    */
 
     function lateQuorumVoteExtension() public view virtual override returns (uint64) {
         return super.lateQuorumVoteExtension();

certora/munged/governance/TimelockController.sol

@@ -332,10 +332,11 @@ contract TimelockController is AccessControl {
         uint256 value,
         bytes calldata data
     ) private {
-        (bool success, ) = target.call{value: value}(data);
-        require(success, "TimelockController: underlying transaction reverted");
+        return; // haven't dealt with external calls yet
+        // (bool success, ) = target.call{value: value}(data);
+        // require(success, "TimelockController: underlying transaction reverted");
 
-        emit CallExecuted(id, index, target, value, data);
+        // emit CallExecuted(id, index, target, value, data);
     }
 
     /**

certora/munged/utils/Address.sol

@@ -131,6 +131,7 @@ library Address {
         uint256 value,
         string memory errorMessage
     ) internal returns (bytes memory) {
+        return ""; // external calls havoc
         require(address(this).balance >= value, "Address: insufficient balance for call");
         require(isContract(target), "Address: call to non-contract");
 

certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -1,9 +1,14 @@
 certoraRun \
-    certora/harnesses/ERC721VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
-    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
+    certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \
     --solc solc \
     --optimistic_loop \
-    --loop_iter 3 \
-    --cloud \
+    --loop_iter 1 \
+    --staging \
+    --rule_sanity advanced \
+    --send_only \
     --rule $1 \
-    --msg "GovernorPreventLateQuorum $1"
+    --msg "$1" \
+
+
+

certora/specs/GovernorBase.spec

@@ -17,16 +17,16 @@ methods {
     queue(address[], uint256[], bytes[], bytes32) returns uint256
 
     // internal functions made public in harness:
-    _quorumReached(uint256) returns bool
-    _voteSucceeded(uint256) returns bool envfree
+    quorumReached(uint256) returns bool
+    voteSucceeded(uint256) returns bool envfree
 
     // 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
+    getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true)
+    getPastVotes(address, uint256) returns uint256 => DISPATCHER(true)
 
     //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true)
     //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
@@ -47,7 +47,7 @@ definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0
 
 function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
     address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash;
-    uint8 support; uint8 v; bytes32 r; bytes32 s;
+    uint8 support; uint8 v; bytes32 r; bytes32 s; bytes params;
 	if (f.selector == propose(address[], uint256[], bytes[], string).selector) {
 		uint256 result = propose@withrevert(e, targets, values, calldatas, reason);
         require(result == proposalId);
@@ -62,10 +62,15 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
 		castVoteBySig@withrevert(e, proposalId, support, v, r, s);
     } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) {
         queue@withrevert(e, targets, values, calldatas, descriptionHash);
-	} else {
+	} else if (f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector) {
+        castVoteWithReasonAndParamsBySig@withrevert(e, proposalId, support, reason, params, v, r, s);
+    } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) {
+        castVoteWithReasonAndParams@withrevert(e, proposalId, support, reason, params);
+    } else {
         calldataarg args;
         f@withrevert(e, args);
     }
+   
 }
 
 /*
@@ -152,8 +157,8 @@ invariant noBothExecutedAndCanceled(uint256 pId)
  */
 rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){
     bool isExecutedBefore = isExecuted(pId);
-    bool quorumReachedBefore = _quorumReached(e, pId);
-    bool voteSucceededBefore = _voteSucceeded(pId);
+    bool quorumReachedBefore = quorumReached(e, pId);
+    bool voteSucceededBefore = voteSucceeded(pId);
     
     calldataarg args;
     f(e, args);
@@ -283,6 +288,7 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f ->
       && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
       && f.selector != relay(address,uint256,bytes).selector
       && f.selector != 0xb9a61961 // __acceptAdmin()
+      && f.selector != setLateQuorumVoteExtension(uint64).selector
 } {
     env e; calldataarg args;
     uint256 pId;
@@ -305,6 +311,7 @@ rule allFunctionsRevertIfCanceled(method f) filtered {
       && f.selector != queue(address[],uint256[],bytes[],bytes32).selector
       && f.selector != relay(address,uint256,bytes).selector
       && f.selector != 0xb9a61961 // __acceptAdmin()
+      && f.selector != setLateQuorumVoteExtension(uint64).selector
 } {
     env e; calldataarg args;
     uint256 pId;

certora/specs/GovernorCountingSimple.spec

@@ -7,7 +7,6 @@ methods {
     proposalVotes(uint256) returns (uint256, uint256, uint256) envfree
 
     quorumNumerator() returns uint256
-    _executor() returns address
 
     getExecutor() returns address
 
@@ -184,7 +183,7 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) {
     
     bool hasVotedAfter = hasVoted(e, pId, acc);
 
-    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
+    assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter, "no correlation";
 }
 
 

certora/specs/GovernorPreventLateQuorum.spec

@@ -3,6 +3,7 @@
 //////////////////////////////////////////////////////////////////////////////
 
 using ERC721VotesHarness as erc721votes
+using ERC20VotesHarness as erc20votes
 
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
@@ -19,97 +20,101 @@ methods {
     quorumDenominator() returns uint256 envfree
     votingPeriod() returns uint256 envfree
     lateQuorumVoteExtension() returns uint64 envfree
+    propose(address[], uint256[], bytes[], string)
 
     // harness
     getExtendedDeadlineIsUnset(uint256) returns bool envfree
     getExtendedDeadline(uint256) returns uint64 envfree
     quorumReached(uint256) returns bool envfree
+    voteSucceeded(uint256) returns bool envfree
+    quorum(uint256) returns uint256
     latestCastVoteCall() returns uint256 envfree // more robust check than f.selector == _castVote(...).selector
 
     // function summarization
     proposalThreshold() returns uint256 envfree
 
+    // erc20votes dispatch
     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
+    // erc721votes/Votes dispatch
+    getPastTotalSupply(uint256) returns uint256 => DISPATCHER(true)
+    getPastVotes(address, uint256) returns uint256 => DISPATCHER(true)
+    // timelock dispatch
+    getMinDelay() returns uint256 => DISPATCHER(true)
+    
+    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
+    executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT
+    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT
 }
 
 //////////////////////////////////////////////////////////////////////////////
 //////////////////////////////// Definitions /////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
+// where can invariants help?
+// can I replace definitions with invariants?
+
 // create definition for extended
-definition deadlineCanBeExtended(uint256 id) returns bool = 
-    getExtendedDeadlineIsUnset(id) &&
-    getExtendedDeadline(id) == 0 && 
-    !quorumReached(id);
+definition deadlineCanBeExtended(uint256 pId) returns bool = 
+    getExtendedDeadlineIsUnset(pId) &&
+    !quorumReached(pId);
 
-definition deadlineHasBeenExtended(uint256 id) returns bool = 
-    !getExtendedDeadlineIsUnset(id) &&
-    getExtendedDeadline(id) > 0 &&
-    quorumReached(id);
+definition deadlineHasBeenExtended(uint256 pId) returns bool = 
+    !getExtendedDeadlineIsUnset(pId) &&
+    quorumReached(pId);
 
+definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
 
+//////////////////////////////////////////////////////////////////////////////
+////////////////////////////////// Rules /////////////////////////////////////
+//////////////////////////////////////////////////////////////////////////////
 
-// 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;
+// RULE deadline can only be extended only once PASSING but vacuous
+    // 1. if deadline changes then we have state transition to deadlineHasBeenExtended RULE PASSING; ADV SANITY PASSING
+rule deadlineChangeEffects(method f) 
+    filtered {
+        f -> !f.isView
+    } {
+    env e; calldataarg args; uint256 pId;
 
-    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); 
+    require (proposalCreated(pId));
     
-    uint256 deadlineBefore = proposalDeadline(id);
+    uint256 deadlineBefore = proposalDeadline(pId);
     f(e, args);
-    uint256 deadlineAfter = proposalDeadline(id);
+    uint256 deadlineAfter = proposalDeadline(pId);
     
-    assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(id));
+    assert(deadlineAfter > deadlineBefore => latestCastVoteCall() == e.block.number && deadlineHasBeenExtended(pId));
 }
 
-    // 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));
+    // 2. cant unextend RULE PASSING*; ADV SANITY PASSING
+rule deadlineCantBeUnextended(method f) 
+    filtered {
+        f -> !f.isView
+        && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function
+    } {
+    env e; calldataarg args; uint256 pId;
+
+    require(deadlineHasBeenExtended(pId));
+    require(proposalCreated(pId));
+    
     f(e, args);
-    assert(deadlineHasBeenExtended(id));
+    
+    assert(deadlineHasBeenExtended(pId));
 }
 
-    // 3. extended => can't change deadline
+    // 3. extended => can't change deadline RULE PASSING; ADV SANITY PASSING
         //@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);
+rule canExtendDeadlineOnce(method f) 
+    filtered {
+        f -> !f.isView 
+    } {
+    env e; calldataarg args; uint256 pId;
+
+    require(deadlineHasBeenExtended(pId));
+    require(proposalCreated(pId)); 
+    
+    uint256 deadlineBefore = proposalDeadline(pId);
     f(e, args);
-    uint256 deadlineAfter = proposalDeadline(id);
+    uint256 deadlineAfter = proposalDeadline(pId);
+    
     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)