setup.md

Compiling Malfunction programs to Wasm

Prerequisites

• Binaryen v118 or greater.
• wasm_of_ocaml
• Node.js v22
• A version of the Malfunction compiler that supports OCaml bytecode compilation. See here for directions.

Compiling Malfunction programs to Wasm

1. malfunction cmo program.mlf produces compiled object bytecode
2. ocamlc program.cmo -o program.byte produces standalone bytecode executable
3. wasm_of_ocaml program.byte produces wasm binary program.wasm and necessary javascript scaffolding program.js

To run the Wasm binary: node program.js

Benchmarks in this directory

The binaries in this directory were produced by using the verified Coq extraction by Forster et al. to first extract the benchmarks from Coq to Malfunction, and then to Wasm using wasm_of_ocaml.

• binaries contain Wasm binaries generated using the defaults of malfunction, ocamlc and wasm_of_ocaml (no extra options/ optimizations)
• binaries-O2 contain Wasm binaries generated by passing the -O2 flag to the Malfunction compiler (e.g. malfunction cmo -O2 program.mlf) when producing the object bytecode

To run the benchmarks and print the results print use the python script benchmark.py and point it to either the binaries or binaries-O2 directory: python benchmark.py --runs 50 --folder binaries

Note that by default, the bernstein_yang benchmark is not included when running benchmarks, as we observed that it exhausts the available memory, even on a machine with 64GB of RAM.