[spec] Pre/post-conditions and some renamings in embedding interface (#1003)

diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst
index 9558bf1..afcb5a6 100644
--- a/document/core/appendix/embedding.rst
+++ b/document/core/appendix/embedding.rst
@@ -13,13 +13,22 @@
 
 .. note::
    On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface.
-   For example, an implementation may not support :ref:`parsing <embed-parse-module>` of the :ref:`text format <text>`.
+   For example, an implementation may not support :ref:`parsing <embed-module-parse>` of the :ref:`text format <text>`.
+
+Types
+.....
 
 In the description of the embedder interface, syntactic classes from the :ref:`abstract syntax <syntax>` and the :ref:`runtime's abstract machine <syntax-runtime>` are used as names for variables that range over the possible objects from that class.
 Hence, these syntactic classes can also be interpreted as types.
 
+For numeric parameters, notation like :math:`n:\u32` is used to specify a symbolic name in addition to the respective value range.
+
+
 .. _embed-error:
 
+Errors
+......
+
 Failure of an interface operation is indicated by an auxiliary syntactic class:
 
 .. math::
@@ -29,12 +38,28 @@
 
 In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific :ref:`implementation limitations <impl>` are reached.
 
-
 .. note::
    Errors are abstract and unspecific with this definition.
    Implementations can refine it to carry suitable classifications and diagnostic messages.
 
 
+Pre- and Post-Conditions
+........................
+
+Some operations state *pre-conditions* about their arguments or *post-conditions* about their results.
+It is the embedder's responsibility to meet the pre-conditions.
+If it does, the post conditions are guaranteed by the semantics.
+
+In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects <syntax-runtime>` (:math:`store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses <syntax-addr>`):
+
+* Every runtime object passed as a parameter must be :ref:`valid <valid-store>` per an implicit pre-condition.
+
+* Every runtime object returned as a result is :ref:`valid <valid-store>` per an implicit post-condition.
+
+.. note::
+   As long as an embedder treats runtime objects as abstract and only creates and manipulates them through the interface defined here, all implicit pre-conditions are automatically met.
+
+
 
 .. index:: allocation, store
 .. _embed-store:
@@ -42,16 +67,16 @@
 Store
 ~~~~~
 
-.. _embed-init-store:
+.. _embed-store-init:
 
-:math:`\F{init\_store}() : \store`
+:math:`\F{store\_init}() : \store`
 ..................................
 
 1. Return the empty :ref:`store <syntax-store>`.
 
 .. math::
    \begin{array}{lclll}
-   \F{init\_store}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
+   \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
    \end{array}
 
 
@@ -63,9 +88,9 @@
 ~~~~~~~
 
 .. index:: binary format
-.. _embed-decode-module:
+.. _embed-module-decode:
 
-:math:`\F{decode\_module}(\byte^\ast) : \module ~|~ \error`
+:math:`\F{module\_decode}(\byte^\ast) : \module ~|~ \error`
 ...........................................................
 
 1. If there exists a derivation for the :ref:`byte <syntax-byte>` sequence :math:`\byte^\ast` as a :math:`\Bmodule` according to the :ref:`binary grammar for modules <binary-module>`, yielding a :ref:`module <syntax-module>` :math:`m`, then return :math:`m`.
@@ -74,16 +99,16 @@
 
 .. math::
    \begin{array}{lclll}
-   \F{decode\_module}(b^\ast) &=& m && (\iff \Bmodule \stackrel\ast\Longrightarrow m{:}b^\ast) \\
-   \F{decode\_module}(b^\ast) &=& \ERROR && (\otherwise) \\
+   \F{module\_decode}(b^\ast) &=& m && (\iff \Bmodule \stackrel\ast\Longrightarrow m{:}b^\ast) \\
+   \F{module\_decode}(b^\ast) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
 .. index:: text format
-.. _embed-parse-module:
+.. _embed-module-parse:
 
-:math:`\F{parse\_module}(\char^\ast) : \module ~|~ \error`
-...............................................................
+:math:`\F{module\_parse}(\char^\ast) : \module ~|~ \error`
+..........................................................
 
 1. If there exists a derivation for the :ref:`source <text-source>` :math:`\char^\ast` as a :math:`\Tmodule` according to the :ref:`text grammar for modules <text-module>`, yielding a :ref:`module <syntax-module>` :math:`m`, then return :math:`m`.
 
@@ -91,15 +116,15 @@
 
 .. math::
    \begin{array}{lclll}
-   \F{parse\_module}(c^\ast) &=& m && (\iff \Tmodule \stackrel\ast\Longrightarrow m{:}c^\ast) \\
-   \F{parse\_module}(c^\ast) &=& \ERROR && (\otherwise) \\
+   \F{module\_parse}(c^\ast) &=& m && (\iff \Tmodule \stackrel\ast\Longrightarrow m{:}c^\ast) \\
+   \F{module\_parse}(c^\ast) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
 .. index:: validation
-.. _embed-validate-module:
+.. _embed-module-validate:
 
-:math:`\F{validate\_module}(\module) : \error^?`
+:math:`\F{module\_validate}(\module) : \error^?`
 ................................................
 
 1. If :math:`\module` is :ref:`valid <valid-module>`, then return nothing.
@@ -108,15 +133,15 @@
 
 .. math::
    \begin{array}{lclll}
-   \F{validate\_module}(m) &=& \epsilon && (\iff {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\
-   \F{validate\_module}(m) &=& \ERROR && (\otherwise) \\
+   \F{module\_validate}(m) &=& \epsilon && (\iff {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\
+   \F{module\_validate}(m) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
 .. index:: instantiation, module instance
-.. _embed-instantiate-module:
+.. _embed-module-instantiate:
 
-:math:`\F{instantiate\_module}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \error)`
+:math:`\F{module\_instantiate}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \error)`
 ....................................................................................................
 
 1. Try :ref:`instantiating <exec-instantiation>` :math:`\module` in :math:`\store` with :ref:`external values <syntax-externval>` :math:`\externval^\ast` as imports:
@@ -129,8 +154,8 @@
 
 .. math::
    \begin{array}{lclll}
-   \F{instantiate\_module}(S, m, \X{ev}^\ast) &=& (S', F.\AMODULE) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \epsilon) \\
-   \F{instantiate\_module}(S, m, \X{ev}^\ast) &=& (S', \ERROR) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \TRAP) \\
+   \F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', F.\AMODULE) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \epsilon) \\
+   \F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', \ERROR) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \TRAP) \\
    \end{array}
 
 .. note::
@@ -138,12 +163,12 @@
 
 
 .. index:: import
-.. _embed-imports:
+.. _embed-module-imports:
 
 :math:`\F{module\_imports}(\module) : (\name, \name, \externtype)^\ast`
 .......................................................................
 
-1. Assert: :math:`\module` is :ref:`valid <valid-module>` with external import types :math:`\externtype^\ast` and external export types :math:`{\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:`\import^\ast` be the :ref:`imports <syntax-import>` :math:`\module.\MIMPORTS`.
 
@@ -155,6 +180,8 @@
 
 5. Return the concatenation of all :math:`\X{result}_i`, in index order.
 
+6. Post-condition: each :math:`\externtype_i` is :ref:`valid <valid-externtype>`.
+
 .. math::
    ~ \\
    \begin{array}{lclll}
@@ -164,12 +191,12 @@
 
 
 .. index:: export
-.. _embed-exports:
+.. _embed-module-exports:
 
 :math:`\F{module\_exports}(\module) : (\name, \externtype)^\ast`
 ................................................................
 
-1. Assert: :math:`\module` is :ref:`valid <valid-module>` with external import types :math:`\externtype^\ast` and external export types :math:`{\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`.
 
@@ -181,6 +208,8 @@
 
 5. Return the concatenation of all :math:`\X{result}_i`, in index order.
 
+6. Post-condition: each :math:`\externtype'_i` is :ref:`valid <valid-externtype>`.
+
 .. math::
    ~ \\
    \begin{array}{lclll}
@@ -189,16 +218,18 @@
    \end{array}
 
 
-.. index:: module, store, module instance, export instance
-.. _embed-export:
+.. index:: module, module instance
+.. _embed-instance:
 
-Exports
-~~~~~~~
+Module Instances
+~~~~~~~~~~~~~~~~
 
-.. _embed-get-export:
+.. index:: export, export instance
 
-:math:`\F{get\_export}(\moduleinst, \name) : \externval ~|~ \error`
-...................................................................
+.. _embed-instance-export:
+
+:math:`\F{instance\_export}(\moduleinst, \name) : \externval ~|~ \error`
+........................................................................
 
 1. Assert: due to :ref:`validity <valid-moduleinst>` of the :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst`, all its :ref:`export names <syntax-exportinst>` are different.
 
@@ -211,8 +242,8 @@
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{get\_export}(m, \name) &=& m.\MIEXPORTS[i].\EIVALUE && (\iff m.\MEXPORTS[i].\EINAME = \name) \\
-   \F{get\_export}(m, \name) &=& \ERROR && (\otherwise) \\
+   \F{instance\_export}(m, \name) &=& m.\MIEXPORTS[i].\EIVALUE && (\iff m.\MEXPORTS[i].\EINAME = \name) \\
+   \F{instance\_export}(m, \name) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
@@ -222,64 +253,64 @@
 Functions
 ~~~~~~~~~
 
-.. _embed-alloc-func:
+.. _embed-func-alloc:
 
-:math:`\F{alloc\_func}(\store, \functype, \hostfunc) : (\store, \funcaddr)`
+:math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)`
 ...........................................................................
 
-1. Let :math:`\funcaddr` be the result of :ref:`allocating a host function <alloc-func>` in :math:`\store` with :ref:`function type <syntax-functype>` :math:`\functype` and host function code :math:`\hostfunc`.
+1. Pre-condition: :math:`\functype` is :math:`valid <valid-functype>`.
 
-2. Return the new store paired with :math:`\funcaddr`.
+2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function <alloc-func>` in :math:`\store` with :ref:`function type <syntax-functype>` :math:`\functype` and host function code :math:`\hostfunc`.
+
+3. Return the new store paired with :math:`\funcaddr`.
 
 .. math::
    \begin{array}{lclll}
-   \F{alloc\_func}(S, \X{ft}, \X{code}) &=& (S', \X{a}) && (\iff \allochostfunc(S, \X{ft}, \X{code}) = S', \X{a}) \\
+   \F{func\_alloc}(S, \X{ft}, \X{code}) &=& (S', \X{a}) && (\iff \allochostfunc(S, \X{ft}, \X{code}) = S', \X{a}) \\
    \end{array}
 
 .. note::
    This operation assumes that :math:`\hostfunc` satisfies the :ref:`pre- and post-conditions <exec-invoke-host>` required for a function instance with type :math:`\functype`.
 
-   Regular (non-host) function instances can only be created indirectly through :ref:`module instantiation <embed-instantiate-module>`.
+   Regular (non-host) function instances can only be created indirectly through :ref:`module instantiation <embed-module-instantiate>`.
 
 
-.. _embed-type-func:
+.. _embed-func-type:
 
-:math:`\F{type\_func}(\store, \funcaddr) : \functype`
+:math:`\F{func\_type}(\store, \funcaddr) : \functype`
 .....................................................
 
-1. Assert: :math:`\store.\SFUNCS[\funcaddr]` exists.
+1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVFUNC~\funcaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETFUNC~\functype`.
 
-2. Assert: the :ref:`external value <syntax-externval>` :math:`\EVFUNC~\funcaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETFUNC~\functype`.
+2. Return :math:`\functype`.
 
-3. Return :math:`\functype`.
+3. Post-condition: :math:`\functype` is :ref:`valid <valid-functype>`.
 
 .. math::
    \begin{array}{lclll}
-   \F{type\_func}(S, a) &=& \X{ft} && (\iff S \vdashexternval \EVFUNC~a : \ETFUNC~\X{ft}) \\
+   \F{func\_type}(S, a) &=& \X{ft} && (\iff S \vdashexternval \EVFUNC~a : \ETFUNC~\X{ft}) \\
    \end{array}
 
 
 .. index:: invocation, value, result
-.. _embed-invoke-func:
+.. _embed-func-invoke:
 
-:math:`\F{invoke\_func}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)`
+:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)`
 ........................................................................................
 
-1. Assert: :math:`\store.\SFUNCS[\funcaddr]` exists.
-
-2. Try :ref:`invoking <exec-invocation>` the function :math:`\funcaddr` in :math:`\store` with :ref:`values <syntax-val>` :math:`\val^\ast` as arguments:
+1. Try :ref:`invoking <exec-invocation>` the function :math:`\funcaddr` in :math:`\store` with :ref:`values <syntax-val>` :math:`\val^\ast` as arguments:
 
   a. If it succeeds with :ref:`values <syntax-val>` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`.
 
   b. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`.
 
-3. Return the new store paired with :math:`\X{result}`.
+2. Return the new store paired with :math:`\X{result}`.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{invoke\_func}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\
-   \F{invoke\_func}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\
+   \F{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\
+   \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\
    \end{array}
 
 .. note::
@@ -292,112 +323,100 @@
 Tables
 ~~~~~~
 
-.. _embed-alloc-table:
+.. _embed-table-alloc:
 
-:math:`\F{alloc\_table}(\store, \tabletype) : (\store, \tableaddr)`
+:math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr)`
 ...................................................................
 
-1. Let :math:`\tableaddr` be the result of :ref:`allocating a table <alloc-table>` in :math:`\store` with :ref:`table type <syntax-tabletype>` :math:`\tabletype`.
+1. Pre-condition: :math:`\tabletype` is :math:`valid <valid-tabletype>`.
 
-2. Return the new store paired with :math:`\tableaddr`.
+2. Let :math:`\tableaddr` be the result of :ref:`allocating a table <alloc-table>` in :math:`\store` with :ref:`table type <syntax-tabletype>` :math:`\tabletype`.
+
+3. Return the new store paired with :math:`\tableaddr`.
 
 .. math::
    \begin{array}{lclll}
-   \F{alloc\_table}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}) = S', \X{a}) \\
+   \F{table\_alloc}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}) = S', \X{a}) \\
    \end{array}
 
 
-.. _embed-type-table:
+.. _embed-table-type:
 
-:math:`\F{type\_table}(\store, \tableaddr) : \tabletype`
+:math:`\F{table\_type}(\store, \tableaddr) : \tabletype`
 ........................................................
 
-1. Assert: :math:`\store.\STABLES[\tableaddr]` exists.
+1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVTABLE~\tableaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETTABLE~\tabletype`.
 
-2. Assert: the :ref:`external value <syntax-externval>` :math:`\EVTABLE~\tableaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETTABLE~\tabletype`.
+2. Return :math:`\tabletype`.
 
-3. Return :math:`\tabletype`.
+3. Post-condition: :math:`\tabletype` is :math:`valid <valid-tabletype>`.
 
 .. math::
    \begin{array}{lclll}
-   \F{type\_table}(S, a) &=& \X{tt} && (\iff S \vdashexternval \EVTABLE~a : \ETTABLE~\X{tt}) \\
+   \F{table\_type}(S, a) &=& \X{tt} && (\iff S \vdashexternval \EVTABLE~a : \ETTABLE~\X{tt}) \\
    \end{array}
 
 
-.. _embed-read-table:
+.. _embed-table-read:
 
-:math:`\F{read\_table}(\store, \tableaddr, i) : \funcaddr^? ~|~ \error`
-.......................................................................
+:math:`\F{table\_read}(\store, \tableaddr, i:\u32) : \funcaddr^? ~|~ \error`
+............................................................................
 
-1. Assert: :math:`\store.\STABLES[\tableaddr]` exists.
+1. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`.
 
-2. Assert: :math:`i` is a non-negative integer.
+2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`.
 
-3. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`.
-
-4. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`.
-
-5. Else, return :math:`\X{ti}.\TIELEM[i]`.
+3. Else, return :math:`\X{ti}.\TIELEM[i]`.
 
 .. math::
    \begin{array}{lclll}
-   \F{read\_table}(S, a, i) &=& \X{fa}^? && (\iff S.\STABLES[a].\TIELEM[i] = \X{fa}^?) \\
-   \F{read\_table}(S, a, i) &=& \ERROR && (\otherwise) \\
+   \F{table\_read}(S, a, i) &=& \X{fa}^? && (\iff S.\STABLES[a].\TIELEM[i] = \X{fa}^?) \\
+   \F{table\_read}(S, a, i) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
-.. _embed-write-table:
+.. _embed-table-write:
 
-:math:`\F{write\_table}(\store, \tableaddr, i, \funcaddr^?) : \store ~|~ \error`
-................................................................................
+:math:`\F{table\_write}(\store, \tableaddr, i:\u32, \funcaddr^?) : \store ~|~ \error`
+.......................................................................................
 
-1. Assert: :math:`\store.\STABLES[\tableaddr]` exists.
+1. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`.
 
-2. Assert: :math:`i` is a non-negative integer.
+2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`.
 
-3. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`.
+3. Replace :math:`\X{ti}.\TIELEM[i]` with the optional :ref:`function address <syntax-funcaddr>` :math:`\X{fa}^?`.
 
-4. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`.
-
-5. Replace :math:`\X{ti}.\TIELEM[i]` with the optional :ref:`function address <syntax-funcaddr>` :math:`\X{fa}^?`.
-
-6. Return the updated store.
+4. Return the updated store.
 
 .. math::
    \begin{array}{lclll}
-   \F{write\_table}(S, a, i, \X{fa}^?) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = \X{fa}^?) \\
-   \F{write\_table}(S, a, i, \X{fa}^?) &=& \ERROR && (\otherwise) \\
+   \F{table\_write}(S, a, i, \X{fa}^?) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = \X{fa}^?) \\
+   \F{table\_write}(S, a, i, \X{fa}^?) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
-.. _embed-size-table:
+.. _embed-table-size:
 
-:math:`\F{size\_table}(\store, \tableaddr) : \X{i32}`
-.....................................................
+:math:`\F{table\_size}(\store, \tableaddr) : \u32`
+..................................................
 
-1. Assert: :math:`\store.\STABLES[\tableaddr]` exists.
-
-2. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`.
+1. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{size\_table}(S, a) &=& n &&
+   \F{table\_size}(S, a) &=& n &&
      (\iff |S.\STABLES[a].\TIELEM| = n) \\
    \end{array}
 
 
 
-.. _embed-grow-table:
+.. _embed-table-grow:
 
-:math:`\F{grow\_table}(\store, \tableaddr, n) : \store ~|~ \error`
-..................................................................
+:math:`\F{table\_grow}(\store, \tableaddr, n:\u32) : \store ~|~ \error`
+.......................................................................
 
-1. Assert: :math:`\store.\STABLES[\tableaddr]` exists.
-
-2. Assert: :math:`n` is a non-negative integer.
-
-3. Try :ref:`growing <grow-table>` the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]` by :math:`n` elements:
+1. Try :ref:`growing <grow-table>` the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]` by :math:`n` elements:
 
    a. If it succeeds, return the updated store.
 
@@ -406,9 +425,9 @@
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{grow\_table}(S, a, n) &=& S' &&
+   \F{table\_grow}(S, a, n) &=& S' &&
      (\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n)) \\
-   \F{grow\_table}(S, a, n) &=& \ERROR && (\otherwise) \\
+   \F{table\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
@@ -418,112 +437,100 @@
 Memories
 ~~~~~~~~
 
-.. _embed-alloc-mem:
+.. _embed-mem-alloc:
 
-:math:`\F{alloc\_mem}(\store, \memtype) : (\store, \memaddr)`
+:math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)`
 ................................................................
 
-1. Let :math:`\memaddr` be the result of :ref:`allocating a memory <alloc-mem>` in :math:`\store` with :ref:`memory type <syntax-memtype>` :math:`\memtype`.
+1. Pre-condition: :math:`\memtype` is :math:`valid <valid-memtype>`.
 
-2. Return the new store paired with :math:`\memaddr`.
+2. Let :math:`\memaddr` be the result of :ref:`allocating a memory <alloc-mem>` in :math:`\store` with :ref:`memory type <syntax-memtype>` :math:`\memtype`.
+
+3. Return the new store paired with :math:`\memaddr`.
 
 .. math::
    \begin{array}{lclll}
-   \F{alloc\_mem}(S, \X{mt}) &=& (S', \X{a}) && (\iff \allocmem(S, \X{mt}) = S', \X{a}) \\
+   \F{mem\_alloc}(S, \X{mt}) &=& (S', \X{a}) && (\iff \allocmem(S, \X{mt}) = S', \X{a}) \\
    \end{array}
 
 
-.. _embed-type-mem:
+.. _embed-mem-type:
 
-:math:`\F{type\_mem}(\store, \memaddr) : \memtype`
+:math:`\F{mem\_type}(\store, \memaddr) : \memtype`
 ..................................................
 
-1. Assert: :math:`\store.\SMEMS[\memaddr]` exists.
+1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVMEM~\memaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETMEM~\memtype`.
 
-2. Assert: the :ref:`external value <syntax-externval>` :math:`\EVMEM~\memaddr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETMEM~\memtype`.
+2. Return :math:`\memtype`.
 
-3. Return :math:`\memtype`.
+3. Post-condition: :math:`\memtype` is :math:`valid <valid-memtype>`.
 
 .. math::
    \begin{array}{lclll}
-   \F{type\_mem}(S, a) &=& \X{mt} && (\iff S \vdashexternval \EVMEM~a : \ETMEM~\X{mt}) \\
+   \F{mem\_type}(S, a) &=& \X{mt} && (\iff S \vdashexternval \EVMEM~a : \ETMEM~\X{mt}) \\
    \end{array}
 
 
-.. _embed-read-mem:
+.. _embed-mem-read:
 
-:math:`\F{read\_mem}(\store, \memaddr, i) : \byte ~|~ \error`
-.............................................................
+:math:`\F{mem\_read}(\store, \memaddr, i:\u32) : \byte ~|~ \error`
+..................................................................
 
-1. Assert: :math:`\store.\SMEMS[\memaddr]` exists.
+1. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`.
 
-2. Assert: :math:`i` is a non-negative integer.
+2. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`.
 
-3. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`.
-
-4. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`.
-
-5. Else, return the  :ref:`byte <syntax-byte>` :math:`\X{mi}.\MIDATA[i]`.
+3. Else, return the  :ref:`byte <syntax-byte>` :math:`\X{mi}.\MIDATA[i]`.
 
 .. math::
    \begin{array}{lclll}
-   \F{read\_mem}(S, a, i) &=& b && (\iff S.\SMEMS[a].\MIDATA[i] = b) \\
-   \F{read\_mem}(S, a, i) &=& \ERROR && (\otherwise) \\
+   \F{mem\_read}(S, a, i) &=& b && (\iff S.\SMEMS[a].\MIDATA[i] = b) \\
+   \F{mem\_read}(S, a, i) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
-.. _embed-write-mem:
+.. _embed-mem-write:
 
-:math:`\F{write\_mem}(\store, \memaddr, i, \byte) : \store ~|~ \error`
-......................................................................
+:math:`\F{mem\_write}(\store, \memaddr, i:\u32, \byte) : \store ~|~ \error`
+...........................................................................
 
-1. Assert: :math:`\store.\SMEMS[\memaddr]` exists.
+1. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`.
 
-2. Assert: :math:`i` is a non-negative integer.
+2. If :math:`\u32` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`.
 
-3. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`.
+3. Replace :math:`\X{mi}.\MIDATA[i]` with :math:`\byte`.
 
-4. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`.
-
-5. Replace :math:`\X{mi}.\MIDATA[i]` with :math:`\byte`.
-
-6. Return the updated store.
+4. Return the updated store.
 
 .. math::
    \begin{array}{lclll}
-   \F{write\_mem}(S, a, i, b) &=& S' && (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b) \\
-   \F{write\_mem}(S, a, i, b) &=& \ERROR && (\otherwise) \\
+   \F{mem\_write}(S, a, i, b) &=& S' && (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b) \\
+   \F{mem\_write}(S, a, i, b) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
-.. _embed-size-mem:
+.. _embed-mem-size:
 
-:math:`\F{size\_mem}(\store, \memaddr) : \X{i32}`
-.................................................
+:math:`\F{mem\_size}(\store, \memaddr) : \u32`
+..............................................
 
-1. Assert: :math:`\store.\SMEMS[\memaddr]` exists.
-
-2. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size <page-size>`.
+1. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size <page-size>`.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{size\_mem}(S, a) &=& n &&
+   \F{mem\_size}(S, a) &=& n &&
      (\iff |S.\SMEMS[a].\MIDATA| = n \cdot 64\,\F{Ki}) \\
    \end{array}
 
 
 
-.. _embed-grow-mem:
+.. _embed-mem-grow:
 
-:math:`\F{grow\_mem}(\store, \memaddr, n) : \store ~|~ \error`
-..............................................................
+:math:`\F{mem\_grow}(\store, \memaddr, n:\u32) : \store ~|~ \error`
+...................................................................
 
-1. Assert: :math:`\store.\SMEMS[\memaddr]` exists.
-
-2. Assert: :math:`n` is a non-negative integer.
-
-3. Try :ref:`growing <grow-mem>` the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]` by :math:`n` :ref:`pages <page-size>`:
+1. Try :ref:`growing <grow-mem>` the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]` by :math:`n` :ref:`pages <page-size>`:
 
    a. If it succeeds, return the updated store.
 
@@ -532,9 +539,9 @@
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{grow\_mem}(S, a, n) &=& S' &&
+   \F{mem\_grow}(S, a, n) &=& S' &&
      (\iff S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\
-   \F{grow\_mem}(S, a, n) &=& \ERROR && (\otherwise) \\
+   \F{mem\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\
    \end{array}
 
 
@@ -545,73 +552,71 @@
 Globals
 ~~~~~~~
 
-.. _embed-alloc-global:
+.. _embed-global-alloc:
 
-:math:`\F{alloc\_global}(\store, \globaltype, \val) : (\store, \globaladdr)`
+:math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)`
 ............................................................................
 
-1. Let :math:`\globaladdr` be the result of :ref:`allocating a global <alloc-global>` in :math:`\store` with :ref:`global type <syntax-globaltype>` :math:`\globaltype` and initialization value :math:`\val`.
+1. Pre-condition: :math:`\globaltype` is :math:`valid <valid-globaltype>`.
 
-2. Return the new store paired with :math:`\globaladdr`.
+2. Let :math:`\globaladdr` be the result of :ref:`allocating a global <alloc-global>` in :math:`\store` with :ref:`global type <syntax-globaltype>` :math:`\globaltype` and initialization value :math:`\val`.
+
+3. Return the new store paired with :math:`\globaladdr`.
 
 .. math::
    \begin{array}{lclll}
-   \F{alloc\_global}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\
+   \F{global\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\
    \end{array}
 
 
-.. _embed-type-global:
+.. _embed-global-type:
 
-:math:`\F{type\_global}(\store, \globaladdr) : \globaltype`
+:math:`\F{global\_type}(\store, \globaladdr) : \globaltype`
 ...........................................................
 
-1. Assert: :math:`\store.\SGLOBALS[\globaladdr]` exists.
+1. Assert: the :ref:`external value <syntax-externval>` :math:`\EVGLOBAL~\globaladdr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETGLOBAL~\globaltype`.
 
-2. Assert: the :ref:`external value <syntax-externval>` :math:`\EVGLOBAL~\globaladdr` is :ref:`valid <valid-externval>` with :ref:`external type <syntax-externtype>` :math:`\ETGLOBAL~\globaltype`.
+2. Return :math:`\globaltype`.
 
-3. Return :math:`\globaltype`.
+3. Post-condition: :math:`\globaltype` is :math:`valid <valid-globaltype>`.
 
 .. math::
    \begin{array}{lclll}
-   \F{type\_global}(S, a) &=& \X{gt} && (\iff S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~\X{gt}) \\
+   \F{global\_type}(S, a) &=& \X{gt} && (\iff S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~\X{gt}) \\
    \end{array}
 
 
-.. _embed-read-global:
+.. _embed-global-read:
 
-:math:`\F{read\_global}(\store, \globaladdr) : \val`
+:math:`\F{global\_read}(\store, \globaladdr) : \val`
 ....................................................
 
-1. Assert: :math:`\store.\SGLOBALS[\globaladdr]` exists.
+1. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`.
 
-2. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`.
-
-3. Return the :ref:`value <syntax-val>` :math:`\X{gi}.\GIVALUE`.
+2. Return the :ref:`value <syntax-val>` :math:`\X{gi}.\GIVALUE`.
 
 .. math::
    \begin{array}{lclll}
-   \F{read\_global}(S, a) &=& v && (\iff S.\SGLOBALS[a].\GIVALUE = v) \\
+   \F{global\_read}(S, a) &=& v && (\iff S.\SGLOBALS[a].\GIVALUE = v) \\
    \end{array}
 
 
-.. _embed-write-global:
+.. _embed-global-write:
 
-:math:`\F{write\_global}(\store, \globaladdr, \val) : \store ~|~ \error`
+:math:`\F{global\_write}(\store, \globaladdr, \val) : \store ~|~ \error`
 ........................................................................
 
-1. Assert: :math:`\store.\SGLOBALS[a]` exists.
+1. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`.
 
-2. Let :math:`\X{gi}` be the :ref:`global instance <syntax-globalinst>` :math:`\store.\SGLOBALS[\globaladdr]`.
+2. If :math:`\X{gi}.\GIMUT` is not :math:`\MVAR`, then return :math:`\ERROR`.
 
-3. If :math:`\X{gi}.\GIMUT` is not :math:`\MVAR`, then return :math:`\ERROR`.
+3. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value <syntax-val>` :math:`\val`.
 
-4. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value <syntax-val>` :math:`\val`.
-
-5. Return the updated store.
+4. Return the updated store.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
-   \F{write\_global}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GIMUT = \MVAR \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
-   \F{write\_global}(S, a, v) &=& \ERROR && (\otherwise) \\
+   \F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GIMUT = \MVAR \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
+   \F{global\_write}(S, a, v) &=& \ERROR && (\otherwise) \\
    \end{array}
diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst
index 4d02f7a..4d610e0 100644
--- a/document/core/appendix/index-rules.rst
+++ b/document/core/appendix/index-rules.rst
@@ -18,6 +18,7 @@
 :ref:`Table type <valid-tabletype>`              :math:`\vdashtabletype \tabletype \ok`
 :ref:`Memory type <valid-memtype>`               :math:`\vdashmemtype \memtype \ok`
 :ref:`Global type <valid-globaltype>`            :math:`\vdashglobaltype \globaltype \ok`
+:ref:`External type <valid-externtype>`          :math:`\vdashexterntype \externtype \ok`
 :ref:`Instruction <valid-instr>`                 :math:`S;C \vdashinstr \instr : \functype`
 :ref:`Instruction sequence <valid-instr-seq>`    :math:`S;C \vdashinstrseq \instr^\ast : \functype`
 :ref:`Expression <valid-expr>`                   :math:`C \vdashexpr \expr : \resulttype`
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 34d821c..679b935 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -434,7 +434,6 @@
 .. |Bf64| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{64}}}
 
 .. |Bname| mathdef:: \xref{binary/values}{binary-name}{\B{name}}
-.. |Bchar| mathdef:: \xref{binary/values}{binary-name}{\B{char}}
 
 
 .. Values, meta functions
@@ -593,9 +592,6 @@
 .. |Tstringelem| mathdef:: \xref{text/values}{text-string}{\T{stringelem}}
 .. |Tstringchar| mathdef:: \xref{text/values}{text-string}{\T{stringchar}}
 .. |Tname| mathdef:: \xref{text/values}{text-name}{\T{name}}
-.. |Tchar| mathdef:: \xref{text/values}{text-name}{\T{char}}
-.. |Tcodeval| mathdef:: \xref{text/values}{text-name}{\T{codeval}}
-.. |Tcodecont| mathdef:: \xref{text/values}{text-name}{\T{cont}}
 
 .. |Tid| mathdef:: \xref{text/values}{text-id}{\T{id}}
 .. |Tidchar| mathdef:: \xref{text/values}{text-idchar}{\T{idchar}}
@@ -725,6 +721,7 @@
 .. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash}
 .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash}
 .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash}
+.. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash}
 
 .. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash}
 .. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash}
diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst
index 39a64c6..a7b9283 100644
--- a/document/core/valid/types.rst
+++ b/document/core/valid/types.rst
@@ -131,3 +131,68 @@
    }{
      \vdashglobaltype \mut~\valtype \ok
    }
+
+
+.. index:: external type, function type, table type, memory type, global type
+   pair: validation; external type
+   single: abstract syntax; external type
+.. _valid-externtype:
+
+External Types
+~~~~~~~~~~~~~~
+
+:math:`\ETFUNC~\functype`
+.........................
+
+* The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
+
+* Then the external type is valid.
+
+.. math::
+   \frac{
+     \vdashfunctype \functype \ok
+   }{
+     \vdashexterntype \ETFUNC~\functype \ok
+   }
+
+:math:`\ETTABLE~\tabletype`
+...........................
+
+* The :ref:`table type <syntax-tabletype>` :math:`\tabletype` must be :ref:`valid <valid-tabletype>`.
+
+* Then the external type is valid.
+
+.. math::
+   \frac{
+     \vdashtabletype \tabletype \ok
+   }{
+     \vdashexterntype \ETTABLE~\tabletype \ok
+   }
+
+:math:`\ETMEM~\memtype`
+.......................
+
+* The :ref:`memory type <syntax-memtype>` :math:`\memtype` must be :ref:`valid <valid-memtype>`.
+
+* Then the external type is valid.
+
+.. math::
+   \frac{
+     \vdashmemtype \memtype \ok
+   }{
+     \vdashexterntype \ETMEM~\memtype \ok
+   }
+
+:math:`\ETGLOBAL~\globaltype`
+.............................
+
+* The :ref:`global type <syntax-globaltype>` :math:`\globaltype` must be :ref:`valid <valid-globaltype>`.
+
+* Then the external type is valid.
+
+.. math::
+   \frac{
+     \vdashglobaltype \globaltype \ok
+   }{
+     \vdashexterntype \ETGLOBAL~\globaltype \ok
+   }
diff --git a/document/js-api/index.bs b/document/js-api/index.bs
index f6b89ed..55bfa36 100644
--- a/document/js-api/index.bs
+++ b/document/js-api/index.bs
@@ -104,30 +104,32 @@
         text: π–ΏπŸ¨πŸ¦.π–Όπ—ˆπ—‡π—Œπ—
     text: function index; url: syntax/modules.html#syntax-funcidx
     text: function instance; url: exec/runtime.html#function-instances
-    text: init_store; url: appendix/embedding.html#embed-init-store
-    text: decode_module; url: appendix/embedding.html#embed-decode-module
-    text: validate_module; url: appendix/embedding.html#embed-validate-module
-    text: instantiate_module; url: appendix/embedding.html#embed-instantiate-module
-    text: module_imports; url: appendix/embedding.html#embed-imports
-    text: get_export; url: appendix/embedding.html#embed-get-export
-    text: alloc_func; url: appendix/embedding.html#embed-alloc-func
-    text: type_func; url: appendix/embedding.html#embed-type-func
-    text: invoke_func; url: appendix/embedding.html#embed-invoke-func
-    text: alloc_table; url: appendix/embedding.html#embed-alloc-table
-    text: type_table; url: appendix/embedding.html#embed-type-table
-    text: read_table; url: appendix/embedding.html#embed-read-table
-    text: write_table; url: appendix/embedding.html#embed-write-table
-    text: grow_table; url: appendix/embedding.html#embed-grow-table
-    text: alloc_mem; url: appendix/embedding.html#embed-alloc-mem
-    text: type_mem; url: appendix/embedding.html#embed-type-mem
-    text: read_mem; url: appendix/embedding.html#embed-read-mem
-    text: write_mem; url: appendix/embedding.html#embed-write-mem
-    text: grow_mem; url: appendix/embedding.html#embed-grow-mem
-    text: alloc_global; url: appendix/embedding.html#embed-alloc-global
-    text: type_global; url: appendix/embedding.html#embed-type-global
-    text: read_global; url: appendix/embedding.html#embed-read-global
-    text: write_global; url: appendix/embedding.html#embed-write-global
-    text: module_exports; url: appendix/embedding.html#embed-exports
+    text: store_init; url: appendix/embedding.html#embed-store-init
+    text: module_decode; url: appendix/embedding.html#embed-module-decode
+    text: module_validate; url: appendix/embedding.html#embed-module-validate
+    text: module_instantiate; url: appendix/embedding.html#embed-module-instantiate
+    text: module_imports; url: appendix/embedding.html#embed-module-imports
+    text: module_exports; url: appendix/embedding.html#embed-module-exports
+    text: instance_export; url: appendix/embedding.html#embed-instance-export
+    text: func_alloc; url: appendix/embedding.html#embed-func-alloc
+    text: func_type; url: appendix/embedding.html#embed-func-type
+    text: func_invoke; url: appendix/embedding.html#embed-func-invoke
+    text: table_alloc; url: appendix/embedding.html#embed-table-alloc
+    text: table_type; url: appendix/embedding.html#embed-table-type
+    text: table_read; url: appendix/embedding.html#embed-table-read
+    text: table_write; url: appendix/embedding.html#embed-table-write
+    text: table_size; url: appendix/embedding.html#embed-table-size
+    text: table_grow; url: appendix/embedding.html#embed-table-grow
+    text: mem_alloc; url: appendix/embedding.html#embed-mem-alloc
+    text: mem_type; url: appendix/embedding.html#embed-mem-type
+    text: mem_read; url: appendix/embedding.html#embed-mem-read
+    text: mem_write; url: appendix/embedding.html#embed-mem-write
+    text: mem_size; url: appendix/embedding.html#embed-mem-size
+    text: mem_grow; url: appendix/embedding.html#embed-mem-grow
+    text: global_alloc; url: appendix/embedding.html#embed-global-alloc
+    text: global_type; url: appendix/embedding.html#embed-global-type
+    text: global_read; url: appendix/embedding.html#embed-global-read
+    text: global_write; url: appendix/embedding.html#embed-global-write
     text: error; url: appendix/embedding.html#embed-error
     text: store; url: exec/runtime.html#syntax-store
     text: table type; url: syntax/types.html#syntax-tabletype
@@ -145,8 +147,6 @@
     text: external value; url: exec/runtime.html#syntax-externval
     text: host function; url: exec/runtime.html#syntax-hostfunc
     text: the instantiation algorithm; url: exec/modules.html#instantiation
-    text: size_table; url: appendix/embedding.html#embed-size-table
-    text: size_mem; url: appendix/embedding.html#embed-size-mem
     text: module; url: syntax/modules.html#syntax-module
     text: π—‚π—†π—‰π—ˆπ—‹π—π—Œ; url: syntax/modules.html#syntax-module
     url: syntax/types.html#external-types
@@ -267,8 +267,8 @@
 
 <div algorithm>
   To <dfn>compile a WebAssembly module</dfn> from source bytes |bytes|, perform the following steps:
-    1. Let |module| be [=decode_module=](|bytes|). If |module| is [=error=], return [=error=].
-    1. If [=validate_module=](|module|) is [=error=], return [=error=].
+    1. Let |module| be [=module_decode=](|bytes|). If |module| is [=error=], return [=error=].
+    1. If [=module_validate=](|module|) is [=error=], return [=error=].
     1. Return |module|.
 </div>
 
@@ -329,7 +329,7 @@
             1. If |v| has a \[[FunctionAddress]] internal slot, and therefore is an [=Exported Function=],
                 1. Let |funcaddr| be the value of |v|'s \[[FunctionAddress]] internal slot.
 
-                Note: The signature is checked by [=instantiate_module=] invoked below.
+                Note: The signature is checked by [=module_instantiate=] invoked below.
             1. Otherwise,
                 1. [=Create a host function=] from |v| and |functype|, and let |funcaddr| be the result.
                 1. Let |index| be the number of external functions in |imports|. This value |index| is known as the <dfn>index of the host function</dfn> |funcaddr|.
@@ -340,7 +340,7 @@
                 1. If |valtype| is [=π—‚πŸ¨πŸ¦=], throw a {{LinkError}} exception.
                 1. Let |value| be [=ToWebAssemblyValue=](|v|, |valtype|)
                 1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-                1. Let (|store|, |globaladdr|) be [=alloc_global=](|store|, [=const=] |valtype|, |value|).
+                1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, [=const=] |valtype|, |value|).
                 1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
             1. If |v| is a {{Global}} instance,
                 1. Let |globaladdr| be |v|.\[[Global]]
@@ -350,12 +350,12 @@
             1. [=Append=] |externglobal| to |imports|.
         1. If |externtype| is of the form [=𝗆𝖾𝗆=] <var ignore>memtype</var>,
             1. If |v| is not a {{Memory}} object, throw a {{LinkError}} exception.
-            1. Note: [=instantiate_module=] invoked below will check the imported {{Memory}}'s size against the importing module's requirements.
+            1. Note: [=module_instantiate=] invoked below will check the imported {{Memory}}'s size against the importing module's requirements.
             1. Let |externmem| be the [=external value=] [=external value|𝗆𝖾𝗆=]  |v|.\[[Memory]].
             1. [=Append=] |externmem| to |imports|.
         1. Otherwise, |externtype| is of the form [=𝗍𝖺𝖻𝗅𝖾=] <var ignore>tabletype</var>,
             1. If |v| is not a {{Table}} instance, throw a {{LinkError}} exception.
-            1. Note: The table's length, etc. is checked by [=instantiate_module=] invoked below.
+            1. Note: The table's length, etc. is checked by [=module_instantiate=] invoked below.
             1. Let |tableaddr| be |v|.\[[Table]]
             1. Let |externtable| be the [=external value=] [=external value|𝗍𝖺𝖻𝗅𝖾=] |tableaddr|.
             1. [=Append=] |externtable| to |imports|.
@@ -366,7 +366,7 @@
   To <dfn>create an instance object</dfn> from a WebAssembly module |module| and instance |instance|, perform the following steps:
     1. Let |exportsObject| be ! [=ObjectCreate=](null).
     1. For each pair (|name|, |externtype|) in [=module_exports=](|module|),
-        1. Let |externval| be [=get_export=](|instance|, |name|).
+        1. Let |externval| be [=instance_export=](|instance|, |name|).
         1. Assert: |externval| is not [=error=].
         1. If |externtype| is of the form [=π–Ώπ—Žπ—‡π–Ό=] <var ignore>functype</var>,
             1. Assert: |externval| is of the form [=external value|π–Ώπ—Žπ—‡π–Ό=] |funcaddr|.
@@ -399,7 +399,7 @@
 <div algorithm>
   To <dfn>instantiate the core of a WebAssembly module</dfn> from a module |module| and imports |imports|, perform the following steps:
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |result| be [=instantiate_module=](|store|, |module|, |imports|).
+    1. Let |result| be [=module_instantiate=](|store|, |module|, |imports|).
     1. If |result| is [=error=], throw an appropriate exception type:
         * A {{LinkError}} exception for most cases which occur during linking.
         * If the error came when running the start function, throw a {{RuntimeError}} for most errors which occur from WebAssembly, or the error object propagated from inner ECMAScript code.
@@ -612,7 +612,7 @@
     1. If |maximum| is not empty and |maximum| &lt; |initial|, throw a {{RangeError}} exception.
     1. Let |memtype| be { min |initial|, max |maximum| }
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let (|store|, |memaddr|) be [=alloc_mem=](|store|, |memtype|). If allocation fails, throw a {{RangeError}} exception.
+    1. Let (|store|, |memaddr|) be [=mem_alloc=](|store|, |memtype|). If allocation fails, throw a {{RangeError}} exception.
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
     1. [=Create a memory object=] from the memory address |memaddr| and return the result.
 </div>
@@ -633,8 +633,8 @@
     1. Let |memory| be the Memory instance.
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
     1. Let |memaddr| be |memory|.\[[Memory]].
-    1. Let |ret| be the [=size_mem=](|store|, |memaddr|).
-    1. Let |store| be [=grow_mem=](|store|, |memaddr|, |delta|).
+    1. Let |ret| be the [=mem_size=](|store|, |memaddr|).
+    1. Let |store| be [=mem_grow=](|store|, |memaddr|, |delta|).
     1. If |store| is [=error=], throw a {{RangeError}} exception.
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
     1. [=Reset the memory buffer=] of |memaddr|.
@@ -694,7 +694,7 @@
     1. If |map|[|tableaddr|] [=map/exists=],
         1. Return |map|[|tableaddr|].
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |values| be a list whose length is [=size_table=](|store|, |tableaddr|) where each element is null.
+    1. Let |values| be a list whose length is [=table_size=](|store|, |tableaddr|) where each element is null.
     1. Let |table| be a new {{Table}} instance with \[[Table]] set to |tableaddr| and \[[Values]] set to |values|.
     1. [=map/Set=] |map|[|tableaddr|] to |table|.
     1. Return |table|.
@@ -707,7 +707,7 @@
     1. If |maximum| is not empty and |maximum| &lt; |initial|, throw a {{RangeError}} exception.
     1. Let |type| be the [=table type=] {[=table type|𝗆𝗂𝗇=] n, [=table type|𝗆𝖺𝗑=] |maximum|} [=table type|π–Ίπ—‡π—’π–Ώπ—Žπ—‡π–Ό=].
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let (|store|, |tableaddr|) be [=alloc_table=](|store|, |type|). <!-- TODO(littledan): Report allocation failure https://github.com/WebAssembly/spec/issues/584 -->
+    1. Let (|store|, |tableaddr|) be [=table_alloc=](|store|, |type|). <!-- TODO(littledan): Report allocation failure https://github.com/WebAssembly/spec/issues/584 -->
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
     1. [=Create a table object=] from the table address |tableaddr| and return the result.
 </div>
@@ -717,7 +717,7 @@
     1. Let |tableaddr| be the Table instance's \[[Table]] internal slot.
     1. Let |initialSize| be the length of the Table instance's \[[Values]] internal slot.
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |result| be [=grow_table=](|store|, |tableaddr|, |delta|).
+    1. Let |result| be [=table_grow=](|store|, |tableaddr|, |delta|).
     1. If |result| is [=error=], throw a {{RangeError}} exception.
 
         Note: The above exception may happen due to either insufficient memory or an invalid size parameter.
@@ -748,7 +748,7 @@
         1. If |value| does not have a \[[FunctionAddress]] internal slot, throw a {{TypeError}} exception.
         1. Let |funcaddr| be |value|.\[[FunctionAddress]].
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |store| be [=write_table=](|store|, |tableaddr|, |index|, |funcaddr|).
+    1. Let |store| be [=table_write=](|store|, |tableaddr|, |index|, |funcaddr|).
     1. If |store| is [=error=], throw a {{RangeError}} exception.
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
     1. Set |values|[|index|] to |value|.
@@ -827,7 +827,7 @@
         1. Let |value| be [=ToWebAssemblyValue=](|v|, |valuetype|).
     1. If |mutable| is true, let |globaltype| be [=var=] |valuetype|; otherwise, let |globaltype| be [=const=] |valuetype|.
     1. Let |store| be the current agent's [=associated store=].
-    1. Let (|store|, |globaladdr|) be [=alloc_global=](|store|, |globaltype|, |value|). <!-- TODO(littledan): Report allocation failure https://github.com/WebAssembly/spec/issues/584 -->
+    1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, |globaltype|, |value|). <!-- TODO(littledan): Report allocation failure https://github.com/WebAssembly/spec/issues/584 -->
     1. Set the current agent's [=associated store=] to |store|.
     1. [=Create a global object=] from the global address |globaladdr| and return the result.
 </div>
@@ -836,9 +836,9 @@
     The algorithm <dfn>GetGlobalValue</dfn>({{Global}} |global|) performs the following steps:
     1. Let |store| be the current agent's [=associated store=].
     1. Let |globaladdr| be |global|.\[[Global]].
-    1. Let |globaltype| be [=type_global=](|store|, |globaladdr|).
+    1. Let |globaltype| be [=global_type=](|store|, |globaladdr|).
     1. If |globaltype| is of the form <var ignore>mut</var> [=π—‚πŸ¨πŸ¦=], throw a {{TypeError}}.
-    1. Let |value| be [=read_global=](|store|, |globaladdr|).
+    1. Let |value| be [=global_read=](|store|, |globaladdr|).
     1. Return [=ToJSValue=](|value|).
 </div>
 
@@ -851,11 +851,11 @@
     1. Let |global| be the {{Global}} instance.
     1. Let |store| be the current agent's [=associated store=].
     1. Let |globaladdr| be |global|.\[[Global]].
-    1. Let |globaltype| be [=type_global=](|store|, |globaladdr|), where |globaltype| is of the form |mut| |valuetype|.
+    1. Let |globaltype| be [=global_type=](|store|, |globaladdr|), where |globaltype| is of the form |mut| |valuetype|.
     1. If |mut| is [=const=], throw a {{TypeError}}.
     1. If |valuetype| is [=π—‚πŸ¨πŸ¦=], throw a {{TypeError}}.
     1. Let |value| be [=ToWebAssemblyValue=](|v|, |valuetype|).
-    1. Let |store| be [=write_global=](|store|, |globaladdr|, |value|).
+    1. Let |store| be [=global_write=](|store|, |globaladdr|, |value|).
     1. If |store| is [=error=], throw a {{RangeError}} exception.
     1. Set the current agent's [=associated store=] to |store|.
 </div>
@@ -898,7 +898,7 @@
     1. Let |function| be [=CreateBuiltinFunction=](|realm|, |steps|, [=%FunctionPrototype%=], &laquo; \[[FunctionAddress]] &raquo;).
     1. Set |function|.\[[FunctionAddress]] to |funcaddr|.
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |functype| be [=type_func=](|store|, |funcaddr|).
+    1. Let |functype| be [=func_type=](|store|, |funcaddr|).
     1. Let [|paramTypes|] → [<var ignore>resultTypes</var>] be |functype|.
     1. Let |arity| be the length of |paramTypes|.
     1. Perform ! [=SetFunctionLength=](|function|, |arity|).
@@ -912,7 +912,7 @@
   To <dfn>call an Exported Function</dfn> with [=function address=] |funcaddr| and a [=list=] of JavaScript arguments |argValues|, perform the following steps:
 
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |functype| be [=type_func=](|store|, |funcaddr|).
+    1. Let |functype| be [=func_type=](|store|, |funcaddr|).
     1. Let [|parameters|] → [|results|] be |functype|.
     1. If |parameters| or |results| contains an [=π—‚πŸ¨πŸ¦=], throw a {{TypeError}}.
 
@@ -926,7 +926,7 @@
         1. [=Append=] [=ToWebAssemblyValue=](|arg|, |t|) to |args|.
         1. Set |i| to |i| + 1.
     1. Let |argsSeq| be a WebAssembly [=sequence=] containing the elements of |args|.
-    1. Let (|store|, |ret|) be the result of [=invoke_func=](|store|, |funcaddr|, |argsSeq|).
+    1. Let (|store|, |ret|) be the result of [=func_invoke=](|store|, |funcaddr|, |argsSeq|).
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
     1. If |ret| is [=error=], throw an exception. This exception should be a WebAssembly {{RuntimeError}} exception, unless otherwise indicated by <a href="#errors">the WebAssembly error mapping</a>.
     1. If |ret| is empty, return undefined.
@@ -961,7 +961,7 @@
         1. If |result|.\[[Type]] is [=throw=], then trigger a WebAssembly trap, and propagate |result|.\[[Value]] to the enclosing JavaScript.
         1. Otherwise, return |result|.\[[Value]].
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let (|store|, |funcaddr|) be [=alloc_func=](|store|, |functype|, |hostfunc|).
+    1. Let (|store|, |funcaddr|) be [=func_alloc=](|store|, |functype|, |hostfunc|).
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
     1. Return |funcaddr|
 </div>