The WebAssembly backend

Obtaining a Wasm binary

Use the CertiRocq command as described here.

Running the Wasm binary

To run a CertiRocq-generated Wasm binary one needs a small helper script that

1. sets up the Wasm runtime
2. invokes the main function
3. obtains and pretty-prints the result.

CertiRocq-generated Wasm binaries should run with any modern Wasm runtime (supporting Wasm 1.0 and Tail calls). We provide the setup for the two most common Wasm runtimes: Wasmtime+Python and Node+JavaScript,

It is also possible to insert custom Wasm code into the binary that interacts with the generated parts directly. This may be a bit tricky though, see e.g. the snippet here and the corresponding Makefile.

Memory layout

Constructor values are stored in the Wasm binary's linear memory in a layout based on the one from the C backend. The only difference is that Wasm's i32 values are used instead of 64-bit pointers in C.

Examples

In addition to the benchmarks in benchmarks/wasm, there is an example setup in this repo that we recommend to follow.