[spec/interpreter/tests] Rename instructions (#926)

* Rename {get,set,tee}_{local,global} to {local,global}.{get,set,tee}
* Rename anyfunc to funcref
* Rename conversion operators

document/core/appendix/index-types.rst

@@ -13,7 +13,7 @@ Category                                  Constructor
 :ref:`Value type <syntax-valtype>`        |F32|                                        :math:`\hex{7D}` (-3 as |Bs7|)
 :ref:`Value type <syntax-valtype>`        |F64|                                        :math:`\hex{7C}` (-4 as |Bs7|)
 (reserved)                                                                             :math:`\hex{7C}` .. :math:`\hex{71}`
-:ref:`Element type <syntax-elemtype>`     |ANYFUNC|                                    :math:`\hex{70}` (-16 as |Bs7|)
+:ref:`Element type <syntax-elemtype>`     |FUNCREF|                                    :math:`\hex{70}` (-16 as |Bs7|)
 (reserved)                                                                             :math:`\hex{6F}` .. :math:`\hex{61}`
 :ref:`Function type <syntax-functype>`    :math:`[\valtype^\ast] \to [\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 (reserved)                                                                             :math:`\hex{5F}` .. :math:`\hex{41}`

document/core/appendix/properties.rst

@@ -220,15 +220,15 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * The :ref:`limits <syntax-limits>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-limits>`.
 
-* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\{\LMIN~n, \LMAX~m^?\}~\ANYFUNC`.
+* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\{\LMIN~n, \LMAX~m^?\}~\FUNCREF`.
 
 .. math::
    \frac{
      ((S \vdash \EVFUNC~\X{fa} : \ETFUNC~\functype)^?)^n
      \qquad
      \vdashlimits \{\LMIN~n, \LMAX~m^?\} \ok
    }{
-     S \vdashtableinst \{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \} : \{\LMIN~n, \LMAX~m^?\}~\ANYFUNC
+     S \vdashtableinst \{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \} : \{\LMIN~n, \LMAX~m^?\}~\FUNCREF
    }
 
 
@@ -490,7 +490,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 :math:`\INITELEM~\tableaddr~o~x^n`
 ..................................
 
-* The :ref:`external table value <syntax-externval>` :math:`\EVTABLE~\tableaddr` must be :ref:`valid <valid-externval-table>` with some :ref:`external table type <syntax-externtype>` :math:`\ETTABLE~\limits~\ANYFUNC`.
+* The :ref:`external table value <syntax-externval>` :math:`\EVTABLE~\tableaddr` must be :ref:`valid <valid-externval-table>` with some :ref:`external table type <syntax-externtype>` :math:`\ETTABLE~\limits~\FUNCREF`.
 
 * The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN`.
 
@@ -502,7 +502,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 .. math::
    \frac{
-     S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\ANYFUNC
+     S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\FUNCREF
      \qquad
      o + n \leq \limits.\LMIN
      \qquad

document/core/binary/instructions.rst

@@ -93,20 +93,20 @@ Variable Instructions
 
 :ref:`Variable instructions <syntax-instr-variable>` are represented by byte codes followed by the encoding of the respective :ref:`index <syntax-index>`.
 
-.. _binary-get_local:
-.. _binary-set_local:
-.. _binary-tee_local:
-.. _binary-get_global:
-.. _binary-set_global:
+.. _binary-local.get:
+.. _binary-local.set:
+.. _binary-local.tee:
+.. _binary-global.get:
+.. _binary-global.set:
 
 .. math::
    \begin{array}{llclll}
    \production{instruction} & \Binstr &::=& \dots \\ &&|&
-     \hex{20}~~x{:}\Blocalidx &\Rightarrow& \GETLOCAL~x \\ &&|&
-     \hex{21}~~x{:}\Blocalidx &\Rightarrow& \SETLOCAL~x \\ &&|&
-     \hex{22}~~x{:}\Blocalidx &\Rightarrow& \TEELOCAL~x \\ &&|&
-     \hex{23}~~x{:}\Bglobalidx &\Rightarrow& \GETGLOBAL~x \\ &&|&
-     \hex{24}~~x{:}\Bglobalidx &\Rightarrow& \SETGLOBAL~x \\
+     \hex{20}~~x{:}\Blocalidx &\Rightarrow& \LOCALGET~x \\ &&|&
+     \hex{21}~~x{:}\Blocalidx &\Rightarrow& \LOCALSET~x \\ &&|&
+     \hex{22}~~x{:}\Blocalidx &\Rightarrow& \LOCALTEE~x \\ &&|&
+     \hex{23}~~x{:}\Bglobalidx &\Rightarrow& \GLOBALGET~x \\ &&|&
+     \hex{24}~~x{:}\Bglobalidx &\Rightarrow& \GLOBALSET~x \\
    \end{array}
 
 
@@ -336,31 +336,31 @@ All other numeric instructions are plain opcodes without any immediates.
 .. math::
    \begin{array}{llclll}
    \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|&
-     \hex{A7} &\Rightarrow& \I32.\WRAP\K{/}\I64 \\ &&|&
-     \hex{A8} &\Rightarrow& \I32.\TRUNC\K{\_s/}\F32 \\ &&|&
-     \hex{A9} &\Rightarrow& \I32.\TRUNC\K{\_u/}\F32 \\ &&|&
-     \hex{AA} &\Rightarrow& \I32.\TRUNC\K{\_s/}\F64 \\ &&|&
-     \hex{AB} &\Rightarrow& \I32.\TRUNC\K{\_u/}\F64 \\ &&|&
-     \hex{AC} &\Rightarrow& \I64.\EXTEND\K{\_s/}\I32 \\ &&|&
-     \hex{AD} &\Rightarrow& \I64.\EXTEND\K{\_u/}\I32 \\ &&|&
-     \hex{AE} &\Rightarrow& \I64.\TRUNC\K{\_s/}\F32 \\ &&|&
-     \hex{AF} &\Rightarrow& \I64.\TRUNC\K{\_u/}\F32 \\ &&|&
-     \hex{B0} &\Rightarrow& \I64.\TRUNC\K{\_s/}\F64 \\ &&|&
-     \hex{B1} &\Rightarrow& \I64.\TRUNC\K{\_u/}\F64 \\ &&|&
-     \hex{B2} &\Rightarrow& \F32.\CONVERT\K{\_s/}\I32 \\ &&|&
-     \hex{B3} &\Rightarrow& \F32.\CONVERT\K{\_u/}\I32 \\ &&|&
-     \hex{B4} &\Rightarrow& \F32.\CONVERT\K{\_s/}\I64 \\ &&|&
-     \hex{B5} &\Rightarrow& \F32.\CONVERT\K{\_u/}\I64 \\ &&|&
-     \hex{B6} &\Rightarrow& \F32.\DEMOTE\K{/}\F64 \\ &&|&
-     \hex{B7} &\Rightarrow& \F64.\CONVERT\K{\_s/}\I32 \\ &&|&
-     \hex{B8} &\Rightarrow& \F64.\CONVERT\K{\_u/}\I32 \\ &&|&
-     \hex{B9} &\Rightarrow& \F64.\CONVERT\K{\_s/}\I64 \\ &&|&
-     \hex{BA} &\Rightarrow& \F64.\CONVERT\K{\_u/}\I64 \\ &&|&
-     \hex{BB} &\Rightarrow& \F64.\PROMOTE\K{/}\F32 \\ &&|&
-     \hex{BC} &\Rightarrow& \I32.\REINTERPRET\K{/}\F32 \\ &&|&
-     \hex{BD} &\Rightarrow& \I64.\REINTERPRET\K{/}\F64 \\ &&|&
-     \hex{BE} &\Rightarrow& \F32.\REINTERPRET\K{/}\I32 \\ &&|&
-     \hex{BF} &\Rightarrow& \F64.\REINTERPRET\K{/}\I64 \\
+     \hex{A7} &\Rightarrow& \I32.\WRAP\K{\_}\I64 \\ &&|&
+     \hex{A8} &\Rightarrow& \I32.\TRUNC\K{\_}\F32\K{\_s} \\ &&|&
+     \hex{A9} &\Rightarrow& \I32.\TRUNC\K{\_}\F32\K{\_u} \\ &&|&
+     \hex{AA} &\Rightarrow& \I32.\TRUNC\K{\_}\F64\K{\_s} \\ &&|&
+     \hex{AB} &\Rightarrow& \I32.\TRUNC\K{\_}\F64\K{\_u} \\ &&|&
+     \hex{AC} &\Rightarrow& \I64.\EXTEND\K{\_}\I32\K{\_s} \\ &&|&
+     \hex{AD} &\Rightarrow& \I64.\EXTEND\K{\_}\I32\K{\_u} \\ &&|&
+     \hex{AE} &\Rightarrow& \I64.\TRUNC\K{\_}\F32\K{\_s} \\ &&|&
+     \hex{AF} &\Rightarrow& \I64.\TRUNC\K{\_}\F32\K{\_u} \\ &&|&
+     \hex{B0} &\Rightarrow& \I64.\TRUNC\K{\_}\F64\K{\_s} \\ &&|&
+     \hex{B1} &\Rightarrow& \I64.\TRUNC\K{\_}\F64\K{\_u} \\ &&|&
+     \hex{B2} &\Rightarrow& \F32.\CONVERT\K{\_}\I32\K{\_s} \\ &&|&
+     \hex{B3} &\Rightarrow& \F32.\CONVERT\K{\_}\I32\K{\_u} \\ &&|&
+     \hex{B4} &\Rightarrow& \F32.\CONVERT\K{\_}\I64\K{\_s} \\ &&|&
+     \hex{B5} &\Rightarrow& \F32.\CONVERT\K{\_}\I64\K{\_u} \\ &&|&
+     \hex{B6} &\Rightarrow& \F32.\DEMOTE\K{\_}\F64 \\ &&|&
+     \hex{B7} &\Rightarrow& \F64.\CONVERT\K{\_}\I32\K{\_s} \\ &&|&
+     \hex{B8} &\Rightarrow& \F64.\CONVERT\K{\_}\I32\K{\_u} \\ &&|&
+     \hex{B9} &\Rightarrow& \F64.\CONVERT\K{\_}\I64\K{\_s} \\ &&|&
+     \hex{BA} &\Rightarrow& \F64.\CONVERT\K{\_}\I64\K{\_u} \\ &&|&
+     \hex{BB} &\Rightarrow& \F64.\PROMOTE\K{\_}\F32 \\ &&|&
+     \hex{BC} &\Rightarrow& \I32.\REINTERPRET\K{\_}\F32 \\ &&|&
+     \hex{BD} &\Rightarrow& \I64.\REINTERPRET\K{\_}\F64 \\ &&|&
+     \hex{BE} &\Rightarrow& \F32.\REINTERPRET\K{\_}\I32 \\ &&|&
+     \hex{BF} &\Rightarrow& \F64.\REINTERPRET\K{\_}\I64 \\
    \end{array}
 
 

document/core/binary/types.rst

@@ -115,7 +115,7 @@ Table Types
    \production{table type} & \Btabletype &::=&
      \X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\
    \production{element type} & \Belemtype &::=&
-     \hex{70} &\Rightarrow& \ANYFUNC \\
+     \hex{70} &\Rightarrow& \FUNCREF \\
    \end{array}
 
 

document/core/exec/instructions.rst

@@ -28,7 +28,7 @@ And for :ref:`conversion operators <exec-cvtop>`:
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \X{cvtop}_{t_1,t_2}(c) &=& \X{cvtop}_{|t_1|,|t_2|}(c) \\
+   \X{cvtop}^{\sx^?}_{t_1,t_2}(c) &=& \X{cvtop}^{\sx^?}_{|t_1|,|t_2|}(c) \\
    \end{array}
 
 Where the underlying operators are partial, the corresponding instruction will :ref:`trap <trap>` when the result is not defined.
@@ -148,16 +148,16 @@ Where the underlying operators are non-deterministic, because they may return on
 
 .. _exec-cvtop:
 
-:math:`t_2\K{.}\cvtop/t_1`
-..........................
+:math:`t_2\K{.}\cvtop\K{\_}t_1\K{\_}\sx^?`
+..........................................
 
 1. Assert: due to :ref:`validation <valid-cvtop>`, a value of :ref:`value type <syntax-valtype>` :math:`t_1` is on the top of the stack.
 
 2. Pop the value :math:`t_1.\CONST~c_1` from the stack.
 
-3. If :math:`\cvtop_{t_1,t_2}(c_1)` is defined:
+3. If :math:`\cvtop^{\sx^?}_{t_1,t_2}(c_1)` is defined:
 
-   a. Let :math:`c_2` be a possible result of computing :math:`\cvtop_{t_1,t_2}(c_1)`.
+   a. Let :math:`c_2` be a possible result of computing :math:`\cvtop^{\sx^?}_{t_1,t_2}(c_1)`.
 
    b. Push the value :math:`t_2.\CONST~c_2` to the stack.
 
@@ -167,10 +167,10 @@ Where the underlying operators are non-deterministic, because they may return on
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   (t_1\K{.}\CONST~c_1)~t_2\K{.}\cvtop\K{/}t_1 &\stepto& (t_2\K{.}\CONST~c_2)
-     & (\iff c_2 \in \cvtop_{t_1,t_2}(c_1)) \\
-   (t_1\K{.}\CONST~c_1)~t_2\K{.}\cvtop\K{/}t_1 &\stepto& \TRAP
-     & (\iff \cvtop_{t_1,t_2}(c_1) = \{\})
+   (t_1\K{.}\CONST~c_1)~t_2\K{.}\cvtop\K{\_}t_1\K{\_}\sx^? &\stepto& (t_2\K{.}\CONST~c_2)
+     & (\iff c_2 \in \cvtop^{\sx^?}_{t_1,t_2}(c_1)) \\
+   (t_1\K{.}\CONST~c_1)~t_2\K{.}\cvtop\K{\_}t_1\K{\_}\sx^? &\stepto& \TRAP
+     & (\iff \cvtop^{\sx^?}_{t_1,t_2}(c_1) = \{\})
    \end{array}
 
 
@@ -237,81 +237,81 @@ Parametric Instructions
 Variable Instructions
 ~~~~~~~~~~~~~~~~~~~~~
 
-.. _exec-get_local:
+.. _exec-local.get:
 
-:math:`\GETLOCAL~x`
+:math:`\LOCALGET~x`
 ...................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-get_local>`, :math:`F.\ALOCALS[x]` exists.
+2. Assert: due to :ref:`validation <valid-local.get>`, :math:`F.\ALOCALS[x]` exists.
 
 3. Let :math:`\val` be the value :math:`F.\ALOCALS[x]`.
 
 4. Push the value :math:`\val` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   F; (\GETLOCAL~x) &\stepto& F; \val
+   F; (\LOCALGET~x) &\stepto& F; \val
      & (\iff F.\ALOCALS[x] = \val) \\
    \end{array}
 
 
-.. _exec-set_local:
+.. _exec-local.set:
 
-:math:`\SETLOCAL~x`
+:math:`\LOCALSET~x`
 ...................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-set_local>`, :math:`F.\ALOCALS[x]` exists.
+2. Assert: due to :ref:`validation <valid-local.set>`, :math:`F.\ALOCALS[x]` exists.
 
-3. Assert: due to :ref:`validation <valid-set_local>`, a value is on the top of the stack.
+3. Assert: due to :ref:`validation <valid-local.set>`, a value is on the top of the stack.
 
 4. Pop the value :math:`\val` from the stack.
 
 5. Replace :math:`F.\ALOCALS[x]` with the value :math:`\val`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   F; \val~(\SETLOCAL~x) &\stepto& F'; \epsilon
+   F; \val~(\LOCALSET~x) &\stepto& F'; \epsilon
      & (\iff F' = F \with \ALOCALS[x] = \val) \\
    \end{array}
 
 
-.. _exec-tee_local:
+.. _exec-local.tee:
 
-:math:`\TEELOCAL~x`
+:math:`\LOCALTEE~x`
 ...................
 
-1. Assert: due to :ref:`validation <valid-tee_local>`, a value is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-local.tee>`, a value is on the top of the stack.
 
 2. Pop the value :math:`\val` from the stack.
 
 3. Push the value :math:`\val` to the stack.
 
 4. Push the value :math:`\val` to the stack.
 
-5. :ref:`Execute <exec-set_local>` the instruction :math:`(\SETLOCAL~x)`.
+5. :ref:`Execute <exec-local.set>` the instruction :math:`(\LOCALSET~x)`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   \val~(\TEELOCAL~x) &\stepto& \val~\val~(\SETLOCAL~x)
+   \val~(\LOCALTEE~x) &\stepto& \val~\val~(\LOCALSET~x)
    \end{array}
 
 
-.. _exec-get_global:
+.. _exec-global.get:
 
-:math:`\GETGLOBAL~x`
+:math:`\GLOBALGET~x`
 ....................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-get_global>`, :math:`F.\AMODULE.\MIGLOBALS[x]` exists.
+2. Assert: due to :ref:`validation <valid-global.get>`, :math:`F.\AMODULE.\MIGLOBALS[x]` exists.
 
 3. Let :math:`a` be the :ref:`global address <syntax-globaladdr>` :math:`F.\AMODULE.\MIGLOBALS[x]`.
 
-4. Assert: due to :ref:`validation <valid-get_global>`, :math:`S.\SGLOBALS[a]` exists.
+4. Assert: due to :ref:`validation <valid-global.get>`, :math:`S.\SGLOBALS[a]` exists.
 
 5. Let :math:`\X{glob}` be the :ref:`global instance <syntax-globalinst>` :math:`S.\SGLOBALS[a]`.
 
@@ -322,29 +322,29 @@ Variable Instructions
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\GETGLOBAL~x) &\stepto& S; F; \val
+   S; F; (\GLOBALGET~x) &\stepto& S; F; \val
    \end{array}
    \\ \qquad
      (\iff S.\SGLOBALS[F.\AMODULE.\MIGLOBALS[x]].\GIVALUE = \val) \\
    \end{array}
 
 
-.. _exec-set_global:
+.. _exec-global.set:
 
-:math:`\SETGLOBAL~x`
+:math:`\GLOBALSET~x`
 ....................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-set_global>`, :math:`F.\AMODULE.\MIGLOBALS[x]` exists.
+2. Assert: due to :ref:`validation <valid-global.set>`, :math:`F.\AMODULE.\MIGLOBALS[x]` exists.
 
 3. Let :math:`a` be the :ref:`global address <syntax-globaladdr>` :math:`F.\AMODULE.\MIGLOBALS[x]`.
 
-4. Assert: due to :ref:`validation <valid-set_global>`, :math:`S.\SGLOBALS[a]` exists.
+4. Assert: due to :ref:`validation <valid-global.set>`, :math:`S.\SGLOBALS[a]` exists.
 
 5. Let :math:`\X{glob}` be the :ref:`global instance <syntax-globalinst>` :math:`S.\SGLOBALS[a]`.
 
-6. Assert: due to :ref:`validation <valid-set_global>`, a value is on the top of the stack.
+6. Assert: due to :ref:`validation <valid-global.set>`, a value is on the top of the stack.
 
 7. Pop the value :math:`\val` from the stack.
 
@@ -353,14 +353,14 @@ Variable Instructions
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; F; \val~(\SETGLOBAL~x) &\stepto& S'; F; \epsilon
+   S; F; \val~(\GLOBALSET~x) &\stepto& S'; F; \epsilon
    \end{array}
    \\ \qquad
    (\iff S' = S \with \SGLOBALS[F.\AMODULE.\MIGLOBALS[x]].\GIVALUE = \val) \\
    \end{array}
 
 .. note::
-   :ref:`Validation <valid-set_global>` ensures that the global is, in fact, marked as mutable.
+   :ref:`Validation <valid-global.set>` ensures that the global is, in fact, marked as mutable.
 
 
 .. index:: memory instruction, memory index, store, frame, address, memory address, memory instance, store, frame, value, integer, limits, value type, bit width

document/core/exec/modules.rst

@@ -43,13 +43,13 @@ The following auxiliary typing rules specify this typing relation relative to a
 
 * The store entry :math:`S.\STABLES[a]` must be a :ref:`table instance <syntax-tableinst>` :math:`\{\TIELEM~(\X{fa}^?)^n, \TIMAX~m^?\}`.
 
-* Then :math:`\EVTABLE~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETTABLE~(\{\LMIN~n, \LMAX~m^?\}~\ANYFUNC)`.
+* Then :math:`\EVTABLE~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETTABLE~(\{\LMIN~n, \LMAX~m^?\}~\FUNCREF)`.
 
 .. math::
    \frac{
      S.\STABLES[a] = \{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}
    }{
-     S \vdashexternval \EVTABLE~a : \ETTABLE~(\{\LMIN~n, \LMAX~m^?\}~\ANYFUNC)
+     S \vdashexternval \EVTABLE~a : \ETTABLE~(\{\LMIN~n, \LMAX~m^?\}~\FUNCREF)
    }