KEVM Verification
Last updated
Last updated
We assume that KEVM is installed, and the has been completed. This document provides instructions for kompiling and running claims using KEVM.
In tests/specs/examples, you can find a few examples to get you started on proving with KEVM.
Have a look at the sum-to-n-spec.k file. It has two modules:
VERIFICATION - containing the EVM program and a few simplification rules.
SUM-TO-N-SPEC - containing the claims which will be executed.
The first step is kompiling the .k file with the below command.
In this example, the arguments used are:
—-pyk: a flag that enables the pyk library.
—-backend haskell: used to kompile the definition with the Haskell backend, enabling the symbolic execution ().
--syntax-module VERIFICATION: explicitly state the syntax module.
--main-module VERIFICATION: explicitly state the main module.
--definition sum-to-n-spec/haskell: the path where the kompiled definition is stored.
Next, run the prover with:
The expected output is #Top which represents that all the claims have been proven.
This example will describe the process of running claims for an ERC20 contract. Have a look at erc20-spec.md. It contains claims for a few basic ERC20 properties and the helper modules required to run the proofs. The ERC20 Solidity contract that is tested is ERC20.sol.
In this example, we rely on a helper module, ERC20-VERIFICATION, which must be generated from the ERC20.sol Solidity contract. The module is generated using the following solc-to-k command.
solc-to-k will parse a Solidity contract and generate a helper K module.
--main-module is used to set the name of the module.
The generated erc20-bin-runtime.k file contains K rules and productions for the contract’s bytecode, storage indexes for the state variables, and function selectors, among others. These rules are then used in the claims. As an example, the #binRuntime(ERC20) production, which is found in the <program> cell, will rewrite to #parseByteStack (contractBytecode), parsing the hexadecimal string into a ByteStack.
Following this, we can compile the Markdown file with:
Next, run the prover with:
Here, --claim tells the prover to run only the decimals spec from the ERC20-SPEC module.
To prove one of the specifications:
You can also debug proofs interactively:
In addition to this, you can use kevm show-kcfg ... or kevm view-kcfg ... to get a visualization.
kevm view-kcfg [spec_file] [--save-directory save_directory] [--claim claim_label] ... command takes the same basic arguments as kevm prove --pyk ... does, including:
spec_file is the file to look in for specifications. This file is read like with kevm prove —pyk …; the KProve.get_claims invokes the frontend.
--save_directory must be passed as where the KCFGs have been saved (by a previous call to kevm prove --pyk --save-directory save_directory ...
--claim claim_label option is added, but unlike the kevm prove --pyk ..., you can only repeat it once. This option lets you select an individual claim out of the spec_file; if not supplied, it’s assumed that only one spec is present.
--spec-module spec_module is also an inherited option.
A running example:
The interactive KCFG (view-kcfg) puts your terminal in application mode. To select text in this mode, hold the modifier key provided by your terminal emulator (typically SHIFT or OPTION) while clicking and dragging. Refer to the for more information.