This project has been archived (2023-03-23)

See KWasm for the core semantics of WebAssembly. At this time (2023-03-23) it is being used for Elrond/MetaverseX semantics.

---

K Semantics of Ewasm

Under Construction

Prototype semantics of Ewasm in the K framework.

git submodule update --init --recursive
make deps
make build

Proving

Run existing proofs using make rules.

make tests/proofs/example-spec.k.prove
make tests/proofs/example-spec.k.repl

You can run the prover on your own specification, with a lemmas module of your choice.

./kewasm prove <path>/<to>/<spec> -m <LEMMAS-MODULE>  # Runs the prover on the given spec, using LEMMAS-MODULE as the top-level sematics module.

You can add the --repl flag to run the proof in an interactive REPL, where you can step through the proof and explore its branches.

./kewasm prove <path>/<to>/<spec> -m <LEMMAS-MODULE>  # Runs the prover on the given spec, using LEMMAS-MODULE as the top-level sematics module.

Structure

This project makes use of the K framework EEI and Wasm semantics. The main file is ewasm.md, which specifies the embedder that acts as a bridge between the Wasm semantics and the EEI.

Contract interface

Ewasm is a subset of WebAssembly (Wasm). Wasm does not specify how modules are embedded, how functions are invoked from the embedder, etc. Ewasm specifies a contract interface (subject to change until finalized) all contracts must adhere to.

Exports

A contract exports exactly one function, "main", and a memory, "memory".

Data passing

From the Wasm point of view, data is passed either as parameters and return values, or (for larger data/data of unknonw size) through the linear memory.