[spec] Proper binary format for element segments (#82)

The element segment binary format allows for `ref.null` as well as
`ref.func`.

TODO: text format

Author: binji

document/core/binary/modules.rst

@@ -314,6 +314,7 @@ It decodes into an optional :ref:`start function <syntax-start>` that represents
    single: element; segment
 .. _binary-elem:
 .. _binary-elemsec:
+.. _binary-elemexpr:
 
 Element Section
 ~~~~~~~~~~~~~~~
@@ -327,13 +328,14 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
      \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\
    \production{element segment} & \Belem &::=&
      \hex{00}~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETABLE~0, \EOFFSET~e, \EINIT~y^\ast \} \\
-   \production{element segment} & \Belem &::=&
-     \hex{01}~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \EINIT~y^\ast \} \\
-   \production{element segment} & \Belem &::=&
+       &\Rightarrow& \{ \ETABLE~0, \EOFFSET~e, \EINIT~((\REFFUNC~y)~\END)^\ast \} \\ &&|&
+     \hex{01}~~e^\ast{:}\Bvec(\Belemexpr)
+       &\Rightarrow& \{ \EINIT~e^\ast \} \\ &&|&
      \hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\
+       &\Rightarrow& \{ \ETABLE~x, \EOFFSET~e, \EINIT~((\REFFUNC~y)~\END)^\ast \} \\
+   \production{elemexpr} & \Belemexpr &::=&
+     \hex{D0}~\hex{0B} &\Rightarrow& \REFNULL~\END \\ &&|&
+     \hex{D2}~x{:}\Bfuncidx~\hex{0B} &\Rightarrow& (\REFFUNC~x)~\END \\
    \end{array}
 
 .. note::
@@ -419,11 +421,9 @@ It decodes into a vector of :ref:`data segments <syntax-data>` that represent th
      \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg} \\
    \production{data segment} & \Bdata &::=&
      \hex{00}~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte)
-       &\Rightarrow& \{ \DMEM~0, \DOFFSET~e, \DINIT~b^\ast \} \\
-   \production{data segment} & \Bdata &::=&
+       &\Rightarrow& \{ \DMEM~0, \DOFFSET~e, \DINIT~b^\ast \} \\ &&|&
      \hex{01}~~b^\ast{:}\Bvec(\Bbyte)
-       &\Rightarrow& \{ \DINIT~b^\ast \} \\
-   \production{data segment} & \Bdata &::=&
+       &\Rightarrow& \{ \DINIT~b^\ast \} \\ &&|&
      \hex{02}~~x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte)
        &\Rightarrow& \{ \DMEM~x, \DOFFSET~e, \DINIT~b^\ast \} \\
    \end{array}

document/core/syntax/modules.rst

@@ -247,6 +247,7 @@ starting with the smallest index not referencing a global :ref:`import <syntax-i
    single: table; element
    single: element; segment
 .. _syntax-elem:
+.. _syntax-elemexpr:
 
 Element Segments
 ~~~~~~~~~~~~~~~~
@@ -260,8 +261,11 @@ The |MELEM| component of a module defines a vector of element segments. Each act
 .. math::
    \begin{array}{llll}
    \production{element segment} & \elem &::=&
-     \{ \ETABLE~\tableidx, \EOFFSET~\expr, \EINIT~\vec(\funcidx) \} \\&&|&
-     \{ \EINIT~\vec(\funcidx) \} \\
+     \{ \ETABLE~\tableidx, \EOFFSET~\expr, \EINIT~\vec(\elemexpr) \} \\&&|&
+     \{ \EINIT~\vec(\elemexpr) \} \\
+   \production{elemexpr} & \elemexpr &::=&
+     \REFNULL~\END \\&&|&
+     (\REFFUNC~\funcidx)~\END \\
    \end{array}
 
 The |EOFFSET| is given by a :ref:`constant <valid-constant>` :ref:`expression <syntax-expr>`.

document/core/util/macros.def

@@ -267,6 +267,9 @@
 .. |EOFFSET| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{offset}}
 .. |EINIT| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{init}}
 
+.. |REFNULL| mathdef:: \xref{syntax/modules}{syntax-elemexpr}{\K{ref.null}}
+.. |REFFUNC| mathdef:: \xref{syntax/modules}{syntax-elemexpr}{\K{ref.func}}
+
 .. |DMEM| mathdef:: \xref{syntax/modules}{syntax-data}{\K{data}}
 .. |DOFFSET| mathdef:: \xref{syntax/modules}{syntax-data}{\K{offset}}
 .. |DINIT| mathdef:: \xref{syntax/modules}{syntax-data}{\K{init}}
@@ -302,6 +305,7 @@
 .. |importdesc| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\X{importdesc}}
 .. |exportdesc| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\X{exportdesc}}
 .. |elem| mathdef:: \xref{syntax/modules}{syntax-elem}{\X{elem}}
+.. |elemexpr| mathdef:: \xref{syntax/modules}{syntax-elemexpr}{\X{elemexpr}}
 .. |data| mathdef:: \xref{syntax/modules}{syntax-data}{\X{data}}
 .. |start| mathdef:: \xref{syntax/modules}{syntax-start}{\X{start}}
 
@@ -529,6 +533,7 @@
 .. |Bimportdesc| mathdef:: \xref{binary/modules}{binary-importdesc}{\B{importdesc}}
 .. |Bexportdesc| mathdef:: \xref{binary/modules}{binary-exportdesc}{\B{exportdesc}}
 .. |Belem| mathdef:: \xref{binary/modules}{binary-elem}{\B{elem}}
+.. |Belemexpr| mathdef:: \xref{binary/modules}{binary-elemexpr}{\B{elemexpr}}
 .. |Bcode| mathdef:: \xref{binary/modules}{binary-code}{\B{code}}
 .. |Blocal| mathdef:: \xref{binary/modules}{binary-local}{\B{local}}
 .. |Blocals| mathdef:: \xref{binary/modules}{binary-local}{\B{locals}}
@@ -773,6 +778,7 @@
 .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash}
 .. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash}
 .. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash}
+.. |vdashelemexpr| mathdef:: \xref{valid/modules}{valid-elemexpr}{\vdash}
 .. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\vdash}
 .. |vdashstart| mathdef:: \xref{valid/modules}{valid-start}{\vdash}
 .. |vdashexport| mathdef:: \xref{valid/modules}{valid-export}{\vdash}

document/core/valid/modules.rst

@@ -147,7 +147,7 @@ Element Segments
 
 Element segments :math:`\elem` are classified by :ref:`segment types <syntax-segtype>`.
 
-:math:`\{ \ETABLE~x, \EOFFSET~\expr, \EINIT~y^\ast \}`
+:math:`\{ \ETABLE~x, \EOFFSET~\expr, \EINIT~e^\ast \}`
 ......................................................
 
 * The table :math:`C.\CTABLES[x]` must be defined in the context.
@@ -160,8 +160,9 @@ Element segments :math:`\elem` are classified by :ref:`segment types <syntax-seg
 
 * The expression :math:`\expr` must be :ref:`constant <valid-constant>`.
 
-* For each :math:`y_i` in :math:`y^\ast`,
-  the function :math:`C.\CFUNCS[y]` must be defined in the context.
+* For each :math:`e_i` in :math:`e^\ast`,
+
+  * The element expression :math:`e_i` must be :ref:`valid <valid-elemexpr>`.
 
 * Then the element segment is valid with type |SACTIVE|.
 
@@ -174,26 +175,51 @@ Element segments :math:`\elem` are classified by :ref:`segment types <syntax-seg
      \qquad
      C \vdashexprconst \expr \const
      \qquad
-     (C.\CFUNCS[y] = \functype)^\ast
+     (C \vdashelemexpr e \ok)^\ast
    }{
-     C \vdashelem \{ \ETABLE~x, \EOFFSET~\expr, \EINIT~y^\ast \} : \SACTIVE
+     C \vdashelem \{ \ETABLE~x, \EOFFSET~\expr, \EINIT~e^\ast \} : \SACTIVE
    }
 
 
-:math:`\{ \EINIT~y^\ast \}`
-......................................................
+:math:`\{ \EINIT~e^\ast \}`
+...........................
 
-* For each :math:`y_i` in :math:`y^\ast`,
-  the function :math:`C.\CFUNCS[y]` must be defined in the context.
+* For each :math:`e_i` in :math:`e^\ast`,
+
+  * The element expression :math:`e_i` must be :ref:`valid <valid-elemexpr>`.
 
 * Then the element segment is valid with type |SPASSIVE|.
 
 
 .. math::
    \frac{
-     (C.\CFUNCS[y] = \functype)^\ast
+     (C \vdashelemexpr e \ok)^\ast
+   }{
+     C \vdashelem \{ \EINIT~e^\ast \} : \SPASSIVE
+   }
+
+
+.. _valid-elemexpr:
+
+:math:`\elemexpr`
+.................
+
+* An element expression must be:
+
+  * either of the form :math:`\REFNULL~\END`,
+
+  * or of the form :math:`(\REFFUNC~x)~\END`, in which case :math:`C.\CFUNCS[x]` must be defined in the context.
+
+.. math::
+   \frac{
+   }{
+     C \vdashelemexpr \REFNULL~\END \ok
+   }
+   \qquad
+   \frac{
+     C.\CFUNCS[x] = \functype
    }{
-     C \vdashelem \{ \EINIT~y^\ast \} : \SPASSIVE
+     C \vdashelemexpr (\REFFUNC~x)~\END \ok
    }