A Coq Formalization of WebAssembly Execution Costs
summary
Formal Coq mechanization over a wasm-cert fork produces parametric execution cost bounds (instruction counts) and extracts an OCaml tool; it proves cost inequalities from basic blocks up to function cost, yields numeric bounds for non‑looping functions and symbolic bounds for some loops, and solves loop iteration unknowns via algebraic reduction, loop patterns and SMT solvers. Testing covers real Wasm artifacts (Bitcoin miner, Doom, AutoCAD); an artificial one‑million path limit hits under 5% of loops. The work targets Wasm 1.0 and plans full call‑tree analysis.
AI-written summary · about
chapters (11)
- 0:00WebAssembly cost analysis intro
- 1:07Motivation for formalizing costs
- 3:16Thesis approach and results
- 5:46Transition to Coq formalization
- 7:54WAMR for formal definitions
- 10:05Control flow graphs and loops
- 13:20Loop condition parameterization
- 14:48Recursive cost inequalities
- 16:36Future work and performance
- 17:46Conclusion and impact
- 18:36Q&A
related talks
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
30mCertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
01h 08mOn WebAssembly
30mMechanising WebAssembly Well?
29mWasocaml: a compiler from OCaml to WebAssembly
55mGenerating Executable Specification from Formal Semantics of WebAssembly
01h 06mAs low-level as possible, but no lower