|
|
|
|
@ -10,7 +10,7 @@ methods { |
|
|
|
|
getPastTotalSupply(uint256) returns (uint256) |
|
|
|
|
delegate(address) |
|
|
|
|
_delegate(address, address) |
|
|
|
|
delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) |
|
|
|
|
// delegateBySig(address, uint256, uint256, uint8, bytes32, bytes32) |
|
|
|
|
totalSupply() returns (uint256) envfree |
|
|
|
|
_maxSupply() returns (uint224) envfree |
|
|
|
|
|
|
|
|
|
@ -19,6 +19,7 @@ methods { |
|
|
|
|
ckptVotes(address, uint32) returns (uint224) envfree |
|
|
|
|
mint(address, uint256) |
|
|
|
|
burn(address, uint256) |
|
|
|
|
unsafeNumCheckpoints(address) returns (uint256) envfree |
|
|
|
|
|
|
|
|
|
// solidity generated getters |
|
|
|
|
_delegates(address) returns (address) envfree |
|
|
|
|
@ -32,9 +33,17 @@ ghost userVotes(address) returns uint224; |
|
|
|
|
|
|
|
|
|
// sums the total votes for all users |
|
|
|
|
ghost totalVotes() returns mathint { |
|
|
|
|
axiom totalVotes() > 0; |
|
|
|
|
init_state axiom totalVotes() == 0; |
|
|
|
|
axiom totalVotes() >= 0; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
ghost lastIndex(address) returns uint32; |
|
|
|
|
|
|
|
|
|
// helper |
|
|
|
|
|
|
|
|
|
// blocked by tool error |
|
|
|
|
invariant totalVotes_gte_accounts() |
|
|
|
|
forall address a. forall address b. a != b => totalVotes() >= getVotes(a) + getVotes(b) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE { |
|
|
|
|
@ -43,6 +52,9 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 |
|
|
|
|
|
|
|
|
|
havoc totalVotes assuming |
|
|
|
|
totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account)); |
|
|
|
|
|
|
|
|
|
havoc lastIndex assuming |
|
|
|
|
lastIndex@new(account) == index; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -53,12 +65,14 @@ ghost doubleFromBlock(address) returns bool { |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newBlock (uint32 oldBlock) STORAGE { |
|
|
|
|
havoc lastFromBlock assuming |
|
|
|
|
lastFromBlock@new(account) == newBlock; |
|
|
|
|
|
|
|
|
|
havoc doubleFromBlock assuming |
|
|
|
|
doubleFromBlock@new(account) == (newBlock == oldBlock); |
|
|
|
|
doubleFromBlock@new(account) == (newBlock == lastFromBlock(account)); |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
rule sanity(method f) { |
|
|
|
|
@ -73,8 +87,13 @@ invariant sanity_invariant() |
|
|
|
|
totalSupply() >= 0 |
|
|
|
|
|
|
|
|
|
// sum of user balances is >= total amount of delegated votes |
|
|
|
|
// blocked by tool error |
|
|
|
|
invariant votes_solvency() |
|
|
|
|
to_mathint(totalSupply()) >= totalVotes() |
|
|
|
|
{ preserved { |
|
|
|
|
require forall address account. unsafeNumCheckpoints(account) < 4294967295; |
|
|
|
|
requireInvariant totalVotes_gte_accounts(); |
|
|
|
|
}} |
|
|
|
|
|
|
|
|
|
// for some checkpoint, the fromBlock is less than the current block number |
|
|
|
|
// passes but fails rule sanity from hash on delegate by sig |
|
|
|
|
@ -86,41 +105,135 @@ invariant timestamp_constrains_fromBlock(address account, uint32 index, env e) |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
// numCheckpoints are less than maxInt |
|
|
|
|
// passes |
|
|
|
|
invariant maxInt_constrains_numBlocks(address account) |
|
|
|
|
numCheckpoints(account) <= 4294967295 // 2^32 |
|
|
|
|
// TODO add a note about this in the report |
|
|
|
|
// // numCheckpoints are less than maxInt |
|
|
|
|
// // passes because numCheckpoints does a safeCast |
|
|
|
|
// invariant maxInt_constrains_numBlocks(address account) |
|
|
|
|
// numCheckpoints(account) < 4294967295 // 2^32 |
|
|
|
|
|
|
|
|
|
// // fails because there are no checks to stop it |
|
|
|
|
// invariant maxInt_constrains_ckptsLength(address account) |
|
|
|
|
// unsafeNumCheckpoints(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) <= lastFromBlock(account) |
|
|
|
|
numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1) |
|
|
|
|
{ preserved with(env e) { |
|
|
|
|
uint32 pos; |
|
|
|
|
uint32 pos2; |
|
|
|
|
requireInvariant fromBlock_greaterThanEq_pos(account, pos); |
|
|
|
|
requireInvariant fromBlock_increasing(account, pos, pos2); |
|
|
|
|
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) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
invariant no_delegate_no_checkpoints(address account) |
|
|
|
|
delegates(account) == 0x0 => numCheckpoints(account) == 0 |
|
|
|
|
{ preserved delegate(address delegatee) with(env e) { |
|
|
|
|
require delegatee != 0; |
|
|
|
|
} preserved _delegate(address delegator, address delegatee) with(env e) { |
|
|
|
|
require delegatee != 0; |
|
|
|
|
}} |
|
|
|
|
|
|
|
|
|
// 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 |
|
|
|
|
rule unique_checkpoints_rule(method f) { |
|
|
|
|
env e; calldataarg args; |
|
|
|
|
|
|
|
|
|
require e.block.number > 0; // we don't care about this exception |
|
|
|
|
|
|
|
|
|
invariant unique_checkpoints(address account) |
|
|
|
|
!doubleFromBlock(account) |
|
|
|
|
address account; |
|
|
|
|
|
|
|
|
|
require unsafeNumCheckpoints(account) < 4294967295; // 2^32 // we don't want to deal with the checkpoint overflow error here |
|
|
|
|
|
|
|
|
|
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, "same fromBlock, new checkpoint"; |
|
|
|
|
assert doubleFromBlock(account) => num_ckpts_ == _num_ckpts, "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 |
|
|
|
|
rule transfer_safe() { |
|
|
|
|
env e; |
|
|
|
|
uint256 amount; |
|
|
|
|
address a; address b; |
|
|
|
|
require a != b; |
|
|
|
|
require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the sameå |
|
|
|
|
// requireInvariant fromBlock_constrains_numBlocks(a); |
|
|
|
|
// requireInvariant fromBlock_constrains_numBlocks(b); |
|
|
|
|
// requireInvariant totalVotes_gte_accounts(a, b); |
|
|
|
|
|
|
|
|
|
uint256 votesA_pre = getVotes(a); |
|
|
|
|
uint256 votesB_pre = getVotes(b); |
|
|
|
|
uint256 votesA_pre = getVotes(delegates(a)); |
|
|
|
|
uint256 votesB_pre = getVotes(delegates(b)); |
|
|
|
|
|
|
|
|
|
require votesA_pre == erc20votes.balanceOf(e, a); |
|
|
|
|
require votesB_pre == erc20votes.balanceOf(e, b); |
|
|
|
|
// for debugging |
|
|
|
|
uint256 balA_ = balanceOf(e, a); |
|
|
|
|
uint256 balB_ = balanceOf(e, b); |
|
|
|
|
|
|
|
|
|
mathint totalVotes_pre = totalVotes(); |
|
|
|
|
|
|
|
|
|
erc20votes.transferFrom(e, a, b, amount); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
require lastIndex(delegates(a)) < 1000000; |
|
|
|
|
require lastIndex(delegates(b)) < 1000000; |
|
|
|
|
|
|
|
|
|
mathint totalVotes_post = totalVotes(); |
|
|
|
|
uint256 votesA_post = getVotes(a); |
|
|
|
|
uint256 votesB_post = getVotes(b); |
|
|
|
|
uint256 votesA_post = getVotes(delegates(a)); |
|
|
|
|
uint256 votesB_post = getVotes(delegates(b)); |
|
|
|
|
|
|
|
|
|
// for debugging |
|
|
|
|
uint256 _balA = balanceOf(e, a); |
|
|
|
|
uint256 _balB = balanceOf(e, 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 votesA_pre - votesA_post == amount, "a lost the proper amount of votes"; |
|
|
|
|
assert votesB_post - votesB_pre == amount, "b lost the proper amount of votes"; |
|
|
|
|
assert delegates(a) != 0 => votesA_pre - votesA_post == amount, "A lost the wrong amount of votes"; |
|
|
|
|
assert delegates(b) != 0 => votesB_post - votesB_pre == amount, "B lost 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"; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -141,28 +254,35 @@ rule delegator_votes_removed() { |
|
|
|
|
assert post == pre - balance, "delegator retained votes"; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
// delegates increases the delegatee's votes by the proper amount |
|
|
|
|
// passes + rule sanity |
|
|
|
|
rule delegatee_receives_votes() { |
|
|
|
|
env e; |
|
|
|
|
address delegator; address delegatee; |
|
|
|
|
require delegator != delegatee; |
|
|
|
|
|
|
|
|
|
require delegates(delegator) != delegatee; |
|
|
|
|
require delegatee != 0x0; |
|
|
|
|
|
|
|
|
|
uint256 delegator_bal = balanceOf(e, delegator); |
|
|
|
|
uint256 votes_= getVotes(delegatee); |
|
|
|
|
|
|
|
|
|
_delegate(e, delegator, delegatee); |
|
|
|
|
|
|
|
|
|
require lastIndex(delegatee) < 1000000; |
|
|
|
|
|
|
|
|
|
uint256 _votes = getVotes(delegatee); |
|
|
|
|
|
|
|
|
|
assert _votes == votes_ + delegator_bal, "delegatee did not receive votes"; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
rule previous_delegatee_zerod() { |
|
|
|
|
rule previous_delegatee_zeroed() { |
|
|
|
|
env e; |
|
|
|
|
address delegator; address delegatee; address third; |
|
|
|
|
|
|
|
|
|
require delegator != delegatee; |
|
|
|
|
require third != delegatee; |
|
|
|
|
require third != delegator; |
|
|
|
|
require delegates(delegator) == third; |
|
|
|
|
// for third to have been delegated to, it must have a checkpoint |
|
|
|
|
|
|
|
|
|
uint256 delegator_bal = balanceOf(e, delegator); |
|
|
|
|
uint256 votes_ = getVotes(third); |
|
|
|
|
@ -171,16 +291,14 @@ rule previous_delegatee_zerod() { |
|
|
|
|
|
|
|
|
|
uint256 _votes = getVotes(third); |
|
|
|
|
|
|
|
|
|
assert votes_ == votes_ - delegator_bal, "votes not removed from the previous delegatee"; |
|
|
|
|
assert _votes == votes_ - delegator_bal, "votes not removed from the previous delegatee"; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
// passes |
|
|
|
|
// passes with rule sanity |
|
|
|
|
rule delegate_contained() { |
|
|
|
|
env e; |
|
|
|
|
address delegator; address delegatee; address other; |
|
|
|
|
|
|
|
|
|
require delegator != delegatee; |
|
|
|
|
require other != delegator; |
|
|
|
|
require other != delegatee; |
|
|
|
|
require other != delegates(delegator); |
|
|
|
|
|
|
|
|
|
@ -228,6 +346,8 @@ rule delegate_no_frontrunning(method f) { |
|
|
|
|
assert other_ == _other, "delegate not contained"; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// passes |
|
|
|
|
rule mint_increases_totalSupply() { |
|
|
|
|
|
|
|
|
|
|
Aleksander Kryukov
3 years ago