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 mutationTest 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 path/to/config/file/Example.conf

Configuration

The tool expects a configuration file (extension .conf is required). which is a JSON object. Here is an example configuration file:

{
    "project_folder" : "Test/10Power",
    "run_script" : "Test/10Power/runDefault.sh",
    "gambit" : {
        "filename" : "Test/10Power/TenPower.sol",
        "solc" : "solc8.10"
    },
    "staging" : "master",
    "manual_mutations" : {
        "path/to/original/file.sol" : "path/to/manual/mutations/",
        "...": "..."
    },
    "...": "..."
}

Note: This configuration is separate from the Prover’s .conf file and also from the configuration file of the mutation generator (Running Gambit Through a Configuration File). Importantly, notice that to use this tool, you can embed the configuration for generating the mutants in this .conf file; you don’t need to write two separate configurations.

Required Keys for the JSON Configuration File:

  • "project_directory" : the directory containing the original Prover project on which to perform mutation testing

  • "run_script" : the bash script used to run verification on the original project, usually project_directory/run.sh or similar. Gambit will pull the configuration for certoraRun from this shell script and verify each mutant using this configuration.

  • "gambit" : the JSON configuration element for invoking Gambit. May be a path to a gambit configuration file or the explicit JSON element contained therein. See Running Gambit Through a Configuration File for more information about the gambit configuration. The solc specific arguments (including the version of the compiler) should be provided here even if they are present in the run_script.

Optional Keys for the JSON Configuration File

  • "num_threads" : the maximum number of threads to use for verification, as an integer

  • "manual_mutations" : optionally supplement the random mutant generation with your own manually-written mutants. Expects a JSON object whose keys are the paths to the original files and whose values are paths to directories containing manually-written mutants as .sol files.

Note

Any manual mutations files provided must follow the naming convention OriginalFileName.<unique-name>.sol, where <unique-name> is a string ID unique with respect to the other manual mutants (for example you might name them OriginalFileName.m1.sol, OriginalFileName.m2.sol and so on).

Additional Optional Flags

Note

Gambit supports --staging [branch] and --cloud.

However, Gambit currently has trouble with --send_only in the run scripts. If you have this flag, please remove it for now. Apologies for the temporary inconvenience!

  • "offline" : run mutation testing without internet connection, skipping the UI output and other web functions. Expects a boolean and defaults to false.

  • "staging" : if your run script does not already have --staging, you can also add it to Gambit. Similar to the Prover, you can provide the branch name for running mutant verification on --staging. We support "staging" : true as an alternative to "staging" : "master". Omitting this key will cause verification to run locally (unless the run script has it).

  • "cloud" : if you instead want to run on the cloud environment you can provide the --cloud flag. You can also add the name of a specific branch.

  • "use_certora_run_py" : Use certoraRun.py rather than certoraRun. Expects a boolean and defaults to false.

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.

  • Make sure the run script you use to run the Prover does not have the --send_only flag or any commented out (using #) lines.

  • Since Gambit requires you to provide the solidity compiler flags to compile the mutants, sometimes it might be useful to first identify what those flags should be. See Running Gambit Through a Configuration File for more information. A strategy you can adopt is

    • first run gambit without going through certoraMutate (you likely have either gambit-linux or gambit-macos binaries in your path already if you are running the tool).

    • Make a foo.json file and copy the content of the "gambit": field in it.

    • Run gambit-OS mutate --json foo.json to identify the issue.

Visualization

The mutation verification results are summarized in an 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.