diff --git a/document/core/intro/introduction.rst b/document/core/intro/introduction.rst index 6c9b058974..4819dbdd76 100644 --- a/document/core/intro/introduction.rst +++ b/document/core/intro/introduction.rst @@ -5,7 +5,7 @@ WebAssembly (abbreviated Wasm [#wasm]_) is a *safe, portable, low-level code for designed for efficient execution and compact representation. Its main goal is to enable high performance applications on the Web, but it does not make any Web-specific assumptions or provide Web-specific features, so it can be employed in other environments as well. -WebAssembly is an open standard developed by a `W3C Community Group `_ that includes representatives of all major browser vendors. +WebAssembly is an open standard developed by a `W3C Community Group `_. This document describes version |release| of the :ref:`core ` WebAssembly standard. It is intended that it will be superseded by new incremental releases with additional features in the future. diff --git a/document/core/syntax/conventions.rst b/document/core/syntax/conventions.rst index bb1fba797c..a1aec4214f 100644 --- a/document/core/syntax/conventions.rst +++ b/document/core/syntax/conventions.rst @@ -41,9 +41,13 @@ The following conventions are adopted in defining grammar rules for abstract syn +.. _notation-epsilon: +.. _notation-length: +.. _notation-index: .. _notation-slice: .. _notation-replace: .. _notation-record: +.. _notation-project: .. _notation-concat: .. _notation-compose: diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 6898fb59ee..012eff4c33 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -49,7 +49,7 @@ Result Types ~~~~~~~~~~~~ *Result types* classify the result of :ref:`executing ` :ref:`instructions ` or :ref:`blocks `, -which is a sequence of values. +which is a sequence of values written with brackets. .. math:: \begin{array}{llll} @@ -71,7 +71,7 @@ Function Types ~~~~~~~~~~~~~~ *Function types* classify the signature of :ref:`functions `, -mapping a vector of parameters to a vector of results. +mapping a vector of parameters to a vector of results, written as follows. .. math:: \begin{array}{llll} diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index d649bd2911..c52a3872c7 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -476,9 +476,8 @@ When omitted, :math:`\T{0}` is assumed. .. math:: \begin{array}{llclll} \production{element segment} & \Telem_I &::=& - \text{(}~\text{elem}~~(x{:}\Ttableidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETABLE~x', \EOFFSET~e, \EINIT~y^\ast \} \\ - &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\ + \text{(}~\text{elem}~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ \end{array} .. note:: @@ -498,6 +497,16 @@ As an abbreviation, a single instruction may occur in place of the offset: \text{(}~\text{offset}~~\Tinstr~\text{)} \end{array} +Also, the table index can be omitted, defaulting to :math:`0`. + +.. math:: + \begin{array}{llclll} + \production{element segment} & + \text{(}~\text{elem}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + &\equiv& + \text{(}~\text{elem}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + \end{array} + As another abbreviation, element segments may also be specified inline with :ref:`table ` definitions; see the respective section. @@ -518,9 +527,8 @@ The data is written as a :ref:`string `, which may be split up into .. math:: \begin{array}{llclll} \production{data segment} & \Tdata_I &::=& - \text{(}~\text{data}~~(x{:}\Tmemidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\ - &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\[1ex] + \text{(}~\text{data}~~x{:}\Tmemidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\[1ex] \production{data string} & \Tdatastring &::=& (b^\ast{:}\Tstring)^\ast \quad\Rightarrow\quad \concat((b^\ast)^\ast) \\ \end{array} @@ -542,6 +550,16 @@ As an abbreviation, a single instruction may occur in place of the offset: \text{(}~\text{offset}~~\Tinstr~\text{)} \end{array} +Also, the memory index can be omitted, defaulting to :math:`0`. + +.. math:: + \begin{array}{llclll} + \production{data segment} & + \text{(}~\text{data}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + &\equiv& + \text{(}~\text{data}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + \end{array} + As another abbreviation, data segments may also be specified inline with :ref:`memory ` definitions; see the respective section. diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 5ed7789a7c..9e5f6f182b 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -40,14 +40,14 @@ which collects relevant information about the surrounding :ref:`module ` for each :ref:`index space `, describing each defined entry in that space. Locals, labels and return type are only used for validating :ref:`instructions ` in :ref:`function bodies `, and are left empty elsewhere. The label stack is the only part of the context that changes as validation of an instruction sequence proceeds. -It is convenient to define contexts as :ref:`records ` :math:`C` with abstract syntax: +More concretely, contexts are defined as :ref:`records ` :math:`C` with abstract syntax: .. math:: \begin{array}{llll} @@ -64,22 +64,18 @@ It is convenient to define contexts as :ref:`records ` :math:`C \end{array} \end{array} -.. note:: - The fields of a context are not defined as :ref:`vectors `, - since their lengths are not bounded by the maximum vector size. +.. _notation-extend: -In addition to field access :math:`C.\K{field}` the following notation is adopted for manipulating contexts: +In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts: * When spelling out a context, empty fields are omitted. * :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. .. note:: - This notation is defined to *prepend* not *append*. - It is only used in situations where the original :math:`C.\K{field}` is either empty - or :math:`\K{field}` is :math:`\K{labels}`. - In the latter case adding to the front is desired - because the :ref:`label index ` space is indexed relatively, that is, in reverse order of addition. + We use :ref:`indexing notation ` like :math:`C.\CLABELS[i]` to look up indices in their respective :ref:`index space ` in the context. + Context extension notation :math:`C,\K{field}\,A` is primarily used to locally extend *relative* index spaces, such as :ref:`label indices `. + Accordingly, the notation is defined to append at the *front* of the respective sequence, introducing a new relative index :math:`0` and shifting the existing ones. .. _valid-notation-textual: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ffc308ff29..a6e3845cd0 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -314,7 +314,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32] \to [t]`. @@ -354,7 +354,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t] \to []`. @@ -483,6 +483,8 @@ Control Instructions } .. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others. + The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the block was entered. This may be generalized in future versions of WebAssembly. @@ -507,6 +509,8 @@ Control Instructions } .. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others. + The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the loop was entered. This may be generalized in future versions of WebAssembly. @@ -536,6 +540,8 @@ Control Instructions } .. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others. + The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the conditional was entered. This may be generalized in future versions of WebAssembly. @@ -559,6 +565,8 @@ Control Instructions } .. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + The |BR| instruction is :ref:`stack-polymorphic `. @@ -580,6 +588,9 @@ Control Instructions C \vdashinstr \BRIF~l : [t^?~\I32] \to [t^?] } +.. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + .. _valid-br_table: @@ -608,6 +619,8 @@ Control Instructions } .. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l_i]` performs a relative lookup as expected. + The |BRTABLE| instruction is :ref:`stack-polymorphic `. @@ -616,7 +629,7 @@ Control Instructions :math:`\RETURN` ............... -* The return type :math:`C.\CRETURN` must not be empty in the context. +* The return type :math:`C.\CRETURN` must not be absent in the context. * Let :math:`[t^?]` be the :ref:`result type ` of :math:`C.\CRETURN`. @@ -632,8 +645,8 @@ Control Instructions .. note:: The |RETURN| instruction is :ref:`stack-polymorphic `. - :math:`C.\CRETURN` is empty (:math:`\epsilon`) when validating an :ref:`expression ` that is not a function body. - This differs from it being set to the empty result type (:math:`[]`), + :math:`C.\CRETURN` is absent (set to :math:`\epsilon`) when validating an :ref:`expression ` that is not a function body. + This differs from it being set to the empty result type (:math:`[\epsilon]`), which is the case for functions not returning anything. @@ -773,7 +786,7 @@ Constant Expressions \frac{ (C \vdashinstrconst \instr \const)^\ast }{ - C \vdashexprconst \instr~\END \const + C \vdashexprconst \instr^\ast~\END \const } .. math:: @@ -789,4 +802,7 @@ Constant Expressions } .. note:: + Currently, constant expressions occurring as initializers of :ref:`globals ` are further constrained in that contained |GETGLOBAL| instructions are only allowed to refer to *imported* globals. + This is enforced in the :ref:`validation rule for modules ` by constraining the context :math:`C` accordingly. + The definition of constant expression may be extended in future versions of WebAssembly. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 6dc45a687b..78e99e77ea 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -129,7 +129,7 @@ Globals :math:`\global` are classified by :ref:`global types \qquad C \vdashexpr \expr : [t] \qquad - C \vdashexprconst \expr ~\F{const} + C \vdashexprconst \expr \const }{ C \vdashglobal \{ \GTYPE~\mut~t, \GINIT~\expr \} : \mut~t } @@ -172,7 +172,7 @@ Element segments :math:`\elem` are not classified by a type. \qquad C \vdashexpr \expr : [\I32] \qquad - C \vdashexprconst \expr ~\F{const} + C \vdashexprconst \expr \const \qquad (C.\CFUNCS[y] = \functype)^\ast }{ @@ -210,7 +210,7 @@ Data segments :math:`\data` are not classified by any type. \qquad C \vdashexpr \expr : [\I32] \qquad - C \vdashexprconst \expr ~\F{const} + C \vdashexprconst \expr \const }{ C \vdashdata \{ \DMEM~x, \DOFFSET~\expr, \DINIT~b^\ast \} \ok } @@ -334,6 +334,9 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi C \vdashexportdesc \EDGLOBAL~x : \ETGLOBAL~(\MCONST~t) } +.. note:: + In future versions of WebAssembly, the restriction to exporting only immutable globals may be removed. + .. index:: import, name, function type, table type, memory type, global type pair: validation; import @@ -425,6 +428,9 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi C \vdashimportdesc \IDGLOBAL~\MCONST~t : \ETGLOBAL~\MCONST~t } +.. note:: + In future versions of WebAssembly, the restriction to importing only immutable globals may be removed. + .. index:: module, type definition, function type, function, table, memory, global, element, data, start function, import, export, context pair: validation; module @@ -447,21 +453,21 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CTYPES` is :math:`\module.\MTYPES`, - * :math:`C.\CFUNCS` is :math:`\etfuncs(\externtype_i^\ast)` concatenated with :math:`\functype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\functype_i^\ast` as determined below, + * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`function types ` :math:`\X{ft}^\ast` as determined below, - * :math:`C.\CTABLES` is :math:`\ettables(\externtype_i^\ast)` concatenated with :math:`\tabletype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\tabletype_i^\ast` as determined below, + * :math:`C.\CTABLES` is :math:`\ettables(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`table types ` :math:`\X{tt}^\ast` as determined below, - * :math:`C.\CMEMS` is :math:`\etmems(\externtype_i^\ast)` concatenated with :math:`\memtype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\memtype_i^\ast` as determined below, + * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`memory types ` :math:`\X{mt}^\ast` as determined below, - * :math:`C.\CGLOBALS` is :math:`\etglobals(\externtype_i^\ast)` concatenated with :math:`\globaltype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\globaltype_i^\ast` as determined below. + * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`global types ` :math:`\X{gt}^\ast` as determined below, * :math:`C.\CLOCALS` is empty, - * :math:`C.\CLABELS` is empty. + * :math:`C.\CLABELS` is empty, * :math:`C.\CRETURN` is empty. @@ -476,15 +482,15 @@ Instead, the context :math:`C` for validation of the module's content is constru the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. * For each :math:`\table_i` in :math:`\module.\MTABLES`, - the definition :math:`\table_i` must be :ref:`valid ` with a :ref:`table type ` :math:`\tabletype_i`. + the definition :math:`\table_i` must be :ref:`valid ` with a :ref:`table type ` :math:`\X{tt}_i`. * For each :math:`\mem_i` in :math:`\module.\MMEMS`, - the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\memtype_i`. + the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: * Under the context :math:`C'`, - the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\globaltype_i`. + the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEM`, the segment :math:`\elem_i` must be :ref:`valid `. @@ -496,10 +502,10 @@ Instead, the context :math:`C` for validation of the module's content is constru then :math:`\module.\MSTART` must be :ref:`valid `. * For each :math:`\import_i` in :math:`\module.\MIMPORTS`, - the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\externtype_i`. + the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\X{it}_i`. * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, - the segment :math:`\import_i` must be :ref:`valid ` with :ref:`external type ` :math:`\externtype'_i`. + the segment :math:`\import_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. * The length of :math:`C.\CTABLES` must not be larger than :math:`1`. @@ -507,11 +513,19 @@ Instead, the context :math:`C` for validation of the module's content is constru * All export names :math:`\export_i.\ENAME` must be different. -* Let :math:`\externtype^\ast` be the concatenation of :ref:`external types ` :math:`\externtype_i` of the imports, in index order. +* Let :math:`\X{ft}^\ast` be the concatenation of the internal :ref:`function types ` :math:`\X{ft}_i`, in index order. + +* Let :math:`\X{tt}^\ast` be the concatenation of the internal :ref:`table types ` :math:`\X{tt}_i`, in index order. + +* Let :math:`\X{mt}^\ast` be the concatenation of the internal :ref:`memory types ` :math:`\X{mt}_i`, in index order. + +* Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types ` :math:`\X{gt}_i`, in index order. + +* Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types ` :math:`\X{it}_i` of the imports, in index order. -* Let :math:`{\externtype'}^\ast` be the concatenation of :ref:`external types ` :math:`\externtype'_i` of the exports, in index order. +* Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types ` :math:`\X{et}_i` of the exports, in index order. -* Then the module is valid with :ref:`external types ` :math:`\externtype^\ast \to {\externtype'}^\ast`. +* Then the module is valid with :ref:`external types ` :math:`\X{it}^\ast \to \X{et}^\ast`. .. math:: \frac{ diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 76c6c70211..89b79a4187 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -54,7 +54,7 @@ Function Types } .. note:: - This restriction may be removed in future versions of WebAssembly. + The restriction to at most one result may be removed in future versions of WebAssembly. .. index:: table type, element type, limits