2.3. ERC20 Example - Basics

We show how to run a spec and how to interpret the results.

ERC20

Let’s take as an example a straightforward simple ERC20 implementation: ERC20.sol (found in folder: ERC20 lesson). The contract has a mapping from users to their balance and the total supply. The primary operations are transfer, mint, burn and approve. Here is a diagram of the contracts and interfaces:

A simple rule

Thinking about the function transfer, a basic property would be:

Correct transfer functionality:

The balance of the beneficiary is increased appropriately.

The rule transferSpec in ERC20.spec (shown below) verifies this property. In fact, it verifies that the transfer operation both decreases the balance of msg.sender by the transferred amount, and increases the balance of the beneficiary.

/** @title Transfer must move `amount` tokens from the caller's
 *  account to `recipient`
 */
rule transferSpec(address recipient, uint amount) {

    env e;
    
    // `mathint` is a type that represents an integer of any size
    mathint balance_sender_before = balanceOf(e.msg.sender);
    mathint balance_recip_before = balanceOf(recipient);

    transfer(e, recipient, amount);

    mathint balance_sender_after = balanceOf(e.msg.sender);
    mathint balance_recip_after = balanceOf(recipient);

    // Operations on mathints can never overflow nor underflow
    assert balance_sender_after == balance_sender_before - amount,
        "transfer must decrease sender's balance by amount";

    assert balance_recip_after == balance_recip_before + amount,
        "transfer must increase recipient's balance by amount";
}

Note

Formal verification can provide complete coverage of the input space, giving guarantees beyond what is possible from testing alone. All possible inputs to the transfer function (all possible recipients and all possible amounts) are taken into account. Additionally, all possible calling contexts are considered. The Certora Prover represents the calling context through the struct variable env. Declaring a single variable e of type env suffices to capture all aspects of the calling contexts. They can also be addressed individually, some example aspects of the calling context are:

• “Who is the transfer from?” (e.msg.sender)

• “In which block does the deposit occur?” (e.block.number)

• “At which time does the deposit occur?” (e.block.timestamp)

Warning

Every call to a contract function must receive an argument of type env as its first parameter. We will later see that we can declare certain functions as entirely independent of the environment (using the envfree keyword). This will allow us to call such functions without an env type parameter.

Running the Prover

Run the following command line (from the ERC20 lesson folder):

certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0

This command triggers a verification run on the contract ERC20 from the solidity file ERC20.sol, checking all rules in the specification file ERC20.spec.

Note

It is recommended to use config files for running the Prover, see Using config files. Use the command line only for simple cases such as this example.

The command proceeds in two steps:

First step

The solidity files are compiled with the specified solidity compiler, in this case 0.8.0, and the specification file is checked for syntax errors. This step happens on the local machine for fast feedback. The --solc argument is optional (see Options that control the Solidity compiler) You can also use this option to provide a path to the Solidity compiler executable file. The default is solc executable. You may also omit the --solc, if you use solc-select, e.g.

solc-select use 0.8.0

Second step

All necessary files are compressed and sent to Certora’s web server for verification. Verification tasks can be very heavy, so running them on the cloud can save time and resources.

Tip

To learn more about the syntax of the certoraRun command and its different options use the --help flag:

certoraRun --help

Tip

If you are using MacOS and get a Bad CPU type in executable error, you can fix it by installing Rosetta. Do this by executing the following in your terminal:

softwareupdate --install-rosetta

Results

While running, the Prover will print various information to the console about the run. In the end, the output will look similar to this:

...
[INFO]: Process returned with 100

Job is completed! View the results at https://prover.certora.com/...
Finished verification request
ERROR: Prover found violations:
ERROR: [rule] transferSpec

This indicates the Prover found a violation in the rule transferSpec. This violation is a counter example to the rule, and can be viewed in the given link. Alternatively, you can go to prover.certora.com and select this job’s link from the list of your recent jobs. In the link you’ll see the verification report, which looks like this:

Understanding rule violations

Viewing the counter example

The Certora Prover helps understand violations of properties by providing concrete counter examples. To see the counter example, click the violated rule name in the report page. You will see something like this:

The counter-example shows values of the rule’s parameters and variables (on the right hand side), and a call trace (in the middle). You can investigate the call trace to see which functions were called, by clicking on the > symbol to open a detailed view.

So, what is the bug?

Notice that the value of recipient is the same as the value of e.msg.sender. We conclude that:

The rule does not hold when a user transfers to himself

Indeed, when a user transfers balance to themselves, their balance should stay the same. So there is an issue with the rule.

Fixing and re-running

Let’s fix the rule and see if this solves the issue. We already have a fixed version in ERC20Fixed.spec, so we need only run it to see if it fixes the issue. Run:

certoraRun ERC20.sol --verify ERC20:ERC20Fixed.spec --solc solc8.0

Exercise

Here is the fixed rule. Do you understand why it passes, while the previous failed?

/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
rule transferSpec(address recipient, uint amount) {

    env e;
    
    // `mathint` is a type that represents an integer of any size
    mathint balance_sender_before = balanceOf(e.msg.sender);
    mathint balance_recip_before = balanceOf(recipient);

    transfer(e, recipient, amount);

    mathint balance_sender_after = balanceOf(e.msg.sender);
    mathint balance_recip_after = balanceOf(recipient);

    address sender = e.msg.sender;  // A convenient alias

    // Operations on mathints can never overflow or underflow. 
    assert recipient != sender => balance_sender_after == balance_sender_before - amount,
        "transfer must decrease sender's balance by amount";

    assert recipient != sender => balance_recip_after == balance_recip_before + amount,
        "transfer must increase recipient's balance by amount";
    
    assert recipient == sender => balance_sender_after == balance_sender_before,
        "transfer must not change sender's balancer when transferring to self";
}