# Property Verification using Kontrol ## Add new code Open the `Counter.sol` file located at `kontrolexample/src/Counter.sol`. The generated contract `Counter` has a public value named `number` that can be incremented using the method `increment()` , or can be set to a specific value using `setNumber(uint256)`. Let's modify the code to include a special case in which `setNumber` would not update the `number` value and will throw an error instead. This will cause the code's symbolic execution to branch. First, before the `Counter` contract declaration, declare an error by adding `error CoffeeBreak()`. Then, in the `setNumber()` function, add an argument `inLuck` as a `bool`. Lastly, add an `if` statement to define when a coffee break is allowed. We'll specify that a coffee break is permitted if `newNumber` is `0xC0FFEE` and `inLuck` is `true`. In that case, the function reverts and the number is not updated. With those changes, `Counter.sol` should look something like this: ```solidity // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; error CoffeeBreak(); contract Counter { uint256 public number; function setNumber(uint256 newNumber, bool inLuck) public { number = newNumber; if (newNumber == 0xC0FFEE && inLuck == true) { revert CoffeeBreak(); } } function increment() public { number++; } } ``` Let's look at what we have. The `setNumber` method will update our only storage variable with the passed value, *except* when `newNumber` is `0xC0FFEE` **and** the `bool` variable is `true`. Now let's write a test for the contract in `kontrolexample/test/Counter.t.sol` ```solidity // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; import {Test, console} from "forge-std/Test.sol"; import {Counter} from "../src/Counter.sol"; contract CounterTest is Test { Counter public counter; function setUp() public { counter = new Counter(); counter.setNumber(0, false); } function testIncrement() public { counter.increment(); assert(counter.number() == 1); } function testFuzz_SetNumber(uint256 x, bool inLuck) public { counter.setNumber(x, inLuck); assert(counter.number() == x); } } ``` Run the following command to run this test: ```bash forge test --match-test testFuzz_SetNumber ``` This should pass almost every time. Note that the test command will automatically build the project as well. Whether the test passes or not depends on the random inputs generated by `forge`. If `forge` generates the input `x = 0xC0FFEE, inLuck = true`, then the test will fail. Otherwise, it will pass. The point is that there is one case where the property (`setNumber` updates the storage) doesn't hold, but `forge` won't catch it unless it happens to randomly generate this specific input. Next, we will demonstrate Property Verification using **Kontrol**, and show how it allows us to catch errors like this that `forge` might miss. ## Building the project with Kontrol Let's build your Foundry project with **Kontrol**. Our tool compiles the source and test files with `forge build` under the hood, so there's no need to call it explicitly. After compilation, it inspects the artifacts generated by `solc` and produces **KEVM** helper modules containing information for each Solidity contract found. Each helper module contains productions and rules for ABI properties and bytecode. If you are curious, you can view the `out/kompiled/foundry.k` file. To get started, run the command below: ```sh kontrol build ``` {% hint style="warning" %} When ran for the first time, this process should take a minute, so don't worry. Also, remember that during the development, you may need to rebuild the definition in various ways. {% endhint %} ```bash kontrol build --help ``` Once you have built the definition, you can run tests symbolically. In this case remember we are expecting the test to **fail**. The proof should **fail** after running for about 1 minute on a modern laptop. {% hint style="info" %} The time it takes to run can vary depending on the machine. If it appears to be stalling, you can add `--verbose` to see what is happening. {% endhint %} To run the tests use the following: ```bash kontrol prove --match-test CounterTest.testFuzz_SetNumber ``` The `--match-test CounterTest.testFuzz_SetNumber` flag is used to specify that only proofs that match the name `CounterTest.testFuzz_SetNumber` will execute. In this case, there is a single proof. However, if you were to pass `CounterTest.test`, **Kontrol** would prove any function in `CounterTest` that is prefixed with `test`. You can find more information on **Kontrol** commands on the [kontrol-cheatsheet](https://docs.runtimeverification.com/kontrol/cheatsheets/kontrol-cheatsheet "mention"). {% hint style="info" %} By default, gas computation is disabled. To activate it, use the `--use-gas` flag when executing the `prove` command. {% endhint %} Now, you can see the status of all the proofs by running the following command: ```bash kontrol list ``` In the output, you will see two proofs: one for the `setUp` function and one for `testFuzz_SetNumber`, the function you just proved! You will see something similar to the screenshot below.

List of Proofs

## Using a Cheatcode Now, let's make the proof more general using cheatcodes. Since the `Counter` contract is deployed in the `setUp` function, its storage will be empty when the `testFuzz_SetNumber` function executes. We can use the `vm.setArbitraryStorage(address)` cheatcode to make the storage of an address symbolic. This allows us to abstract the storage and assume that any storage variable in the contract can have any possible value, not just the ones assigned during initialization. The cheatcode is supported both by Foundry and Kontrol, so you can use it without importing the include the `kontrol-cheatcode` library. However, for illustration purposes, we will do it here. Your `Counter.t.sol` will then look like this: ```solidity // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; import {Test, console} from "forge-std/Test.sol"; import {Counter} from "../src/Counter.sol"; import {KontrolCheats} from "kontrol-cheatcodes/KontrolCheats.sol"; contract CounterTest is Test, KontrolCheats { Counter public counter; function setUp() public { counter = new Counter(); counter.setNumber(0, false); } function testIncrement() public { counter.increment(); assert(counter.number() == 1); } function testFuzz_SetNumber(uint256 x, bool inLuck) public { vm.setArbitraryStorage(address(counter)); counter.setNumber(x, inLuck); assert(counter.number() == x); } } ``` {% hint style="info" %} Cheatcodes that are only supported by Kontrol need to be called from the `kevm` (not `vm`) contract. One example of that is `kevm.setSymbolicStorage(address)`—a Kontrol-specific analog of `vm.setArbitraryStorage(address)`. The list of supported cheatcodes is available on the [Cheatcodes](https://docs.runtimeverification.com/kontrol/cheatsheets/cheatcodes) page. {% endhint %} To rerun the proof with these changes, you need to run the following: ```bash kontrol build ``` This will re-run `forge build`, recompiling the updated files. Next you will need to run `prove` again. This time with the `--reinit` flag to ensure that you are verifying the latest version of the code. ```bash kontrol prove --match-test CounterTest.testFuzz_SetNumber --reinit ``` This will create a new version of the proof. You can run `kontrol list` again and you will see something similar to the screenshot below.

List of Proofs

Notice that the first proofs have `:0` and there are now proofs labeled `:1` this indicates the version of the proof. {% hint style="info" %} For more information on proofs check out [proof-management](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/proof-management "mention") {% endhint %} With the new proof generated let's check it out with the **Kontrol KCFG** visualizer. The visualizer allows you to analyze the state of the virtual machine at different points (nodes) during the symbolic execution. The main difference should be that the deployed `Counter` test now has symbolic storage instead of an empty Map. Next, we will cover how to read the **KCFG** visualizer and investigate **why** the test failed. --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://docs.runtimeverification.com/kontrol/guides/kontrol-example/property-verification-using-kontrol.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.