Using Gambit with the Prover
This is the mutation verifier which checks that variants of the original solidity program do not pass the specification. It uses mutations from the Gambit mutation generator. It also allows users to include manually generated mutants. If a mutated program passes the specification, it may indicate that the specification is vacuous or not rigorous enough. In the rest of the document, we refer to both the mutation generator and the verifier as Gambit.
Installations and Setup
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
Running the Mutation Verifier
Once you have updated your certora-cli
installation using pip
to get the relevant
dependencies, run Gambit from the command line:
certoraMutate --prover_conf path/to/prover/prover.conf --mutation_conf path/to/mutation/mutation.conf
Note
You must run certoraMutate
from the root of the Solidity project directory.
The files prover.conf
and mutation.conf
can be in their own directories.
All paths in mutation.conf
are relative to the parent directory containing mutation.conf
.
Paths in prover.conf
are all relative to the project directory’s root, which is assumed to be the working directory.
of the project directory, which is assumed to be the working directory.
Configurations
The tool expects two separate configuration files:
the configuration file which defines the execution of mutant generation (--mutation_conf
),
and the configuration file which defines execution of the Prover (--prover_conf
).
Here is a simple configuration file setup using the example above:
In prover.conf
:
{
"files": [
"C.sol"
],
"verify": "C:c.spec"
}
In mutation.conf
:
{ "gambit": {
"filename" : "C.sol",
"num-mutants": 5
}
}
Manual Mutations
You can add manual mutations to mutation.conf
like so:
{ "gambit": {
"filename" : "C.sol",
"num-mutants": 5
},
"manual_mutants": {
"C.sol": "path/to/dir/with/manual_mutants/for/C"
}
}
If you set num_mutants
to 0 in the above file, gambit
will run only on the mutants added manually and no other mutants will be generated.
certoraMutate
on manually written mutants.
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 as C.m1.sol, C.m2.sol, D.m3.sol, D.m4.sol, ...
etc.
CLI Options
certoraMutate
runs in two distinct modes: synchronous and asynchronous.
Use the --sync
flag to run the entire tool synchronously
in your shell, from mutant generation to the web report UI.
Alternatively, running without the --sync
flag will dump
data about the mutation verification jobs in the collect.json
file in the working directory. These jobs are submitted
to the server environment specified and run asynchronously.
They may be polled later with
certoraMutate --collect_file collect.json
.
Usually, the synchronous mode is suitable when the original specification run finishes quickly. The asynchronous mode is suitable for bigger specifications of more complicated contracts, where each run takes more than just several minutes. It avoids depending on an active internet connection for the entire duration of the original run and the mutations. Soon, Certora will enable automatic notifications for asynchronous mutation testing runs, so that manual checks will not be necessary.
certoraMutate
supports the following options; for a comprehensive list, run certoraMutate --help
:
Option |
Description |
---|---|
|
specify the Prover configuration file for verifying mutants |
|
specify the configuration file for mutant generation |
|
request the mutant generator to generate a specific number of mutants. Defaults to 5 |
|
specify the version of |
|
specify the server environment to run on. Defaults to the value specified in the file of |
|
show additional logging information during execution |
|
specify the output directory for gambit. Defaults to a new directory which is added in the working directory |
|
specify the target directory for mutant verification build files. Defaults to a hidden Prover internal directory |
|
specify a JSON file to dump the mutant verification report used for the web UI |
|
specify a text file to write the UI report link |
|
specify a CSV file to write the verification report. Much of this content is in the JSON report as well, but this is intended to be an alternative representation of the data |
|
specify the collect file from which to run in asynchronous mode |
|
enable synchronous execution |
|
specify the maximum number of times a web request is attempted |
|
specify the length in seconds for a web request timeout |
|
specify the number of minutes to poll a task in sync mode before giving up. Polling is possible even after the timeout with another call to |
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.
Sometimes it might be useful to first run
gambit
without going throughcertoraMutate
.gambit
can be found under thesite-packages
directory undercertora_bins
.Run
gambit mutate --json foo.json
orgambit mutate --filename solidity.sol
to identify the issue.Here,
foo.json
can also befoo.conf
.Note. you must remove the field
manual_mutants
from thejson
if it is present, before runninggambit
.
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 withcertoraRun
. It is also possible that you are encountering a bug with the underlying version of the Prover.In sync mode, even if the polling timeout was hit, it is possible to re-run
certoraMutate
with just the--collect_file
option to to retry getting the results without restarting the entire mutation testing task.
Visualization
The mutation verification results are summarized in a user-friendly visualization. Here is an example summary for the Borda example. Rules are represented by the green outer circles and the mutants are represented by the gray dots. Selecting a rule shows which mutants it detected and selecting a mutant shows which rules detected it. The coverage metric is computed as the fraction of total generated mutants that were detected. Clicking on a mutant’s patch also shows the diff with respect to the original program.