# 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 {doc}`Gambit <gambit>` 
  or {ref}`manually crafted <man-mutants>` 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 {ref}`install the Certora Prover and its dependencies <installation>`.
To install it, run

```sh
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

```sh
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 {ref}`Prover configuration file <conf-files>` by adding a {ref}`mutation object<mut-conf>`.
The mutation verification script is called `certoraMutate`.
Run it from the command line just like `certoraRun`:

```sh
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:

```text
******************** 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 {ref}`mutations dashboard <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](doc/email_mutation_success.png)

(mut-conf)=
## 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](https://github.com/Certora/CertoraInit) repository:

```json
{
  "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 {doc}`Gambit <gambit>`, or manually generated by you.

### Randomly generated mutations via Gambit

To generate random mutations via {doc}`Gambit <gambit>`, 
  add a `gambit` key inside the `mutations` object. 
This key should include a list of {ref}`Gambit mutation objects <gambit-config>`. 
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](https://github.com/Certora/CertoraInit) repository:

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

(man-mutants)=
### 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](https://github.com/Certora/CertoraInit) repository:

```json
"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 {ref}`basic sanity checks <built-in-sanity>` 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.

(orig-verification-link)=
### Original verification link

You can also provide a link to a run that was already executed.
The mutants will run with the same specification and configuration as that run.
The files relevant for that run will be downloaded to your local machine.

You can provide the original run job's link via `--orig_run`, for example: 
```sh
--orig_run https://prover.certora.com/output/53342/9487899b2afc4709899889fab6c2c673/?anonymousKey=5c365717c9c1076f0c1acb050c7eb5867f07a236
```

```{note}
The run must have the job status `Executed` on the [Prover dashboard](https://prover.certora.com).
```

The files will be downloaded to either a default directory or to one specified with `--orig_run_dir`.

(mutations-dashboard)=
## The Mutations Dashboard

You can track your mutation tests at the [mutations dashboard](https://prover.certora.com/mutations).
A test that just started would look like this:

![Mutation test running](doc/mutation_test_started_dashboard.png)

- 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](doc/mutation_test_started_dashboard.png)

- _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](doc/mutation_test_calculating.png)

- _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](doc/mutation_test_executed.png)

- _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](doc/halted_mutation_test.png)

- _Problem_ indicates the test had errors. A report is usually not generated.

![Mutation test problem](doc/mutation_test_problem.png)

## Mutation Test Report

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


[Here](https://mutation-testing-beta.certora.com/?id=01623b02-0cda-435b-8c31-af9306d6d302&anonymousKey=857c3aeb-169c-4c93-8021-e82058603ca1) 
  is an example summary for the 
  [advanced mutation of an ERC20 example](https://github.com/Certora/CertoraInit/blob/master/mutation/advanced_mutation.conf).
The green outer circles represent the rules, 
  and the gray dots represent the mutants.

![Report of the advanced mutation of CertoraInit](doc/mutation_advanced_results.png)

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

![Selecting a rule](doc/selecting_a_rule.png)

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

![Showing a mutant patch](doc/show_mutant_patch.png)

### Metrics

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

![Mutation metrics](doc/mutation_metrics.png)

- 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`:

| <div style="width:160px">Option</div> | Description                                                                                                           |
|:--------------------------------------|:----------------------------------------------------------------------------------------------------------------------|
| `--orig_run`                          | Specify the {ref}`link to a previous verification job<orig-verification-link>`                                                            |
| `--orig_run_dir`                      | Specify the folder where the files will be downloaded from the {ref}`original verification job <orig-verification-link>` |
| `--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 {ref}`built from source <build-gambit-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`.
  {ref}`Manual mutants <man-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 `/`.