Verification Instructions for KEVM
+
We assume that KEVM is installed, and the K tutorial 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.
+
Example 1: Sum to N
+
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.
+
kevm kompile-spec sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+
+
In this example, the arguments used are:
+
+--target haskell: specify which symbolic backend to use for reasoning.--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:
+
kevm prove sum-to-n-spec.k --definition sum-to-n-spec/haskell
+
+
The expected output is #Top which represents that all the claims have been proven.
+
Example 2: Faulty ERC20
+
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.
+
kevm solc-to-k ERC20.sol ERC20 --main-module ERC20-VERIFICATION > erc20-bin-runtime.k
+
+
+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:
+
kevm kompile-spec erc20-spec.md --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
+
+
Next, run the prover with:
+
kevm prove erc20-spec.md --definition erc20-spec/haskell --claim ERC20-SPEC.decimals
+
+
Here, --claim tells the prover to run only the decimals spec from the ERC20-SPEC module.
+
More to know
+
To prove one of the specifications:
+
kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k --definition tests/specs/erc20/verification/haskell
+
+
You can also debug proofs interactively:
+
kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k --definition tests/specs/erc20/verification/haskell --debugger
+
+
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 ... 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 --save-directory save_directory ...--claim claim_label option is added, but unlike the kevm prove ..., 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.
+
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 Textualize documentation for more information.
+
A running example:
+
mkdir kcfgs
+kevm kompile-spec tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --verbose --save-directory kcfgs
+kevm view-kcfg --verbose kcfgs tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell
+
+