> For the complete documentation index, see [llms.txt](https://docs.runtimeverification.com/kontrol/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.runtimeverification.com/kontrol/guides/advancing-proofs.md).

# Advancing Proofs

{% hint style="info" %}
**Prerequisites:** Before proceeding with this section, it is recommended that you have already gone through the [Kontrol Example](/kontrol/guides/kontrol-example.md) and have a basic understanding of the [**K**](https://github.com/runtimeverification/k) framework and [**KEVM**](https://github.com/runtimeverification/evm-semantics). For more information, refer to [Resources](/kontrol/learn-more/resources.md) page.
{% endhint %}

***

## Manual Intervention

During the verification process using [**Kontrol**](https://github.com/runtimeverification/kontrol), there are situations where manual intervention is necessary to help the tool reason correctly and advance the symbolic execution. Two common situations involve `stuck` nodes and invalid execution paths.

* `stuck` **nodes:** These nodes have not reached the end of execution, have not been subsumed into the target node, *and* **Kontrol** does not see any further execution steps.
* **Invalid execution paths:** It is not always easy for **Kontrol** to deduce that a particular execution path is infeasible. If an invalid execution path is traversed, it means that **Kontrol** failed to identify a contradiction from the path condition.

When these situations arise, the way to progress past them is to identify the missing reasoning links and make them available to **Kontrol** as Lemmas.

## Intro to Lemmas

Lemmas can be seen as one-step reasoning processes that you want **Kontrol** to consider during symbolic execution of your properties.

Similar to `rewrite` rules, lemmas have a left-hand side (LHS) and a right-hand side (RHS). When **Kontrol** identifies a symbolic match for the LHS in the **K** configuration of a proof, it applies the rule and rewrites the LHS to the RHS.

### Structure of a Lemma

The general structure of a lemma is as follows:

```bash
rule [name-of-lemma]: <k> LHS(X, Y) => RHS(X, Y) </k>
  requires condition1(X)
  andBool condition2(Y)
  [simplification]
```

In short, lemmas are simplification rules, specifically, **K** rewrite rules with the `simplification` attribute. You can include other attributes in addition to `simplification`. Below is a list of commonly used attributes when defining lemmas:

* `smt-lemma`: passes the `simplification` rule down to the SMT-solver. To use this predicate, the functions in the lemma must be defined with the `smt-lib` attribute.
* `concrete(VAR)`: applies the rule only when `VAR` can be matched to a concrete value
* `symbolic(VAR)`: applies the rule only when `VAR` can be matched to a symbolic value

Multiple attributes can be separated by commas, for example: `[simplification, concrete(X), symbolic(Y)]`. Additionally, instead of the `andBool` connective, `orBool` can also be used.

### Lemmas and Your Verification Project

To add lemmas to your project, create a file called: `myproject-lemmas.k`. This file is usually located in the `kontrol/` directory and should have the following structure:

```solidity
requires "foundry.md"

module MYPROJECT-LEMMAS
    imports BOOL
    imports FOUNDRY
    imports INFINITE-GAS
    imports INT-SYMBOLIC

// Your lemmas go here

endmodule
```

After creating this file, you need to inform **Kontrol** about the lemmas in the file so that it can reason with them. This can be done during the `build` phase of your project. To include `test/myproject-lemmas.k` in the reasoning capabilities of **Kontrol**, the following flags should be included:

* `--require test/myproject-lemmas.k` : specifies from which file the module `MYPROJECT-LEMMAS` is imported.
* `--module-import MyProjectTests:MYPROJECT-LEMMAS`: specifies the module to import. The module name is preceded by the string `MyProjectTests:` , which represents the contract name for the tests being symbolically executed.
* `--rekompile` (optional): rebuild the project. It is necessary to include the `--rekompile` flag when adding new lemmas, otherwise **Kontrol** won't be aware of them.

You can find more information about `build` flags here: [Kontrol Cheatsheet](/kontrol/cheatsheets/kontrol-cheatsheet.md#kontrol-build)

To `build` with the flags above, run the following command:

{% code fullWidth="true" %}

```bash
kontrol build --require kontrol/myproject-lemmas.k --module-import MyProjectTests:MYPROJECT-LEMMAS
```

{% endcode %}

### Finding Lemmas

In the next section, we will explore how to find **KEVM** lemmas, which are used to address reasoning gaps at the EVM semantic level. The following sections, [Simplifications Guide](/kontrol/guides/advancing-proofs/simplifications-guide.md) and [Rule Application](/kontrol/guides/advancing-proofs/rule-application.md), cover the process of writing and using lemmas in more detail.