[spec] Add table.copy exec text

document/core/exec/instructions.rst

@@ -810,6 +810,96 @@ Memory Instructions
 Table Instructions
 ~~~~~~~~~~~~~~~~~~
 
+.. _exec-table.copy:
+
+:math:`\TABLECOPY`
+...................
+
+1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
+
+2. Assert: due to :ref:`validation <valid-table.copy>`, :math:`F.\AMODULE.\MITABLES[0]` exists.
+
+3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.
+
+4. Assert: due to :ref:`validation <valid-table.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+
+5. Pop the value :math:`\I32.\CONST~cnt` from the stack.
+
+6. Assert: due to :ref:`validation <valid-table.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+
+7. Pop the value :math:`\I32.\CONST~src` from the stack.
+
+8. Assert: due to :ref:`validation <valid-table.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+
+9. Pop the value :math:`\I32.\CONST~dst` from the stack.
+
+10. If :math:`cnt = 0`, then:
+
+    a. Return.
+
+11. If :math:`dst < src`, then:
+
+    a. Push the value :math:`\I32.\CONST~dst` to the stack.
+
+    b. Push the value :math:`\I32.\CONST~src` to the stack.
+
+    c. Execute the instruction :math:`\TABLEGET`.
+
+    d. Execute the instruction :math:`\TABLESET`.
+
+    e. Push the value :math:`\I32.\CONST~(dst+1)` to the stack.
+
+    f. Push the value :math:`\I32.\CONST~(src+1)` to the stack.
+
+12. Else:
+
+    a. Push the value :math:`\I32.\CONST~(dst+cnt-1)` to the stack.
+
+    b. Push the value :math:`\I32.\CONST~(src+cnt-1)` to the stack.
+
+    c. Execute the instruction :math:`\TABLEGET`.
+
+    d. Execute the instruction :math:`\TABLESET`.
+
+    e. Push the value :math:`\I32.\CONST~dst` to the stack.
+
+    f. Push the value :math:`\I32.\CONST~src` to the stack.
+
+13. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
+
+14. Execute the instruction :math:`\TABLECOPY`.
+
+.. math::
+   ~\\[-1ex]
+   \begin{array}{l}
+   \begin{array}{lcl@{\qquad}l}
+   S; F; (\I32.\CONST~dst)~(\I32.\CONST~(src)~(\I32.\CONST~0)~(\TABLECOPY) &\stepto& S'; F; \epsilon
+   \end{array}
+   \\[1ex]
+   \begin{array}{lcl@{\qquad}l}
+   S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt+1))~(\TABLECOPY) &\stepto& S; F;
+     \begin{array}[t]{@{}l@{}}
+     (\I32.\CONST~dst)~((\I32.\CONST~src)~\TABLEGET)~\TABLESET \\
+     (\I32.\CONST~(dst+1))~(\I32.\CONST~(src+1))~(\I32.\CONST~cnt)~(\TABLECOPY~x) \\
+     \end{array} \\
+   \end{array} \\
+   \\ \qquad
+     \begin{array}[t]{@{}r@{~}l@{}}
+     (\iff & dst < src)
+     \end{array}
+   \\[1ex]
+   \begin{array}{lcl@{\qquad}l}
+   S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt+1))~(\TABLECOPY) &\stepto& S; F;
+     \begin{array}[t]{@{}l@{}}
+     (\I32.\CONST~(dst+cnt-1))~((\I32.\CONST~(src+cnt-1))~\TABLEGET)~\TABLESET \\
+     (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~(\TABLECOPY) \\
+     \end{array} \\
+   \end{array} \\
+   \\ \qquad
+     (\otherwise) \\
+   \end{array}
+
+
 .. _exec-table.init:
 
 :math:`\TABLEINIT~x`