ERC1155Supply.spec 2.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293
  1. methods {
  2. totalSupply(uint256) returns uint256 envfree
  3. balanceOf(address, uint256) returns uint256 envfree
  4. exists_wrapper(uint256) returns bool envfree
  5. }
  6. /// given two different token ids, if totalSupply for one changes, then
  7. /// totalSupply for other should not
  8. rule token_totalSupply_independence(method f)
  9. filtered {
  10. f -> f.selector != _burnBatch(address,uint256[],uint256[]).selector
  11. && f.selector != _mintBatch(address,uint256[],uint256[],bytes).selector
  12. && f.selector != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector
  13. }
  14. {
  15. uint256 token1; uint256 token2;
  16. require token1 != token2;
  17. uint256 token1_before = totalSupply(token1);
  18. uint256 token2_before = totalSupply(token2);
  19. env e; calldataarg args;
  20. f(e, args);
  21. uint256 token1_after = totalSupply(token1);
  22. uint256 token2_after = totalSupply(token2);
  23. assert token1_after != token1_before => token2_after == token2_before,
  24. "methods must not change the total supply of more than one token";
  25. }
  26. /******************************************************************************/
  27. ghost mapping(uint256 => mathint) sumOfBalances;
  28. hook Sstore _balances[KEY uint256 token][KEY address user] uint256 newValue (uint256 oldValue) STORAGE {
  29. sumOfBalances[token] = sumOfBalances[token] + newValue - oldValue;
  30. }
  31. // status: not passing, because mint and burn are the same as transferring to/from
  32. // the 0 address.
  33. invariant total_supply_is_sum_of_balances(uint256 token)
  34. sumOfBalances[token] == totalSupply(token) + balanceOf(0, token)
  35. rule total_supply_is_sum_of_balances_as_rule {
  36. uint256 token;
  37. require sumOfBalances[token] == totalSupply(token) + balanceOf(0, token);
  38. mathint sum_before = sumOfBalances[token];
  39. method f; calldataarg arg; env e;
  40. f(e, arg);
  41. mathint sum_after = sumOfBalances[token];
  42. assert sumOfBalances[token] == totalSupply(token) + balanceOf(0, token);
  43. }
  44. /******************************************************************************/
  45. /// The balance of a token for the zero address must be zero.
  46. invariant balanceOfZeroAddressIsZero(uint256 token)
  47. balanceOf(0, token) == 0
  48. // if a user has a token, then the token should exist
  49. /*
  50. hook Sload _balances[...] {
  51. require balance <= totalSupply
  52. }
  53. */
  54. rule held_tokens_should_exist {
  55. address user; uint256 token;
  56. // This assumption is safe because of total_supply_is_sum_of_balances
  57. require balanceOf(user, token) <= totalSupply(token);
  58. assert balanceOf(user, token) > 0 => exists_wrapper(token),
  59. "if a user's balance for a token is positive, the token must exist";
  60. }
  61. /******************************************************************************/
  62. rule sanity {
  63. method f; env e; calldataarg args;
  64. f(e, args);
  65. assert false;
  66. }