diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/GovernorBasicHarness.sol index db3f0818b..02846a137 100644 --- a/certora/harnesses/GovernorBasicHarness.sol +++ b/certora/harnesses/GovernorBasicHarness.sol @@ -59,6 +59,12 @@ contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes return deltaWeight; } + function callPropose(address[] memory targets, + uint256[] memory values, + bytes[] memory calldatas) public virtual returns (uint256) { + return super.propose(targets, values, calldatas, ""); + } + /* mapping (address => mapping (uint256 => uint256)) _getVotes; diff --git a/certora/scripts/GovernorBasic.sh b/certora/scripts/GovernorBasic.sh index 8a6b48373..7b3db7077 100644 --- a/certora/scripts/GovernorBasic.sh +++ b/certora/scripts/GovernorBasic.sh @@ -1,9 +1,8 @@ certoraRun certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \ - --solc solc8.2 \ - --staging uri/add_with_env_to_preserved_all \ + --solc solc8.0 \ + ---staging shelly/stringCVL \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --disableLocalTypeChecking \ - --rule proposalInitiated \ + --rule unaffectedThreshhold \ --msg "$1" \ No newline at end of file diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh index 26df57c7b..6413e5694 100644 --- a/certora/scripts/GovernorCountingSimple-counting.sh +++ b/certora/scripts/GovernorCountingSimple-counting.sh @@ -1,7 +1,7 @@ certoraRun certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ - --staging \ + --staging alex/external-timeout-for-solvers \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ --rule hasVotedCorrelation \ diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index f9814cfa7..35ecac5a4 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -21,6 +21,7 @@ methods { // function summarization hashProposal(address[], uint256[], bytes[], bytes32) => CONSTANT + proposalThreshold() returns uint256 envfree } ////////////////////////////////////////////////////////////////////////////// @@ -292,3 +293,19 @@ rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] c bool executedAfter = isExecuted(pId); assert(executedAfter != executedBefore, "executed property did not change"); } + + +/* +* User should not be able to affect proposal threshold +*/ +rule unaffectedThreshhold(method f){ + uint256 thresholdBefore = proposalThreshold(); + + env e; + calldataarg args; + f(e, args); + + uint256 thresholdAfter = proposalThreshold(); + + assert thresholdBefore == thresholdAfter, "threshold was changed"; +} diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec index a73edaa67..e2fc1fdf9 100644 --- a/certora/specs/GovernorCountingSimple.spec +++ b/certora/specs/GovernorCountingSimple.spec @@ -9,8 +9,17 @@ methods { quorum(uint256) returns uint256 envfree proposalVotes(uint256) returns (uint256, uint256, uint256) envfree - getVotes(address, uint256) returns uint256 envfree - //getVotes(address, uint256) => CONSTANT + quorumNumerator() returns uint256 + updateQuorumNumerator(uint256) + _executor() returns address + + getVotes(address, uint256) returns uint256 envfree => DISPATCHER(true) + //getVotes(address, uint256) => DISPATCHER(true) + + getPastTotalSupply(uint256) returns uint256 envfree => DISPATCHER(true) + //getPastTotalSupply(uint256) => DISPATCHER(true) + + getPastVotes(address, uint256) returns uint256 envfree => DISPATCHER(true) } ////////////////////////////////////////////////////////////////////////////// @@ -21,18 +30,18 @@ ghost hasVoteGhost(uint256) returns uint256 { init_state axiom forall uint256 pId. hasVoteGhost(pId) == 0; } -hook Sstore _proposalVotes[KEY uint256 pId].hasVoted[KEY address user] bool current_voting_State (bool old_voting_state) STORAGE{ - havoc hasVoteGhost assuming forall uint256 p. ((p == pId && current_voting_State && !old_voting_state) ? (hasVoteGhost@new(p) == hasVoteGhost@old(p) + 1) : - (hasVoteGhost@new(p) == hasVoteGhost@old(p))); -} +//hook Sstore _proposalVotes[KEY uint256 pId].hasVoted[KEY address user] bool current_voting_State (bool old_voting_state) STORAGE{ +// havoc hasVoteGhost assuming forall uint256 p. ((p == pId && current_voting_State && !old_voting_state) ? (hasVoteGhost@new(p) == hasVoteGhost@old(p) + 1) : +// (hasVoteGhost@new(p) == hasVoteGhost@old(p))); +//} ghost sum_all_votes_power() returns uint256 { init_state axiom sum_all_votes_power() == 0; } -hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE { - havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power; -} +//hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE { +// havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power; +//} ghost tracked_weight(uint256) returns uint256 { init_state axiom forall uint256 p. tracked_weight(p) == 0; @@ -74,30 +83,20 @@ hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes; } -/* + ghost totalVotesPossible(uint256) returns uint256 { init_state axiom forall uint256 bn. totalVotesPossible(bn) == 0; } -ghost possibleMaxOfVoters(uint256) returns uint256{ - init_state axiom forall uint256 pId. possibleMaxOfVoters(pId) == 0; -} +// Was done with _getVotes by mistake. Should check GovernorBasicHarness but _getVotes is from GovernorHarness +//hook Sstore _getVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE { +// havoc totalVotesPossible assuming forall uint256 bn. +// (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight) +// && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn)); +// +//} + -hook Sstore _getVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE { - havoc totalVotesPossible assuming forall uint256 bn. - (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight) - && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn)); - //somehow havoc possibleMaxOfVoters based on scheme. Probably can be implemented if previous havoc is possible -} -*/ -/* -_proposalVotes[pId].hasVoted[account] -> bool - ^ - | - go through all accounts, - if true => -possibleMaxOfVoters(pId) += getVotes(pId, acount); -*/ ////////////////////////////////////////////////////////////////////////////// ////////////////////////////// INVARIANTS //////////////////////////////////// @@ -174,7 +173,7 @@ rule noVoteForSomeoneElse(uint256 pId, uint8 support){ } */ -//ok +// ok rule votingWeightMonotonicity(method f){ uint256 votingWeightBefore = sum_tracked_weight(); @@ -187,8 +186,9 @@ rule votingWeightMonotonicity(method f){ assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow"; } -// timeouts and strange violations -// https://vaas-stg.certora.com/output/3106/23f63c84c58b06285f4f/?anonymousKey=e5a7dc2e0ce7829cf5af8eb29a4ba231d915704c +// 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){ uint256 quorumBefore = quorum(blockNumber); @@ -201,30 +201,90 @@ rule quorumMonotonicity(method f, uint256 blockNumber){ assert quorumBefore <= quorumAfter, "Quorum was decreased somehow"; } + +function callFunctionWithParams(method f, uint256 proposalId, env e) { + address[] targets; + uint256[] values; + bytes[] calldatas; + bytes32 descriptionHash; + uint8 support; + uint8 v; bytes32 r; bytes32 s; + if (f.selector == callPropose(address[], uint256[], bytes[]).selector) { + uint256 result = callPropose(e, targets, values, calldatas); + require result == proposalId; + } else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) { + uint256 result = execute(e, targets, values, calldatas, descriptionHash); + require result == proposalId; + } else if (f.selector == castVote(uint256, uint8).selector) { + castVote(e, proposalId, support); + //} else if (f.selector == castVoteWithReason(uint256, uint8, string).selector) { + // castVoteWithReason(e, proposalId, support, reason); + } else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) { + castVoteBySig(e, proposalId, support, v, r, s); + } else { + calldataarg args; + f(e,args); + } +} + + // 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 -rule hasVotedCorrelation(uint256 pId, method f, address acc, env e){ + +// 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(); uint256 abstainBefore = votesAbstain(); //againstBefore, forBefore, abstainBefore = proposalVotes(pId); + address acc = e.msg.sender; + bool hasVotedBefore = hasVoted(e, pId, acc); - uint256 votesBefore = getVotes(acc, pId); + uint256 votesBefore = getVotes(acc, bn); require votesBefore > 0; - calldataarg args; - f(e, args); + //calldataarg args; + //f(e, args); + callFunctionWithParams(f, pId, e); uint256 againstAfter = votesAgainst(); uint256 forAfter = votesFor(); uint256 abstainAfter = votesAbstain(); //againstAfter, forAfter, abstainAfter = proposalVotes(pId); - uint256 votesAfter = getVotes(acc, pId); + uint256 votesAfter = getVotes(acc, bn); bool hasVotedAfter = hasVoted(e, pId, acc); assert hasVotedBefore != hasVotedAfter => againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter, "no correlation"; +} + + +/* +* 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 +rule privilegedOnly(method f){ + env e; + calldataarg arg; + uint256 quorumNumBefore = quorumNumerator(e); + + f(e, arg); + + uint256 quorumNumAfter = quorumNumerator(e); + + address executorCheck = currentContract; + // address executorCheck = _executor(e); + + assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non priveleged user changed quorum numerator"; } \ No newline at end of file