3.1. Fixing ERC20 spec

Writing specifications is as challenging as writing code, and specs may contain errors that cause misleading results. Let’s continue with the ERC20 example, which can be found in the ERC20 folder. In this folder you will find:

Use the Certora Prover’s results to find the mistakes in the faulty implementations of the spec and fix the rules. Run certoraRun ERC20.conf (in the ERC20 folder) and understand the violations, then fix the spec to get all the rules passing.

Important: Optimistic loop

When running the spec ERC20.spec you must add "optimistic_loop": true to your config file, or use --optimistic_loop flag if running from command line. Otherwise, you will get a violation whenever the Prover encounters the getters name() and symbol(). The violation occurs because the Prover uses loops to handle strings, or any dynamic array. Loops require special care and handling which we will address in a later lesson. For now, simply use this flag whenever you have a string.

Hints for ERC20

Hint for integrityOfTransferFrom

Prover takes into account all cases, including a non-typical one. Look at the arguments to transferFrom. The spec must cover all cases either by adding another requirement that excludes those particular cases or weakening the assert to hold onto those cases

Hint for balanceChangesFromCertainFunctions

This rule fails for only one function. What is missing in the assert?

Hint for onlyOwnersMayChangeTotalSupply

If a rule fails for multiple functions choose the simplest function and look at the violation. Look at the assert statement and remember the definition of implication.

Hint 1 for doesNotAffectAThirdPartyBalance

Violations can occur on a specific set of values. Look for variables that have the same value.

Hint 2 for doesNotAffectAThirdPartyBalance

thirdParty is not constrained to be different than the from argument in transfer.

Hint

A fixed ERC20 spec can be found in the solutions folder at ERC20Fixed.sol.