You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
276 lines
9.4 KiB
276 lines
9.4 KiB
using Checkpoints as Checkpoints
|
|
|
|
methods {
|
|
// functions
|
|
checkpoints(address, uint32) envfree
|
|
numCheckpoints(address) returns (uint32) envfree
|
|
getVotes(address) returns (uint256) envfree
|
|
getPastVotes(address, uint256) returns (uint256)
|
|
getPastTotalSupply(uint256) returns (uint256)
|
|
delegates(address) returns (address) envfree
|
|
delegate(address)
|
|
_delegate(address, address)
|
|
delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32)
|
|
nonces(address) returns (uint256)
|
|
totalSupply() returns (uint256) envfree
|
|
_maxSupply() returns (uint224) envfree
|
|
|
|
// harnesss functions
|
|
ckptFromBlock(address, uint32) returns (uint32) envfree
|
|
ckptVotes(address, uint32) returns (uint224) envfree
|
|
mint(address, uint256)
|
|
burn(uint256)
|
|
unsafeNumCheckpoints(address) returns (uint256) envfree
|
|
|
|
// solidity generated getters
|
|
_delegation(address) returns (address) envfree
|
|
|
|
// external functions
|
|
|
|
|
|
}
|
|
|
|
// gets the most recent votes for a user
|
|
ghost userVotes(address) returns uint224{
|
|
init_state axiom forall address a. userVotes(a) == 0;
|
|
}
|
|
|
|
// sums the total votes for all users
|
|
ghost totalVotes() returns mathint {
|
|
init_state axiom totalVotes() == 0;
|
|
axiom totalVotes() >= 0;
|
|
}
|
|
|
|
hook Sstore _checkpoints[KEY address account].votes uint224 newVotes (uint224 oldVotes) STORAGE {
|
|
havoc userVotes assuming
|
|
userVotes@new(account) == newVotes;
|
|
|
|
havoc totalVotes assuming
|
|
totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account));
|
|
}
|
|
|
|
|
|
ghost lastFromBlock(address) returns uint32;
|
|
|
|
ghost doubleFromBlock(address) returns bool {
|
|
init_state axiom forall address a. doubleFromBlock(a) == false;
|
|
}
|
|
|
|
|
|
|
|
|
|
hook Sstore _checkpoints[KEY address account].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE {
|
|
havoc lastFromBlock assuming
|
|
lastFromBlock@new(account) == newBlock;
|
|
|
|
havoc doubleFromBlock assuming
|
|
doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
|
|
}
|
|
|
|
// sum of user balances is >= total amount of delegated votes
|
|
// blocked by tool error
|
|
invariant votes_solvency()
|
|
to_mathint(totalSupply()) >= totalVotes()
|
|
{ preserved with(env e) {
|
|
require forall address account. numCheckpoints(account) < 1000000;
|
|
} }
|
|
|
|
|
|
// for some checkpoint, the fromBlock is less than the current block number
|
|
// passes but fails rule sanity from hash on delegate by sig
|
|
invariant timestamp_constrains_fromBlock(address account, uint32 index, env e)
|
|
ckptFromBlock(account, index) < e.block.number
|
|
{
|
|
preserved {
|
|
require index < numCheckpoints(account);
|
|
}
|
|
}
|
|
|
|
// numCheckpoints are less than maxInt
|
|
// passes because numCheckpoints does a safeCast
|
|
// invariant maxInt_constrains_numBlocks(address account)
|
|
// numCheckpoints(account) < 4294967295 // 2^32
|
|
|
|
// can't have more checkpoints for a given account than the last from block
|
|
// passes
|
|
invariant fromBlock_constrains_numBlocks(address account)
|
|
numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1)
|
|
{ preserved with(env e) {
|
|
require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
|
|
}}
|
|
|
|
// for any given checkpoint, the fromBlock must be greater than the checkpoint
|
|
// this proves the above invariant in combination with the below invariant
|
|
// if checkpoint has a greater fromBlock than the last, and the FromBlock is always greater than the pos.
|
|
// Then the number of positions must be less than the currentFromBlock
|
|
// ^note that the tool is assuming it's possible for the starting fromBlock to be 0 or anything, and does not know the current starting block
|
|
// passes + rule sanity
|
|
invariant fromBlock_greaterThanEq_pos(address account, uint32 pos)
|
|
ckptFromBlock(account, pos) >= pos
|
|
|
|
// a larger index must have a larger fromBlock
|
|
// passes + rule sanity
|
|
invariant fromBlock_increasing(address account, uint32 pos, uint32 pos2)
|
|
pos > pos2 => ckptFromBlock(account, pos) > ckptFromBlock(account, pos2)
|
|
|
|
|
|
// converted from an invariant to a rule to slightly change the logic
|
|
// if the fromBlock is the same as before, then the number of checkpoints stays the same
|
|
// however if the fromBlock is new than the number of checkpoints increases
|
|
// passes, fails rule sanity because tautology check seems to be bugged
|
|
rule unique_checkpoints_rule(method f) {
|
|
env e; calldataarg args;
|
|
address account;
|
|
uint32 num_ckpts_ = numCheckpoints(account);
|
|
uint32 fromBlock_ = num_ckpts_ == 0 ? 0 : ckptFromBlock(account, num_ckpts_ - 1);
|
|
|
|
f(e, args);
|
|
|
|
uint32 _num_ckpts = numCheckpoints(account);
|
|
uint32 _fromBlock = _num_ckpts == 0 ? 0 : ckptFromBlock(account, _num_ckpts - 1);
|
|
|
|
|
|
assert fromBlock_ == _fromBlock => num_ckpts_ == _num_ckpts || _num_ckpts == 1, "same fromBlock, new checkpoint";
|
|
// this assert fails consistently
|
|
// assert !doubleFromBlock(account) => ckpts_ != _ckpts, "new fromBlock but total checkpoints not being increased";
|
|
}
|
|
|
|
// assumes neither account has delegated
|
|
// currently fails due to this scenario. A has maxint number of checkpoints
|
|
// an additional checkpoint is added which overflows and sets A's votes to 0
|
|
// passes + rule sanity (- a bad tautology check)
|
|
rule transfer_safe() {
|
|
env e;
|
|
uint256 ID;
|
|
address a; address b;
|
|
|
|
require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same
|
|
require numCheckpoints(delegates(a)) < 1000000;
|
|
require numCheckpoints(delegates(b)) < 1000000;
|
|
|
|
uint256 votesA_pre = getVotes(delegates(a));
|
|
uint256 votesB_pre = getVotes(delegates(b));
|
|
|
|
mathint totalVotes_pre = totalVotes();
|
|
|
|
transferFrom(e, a, b, ID);
|
|
|
|
mathint totalVotes_post = totalVotes();
|
|
uint256 votesA_post = getVotes(delegates(a));
|
|
uint256 votesB_post = getVotes(delegates(b));
|
|
|
|
// if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes
|
|
assert totalVotes_pre == totalVotes_post, "transfer changed total supply";
|
|
assert delegates(a) != 0 => votesA_pre - 1 == votesA_post, "A lost the wrong amount of votes";
|
|
assert delegates(b) != 0 => votesB_pre + 1 == votesB_post, "B gained the wrong amount of votes";
|
|
}
|
|
|
|
// for any given function f, if the delegate is changed the function must be delegate or delegateBySig
|
|
// passes
|
|
rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).selector &&
|
|
f.selector != _delegate(address, address).selector &&
|
|
f.selector != delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32).selector) }
|
|
{
|
|
env e; calldataarg args;
|
|
address account;
|
|
address pre = delegates(account);
|
|
|
|
f(e, args);
|
|
|
|
address post = delegates(account);
|
|
|
|
assert pre == post, "invalid delegate change";
|
|
}
|
|
|
|
// delegates increases the delegatee's votes by the proper amount
|
|
// passes + rule sanity
|
|
rule delegatee_receives_votes() {
|
|
env e;
|
|
address delegator; address delegatee;
|
|
|
|
require numCheckpoints(delegatee) < 1000000;
|
|
require delegates(delegator) != delegatee;
|
|
require delegatee != 0x0;
|
|
|
|
|
|
uint256 delegator_bal = balanceOf(e, delegator);
|
|
uint256 votes_= getVotes(delegatee);
|
|
|
|
_delegate(e, delegator, delegatee);
|
|
|
|
uint256 _votes = getVotes(delegatee);
|
|
assert _votes == votes_ + delegator_bal, "delegatee did not receive votes";
|
|
}
|
|
|
|
// passes + rule sanity
|
|
rule previous_delegatee_votes_removed() {
|
|
env e;
|
|
address delegator; address delegatee; address third;
|
|
|
|
require third != delegatee;
|
|
require delegates(delegator) == third;
|
|
require numCheckpoints(third) < 1000000;
|
|
|
|
uint256 delegator_bal = balanceOf(e, delegator);
|
|
uint256 votes_ = getVotes(third);
|
|
|
|
_delegate(e, delegator, delegatee);
|
|
|
|
uint256 _votes = getVotes(third);
|
|
|
|
assert third != 0x0 => _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee";
|
|
}
|
|
|
|
// passes with rule sanity
|
|
rule delegate_contained() {
|
|
env e;
|
|
address delegator; address delegatee; address other;
|
|
|
|
require other != delegatee;
|
|
require other != delegates(delegator);
|
|
|
|
uint256 votes_ = getVotes(other);
|
|
|
|
_delegate(e, delegator, delegatee);
|
|
|
|
uint256 _votes = getVotes(other);
|
|
|
|
assert votes_ == _votes, "votes not contained";
|
|
}
|
|
|
|
rule delegate_no_frontrunning(method f) {
|
|
env e; calldataarg args;
|
|
address delegator; address delegatee; address third; address other;
|
|
|
|
|
|
|
|
require numCheckpoints(delegatee) < 1000000;
|
|
require numCheckpoints(third) < 1000000;
|
|
|
|
|
|
f(e, args);
|
|
|
|
uint256 delegator_bal = balanceOf(e, delegator);
|
|
uint256 delegatee_votes_ = getVotes(delegatee);
|
|
uint256 third_votes_ = getVotes(third);
|
|
uint256 other_votes_ = getVotes(other);
|
|
require delegates(delegator) == third;
|
|
require third != delegatee;
|
|
require other != third;
|
|
require other != delegatee;
|
|
require delegatee != 0x0;
|
|
|
|
_delegate(e, delegator, delegatee);
|
|
|
|
uint256 _delegatee_votes = getVotes(delegatee);
|
|
uint256 _third_votes = getVotes(third);
|
|
uint256 _other_votes = getVotes(other);
|
|
|
|
|
|
// previous delegatee loses all of their votes
|
|
// delegatee gains that many votes
|
|
// third loses any votes delegated to them
|
|
assert _delegatee_votes == delegatee_votes_ + delegator_bal, "delegatee did not receive votes";
|
|
assert third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third";
|
|
assert other_votes_ == _other_votes, "delegate not contained";
|
|
} |