# KEVM: Semantics of EVM in K ### Fast Installation * `bash <(curl https://kframework.org/install)`: install [kup package manager](https://github.com/runtimeverification/kup). * `kup install kevm`: install **KEVM**. * `kup list kevm`: list available **KEVM** versions. * `kup update kevm`: update to latest **KEVM** version. **NOTE**: The first run will take longer to fetch all the libraries and compile sources. (30m to 1h) ### Documentation/Support These may be useful for learning **KEVM** and **K** (newest to oldest): * [K, KEVM and Foundry Integration overview](https://www.youtube.com/watch?v=9PLnQStkiUo) * [Jello Paper](https://jellopaper.org), a nice presentation of this repository. * [20 minute tour of the semantics](https://www.youtube.com/watch?v=tIq_xECoicQNov) at [2017 Devcon3](https://archive.devcon.org/archive/watch?edition=3\&order=desc\&sort=edition). * [KEVM 1.0 technical report](http://hdl.handle.net/2142/97207), especially sections 3 and 5. * [KEVM Paper at CSF'18/FLoC](https://fsl.cs.illinois.edu/publications/hildenbrandt-saxena-zhu-rodrigues-daian-guth-moore-zhang-park-rosu-2018-csf). To get support for **KEVM**, please join our [Discord Channel](https://discord.com/invite/CurfmXNtbN). If you want to start proving with **KEVM**, refer to `VERIFICATION.md`. ### Building from source There are two backends of **K** available: LLVM for concrete execution and Haskell for symbolic execution. This repository generates the build-products for each backend in `.build/usr/lib/kevm`. #### System Dependencies First install the following tools: * [git](https://git-scm.com/) * GNU [Bison](https://www.gnu.org/software/bison/), [Flex](https://github.com/westes/flex), and [Autoconf](http://www.gnu.org/software/autoconf/). * GNU [libmpfr](https://www.mpfr.org/) and [libtool](https://www.gnu.org/software/libtool/). * [Z3](https://github.com/Z3Prover/z3) version 4.12.1 **Installing Z3** **KEVM** requires Z3 version 4.12.1, which you may need to install from a source build if your package manager supplies a different version. To do so, follow the instructions [here](https://github.com/Z3Prover/z3#building-z3-using-make-and-gccclang) after checking out the correct tag in the Z3 repository: ```sh git clone https://github.com/Z3Prover/z3.git cd z3 git checkout z3-4.12.1 python scripts/mk_make.py cd build make sudo make install ``` On macOS, it is easiest to install Z3 from Homebrew. If you wish to install from the source, install it to an appropriate prefix (e.g. `/usr/local` on Intel machines). **Ubuntu** On Ubuntu >= 22.04 (for example): ```sh sudo apt-get install --yes \ autoconf bison clang-12 cmake curl flex gcc jq libboost-test-dev \ libcrypto++-dev libffi-dev libgflags-dev libjemalloc-dev libmpfr-dev \ libprocps-dev libsecp256k1-dev libssl-dev libtool libyaml-dev lld-12 \ llvm-12-tools make maven netcat-openbsd openjdk-11-jdk pkg-config \ protobuf-compiler python3 python3-dev python3-pip rapidjson-dev time \ zlib1g-dev libfmt-dev ``` On Ubuntu < 18.04, you'll need to skip `libsecp256k1-dev` and instead build it from source (via our `Makefile`): ```sh make libsecp256k1 ``` **Arch Linux** On ArchLinux: ```sh sudo pacman -S \ base base-devel boost clang cmake crypto++ curl git gmp \ gflags jdk-openjdk jemalloc libsecp256k1 lld llvm maven \ mpfr protobuf poetry python stack yaml-cpp zlib ``` **macOS** After installing the Command Line Tools, [Homebrew](https://brew.sh/), and getting the blockchain plugin, run: ```sh brew tap kframework/k brew install java automake libtool gmp mpfr pkg-config maven libffi llvm@14 openssl protobuf python bash kframework/k/cryptopp@8.6.0 poetry solidity make libsecp256k1 ``` **NOTE**: It is recommended to use the homebrew version of `flex` and XCode. If you are building on an Apple Silicon machine, ensure that your `PATH` is set up correctly before running `make deps` or `make k-deps`. You can do so using [`direnv`](https://direnv.net/) by copying `macos-envrc` to `.envrc`, then running `direnv allow`. If the build on macOS still fails, you can also try adding the following lines to the top of your `Makefile` under `UNAME_S`: ```sh ifeq ($(UNAME_S), Darwin) SHELL := /usr/local/bin/bash PATH := $(pwd)/.build/usr/bin:$(PATH) endif ``` **Haskell Stack (all platforms)** * [Haskell Stack](https://docs.haskellstack.org/en/stable/install_and_upgrade/#installupgrade). Note that the version of the `stack` tool provided by your package manager might not be recent enough. Please follow installation instructions from the Haskell Stack website linked above. To upgrade `stack` (if needed): ```sh stack upgrade export PATH=$HOME/.local/bin:$PATH ``` #### Build Dependencies **K Framework** The `Makefile` and `kevm` will work with either a (i) globally installed **K** or a (ii) **K** submodule included in this repository. For contributing to `kevm`, it is highly recommended to go with (ii) because some of the build scripts might not work otherwise. Follow these instructions to get and build the **K** submodule: ```sh git submodule update --init --recursive -- deps/k make k-deps ``` If you don't need either the LLVM or Haskell backend, there are flags to skip them: ```sh make k-deps SKIP_LLVM=true SKIP_HASKELL=true ``` On an Apple Silicon machine, an additional flag to `make` is required to correctly build the Haskell backend: ```sh make k-deps APPLE_SILICON=true ``` **Blockchain Plugin** You also need to get the blockchain plugin submodule and install it. ```sh git submodule update --init --recursive -- deps/plugin make plugin-deps ``` #### Building You need to set up a virtual environment using Poetry with the prerequisites `python 3.8.*`, `pip >= 20.0.2`, `poetry >= 1.3.2`: ```sh make poetry ``` Finally, you can build the semantics. ```sh make build ``` You can build specific targets using `build-llvm`, `build-Haskell`, or `build-foundry`. For more information, refer to the Makefile. ### Running Tests To execute tests from the [Ethereum Test Set](https://github.com/ethereum/tests), the submodule needs to be fetched first. ```sh git submodule update --init --recursive -- tests/ethereum-tests ``` The tests are run using the supplied `Makefile`. Run `make build-prove` to generate tests from the markdown files. The following subsume all other tests: * `make test`: All of the quick tests. * `make test-all`: All of the quick and slow tests. These are the individual test-suites (all of these can be suffixed with `-all` to also run slow tests): * `make test-vm`: VMTests from the [Ethereum Test Set](https://github.com/ethereum/tests). * `make test-bchain`: Subset of BlockchainTests from the [Ethereum Test Set](https://github.com/ethereum/tests). * `make test-proof`: Proofs from the [Verified Smart Contracts](https://github.com/runtimeverification/verified-smart-contracts). * `make test-interactive`: Tests of the `kevm` command. When running tests with the `Makefile`, you can specify the `TEST_CONCRETE_BACKEND` (for concrete tests), or `TEST_SYMBOLIC_BACKEND` (for proofs). ### For Developers If built from the source, the `kevm` executable will be in the `.build/usr/bin` directory. To make sure you are using the correct `kevm`, add this directory to your `PATH`: ```sh export PATH=$(pwd)/.build/usr/bin:$PATH ``` Alternatively, if you work on multiple checkouts of `evm-semantics` or other semantics, you could add the relative path `.build/usr/bin` to your `PATH`. Do note, however, that this is a security concern. You can call `kevm help` to get a quick summary of how to use the script. Run the file `tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json`: ```sh kevm run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS ``` To enable the debug symbols for the llvm backend, build using this command: ```sh make build-llvm KEVM_OPTS=--enable-llvm-debug ``` To debug a conformance test, add the `--debugger` flag to the command: ```sh kevm interpret tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --backend llvm --mode NORMAL --schedule MERGE --chainid 1 --debugger ``` #### Keeping in mind while developing Always have your build up-to-date. * If using the kup package manager, run `kup install kevm --version .` to install the local version. * If building from source: * `make poetry` needs to be re-run if you touch any of the `kevm-pyk` code. * `make build` needs to be re-run if you touch any of this repos files. * `make deps` needs to be re-run if there is an update of the K submodule (you did `git submodule update --init --recursive -- deps/k` and it actually did something). * If both `deps` and `build` need to be re-run, you need to do `deps` first. * `make clean` is a safe way to remove the `.build` directory, but then you need to re-run `make deps` (should be quick this time) and `make build`. #### Building with Nix We now support building **KEVM** using [nix flakes](https://nixos.wiki/wiki/Flakes). To set up nix flakes you will need to be on `nix` 2.4 or higher and follow the instructions [here](https://nixos.wiki/wiki/Flakes). For example, if you are on a standard Linux distribution, such as Ubuntu, first [install nix](https://nixos.org/download.html#download-nix) and then enable flakes by editing either `~/.config/nix/nix.conf` or `/etc/nix/nix.conf` and adding: ``` experimental-features = nix-command flakes ``` This is needed to expose the Nix 2.0 CLI and flakes support that are hidden behind feature-flags. By default, Nix will build the project and its transitive dependencies from source, which can take up to an hour. We recommend setting up [the binary cache](https://app.cachix.org/cache/kore) to speed up the build process significantly. To build **KEVM**, run: ```sh nix build .#kevm ``` This will build all of **KEVM** and **K** and put a link to the resulting binaries in the `result/` folder. **NOTE**: Mac users, especially those running M1/M2 Macs may find nix segfaulting on occasion. If this happens, try running the nix command like this: `GC_DONT_GC=1 nix build .` If you want to temporarily add the `kevm` binary to the current shell, run ```sh nix shell .#kevm ``` #### Profiling with Nix Nix can also be used to quickly profile different versions of the Haskell backend. Simply run: ```sh nix build github:runtimeverification/evm-semantics#profile \ --override-input k-framework/haskell-backend github:runtimeverification/haskell-backend/ \ -o prof- ``` replacing `` with the commit you want to run profiling against. If you want to profile against a working version of the Haskell backend repository, simply `cd` into the root of the repo and run: ```sh nix build github:runtimeverification/evm-semantics#profile \ --override-input k-framework/haskell-backend $(pwd) \ -o prof-my-feature ``` To compare profiles, you can use: ```sh nix run github:runtimeverification/evm-semantics#compare-profiles -- prof-my-feature prof- ``` This will produce a nice table with the times for both versions of the haskell-backend. Note that `#profile` pre-pends the output of `kore-exec --version` to the profile run, which is then used as a tag by the `#compare-profiles` script. Therefore, any profiled local checkout of the haskell-backend will report as `dirty-ghc8107` in the resulting table. ### Media This repository can build two pieces of documentation for you, the [Jello Paper](https://jellopaper.org) and the [2017 Devcon3](https://archive.devcon.org/archive/watch?edition=3\&order=desc\&sort=edition) presentation. #### System Dependencies For the presentations in the `media` directory, you'll need `pdflatex`, commonly provided with `texlive-full`, and `pandoc`. ```sh sudo apt install texlive-full pandoc ``` #### Building To build all the PDFs (presentations and reports) available in the `media/` directory, use: ```sh make media ``` --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://docs.runtimeverification.com/kevm/overview/kevm-semantics-of-evm-in-k.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.