update

certora/harnesses/GovernorHarness.sol

@@ -88,21 +88,6 @@ contract GovernorHarness is
         return abstainVotes;
     }
 
-    /// The following functions are overrides required by Solidity added by Certora.
-    // mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
-    //
-    // function _castVote(
-    //     uint256 proposalId,
-    //     address account,
-    //     uint8 support,
-    //     string memory reason,
-    //     bytes memory params
-    // ) internal virtual override returns (uint256) {
-    //     uint256 deltaWeight = super._castVote(proposalId, account, support, reason, params);
-    //     ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
-    //     return deltaWeight;
-    // }
-
     // The following functions are overrides required by Solidity added by OZ Wizard.
     function votingDelay() public pure override returns (uint256) {
         return 1; // 1 block

certora/specs/Governor.helpers.spec

@@ -7,10 +7,23 @@ import "methods/IGovernor.spec"
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 function clockSanity(env e) returns bool {
-    return
-        e.block.number < max_uint48() &&
-        e.block.timestamp < max_uint48() &&
-        clock(e) > 0;
+    return e.block.number    < max_uint48()
+        && e.block.timestamp < max_uint48()
+        && clock(e) > 0;
+}
+
+function validProposal(address[] targets, uint256[] values, bytes[] calldatas) returns bool {
+    return targets.length > 0
+        && targets.length == values.length
+        && targets.length == calldatas.length;
+}
+
+function validString(string s) returns bool {
+    return s.length < 0xffff;
+}
+
+function validBytes(bytes b) returns bool {
+    return b.length < 0xffff;
 }
 
 /*
@@ -18,15 +31,15 @@ function clockSanity(env e) returns bool {
 │ States                                                                                                              │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-definition UNSET()      returns uint8 = 255;
-definition PENDING()    returns uint8 = 0;
-definition ACTIVE()     returns uint8 = 1;
-definition CANCELED()   returns uint8 = 2;
-definition DEFEATED()   returns uint8 = 3;
-definition SUCCEEDED()  returns uint8 = 4;
-definition QUEUED()     returns uint8 = 5;
-definition EXPIRED()    returns uint8 = 6;
-definition EXECUTED()   returns uint8 = 7;
+definition UNSET()     returns uint8 = 255;
+definition PENDING()   returns uint8 = 0;
+definition ACTIVE()    returns uint8 = 1;
+definition CANCELED()  returns uint8 = 2;
+definition DEFEATED()  returns uint8 = 3;
+definition SUCCEEDED() returns uint8 = 4;
+definition QUEUED()    returns uint8 = 5;
+definition EXPIRED()   returns uint8 = 6;
+definition EXECUTED()  returns uint8 = 7;
 
 function safeState(env e, uint256 pId) returns uint8 {
     return proposalCreated(pId) ? state(e, pId): UNSET();
@@ -67,9 +80,6 @@ definition votingAll(method f) returns bool =
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 support) returns uint256 {
-    string reason; bytes params;
-    require reason.length >= 0;
-
     if (f.selector == castVote(uint256,uint8).selector)
     {
         require e.msg.sender == voter;
@@ -77,12 +87,14 @@ function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8
     }
     else  if (f.selector == castVoteWithReason(uint256,uint8,string).selector)
     {
-        require e.msg.sender == voter;
+        string reason;
+        require e.msg.sender == voter && validString(reason);
         return castVoteWithReason@withrevert(e, pId, support, reason);
     }
     else  if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector)
     {
-        require e.msg.sender == voter;
+        string reason; bytes params;
+        require e.msg.sender == voter && validString(reason) && validBytes(params);
         return castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params);
     }
     else

certora/specs/GovernorBaseRules.spec

@@ -152,3 +152,21 @@ rule allFunctionsRevertIfCanceled(uint256 pId, env e, method f, calldataarg args
 
     assert lastReverted, "Function was not reverted";
 }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Update operation are restricted to executor                                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule privilegedUpdate(env e, method f, calldataarg args)
+    filtered { f -> !skip(f) }
+{
+    address executorBefore        = getExecutor();
+    uint256 quorumNumeratorBefore = quorumNumerator();
+    address timelockBefore        = timelock();
+
+    f(e, args);
+
+    assert quorumNumerator() != quorumNumeratorBefore => e.msg.sender == executorBefore;
+    assert timelock()        != timelockBefore        => e.msg.sender == executorBefore;
+}

certora/specs/GovernorChanges.spec

@@ -18,22 +18,40 @@ rule changes(uint256 pId, env e, method f, calldataarg args)
 
     address user;
 
-    bool existBefore      = proposalCreated(pId);
-    bool isExecutedBefore = isExecuted(pId);
-    bool isCanceledBefore = isCanceled(pId);
-    bool isQueuedBefore   = isQueued(pId);
-    bool hasVotedBefore   = hasVoted(pId, user);
+    bool    existBefore        = proposalCreated(pId);
+    bool    isExecutedBefore   = isExecuted(pId);
+    bool    isCanceledBefore   = isCanceled(pId);
+    bool    isQueuedBefore     = isQueued(pId);
+    bool    hasVotedBefore     = hasVoted(pId, user);
+    uint256 votesAgainstBefore = getAgainstVotes(pId);
+    uint256 votesForBefore     = getForVotes(pId);
+    uint256 votesAbstainBefore = getAbstainVotes(pId);
 
     f(e, args);
 
-    assert proposalCreated(pId) != existBefore      => (!existBefore      && f.selector == propose(address[],uint256[],bytes[],string).selector);
-    assert isExecuted(pId)      != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector);
-    assert isCanceled(pId)      != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector);
-    assert hasVoted(pId, user)  != hasVotedBefore   => (!hasVotedBefore   && votingAll(f));
+    bool    existAfter        = proposalCreated(pId);
+    bool    isExecutedAfter   = isExecuted(pId);
+    bool    isCanceledAfter   = isCanceled(pId);
+    bool    isQueuedAfter     = isQueued(pId);
+    bool    hasVotedAfter     = hasVoted(pId, user);
+    uint256 votesAgainstAfter = getAgainstVotes(pId);
+    uint256 votesForAfter     = getForVotes(pId);
+    uint256 votesAbstainAfter = getAbstainVotes(pId);
+
+    // propose, execute, cancel
+    assert existAfter      != existBefore      => (!existBefore      && f.selector == propose(address[],uint256[],bytes[],string).selector);
+    assert isExecutedAfter != isExecutedBefore => (!isExecutedBefore && f.selector == execute(address[],uint256[],bytes[],bytes32).selector);
+    assert isCanceledAfter != isCanceledBefore => (!isCanceledBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector);
 
     // queue is cleared on cancel
-    assert isQueued(pId) != isQueuedBefore => (
+    assert isQueuedAfter != isQueuedBefore => (
         (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) ||
         (isQueuedBefore  && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector)
     );
+
+    // votes
+    assert hasVotedAfter     != hasVotedBefore     => (!hasVotedBefore                        && votingAll(f));
+    assert votesAgainstAfter != votesAgainstBefore => (votesAgainstAfter > votesAgainstBefore && votingAll(f));
+    assert votesForAfter     != votesForBefore     => (votesForAfter     > votesForBefore     && votingAll(f));
+    assert votesAbstainAfter != votesAbstainBefore => (votesAbstainAfter > votesAbstainBefore && votingAll(f));
 }

certora/specs/GovernorFunctions.spec

@@ -20,11 +20,15 @@ rule propose(uint256 pId, env e) {
     address otherProposer    = proposalProposer(otherId);
 
     address[] targets; uint256[] values; bytes[] calldatas; string descr;
+    require validString(descr);
     require pId == propose@withrevert(e, targets, values, calldatas, descr);
     bool success = !lastReverted;
 
     // liveness & double proposal
-    assert success <=> stateBefore == UNSET();
+    assert success <=> (
+        stateBefore == UNSET() &&
+        validProposal(targets, values, calldatas)
+    );
 
     // effect
     assert success => (

certora/specs/methods/IGovernor.spec

@@ -2,6 +2,8 @@
 methods {
     name()                                            returns string  envfree
     version()                                         returns string  envfree
+    token()                                           returns address envfree
+    timelock()                                        returns address envfree
     clock()                                           returns uint48
     CLOCK_MODE()                                      returns string
     COUNTING_MODE()                                   returns string  envfree
@@ -16,6 +18,9 @@ methods {
     getVotes(address,uint256)                         returns uint256 envfree
     getVotesWithParams(address,uint256,bytes)         returns uint256 envfree
     hasVoted(uint256,address)                         returns bool    envfree
+    quorumNumerator()                                 returns uint256 envfree
+    quorumNumerator(uint256)                          returns uint256 envfree
+    quorumDenominator()                               returns uint256 envfree
 
     propose(address[],uint256[],bytes[],string)                                        returns uint256
     execute(address[],uint256[],bytes[],bytes32)                                       returns uint256
@@ -27,6 +32,7 @@ methods {
     castVoteBySig(uint256,uint8,uint8,bytes32,bytes32)                                 returns uint256
     castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32) returns uint256
     updateQuorumNumerator(uint256)
+    updateTimelock(address)
 
     // harness
     token_getPastTotalSupply(uint256)   returns uint256 envfree