From 92f5f0dfbb42363c5b156183ca39ea818f3ac022 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 19 Nov 2021 20:13:06 +0200 Subject: [PATCH] TryingToFixRules --- certora/harnesses/GovernorBasicHarness.sol | 4 -- certora/harnesses/WizardHarness1.sol | 4 ++ certora/specs/GovernorBase.spec | 23 ++++++-- certora/specs/GovernorCountingSimple.spec | 68 +++++++++------------- 4 files changed, 49 insertions(+), 50 deletions(-) diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/GovernorBasicHarness.sol index f93855929..f63aaa161 100644 --- a/certora/harnesses/GovernorBasicHarness.sol +++ b/certora/harnesses/GovernorBasicHarness.sol @@ -43,10 +43,6 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes return _votingPeriod; } - function snapshot(uint256 proposalId) public view returns (uint64) { - return _proposals[proposalId].voteStart._deadline; - } - mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; function _castVote( diff --git a/certora/harnesses/WizardHarness1.sol b/certora/harnesses/WizardHarness1.sol index 0407efc79..8cbdf92c6 100644 --- a/certora/harnesses/WizardHarness1.sol +++ b/certora/harnesses/WizardHarness1.sol @@ -76,6 +76,10 @@ contract WizardHarness1 is Governor, GovernorProposalThreshold, GovernorCounting return super.castVoteWithReason(proposalId, support, reason); } + function getExecutor() public returns (address){ + return _executor(); + } + // original code function votingDelay() public view override returns (uint256) { // HARNESS: pure -> view diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index ad0626b5c..18863c4dc 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -2,6 +2,8 @@ ///////////////////// Governor.sol base definitions ////////////////////////// ////////////////////////////////////////////////////////////////////////////// +using ERC20VotesHarness as erc20votes + methods { proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd @@ -28,10 +30,10 @@ methods { getVotes(address, uint256) returns uint256 => DISPATCHER(true) //getVotes(address, uint256) => DISPATCHER(true) - getPastTotalSupply(uint256) returns uint256 envfree => DISPATCHER(true) + erc20votes.getPastTotalSupply(uint256) returns uint256 //getPastTotalSupply(uint256) => DISPATCHER(true) - getPastVotes(address, uint256) returns uint256 envfree => DISPATCHER(true) + erc20votes.getPastVotes(address, uint256) returns uint256 } ////////////////////////////////////////////////////////////////////////////// @@ -105,7 +107,7 @@ invariant proposalInitiated(uint256 pId) * A proposal cannot end unless it started. */ invariant voteStartBeforeVoteEnd(uint256 pId) - (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) < proposalDeadline(pId)) + (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) // from < to <= because snapshot and deadline can be the same block number if delays are set to 0 && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0) @@ -119,9 +121,20 @@ invariant noBothExecutedAndCanceled(uint256 pId) /** * A proposal could be executed only if quorum was reached and vote succeeded */ -invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e) - isExecuted(pId) => _quorumReached(e, pId) && _voteSucceeded(pId) +//invariant executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e) +// isExecuted(pId) => _quorumReached(e, pId) && _voteSucceeded(pId) +rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){ + + bool isExecutedBefore = isExecuted(pId); + + calldataarg args; + f(e, args); + + bool isExecutedAfter = isExecuted(pId); + + assert isExecutedBefore != isExecutedAfter => _quorumReached(e, pId) && _voteSucceeded(pId), "quorum was changed"; +} /////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////// In-State Rules ///////////////////////////////////// diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index 949cdc876..89fb1e719 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -6,15 +6,18 @@ methods { ghost_sum_vote_power_by_id(uint256) returns uint256 envfree // castVote(uint256, uint8) returns uint256 // castVoteBySig(uint256,uint8,uint8,bytes32,bytes32) returns uint256 - - snapshot(uint256) returns uint64 envfree + quorum(uint256) returns uint256 proposalVotes(uint256) returns (uint256, uint256, uint256) envfree quorumNumerator() returns uint256 _executor() returns address - erc20votes._getPastVotes(address, uint256) returns uint256 envfree + erc20votes._getPastVotes(address, uint256) returns uint256 + + getExecutor() returns address + + //0xe38335e5 => DISPATCHER(true) } ////////////////////////////////////////////////////////////////////////////// @@ -90,9 +93,17 @@ hook Sstore erc20votes._getPastVotes[KEY address uId][KEY uint256 blockNumber] u && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn)); } -invariant checkGetVotesGhost(address uId, uint256 blockNumber) - erc20votes._getPastVotes(uId, blockNumber) == getPastVotes(uId, blockNumber) +invariant checkGetVotesGhost(address uId, uint256 blockNumber, env e) + erc20votes._getPastVotes(e, uId, blockNumber) == erc20votes.getPastVotes(e, uId, blockNumber) +rule whatCahnges(uint256 blockNumber, method f) { + env e; + calldataarg args; + uint256 ghostBefore = totalVotesPossible(blockNumber); + f(e,args); + uint256 ghostAfter = totalVotesPossible(blockNumber); + assert ghostAfter == ghostBefore, "ghost was changed"; +} ////////////////////////////////////////////////////////////////////////////// ////////////////////////////// INVARIANTS //////////////////////////////////// @@ -122,8 +133,11 @@ invariant OneIsNotMoreThanAll(uint256 pId) /* * totalVotesPossible >= votePower(id) */ -invariant possibleTotalVotes(uint256 pId) - tracked_weight(pId) <= totalVotesPossible(snapshot(pId)) +invariant possibleTotalVotes(uint256 pId, env e) + tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)) + +invariant voteGettersCheck(uint256 pId, address acc, env e) + erc20votes.getPastVotes(e, acc, proposalSnapshot(pId)) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)) /* * totalVotesPossible >= votePower(id) @@ -178,7 +192,7 @@ rule noVoteForSomeoneElse(uint256 pId, uint8 support){ assert(hasVotedBefore != hasVotedAfter => (forall address user. user != voter => !hasVoted(e, pId, user))); } -// ok + rule votingWeightMonotonicity(method f){ uint256 votingWeightBefore = sum_tracked_weight(); @@ -191,22 +205,6 @@ rule votingWeightMonotonicity(method f){ assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow"; } -// ok with this branch: thomas/bool-hook-values -// can't use link because contracts are abstract, they don't have bytecode/constructor -// add implementation harness -rule quorumMonotonicity(method f, uint256 blockNumber){ - env e; - - uint256 quorumBefore = quorum(e, blockNumber); - - calldataarg args; - f(e, args); - - uint256 quorumAfter = quorum(e, blockNumber); - - assert quorumBefore <= quorumAfter, "Quorum was decreased somehow"; -} - function callFunctionWithParams(method f, uint256 proposalId, env e) { address[] targets; @@ -233,18 +231,8 @@ function callFunctionWithParams(method f, uint256 proposalId, env e) { } } - -// getVotes() returns different results. -// how to ensure that the same acc is used in getVotes() in uint256 votesBefore = getVotes(acc, bn);/uint256 votesAfter = getVotes(acc, bn); and in callFunctionWithParams -// votesBefore and votesAfter give different results but shoudn't - -// are we assuming that a person with 0 votes can vote? are we assuming that a person may have 0 votes -// it seems like a weight can be 0. At least there is no check for it -// If it can be 0 then < should be changed to <= but it gives less coverage - // run on ALex's branch to avoid tiomeouts: --staging alex/external-timeout-for-solvers // --staging shelly/forSasha -// implement ERC20Votes as a harness rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f -> f.selector != 0x7d5e81e2}{ uint256 againstBefore = votesAgainst(); uint256 forBefore = votesFor(); @@ -276,21 +264,19 @@ rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f - /* * Check privileged operations */ -// NO NEED FOR SPECIFIC CHANGES -// how to check executor()? -// to make it public instead of internal is not best idea, I think. -// currentContract gives a violation in -// maybe need harness implementation for one of the contracts -rule privilegedOnly(method f){ +rule privilegedOnly(method f, uint256 newQuorumNumerator){ env e; calldataarg arg; uint256 quorumNumBefore = quorumNumerator(e); + //require e.msg.sender == currentContract; f(e, arg); + //updateQuorumNumerator(e, newQuorumNumerator); + uint256 quorumNumAfter = quorumNumerator(e); - address executorCheck = currentContract; + address executorCheck = getExecutor(e); // address executorCheck = _executor(e); assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non priveleged user changed quorum numerator";