NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

comment cleanup

Browse Source
This commit is contained in:
Nick Armstrong
2022-04-11 13:26:46 -07:00
parent 6662d0556f
commit 135e21f35d
2 changed files with 6 additions and 69 deletions
Download Patch File Download Diff File Expand all files Collapse all files

72
certora/specs/ERC721Votes.spec
View File

@ -84,12 +84,8 @@ invariant votes_solvency()
to_mathint(totalSupply()) >= totalVotes() to_mathint(totalSupply()) >= totalVotes()
{ preserved with(env e) { { preserved with(env e) {
require forall address account. numCheckpoints(account) < 1000000; 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 // for some checkpoint, the fromBlock is less than the current block number
// passes but fails rule sanity from hash on delegate by sig // 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
// // numCheckpoints are less than maxInt // passes because numCheckpoints does a safeCast
// // passes because numCheckpoints does a safeCast
// invariant maxInt_constrains_numBlocks(address account) // invariant maxInt_constrains_numBlocks(address account)
// numCheckpoints(account) < 4294967295 // 2^32 // 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 // can't have more checkpoints for a given account than the last from block
// passes // passes
invariant fromBlock_constrains_numBlocks(address account) 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 _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 third != 0 => _third_votes == third_votes_ - delegator_bal, "votes not removed from third";
assert other_votes_ == _other_votes, "delegate not contained"; 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";
// }

3
resource_errors.json Normal file
View File

@ -0,0 +1,3 @@
{
"topics": []
}