# KEVM Lemmas

How to debug your KCFG and find KEVM reasoning gaps

In this section, we will verify Solady's `mulWad`

function, demonstrating how to identify and write good lemmas.

The reasoning engine behind **Kontrol** is the **K** framework, which is accessed through the **K** definition of the EVM semantics, **KEVM**. Sometimes it is necessary to address reasoning gaps or suggest simplification strategies at the **KEVM** level. To gain a better understanding of the definitions and rules involved in expressions that are not being simplified as desired, you can explore the **KEVM** repository.

## Verifying Solady's `mulWad`

`mulWad`

Note: `WAD = 10**18`

For this example, we'll verify Solady's `mulWad`

function, defined as:

Our goal is to demonstrate that this is equivalent to `(x * y) / WAD`

for any two integers `x`

and `y`

. To achieve this, we define the following property test:

This property test asserts that if the product `x*y`

does not result in an overflow, *or* if `y`

is zero, then output of `mulWad(x, y)`

should be equal to `(x*y)/WAD`

. However, if an overflow occurs, the function `mulWad`

should revert.

After symbolically executing this test, the generated message indicates that **Kontrol** was unable to prove that the property holds for all possible inputs. This output will look like the following:

Our next step is to inspect the **KCFG** (`kontrol view-kcfg`

) to understand which path condition is leading to node 23. To learn more about the **KCFG:** K Control Flow Graph (KCFG)

## Identifying branching conditions

When we inspect the branching condition that leads to the failing node, we can see that it corresponds to the `if`

statement of the `mulWad`

function.

Let's unparse the branching condition. The condition is:

Taking into account that `chop(x)`

is `(x)mod[2**256]`

, we can write the expression in a more palatable way:

There are three main things to know about this condition.

The operands

`*Int`

,`<Int`

,`modInt`

,`/Int`

, and`==Int`

are**K**functions doing the obvious thing, with the suffix`Int`

indicating the type of their argumentsThe function

`bool2Word`

takes a boolean value and converts it into an EVM word. Particularly, it converts`true`

to`1`

and`false`

to`0`

. You can find the definition here.The modulo operation appears because, inside assembly blocks, the Solidity compiler doesn't insert overflow checks

Thus, the condition is equivalent to `y == 0 || types(uint256).max / y >= x`

. Now, since this is the condition to branch on the first `if`

of the `mulWad`

function, **Kontrol** will explore the two different branches, one asserting that `(y *Int bool2Word((maxUInt256 /Int y) <Int x)) modInt 2**256 ==Int 0`

holds, and another one asserting that the opposite holds (via the `notBool`

operator).

The branch starting on node 21 explores the path of negating `(y *Int bool2Word((maxUInt256 /Int y) <Int x)) modInt 2**256 ==Int 0`

. That is, entering the `if`

statement, which is why we see that node 23 has `statusCode: EVMC_REVERT`

.

## Dealing with path constraints

Having a node with a status code `EVMC_REVERT`

can mean that either there's a bug and that revert should not be happening, or that the branch is unfeasible but **Kontrol** did not realize it. Let's look at the path conditions of node 21 to see if a contradiction can be derived.

If we look a the first condition and the ones at the end, we can spot something suspicious. Let's inspect the following conditions:

`#Not ( { VV1_y_114b9705:Int #Equals 0 } )`

`{ VV0_x_114b9705:Int <=Int ( maxUInt256 /Int VV1_y_114b9705:Int ) #Equals true }`

`( notBool chop ( ( VV1_y_114b9705:Int *Int bool2Word ( ( maxUInt256 /Int VV1_y_114b9705:Int ) <Int VV0_x_114b9705:Int ) ) ) ==Int 0 )`

After renaming the Matching Logic operators and other syntactic noise, the three conditions are

`y != 0`

`x <= maxUInt256 / y`

`y * bool2Word(maxUInt256 / y < x)) != 0`

Given these constraints, we can see how 1 and 2 imply that condition 3 is false. Thus we're not facing a bug in `mulWad`

, but rather a reasoning gap in Kontrol.

## Bridging the (reasoning) gap

**Kontrol** is able to infer `maxUInt256 / y < x = false`

from conditions 1 and 2, and a quick `git grep -rin 'rule bool2Word'`

in the evm-semantics definition tells us that these are the defined rewrite rules for `bool2Word`

:

Knowing the existing rules for any function is important since this means knowing how the function is treated by **KEVM** and thus by **Kontrol**.

Note that none of those rules is telling **Kontrol** (actually, **KEVM**) to attempt to simplify the boolean arguments of `bool2Word`

. Because none of these rules really apply to condition 3, no simplification is made. This is why **Kontrol** derives no contradiction from condition 3 above, it's treating that expression as purely symbolic. To tell **Kontrol** to attempt to simplify the boolean arguments of the `bool2Word`

function, we need to add the following rules to the file described in the last section

Now **Kontrol** will attempt to simplify `X`

to `true`

or `false`

in order to apply any of these two new rules. Indeed, if we run again our property test with these added rules, the proof will pass.

## Finishing an existing proof

We've identified the missing reasoning link, great! To include our brand new lemmas in the **KEVM** definition (i.e., make them available for **Kontrol** to reason with) we need to rekompile the project, that is, building it again with the `--rekompile`

flag (`kontrol build --rekompile --require ${path_to_lemmas} --module-import ${module}`

). After this, re-running the proof with the `--reinit`

flag will attempt (and succeed) to prove our property from scratch. But what if we don't want to spend more computational resources than necessary to finish the proof from where we left it? That is, what if don't want to explore those branches that we have already explored and know are not problematic? Enter **KCFG** manipulation.

### Node pruning

From the screenshots above we know that the branch starting at node 21 should be pruned by **Kontrol** itself. However, due to the lack of reasoning arguments, it was not able to do so. Now that we've endowed **Kontrol** with the necessary weaponry, all we have to do is remove the reverting node, node 23, and restart the proof * without* the

`--reinit`

flag to let **Kontrol**resume the proof without the reverting node, and figure out that such an execution branch will never be traversed.

To remove the reverting node we can run the following command

Note that `FixedPointMathLibVerification`

is the contract where our property test lives.

With the node pruned, our configuration will look like this

#### Resuming execution

After this, we can resume the proof without the `--reinit`

flag

Indeed, after allowing **Kontrol** to reason again about the reverting branch, we're greeted with the following message

Last updated