Update VERIFICATION.md (#2337)

* VERIFICATION.md: update docs

* VERIFICATION.md: add legacy debugger mention

* Set Version: 1.0.486

* Apply suggestions from code review

Co-authored-by: Palina Tolmach <[email protected]>

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>

Author: 3 people

VERIFICATION.md

@@ -1,13 +1,15 @@
 Verification Instructions for KEVM
 ==================================
 
+If you're trying to analyze Solidity smart contracts with symbolic execution, check out our guide for Kontrol at [docs.runtimeverification.com/kontrol].
+
 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
--------------------
+Example: Sum to N
+-----------------
 
 Have a look at the [sum-to-n-spec.k] file.
 It has two modules:
@@ -18,95 +20,52 @@ It has two modules:
 The first step is kompiling the `.k` file with the below command.
 
 ```sh
-kevm kompile-spec sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile-spec sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --output-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.
+  - `--output-definition sum-to-n-spec/haskell`: the path where the kompiled definition is stored.
 
 Next, run the prover with:
 
 ```sh
-kevm prove sum-to-n-spec.k --definition sum-to-n-spec/haskell
+kevm prove-legacy 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.
-
-```sh
-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.
+Debugging a proof
+-----------------
 
-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`.
+For `kevm prove-legacy`, you can use the `--debugger` flag to debug a proof. With it, you can use `step`/`stepf` to navigate through the rewrite steps and `konfig` to display the K configuration. You can see all the available commands using `help`.
 
-Following this, we can compile the Markdown file with:
-
-```sh
-kevm kompile-spec erc20-spec.md --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
-```
-
-Next, run the prover with:
-
-```sh
-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:
-
-```sh
-kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k --definition tests/specs/erc20/verification/haskell
-```
-
-You can also debug proofs interactively:
-
-```sh
-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.
+For `kevm prove`, you can use `kevm show-kcfg ...` or `kevm view-kcfg ...` to get a visualization.
+***Note:*** this is not compatible with `kevm prove-legacy`.
 
 `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_file` is the file to look in for specifications. This is the same file that is used for `kevm prove …`.
+  - `--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` lets you select an individual claim out of the `spec_file`. If the flag is ommited, it’s assumed that only one claim is present. If the flag is ommited and more than one claim is present in the `spec_file` then an error will be raised.
   - `--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](https://github.com/Textualize/textual/blob/main/FAQ.md#how-can-i-select-and-copy-text-in-a-textual-app) for more information.
 
+`kevm show-kcfg [spec_file] [--save-directory save_directory] [--claim claim_label] ...` command is pretty similar, but prints out the K Control Flow Graph to `stdout` instead.
+
 A running example:
 
 ```sh
 mkdir kcfgs
-kevm kompile-spec tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm kompile-spec tests/specs/benchmarks/verification.k --output-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
+kevm view-kcfg tests/specs/benchmarks/address00-spec.k --save-directory kcfgs --definition tests/specs/benchmarks/verification/haskell
 ```
 
 [sum-to-n-spec.k]: <./tests/specs/examples/sum-to-n-spec.k>
-[erc20-spec.md]: <./tests/specs/examples/erc20-spec.md>
-[ERC20.sol]: <./tests/specs/examples/ERC20.sol>
 [K tutorial]: <https://github.com/runtimeverification/k/tree/master/k-distribution/k-tutorial>
 [more about it here]: <https://github.com/runtimeverification/k/tree/master/k-distribution/k-tutorial/1_basic/20_backends#k-backends>
+[docs.runtimeverification.com/kontrol]: <https://docs.runtimeverification.com/kontrol/>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.485"
+version = "1.0.486"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.485'
+VERSION: Final = '1.0.486'

package/version

@@ -1 +1 @@
-1.0.485
+1.0.486