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

filters for skipped functions

Browse Source
This commit is contained in:
Nick Armstrong
2022-08-11 21:11:01 -07:00
parent 3e6045155e
commit 4a3b0bb875
4 changed files with 13 additions and 30 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
certora/specs/ERC20Votes.spec
View File

@ -18,13 +18,10 @@ methods {
mint(address, uint256)
burn(address, uint256)
unsafeNumCheckpoints(address) returns (uint256) envfree
// solidity generated getters
_delegates(address) returns (address) envfree
// external functions
}
// gets the most recent votes for a user
ghost userVotes(address) returns uint224 {
@ -36,9 +33,7 @@ ghost totalVotes() returns mathint {
init_state axiom totalVotes() == 0;
axiom totalVotes() >= 0;
}
ghost lastIndex(address) returns uint32;
// helper
hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
@ -82,12 +77,12 @@ invariant votes_solvency()
// for some checkpoint, the fromBlock is less than the current block number
invariant blockNum_constrains_fromBlock(address account, uint32 index, env e)
ckptFromBlock(account, index) < e.block.number
filtered { f -> !f.isView }
{
preserved {
require index < numCheckpoints(account);
}
}
// numCheckpoints are less than maxInt
// passes because numCheckpoints does a safeCast
// invariant maxInt_constrains_numBlocks(address account)
@ -97,6 +92,7 @@ invariant blockNum_constrains_fromBlock(address account, uint32 index, env e)
// passes
invariant fromBlock_constrains_numBlocks(address account)
numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1)
filtered { f -> !f.isView }
{ preserved with(env e) {
require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
}}
@ -109,11 +105,13 @@ invariant fromBlock_constrains_numBlocks(address account)
// passes + rule sanity
invariant fromBlock_greaterThanEq_pos(address account, uint32 pos)
ckptFromBlock(account, pos) >= pos
filtered { f -> !f.isView }
// 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)
filtered { f -> !f.isView }
// converted from an invariant to a rule to slightly change the logic
@ -144,27 +142,21 @@ rule transfer_safe() {
uint256 amount;
address a; address b;
require delegates(a) != delegates(b); // confirmed if they both delegate to the same person then transfer keeps the votes the same
require numCheckpoints(delegates(a)) < 1000000;
require numCheckpoints(delegates(b)) < 1000000;
uint256 votesA_pre = getVotes(delegates(a));
uint256 votesB_pre = getVotes(delegates(b));
mathint totalVotes_pre = totalVotes();
transferFrom(e, a, b, amount);
mathint totalVotes_post = totalVotes();
uint256 votesA_post = getVotes(delegates(a));
uint256 votesB_post = getVotes(delegates(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 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 &&
@ -174,14 +166,10 @@ rule delegates_safe(method f) filtered {f -> (f.selector != delegate(address).se
env e; calldataarg args;
address account;
address pre = delegates(account);
f(e, args);
address post = delegates(account);
assert pre == post, "invalid delegate change";
}
// delegates increases the delegatee's votes by the proper amount
// passes + rule sanity
rule delegatee_receives_votes() {

2
certora/specs/ERC20Wrapper.spec
View File

@ -15,7 +15,7 @@ methods {
// totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency
invariant whatAboutTotal(env e)
totalSupply(e) <= underlyingTotalSupply()
filtered { f -> f.selector != certorafallback_0().selector }
filtered { f -> f.selector != certorafallback_0().selector && !f.isView}
{
preserved {
require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();

13
certora/specs/ERC721Votes.spec
View File

@ -67,19 +67,11 @@ hook Sstore _checkpoints[KEY address account].fromBlock uint32 newBlock (uint32
doubleFromBlock@new(account) == (newBlock == lastFromBlock(account));
}
// sum of user balances is >= total amount of delegated votes
// blocked by tool error
invariant votes_solvency()
to_mathint(totalSupply()) >= totalVotes()
{ preserved with(env e) {
require forall address account. numCheckpoints(account) < 1000000;
} }
// for some checkpoint, the fromBlock is less than the current block number
// passes but fails rule sanity from hash on delegate by sig
invariant timestamp_constrains_fromBlock(address account, uint32 index, env e)
ckptFromBlock(account, index) < e.block.number
filtered { f -> !f.isView }
{
preserved {
require index < numCheckpoints(account);
@ -95,6 +87,7 @@ invariant timestamp_constrains_fromBlock(address account, uint32 index, env e)
// passes
invariant fromBlock_constrains_numBlocks(address account)
numCheckpoints(account) <= ckptFromBlock(account, numCheckpoints(account) - 1)
filtered { f -> !f.isView }
{ preserved with(env e) {
require e.block.number >= ckptFromBlock(account, numCheckpoints(account) - 1); // this should be true from the invariant above!!
}}
@ -107,11 +100,13 @@ invariant fromBlock_constrains_numBlocks(address account)
// passes + rule sanity
invariant fromBlock_greaterThanEq_pos(address account, uint32 pos)
ckptFromBlock(account, pos) >= pos
filtered { f -> !f.isView }
// 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)
filtered { f -> !f.isView }
// converted from an invariant to a rule to slightly change the logic

8
certora/specs/TimelockController.spec
View File

@ -40,25 +40,25 @@ function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data
// `isOperation()` correctness check
invariant operationCheck(bytes32 id)
getTimestamp(id) > 0 <=> isOperation(id)
filtered { f -> !f.isView }
// STATUS - verified
// `isOperationPending()` correctness check
invariant pendingCheck(bytes32 id)
getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id)
filtered { f -> !f.isView }
// STATUS - verified
// `isOperationReady()` correctness check
invariant readyCheck(env e, bytes32 id)
(e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id)
filtered { f -> !f.isView }
// STATUS - verified
// `isOperationDone()` correctness check
invariant doneCheck(bytes32 id)
getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id)
filtered { f -> !f.isView }
////////////////////////////////////////////////////////////////////////////