Kontrol updates April 4t, 2024

Today, we are introducing a new way to bring updates!

From now on, we will publish weekly updates and each week, we will dive into different topics and tools!

Let’s start with Kontrol:

• Added proof execution time to the output of `kontrol prove`: we now record how long it took each proof to execute and show this information in the default output of `kontrol prove` as well as `kontrol view`.
• Implemented `hevm` success predicate in addition to the `foundry_success` one that is used by default. It can be enabled by an ` — hevm` option available in `kontrol prove`. According to this success predicate, only failed `assert` and `DSTest` assert expressions constitute a test failure, as opposed to `foundry` success predicate that includes revert into the list of failure reasons. The details are available at https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/hevm.md.
• Updated UX for `kontrol view-kcfg` and `kontrol show` commands. Now, the latest proof is loaded by default if no ` — version` option is provided, and a warning message is displayed. In addition, to assist the user, we refactored an error message that is shown if there are multiple proofs that can be selected — we now print the names of all available proofs for the user to select and copy one of them.
• Based on user feedback, we refactored NatSpec tags for dynamically sized arguments in functions: now, the number of elements in the `vaults` array can be specified as `/// @custom:kontrol-array-length-equals vaults: 4`, and the length of `bytes vaultData` — as ` /// @custom:kontrol-bytes-length-equals vaultData: 256`.
• Implemented `kontrol split-node` command, which allows manually splitting a node on a user-provided branching condition. This feature is useful, for example, for introducing assumptions without having to restart a proof, by splitting a node on the assumption and then refuting (i.e., delaying the execution of) the negative branch.
• Added JUnit XML report generation for `kontrol prove` results. A report is generated if `kontrol prove` is ran with ` — xml-report` option. This feature is aimed at providing more advanced result and test reporting and is particularly useful when running Kontrol in CI, as JUnit XML reports are widely used in CI tools.
• Added ` — cse` flag for `kontrol prove` that enables compositional symbolic execution. With this option, when Kontrol executes a function `a()` that calls another function `b()`, it will first execute `b()` and build a summary for it. It will then re-use this summary when `b()` is called within `a()` or any other function instead of re-executing it every time.
• To facilitate debugging with Simbolik, we introduced ` — with-non-general-state` option to `kontrol prove`. By default, when `kontrol prove` is ran on a non-test (e.g., a function that does not start with `test`, `prove`, or `check`), the initial state is kept largely symbolic to allow for symbolic exploration of all possible behaviors. With this option, initial state has a similar configuration that Kontrol uses when executing symbolic tests and is, therefore, less general.

That’s all for this week’s updates on Kontrol! We will be back next week with more updates for ERCx

If you have questions about Kontrol or other topics, you can talk directly with our team in Discord.