|
1 | | -Foundry Specifications |
2 | | -====================== |
| 1 | +#[Kontrol documentation](https://docs.runtimeverification.com/kontrol). |
3 | 2 |
|
4 | | -**ACTIVE DEVELOPMENT** |
| 3 | +The documentation below may become deprecated. The documentation at the link above will be continuously updated and improved. |
5 | 4 |
|
6 | | -The Foundry integration allows users to take Solidity property tests and generate K specifications which can be executed using the Haskell symbolic backend. |
7 | | - |
8 | | -Before executing any of the KEVM instructions, make sure that you have the following: |
9 | | - 1. Successfully built or installed KEVM, |
10 | | - 2. The`kevm` binary is on your PATH, |
11 | | - 3. Activated the virtual environment (*applicable only for builds from source*). |
12 | | - |
13 | | -Below we are providing an example usage and a description of all the commands you can use with KEVM to improve your experience. |
14 | | - |
15 | | -Available Commands |
16 | | ------------------- |
17 | | - |
18 | | -Basic commands are (and each can be passed `--help`): |
19 | | - |
20 | | -- `kevm foundry-kompile`: Kompile a definition, generating claims for each Foundry test. |
21 | | - The best options are: |
22 | | - - `--regen` - needed if Solidity sources change, |
23 | | - - `--rekompile` - needed if K lemmas change, or K definition changes, |
24 | | - - `--require` - for adding an extra K file with lemmas, |
25 | | - - `--module-import` - importing an extra K module in one of the added K files with lemmas. |
26 | | - |
27 | | -- `kevm foundry-prove`: Run a given proof using the KCFG-based prover (not supporting loops yet, need to fall back to typical K for that). |
28 | | - The best options are: |
29 | | - - `--reinit` - want to start over from scratch, |
30 | | - - `--no-simplify-init` - do not want to invoke simplification on all the original nodes, can be faster, |
31 | | - - `--max-depth` - increase the space between saved nodes; bigger is faster, |
32 | | - - `--max-iterations` - maximum number of nodes to store in KCFG before giving on attempting proof for that run, |
33 | | - - `--break-every-step` - save a state every opcode, slow, good for debugging, |
34 | | - - `--break-on-calls` - save a state every time a call is made, good to turn on. |
35 | | - - `--verbose` - output what the prover is doing to make sure it's making progress. |
36 | | - |
37 | | -- `kevm foundry-show`: Display the given KCFG so far as text. |
38 | | - Options are: |
39 | | - - `--no-minimize` - do not omit all the gory details, |
40 | | - - `--node` - can be a repeated option, display more information about a given node hash, |
41 | | - - `--node-delta` - displays the delta between two given nodes in the KCFG. |
42 | | - |
43 | | -- `kevm foundry-view-kcfg`: Launch the more interactive exploration of the KCFG (can be done while exploration is running, must Ctrl-C + relaunch to view updates to KCFG). |
44 | | - - The interactive 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. |
45 | | - |
46 | | -- `kevm foundry-section-edge`: Given an edge in the graph, cut it into sections to get intermediate nodes. |
47 | | - |
48 | | -- `kevm foundry-step-node`: Step from a given node, adding it to the CFG. |
49 | | - |
50 | | -- `kevm foundry-simplify-node`: Simplify a given node, and potentially replace it. |
51 | | - |
52 | | -Example Usage |
53 | | -------------- |
54 | | - |
55 | | -The first step is to ensure the Solidity codebase is compiled and the `out/` directory is generated. |
56 | | - |
57 | | -For example, in the root of this repository, you can run: |
58 | | - |
59 | | -*Build Foundry Project:* |
60 | | - |
61 | | -```sh |
62 | | -$ cd tests/foundry |
63 | | -$ forge build |
64 | | -``` |
65 | | - |
66 | | -*Kompile to generate K specifications:* |
67 | | - |
68 | | -```sh |
69 | | -$ kevm foundry-kompile |
70 | | -``` |
71 | | - |
72 | | -*And discharge some specific test as a proof obligation (inside virtual environment):* |
73 | | - |
74 | | -```sh |
75 | | -$ kevm foundry-prove --test AssertTest.test_assert_true |
76 | | -``` |
77 | | - |
78 | | -Foundry Module for KEVM |
79 | | ------------------------ |
| 5 | +Foundry Module for Kontrol |
| 6 | +-------------------------- |
80 | 7 |
|
81 | 8 | Foundry's testing framework provides a series of cheatcodes so that developers can specify what situation they want to test. |
82 | | -This file describes the KEVM specification of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass. |
| 9 | +This file describes the K semantics of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass. |
83 | 10 |
|
84 | 11 | ```k |
85 | 12 | requires "evm.md" |
@@ -145,9 +72,9 @@ Hence, checking if a `DSTest.assert*` has failed amounts to reading as a boolean |
145 | 72 | module FOUNDRY-SUCCESS |
146 | 73 | imports EVM |
147 | 74 |
|
148 | | - syntax Bool ::= |
| 75 | + syntax Bool ::= |
149 | 76 | "foundry_success" "(" |
150 | | - statusCode: StatusCode "," |
| 77 | + statusCode: StatusCode "," |
151 | 78 | failed: Int "," |
152 | 79 | revertExpected: Bool "," |
153 | 80 | opcodeExpected: Bool "," |
@@ -1019,8 +946,8 @@ With address: Asserts the topics match and that the emitting address matches. |
1019 | 946 | ``` |
1020 | 947 |
|
1021 | 948 |
|
1022 | | -Restricting the accounts that can be called in KEVM |
1023 | | ---------------------------------------------------- |
| 949 | +Restricting the accounts that can be called in Kontrol |
| 950 | +------------------------------------------------------ |
1024 | 951 |
|
1025 | 952 | A `StorageSlot` pair is formed from an address and a storage index. |
1026 | 953 |
|
|
0 commit comments