ERC1155Supply.spec 7.5 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208
  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 != safeBatchTransferFrom(address,address,uint256[],uint256[],bytes).selector
  11. }
  12. {
  13. uint256 token1; uint256 token2;
  14. require token1 != token2;
  15. uint256 token1_before = totalSupply(token1);
  16. uint256 token2_before = totalSupply(token2);
  17. env e; calldataarg args;
  18. f(e, args);
  19. uint256 token1_after = totalSupply(token1);
  20. uint256 token2_after = totalSupply(token2);
  21. assert token1_after != token1_before => token2_after == token2_before,
  22. "methods must not change the total supply of more than one token";
  23. }
  24. /// TODO possibly show equivalence between batch and non-batch methods
  25. /// in order to leverage non-batch rules wrt batch rules
  26. /*
  27. /// The result of transferring a single token must be equivalent whether done
  28. /// via safeTransferFrom or safeBatchTransferFrom.
  29. rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
  30. storage beforeTransfer = lastStorage;
  31. env e;
  32. address holder; address recipient;
  33. uint256 token; uint256 transferAmount; bytes data;
  34. uint256[] tokens; uint256[] transferAmounts;
  35. /// safeTransferFrom(address,address,uint256,uint256,bytes)
  36. /// safeBatchTransferFrom(address,address,uint256[],uint256[],bytes)
  37. mathint holderStartingBalance = balanceOf(holder, token);
  38. mathint recipientStartingBalance = balanceOf(recipient, token);
  39. require tokens.length == 1; require transferAmounts.length == 1;
  40. require tokens[0] == token; require transferAmounts[0] == transferAmount;
  41. // transferring via safeTransferFrom
  42. safeTransferFrom(e, holder, recipient, token, transferAmount, data) at beforeTransfer;
  43. mathint safeTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
  44. // transferring via safeBatchTransferFrom
  45. safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfer;
  46. mathint safeBatchTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
  47. assert safeTransferFromBalanceChange == safeBatchTransferFromBalanceChange,
  48. "Transferring a single token via safeTransferFrom or safeBatchTransferFrom must be equivalent";
  49. }
  50. rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
  51. assert false,
  52. "TODO implement this rule using burn version as structural model";
  53. }
  54. /*
  55. /// The results of burning multiple tokens must be equivalent whether done
  56. /// separately via burn or together via burnBatch.
  57. rule multipleTokenBurnBurnBatchEquivalence {
  58. storage beforeBurns = lastStorage;
  59. env e;
  60. address holder;
  61. uint256 tokenA; uint256 tokenB; uint256 tokenC;
  62. uint256 burnAmountA; uint256 burnAmountB; uint256 burnAmountC;
  63. uint256[] tokens; uint256[] burnAmounts;
  64. mathint startingBalanceA = balanceOf(holder, tokenA);
  65. mathint startingBalanceB = balanceOf(holder, tokenB);
  66. mathint startingBalanceC = balanceOf(holder, tokenC);
  67. require tokens.length == 3; require burnAmounts.length == 3;
  68. require tokens[0] == tokenA; require burnAmounts[0] == burnAmountA;
  69. require tokens[1] == tokenB; require burnAmounts[1] == burnAmountB;
  70. require tokens[2] == tokenC; require burnAmounts[2] == burnAmountC;
  71. // burning via burn
  72. burn(e, holder, tokenA, burnAmountA) at beforeBurns;
  73. burn(e, holder, tokenB, burnAmountB);
  74. burn(e, holder, tokenC, burnAmountC);
  75. mathint burnBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA);
  76. mathint burnBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB);
  77. mathint burnBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC);
  78. // burning via burnBatch
  79. burnBatch(e, holder, tokens, burnAmounts) at beforeBurns;
  80. mathint burnBatchBalanceChangeA = startingBalanceA - balanceOf(holder, tokenA);
  81. mathint burnBatchBalanceChangeB = startingBalanceB - balanceOf(holder, tokenB);
  82. mathint burnBatchBalanceChangeC = startingBalanceC - balanceOf(holder, tokenC);
  83. assert burnBalanceChangeA == burnBatchBalanceChangeA
  84. && burnBalanceChangeB == burnBatchBalanceChangeB
  85. && burnBalanceChangeC == burnBatchBalanceChangeC,
  86. "Burning multiple tokens via burn or burnBatch must be equivalent";
  87. }
  88. /// If passed empty token and burn amount arrays, burnBatch must not change
  89. /// token balances or address permissions.
  90. rule burnBatchOnEmptyArraysChangesNothing {
  91. env e;
  92. address holder; uint256 token;
  93. address nonHolderA; address nonHolderB;
  94. uint256 startingBalance = balanceOf(holder, token);
  95. bool startingPermissionNonHolderA = isApprovedForAll(holder, nonHolderA);
  96. bool startingPermissionNonHolderB = isApprovedForAll(holder, nonHolderB);
  97. uint256[] noTokens; uint256[] noBurnAmounts;
  98. require noTokens.length == 0; require noBurnAmounts.length == 0;
  99. burnBatch(e, holder, noTokens, noBurnAmounts);
  100. uint256 endingBalance = balanceOf(holder, token);
  101. bool endingPermissionNonHolderA = isApprovedForAll(holder, nonHolderA);
  102. bool endingPermissionNonHolderB = isApprovedForAll(holder, nonHolderB);
  103. assert startingBalance == endingBalance,
  104. "burnBatch must not change token balances if passed empty arrays";
  105. assert startingPermissionNonHolderA == endingPermissionNonHolderA
  106. && startingPermissionNonHolderB == endingPermissionNonHolderB,
  107. "burnBatch must not change account permissions if passed empty arrays";
  108. }
  109. */
  110. /******************************************************************************/
  111. ghost mapping(uint256 => mathint) sumOfBalances {
  112. init_state axiom forall uint256 token . sumOfBalances[token] == 0;
  113. }
  114. hook Sstore _balances[KEY uint256 token][KEY address user] uint256 newValue (uint256 oldValue) STORAGE {
  115. sumOfBalances[token] = sumOfBalances[token] + newValue - oldValue;
  116. }
  117. // status: not passing, because mint and burn are the same as transferring to/from
  118. // the 0 address.
  119. invariant total_supply_is_sum_of_balances(uint256 token)
  120. sumOfBalances[token] == totalSupply(token)
  121. {
  122. preserved {
  123. requireInvariant balanceOfZeroAddressIsZero(token);
  124. }
  125. }
  126. /*
  127. rule total_supply_is_sum_of_balances_as_rule {
  128. uint256 token;
  129. require sumOfBalances[token] == totalSupply(token) + balanceOf(0, token);
  130. mathint sum_before = sumOfBalances[token];
  131. method f; calldataarg arg; env e;
  132. f(e, arg);
  133. mathint sum_after = sumOfBalances[token];
  134. assert sumOfBalances[token] == totalSupply(token) + balanceOf(0, token);
  135. }
  136. */
  137. /******************************************************************************/
  138. /// The balance of a token for the zero address must be zero.
  139. invariant balanceOfZeroAddressIsZero(uint256 token)
  140. balanceOf(0, token) == 0
  141. // if a user has a token, then the token should exist
  142. /*
  143. hook Sload _balances[...] {
  144. require balance <= totalSupply
  145. }
  146. */
  147. rule held_tokens_should_exist {
  148. address user; uint256 token;
  149. requireInvariant balanceOfZeroAddressIsZero(token);
  150. // This assumption is safe because of total_supply_is_sum_of_balances
  151. require balanceOf(user, token) <= totalSupply(token);
  152. assert balanceOf(user, token) > 0 => exists_wrapper(token),
  153. "if a user's balance for a token is positive, the token must exist";
  154. }
  155. /******************************************************************************/
  156. rule sanity {
  157. method f; env e; calldataarg args;
  158. f(e, args);
  159. assert false;
  160. }