diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol index b87879f80..c2cad2f6d 100644 --- a/certora/harnesses/ERC20VotesHarness.sol +++ b/certora/harnesses/ERC20VotesHarness.sol @@ -19,6 +19,10 @@ contract ERC20VotesHarness is ERC20Votes { _burn(account, amount); } + function unsafeNumCheckpoints(address account) public view returns (uint256) { + return _checkpoints[account].length; + } + function delegateBySig( address delegatee, uint256 nonce, diff --git a/certora/scripts/ERC20VotesRule.sh b/certora/scripts/ERC20VotesRule.sh index 6aac06c6c..64ff6a27d 100644 --- a/certora/scripts/ERC20VotesRule.sh +++ b/certora/scripts/ERC20VotesRule.sh @@ -19,4 +19,5 @@ certoraRun \ --optimistic_loop \ --rule ${rule} \ --msg "${msg}" \ + --staging "Eyal/SanityWithoutCallTrace" \ # --rule_sanity \ \ No newline at end of file diff --git a/certora/scripts/verifyERC20Votes.sh b/certora/scripts/verifyERC20Votes.sh index 7b23e29fe..b3b4e2035 100644 --- a/certora/scripts/verifyERC20Votes.sh +++ b/certora/scripts/verifyERC20Votes.sh @@ -19,4 +19,5 @@ certoraRun \ --solc solc8.2 \ --optimistic_loop \ --loop_iter 4 \ + --staging "Eyal/SanityWithoutCallTrace" \ --msg "${msg}" diff --git a/certora/specs/ERC20Votes.spec b/certora/specs/ERC20Votes.spec index d3c95973d..33bef7384 100644 --- a/certora/specs/ERC20Votes.spec +++ b/certora/specs/ERC20Votes.spec @@ -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,13 +33,17 @@ ghost userVotes(address) returns uint224; // sums the total votes for all users ghost totalVotes() returns mathint { + init_state axiom totalVotes() == 0; axiom totalVotes() >= 0; } +ghost lastIndex(address) returns uint32; + // helper -invariant totalVotes_gte_accounts(address a, address b) - totalVotes() >= getVotes(a) + getVotes(b) +// 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 { @@ -47,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; } @@ -57,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) { @@ -77,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 @@ -90,54 +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 -// this fails, which makes sense because there is no require about the previous fromBlock -invariant unique_checkpoints(address account) - !doubleFromBlock(account) +// 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) -// if an account has been delegated too, then both accounts must have a checkpoint -invariant delegated_implies_checkpoints(address delegator, address delegatee) - delegates(delegator) == delegatee => numCheckpoints(delegator) > 0 && numCheckpoints(delegatee) > 0 -{ preserved with (env e) { + +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; - require balanceOf(e, delegator) > 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 + + 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); - address delegateA = delegates(a); - address delegateB = delegates(b); + uint256 votesA_pre = getVotes(delegates(a)); + uint256 votesB_pre = getVotes(delegates(b)); - uint256 votesA_pre = getVotes(delegateA); - uint256 votesB_pre = getVotes(delegateB); + // 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(delegateA); - uint256 votesB_post = getVotes(delegateB); + 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 delegateA == delegates(a) && delegateB == delegates(b), "delegates changed by transfer"; - assert delegateA != 0 => votesA_pre - votesA_post == amount, "a lost the proper amount of votes"; - assert delegateB != 0 => 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"; } @@ -158,18 +254,22 @@ 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"; @@ -246,6 +346,8 @@ rule delegate_no_frontrunning(method f) { assert other_ == _other, "delegate not contained"; } + + // passes rule mint_increases_totalSupply() {