[spec] Document validation (WebAssembly#16)

document/core/syntax/instructions.rst

@@ -265,7 +265,7 @@ The |MEMORYSIZE| instruction returns the current size of a memory.
 The |MEMORYGROW| instruction grows memory by a given delta and returns the previous size, or :math:`-1` if enough memory cannot be allocated.
 Both instructions operate in units of :ref:`page size <page-size>`.
 
-The |MEMORYINIT| instruction copies data from a :ref:`passive data segment <syntax-activeness>` into a memory.
+The |MEMORYINIT| instruction copies data from a :ref:`passive data segment <syntax-data>` into a memory.
 The |MEMORYDROP| instruction prevents further use of a passive data segment. This instruction is intended to be used as an optimization hint. After a data segment is dropped its data can no longer be retrieved, so the memory used by this segment may be freed.
 The |MEMORYCOPY| instruction copies data from a source memory region to a possibly overlapping destination region.
 The |MEMORYFILL| instruction sets all values in a region to a given byte.
@@ -294,7 +294,7 @@ Instructions in this group are concerned with tables :ref:`table <syntax-table>`
      \TABLECOPY \\
    \end{array}
 
-The |TABLEINIT| instruction copies elements from a :ref:`passive element segment <syntax-activeness>` into a table.
+The |TABLEINIT| instruction copies elements from a :ref:`passive element segment <syntax-elem>` into a table.
 The |TABLEDROP| instruction prevents further use of a passive element segment. This instruction is intended to be used as an optimization hint. After an element segment is dropped its elements can no longer be retrieved, so the memory used by this segment may be freed.
 The |TABLECOPY| instruction copies elements from a source table region to a possibly overlapping destination region.
 

document/core/syntax/modules.rst

@@ -9,7 +9,7 @@ WebAssembly programs are organized into *modules*,
 which are the unit of deployment, loading, and compilation.
 A module collects definitions for :ref:`types <syntax-type>`, :ref:`functions <syntax-func>`, :ref:`tables <syntax-table>`, :ref:`memories <syntax-mem>`, and :ref:`globals <syntax-global>`.
 In addition, it can declare :ref:`imports <syntax-import>` and :ref:`exports <syntax-export>`
-and provide initialization logic in the form of active and passive :ref:`data <syntax-data>` and :ref:`element <syntax-elem>` segments, or a :ref:`start function <syntax-start>`.
+and provide initialization in the form of :ref:`active <syntax-active>` and :ref:`passive <syntax-passive>` :ref:`data <syntax-data>` and :ref:`element <syntax-elem>` segments, or a :ref:`start function <syntax-start>`.
 
 .. math::
    \begin{array}{lllll}
@@ -228,7 +228,7 @@ Globals are referenced through :ref:`global indices <syntax-globalidx>`,
 starting with the smallest index not referencing a global :ref:`import <syntax-import>`.
 
 
-.. index:: ! element, ! active, ! passive, element index, table, table index, expression, constant, function index, vector
+.. index:: ! element, active, passive, element index, table, table index, expression, constant, function index, vector
    pair: abstract syntax; element
    single: table; element
    single: element; segment
@@ -239,7 +239,7 @@ Element Segments
 
 The initial contents of a table is uninitialized. *Element segments* can be used to initialize a subrange of a table from a static :ref:`vector <syntax-vec>` of elements.
 
-Element segments can be *active* or *passive*. An active element segment copies its elements into a table during :ref:`instantiation <exec-instantiation>`. A passive element segment's elements can be copied using the |TABLEINIT| instruction.
+Element segments can be :ref:`active <syntax-active>` or :ref:`passive <syntax-passive>`. An active element segment copies its elements into a table during :ref:`instantiation <exec-instantiation>`. A passive element segment's elements can be copied using the |TABLEINIT| instruction.
 
 The |MELEM| component of a module defines a vector of element segments. Each active element segment defines the |ETABLE| and the starting |EOFFSET| in that table to initialize. Each passive element segment only defines its contents.
 
@@ -270,7 +270,7 @@ Data Segments
 
 The initial contents of a :ref:`memory <syntax-mem>` are zero bytes. *Data segments* can be used to initialize a range of memory from a static :ref:`vector <syntax-vec>` of :ref:`bytes <syntax-byte>`.
 
-Like element segments, data segments can be active or passive. An active data segment copies its contents into a table during :ref:`instantiation <exec-instantiation>`. A passive data segment's contents can be copied using the |MEMORYINIT| instruction.
+Like element segments, data segments can be :ref:`active <syntax-active>` or :ref:`passive <syntax-passive>`. An active data segment copies its contents into a table during :ref:`instantiation <exec-instantiation>`. A passive data segment's contents can be copied using the |MEMORYINIT| instruction.
 
 The |MDATA| component of a module defines a vector of data segments. Each active data segment defines the memory to initialize, and the starting |DOFFSET| in that memory to initialize. Each passive data segment only defines its contents.
 

document/core/syntax/types.rst

@@ -181,6 +181,25 @@ Global Types
    \end{array}
 
 
+.. index:: ! segtype, ! active, ! passive
+   pair: abstract syntax; segtype
+.. _syntax-segtype:
+.. _syntax-active:
+.. _syntax-passive:
+
+Segment Types
+~~~~~~~~~~~~~
+
+*Segment types* classify :ref:`data segments <syntax-data>` and :ref:`element segments <syntax-elem>`, which can either be *active* or *passive*.
+
+.. math::
+   \begin{array}{llll}
+   \production{segment type} & \segtype &::=&
+     \SACTIVE ~|~
+     \SPASSIVE \\
+   \end{array}
+
+
 .. index:: ! external type, function type, table type, memory type, global type, import, external value
    pair: abstract syntax; external type
    pair: external; type

document/core/util/macros.def

@@ -179,6 +179,9 @@
 .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}}
 .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}}
 
+.. |SACTIVE| mathdef:: \xref{syntax/types}{syntax-segtype}{\K{active}}
+.. |SPASSIVE| mathdef:: \xref{syntax/types}{syntax-segtype}{\K{passive}}
+
 .. |ETFUNC| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{func}}
 .. |ETTABLE| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{table}}
 .. |ETMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}}
@@ -194,6 +197,7 @@
 .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
 .. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}}
 .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
+.. |segtype| mathdef:: \xref{syntax/types}{syntax-segtype}{\X{segtype}}
 
 .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
 .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
@@ -723,6 +727,8 @@
 .. |CTABLES| mathdef:: \xref{valid/conventions}{context}{\K{tables}}
 .. |CMEMS| mathdef:: \xref{valid/conventions}{context}{\K{mems}}
 .. |CGLOBALS| mathdef:: \xref{valid/conventions}{context}{\K{globals}}
+.. |CELEM| mathdef:: \xref{valid/conventions}{context}{\K{elem}}
+.. |CDATA| mathdef:: \xref{valid/conventions}{context}{\K{data}}
 .. |CLOCALS| mathdef:: \xref{valid/conventions}{context}{\K{locals}}
 .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
 .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}

document/core/valid/conventions.rst

@@ -38,6 +38,8 @@ which collects relevant information about the surrounding :ref:`module <syntax-m
 * *Tables*: the list of tables declared in the current module, represented by their table type.
 * *Memories*: the list of memories declared in the current module, represented by their memory type.
 * *Globals*: the list of globals declared in the current module, represented by their global type.
+* *Element Segments*: the list of element segments declared in the current module, represented by their segment type.
+* *Data Segments*: the list of data segments declared in the current module, represented by their segment type.
 * *Locals*: the list of locals declared in the current function (including parameters), represented by their value type.
 * *Labels*: the stack of labels accessible from the current position, represented by their result type.
 * *Return*: the return type of the current function, represented as an optional result type that is absent when no return is allowed, as in free-standing expressions.
@@ -58,6 +60,8 @@ More concretely, contexts are defined as :ref:`records <notation-record>` :math:
         & \CTABLES & \tabletype^\ast, \\
         & \CMEMS & \memtype^\ast, \\
         & \CGLOBALS & \globaltype^\ast, \\
+        & \CELEM & \segtype^\ast, \\
+        & \CDATA & \segtype^\ast, \\
         & \CLOCALS & \valtype^\ast, \\
         & \CLABELS & \resulttype^\ast, \\
         & \CRETURN & \resulttype^? ~\} \\

document/core/valid/instructions.rst

@@ -423,6 +423,149 @@ Memory Instructions
    }
 
 
+.. _valid-memory.init:
+
+:math:`\MEMORYINIT~x`
+.....................
+
+* The memory :math:`C.\CMEMS[0]` must be defined in the context.
+
+* The data segment :math:`C.\CDATA[x]` must be defined in the context.
+
+* The :ref:`segment type <syntax-segtype>` :math:`C.\CDATA[x]` must be |SPASSIVE|.
+
+* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
+
+.. math::
+   \frac{
+     C.\CMEMS[0] = \memtype
+     \qquad
+     C.\CDATA[x] = \SPASSIVE
+   }{
+     C \vdashinstr \MEMORYINIT~x : [\I32~\I32~\I32] \to []
+   }
+
+
+.. _valid-memory.drop:
+
+:math:`\MEMORYDROP~x`
+.....................
+
+* The data segment :math:`C.\CDATA[x]` must be defined in the context.
+
+* The :ref:`segment type <syntax-segtype>` :math:`C.\CDATA[x]` must be |SPASSIVE|.
+
+* Then the instruction is valid with type :math:`[] \to []`.
+
+.. math::
+   \frac{
+     C.\CDATA[x] = \SPASSIVE
+   }{
+     C \vdashinstr \MEMORYDROP~x : [] \to []
+   }
+
+
+.. _valid-memory.copy:
+
+:math:`\MEMORYCOPY`
+.....................
+
+* The memory :math:`C.\CMEMS[0]` must be defined in the context.
+
+* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
+
+.. math::
+   \frac{
+     C.\CMEMS[0] = \memtype
+   }{
+     C \vdashinstr \MEMORYCOPY : [\I32~\I32~\I32] \to []
+   }
+
+
+.. _valid-memory.fill:
+
+:math:`\MEMORYFILL`
+.....................
+
+* The memory :math:`C.\CMEMS[0]` must be defined in the context.
+
+* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
+
+.. math::
+   \frac{
+     C.\CMEMS[0] = \memtype
+   }{
+     C \vdashinstr \MEMORYFILL : [\I32~\I32~\I32] \to []
+   }
+
+
+.. index:: table instruction, table index, context
+   pair: validation; instruction
+   single: abstract syntax; instruction
+.. _valid-instr-table:
+
+Table Instructions
+~~~~~~~~~~~~~~~~~~
+
+.. _valid-table.init:
+
+:math:`\TABLEINIT~x`
+.....................
+
+* The table :math:`C.\CTABLES[0]` must be defined in the context.
+
+* The element segment :math:`C.\CELEM[x]` must be defined in the context.
+
+* The :ref:`segment type <syntax-segtype>` :math:`C.\CELEM[x]` must be |SPASSIVE|.
+
+* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
+
+.. math::
+   \frac{
+     C.\CTABLES[0] = \tabletype
+     \qquad
+     C.\CELEM[x] = \SPASSIVE
+   }{
+     C \vdashinstr \TABLEINIT~x : [\I32~\I32~\I32] \to []
+   }
+
+
+.. _valid-table.drop:
+
+:math:`\TABLEDROP~x`
+.....................
+
+* The element segment :math:`C.\CELEM[x]` must be defined in the context.
+
+* The :ref:`segment type <syntax-segtype>` :math:`C.\CELEM[x]` must be |SPASSIVE|.
+
+* Then the instruction is valid with type :math:`[] \to []`.
+
+.. math::
+   \frac{
+     C.\CELEM[x] = \SPASSIVE
+   }{
+     C \vdashinstr \TABLEDROP~x : [] \to []
+   }
+
+
+.. _valid-table.copy:
+
+:math:`\TABLECOPY`
+.....................
+
+* The table :math:`C.\CTABLES[0]` must be defined in the context.
+
+* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
+
+.. math::
+   \frac{
+     C.\CTABLES[0] = \tabletype
+   }{
+     C \vdashinstr \TABLECOPY : [\I32~\I32~\I32] \to []
+   }
+
+
 .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism, context
    pair: validation; instruction
    single: abstract syntax; instruction