New Summary

Summary Wasm Engineering a Formal Language Standard arxiv.org

3,608 words - PDF document - View PDF document

Chat with this pdf   Buy me a coffee

One Line

Wasm SpecTec automates the creation of formal specification artifacts for Wasm, improving efficiency and reliability by generating specs for Wasm 2.0.

Slides

Slide Presentation (12 slides)

Copy slides outline   Copy embed code   Download as Word

Automating Formal Specification Artifacts for WebAssembly

Source: arxiv.org - PDF - 3,608 words - view

   

Key Points

  • Wasm SpecTec is a technology that automates the process of generating formal specification artifacts for WebAssembly.
  • The current process of manually creating these artifacts can be time-consuming and laborious.
  • Wasm SpecTec provides a domain-specific language (DSL) that allows for the automatic generation of Wasm's specification artifacts from a single source of truth.
  • The DSL is designed to be easy to write, read, compare, and review.
  • Wasm SpecTec aims to ease the burden on specification authors and improve the efficiency of the standardization process.
  • The toolchain is being extended to generate unit tests and full theorem prover definitions.
  • The ultimate goal is for the Wasm standards community to adopt Wasm SpecTec as the primary method for specifying current and future Wasm features.
  • By replacing manually authored artifacts with those generated by Wasm SpecTec, the standardization process can be made more efficient and reliable.

Summaries

22 word summary

Wasm SpecTec automates creation of formal specification artifacts for Wasm, improving efficiency and reliability. It has already generated specs for Wasm 2.0.

62 word summary

Wasm SpecTec automates the creation of formal specification artifacts for WebAssembly (Wasm) by providing a domain-specific language (DSL) that generates these artifacts. It aims to improve efficiency and reliability by replacing manual creation with automated generation. Wasm SpecTec has already generated formal specifications and pseudocode for Wasm 2.0, passing all tests. The goal is for the Wasm community to adopt this technology.

133 word summary

Wasm SpecTec automates the creation of formal specification artifacts for WebAssembly (Wasm) by providing a domain-specific language (DSL) that generates these artifacts from a single source of truth. It aims to improve the efficiency and reliability of the standardization process by replacing manual creation with automated generation. Wasm SpecTec offers a unified DSL that closely mirrors Wasm's syntactic constructs. The DSL definitions are processed into internal representations, such as the Internal Language (IL) and Algorithmic Language (AL), which enable deep analysis and transformation of the specifications. Prose pseudocode specifications can be generated from the AL, closely resembling handwritten descriptions. Wasm SpecTec has already generated formal specifications and pseudocode for all of Wasm 2.0, passing all applicable tests. The goal is for the Wasm community to adopt this technology to enhance the standardization process.

384 word summary

Wasm SpecTec is a technology that automates the generation of formal specification artifacts for WebAssembly (Wasm). It aims to address the time-consuming and laborious process of manually creating these artifacts by providing a domain-specific language (DSL) that allows for their automatic generation from a single source of truth. By automating this process, Wasm SpecTec aims to ease the burden on specification authors and improve the efficiency of the standardization process.

The current Wasm specification is authored in reStructuredText and LaTeX, which can be challenging to work with. Wasm SpecTec offers a unified DSL that closely mirrors the syntactic constructs used in Wasm's formal specification. The DSL definitions are processed into internal representations, such as the Internal Language (IL) and Algorithmic Language (AL), which are used to generate the desired artifacts.

The IL representation enables deep analysis and transformation of the specifications, including type inference and annotation. The AL representation further restricts the definitions to enforce an algorithmic order of evaluation. From the AL, prose pseudocode specifications can be generated, closely resembling the original handwritten descriptions. Additionally, an interpreter for the AL can be implemented to indirectly obtain an interpreter for Wasm.

Wasm SpecTec has already demonstrated its capabilities by generating formal specifications and prose pseudocode for all of Wasm 2.0. The generated specifications have been tested against the official Wasm unit test suite and have passed all applicable tests. The toolchain is also being extended to generate unit tests and full theorem prover definitions.

The ultimate goal of Wasm SpecTec is for the Wasm standards community to adopt it as the primary method for specifying current and future Wasm features. By replacing manually authored artifacts with those generated by Wasm SpecTec, the standardization process can be made more efficient and reliable. Feedback from industrial stakeholders will be gathered to evaluate the ease of extending SpecTec to cover additional features, such as Exception Handling, Garbage Collected Types, and Threads.

In conclusion, Wasm SpecTec is a technology that automates the generation of formal specification artifacts for WebAssembly. It provides a domain-specific language and toolchain that allows for the automatic generation of specifications, pseudocode descriptions, and more. By easing the burden on specification authors and improving the consistency and trustworthiness of the artifacts, Wasm SpecTec aims to enhance the efficiency and reliability of the Wasm standardization process.

470 word summary

Wasm SpecTec is a technology that aims to automate the process of generating formal specification artifacts for WebAssembly (Wasm). Wasm is a low-level bytecode language and virtual machine that serves as a compilation target for various programming languages. The standardization process for new Wasm features requires the presentation of four key artifacts: a formal specification, a prose pseudocode description, an implementation in the reference interpreter, and a suite of unit tests. However, manually creating these artifacts can be time-consuming and laborious.

To address this issue, Wasm SpecTec provides a domain-specific language (DSL) that allows for the automatic generation of Wasm's specification artifacts from a single source of truth. The DSL is designed to be easy to write, read, compare, and review. By automating the generation of these artifacts, Wasm SpecTec aims to ease the burden on specification authors and improve the efficiency of the standardization process.

The current Wasm specification is authored in reStructuredText and LaTeX, which can be challenging to work with. Wasm SpecTec offers a unified DSL that closely mirrors the syntactic constructs used in Wasm's formal specification. The DSL definitions are processed into internal representations, such as the Internal Language (IL) and Algorithmic Language (AL), which are used to generate the desired artifacts.

The IL representation allows for deep analysis and transformation of the specifications, including type inference and annotation. The AL representation further restricts the definitions to enforce an algorithmic order of evaluation. From the AL, prose pseudocode specifications can be generated, closely resembling the original handwritten descriptions. Additionally, an interpreter for the AL can be implemented to indirectly obtain an interpreter for Wasm.

Wasm SpecTec is still in development but has already demonstrated its capabilities by generating formal specifications and prose pseudocode for all of Wasm 2.0 (except SIMD instructions). The generated specifications have been tested against the official Wasm unit test suite and have passed all applicable tests. The toolchain is also being extended to generate unit tests and full theorem prover definitions.

The ultimate goal of Wasm SpecTec is for the Wasm standards community to adopt it as the primary method for specifying current and future Wasm features. By replacing the manually authored artifacts with those generated by Wasm SpecTec, the standardization process can be made more efficient and reliable. Feedback from industrial stakeholders will be gathered to evaluate the ease of extending SpecTec to cover additional features, such as Exception Handling, Garbage Collected Types, and Threads.

In conclusion, Wasm SpecTec is a technology that automates the generation of formal specification artifacts for WebAssembly. It provides a domain-specific language and toolchain that allows for the automatic generation of specifications, pseudocode descriptions, and more. By easing the burden on specification authors and improving the consistency and trustworthiness of the artifacts, Wasm SpecTec aims to enhance the efficiency and reliability of the Wasm standardization process.

Raw indexed text (25,910 chars / 3,608 words / 481 lines)

Wasm SpecTec: Engineering a Formal Language Standard
Joachim Breitner Philippa Gardner Jaehyun Lee
Independent
Germany
[email protected] Imperial College London
United Kingdom
[email protected] KAIST
South Korea
[email protected]
Sam Lindley Matija Pretnar Xiaojia Rao
The University of Edinburgh
United Kingdom
[email protected] University of Ljubljana
Slovenia
[email protected] Imperial College London
United Kingdom
[email protected]
Andreas Rossberg Sukyoung Ryu Wonho Shin
Independent
Germany
[email protected] KAIST
South Korea
[email protected] KAIST
South Korea
[email protected]
Conrad Watt Dongjun Youn
University of Cambridge
United Kingdom
[email protected] KAIST
South Korea
[email protected]
ABSTRACT 1
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 arte-
facts 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 speci-
fication.
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 re-
placing the manually written official Wasm specification document
with specifications generated by Wasm SpecTec. WebAssembly (Wasm) is a low-level bytecode language and virtual
machine [13]. Initially introduced to allow efficient compilation
and execution of a larger variety of programming languages on the
Web platform, it has since been adopted across a broad range of
ecosystems, such as cloud and edge computing [15, 25], mobile and
embedded systems [27], IoT [14], and blockchains [24].
Following its initial release, there has been growing demand for
the integration of new language features into Wasm. The version
of Wasm initially supported by browsers in 2017, referred to by
its designers as a “Minimum Viable Product” (MVP) [17], served
as a simple compilation target for languages like C/C++ and Rust.
However, the performance of programs compiled with the MVP is
suboptimal, and a few key features such as shared memory con-
currency and exception handling are not supported by the MVP.
Other languages involving runtime-managed memory such as Java
cannot be compiled without significant performance or usability
compromises, for example, because the Wasm MVP cannot easily
express the stack walking strategies used by the garbage collectors
of these languages’ runtimes. Several proposals, including SIMD
Vector Instrutions [9], Exception Handling [10], Garbage Collected
Types [11], and Threads [12] are being developed in Wasm to alle-
viate these problems.
For a feature to be standardised in Wasm, four key artefacts must
be presented to the W3C Wasm Community Group [23]:
INTRODUCTION
• a formal specification for the feature in the form of mathe-
matical rules, written in LaTeX;
• a prose pseudocode description of the feature’s behaviour,
written in reStructuredText markup;
• an implementation of the feature in the Wasm reference
interpreter, written in OCaml; and
• a suite of unit tests for the feature, written in (an enriched
version of) the Wasm text format.Joachim Breitner, Philippa Gardner, Jaehyun Lee, Sam Lindley, Matija Pretnar, Xiaojia Rao, Andreas Rossberg, Sukyoung Ryu, Wonho Shin, Conrad Watt, and Dongjun Youn
SpecTec Files (DSL)
External
(EL)
Representation
parsing
checking, elaboration
LaTeX backend
transforms
Internal
(IL)
Representation
animation
prover backends
Algorithmic
(AL)
Representation
prose backend
Formalism (LaTeX)
AL Interpreter Mechanisations
(Coq/Isabelle/Agda/Lean)
Test Suite / Fuzzer Proof Obligations
Prose (Sphinx)
Figure 1: An overview of Wasm SpecTec
First, a formal specification significantly reduces the risk of under-
defined edge cases. Indeed, if it is also accompanied by formal proofs
of appropriate correctness properties, as has been the case for the
Wasm MVP, certain risks such as type safety violations can be en-
tirely precluded [28, 29]. Second, the prose pseudocode description
is designed to be more accessible to non-experts, similar to other
normative language specifications such as JavaScript’s [5]. Third, a
reference interpreter can often be useful in situations where an opti-
mised implementation in a production engine is not yet available or
is substantially more complex. Finally, the insistence on a compre-
hensive test suite for each newly added feature further guarantees
that various implementations of Wasm exhibit consistent behavior.
This collective effort to include both formal and prose specifica-
tions, reference interpreters, and thorough test suites underscores
the commitment to precision, reliability, and compatibility within
the Wasm standardization process, and serve to reduce the risk of
implementation divergence.
This meticulous process exists as a reaction to past experiences;
historically Web languages have been particularly vulnerable to is-
sues of implementation discrepancy. Leaving aside deliberate breaks
from a Web standard by a browser vendor, discrepancies may occur
inadvertently simply due to the number of different browser im-
plementations in existence, each one in itself consisting of several
tiers of interpretation and just-in-time compilation. Additionally,
developers deploying code on the Web platform have particuarly
limited control over a Web site visitor’s execution environment, am-
plifying the impact of any discrepancies. Portability is only feasible
if implementations are meticulous in aligning their behaviours.
One significant challenge in Wasm’s current standardisation pro-
cess [8] lies in the poor developer experience, where the developer
in question is an author of the specification artefacts described
above. The development of these artefacts has on occasion lagged
significantly behind other aspects of the standardisation process,
delaying the integration of a new proposal into the standard. For ex-
ample the highly anticipated Threads [12] proposal has not yet been
standardized in large part due to specification authoring delays.
The current Wasm specification [6] is authored in reStructured-
Text, a (somewhat cumbersome) markup language, from which
both HTML and PDF documents are generated by the Sphinx docu-
ment processor [19]. The formal pieces of the specification consist
of embedded mathematics that must be expressed in a (severely
restricted) subset of LaTeX; for HTML, it is rendered by MathJax [3].
Wasm specification authors complain of the following significant
difficulties in preparing and maintaining the specification text:
• lack of visual clarity when reading the raw source (com-
plicating code reviews and necessitating repeated lengthy
builds);
• absence of useful abstraction capabilities in Sphinx markup
and in the available LaTeX subset (due to the limitations of
Sphinx and MathJax);
• difficulty in interpreting LaTeX errors (because Sphinx gen-
erates one monolithic file before passing it to LaTeX, de-
stroying line number information); and
• no protection against misuse of definitions (e.g. wrong ar-
guments, incorrect placement, incorrect symbol bindings).
To address these challenges and improve the productivity of
Wasm’s standards developers, we propose a unified domain-specificWasm SpecTec: Engineering a Formal Language Standard
specification language and corresponding toolchain, Wasm SpecTec.
SpecTec will alleviate the burden on developers by conducting meta-
level error checking and automatically generating the required
specification artefacts. Unlike existing general-purpose specifica-
tion languages such as Ott [21], PLTRedex [7], Skeleton [20], the K
framework [26], or Spoofax [22], our solution is unashamedly spe-
cialised to Wasm, both to provide a development experience tailored
to the expectations and needs of Wasm’s standards community, and
to pursue more ambitious analyses and generated outputs which
are only tractable with this more targetted scope. We ultimately
aim for the Wasm standards community to specify all current and
future Wasm features using SpecTec and replace the manually au-
thored artefacts necessary for Wasm’s standardization process with
our generated artefacts, enhancing the standardization process’
efficiency and reliability. Our in-development SpecTec toolchain is
available publicly [16].
(a) Prose specification
(b) Formal specification
Figure 2: The binary operator semantics in the specification
2
WASM SPECTEC
An overview of Wasm SpecTec is illustrated in Figure 1. The Wasm
specification is primarily concerned with defining the binary for-
mat, type system, and runtime behaviour of Wasm. With SpecTec,
an author will write these definitions in our Domain-Specific Lan-
guage (DSL), which the Wasm SpecTec toolchain accepts as input.
This input is parsed as the External Language (EL) representation
and processed into further representations, namely the Internal
Language (IL) representation, and the Algorithmic Language (AL)
representation. Our various backends use these representations
to produce the previously-described output artefacts, as well as
mechanised definitions in interactive theorem provers suitable for
machine-checked proofs about the language semantics [28, 29].
As discussed in §1, the Wasm specification is currently written in
a mixture of reStructuredText and raw LaTeX. Figure 2 presents the
execution semantics of the 𝑡 .binop binary operator instruction in the
Wasm specification [6, Section 4.4], as rendered today. Figure 2(a)
shows the prose pseudocode describing the five execution steps,
and Figure 2(b) shows the mathematics in the gray box for the
corresponding operational semantics. SpecTec aims to provide a
significantly better developer experience without compromising
on the fidelity of the rendered specification. Moving forward, we
will provide a comprehensive breakdown of each step.
SpecTec’s DSL and EL are intended to closely mirror an ASCII
representation of the syntactic constructs used in Wasm’s formal
specification. Figure 3 gives a DSL definition of the runtime se-
mantics of Wasm’s binary arithmetic operator, where $binop is a
separately defined auxiliary function. Crucially, all definitions and
variables in the parsed EL are “type-checked” so that ill-formed
definitions can be detected. For example, if a specification author
misses the final argument of $binop as in $binop(binop, nt, c_1) ,
then an arity-mismatch error will be raised. From the EL, SpecTec
can directly produce the LaTeX-based formal specification, which is
intended to replace the current specification’s handwritten defini-
tions. Figure 4 is an excerpt from the PDF generated from the LaTeX
translated from Figure 3. Compare this to the original handwritten
LaTeX in Figure 2.
To produce the other artefacts mentioned in Section 1, the SpecTec
definitions are processed further. First, the EL is elaborated into
rule Step_pure/binop-val:
(CONST nt c_1) (CONST nt c_2) (BINOP nt binop) ~> (CONST nt c)
-- if $binop(binop, nt, c_1, c_2) = c
rule Step_pure/binop-trap:
(CONST nt c_1) (CONST nt c_2) (BINOP nt binop) ~> TRAP
-- if $binop(binop, nt, c_1, c_2) = epsilon
Figure 3: The binary operator semantics in SpecTec’s DSL
the IL, suitable for deep analysis and transformation. Among other
things, types and multiplicities of variables are inferred and anno-
tated in the IL, mutually recursive definitions are identified, and
implicit upcasts are made explicit and disambiguated. As Figure 1
illustrates, the IL can undergo internal transformations to meet the
needs of subsequent backends. For example, in the EL expressions
are modelled as relations that can fail or can denote multiple values,
whereas various theorem prover backends require that expressions
must be purely functional, i.e. must denote exactly one value given
values for all free variables. Figure 5 is an excerpt from the code gen-
erated for the Lean theorem prover [4]. We are currently working
on similarly generating code for Coq, Isabelle, and Agda.
The operational semantics of Wasm described in the IL is further
transformed into the more restricted AL, which does not allow
arbitrary relational definitions and enforces an algorithmic order
of evaluation. The problem of transforming a relational definition
into an executable, algorithmic one is known as animation [2]. At
its core, the process of animation involves performing a dataflow
analysis on a relational definition to infer which equations of the
relational definition should be interpreted as binding new variables,
and ensures that these binding definitions can be ordered such that
each binding definition only depends on prior animated definitions.
Figure 6 shows how the declarative specification of the binary
operator semantics from Figure 3 is translated to the algorith-
mic version. Note that the implicit conditions guaranteed by the
Wasm validation phase are explicitly added as assertions such as
AssertI(TopValueC(NameE(nt))) . Interestingly, two equality expres-
sions are translated to different AL constructs. Because the equalityJoachim Breitner, Philippa Gardner, Jaehyun Lee, Sam Lindley, Matija Pretnar, Xiaojia Rao, Andreas Rossberg, Sukyoung Ryu, Wonho Shin, Conrad Watt, and Dongjun Youn
(nt.const c 1 )
if binop nt (c 1 ,
[ E-binop-trap ] (nt.const c 1 )
if binop nt (c 1 ,
[ E-binop-val ]
(nt.const c 2 ) (nt.binop)
c 2 ) = c
(nt.const c 2 ) (nt.binop)
c 2 ) = 𝜖
↩→ (nt.const c)
↩→ trap
Figure 4: The binary operator semantics in a generated PDF
| binop_val (binop : Binop_numtype) (c : C_numtype) (c_1 : C_numtype)
(c_2 : C_numtype) (nt : Numtype) :
((«$binop» (binop, nt, c_1, c_2)) == [c]) ->
(Step_pure ([(Admininstr.CONST (nt, c_1)),
(Admininstr.CONST (nt, c_2)),
(Admininstr.BINOP (nt, binop))],
[(Admininstr.CONST (nt, c))]))
| binop_trap (binop : Binop_numtype) (c_1 : C_numtype)
(c_2 : C_numtype) (nt : Numtype) :
((«$binop» (binop, nt, c_1, c_2)) == []) ->
(Step_pure ([(Admininstr.CONST (nt, c_1)),
(Admininstr.CONST (nt, c_2)),
(Admininstr.BINOP (nt, binop))],
[Admininstr.TRAP]))
Figure 5: The binary operator semantics in generated Lean
execution_of_BINOP_ainstr NameE(nt) NameE(binop):
AssertI(TopValueC(NameE(nt)))
PopI(ConstructE(CONST_ainstr, [NameE(nt), NameE(c_2)]))
AssertI(TopValueC(NameE(nt)))
PopI(ConstructE(CONST_ainstr, [NameE(nt), NameE(c_1)]))
IfI(
CompareC(is, LengthE(AppE(binop, [NameE(binop), NameE(nt),
NameE(c_1), NameE(c_2)])), 1),
[LetI(ListE([NameE(c)]),
AppE(binop, [NameE(binop), NameE(nt),
NameE(c_1), NameE(c_2)]))
PushI(ConstructE(CONST_ainstr, [NameE(nt), NameE(c)]))],
[])
IfI(
CompareC(is, AppE(binop, [NameE(binop), NameE(nt),
NameE(c_1), NameE(c_2)]), ListE([])),
[TrapI],
[])
Figure 6: The binary operator semantics in SpecTec’s AL
“ if $binop(binop, nt, c_1, c_2) = c ” is a binding that binds the
result of the $binop call to c , it is translated as a let instruction:
LetI(ListE([NameE(c)]),
AppE(binop, [NameE(binop), NameE(nt),
NameE(c_1), NameE(c_2)]))
On the contrary, since “ if $binop(binop, nt, c_1, c_2) = epsilon ”
is an equality check which is inferred to bind no new variable, it is
translated as a conditional expression:
CompareC(is, AppE(binop, [NameE(binop), NameE(nt),
NameE(c_1), NameE(c_2)]),
ListE([]))
From the AL, we directly generate a prose pseudocode spec-
ification. Figure 7 shows the prose pseudocode generated from
the specification in Figure 6, which is strikingly close to the origi-
nal handwritten prose description in Figure 2. We also implement
an interpreter for the AL. By interpreting AL that represents the
Wasm semantics, we indirectly obtain an interpreter for Wasm.
This technique was previously used by JISET [1, 18] to extract an
Figure 7: The binary operator semantics in generated prose
executable semantics from the ECMAScript prose that represents
the official JavaScript specification [5], and we use it here to extract
an executable semantics for Wasm, from the SpecTec AL.
Currently, Wasm SpecTec covers all of Wasm 2.0 except for the
recently-standardized SIMD vector instructions. Within one second,
our toolchain can automatically generate both prose pseudocode
and operational semantics in LaTeX with hyperlinks and cross-
references in the generated PDF document, and a Lean mechaniza-
tion. We tested the extracted Wasm semantics against the official
Wasm unit test suite on an Ubuntu machine with a 4.0GHz Intel(R)
Core(TM) i7-6700k and 32GB of RAM (Samsung DDR4 2133MHz
8GB*4). On this machine, the extracted semantics passed all 23,778
tests (SIMD excluded) in the test suite in 21.349 seconds.
3
FUTURE PLANS
The key measure of SpecTec’s success is its level of adoption and
ongoing support by the industrial stakeholders of the WebAssembly
Community Group. Our ultimate aim is for the normative definition
of Wasm to be written using SpecTec, and for all of the specification
artefacts which are currently manually generated and maintained
separately to be instead automatically generated from this SpecTec
definition as a single source of truth.
We now plan to gather feedback from industrial stakeholders,
and evaluate how easily we can extend our definitions written
in SpecTec to cover additional features. Wasm 3.0, an upcoming
edition of the specification, may include Exception Handling [10],
Garbage Collected Types [11], and Threads [12]. Because these
features contain far more ambitious extensions to the Wasm virtual
machine, and are expected to lay the groundwork on which many
future proposals will be built, investigating the extent to which our
SpecTec definitions can be extended to cover these features would
be the strongest possible validation of our approach. The associated
changes to the Wasm virtual machine will be wide ranging enough
that we expect modifications to SpecTec itself may be necessary
to make it sufficiently expressive, although we are already mak-
ing a best effort to anticipate the future effects of these proposals
in our current design. Succeeding in expressing all of these fea-
tures as SpecTec definitions would be a strong signal to industry
stakeholders that SpecTec can be seriously considered for official
adoption.Wasm SpecTec: Engineering a Formal Language Standard
4
CONCLUSION
We have presented Wasm SpecTec, a technology for automatically
generating various artefacts from a single source of truth, written
in the Wasm specification DSL. We hope to replace the artefacts of
the Wasm specification process which are today onerously crafted
by hand with those generated by Wasm SpecTec. This approach
will facilitate the standardisation of future Wasm features while
improving the consistency and trustworthiness of Wasm’s various
specification artefacts. We also believe that SpecTec will facilitate
the production of trustworthy mechanizations in diverse theorem
provers, including Coq, Isabelle, Agda, and Lean. While SpecTec is
still currently in development, it is already capable of generating a
formal specification and prose pseudocode covering all of Wasm
2.0 minus the SIMD instructions, and an extracted Wasm seman-
tics which passes all 23,778 applicable tests in the official Wasm
test suite. We continue to work on further backends for automati-
cally generating unit tests and full theorem prover definitions. We
intend to use upcoming Wasm features such as Exception Han-
dling, Garbage-Collected Types, and Threads to further evaluate
the utility and applicability of SpecTec. We acknowledge that a key
challenge moving forward will be transitioning SpecTec from a
research tool to a robust and maintainable part of the Wasm indus-
try standards ecosystem, and we intend to work with key Wasm
industry stakeholders to achieve this goal.
REFERENCES
[1] 2022. ESMeta: An ECMAScript specification metalanguage used for automatically
generating language-based tools. https://github.com/es-meta/esmeta
[2] Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann. 2009. Turning Inductive
into Equational Specifications. In Proceedings of the 22nd International Conference
on Theorem Proving in Higher Order Logics (TPHOLs ’09). Springer-Verlag, Berlin,
Heidelberg, 131–146. https://doi.org/10.1007/978-3-642-03359-9_11
[3] The MathJax Consortium. 2009. MathJax. https://www.mathjax.org/
[4] Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn,
and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description).
In CADE. https://api.semanticscholar.org/CorpusID:232990
[5] ECMA International. 2023. ECMA-262, 14th edition, ECMAScript ®2023 Language
Specification. https://262.ecma-international.org
[6] Andreas Rossberg (editor). 2022. WebAssembly Specification (Release 2.0). https:
//webassembly.github.io/spec/core/
[7] Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics
Engineering with PLT Redex. The MIT Press.
[8] WebAssembly Community Group. 2017. WebAssembly W3C Process. https:
//github.com/WebAssembly/meetings/blob/main/process/phases.md
[9] WebAssembly Community Group. 2021.
SIMD.
https://github.com/
WebAssembly/simd
[10] WebAssembly Community Group. 2023. Exception Handling. https://github.
com/WebAssembly/exception-handling
[11] WebAssembly Community Group. 2023. GC types.
https://github.com/
WebAssembly/gc
https://github.com/
[12] WebAssembly Community Group. 2023. Threads.
WebAssembly/threads
[13] Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman,
Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the
Web up to Speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN
Conference on Programming Language Design and Implementation. Association
for Computing Machinery, New York, NY, USA, 185–200. https://doi.org/10.
1145/3062341.3062363
[14] Adam Hall and Umakishore Ramachandran. 2019. An Execution Model for
Serverless Functions at the Edge. In Proceedings of the International Conference
on Internet of Things Design and Implementation. Association for Computing Ma-
chinery, New York, NY, USA, 225–236. https://doi.org/10.1145/3302505.3310084
[15] Pat Hickey. 2019.
Lucet Takes WebAssembly Beyond the Browser.
https://www.fastly.com/blog/announcing-lucet-fastly-native-webassembly-
compiler-runtime
[16] Joachim Breitner and Philippa Gardner and Jaehyun Lee and Sam Lindley and
Matija Pretnar and Xiaojia Rao and Andreas Rossberg and Sukyoung Ryu and
Wonho Shin Conrad Watt and Dongjun Youn. 2023. Wasm SpecTec Specification
Tools. https://github.com/Wasm-DSL/spectec
WebAssembly is now ready for browsers to use.
[17] Paul Krill. 2017.
https://www.infoworld.com/article/3176681/webassembly-is-now-ready-
for-browsers-to-use.html
[18] Jihyeok Park, Jihee Park, Seungmin An, and Sukyoung Ryu. 2020. JISET:
JavaScript IR-based Semantics Extraction Toolchain. In Proceedings of the 35th
IEEE/ACM International Conference on Automated Software Engineering (ASE).
IEEE, 647–658. https://doi.org/10.1145/3324884.3416632
[19] Sphinx Project. 2008. Sphinx. https://www.sphinx-doc.org/
[20] Alan Schmitt. 2019. Skeletal Semantics. https://skeletons.inria.fr/
[21] Peter Sewell and Francesco Zappa Nardelli. 2007. Ott release, version 0.10.9.
http://www.cl.cam.ac.uk/~pes20/ott/
[22] Spoofax Team. 2010. Spoofax: The Language Designer’s Workbench. https:
//spoofax.dev
[23] W3C Team. 2015. WebAssembly Community Group. https://www.w3.org/
community/webassembly/
[24] Ata Tekeli. 2022. WebAssembly (WASM) in Blockchain. https://blog.devgenius.
io/webassembly-wasm-in-blockchain-f651a8ac767b
[25] Kenton Varda. 2017. Introducing Cloudflare Workers: Run JavaScript Service Work-
ers at the Edge. https://blog.cloudflare.com/introducing-cloudflare-workers/
[26] Runtime Verification. 2013. K Semantic Framework. https://kframework.org/
[27] Stefan Wallentowitz, Bastian Kersting, and Dan Mihai Dumitriu. 2022. Potential
of WebAssembly for Embedded Systems. In 2022 11th Mediterranean Conference
on Embedded Computing (MECO). 1–4. https://doi.org/10.1109/MECO55406.2022.
9797106
[28] Conrad Watt. 2018. Mechanising and verifying the WebAssembly specifica-
tion. Proceedings of the 7th ACM SIGPLAN International Conference on Certified
Programs and Proofs (2018). https://dl.acm.org/doi/10.1145/3167082
[29] Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa
Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Proceedings of the
24 th international symposium of Formal Methods (FM21), Beijing, China; November
20-25, 2021 (Lecture Notes in Computer Science, Vol. 13047), Marieke Huisman,
Corina S. Pasareanu, and Naijun Zhan (Eds.). Springer, 61–79. https://doi.org/
10.1007/978-3-030-90870-6_4

loading