3.1. Fixing ERC20 spec¶
Writing specifications is as challenging as writing code, and may contain errors. Let’s continue with the ERC20 example, which can be found in the ERC20 folder. In this folder you will find:
ERC20.spec - the spec file to fix
ERC20.sol - a well known implementation of ERC20
IERC20.sol - the main interface and description of the ERC20 standard
IERC20Metadata.sol - an interface for ERC20 metadata
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
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
A fixed ERC20
spec can be found in the solutions folder at
ERC20Fixed.sol.