WIP - memory.fill spec text

Author: eqrion

document/core/exec/instructions.rst

@@ -689,24 +689,21 @@ Memory Instructions
    S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\MEMORYFILL) &\stepto& S; F; \epsilon
    \end{array} \\
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~1)~(\MEMORYFILL) &\stepto& S; F;
-     (\I32.\CONST~i)~\val~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\
-   \end{array} \\
+   S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n)~(\MEMORYFILL) &\stepto& S; F; \TRAP \\
+   \end{array}
+   \\ \qquad
+     \begin{array}[t]{@{}r@{~}l@{}}
+     (\iff & \X{i} + \X{n} \gt |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|) \\
+     \end{array} \\
    \begin{array}{lcl@{\qquad}l}
    S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n)~(\MEMORYFILL) &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
-     (\I32.\CONST~i)~\val~(\I32.\CONST~1)~(\MEMORYFILL) \\
-     (\vconst_{\I32}(i+1))~\val~(\I32.\CONST~(n-1))~(\MEMORYFILL) \\
+     (\I32.\CONST~i)~\val~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\
+     (\I32.\CONST~(i+1))~\val~(\I32.\CONST~(n-1))~(\MEMORYFILL) \\
      \end{array} \\
    \end{array}
-   \\ \qquad
-     (\iff n > 1) \\
    \end{array}
 
-.. note::
-   The use of the :math:`\vconst_t` meta function in the rules for this and the following instructions ensures that an overflowing index turns into a :ref:`trap <syntax-trap>`.
-
-
 .. _exec-memory.init:
 
 :math:`\MEMORYINIT~x`

document/core/exec/runtime.rst

@@ -29,19 +29,6 @@ It is convenient to reuse the same notation as for the |CONST| :ref:`instruction
      \F64.\CONST~\f64
    \end{array}
 
-Conventions
-...........
-
-The following auxiliary notation is defined for constant values, to ensure they are well-formed for the given :ref:`value type <syntax-valtype>`.
-
-.. math::
-   \begin{array}{lcl@{\qquad}l}
-   \vconst_t(x) &=& (t\K{.}\CONST~x)
-     & (\iff x~\mbox{is well-formed for}~t) \\
-   \vconst_t(x) &=& \TRAP
-     & (\otherwise) \\
-   \end{array}
-
 
 .. index:: ! result, value, trap
    pair: abstract syntax; result