This repository was archived by the owner on Sep 27, 2023. It is now read-only.
This repository was archived by the owner on Sep 27, 2023. It is now read-only.
ERC20 - totalSupplyNotLessThanSingleUserBalance rule #2
Description
The rule "totalSupplyNotLessThanSingleUserBalance" intends to check the invariance of : totalSupply > UserBalance for a specific user even though the called function didn't use the user as address. One should be advised that the correct rule should check that for all users, or either calculate the actual sum of balances and compare it to the totalSupply variable. Using ghosts is one option but is quite advanced for this level of tutorial.