Move VERIFICATION.md in examples/README.md (#2344)

* examples/README.md: move VERIFICATION.md

* README.md: typo

* Set Version: 1.0.492

* Update tests/specs/examples/README.md

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

* Set Version: 1.0.494

---------

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

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.493"
+version = "1.0.494"
 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.493'
+VERSION: Final = '1.0.494'

package/version

@@ -1 +1 @@
-1.0.493
+1.0.494

VERIFICATION.md → tests/specs/examples/README.md

@@ -3,10 +3,7 @@ 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.
+This folder contains instructions for kompiling and running claims using KEVM to help you start proving.
 
 Example: Sum to N
 -----------------
@@ -41,22 +38,29 @@ The expected output is `#Top` which represents that all the claims have been pro
 Debugging a proof
 -----------------
 
-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`.
+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`.
 
 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 is the same file that is used for `kevm prove …`.
+  - `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.
+  - `--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.
+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/docs/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:
+A running example (starting from the root of the repository):
 
 ```sh
 mkdir kcfgs
@@ -65,7 +69,7 @@ kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benc
 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>
+[sum-to-n-spec.k]: <./sum-to-n-spec.k>
 [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/>