From fd5f309d86c82227ff1623b66d8310b1d67d5d34 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 4 May 2023 16:51:18 +0200 Subject: [PATCH] improve stateTransitionWait --- certora/diff/governance_Governor.sol.patch | 6 +++--- ...extensions_GovernorPreventLateQuorum.sol.patch | 6 +++--- ...e_extensions_GovernorTimelockControl.sol.patch | 14 ++++++++++++-- ...tensions_GovernorVotesQuorumFraction.sol.patch | 8 ++++---- certora/diff/token_ERC721_ERC721.sol.patch | 4 ++-- certora/run.js | 2 +- certora/specs/GovernorStates.spec | 15 +++++++-------- certora/specs/methods/IGovernor.spec | 1 + 8 files changed, 33 insertions(+), 23 deletions(-) diff --git a/certora/diff/governance_Governor.sol.patch b/certora/diff/governance_Governor.sol.patch index 1e9d63215..7bdca832e 100644 --- a/certora/diff/governance_Governor.sol.patch +++ b/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-14 22:09:12.664754077 +0100 -@@ -216,6 +216,21 @@ +--- governance/Governor.sol 2023-05-03 09:17:45.566699712 +0200 ++++ governance/Governor.sol 2023-05-04 15:18:42.667741565 +0200 +@@ -224,6 +224,21 @@ return _proposals[proposalId].proposer; } diff --git a/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch index 05f72f8a9..1d387b376 100644 --- a/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch +++ b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch @@ -1,6 +1,6 @@ ---- governance/extensions/GovernorPreventLateQuorum.sol 2023-03-15 17:13:06.879632860 +0100 -+++ governance/extensions/GovernorPreventLateQuorum.sol 2023-03-15 14:14:59.121060484 +0100 -@@ -84,6 +84,11 @@ +--- governance/extensions/GovernorPreventLateQuorum.sol 2023-05-03 09:17:45.566699712 +0200 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2023-05-04 15:18:42.657742113 +0200 +@@ -82,6 +82,11 @@ return _voteExtension; } diff --git a/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch index f1688e2ab..7213188a6 100644 --- a/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch +++ b/certora/diff/governance_extensions_GovernorTimelockControl.sol.patch @@ -1,5 +1,5 @@ ---- governance/extensions/GovernorTimelockControl.sol 2023-03-14 15:48:49.307543354 +0100 -+++ governance/extensions/GovernorTimelockControl.sol 2023-03-16 16:01:13.857331689 +0100 +--- governance/extensions/GovernorTimelockControl.sol 2023-05-04 11:44:55.587737817 +0200 ++++ governance/extensions/GovernorTimelockControl.sol 2023-05-04 15:18:42.661075263 +0200 @@ -24,7 +24,7 @@ * _Available since v4.3._ */ @@ -21,3 +21,13 @@ /** * @dev Function to queue a proposal to the timelock. */ +@@ -163,4 +168,9 @@ + emit TimelockChange(address(_timelock), address(newTimelock)); + _timelock = newTimelock; + } ++ ++ // FV ++ function timelockId(uint256 proposalId) public view returns (bytes32) { ++ return _timelockIds[proposalId]; ++ } + } diff --git a/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch b/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch index 98d3b25d2..bdf9d1b11 100644 --- a/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch +++ b/certora/diff/governance_extensions_GovernorVotesQuorumFraction.sol.patch @@ -1,7 +1,7 @@ ---- governance/extensions/GovernorVotesQuorumFraction.sol 2023-03-07 10:48:47.733488857 +0100 -+++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-03-15 22:52:06.424537201 +0100 -@@ -62,6 +62,11 @@ - return _quorumNumeratorHistory.upperLookupRecent(timepoint.toUint32()); +--- governance/extensions/GovernorVotesQuorumFraction.sol 2023-05-03 09:17:45.570033048 +0200 ++++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-05-04 15:18:42.664408414 +0200 +@@ -61,6 +61,11 @@ + return _quorumNumeratorHistory.upperLookupRecent(SafeCast.toUint32(timepoint)); } + // FV diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch index c3eae357a..0c53650aa 100644 --- a/certora/diff/token_ERC721_ERC721.sol.patch +++ b/certora/diff/token_ERC721_ERC721.sol.patch @@ -1,5 +1,5 @@ ---- token/ERC721/ERC721.sol 2023-03-07 10:48:47.736822221 +0100 -+++ token/ERC721/ERC721.sol 2023-03-09 19:49:39.669338673 +0100 +--- token/ERC721/ERC721.sol 2023-04-27 22:16:54.864065073 +0200 ++++ token/ERC721/ERC721.sol 2023-05-04 15:18:42.671074716 +0200 @@ -199,6 +199,11 @@ return _owners[tokenId]; } diff --git a/certora/run.js b/certora/run.js index cd4722541..331630500 100755 --- a/certora/run.js +++ b/certora/run.js @@ -59,7 +59,7 @@ if (process.exitCode) { } for (const { spec, contract, files, options = [] } of specs) { - limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]); + limit(runCertora, spec, contract, files, [...options, ...argv.options].flatMap(opt => opt.split(' '))); } // Run certora, aggregate the output and print it at the end diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index 84b43b394..6baba699b 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -57,6 +57,11 @@ rule stateTransitionFn(uint256 pId, env e, method f, calldataarg args) │ Rule: State transitions caused by time passing │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +// The timelockId can be set in states QUEUED, EXECUTED and CANCELED. However, checking the full scope of this results +// in a timeout. This is a weaker version that is still usefull +invariant noTimelockBeforeEndOfVote(env e, uint256 pId) + state(e, pId) == ACTIVE() => timelockId(pId) == 0 + rule stateTransitionWait(uint256 pId, env e1, env e2) { require clockSanity(e1); require clockSanity(e2); @@ -66,6 +71,7 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) { // possible before the time passes. We don't want the state transition include elements that cannot have happened // before e1. This ensure that the e1 → e2 state transition is purelly a consequence of time passing. requireInvariant votesImplySnapshotPassed(e1, pId); + requireInvariant noTimelockBeforeEndOfVote(e1, pId); uint8 stateBefore = state(e1, pId); uint8 stateAfter = state(e2, pId); @@ -74,14 +80,7 @@ rule stateTransitionWait(uint256 pId, env e1, env e2) { (stateBefore == PENDING() && stateAfter == ACTIVE() ) || (stateBefore == PENDING() && stateAfter == DEFEATED() ) || (stateBefore == ACTIVE() && stateAfter == SUCCEEDED()) || - (stateBefore == ACTIVE() && stateAfter == DEFEATED() ) || - // Strange consequence of the timelock binding: - // When transitioning from ACTIVE to SUCCEEDED (because of the clock moving forward) the proposal state in - // the timelock is suddenly considered. Prior state set in the timelock can cause the proposal to already be - // queued, executed or canceled. - (stateBefore == ACTIVE() && stateAfter == CANCELED()) || - (stateBefore == ACTIVE() && stateAfter == EXECUTED()) || - (stateBefore == ACTIVE() && stateAfter == QUEUED()) + (stateBefore == ACTIVE() && stateAfter == DEFEATED() ) ); } diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec index 7737bb23e..25abb6c22 100644 --- a/certora/specs/methods/IGovernor.spec +++ b/certora/specs/methods/IGovernor.spec @@ -52,4 +52,5 @@ methods { getForVotes(uint256) returns uint256 envfree getAbstainVotes(uint256) returns uint256 envfree quorumNumeratorLength() returns uint256 envfree + timelockId(uint256) returns bytes32 envfree }