diff --git a/certora/specs/ERC721Votes.spec b/certora/specs/ERC721Votes.spec index 670f1fd59..0df63d1e2 100644 --- a/certora/specs/ERC721Votes.spec +++ b/certora/specs/ERC721Votes.spec @@ -84,12 +84,8 @@ invariant votes_solvency() to_mathint(totalSupply()) >= totalVotes() { preserved with(env e) { require forall address account. numCheckpoints(account) < 1000000; - // requireInvariant totalVotes_sums_accounts(); } } -// invariant totalVotes_sums_accounts() -// forall address a. forall address b. (a != b && a != 0x0 && b != 0x0) => totalVotes() >= getVotes(delegates(a)) + getVotes(delegates(b)) - // for some checkpoint, the fromBlock is less than the current block number // passes but fails rule sanity from hash on delegate by sig @@ -101,16 +97,11 @@ invariant timestamp_constrains_fromBlock(address account, uint32 index, env e) } } -// TODO add a note about this in the report -// // numCheckpoints are less than maxInt -// // passes because numCheckpoints does a safeCast +// 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) @@ -293,61 +284,4 @@ rule delegate_no_frontrunning(method f) { 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"; -} - - -// mint and burn need to be handled differently for ERC721 - -// rule mint_increases_totalSupply() { - -// env e; -// uint256 amount; address account; -// uint256 fromBlock = e.block.number; -// uint256 totalSupply_ = totalSupply(); - -// mint(e, account, amount); - -// uint256 _totalSupply = totalSupply(); -// require _totalSupply < _maxSupply(); - -// assert _totalSupply == totalSupply_ + amount, "totalSupply not increased properly"; -// assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; -// } - -// rule burn_decreases_totalSupply() { -// env e; -// uint256 amount; address account; - -// uint256 fromBlock = e.block.number; -// uint256 totalSupply_ = totalSupply(); - -// burn(e, account, amount); - -// uint256 _totalSupply = totalSupply(); - -// assert _totalSupply == totalSupply_ - amount, "totalSupply not decreased properly"; -// assert getPastTotalSupply(e, fromBlock) == totalSupply_ , "previous total supply not saved properly"; -// } - - -// rule mint_doesnt_increase_totalVotes() { -// env e; -// uint256 amount; address account; - -// mathint totalVotes_ = totalVotes(); - -// mint(e, account, amount); - -// assert totalVotes() == totalVotes_, "totalVotes increased"; -// } - -// rule burn_doesnt_decrease_totalVotes() { -// env e; -// uint256 amount; address account; - -// mathint totalVotes_ = totalVotes(); - -// burn(e, account, amount); - -// assert totalVotes() == totalVotes_, "totalVotes decreased"; -// } +} \ No newline at end of file diff --git a/resource_errors.json b/resource_errors.json new file mode 100644 index 000000000..d9bd79235 --- /dev/null +++ b/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file