@ -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";
}
Aleksander Kryukov
3 years ago