Skip to content
This repository has been archived by the owner on Sep 27, 2023. It is now read-only.

ERC20 - totalSupplyNotLessThanSingleUserBalance rule #2

Open
Roy-Certora opened this issue Mar 20, 2022 · 0 comments
Open

ERC20 - totalSupplyNotLessThanSingleUserBalance rule #2

Roy-Certora opened this issue Mar 20, 2022 · 0 comments
Labels
help wanted Extra attention is needed

Comments

@Roy-Certora
Copy link

Roy-Certora commented Mar 20, 2022 •
edited
Loading

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.
@Roy-Certora Roy-Certora added the help wanted Extra attention is needed label Mar 20, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
help wanted Extra attention is needed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Roy-Certora