-
Notifications
You must be signed in to change notification settings - Fork 42
The WebAssembly backend
Use the CertiRocq command as described here.
To run a CertiRocq-generated Wasm binary one needs a small helper script that
- sets up the Wasm runtime
- invokes the main function
- 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.
Constructor values are stored in the Wasm binary's linear memory using a very similar layout as the C backend. The difference is that Wasm's i32 values are used instead of 64-bit pointers in C.
As opposed to the C backend, there is no garbage collection: Memory is not freed and old values are not overwritten.
Wasm's linear memory is limited to 2GB (a future proposal may change that), this means that running the Wasm binary of a very large Gallina program may run out of memory, which is indicated by the public out_of_mem being set to 1.
Wasm 3.0 introduces garbage-collected structs and arrays, but these are not yet formalized in WasmCert.
In addition to the benchmarks in benchmarks/wasm, there is an example setup in this repo that we recommend to follow.