WebAssembly Specification

Wasm SpecTec is a domain-specific language (DSL) designed for the formal specification of WebAssembly. It provides a unified source for reading, writing, and code-reviewing specifications, while enabling the generation of various artifacts through dedicated backends, such as:

• Latex: For formal specification documents.
• Prose: For pseudo-algorithms.
• Coq/Isabelle: For formal mechanization.
• Interpreter: A reference interpreter.
• Test Suite: To exercise individual rules.

The language supports generic syntax for uninterpreted hint annotations that backends can hook into.

The Typed Function References proposal introduces typed function references that can be called directly without requiring a table. This allows for efficient indirect function calls without runtime checks and enables representing first-class function pointers.

Key features include:

• Regular vs. Nullable References: Regular references (ref $t) cannot be null and do not require runtime checks during calls. Nullable references (ref null $t) can be null.
• Direct Calling: Use call_ref to invoke functions through a typed reference.
• Initialization Tracking: The proposal tracks the initialization status of locals to ensure local.get is only called after a local.set or local.tee has initialized the value.

SpecTec is an authoring tool for the WebAssembly (Wasm) specification designed to maintain a single source of truth for language definitions. It uses a domain-specific language to define syntax and semantics, which can then be automatically generated into multiple formats via different backends:

• Latex: For formal rules.
• reStructuredText: For prose rules.
• Theorem Provers (ongoing): Formulations for tools like Coq.
• Future Backends: Potential support for reference interpreter OCaml code or automatic .wast test generation.

The WebAssembly Garbage Collection (GC) extension provides efficient support for high-level languages by allowing the allocation of garbage-collected data structures and byte arrays. It is designed to be independent of linear memory and focuses on low-level data representation types rather than high-level language object models.

Key capabilities include:

• Allocation of garbage-collected structs and arrays.
• Support for heap values from the embedder (e.g., JavaScript objects).
• Unboxing of small scalar values.
• Explicit low-level control with no implicit allocations or implicit runtime types.
• Modular design that does not require shared type definitions.

Note that basic support for reference types, typed function references, and type imports have been moved to separate proposals which form the basis for this extension.

The Garbage Collection (GC) extension introduces three disjoint hierarchies of heap types:

1. Internal: Values in Wasm representation. The common supertype (top) is any and the common subtype (bottom) is none.
2. External: Values in a host-specific representation. The common supertype is extern and the common subtype is noextern.
3. Functions: The common supertype is func and the common subtype is nofunc.

Additionally, eq is the common supertype for all referenceable types allowing ref.eq comparison. struct and array serve as common supertypes for their respective concrete types.

WebAssembly value types follow specific subtyping rules that form a lattice structure:

• Greatest Lower Bounds (GLB): For any two valid value types, there exists a valid value type that is a subtype of both. This GLB may be \bot.
• Conditional Least Upper Bounds (LUB): Two valid value types either have no common supertype, or there exists a valid value type that is a supertype of both (the LUB).
• Disjoint Hierarchies: Value types are partitioned into disjoint hierarchies. If two types do not have a common supertype, their greatest lower bound is \bot or \REF \bot. Types in different hierarchies can be implemented using mutually incompatible representations because their values can never flow to the same place.

Bulk Memory Operations (like memory.copy) are designed to address performance bottlenecks in WebAssembly benchmarks where memcpy and memset operations are frequently identified as hot functions.

Performance comparisons show that the memory.copy intrinsic can achieve significantly higher throughput (e.g., ~30 Gib/s for 1.0Mib transfers) compared to manual implementations using i64 or i32 load/store loops, which may struggle to exceed 10 Gib/s for similar workloads.

WebAssembly relates its type system to execution semantics through configurations denoted as $S;T$, which link the store ($S$) to execution threads ($T$).

Key components of a valid configuration include:

• Store ($S$): Must be a valid store.
• Threads ($T$): Must be valid under an allowed return type (denoted as $\resulttype^?$). This return type controls which return instructions are permitted. It is absent ($\epsilon$) except within administrative FRAME instructions.
• Frames ($F$): Classified by frame contexts, which extend the module context of the associated module instance with the locals contained within the frame.

A configuration is valid if the store is valid and the thread is valid with a specific result type $[t^*]$.

When implementing host functions or modifying a WebAssembly store, you must ensure that the new store state $S'$ is an extension of the original state $S$. This is critical for maintaining type soundness.

An extension $S \extends S'$ requires that:

1. The lengths of all instance collections (Tags, Globals, Memories, Tables, Functions, Datas, Elements, Structs, Arrays, and Exceptions) must not shrink.
2. Every existing instance in the original store must be replaced by an extension of itself in the new store.

Note: An extension does not automatically guarantee that the new store is valid; validity is a separate property that must be maintained.