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.
The following files constitute the KWasm semantics:
These additional files extend the semantics to make the repository more useful:
./kwasm
runner scriptAfter 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
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
.
The following are needed for building/running KWasm:
*.k
files from the *.md
files.stack
tool provided by your package manager might not be recent enough.
Please follow installation instructions from the Haskell Stack website linked above.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
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
And then build the semantics:
make build
To only build a specific backend, you can do make build-llvm
or make build-haskell
.
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
The target test
contains all the currently passing tests.
make test