diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec index 5e44b7fa1..737310fba 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -54,6 +54,13 @@ definition voting(method f) returns bool = f.selector == castVoteWithReason(uint256,uint8,string).selector || f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector; +definition votingBySig(method f) returns bool = + f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector || + f.selector == castVoteWithReasonAndParamsBySig(uint256,uint8,string,bytes,uint8,bytes32,bytes32).selector; + +definition votingAll(method f) returns bool = + voting(f) || votingBySig(f); + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Helper functions │ @@ -79,7 +86,8 @@ function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 } else { - require false; + calldataarg args; + f(e, args); return 0; } } @@ -132,6 +140,7 @@ function helperFunctionsWithRevert(env e, method f, uint256 pId) { } else { - require false; + calldataarg args; + f(e, args); } } diff --git a/certora/specs/GovernorChanges.spec b/certora/specs/GovernorChanges.spec index 2404bbc61..bd3ff681f 100644 --- a/certora/specs/GovernorChanges.spec +++ b/certora/specs/GovernorChanges.spec @@ -22,6 +22,11 @@ rule changes(uint256 pId, env e) { 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 isQueued(pId) != isQueuedBefore => (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector); - assert hasVoted(pId, user) != hasVotedBefore => (!hasVotedBefore && voting(f)); + assert hasVoted(pId, user) != hasVotedBefore => (!hasVotedBefore && votingAll(f)); + + // queue is cleared on cancel + assert isQueued(pId) != isQueuedBefore => ( + (!isQueuedBefore && f.selector == queue(address[],uint256[],bytes[],bytes32).selector) || + (isQueuedBefore && f.selector == cancel(address[],uint256[],bytes[],bytes32).selector) + ); }