Support direct global bindings

Author: Guy Bedford

document/core/appendix/embedding.rst

@@ -137,6 +137,37 @@ Modules
    \F{module\_validate}(m) &=& \ERROR && (\otherwise) \\
    \end{array}
 
+.. index:: matching, external type
+.. _embed-extern-subtype:
+
+:math:`\F{module\_extern\_subtype}(\externtype_1, \externtype_2) : \bool`
+.......................................................................
+
+1. If :math:`\externtype_1` and :math:`\externtype_2` are both of the form :math:`\ETFUNC~\functype_1` and :math:`\ETFUNC~\functype_2` respectively:
+
+   a. Return true if and only if :math:`\vdashexterntypematch \ETFUNC~\functype_1 \matchesexterntype \ETFUNC~\functype_2`.
+
+2. If :math:`\externtype_1` and :math:`\externtype_2` are both of the form :math:`\ETTABLE~\tabletype_1` and :math:`\ETTABLE~\tabletype_2` respectively:
+
+   a. Return true if and only if :math:`\vdashexterntypematch \ETTABLE~\tabletype_1 \matchesexterntype \ETTABLE~\tabletype_2`.
+
+3. If :math:`\externtype_1` and :math:`\externtype_2` are both of the form :math:`\ETMEM~\memtype_1` and :math:`\ETMEM~\memtype_2` respectively:
+
+   a. Return true if and only if :math:`\vdashexterntypematch \ETMEM~\memtype_1 \matchesexterntype \ETMEM~\memtype_2`.
+
+4. If :math:`\externtype_1` and :math:`\externtype_2` are both of the form :math:`\ETGLOBAL~\globaltype_1` and :math:`\ETGLOBAL~\globaltype_2` respectively:
+
+   a. Return true if and only if :math:`\vdashexterntypematch \ETGLOBAL~\globaltype_1 \matchesexterntype \ETGLOBAL~\globaltype_2`.
+
+5. Return false.
+
+.. math::
+   \begin{array}{lclll}
+   \F{module\_extern\_subtype}(\externtype_1, \externtype_2) &=& \TRUE && (\iff \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2) \\
+   \end{array}
+
+.. note::
+   This function encapsulates the external type matching relation defined in the core specification. It allows for checking compatibility of external types when linking modules or validating imports against exports. The current implementation uses the exact matching rules from the core specification, but this function provides a single point for potential future extensions to the type system.
 
 .. index:: instantiation, module instance
 .. _embed-module-instantiate:
@@ -218,6 +249,66 @@ Modules
    \end{array}
 
 
+.. index:: direct export
+.. _embed-direct-exports:
+
+:math:`\F{module\_direct\_exports}(\module) : (\name, \externtype)^\ast`
+.......................................................................
+
+1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
+
+2. Let :math:`\export^\ast` be the :ref:`exports <syntax-export>` :math:`\module.\MEXPORTS`.
+
+3. Let :math:`\X{result}` be the empty sequence.
+
+4. For each :math:`\export_i` in :math:`\export^\ast` and corresponding :math:`\externtype'_i` in :math:`{\externtype'}^\ast`, do:
+
+   a. If :math:`\isdirectexport(\module, \export_i.\EDESC)`, then append the pair :math:`(\export_i.\ENAME, \externtype'_i)` to :math:`\X{result}`.
+
+5. Return :math:`\X{result}`.
+
+.. math::
+   ~ \\
+   \begin{array}{lclll}
+   \F{module\_direct\_exports}(m) &=& (\X{ex}.\ENAME, \externtype')^\ast \\
+   && \qquad (\iff \X{ex} \in m.\MEXPORTS \wedge \externtype' \in {\externtype'}^\ast \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast \\
+   && \qquad\quad \wedge \isdirectexport(m, \X{ex}.\EDESC)) \\
+   \end{array}
+
+
+.. index:: indirect export, re-export
+.. _embed-indirect-exports:
+
+:math:`\F{module\_indirect\_exports}(\module) : (\name, \name, \name)^\ast`
+................................................................
+
+1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
+
+2. Let :math:`\import^\ast` be the :ref:`imports <syntax-import>` :math:`\module.\MIMPORTS`.
+
+3. Let :math:`\export^\ast` be the :ref:`exports <syntax-export>` :math:`\module.\MEXPORTS`.
+
+4. Let :math:`\X{result}` be the empty sequence.
+
+5. For each :math:`\export_i` in :math:`\export^\ast`, do:
+
+   a. If :math:`\isindirectexport(\module, \export_i.\EDESC)`, then:
+
+      i. Let :math:`\import_j` be the import corresponding to the index in :math:`\export_i.\EDESC`.
+
+      ii. Append the triple :math:`(\export_i.\ENAME, \import_j.\IMODULE, \import_j.\INAME)` to :math:`\X{result}`.
+
+6. Return :math:`\X{result}`.
+
+.. math::
+   ~ \\
+   \begin{array}{lclll}
+   \F{module\_indirect\_exports}(m) &=& (\X{ex}.\ENAME, \X{im}.\IMODULE, \X{im}.\INAME)^\ast \\
+   && \qquad (\iff \X{ex} \in m.\MEXPORTS \wedge \X{im} \in m.\MIMPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast \\
+   && \qquad\quad \wedge \isindirectexport(m, \X{ex}.\EDESC) \wedge \X{im} = \importforexport(m, \X{ex}.\EDESC)) \\
+   \end{array}
+
+
 .. index:: module, module instance
 .. _embed-instance:
 

document/core/syntax/modules.rst

@@ -327,7 +327,7 @@ The |MSTART| component of a module declares the :ref:`function index <syntax-fun
    The module and its exports are not accessible externally before this initialization has completed.
 
 
-.. index:: ! export, name, index, function index, table index, memory index, global index, function, table, memory, global, instantiation
+.. index:: ! export, direct export, indirect export, re-export, name, index, function index, table index, memory index, global index, function, table, memory, global, instantiation
    pair: abstract syntax; export
    single: function; export
    single: table; export
@@ -356,6 +356,32 @@ Each export is labeled by a unique :ref:`name <syntax-name>`.
 Exportable definitions are :ref:`functions <syntax-func>`, :ref:`tables <syntax-table>`, :ref:`memories <syntax-mem>`, and :ref:`globals <syntax-global>`,
 which are referenced through a respective descriptor.
 
+A *direct export* is one where the export references a function, table, memory, or global instance that is defined within the module itself rather than being imported.
+
+An *indirect export* (or *re-export*) is one where the export references a function, table, memory, or global that the module imports.
+
+The import corresponding to an export description is given by:
+
+.. math::
+   \begin{array}{lllll}
+   \production{import for export} & \importforexport(m, \exportdesc) &=&
+     \begin{cases}
+       m.\MIMPORTS[\X{idx}] & (\iff \exportdesc = \EDFUNC~\X{idx} \wedge \X{idx} < |\etfuncs(m.\MIMPORTS)|) \\
+       m.\MIMPORTS[\X{fidx} + \X{idx}] & (\iff \exportdesc = \EDTABLE~\X{idx} \wedge \X{idx} < |\ettables(m.\MIMPORTS)| \\
+       & \quad \wedge \X{fidx} = |\etfuncs(m.\MIMPORTS)|) \\
+       m.\MIMPORTS[\X{fidx} + \X{tidx} + \X{idx}] & (\iff \exportdesc = \EDMEM~\X{idx} \wedge \X{idx} < |\etmems(m.\MIMPORTS)| \\
+       & \quad \wedge \X{fidx} = |\etfuncs(m.\MIMPORTS)| \wedge \X{tidx} = |\ettables(m.\MIMPORTS)|) \\
+       m.\MIMPORTS[\X{fidx} + \X{tidx} + \X{midx} + \X{idx}] & (\iff \exportdesc = \EDGLOBAL~\X{idx} \wedge \X{idx} < |\etglobals(m.\MIMPORTS)| \\
+       & \quad \wedge \X{fidx} = |\etfuncs(m.\MIMPORTS)| \wedge \X{tidx} = |\ettables(m.\MIMPORTS)| \\
+       & \quad \wedge \X{midx} = |\etmems(m.\MIMPORTS)|) \\
+       \epsilon & (\otherwise) \\
+     \end{cases} \\
+   \end{array}
+
+For embedder convenience, we also define:
+
+* :math:``\isdirectexport(m, \exportdesc) = (\importforexport(m, \exportdesc) = \epsilon)`
+* :math:``\isindirectexport(m, \exportdesc) = (\importforexport(m, \exportdesc) \neq \epsilon)`
 
 Conventions
 ...........