WASM 2.0

Summary

2.1. Conventions WebAssembly is a programming language that has multiple concrete representations (its binary format and the text format). Both map to a common structure. For conciseness, this structure is described in the form of an abstract syntax. All parts of this specification are defined in terms of this abstract syntax. 2.1.1. Grammar Notation The following conventions are adopted in defining grammar rules for abstract syntax. Terminal symbols (atoms) are written in sans-serif font or in symbolic form: i32,end,→,[,]. Nonterminal symbols are written in italic font: valtype,instr. An is a sequence of n≥0 iterations of A. A∗ is a possibly empty sequence of iterations of A. (This is a shorthand for An used where n is not relevant.) A+ is a non-empty sequence of iterations of A. (This is a shorthand for An where n≥1.) A? is an optional occurrence of A. (This is a shorthand for An where n≤1.) Productions are written sym::=A1​ ∣ … ∣ An​. Large productions may be split into multiple definitions, indicated by ending the first one with explicit ellipses, sym::=A1​ ∣ …, and starting continuations with ellipses, sym::=… ∣ A2​. Some productions are augmented with side conditions in parentheses, “(ifcondition)”, that provide a shorthand for a combinatorial expansion of the production into many separate cases. If the same meta variable or non-terminal symbol appears multiple times in a production, then all those occurrences must have the same instantiation. (This is a shorthand for a side condition requiring multiple different variables to be equal.) 2.1.2. Auxiliary Notation When dealing with syntactic constructs the following notation is also used: ϵ denotes the empty sequence. ∣s∣ denotes the length of a sequence s. s[i] denotes the i-th element of a sequence s, starting from 0. s[i:n] denotes the sub-sequence s[i] … s[i+n−1] of a sequence s. swith[i]=A denotes the same sequence as s, except that the i-th element is replaced with A. swith[i:n]=An denotes the same sequenc...