# KEVM Lemmas In this section, we will verify [Solady's](https://github.com/Vectorized/solady) `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](https://github.com/runtimeverification/evm-semantics). ## Verifying Solady's `mulWad` {% hint style="info" %} Note: `WAD = 10**18` {% endhint %} For this example, we'll verify Solady's [`mulWad`](https://github.com/Vectorized/solady/blob/16c0dda5838fbb1350a0735dffa564b0b0a11e7e/src/utils/FixedPointMathLib.sol#L54)function, defined as: ```solidity function mulWad(uint256 x, uint256 y) internal pure returns (uint256 z) { assembly { if mul(y, gt(x, div(not(0), y))) { mstore(0x00, 0xbac65e5b) revert(0x1c, 0x04) } z := div(mul(x, y), WAD) } } ``` 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: ```solidity // Public wrapper for `FixedPointMathLib.mulWad` to ensure that `vm.expectRevert` works well function mulWad(uint x, uint y) public pure returns (uint256) { return FixedPointMathLib.mulWad(x, y); } function testMulWad(uint256 x, uint256 y) public { if (y == 0 || x <= type(uint256).max / y) { uint256 zSpec = (x * y) / WAD; uint256 zImpl = FixedPointMathLib.mulWad(x, y); assert(zImpl == zSpec); } else { vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); this.mulWad(x, y); } } ``` 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: {% code fullWidth="true" %} ```bash 1 Failure nodes. (0 pending and 1 failing) Failing nodes: Node id: 23 Failure reason: Implication check failed, the following is the remaining implication: ( ( #Not ( { VV1_y_114b9705:Int #Equals 0 } ) #And ( { true #Equals 0 <=Int CALLER_ID:Int } #And ( { true #Equals 0 <=Int ORIGIN_ID:Int } #And ( { true #Equals 0 <=Int NUMBER_CELL:Int } #And ( { true #Equals 0 <=Int VV0_x_114b9705:Int } #And ( { true #Equals 0 <=Int VV1_y_114b9705:Int } #And ( { true #Equals CALLER_ID:Int

Branching condition leading to failing node

Let's unparse the branching condition. The condition is: {% code overflow="wrap" fullWidth="true" %} ```bash chop ( ( VV1_y_114b9705:Int *Int bool2Word ( ( maxUInt256 /Int VV1_y_114b9705:Int) = 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)

Path conditions (constraints) of node 21

If we look a the first condition and the ones at the end, we can spot something suspicious. Let's inspect the following conditions: 1. `#Not ( { VV1_y_114b9705:Int #Equals 0 } )` 2. `{ VV0_x_114b9705:Int <=Int ( maxUInt256 /Int VV1_y_114b9705:Int ) #Equals true }` 3. `( notBool chop ( ( VV1_y_114b9705:Int *Int bool2Word ( ( maxUInt256 /Int VV1_y_114b9705:Int ) 1 evm-types.md:33: rule bool2Word( false ) => 0 lemmas/lemmas.k:50: rule bool2Word(A) |Int bool2Word(B) => bool2Word(A orBool B) [simplification] lemmas/lemmas.k:51: rule bool2Word(A) &Int bool2Word(B) => bool2Word(A andBool B) [simplification] lemmas/lemmas.k:56: rule bool2Word(_B) |Int 1 => 1 [simplification] lemmas/lemmas.k:57: rule bool2Word( B) &Int 1 => bool2Word(B) [simplification] lemmas/lemmas.k:174: rule bool2Word(X ==Int 1) => X requires #rangeBool(X) [simplification] lemmas/lemmas.k:178: rule bool2Word( B:Bool ) ==Int I => B ==K word2Bool(I) [simplification, concrete(I)] ``` {% endcode %} 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 ```bash rule bool2Word ( X ) => 1 requires X [simplification] rule bool2Word ( X ) => 0 requires notBool X [simplification] ``` 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 ```bash kontrol remove-node FixedPointMathLibVerification.testMulWad 23 ``` Note that `FixedPointMathLibVerification` is the contract where our property test lives. With the node pruned, our configuration will look like this

KCFG after removing the reverting node 23

#### Resuming execution After this, we can resume the proof without the `--reinit` flag ```bash kontrol prove --test FixedPointMathLibVerification.testMulWad ``` Indeed, after allowing **Kontrol** to reason again about the reverting branch, we're greeted with the following message ```bash PROOF PASSED: FixedPointMathLibVerification.testMulWad(uint256,uint256):0 ```