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

Added unfinished invariant regarding user token sums and totalSupply

Browse Source
This commit is contained in:
Thomas Adams
2022-05-10 17:36:19 -07:00
parent 2fc3a5d4b8
commit 0deaee1217
1 changed files with 9 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
certora/specs/ERC1155Supply.spec
View File

@ -1,6 +1,7 @@
methods {
totalSupply(uint256) returns uint256 envfree
balanceOf(address, uint256) returns uint256 envfree
}
/// given two different token ids, if totalSupply for one changes, then
@ -28,6 +29,14 @@ filtered {
"methods must not change the total supply of more than one token";
}
invariant sum_user_token_balances_vs_totalSupply(uint256 id, address user1, address user2)
balanceOf(user1, id) + balanceOf(user2, id) <= totalSupply(id)
{ preserved {
require user1 != user2;
//for every address not user1 or user2, balance is < user1 and < user2
require forall address user3. (user3 != user1 && user3 != user2) => balanceOf(user3, id) < balanceOf(user1, id) && balanceOf(user3, id) < balanceOf(user2, id);
}
}
rule sanity {
method f; env e; calldataarg args;