Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

docs: add naught coin exercise #211

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
Open
Prev Previous commit
Next Next commit
docs: fix technical issue with burning tokens
  • Loading branch information
ChmielewskiKamil committed Feb 2, 2023
commit 7830d0e4a5f941d16eab98c599343ce49cfeb583
12 changes: 6 additions & 6 deletions program-analysis/echidna/Exercise-X.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ If you are stuck at any point, feel free to look at the following hints. You can
<details>
<summary>5th invariant </summary>

The player should not be able to burn tokens before the `timelock`.
The player should not be able to burn (lock) tokens before the `timelock`.

</details>

Expand Down Expand Up @@ -296,11 +296,11 @@ Run Echidna and check the corpus. Now we have fully covered this property.
<details>
<summary>5th property</summary>

Player should not `burn` tokens before the `timeLock` period.
What is token burning?
You can burn tokens by sending them to the `0` address or by sending them to a non existent address. Sending to the `0` address is not possible because of the `0` address checks in the `ERC20` OZ standard. Sending them to any address shouldn't be possible as well because of the `timeLock`.
Player should not `burn` (lock) tokens before the `timeLock` period.
The `ERC20` used in this exercise does not implement a public `burn` functionality, so the actual burning (removing from the total supply) is not possible.

The only way a player could lock the tokens is by sending them to a non-existent address.

This property would be invalidated if any of our previous property were invalidated (which seems to not be the case at the moment). Let's leave this property for now and move on.

</details>
Expand Down