ERC20Votes.spec 6.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148
  1. import "helpers.spec"
  2. import "methods/IERC20.spec"
  3. import "methods/IERC5805.spec"
  4. import "methods/IERC6372.spec"
  5. import "ERC20.spec"
  6. methods {
  7. numCheckpoints(address) returns (uint32) envfree
  8. ckptFromBlock(address, uint32) returns (uint32) envfree
  9. ckptVotes(address, uint32) returns (uint224) envfree
  10. maxSupply() returns (uint224) envfree
  11. }
  12. use invariant totalSupplyIsSumOfBalances
  13. /*
  14. ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
  15. │ Ghost: user (current) voting weight │
  16. └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
  17. */
  18. ghost lastUserVotes(address) returns uint224 {
  19. init_state axiom forall address a. lastUserVotes(a) == 0;
  20. }
  21. ghost userCkptNumber(address) returns uint32 {
  22. init_state axiom forall address a. userCkptNumber(a) == 0;
  23. }
  24. ghost lastUserIndex(address) returns uint32;
  25. ghost lastUserTimepoint(address) returns uint32;
  26. /*
  27. ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
  28. │ Ghost: total voting weight │
  29. └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
  30. */
  31. ghost totalVotes() returns uint224 {
  32. init_state axiom totalVotes() == 0;
  33. }
  34. /*
  35. ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
  36. │ Ghost: duplicate checkpoint detection │
  37. └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
  38. */
  39. ghost lastUserDuplicate(address) returns bool {
  40. init_state axiom forall address a. lastUserDuplicate(a) == false;
  41. }
  42. /*
  43. ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
  44. │ Hook │
  45. └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
  46. */
  47. hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].votes uint224 newVotes (uint224 oldVotes) STORAGE {
  48. havoc lastUserVotes assuming
  49. lastUserVotes@new(account) == newVotes;
  50. havoc totalVotes assuming
  51. totalVotes@new() == totalVotes@old() + newVotes - lastUserVotes(account);
  52. havoc lastUserIndex assuming
  53. lastUserIndex@new(account) == index;
  54. }
  55. hook Sstore currentContract._checkpoints[KEY address account][INDEX uint32 index].fromBlock uint32 newTimepoint (uint32 oldTimepoint) STORAGE {
  56. havoc lastUserTimepoint assuming
  57. lastUserTimepoint@new(account) == newTimepoint;
  58. havoc userCkptNumber assuming
  59. userCkptNumber@new(account) == index + 1;
  60. havoc lastUserDuplicate assuming
  61. lastUserDuplicate@new(account) == (newTimepoint == lastUserTimepoint(account));
  62. }
  63. definition max_uint224() returns uint224 = 0xffffffffffffffffffffffffffff;
  64. invariant clockMode(env e)
  65. clock(e) == e.block.number || clock(e) == e.block.timestamp
  66. invariant numCheckpointsConsistency(address a)
  67. userCkptNumber(a) == numCheckpoints(a) &&
  68. userCkptNumber(a) <= max_uint32
  69. invariant lastUserVotesAndTimepointConsistency(address a)
  70. numCheckpoints(a) > 0 => (
  71. lastUserIndex(a) == numCheckpoints(a) - 1 &&
  72. lastUserIndex(a) <= max_uint32 &&
  73. lastUserVotes(a) == ckptVotes(a, lastUserIndex(a)) &&
  74. lastUserVotes(a) <= max_uint224() &&
  75. lastUserTimepoint(a) == ckptFromBlock(a, lastUserIndex(a)) &&
  76. lastUserTimepoint(a) <= max_uint224()
  77. )
  78. /*
  79. invariant noDuplicate(address a)
  80. !lastUserDuplicate(a)
  81. // passes
  82. invariant userVotesOverflow()
  83. forall address a. lastUserVotes(a) <= max_uint256
  84. invariant userVotes(env e)
  85. forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) == getVotes(e, a)
  86. {
  87. preserved {
  88. requireInvariant totalSupplyIsSumOfBalances;
  89. }
  90. }
  91. invariant userVotesLessTotalVotes()
  92. forall address a. userCkptNumber(a) > 0 => lastUserVotes(a) <= totalVotes()
  93. {
  94. preserved {
  95. requireInvariant totalSupplyIsSumOfBalances;
  96. }
  97. }
  98. // passes
  99. invariant totalVotesLessTotalSupply()
  100. totalVotes() <= totalSupply()
  101. {
  102. preserved {
  103. requireInvariant totalSupplyIsSumOfBalances;
  104. }
  105. }
  106. */