Machine-Checkable Formal Semantics

[lorenzleutgeb]

TL;DR: What's the state of a formal, machine-checkable semantics for WebAssembly?

Hello!

This is meant as a question and basis for discussion.

WebAssembly is an attractive compilation target (golang/go#18892, rust-lang-nursery/rust-wasm, emscripten, ...). And it would be nice to have a spec that is as precise as possible, to eliminate ambiguities between the languages that compile to wasm. From what I see, you, the designers, are very aware of these facts and steering towards that goal.

However, my understanding of a "formal" specification is more rigid. Instead of a carefully crafted specification in natural language, I am interested in a formulation using mathematical language. Also, I would want it to be machine-readable and machine-checkable.

Example of such specification efforts:

• JsCert (paper as PDF and via DOI)
• A Formal Semantics for C++ (paper as PDF and at CSIRO) by @mn200
• RustBelt (paper via DOI) by @RalfJung, see Prove the Rust type system sound rust-lang/rust#9883. And @cmr dreaming about MIR-to-CakeML
• The Semantics of CakeML
• The Definition of Standard ML

As the authors of JsCert note in the paper referenced above:

Our challenge is to convince ourselves and others that JSCert is indeed an accurate formulation of the ES5 English specification. We designed JSCert to follow the structure of the ES5 English standard as much as possible. Whenever we found parts of ES5 English prose to be ambiguous, we checked the browser implementations and were active on discussion groups [...]

Many of these efforts do not reach widespread adoption/acceptance, because they are not coupled well with the ongoing standardization efforts. I would to ask for your opinion on the matter and whether a formal semantics would be attractive to you. Thanks.

P.S.: I know the common criticism that a formal semantics does not get you anywhere since it is hard to verify correctness of compilation phases that get you from high-level code to wasm in the first place. However, CakeML for example is verified and it would be interesting to see this verification extend down to wasm code. Also, there might be more verified compilers that target wasm available in the future.

[rossberg]

Have you checked out the actual language specification for Wasm? ;) It not only contains a formal semantics of the complete language, this semantics even represents the normative core of the spec. It is based on the formalisation from our PLDI 2017 paper. I am confident to say that the Wasm spec is even more rigorous and precise than the SML Definition.

Moreover, this semantics has already been mechanised in Isabelle, see the CPP 2018 paper by @conrad-watt (who was previously involved in JsCert). That work also includes a verified interpreter. Two other mechanisations are currently under development, one in Coq by @swasey (who is also part of the RustBelt team), and another one using the K framework.

[lorenzleutgeb]

Sweet! Except from exposing my poor search skills, this is a great and probably definitive answer :) Nice to find out.

I saw the language specification, but did not find the mechanisation in Isabelle. For reference, the one mentioned can be downloaded here.

[jwiegley]

@swasey Is it possible to look at and perhaps assist with your Coq development?

[swasey]

@jwiegley yes. I will move it somewhere public on Monday.

I'd welcome assistance, mainly because I'm focused on other things (that will, eventually, bring me back to working with this Coq development). Roughly, my TODO list is (i) flesh out the semantics of floating point and (ii) develop a basic sanity check (like a proof of type soundness or an instantiation of Iris) and (iii) catch up with changes to the WebAsembly spec since around February.

[jwiegley]

@swasey Any word on making this code publicly accessible?

[tchajed]

@swasey I would also be interested in looking at and possibly assisting with a Coq development, especially instantiating Iris over wasm

[vzaliva]

@swasey I am also interested in WASM semantics in Coq.

[stefandeml]

@swasey is the Coq work publicly available?