Environment setup

Isabelle

This project requires Isabelle2025-2. As of Jun 2026, the installation instructions can be found here.

Isabelle AFP

Download AFP here.

Assume that isabelle has been installed with PATH set properly, before building the project, add AFP to Isabelle:

tar -xvf afp-current.tar.gz
isabelle components -u ${EXTRACTED_AFP_DIR}/thys

See scripts/install-isabelle.sh for more info.

spec

Build spec/interpreter. It requires installing OCaml (instructions). See spec/interpreter/README.md for more info.

Workflow

Update coupon.wat

After making changes to coupon.wat, run generate.sh to update the coupon ISA in Isabelle.

or

make thy

Invoke jedit

isabelle jedit -d wasm-proofs

Build from command line

isabelle build -D wasm-proofs -v Wasm-Proof

or

make