From 5ef4d207a61313b8d1e64b98a17070b947ee2320 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 16 Mar 2023 17:49:21 +0100 Subject: [PATCH] more fixes ? --- certora/harnesses/GovernorHarness.sol | 2 +- .../harnesses/GovernorPreventLateHarness.sol | 2 +- certora/specs/GovernorFunctions.spec | 49 +++---------------- certora/specs/GovernorInvariants.spec | 19 +++++-- 4 files changed, 25 insertions(+), 47 deletions(-) diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol index d3494d66b..a6b1a2738 100644 --- a/certora/harnesses/GovernorHarness.sol +++ b/certora/harnesses/GovernorHarness.sol @@ -40,7 +40,7 @@ contract GovernorHarness is } // Harness from Governor - function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public returns (uint256) { + function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public pure returns (uint256) { return hashProposal(targets, values, calldatas, keccak256(bytes(description))); } diff --git a/certora/harnesses/GovernorPreventLateHarness.sol b/certora/harnesses/GovernorPreventLateHarness.sol index a4b1ca3f7..dc306d63e 100644 --- a/certora/harnesses/GovernorPreventLateHarness.sol +++ b/certora/harnesses/GovernorPreventLateHarness.sol @@ -43,7 +43,7 @@ contract GovernorPreventLateHarness is } // Harness from Governor - function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public returns (uint256) { + function hashProposal(address[] memory targets,uint256[] memory values,bytes[] memory calldatas,string memory description) public pure returns (uint256) { return hashProposal(targets, values, calldatas, keccak256(bytes(description))); } diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec index 016c12360..b5e6d561c 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -1,6 +1,8 @@ import "helpers.spec" import "Governor.helpers.spec" +use invariant queuedImplySuccess + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rule: propose effect and liveness. Includes "no double proposition" │ @@ -26,9 +28,6 @@ rule propose_liveness(uint256 pId, env e) { } rule propose_effect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - address[] targets; uint256[] values; bytes[] calldatas; string descr; require pId == hashProposal(targets, values, calldatas, descr); @@ -41,12 +40,7 @@ rule propose_effect(uint256 pId, env e) { assert proposalDeadline(pId) == clock(e) + votingDelay() + votingPeriod(); } -rule propose_sideeffect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - - uint256 otherId; - +rule propose_sideeffect(uint256 pId, env e, uint256 otherId) { uint8 otherStateBefore = state(e, otherId); uint256 otherVoteStart = proposalSnapshot(otherId); uint256 otherVoteEnd = proposalDeadline(otherId); @@ -99,9 +93,6 @@ rule castVote_liveness(uint256 pId, env e, method f) rule castVote_effect(uint256 pId, env e, method f) filtered { f -> voting(f) } { - require nonpayable(e); - require clockSanity(e); - uint8 support; address voter; @@ -124,9 +115,6 @@ rule castVote_effect(uint256 pId, env e, method f) rule castVote_sideeffect(uint256 pId, env e, method f) filtered { f -> voting(f) } { - require nonpayable(e); - require clockSanity(e); - uint8 support; address voter; address otherVoter; @@ -168,9 +156,6 @@ rule queue_liveness(uint256 pId, env e) { } rule queue_effect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - uint8 stateBefore = state(e, pId); bool queuedBefore = isQueued(pId); @@ -184,12 +169,7 @@ rule queue_effect(uint256 pId, env e) { assert !queuedBefore; } -rule queue_sideeffect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - - uint256 otherId; - +rule queue_sideeffect(uint256 pId, env e, uint256 otherId) { uint8 otherStateBefore = state(e, otherId); bool otherQueuedBefore = isQueued(otherId); @@ -224,9 +204,6 @@ rule execute_liveness(uint256 pId, env e) { } rule execute_effect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; require pId == hashProposal(targets, values, calldatas, descrHash); @@ -236,12 +213,7 @@ rule execute_effect(uint256 pId, env e) { assert state(e, pId) == EXECUTED(); } -rule execute_sideeffect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - - uint256 otherId; - +rule execute_sideeffect(uint256 pId, env e, uint256 otherId) { uint8 otherStateBefore = state(e, otherId); address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; @@ -261,6 +233,7 @@ rule execute_sideeffect(uint256 pId, env e) { rule cancel_liveness(uint256 pId, env e) { require nonpayable(e); require clockSanity(e); + requireInvariant queuedImplySuccess(pId); uint8 stateBefore = state(e, pId); @@ -277,9 +250,6 @@ rule cancel_liveness(uint256 pId, env e) { } rule cancel_effect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - address[] targets; uint256[] values; bytes[] calldatas; bytes32 descrHash; require pId == hashProposal(targets, values, calldatas, descrHash); @@ -290,12 +260,7 @@ rule cancel_effect(uint256 pId, env e) { assert !isQueued(pId); // cancel resets timelockId } -rule cancel_sideeffect(uint256 pId, env e) { - require nonpayable(e); - require clockSanity(e); - - uint256 otherId; - +rule cancel_sideeffect(uint256 pId, env e, uint256 otherId) { uint8 otherStateBefore = state(e, otherId); bool otherQueuedBefore = isQueued(otherId); diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec index 9be77e244..7bbb5bf8b 100644 --- a/certora/specs/GovernorInvariants.spec +++ b/certora/specs/GovernorInvariants.spec @@ -40,9 +40,9 @@ invariant proposalStateConsistency(uint256 pId) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant votesImplySnapshotPassed(env e, uint256 pId) - getAgainstVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e) && - getForVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e) && - getAbstainVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e) + (getAgainstVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e)) && + (getForVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e)) && + (getAbstainVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e)) { preserved { require clockSanity(e); @@ -91,6 +91,19 @@ invariant queuedImplyCreated(uint pId) } } +invariant queuedImplyVoteOverAndSuccessful(env e, uint pId) + isQueued(pId) => ( + quorumReached(pId) && + voteSucceeded(pId) && + proposalDeadline(pId) < clock(e) + ) + { + preserved { + require clockSanity(e); + requireInvariant proposalStateConsistency(pId); + } + } + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: Votes start before it ends │