There's a formalization of wasm in Coq
The author would be happy to contribute it to the community. Are there any alternative formalizations, before I suggest him to open an issue on github.
there seems to be a definitive formalization in Isabelle/HOL, is there an obvious relation between that and the Coq one? https://github.com/WebAssembly/design/issues/1198#issuecomment-377697712
There's a bit of discussion in the beginning of the thesis.
In any case, having something in Coq seems useful...
maybe you can try to reach out to David Swasey what happened with his formalization? See multiple people asking for it in that issue.
unless someone adds a verified interpreter that can be conformance-tested,the formalization by Huang might not win out in the end
Does he have a formalization in Coq or isabelle?
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.
ideally, both formalizations would be available and the community could work to consolidate them
Conrad Watt gave a talk Yesterday at the REM-DeepSpec workshop on formalization efforts of Wasm: https://pldi20.sigplan.org/details/rems-deepspec-2020/11/-WebAssembly-sequential-and-concurrent-semantics
He has mainly developed an Isabelle HOL formalization as far as I understand: https://www.isa-afp.org/entries/WebAssembly.html
However, he also said, I quote: "On my side, there's some work with a group at ICL (including @Philippa Gardner) on a more modern mechanisation of Wasm in Coq. It's at an advanced stage, but still ongoing. It would be nice to be able to hook it into Compcert"
oh gods, everyone and their brother is doing it.... this is why I honestly prefer working on cold topics all things considered.
for example, there are already three industry-scale incompatible formalizations of the C language, and depending on how one counts there are probably 3-4 additional serious academic formalizations
There are a number of people interested in the work by @swasey, but he does not seem to open his code:
I'll be talking with him live tonight
I can ask him directly
(he happens to be DM-ing our remote D&D game)
if appropriate (e.g., he is not working on it and wants help porting, etc.), you might mention that we could host the project in coq-community as per above
Hey, I'm Xuan, the author of WasmCert. Thanks @Bas Spitters for reaching out to me and discussing the possibility of moving it to coq-community. This is my first time here, so very nice to meet you folks!
I see some of the questions raised in the thread that I can quickly respond with:
I actually started the project after seeing the needs and interests, also the absence of updates, from https://github.com/WebAssembly/design/issues/1198. My project was actually started as late as Sept 2019, even after the latest comment from that issue.
Conrad Watt's work is one of the major sources of inspiration of my project, which I have explicitly compared with in my thesis. In fact, Both Watt and Rossberg are likely aware of my works from the very beginning (https://github.com/WebAssembly/multi-value/issues/23). I'm not sure which project did Watt refer to, but "modern mechanization" was a goal of my effort as well. I was explicitly targeting the published W3C version of Wasm spec, while Watt's original work was targeting the semantics included in the Wasm PLDI 17 paper.
Personally, I don't have a strong willing that my effort should be chosen over others. I just started learning and using Coq and I'd love to see mechanization and proof engineering better than I did.
But by any chance, I'm more than happy to get more people involved. I explicitly stated in my thesis that one of the initiative of the project was to (potentially) "serve as a foundation for certified software development in the Coq community", which couldn't be accomplished without the help from the community.
@Xuan Huang please see here for how the process for moving the project to coq-community works: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#proposing-a-new-package
We (alphabetically: Martin Bodin, Philippa Gardner, Jean Pichon, Xiaojia Rao, Conrad Watt) started even later than that, in response to people asking at conferences whether there was a Coq version of Conrad's Isabelle/HOL version.
As Conrad pointed out, it's work in progress (>60%?). We wanted to finish the proofs and validate the formalisation more before publicising.
Sadly, we were not aware of Xuan Huang's version.
We are aiming for W3C-spec compliance, and to be broader than Conrad's original model
I don't think Dave has worked on this in a while, and I don't know what the status is. He has been trying to finish up his PhD thesis (on something completely unrelated), and is now going to work at Bedrock. But it would be great if others will be able to see what he's done.
right, a good step would be to get as much code as authors will allow into the open, and ideally there would be work towards unifying projects at some (possibly much) later point
F* has it :-) @Kenji Maillard may know more
Dave told me he would publish his repo on Friday BTW
Bas Spitters said:
F* has it :-)
sigh... can't there be "formalization consortia"?
How would you organize those?
along the lines of what they do in industry: you lock technical people & some managers in a room, and they don't come out until they agree on some basic rules/efforts that will not lead to complete fragmentation
(the technique seems to have been invented by the Roman Curia though...)
I think the C++ committee meetings are legendary, and can sometimes go on for weeks(?)
Speaking of formalisation consortia, there is also an on-going skeletal formalisation of Wasm in Rennes.
But I believe that each of these formalisations have a very different goal in mind.
We (see Jean Pichon’s post above) for instance explicitly target Iris, as well as a very low-level formalisation of each operations.
@Karl Palmskog I have the impression that the standardization process of TLS 1.3 benefited from having formal feedback from multiple parties (I mostly heard about the formalization in F* of project everest being developed at the same time as the RFC)
@Kenji Maillard right, and they said the same about some aspects of C++. However, I was alluding to "standardizing" the formalizations of something that is already fixed, i.e., making sure formalizations are at least comparable in some way and that the same work is not done over and over
case in point: compiling the seL4 kernel with CompCert gives unknown outcome/guarantees, since CompCert C and the seL4 C semantics are incomparable
There is also @Robbert Krebbers Coq formalization of the C standard, which is not really connected to compcert IIRC.
I think Robbert wrote a paper with Xavier where the differences are discussed at least?
I have an M.Sc student, Xiaojia Rao, doing a Coq-specification of Wasm, supported by Martin Bodin from Imperial and Jean Pichon and Conrad Watt from Cambridge. Following methodology introduced in the JSCert project (see my web page), the MSc project is:
1-3 have been done for the Wasm published in PLDI’17 and are now being adapted slightly to Wasm 1.0. We are also thinking about a new WasmRef written in a monadic style to make a better link to the English pseudocode, with interaction trees used to represent the interaction with the host (thank you Kenji Maillard!). We should have the type safety done fairly soon, and then Rao will be doing 6 (probably straightforward) and Iris Wasm (a bit of a learning curve!).
Given this discussion, we have made our current work public on Github today, see https://github.com/Imperial-Wasm/wasm-coq-public. We will be working in a private repository, publishing further snapshots (e.g. Wasm 1.0 and type safety) as soon as they are ready. We would welcome collaboration and interaction with others, whilst at the same time protecting Rao’s M.Sc thesis. Please do not hesitate to get in contact if you wish.
PS. We recently found out about Xuan’s work independently of this discussion and were about to reach out to him! We have sent email to Xuan and his supervisor, Matthew Fluent, and would very much like to find a way to collaborate if it makes sense. We have also been using the names WasmCert and WasmRef, following Imperial and INRIA’s previous work on the JsCert/JSRef project. We need to work out what to do about this….
@Philippa Gardner Sounds very interesting! I'm curious about the comparison with the work by Xuan.
Can you say anything about how this compares to the work in F* https://eprint.iacr.org/2019/542.pdf and the work in Isabelle?
many valuable comments here, but recall that this is not a publicly visible forum. @Bas Spitters perhaps you could summarize the key facts from above in a coq-community GitHub issue (proposing to move https://github.com/Huxpro/WasmCert)
Thanks Bas. Our work on our WasmCert closely follows Conrad's work on an Isabelle-spec of Wasm, to the extent that we are copying Conrad's definitions and proofs as much as we can. Our work will be more complete than Xuan's, but we are a large team of Coq and Wasm experts supporting the M.Sc student Rao. The comparison is not really fair. I need to take a look at the F* work. Have they done a Coq-Specification of Wasm? It's not apparent from a quick read of the intro.
As far as I understood, the idea of the F* work is that they write specs for cryptographic functions, implement them in a source language (Low*), and then verify that the spec is satisfied using weakest pre-condition. They then compile the code to WebAssembly. AFAIK the compiler isn't verified beyond some hand-proofs of intermediate stages, and they don't need to handle the full Wasm language, just what's in the image of their compilation.
@Karl Palmskog Let's wait for @Philippa Gardner to talk to @Xuan Huang and see what is the best way forward.
Thanks very much Bas, I haven't got contact yet but hopefully will. I gather that Xuan is now at Facebook, but I need to check this. I also want to understand Matthew's plans.
Hi all, I’ve been in contact with Matthew Fluet. Xuan is now at Facebook. He might be moving to a Wasm group in future which would be interesting. Matthew is not currently active on a Wasm Coq-specification. We will keep in contact.
We’ve been doing a little bit of clean-up to our WasmCert, merging branches and moving to Wasm 1.0. We have a new link at https://github.com/WasmCert/WasmCert-Coq (the old link https://github.com/Imperial-Wasm/wasm-coq-public redirects to this new place). The organisation is “WasmCert” with two repositories: "WasmCert-Coq" and "WasmCert-Isabelle” which we hope to eventually link together. The link https://github.com/WasmCert/WasmCert-Coq contains:
—master: WasmCert/WasmRef/correctness proof and preservation for type safety. We have moved to Wasm 1.0. Our specification might contain a few niggles, but they will get ironed out as we test and continue with the type safety proof.
—a branch where Rao is at the moment doing progress for type safety, which we will merge with the master as soon as its done.
—a branch where there is a new WasmRef that models interaction with the host using interaction trees. It’s work in progress.
Last updated: Feb 05 2023 at 14:02 UTC