update

certora/diff/governance_Governor.sol.patch

@@ -1,6 +1,6 @@
 --- governance/Governor.sol	2023-03-07 10:48:47.730155491 +0100
-+++ governance/Governor.sol	2023-03-10 10:13:31.926616811 +0100
-@@ -216,6 +216,16 @@
++++ governance/Governor.sol	2023-03-13 14:07:30.704202049 +0100
+@@ -216,6 +216,21 @@
          return _proposals[proposalId].proposer;
      }
  
@@ -13,6 +13,11 @@
 +    function _isCanceled(uint256 proposalId) internal view returns (bool) {
 +        return _proposals[proposalId].canceled;
 +    }
++
++    // FV
++    function _governanceCallLength() public view returns (uint256) {
++        return _governanceCall.length();
++    }
 +
      /**
       * @dev Amount of votes already cast passes the threshold limit.

certora/diff/token_ERC721_ERC721.sol.patch

@@ -0,0 +1,14 @@
+--- token/ERC721/ERC721.sol	2023-03-07 10:48:47.736822221 +0100
++++ token/ERC721/ERC721.sol	2023-03-09 19:50:20.555856358 +0100
+@@ -199,6 +199,11 @@
+         return _owners[tokenId];
+     }
+ 
++    // FV
++    function _getApproved(uint256 tokenId) internal view returns (address) {
++        return _tokenApprovals[tokenId];
++    }
++
+     /**
+      * @dev Returns whether `tokenId` exists.
+      *

certora/harnesses/GovernorHarness.sol

@@ -64,6 +64,10 @@ contract GovernorHarness is
         return _isCanceled(proposalId);
     }
 
+    function governanceCallLength() public view returns (uint256) {
+        return _governanceCallLength();
+    }
+
     // Harness from GovernorCountingSimple
     function getAgainstVotes(uint256 proposalId) public view returns (uint256) {
         (uint256 againstVotes,,) = proposalVotes(proposalId);

certora/run.js

@@ -22,14 +22,15 @@ if (request.startsWith('-')) {
 const [reqSpec, reqContract] = request.split(':').reverse();
 
 const specs = require(__dirname + '/specs.js')
-  .filter(entry => !reqSpec || micromatch(entry.spec, reqSpec))
-  .filter(entry => !reqContract || micromatch(entry.contract, reqContract));
+  .filter(entry => !reqSpec || micromatch.isMatch(entry.spec, reqSpec))
+  .filter(entry => !reqContract || micromatch.isMatch(entry.contract, reqContract));
 
 if (specs.length === 0) {
   console.error(`Error: Requested spec '${request}' not found in specs.json`);
   process.exit(1);
 }
 
+console.table(specs.map(spec => `${spec.contract}:${spec.spec} ${spec.options.join(' ')}`))
 for (const { spec, contract, files, options = [] } of Object.values(specs)) {
   limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]);
 }

certora/specs.js

@@ -1,6 +1,7 @@
 const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat())));
 
 module.exports = [
+  // AccessControl
   {
     spec: 'AccessControl',
     contract: 'AccessControlHarness',
@@ -16,6 +17,7 @@ module.exports = [
     contract: 'Ownable2StepHarness',
     files: ['certora/harnesses/Ownable2StepHarness.sol'],
   },
+  // Tokens
   {
     spec: 'ERC20',
     contract: 'ERC20PermitHarness',
@@ -34,13 +36,15 @@ module.exports = [
     files: ['certora/harnesses/ERC20PermitHarness.sol', 'certora/harnesses/ERC20WrapperHarness.sol'],
     options: ['--link ERC20WrapperHarness:_underlying=ERC20PermitHarness', '--optimistic_loop'],
   },
+  // Proxy
   {
     spec: 'Initializable',
     contract: 'InitializableHarness',
     files: ['certora/harnesses/InitializableHarness.sol'],
   },
+  // Governor
   ...product(
-    ['GovernorBase', 'GovernorInvariants', 'GovernorStates', /*'GovernorFunctions'*/],
+    ['GovernorInvariants', 'GovernorBaseRules', 'GovernorStates'],
     ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
   ).map(([spec, token]) => ({
     spec,
@@ -48,4 +52,14 @@ module.exports = [
     files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
     options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
   })),
+  // WIP part
+  // ...product(
+  //   ['GovernorFunctions'],
+  //   ['ERC20VotesBlocknumberHarness'],
+  // ).map(([spec, token]) => ({
+  //   spec,
+  //   contract: 'GovernorHarness',
+  //   files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
+  //   options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
+  // })),
 ];

certora/specs/Governor.helpers.spec

@@ -20,6 +20,9 @@ function safeState(env e, uint256 pId) returns uint8 {
     return lastReverted ? UNSET() : result;
 }
 
+definition proposalCreated(uint256 pId) returns bool =
+    proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0;
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Filters                                                                                                             │

certora/specs/GovernorBase.spec → certora/specs/GovernorBaseRules.spec

@@ -1,80 +1,11 @@
 import "methods/IGovernor.spec"
 import "Governor.helpers.spec"
+import "GovernorInvariants.spec"
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Definitions                                                                                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-
-definition proposalCreated(uint256 pId) returns bool =
-    proposalSnapshot(pId) > 0 && proposalDeadline(pId) > 0 && proposalProposer(pId) != 0;
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: Votes start and end are either initialized (non zero) or uninitialized (zero) simultaneously             │
-│                                                                                                                     │
-│ This invariant assumes that the block number cannot be 0 at any stage of the contract cycle                         │
-│ This is very safe assumption as usually the 0 block is genesis block which is uploaded with data                    │
-│ by the developers and will not be valid to raise proposals (at the current way that block chain is functioning)     │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant proposalStateConsistency(uint256 pId)
-    (proposalProposer(pId) != 0 <=> proposalSnapshot(pId) != 0) && (proposalProposer(pId) != 0 <=> proposalDeadline(pId) != 0)
-    {
-        preserved with (env e) {
-            require clock(e) > 0;
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: cancel => created                                                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant canceledImplyCreated(uint pId)
-    isCanceled(pId) => proposalCreated(pId)
-    {
-        preserved with (env e) {
-            requireInvariant proposalStateConsistency(pId);
-            require clock(e) > 0;
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: executed => created                                                                                      │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant executedImplyCreated(uint pId)
-    isExecuted(pId) => proposalCreated(pId)
-    {
-        preserved with (env e) {
-            requireInvariant proposalStateConsistency(pId);
-            require clock(e) > 0;
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: Votes start before it ends                                                                               │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant voteStartBeforeVoteEnd(uint256 pId)
-    proposalSnapshot(pId) <= proposalDeadline(pId)
-    {
-        preserved {
-            requireInvariant proposalStateConsistency(pId);
-        }
-    }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: A proposal cannot be both executed and canceled simultaneously                                           │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant noBothExecutedAndCanceled(uint256 pId)
-    !isExecuted(pId) || !isCanceled(pId)
+use invariant proposalStateConsistency
+use invariant canceledImplyCreated
+use invariant executedImplyCreated
+use invariant noBothExecutedAndCanceled
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -143,7 +74,7 @@ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f,
 
     f(e, args);
 
-    assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed";
+    assert isExecuted(pId) => (quorumReachedBefore && voteSucceededBefore), "quorum not met or vote not succesfull";
 }
 
 /*
@@ -216,21 +147,24 @@ rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule stateOnlyAfterFunc(uint256 pId, env e, method f) {
-    bool createdBefore = proposalCreated(pId);
+    bool createdBefore  = proposalCreated(pId);
     bool executedBefore = isExecuted(pId);
     bool canceledBefore = isCanceled(pId);
 
     helperFunctionsWithRevert(e, f, pId);
 
-    assert (proposalCreated(pId) != createdBefore)
-        => (createdBefore == false && f.selector == propose(address[], uint256[], bytes[], string).selector),
-        "proposalCreated only changes in the propose method";
+    assert (proposalCreated(pId) != createdBefore) => (
+        createdBefore == false &&
+        f.selector == propose(address[], uint256[], bytes[], string).selector
+    ), "proposalCreated only changes in the propose method";
 
-    assert (isExecuted(pId) != executedBefore)
-        => (executedBefore == false && f.selector == execute(address[], uint256[], bytes[], bytes32).selector),
-        "isExecuted only changes in the execute method";
+    assert (isExecuted(pId) != executedBefore) => (
+        executedBefore == false &&
+        f.selector == execute(address[], uint256[], bytes[], bytes32).selector
+    ), "isExecuted only changes in the execute method";
 
-    assert (isCanceled(pId) != canceledBefore)
-        => (canceledBefore == false && f.selector == cancel(address[], uint256[], bytes[], bytes32).selector),
-        "isCanceled only changes in the cancel method";
+    assert (isCanceled(pId) != canceledBefore) => (
+        canceledBefore == false &&
+        f.selector == cancel(address[], uint256[], bytes[], bytes32).selector
+    ), "isCanceled only changes in the cancel method";
 }

certora/specs/GovernorFunctions.spec

@@ -95,3 +95,79 @@ rule castVote(uint256 pId, env e, method f)
     assert getForVotes(otherId)          != otherForVotesBefore     => (otherId == pId);
     assert getAbstainVotes(otherId)      != otherAbstainVotesBefore => (otherId == pId);
 }
+
+
+rule queue(uint256 pId, env e) {
+    require nonpayable(e);
+
+    uint256 otherId;
+
+    uint8 stateBefore      = state(e, pId);
+    uint8 otherStateBefore = state(e, otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    require pId == queue@withrevert(e, targets, values, calldatas, reason);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> stateBefore == SUCCEEDED();
+
+    // effect
+    assert success => (
+        state(e, pId) == QUEUED()
+    );
+
+    // no side-effect
+    assert state(e, otherId) != otherStateBefore => otherId == pId;
+}
+
+rule execute(uint256 pId, env e) {
+    require nonpayable(e);
+
+    uint256 otherId;
+
+    uint8 stateBefore      = state(e, pId);
+    uint8 otherStateBefore = state(e, otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    require pId == execute@withrevert(e, targets, values, calldatas, reason);
+    bool success = !lastReverted;
+
+    // liveness: can't check full equivalence because of execution call reverts
+    assert success => (stateBefore == SUCCEEDED() || stateBefore == QUEUED());
+
+    // effect
+    assert success => (
+        state(e, pId) == EXECUTED()
+    );
+
+    // no side-effect
+    assert state(e, otherId) != otherStateBefore => otherId == pId;
+}
+
+rule cancel(uint256 pId, env e) {
+    require nonpayable(e);
+
+    uint256 otherId;
+
+    uint8 stateBefore      = state(e, pId);
+    uint8 otherStateBefore = state(e, otherId);
+
+    address[] targets; uint256[] values; bytes[] calldatas; string reason;
+    require pId == cancel@withrevert(e, targets, values, calldatas, reason);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        stateBefore == PENDING() &&
+        e.msg.sender == proposalProposer(pId)
+    );
+
+    // effect
+    assert success => (
+        state(e, pId) == CANCELED()
+    );
+
+    // no side-effect
+    assert state(e, otherId) != otherStateBefore => otherId == pId;
+}

certora/specs/GovernorInvariants.spec

@@ -8,32 +8,70 @@ import "Governor.helpers.spec"
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule clockMode(env e) {
+    require e.block.number < max_uint48() && e.block.timestamp < max_uint48();
+
     assert clock(e) == e.block.number || clock(e) == e.block.timestamp;
     assert clock(e) == token_clock(e);
+
+    /// This causes a failure in the prover
+    // assert CLOCK_MODE(e) == token_CLOCK_MODE(e);
 }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: Proposal is UNSET iff the proposer, the snapshot and the deadline are unset.                             │
+│ Invariant: Votes start and end are either initialized (non zero) or uninitialized (zero) simultaneously             │
+│                                                                                                                     │
+│ This invariant assumes that the block number cannot be 0 at any stage of the contract cycle                         │
+│ This is very safe assumption as usually the 0 block is genesis block which is uploaded with data                    │
+│ by the developers and will not be valid to raise proposals (at the current way that block chain is functioning)     │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant createdConsistency(env e, uint256 pId)
-    safeState(e, pId) == UNSET() <=> proposalProposer(pId) == 0 &&
-    safeState(e, pId) == UNSET() <=> proposalSnapshot(pId) == 0 &&
-    safeState(e, pId) == UNSET() <=> proposalDeadline(pId) == 0 &&
-    safeState(e, pId) == UNSET()  => !isExecuted(pId) &&
-    safeState(e, pId) == UNSET()  => !isCanceled(pId)
+invariant proposalStateConsistency(uint256 pId)
+    (proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0) &&
+    (proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0)
     {
-        preserved {
+        preserved with (env e) {
+            require clock(e) > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: cancel => created                                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant canceledImplyCreated(uint pId)
+    isCanceled(pId) => proposalCreated(pId)
+    {
+        preserved with (env e) {
+            requireInvariant proposalStateConsistency(pId);
             require clock(e) > 0;
         }
     }
 
-invariant createdConsistencyWeak(uint256 pId)
-    proposalProposer(pId) == 0 <=> proposalSnapshot(pId) == 0 &&
-    proposalProposer(pId) == 0 <=> proposalDeadline(pId) == 0
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: executed => created                                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant executedImplyCreated(uint pId)
+    isExecuted(pId) => proposalCreated(pId)
     {
         preserved with (env e) {
+            requireInvariant proposalStateConsistency(pId);
+            require clock(e) > 0;
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: The state UNSET() correctly catched uninitialized proposal.                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant proposalStateConsistencyUnset(env e, uint256 pId)
+    proposalCreated(pId) <=> safeState(e, pId) == UNSET()
+    {
+        preserved {
             require clock(e) > 0;
         }
     }
@@ -47,7 +85,7 @@ invariant voteStartBeforeVoteEnd(uint256 pId)
     proposalSnapshot(pId) <= proposalDeadline(pId)
     {
         preserved {
-            requireInvariant createdConsistencyWeak(pId);
+            requireInvariant proposalStateConsistency(pId);
         }
     }
 
@@ -61,21 +99,8 @@ invariant noBothExecutedAndCanceled(uint256 pId)
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: Once a proposal is created, voteStart, voteEnd and proposer are immutable                                     │
+│ Invariant: the "governance call" dequeue is empty                                                                   │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule immutableFieldsAfterProposalCreation(uint256 pId, env e, method f, calldataarg arg)
-    filtered { f -> !skip(f) }
-{
-    require state(e, pId) != UNSET();
-
-    uint256 voteStart = proposalSnapshot(pId);
-    uint256 voteEnd   = proposalDeadline(pId);
-    address proposer  = proposalProposer(pId);
-
-    f(e, arg);
-
-    assert voteStart == proposalSnapshot(pId), "Start date was changed";
-    assert voteEnd   == proposalDeadline(pId), "End date was changed";
-    assert proposer  == proposalProposer(pId), "Proposer was changed";
-}
+invariant governanceCallLength()
+    governanceCallLength() == 0

certora/specs/GovernorStates.spec

@@ -1,6 +1,9 @@
 import "helpers.spec"
 import "methods/IGovernor.spec"
 import "Governor.helpers.spec"
+import "GovernorInvariants.spec"
+
+use invariant proposalStateConsistency
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -78,3 +81,45 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) {
         stateBefore == EXECUTED()  => false
     );
 }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: State corresponds to the vote timming and results                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule stateFollowsVoteTimmingAndResult(uint256 pId, env e) {
+    require clock(e) > 0; // Sanity
+    requireInvariant proposalStateConsistency(pId);
+
+    uint8  currentState = state(e, pId);
+    uint48 currentClock = clock(e);
+
+    // Pending = before vote starts
+    assert currentState == PENDING() => (
+        proposalSnapshot(pId) >= currentClock
+    );
+
+    // Active = after vote starts & before vote ends
+    assert currentState == ACTIVE() => (
+        proposalSnapshot(pId) < currentClock &&
+        proposalDeadline(pId) >= currentClock
+    );
+
+    // Succeeded = after vote end, with vote successfull and quorum reached
+    assert currentState == SUCCEEDED() => (
+        proposalDeadline(pId) < currentClock &&
+        (
+            quorumReached(pId) &&
+            voteSucceeded(pId)
+        )
+    );
+
+    // Succeeded = after vote end, with vote not successfull or quorum not reached
+    assert currentState == DEFEATED() => (
+        proposalDeadline(pId) < currentClock &&
+        (
+            !quorumReached(pId) ||
+            !voteSucceeded(pId)
+        )
+    );
+}

certora/specs/helpers.spec

@@ -1 +1,3 @@
 definition nonpayable(env e) returns bool = e.msg.value == 0;
+
+definition max_uint48() returns uint48 = 0xffffffffffff;

certora/specs/methods/IGovernor.spec

@@ -39,6 +39,7 @@ methods {
     voteSucceeded(uint256)              returns bool    envfree
     isExecuted(uint256)                 returns bool    envfree
     isCanceled(uint256)                 returns bool    envfree
+    governanceCallLength()              returns uint256 envfree
     getAgainstVotes(uint256)            returns uint256 envfree
     getForVotes(uint256)                returns uint256 envfree
     getAbstainVotes(uint256)            returns uint256 envfree

requirements.txt

@@ -1 +1 @@
-certora-cli==3.6.3
+certora-cli==3.6.4