The Certora Equivalence Checker

This chapter describes how one can use the Certora Prover to check the equivalence of two smart contract functions.

Note

Currently the equivalence checker only compares two pure functions, but we are actively working to develop an equivalence checker for non-pure functions as well.

The equivalence checker front-end automatically generates (1) a CVL spec to check if two functions are equivalent, and, (2) a configuration file (.conf) for running the Certora Prover.

Installation

The equivalence checker is part of the certora-cli package; see Installation.

Example

Consider two contracts, BasicMathGood.sol and BasicMathBad.sol shown below with two functions, add and add_mult.

contract BasicMathGood {
    function add(uint256 a, uint256 b) public pure returns(uint256) {
        return a + b;
    }
}

contract BasicMathBad {
    function add_uncheck(uint256 a, uint256 b) public pure returns(uint256) {
        unchecked {
            return a * b;
        }
    }
}

We are interested in checking the equivalence of add and add_uncheck. While this is a simple case, you can imagine scenarios where the functions are more complex. Equivalence checking can be used to check whether two functions that may be implemented differently, are still semantically equivalent. The following sections describe how to use the tool.

Usage

certoraEqCheck can be run either in default (def) mode, in which the user must supply all the required information as command line arguments (see below), or in a conf mode where the user supplies a Certora Prover conf file along with additional arguments.

Default mode

To run the equivalence checker in default mode, use certoraEqCheck:

certoraEqCheck def "path_to_file:contract:function:solc" "path_to_file:contract:function:solc"

For the functions in Example, this would look as follows:

certoraEqCheck def Test/EqCheck/BasicMathGood.sol:add:solc8.0 Test/EqCheck/BasicMathBad.sol:add_pass:solc8.0

In the above example, solc is the name of the executable for the Solidity compiler version you are using. The Solidity compilers do not need to be the same for both arguments to certoraEqCheck, it only need to be appropriate for the given contract. Also note how the contract field can be omitted if the contract name is the same the file name.

Configuration mode

To run the equivalence checker in the configuration mode, use certoraEqCheck as follows:

certoraEqCheck conf <path_to_conf>.conf contract:function contract:function

For the functions in Example, this would be:

   certoraEqCheck conf Test/EqCheck/testGood.conf BasicMathGood:add BasicMathBad:add_mult

where testGood.conf is the standard Certora configuration file and contains:

{
    "disable_local_typechecking": true,
    "files": ["BasicMathGood.sol", "BasicMathBad.sol"],
    "msg": "Equivalence Check",
    "optimistic_loop": true,
    "loop_iter": "4",
    "process": "emv",
    "send_only": true,
    "short_output": true,
    "rule_sanity": "basic",
    "solc": "solc8.0",
    "solc_optimize": "200",
    "server": "staging",
    "prover_version": "master"
}

Note

Use --precise_bitwise_ops if you are comparing functions with bitwise operations. This will slow down the tool slightly, but ensure that the results are sound.

certoraEqCheck produces two files that are then used to run the Certora Prover automatically. The first one is a CVL specification file, whose content in the case of the example shown here is:

  using BasicMathBad as B;

// sets everything but the callee the same in two environments
function e_equivalence(env e1, env e2) {
    require e1.msg.sender == e2.msg.sender;
    require e1.block.timestamp == e2.block.timestamp;
    require e1.msg.value == e2.msg.value;
    // require e1.msg.data == e2.msg.data;
}

rule equivalence_of_revert_conditions()
{
    bool add_revert;
    bool add_mult_revert;
    // using this as opposed to generating input parameters is experimental
    env e_add; calldataarg args;
    env e_add_mult;
    e_equivalence(e_add, e_add_mult);

    add@withrevert(e_add, args);
    add_revert = lastReverted;

    B.add_mult@withrevert(e_add_mult, args);
    add_mult_revert = lastReverted;

    assert(add_revert == add_mult_revert);
}

rule equivalence_of_return_value()
{
    uint256 add_uint256_out0;
    uint256 add_mult_uint256_out0;

    env e_add; calldataarg args;
    env e_add_mult;

    e_equivalence(e_add, e_add_mult);

    add_uint256_out0 = add(e_add, args);
    add_mult_uint256_out0 = B.add_mult(e_add_mult, args);

    assert(add_uint256_out0 == add_mult_uint256_out0);
}

The second one is a standard Certora conf file:

{
    "disable_local_typechecking": true,
    "files": [
        "Test/EqCheck/BasicMathGood.sol",
        "Test/EqCheck/BasicMathBad.sol"
    ],
    "msg": "EquivalenceCheck of add and add_mult",
    "optimistic_loop": true,
    "loop_iter": "4",
    "process": "emv",
    "send_only": true,
    "short_output": true,
    "rule_sanity": "basic",
    "server": "staging",
    "prover_version": "master",
    "solc_optimize": "200",
    "verify": "BasicMathGood:Test/EqCheck/add_to_add_mult_equivalence.spec",
    "solc": "solc8.0"
}

The script then invokes the Certora Prover using this conf file.