ERC20

Hints for ERC20

General

A disclaimer before we begin - in all parametric rules that try to invoke the getters name() and symbol() you will get a violation. That happens because the way that the prover handles strings - basically a dynamic array. This representation forces the tool to use loops to handle this data type. Loops are a complex problem in the space of formal verification which we're going to explain and address in later lesson. For now just add the flag --optimistic_loop to the run command or shell script to mitigate this problem.

ERC20Bug1.sol

Hint:

What are the values in the assertion that does not align correctly? Is it possible that the failing function got the final values to such relation?

ERC20Bug2.sol

Hint 1:

How is it possible to overspend and in the same time gain funds?

Hint 2:

remember that code inside the unchecked{} isn't checked for overflow or underflow, so we need to check it manually

ERC20Bug3.sol

Hint 1:

Is there anything in common to the 3 function that fail?

ERC20Bug4.sol

Hint 1:

You've already fixed a similar bug on ERC20Bug2.sol

Hint 2:

Now that you've handled the underflow, is the allowance amount updates correctly?

Rule totalSupplyNotLessThanSingleUserBalance

Hint 1:

Remember that the Certora Prover over-approximate, and so, if never told otherwise, it can start from infeasible states.

Hint 2:

Note what is the initial `totalSupply`, `balanceBefore`, and what is the balance of the user from which the `transfer` is being made. Does the sum of the 2 balances really sum up to `totalSupply`?