0xJayPi/secureum-kontrol

Secureum Workshop on Kontrol

This repository contains a project that will be used during a Secureum workshop on Kontrol. Contracts present in this repository are modified for educational purposes, please DO NOT use them in production.

Documentation

Documentation and installation instructions for Kontrol can be found in Kontrol Book. Source code for Kontol is available in Kontrol repository.

Workshop Instructions

Day Three — Introduction to Kontrol

The first workshop for Kontrol is focused on basic usage of its commands in application to WETH9 contract and the tests we have defined for it.

Build

To clone and build this project, run

git clone https://github.com/runtimeverification/secureum-kontrol.git && cd secureum-kontrol

followed by

kontrol build

This command will run forge build under the hood, and will, then, use the produced compilation artifacts to generate K definitions that can be verified. You can inspect the out/ folder to view the artifacts produced by kontrol build and make sure that it executed successfully.

Prove

To prove that WETH9 approve() function changes allowance correctly, you can run the following command:

kontrol prove --match-test 'WETH9Test.test_approve(address,address,uint256)'

The process should end successfully, indicating that this property is always true and, whatever the values of from, to, and amount are, approve() behaves correctly. The test being executed is as follows:

    function test_approve(address from, address to, uint256 amount) public {
        vm.prank(from);
        asset.approve(to, amount);

        uint256 toAllowance = asset.allowance(from, to);
        assert(toAllowance == amount);
    }

Day Four — Advanced Symbolic Testing with Kontrol

The second workshop for Kontrol will cover several aspects, including ERC4626 tests, addressing verification challenges such as loops and dynamically-sized Solidity types, and proving equivalence between Solidity and low-level gas optimized implementations for Solady.

Proving properties

In the first part of the workshop, the following commands would help build the project and run two tests for the ERC4626 implementation we are using:

kontrol build
kontrol prove --match-test test_totalAssets_doesNotRevert --match-test test_totalAssets_revertsWhenPaused -j2

The first test, checking if test_totalAssets_doesNotRevert never reverts, as requested by the EIP

    function test_totalAssets_doesNotRevert(address caller) public {
        _notBuiltinAddress(caller);
        vm.prank(caller); vault.totalAssets();
    }

will revert, since the implementation of the ERC4626 vault we are using here (for illustration purposes!) reverts if the contract has been paused.

Proving equivalence

Kontrol, and FV in general, can be used to assert equivalence between different implementations of smart contract functions. To prove that a highly optimized implementation of mulWad funciton in Solady is equivalent to a more readable Solidity version, run

kontrol build --require lemmas/eq-lemmas.k --module-import EquivalenceTest:EQ-LEMMAS

to build a project with lemmas that, as discussed in the workshop, are needed for the following test to succeed:

    function test_mulWad(uint256 x, uint256 y) public {
        if (y == 0 || x <= type(uint256).max / y) {
            uint256 zSpec = (x * y) / WAD;
            uint256 zImpl = mulWad(x, y);
            assert(zImpl == zSpec);
        } else {
            vm.expectRevert();
            this.mulWad(x, y);
        }
    }

Then, run

kontrol prove --match-test testMulWad --smt-solver 10000

Help

If you need any assistance, please reach out to us in a dedicated Secureum Discord channel or RV Discord.