From 2a0532daccc5e48172d63aa8ce733620d0dae219 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com> Date: Thu, 11 Nov 2021 17:28:22 +0200 Subject: [PATCH] CountingSimpleMoreCleanAndAddedMoreRules --- certora/specs/GovernorBase.spec | 253 +++++++++++++--------- certora/specs/GovernorCountingSimple.spec | 31 +-- 2 files changed, 151 insertions(+), 133 deletions(-) diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 9faa14f9f..ba4565ad0 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -1,6 +1,7 @@ ////////////////////////////////////////////////////////////////////////////// ///////////////////// Governor.sol base definitions ////////////////////////// ////////////////////////////////////////////////////////////////////////////// + methods { proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart proposalDeadline(uint256) returns uint256 envfree @@ -17,131 +18,175 @@ methods { // internal functions made public in harness: _quorumReached(uint256) returns bool envfree _voteSucceeded(uint256) returns bool envfree - } + ////////////////////////////////////////////////////////////////////////////// ////////////////////////////// INVARIANTS //////////////////////////////////// ////////////////////////////////////////////////////////////////////////////// - /* - * A proposal cannot end unless it started. - */ - invariant voteStartBeforeVoteEnd(uint256 pId) - (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) < proposalDeadline(pId)) - && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0) +/* + * A proposal cannot end unless it started. + */ +invariant voteStartBeforeVoteEnd(uint256 pId) + (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) < proposalDeadline(pId)) + && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0) - /* - * A proposal cannot be both executed and canceled. - */ - invariant noBothExecutedAndCanceled(uint256 pId) - !isExecuted(pId) || !isCanceled(pId) +/** + * A proposal cannot be both executed and canceled. + */ +invariant noBothExecutedAndCanceled(uint256 pId) + !isExecuted(pId) || !isCanceled(pId) - /* - * A proposal cannot be neither executed nor canceled before it starts - */ - invariant noExecuteOrCancelBeforeStarting(env e, uint256 pId) - e.block.number < proposalSnapshot(pId) - => !isExecuted(pId) && !isCanceled(pId) +/** + * A proposal could be executed only if quorum was reached and vote succeeded + */ +invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) + isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId) - /* - * A proposal could be executed only if quorum was reached and vote succeeded - */ - invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId) - isExecuted(pId) => _quorumReached(pId) && _voteSucceeded(pId) - - - ////////////////////////////////////////////////////////////////////////////// - /////////////////////////////////// RULES //////////////////////////////////// - ////////////////////////////////////////////////////////////////////////////// +////////////////////////////////////////////////////////////////////////////// +/////////////////////////////////// RULES //////////////////////////////////// +////////////////////////////////////////////////////////////////////////////// - /* - * The voting must start not before the proposal’s creation time - */ - rule noStartBeforeCreation(uint256 pId) { - uint previousStart = proposalSnapshot(pId); - require previousStart == 0; - env e; - calldataarg arg; - propose(e, arg); - uint newStart = proposalSnapshot(pId); - // if created, start is after creation - assert(newStart != 0 => newStart >= e.block.number); - } +/* + * No functions should be allowed to run after a job is deemed as canceled + */ +rule cannotSetIfCanceled(uint256 pId, method f) filtered { f-> !f.isView }{ + require(isCanceled(pId)); + env e; calldataarg args; + f(e, args); + assert(isCanceled(pId) => lastReverted == true, "Function did not revert when canceled"); +} - /* - * Once a proposal is created, voteStart and voteEnd are immutable - */ - rule immutableFieldsAfterProposalCreation(uint256 pId, method f) { - uint _voteStart = proposalSnapshot(pId); - uint _voteEnd = proposalDeadline(pId); - require _voteStart > 0; // proposal was created - - env e; - calldataarg arg; - f(e, arg); - - uint voteStart_ = proposalSnapshot(pId); - uint voteEnd_ = proposalDeadline(pId); - assert _voteStart == voteStart_; - assert _voteEnd == voteEnd_; - } +/* + * No functions should be allowed to run after a job is deemed as executed + */ +rule cannotSetIfExecuted(uint256 pId, method f) filtered { f-> !f.isView }{ + require(isExecuted(pId)); + env e; calldataarg args; + f(e, args); + assert(isExecuted(pId) => lastReverted == true, "Function did not revert after executed"); +} - /* - * A user cannot vote twice - */ - rule doubleVoting(uint256 pId, uint8 sup) { - env e; - address user = e.msg.sender; +/* + * The voting must start not before the proposal’s creation time + */ +rule noStartBeforeCreation(uint256 pId) { + uint previousStart = proposalSnapshot(pId); + require previousStart == 0; + env e; + calldataarg arg; + propose(e, arg); - bool votedCheck = hasVoted(e, pId, user); - require votedCheck == true; - - castVote@withrevert(e, pId, sup); - bool reverted = lastReverted; - - assert votedCheck => reverted, "double voting accured"; - } + uint newStart = proposalSnapshot(pId); + // if created, start is after creation + assert(newStart != 0 => newStart >= e.block.number); +} - /* - * When a proposal is created the start and end date are created in the future. - */ - rule proposalCreatedStartAndEndDateInFuture(address[] targets, uint256[] values, bytes[] calldatas){ - env e; - uint256 pId = callPropose(e, targets, values, calldatas); - uint256 startDate = proposalSnapshot(pId); - uint256 endDate = proposalDeadline(pId); - assert(startDate >= e.block.number && endDate >= e.block.number, "Start or end date were set in the past"); - } +/* + * Once a proposal is created, voteStart and voteEnd are immutable + */ +rule immutableFieldsAfterProposalCreation(uint256 pId, method f) { + uint _voteStart = proposalSnapshot(pId); + uint _voteEnd = proposalDeadline(pId); + require _voteStart > 0; // proposal was created + + env e; + calldataarg arg; + f(e, arg); + + uint voteStart_ = proposalSnapshot(pId); + uint voteEnd_ = proposalDeadline(pId); + assert _voteStart == voteStart_; + assert _voteEnd == voteEnd_; +} - /** - * Check hashProposal hashing is reliable (different inputs lead to different buffers hashed) - */ - /* - rule checkHashProposal { - address[] t1; - address[] t2; - uint256[] v1; - uint256[] v2; - bytes[] c1; - bytes[] c2; - bytes32 d1; - bytes32 d2; +/* + * A user cannot vote twice + */ +rule doubleVoting(uint256 pId, uint8 sup) { + env e; + address user = e.msg.sender; - uint256 h1 = hashProposal(t1,v1,c1,d1); - uint256 h2 = hashProposal(t2,v2,c2,d2); - bool equalHashes = h1 == h2; - assert equalHashes => t1.length == t2.length; - assert equalHashes => v1.length == v2.length; - assert equalHashes => c1.length == c2.length; - assert equalHashes => d1 == d2; - } - */ + bool votedCheck = hasVoted(e, pId, user); + + castVote@withrevert(e, pId, sup); + bool reverted = lastReverted; + + assert votedCheck => reverted, "double voting accured"; +} + + +/* + * When a proposal is created the start and end date are created in the future. + */ +rule proposalCreatedStartAndEndDateInFuture(address[] targets, uint256[] values, bytes[] calldatas){ + env e; + uint256 pId = callPropose(e, targets, values, calldatas); + uint256 startDate = proposalSnapshot(pId); + uint256 endDate = proposalDeadline(pId); + assert(startDate >= e.block.number && endDate >= e.block.number, "Start or end date were set in the past"); +} + + +/** + * Check hashProposal hashing is reliable (different inputs lead to different buffers hashed) + */ +/* +rule checkHashProposal { + address[] t1; + address[] t2; + uint256[] v1; + uint256[] v2; + bytes[] c1; + bytes[] c2; + bytes32 d1; + bytes32 d2; + + uint256 h1 = hashProposal(t1,v1,c1,d1); + uint256 h2 = hashProposal(t2,v2,c2,d2); + bool equalHashes = h1 == h2; + assert equalHashes => t1.length == t2.length; + assert equalHashes => v1.length == v2.length; + assert equalHashes => c1.length == c2.length; + assert equalHashes => d1 == d2; +} +*/ + + +/** + * A proposal cannot be neither executed nor canceled before it starts + */ +rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){ + env e; + + require !isExecuted(pId) && !isCanceled(pId); + + calldataarg arg; + f(e, arg); + + assert e.block.number < proposalSnapshot(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start"; +} + +/** + * A proposal cannot be neither executed nor canceled before proposal's deadline + */ +rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){ + env e; + + requireInvariant voteStartBeforeVoteEnd(pId); + require !isExecuted(pId) && !isCanceled(pId); + + calldataarg arg; + f(e, arg); + + assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start"; +} \ No newline at end of file diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index d3094896f..a0ae7b6d6 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -1,23 +1,6 @@ -////////////////////////////////////////////////////////////////////////////// -///////////////////// Governor.sol base definitions ////////////////////////// -////////////////////////////////////////////////////////////////////////////// +import "GovernorBase.spec" + methods { - proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart - proposalDeadline(uint256) returns uint256 envfree - hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree - isExecuted(uint256) returns bool envfree - isCanceled(uint256) returns bool envfree - // initialized(uint256) returns bool envfree - - hasVoted(uint256, address) returns bool - - castVote(uint256, uint8) returns uint256 - - // internal functions made public in harness: - _quorumReached(uint256) returns bool envfree - _voteSucceeded(uint256) returns bool envfree - - // getter for checking the sums ghost_sum_vote_power_by_id(uint256) returns uint256 envfree } @@ -40,29 +23,19 @@ ghost sum_tracked_weight() returns uint256 { init_state axiom sum_tracked_weight() == 0; } -/* -function update_tracked_weights(uint256 pId, uint256 votes, uint256 old_votes) { - havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; -}*/ - hook Sstore _proposalVotes[KEY uint256 pId].againstVotes uint256 votes (uint256 old_votes) STORAGE { - //update_tracked_weights(pId, votes, old_votes); havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; } hook Sstore _proposalVotes[KEY uint256 pId].forVotes uint256 votes (uint256 old_votes) STORAGE { - //update_tracked_weights(pId, votes, old_votes); havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; } hook Sstore _proposalVotes[KEY uint256 pId].abstainVotes uint256 votes (uint256 old_votes) STORAGE { - //update_tracked_weights(pId, votes, old_votes); havoc tracked_weight assuming forall uint256 p. (p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;