State of mechanisation of the spec

[ppenzin]

Apologies for the ignorance, I've manage to miss a couple of recent meetings on SpecTec where this might've been discussed, but what is our current state of mechanisation and verification of the spec?

I know there is the WasmCert org, and I vaguely recall that the Isabelle project was more up-to-date on features, but it hasn't been updated in a couple of years.

How far is SpecTec from producing a working mechanisation of the spec?

CC: @keithw, @woodsmc

[rossberg]

Just to be clear, mechanisation consists of at least two parts: translating definitions and doing proofs. SpecTec should automate the first, but generally cannot do the second, which still requires actual real-world intelligence — although there are various boring auxiliary lemmas and proofs that could presumably be automated as well.

The Coq backend for SpecTec still is very much work in progress, @raoxiaojia from the WasmCert project has done most of that so far. I don't think anybody is currently planning an Isabelle backend. The active development for WasmCert is on the Coq mechanisation as well, which handles Wasm 2.0 and has other added value, like a bridge to the Iris program logic framework.

[raoxiaojia]

To add a bit to the SpecTec part, we've been back to active development of the Coq backend (as well as something more general) after the 2.0 update last month -- taking some time as we are trying to recover some passes that are required for mechasnisation backends, plus dealing with some new constructs in the IL since the previous experiments.

Regarding hand mechanisations, the Isabelle project on WasmCert implemented the vector instructions and additional numerics instructions in 2.0 (maybe Conrad can comment on this further), while the recent Coq 2.0 update left them out and implemented the other features plus some features from the future proposals.