2.5. Parametric rules

We continue with our ERC20 example, to demonstrate parametric rules.

The need

Many properties can be generalized for all the contract’s functions. For example, consider the property:

Allowance integrity:

The allowance can only be changed by the owner.

This property should hold regardless of the contract method called. To do so, we introduce the notion of parametric rules.

Usage

Applying

To simulate the execution of all functions in the main contract we use a method variable method f, either as a parameter to the rule, or as a local variable. The most common usage is to simulate any method on any arguments, using the following syntax:

rule someParametricRule(method f) {
    ...
    env e;  // The env for f
    calldataarg args;  // Any possible arguments for f
    f(e, args);  // Calling the contract method f
    ...
}

Different functions in the contract might have different number or types of parameters. Using a variable of CVL type calldataarg solves this problem and ensures that each simulated contract method gets valid input parameters.

Referring to particular methods

At times, we need to handle particular methods differently. For example we sometimes wish to exclude certain methods from the rule. To differentiate between methods (or values of method f) use selector and sig, like so:

f.selector == sig:approve(address, uint).selector

The above evaluates to true when f is the method approve with the specified signature.

Here is a more complete example from Parametric.spec:

    // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
    assert (
        allowance_after > allowance_before =>
        (
            f.selector == sig:approve(address, uint).selector ||
            f.selector == sig:increaseAllowance(address, uint).selector
        )
    ),
    "only approve and increaseAllowance can increase allowances";
}

Example

Run the parametric rule from Parametric.spec:

certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"

The rule would have a check mark (i.e. passed verification) only if it was verified on all contract methods. An inner rule is created for every function in the main contract, as you can see in the report page. Click on the function name to see its counter-example.

This rule uncovers a bug in decreaseAllowance method. Can you understand the counter-example?

Conclusion

Parametric rules enable expressing reusable and concise correctness conditions. Note that they are not dependent on the implementation. So you can integrate them easily into the CI to verify changes to the code, including signature changes, new functions, and implementation changes.