2.4. ERC20 Example - preconditions

We demonstrate how sometimes preconditions are needed to avoid unwanted over-approximation. We use the same ERC20.sol contract as before.

Total supply rule

Consider the following property: The total supply of the token \(\geq\) the balance of any single user.

This property is asserted in the rule totalSupplyAfterMint of TotalGreaterThanUser.spec. In this case the assertion is only that the property holds after mint:

/// @title Total supply after mint is at least the balance of the receiving account
rule totalSupplyAfterMint(address account, uint256 amount) {
    env e; 
    
    mint(e, account, amount);
    
    uint256 userBalanceAfter = balanceOf(account);
    uint256 totalAfter = totalSupply();
    
    // Verify that the total supply of the system is at least the current balance of the account.
    assert totalAfter >=  userBalanceAfter, "total supply is less than a user's balance";
}

Let’s run this rule:

certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc solc8.0 --rule totalSupplyAfterMint

Tip

The --rule argument allows running one specific rule from the entire spec file.

Helper variables

As you discovered, the Prover finds that the rule is violated. Understanding the counter-example in this case can be difficult. Adding additional variables to the rule can help understand the counter-example.

Try adding the helper variables userBalanceBefore and totalBefore before calling mint. Re-run the rule and see if you now understand the counter-example.

Hint

Try adding the following lines before calling mint:

uint256 userBalanceBefore = balanceOf(account);
uint256 totalBefore = totalSupply();

Over-approximation

The Prover assumes all possible input values as a starting state, even those that can never be reached. In other words, the Prover over-approximates the possible states of the system. This over-approximation protects the Prover from erroneously claiming that a rule passes. But it may result sometimes in wrong violations, like this case.

Here, the rule is violated when the initial state’s totalSupply is less than the current balance of account. Even though such a state is unreachable by any route of action by any user, the tool still considers this initial state as a valid state.

This is not a mistake but a designed behavior of the Certora Prover. It’s designed to over-approximate states to avoid missing paths that lead to bugs (false positives). However, doing so leads to evaluating states that might not be reachable (false negatives), as shown in this example. In the upcoming lessons, we will learn how to prove that such states are never feasible.

Preconditions

By adding preconditions, one can eliminate infeasible states and put constraints on values. The Rule totalSupplyAfterMintWithPrecondition is a copy of totalSupplyAfterMint with an additional constraint, shown in emphasis below:

/** @title Total supply after mint is at least the balance of the receiving account, with
 *  precondition.
 */
rule totalSupplyAfterMintWithPrecondition(address account, uint256 amount) {
    env e; 
    
    // Assume that in the current state before calling mint, the total supply of the 
    // system is at least the user balance.
    uint256 userBalanceBefore =  balanceOf(account);
    uint256 totalBefore = totalSupply();
    require totalBefore >= userBalanceBefore; 
    
    mint(e, account, amount);
    
    uint256 userBalanceAfter = balanceOf(account);
    uint256 totalAfter = totalSupply();
    
    // Verify that the total supply of the system is at least the current balance of the account.
    assert totalAfter >= userBalanceAfter, "total supply is less than a user's balance ";
}

The Prover will now assume that in the initial state, i.e. before calling mint(), the total supply is at least the user’s balance. Now run the rule totalSupplyAfterMintWithPrecondition:

certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc solc8.0 --rule totalSupplyAfterMintWithPrecondition --msg "running with precondition"

Tip

The --msg flag adds a message description to your run. It can help you recognize a specific run. You will see the message in the run results, and in the jobs list (prover.certora.com).

A note on CVL variables

Unlike Solidity, in CVL an uninitialized variable can have any value, though its possible values are constrained by CVL require statements in the rule. Additionally, CVL variables are immutable, so they cannot be changed in the course of the rule.

We will later meet another kind of variables in CVL which can be modified. These are called ghost variables and we will meet them in Invariants and Ghosts.