Bas Spitters (Jun 17 2020 at 10:35): Bas Spitters (Jun 17 2020 at 10:35):There's a formalization of wasm in Coq
https://www.cs.rit.edu/~mtf/student-resources/20191_huang_mscourse.pdf
https://github.com/Huxpro/WasmCert
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.
Karl Palmskog (Jun 17 2020 at 10:37):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
Bas Spitters (Jun 17 2020 at 13:06):There's a bit of discussion in the beginning of the thesis.
In any case, having something in Coq seems useful...
Karl Palmskog (Jun 17 2020 at 13:11):maybe you can try to reach out to David Swasey what happened with his formalization? See multiple people asking for it in that issue.
Karl Palmskog (Jun 17 2020 at 13:15):unless someone adds a verified interpreter that can be conformance-tested,the formalization by Huang might not win out in the end
Bas Spitters (Jun 17 2020 at 13:45):Does he have a formalization in Coq or isabelle?
Karl Palmskog (Jun 17 2020 at 13:46):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.
Karl Palmskog (Jun 17 2020 at 13:51):ideally, both formalizations would be available and the community could work to consolidate them
Yannick Zakowski (Jun 17 2020 at 13:51):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"
Karl Palmskog (Jun 17 2020 at 13:51):oh gods, everyone and their brother is doing it.... this is why I honestly prefer working on cold topics all things considered.
Karl Palmskog (Jun 17 2020 at 13:53):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
Bas Spitters (Jun 17 2020 at 14:00):There are a number of people interested in the work by @swasey, but he does not seem to open his code:
https://github.com/WebAssembly/design/issues/1198
Pierre-Marie Pédrot (Jun 17 2020 at 14:01):I'll be talking with him live tonight
Pierre-Marie Pédrot (Jun 17 2020 at 14:01):I can ask him directly
Pierre-Marie Pédrot (Jun 17 2020 at 14:01):(he happens to be DM-ing our remote D&D game)
Karl Palmskog (Jun 17 2020 at 14:02):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
Pierre-Marie Pédrot (Jun 17 2020 at 14:02):will do
Xuan Huang (Jun 18 2020 at 05:20):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.
Karl Palmskog (Jun 18 2020 at 07:47):@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
Jean Pichon (Jun 18 2020 at 11:43):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
Derek Dreyer (Jun 18 2020 at 12:15):[Quoting…]
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.
Karl Palmskog (Jun 18 2020 at 12:31):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
Bas Spitters (Jun 18 2020 at 13:00):F* has it :-) @Kenji Maillard may know more
https://eprint.iacr.org/2019/542.pdf
Pierre-Marie Pédrot (Jun 18 2020 at 13:00):Dave told me he would publish his repo on Friday BTW
Karl Palmskog (Jun 18 2020 at 13:05):Bas Spitters said:
F* has it :-)
sigh... can't there be "formalization consortia"?
Bas Spitters (Jun 18 2020 at 13:07):How would you organize those?
Karl Palmskog (Jun 18 2020 at 13:08):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
Pierre-Marie Pédrot (Jun 18 2020 at 13:10):(the technique seems to have been invented by the Roman Curia though...)
Karl Palmskog (Jun 18 2020 at 13:12):I think the C++ committee meetings are legendary, and can sometimes go on for weeks(?)
Martin Constantino–Bodin (Jun 18 2020 at 13:21):Speaking of formalisation consortia, there is also an on-going skeletal formalisation of Wasm in Rennes.
Martin Constantino–Bodin (Jun 18 2020 at 13:23):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.
Kenji Maillard (Jun 18 2020 at 14:10):@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)
Karl Palmskog (Jun 18 2020 at 14:11):@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
Karl Palmskog (Jun 18 2020 at 15:05):case in point: compiling the seL4 kernel with CompCert gives unknown outcome/guarantees, since CompCert C and the seL4 C semantics are incomparable
Bas Spitters (Jun 18 2020 at 15:08):There is also @Robbert Krebbers Coq formalization of the C standard, which is not really connected to compcert IIRC.
Karl Palmskog (Jun 18 2020 at 15:11):I think Robbert wrote a paper with Xavier where the differences are discussed at least?
Philippa Gardner (Jun 18 2020 at 21:48):Hi all,
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.
Best wishes,
Philippa
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….
Bas Spitters (Jun 19 2020 at 07:09):@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?
Karl Palmskog (Jun 19 2020 at 16:19):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)
Philippa Gardner (Jun 19 2020 at 19:49):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.
Conrad Watt (Jun 19 2020 at 20:04):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.
Bas Spitters (Jun 20 2020 at 08:18):@Karl Palmskog Let's wait for @Philippa Gardner to talk to @Xuan Huang and see what is the best way forward.
Philippa Gardner (Jun 20 2020 at 10:44):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.
Philippa Gardner (Jul 18 2020 at 11:28):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.
Best wishes,
Philippa
Last updated: Jun 03 2023 at 15:31 UTC