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:

// 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

// 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 testSetNumber(uint256 x, bool inLuck) public {
        counter.setNumber(x, inLuck);
        assert(counter.number() == x);
    }
}

Run the following command to run this test:

forge test --match-test testSetNumber

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:

kontrol build

The process should take a minute and may emit some warnings, so don’t worry. Also, remember that during the development, you may need to rebuild the definition in various ways.

If you change the Solidity code, you must re-run the kontrol build command. For more information about kontrol build, you can refer to kontrol build, Kontrol Build Options, or run:

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 3 minutes.

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.

To run the tests use the following:

kontrol prove --match-test CounterTest.testSetNumber

The --match-test CounterTest.testSetNumber flag is used to specify that only proofs that match the name CounterTest.testSetNumber 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.

By default, gas computation is disabled. To activate it, use the --use-gas flag when executing the prove command.

Now, you can see the status of all the proofs by running the following command:

kontrol list

In the output, you will see two proofs: one for the setUp function and one for testSetNumber, the function you just proved! You will see something similar to the screenshot below.

List of Proofs

Using a Kontrol 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 testSetNumber function executes. We can use the kevm.symbolicStorage(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.

To add the cheatcode, we need to include the kontrol-cheatcode library and inherit the contract. Your Counter.t.sol should look like this:

// 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 testSetNumber(uint256 x, bool inLuck) public {
        kevm.symbolicStorage(address(counter));
        counter.setNumber(x, inLuck);
        assert(counter.number() == x);
    }
}

To rerun the proof with these changes, you need to run the following:

kontrol build --regen --rekompile

This will regenerate and rekompile foundry.k. Next you will need to run prove again. This time with the --reinit flag.

kontrol prove --match-test CounterTest.testSetNumber --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.

For more information on proofs check out Proof Management

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.