wasm_coq

WebAssembly (aka Wasm) 1.0 formalisation in Coq, based on the official formalisation. Our definitions and proofs initially drew from those given in the Isabelle mechanisation of Conrad Watt.

The quotes from the WebAssembly standard (starting with std-doc) are (C) their respective authors.

This work is in progress. While our initial work used the definitions published in PLDI'17, we have now adapted the mechanisation to Wasm 1.0., the specification as ratified by the W3C. A large part of the work has been published at FM'21, with more additions to the repository since then.

Components of the Repository

In Publication

Core definitions of WasmCert-Coq and WasmRef-Coq.
Soundness results for WasmRef-Coq (interpreter) with respect to WasmCert-Coq.
Type safety results for Wasm typing system.
Soundness and completeness results for the type checker with respect to the typing system.
Implementing Wasm numerics (via CompCert numerics).

Merged

Soundness results for module instantiation.
Proof carrying interpreter deriving progress.

Unmerged/Future Work

Generalised framework for evaluation contexts.
Validate WasmRef-Coq (conformance tests).
Optimise interpreter for contexts.

Program Logic

This repository contains a mechanised Wasm program logic using the Iris framework: iris branch. This is migrated from an older build for the artefact submitted along with the Iris-Wasm publication at PLDI'23.

Binary Parser (experimental)

This repository contains some experimental work on a parser for the binary format which is currently unverified.

Usage

Installation and Compilation

The project can be installed using opam.

Compiling the dependencies requires having at least 4-8 GB of RAM on your computer.

opam repo add coq-released https://coq.inria.fr/opam/released
opam install .

Build Based on Esy

The previous esy-based build is now deprecated; it is moved to esy branch.

Testing the Installation

The project comes with a small set of tests for the extracted interpreter:

dune test

Using the project

A file wasm_coq_interpreter will have been generated. It takes as argument a list of Wasm files, followed by a function name, followed by the number of steps of execution (fuel). For instance, to interpret the function main defined in tests/floatmul.wasm, run:

dune exec -- wasm_coq_interpreter tests/floatmul.wasm main 10

The interpreter can display intermediate states of the operational semantics:

dune exec -- wasm_coq_interpreter tests/floatmul.wasm main 10 --vi

would produce:

parsing OK
instantiation OK
interpreting OK
step 0:

invoke 0
with values (empty)

step 1:
normal
  local 1
  with values (empty)
    block f32
        f32.const 4350553f
        f32.const 431c4000
        f32.mul
    end
  end local
with values (empty)
and store unchanged
step 2:
normal
  local 1
  with values (empty)
    label 1
    label_cont
      f32.const 4350553f
      f32.const 431c4000
      f32.mul
    end label
  end local
with values (empty)
and store unchanged
step 3:
normal
  local 1
  with values (empty)
    label 1
    label_cont
      f32.const 46fe500f
    end label
  end local
with values (empty)
and store unchanged
step 4:
normal
  local 1
  with values (empty)
    f32.const 46fe500f
  end local
with values (empty)
and store unchanged
step 5:
normal
  f32.const 46fe500f
with values (empty)
and store unchanged

posticarus/WasmCert-Coq