Awesome
KWasm: Semantics of WebAssembly in K
Want to Support KWasm Development?
Contribute to our Gitcoin Grant.
This repository presents the formal semantics of WebAssembly. KWasm is a mature and production-ready semantics for WebAssembly, actively developed and maintained since 2019.
For examples of current capabilities, see the unit tests under the tests/simple
directory.
Repository Structure
Semantics Layout
The following files constitute the KWasm semantics:
- data.md provides the (functional) data of WebAssembly (basic types, type constructors, and values).
- numeric.md provides the functional rules for numeric operators.
- wasm.md is the main KWasm semantics, containing the configuration and transition rules of WebAssembly.
These additional files extend the semantics to make the repository more useful:
- test.md is an execution harness for KWasm, providing a simple language for describing tests/programs.
Example usage: ./kwasm
runner script
After building the definition, you can run the definition using ./kwasm
.
The most up-to-date documentation will always be in ./kwasm help
.
Run the file tests/simple/arithmetic.wast
:
./kwasm run tests/simple/arithmetic.wast
To run proofs, you can similarly use ./kwasm
, but must specify the module to use for proving.
For example, to prove the specification tests/proofs/simple-arithmetic-spec.k
:
./kwasm prove tests/proofs/simple-arithmetic-spec.k kwasm-lemmas
To prove WRC-20 specifications:
./kwasm prove tests/proofs/wrc20-spec.k wrc20
You can optionally override the default backend using the --backend BACKEND
flag:
./kwasm run --backend llvm tests/simple/arithmetic.wast
./kwasm prove --backend haskell tests/proofs/simple-arithmetic-spec.k kwasm-lemmas
Installing/Building
K Backends
There are two backends of K available, the LLVM backend for concrete execution, and the Haskell backend for symbolic reasoning and proofs.
This repository generates the build-products for the backends in .build/defn/llvm
and .build/defn/haskell
.
Dependencies
The following are needed for building/running KWasm:
- git
- Pandoc >= 1.17 is used to generate the
*.k
files from the*.md
files. - GNU Bison, Flex, and Autoconf.
- GNU libmpfr and libtool.
- Java 8 JDK (eg. OpenJDK)
- Haskell Stack.
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. - LLVM For building the LLVM backend.
- Z3 version 4.8.15
On Ubuntu >= 15.04 (for example):
sudo apt-get install --yes \
autoconf bison clang++-8 clang-8 cmake curl flex gcc libboost-test-dev libffi-dev \
libgmp-dev libjemalloc-dev libmpfr-dev libprocps-dev libprotobuf-dev libtool \
libyaml-dev lld-8 llvm llvm-8 llvm-8-tools maven openjdk-8-jdk pandoc pkg-config \
protobuf-compiler python3 python-pygments python-recommonmark python-sphinx time \
zlib1g-dev
To upgrade stack
(if needed):
stack upgrade
export PATH=$HOME/.local/bin:$PATH
After installing the above dependencies, make sure the submodules are setup:
git submodule update --init --recursive
Install repository specific dependencies:
make deps
Installing Z3
Note that KWASM requires Z3 version 4.8.15, 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 after checking out the correct tag in the Z3 repository:
git clone https://github.com/Z3Prover/z3.git
cd z3
git checkout z3-4.8.15
python scripts/mk_make.py
cd build
make
sudo make install
Building
And then build the semantics:
make build
To only build a specific backend, you can do make build-llvm
or make build-haskell
.
Media and documents
The media/
directory contains presentations and reports about about KWasm.
The documents are named with an approximate date of presentation/submission, what type of document it is, and a brief contextual name, e.g., name of conference where it was held.
GhostScript is a dependency for building documents of type report
.
sudo apt install ghostscript
To build all documents in the media file:
make media
Testing
The target test
contains all the currently passing tests.
make test