Updating WasmCert-Isabelle to WebAssembly 2.0
summary
WasmCert-Isabelle is updated to WebAssembly 2.0, adding bulk memory and reference types, a new bottom value for unreachable code, and a new subtyping rule for stack types; the mechanisation grows from 20,000 to 27,000 lines and takes roughly three months of effort. Verified artifacts updated include the type soundness proof, verified type checker, verified interpreter and module instantiation. The verified interpreter extracts to OCaml, passes the WebAssembly test suite, and with a new persistent P bytes memory representation runs close to or faster than the reference interpreter except on bulk-memory‑heavy tests.
AI-written summary · about
chapters (9)
- 0:00WasmCert-Isabelle and Wasm 2.0 intro
- 1:04WasmCert-Isabelle updates for Wasm 2.0
- 2:28Type system changes in Wasm 2.0
- 4:13Code metrics and type checker improvements
- 4:56Verified interpreter optimizations
- 12:12Bulk memory bottlenecks and optimizations
- 15:01Future for Wasm 3.0
- 16:26Q&A: Effort and optimizations
- 17:49Q&A: Time-consuming instruction
related talks
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
30mMechanising WebAssembly Well?
01h 08mOn WebAssembly
30mCertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
29mVerification of WebAssembly Features
51mLightning Talks