Using Gambit with the Prover

The mutation verifier checks that variants of the original Solidity program do not pass verification against a given specification. You can either use random mutations generated by Gambit or manually crafted with a specific error. If a mutated program passes the specification, it may indicate that the specification is vacuous or not rigorous enough.

Installation

To use the mutation verifier, first install the Certora Prover and its dependencies. To install it, run

pip install certora-cli

If you already have certora-cli installed and the certoraMutate command is not available, you may need to update to a newer version by running

pip install --upgrade certora-cli

Note

If you are on Linux, you will need pip version 20.3 or above.

Running the Mutation Verifier

You need to extend your Prover configuration file by adding a mutation object. The mutation verification script is called certoraMutate. Run it from the command line just like certoraRun:

certoraMutate path/to/prover.conf

If you do, the script will generate code mutants, then submit a verification job per mutant to Certora’s server.

Submitting the verification jobs of the mutants may take several minutes. When it finishes successfully, you should see the following lines printed:

******************** PROVER END ********************

You will receive an email notification when this mutation test is completed. It may take several hours.
You can follow the test's progress at https://prover.certora.com/mutations

The time required to verify all mutants depends on various factors, such as the number of mutants, the complexity of the contracts, and the complexity of the specifications. In some instances, the entire testing process may take several hours.

You can follow the test’s progress in the mutations dashboard. The results will be available in the dashboard when they are ready.

Once the test is completed, you should receive an email that looks like this:

Mutation suceeded email

Mutation Configuration

The mutation tester script requires a Prover JSON .conf configuration file that includes a mutations key. Within this key, an object is defined to specify the behavior of mutation testing. Notably, all other settings, including those influencing compilation or verification, remain consistent with those defined outside the mutations object.

For example, see the file default.conf from the CertoraInit repository:

{
  "files": [
    "contracts/ERC20.sol"
  ],
  "verify": "ERC20:certora/spec/ERC20.spec",
  "msg": "ERC20Rules",
  "mutations": {
    "gambit": [
        {
            "filename" : "contracts/ERC20.sol",
            "num_mutants": 5
        }
    ],
    "msg": "basic mutation configuration"
  } 
}

Mutation Sources

Mutations can either be randomly generated via Gambit, or manually generated by you.

Randomly generated mutations via Gambit

To generate random mutations via Gambit, add a gambit key inside the mutations object. This key should include a list of Gambit mutation objects. All file paths are relative to the current working directory.

For example, see the gambit value from the file advanced_mutation.conf of the CertoraInit repository:

"gambit": [
  {
    "filename": "contracts/ERC20.sol",
    "num_mutants": 2,
    "mutations": [
      "require-mutation"
    ]
  },
  {
    "filename": "contracts/ERC20.sol",
    "num_mutants": 1,
    "mutations": [
      "assignment-mutation"
    ]
  }
],

Manual mutations

You have the option to include manually generated mutated files, not produced by Gambit, in your mutation test. We refer to these as ‘manual mutations.’ They can be used for regression tests, or to check mutations that Gambit does not currently support.

Note

It is recommended to limit each manually mutated file to a single mutation for more accurate coverage analysis and better traceability.

To add manual mutations, under mutations create a key manual_mutants containing a list of manual mutation objects. Each manual mutation object must contain two keys:

  • file_to_mutate: A file path relative to the current working directory of the file we wish to replace with the mutations

  • mutants_location: A relative path to a directory from the current working directory. This directory contains files that will be tested in place of the mutated file. All .sol files in the directory will undergo testing.

For example, see the manual_mutants value from the file advanced_mutation.conf of the CertoraInit repository:

"manual_mutants": [
  {
    "file_to_mutate": "contracts/ERC20.sol",
    "mutants_location": "mutations"
  }
]

If you don’t have a gambit object in the conf file, certoraMutate will run only on the manual mutants, and no other mutants will be generated.

Note

All manual mutations must be named uniquely. For example, if you want to generate manual mutations for C.sol and D.sol, name them C.m1.sol, C.m2.sol, D.m3.sol, D.m4.sol, ... etc.

Original Verification Run

A mutation test requires a verification job that was completed successfully without halting as a basis for comparison, called the original run. All mutant checks will be run with the same verification configuration as the original run, and their results will be compared to the original run. Rules that are not verified or did not pass basic sanity checks on the original run will be ignored.

Generating the original run

Usually, the original run is sent for verification with the mutants. An unaltered file without mutations is sent for verification before all mutant verification runs. The mutation test will be aborted if the original run fails to compile.

The Mutations Dashboard

You can track your mutation tests at the mutations dashboard. A test that just started would look like this:

Mutation test running

  • The Mutation ID is a unique identifier for the test.

  • The Message column includes the description given either in the command line via the --msg flag or the conf file’s "msg" key. It aids in identifying and documenting mutation tests. By default, it will show None.

  • The Status column of a test includes two different parts - the status of the test (see below) and a progress counter. The progress counter shows how many of the sent mutant verification jobs have already been executed.

Mutation test statuses

A mutation test can have one of five different statuses:

  • Running indicates that the verification jobs of the mutants are still being computed.

Mutation test running

  • Calculating indicates that all the verification jobs have finished, and the results are now being gathered and processed into a verification report.

Mutation test calculating

  • Executed indicates that all mutant verification jobs were executed correctly and are available in the report, which can be accessed by clicking on the Mutation ID.

Mutation test executed

  • Halted indicates that the mutation test reached a global time limit and was stopped. The partial verification results that were collected before the time limit are available in the verification report. This usually happens when too many mutants are used in a single test.

Mutation test halted

  • Problem indicates the test had errors. A report is usually not generated.

Mutation test problem

Mutation Test Report

The mutation verification results are summarized in a user-friendly visual report.

Here is an example summary for the advanced mutation of an ERC20 example. The green outer circles represent the rules, and the gray dots represent the mutants.

Report of the advanced mutation of CertoraInit

Selecting a rule shows which mutants it detected, and selecting a mutant shows which rules caught it.

Selecting a rule

Clicking on a mutant’s patch shows the difference between it and the original program.

Showing a mutant patch

Metrics

At the top bar of the report there are different coverage metrics.

Mutation metrics

  • The Coverage metric is the ratio of the caught mutants to all mutants tested, also shown under Caught Mutations.

  • The Rules metric shows the ratio of the rules that caught at least one mutation out of all the rules in the tested specification.

  • The Solo Rules metric shows the ratio between the rules that caught a unique mutation and all rules that caught at least one mutation.

CLI Options

certoraMutate supports the following options; for a comprehensive list, run certoraMutate --help:

Option

Description

--orig_run

Specify the link to a previous verification job

--orig_run_dir

Specify the folder where the files will be downloaded from the original verification job

--msg

Add a message to identify the certoraMutate run

--gambit_only

Stop processing after generating mutations

--dump_failed_collects

Specify a log file to capture mutant collection failures

--debug

Show additional logging information during execution

Troubleshooting

At the moment, there are a few ways in which certoraMutate can fail. Here are some suggestions on how to troubleshoot when that happens. We are actively working on mitigating them.

  • There are currently no official Gambit binaries for Linux ARM or Windows. That means that Gambit will not be installed with pip install certora-cli, and must be built from source.

  • Sometimes, the problem stems from Gambit’s mutant generation. Try running with --gambit_only and look at the generated mutations.

  • Try running the Prover on your mutants individually using certoraRun. Usually the mutant setup will be in .certora_internal/applied_mutants_dir and can be retried by running the Prover’s .conf file with certoraRun. Manual mutants that don’t show up in the report may had a Solidity compilation error. It is also possible that you are encountering a bug with the underlying version of the Prover.

  • Check if your packages paths have a trailing /. The packages paths, both sources and targets, should never end with a /.