Home

Awesome

KWasm: Semantics of WebAssembly in K

Want to Support KWasm Development?

Contribute to our Gitcoin Grant.


This repository presents a prototype formal semantics of WebAssembly. It is currently under construction. 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:

These additional files extend the semantics to make the repository more useful:

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:

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

Resources