WebAssembly (Wasm) is a low-level bytecode language and virtual machine, intended as a compilation target for a wide range of programming languages, which is seeing increasing adoption across diverse ecosystems. As a young technology, Wasm continues to evolve -- it reached version 2.0 last year and another major update is expected soon. For a new feature to be standardised in Wasm, four key artefacts must be presented: a formal (mathematical) specification of the feature, an accompanying prose pseudocode description, an implementation in the official reference interpreter, and a suite of unit tests. This rigorous process helps to avoid errors in the design and implementation of new Wasm features, and Wasm's distinctive formal specification in particular has facilitated machine-checked proofs of various correctness properties for the language. However, manually crafting all of these artefacts requires expert knowledge combined with repetitive and tedious labor, which is a burden on the language's standardization process and authoring of the specification. This paper presents Wasm SpecTec, a technology to express the formal specification of Wasm through a domain-specific language. This DSL allows all of Wasm's currently handwritten specification artefacts to be error-checked and generated automatically from a single source of truth, and is designed to be easy to write, read, compare, and review. We believe that Wasm SpecTec's automation and meta-level error checking will significantly ease the current burden of the language's specification authors. We demonstrate the current capabilities of Wasm SpecTec by showcasing its proficiency in generating various artefacts, and describe our work towards replacing the manually written official Wasm specification document with specifications generated by Wasm SpecTec.

翻译：论文摘要：WebAssembly（Wasm）是一种底层字节码语言和虚拟机，旨在作为多种编程语言的编译目标，正被广泛应用于不同生态系统。作为新兴技术，Wasm持续演进——去年发布了2.0版本，预计近期将迎来又一次重大更新。对于Wasm中新增功能的标准制定，需提供四项关键产品：该功能的形式化（数学）规范、配套的伪代码描述、官方参考解释器的实现，以及完整的单元测试套件。这一严格的流程有助于避免新Wasm功能设计与实现中的错误，而Wasm独特的形式化规范尤其促进了语言各类正确性属性的机器可验证证明。然而，手动构建所有这些产品既需要专业知识，又涉及重复性繁重劳动，给语言标准化进程和规范编写带来了沉重负担。本文提出Wasm SpecTec——一种通过领域特定语言表达Wasm形式化规范的技术。该DSL能够自动校验并生成Wasm当前所有手写规范产品，且这些产品均源于单一可信源；其设计注重易写、易读、易比较、易审查。我们相信，Wasm SpecTec的自动化和元级错误校验将显著减轻规范编写者的当前负担。通过展示其在生成各类产品方面的卓越能力，我们阐述了Wasm SpecTec的现有功能，并描述了用其自动生成的规范替代手写官方Wasm规范文档的工作进展。