| description |
|---|
Cheatsheet with (almost) all Kontrol options and gotchas |
This cheatsheet provides a comprehensive list of options for conducting Kontrol verification of smart contracts, along with additional information about the K ecosystem.
These commands encompass all the functionality involved in the verification process, from building your project into a full-fledged K definition to examining the verification output of a symbolic run in detail.
| Command | Description | Example |
|---|---|---|
build | Make K definitions from a Foundry project | kontrol build |
prove | Symbolically execute provided tests | kontrol prove --test TestContract.testName |
list | List all proof files with their status | kontrol list |
show | Statically print a proof | kontrol show ContractTest.testName |
view-kcfg | Show a proof in the KCFG visualizer | kontrol view-kcfg ContractTest.testName |
You can extensively customize the above commands to meet your specific verification requirements using the following flags.
Make K definitions from a Foundry project with build.
There are flags available for the build stage that allow you to change the set of lemmas used for reasoning and specify the desired behavior for rebuilding or re-executing symbolic tests.
| Flag | Description |
|---|---|
--verbose | Verbose build trace |
--require $lemmas | Include a file of $lemmas when forming the K definition |
--module-import $module | A Note: |
--rekompile | Will rebuild the K definition, even if it was previously built |
Let's look at what a typical kontrol build example may look like. You will likely have the following contents:
| Content | File Name | File Path |
|---|---|---|
| Custom Lemma | myproject-lemmas.k |
test/myproject-lemmas.k |
| A module you want Kontrol to include in its reasoning | MYPROJECT-LEMMAS |
test/myproject-lemmas.k |
| Symbolic properties | MyProperties |
For this example, we will assume that you have already run kontrol build once and this is not your first time symbolically executing the properties. You have also identified the necessary lemmas and included them in MYPROJECT-LEMMAS.
To symbolically execute your properties using the fastest available backend (booster backend), you will need to rekompile the K definition of the project. To do this your command will look like this:
kontrol build --require test/myproject-lemmas.k \
--module-import MyProperties:MYPROJECT-LEMMAS \
--rekompileSymbolically execute provided tests with prove.
These flags specify what you prove and how you prove it. The flags include: the backend used for symbolic execution, the new lemmas to include for symbolic reasoning, resource distribute and other potential changes.
| Flag | Description |
|---|---|
--test $testName | Specifies the name of the test function to symbolically execute. Multiple flags can be provided for parallel execution with different functions. |
--reinit | Restarts symbolic execution instead of resuming from the last saved run. |
--bmc-depth $n | Enables bounded model checking, unrolling all loops to a maximum depth of $n . |
--use-booster | Uses the booster backend (faster) instead of the legacy backend. |
--smt-timeout $ms | Sets the timeout in milliseconds for SMT queries. |
--smt-retry-limit $n | Specifies the number of times to retry SMT queries with scaling timeouts. |
--smt-tactic $smt_tactic | Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt) |
--auto-abstract-gas | Abstract any gas-related computations, provided the cheatcode infiniteGas was enabled. This simplifies and speeds up symbolic execution. |
--no-break-on-calls | Does not store a node for every EVM call made. |
--workers $n | Sets the number of parallel processes run by the prover. It should be at most (M - 8) / 8 in a machine with M GB of RAM. |
--max-depth $n | Sets the maximum number of K steps before the state is saved in a new node in the KCFG. |
--max-iterations $n | Sets the number of times to expand the next pending node in the KCFG. |
--bug-report $name | Generates a bug report with the given name. |
--counterexample-information | Generates and shows the counterexample, which refers to the test parameter values that lead to a failing test. |
--fail-fast | Stop execution on other branches if a failing node is detected. |
Let's look at what a typical kontrol prove example may look like. For this example we will assume the following scenario:
- There are two symbolic properties to execute in parallel.
testMyProperty1testMyProperty2- Both are in a contract named
MyProperties
- There are loops present in the code, and before providing invariants for those we want to use the simpler approach of bounded model checking, unrolling the loops only up to 10 iterations
- We want to allow the SMT solver enough time to reason
- We want to achieve maximum speed of symbolic execution. This is possible with the following tweaks:
- Don't allocate any resources to gas computations, since these are costly and can cause numerous branching
- Create as few nodes as possible, since this saves on writing time. In particular, don't produce any nodes when making EVM calls
- Use the fastest symbolic execution backend available, the booster backend
The command to execute testMyProperty1 and testMyProperty2, with that set of characteristics is the following:
{% code overflow="wrap" fullWidth="false" %}
kontrol prove --test MyProperties.testMyProperty1 \
--test MyProperties.testMyProperty2 \
--bmc-depth 10 \
--smt-timeout 10000 \
--auto-abstract-gas \
--no-break-on-calls \
--workers 2 \
--use-booster{% endcode %}
To make use of for all kontrol options, it is recommended you use a bash script that simplifies parameter tweaking and allows for a better verification experience. It is also recommended you save the output of running kontrol to a file for easier inspection and debugging.
Here is a template to have better control over kontrol. To save the output of running a template run-kontrol.sh to log.out , from the root directory of a Foundry project, you can use the following command:
time bash test/run-kontrol.sh 2>&1 | tee log.outTo interpret the result of running this script, please refer to k-control-flow-graph-kcfg.md.
#!/bin/bash
set -euxo pipefail
kontrol_build() {
kontrol build \
--verbose \
--require ${lemmas} \
--module-import ${module} \
${rekompile} \
${llvm_library}
}
kontrol_prove() {
kontrol prove \
--max-depth ${max_depth} \
--max-iterations ${max_iterations} \
--smt-timeout ${smt_timeout} \
--bmc-depth ${bmc_depth} \
--workers ${workers} \
${reinit} \
${bug_report} \
${break_on_calls} \
${auto_abstract} \
${tests} \
${use_booster}
}
###
# kontrol build options
###
lemmas=test/myproject-lemmas.k
base_module=MYPROJECT-LEMMAS
module=MyProperties:${base_module}
rekompile=--rekompile
#rekompile=
###
# kontrol prove options
###
max_depth=10000
max_iterations=10000
smt_timeout=100000
bmc_depth=10
workers=2
reinit=--reinit
reinit=
break_on_calls=--no-break-on-calls
# break_on_calls=
auto_abstract=--auto-abstract-gas
# auto_abstract=
bug_report=--bug-report
#bug_report=
use_booster=--use-booster
# use_booster=
# List of tests to symbolically execute
tests=""
tests+="--test MyProperties.testMyProperty1 "
tests+="--test MyProperties.testMyProperty2 "
pkill kore-rpc || true
kontrol_build
kontrol_prove