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

removed sanity

Browse Source
This commit is contained in:
Nick Armstrong
2022-04-11 13:56:34 -07:00
parent 135e21f35d
commit 02de598056
2 changed files with 3 additions and 64 deletions
Download Patch File Download Diff File Expand all files Collapse all files

56
certora/specs/ERC20Votes.spec
View File

@ -70,35 +70,14 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint
doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
}
rule sanity(method f) {
env e;
calldataarg arg;
f(e, arg);
assert false;
}
// something stupid just to see
invariant sanity_invariant()
totalSupply() >= 0
// sum of user balances is >= total amount of delegated votes
// fails on burn. This is because burn does not remove votes from the users
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))
// invariant totalVotes_sums_accounts()
// forall address a. forall address b. (a != b) => totalVotes() >= userVotes(a) + userVotes(b)
// { preserved {
// require forall address account. numCheckpoints(account) < 1000000;
// }}
// for some checkpoint, the fromBlock is less than the current block number
invariant blockNum_constrains_fromBlock(address account, uint32 index, env e)
@ -109,16 +88,11 @@ invariant blockNum_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)
@ -362,28 +336,4 @@ rule burn_doesnt_decrease_totalVotes() {
burn(e, account, amount);
assert totalVotes() == totalVotes_, "totalVotes decreased";
}
// // fails
// rule mint_increases_totalVotes() {
// env e;
// uint256 amount; address account;
// mathint totalVotes_ = totalVotes();
// mint(e, account, amount);
// assert totalVotes() == totalVotes_ + to_mathint(amount), "totalVotes not increased";
// }
// // fails
// rule burn_decreases_totalVotes() {
// env e;
// uint256 amount; address account;
// mathint totalVotes_ = totalVotes();
// burn(e, account, amount);
// assert totalVotes() == totalVotes_ - to_mathint(amount), "totalVotes not decreased";
// }
}

11
certora/specs/ERC721Votes.spec
View File

@ -67,17 +67,6 @@ hook Sstore _checkpoints[KEY address account].fromBlock uint32 newBlock (uint32
doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
}
rule sanity(method f) {
env e;
calldataarg arg;
f(e, arg);
assert false;
}
// something stupid just to see
invariant sanity_invariant()
totalSupply() >= 0
// sum of user balances is >= total amount of delegated votes
// blocked by tool error
invariant votes_solvency()