diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
index 81c81ea85..9ffe84591 100644
--- a/document/core/exec/instructions.rst
+++ b/document/core/exec/instructions.rst
@@ -380,7 +380,7 @@ Reference Instructions
 :math:`\I31NEW`
 ...............
 
-1. Assert: due to :ref:`validation <valid-extern.externalize>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` |I32| is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-i31.new>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` |I32| is on the top of the stack.
 
 2. Pop the value :math:`(\I32.\CONST~i)` from the stack.
 
@@ -399,7 +399,7 @@ Reference Instructions
 :math:`\I31GET\K{\_}\sx`
 ........................
 
-1. Assert: due to :ref:`validation <valid-extern.externalize>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~\I31)` is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-i31.get_s>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~\I31)` is on the top of the stack.
 
 2. Pop the value :math:`\reff` from the stack.
 
@@ -427,8 +427,35 @@ Reference Instructions
 :math:`\STRUCTNEW~\typeidx`
 ...........................
 
-.. todo:: Abstract allocation of structs and arrays into alloc functions
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-struct.new>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-struct.new>`, :math:`\deftype` is a :ref:`structure type <syntax-structtype>`.
+
+4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`structure type <syntax-structtype>` :math:`\deftype`. (todo: unroll)
+
+5. Let :math:`n` be the length of the :ref:`field type <syntax-fieldtype>` sequence :math:`\X{ft}^\ast`.
+
+6. Assert: due to :ref:`validation <valid-struct.set>`, :math:`n` :ref:`values <syntax-val>` are on the top of the stack.
+
+7. Pop the :math:`n` values :math:`\val^\ast` from the stack.
+
+8. For every value :math:`\val_i` in :math:`\val^\ast` and corresponding :ref:`field type <syntax-fieldtype>` :math:`\X{ft}_i` in :math:`\X{ft}^\ast`:
+
+   a. Let :math:`\fieldval_i` be the result of computing :math:`\packval_{\X{ft}_i}(\val_i))`.
+
+9. Let :math:`\fieldval^\ast` the concatenation of all field values :math:`\fieldval_i`.
+
+10. Let :math:`\X{si}` be the :ref:`structure instance <syntax-structinst>` :math:`\{\SITYPE~\deftype, \SIFIELDS~\fieldval^\ast\}`.
+
+11. Let :math:`a` be the length of :math:`S.\SSTRUCTS`.
+
+12. Append :math:`\X{si}` to :math:`S.\SSTRUCTS`.
+
+13. Return the :ref:`structure reference <syntax-ref.struct>` :math:`\REFSTRUCTADDR~a`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -436,7 +463,7 @@ Reference Instructions
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
       (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\
-      \land & \X{si} = \{\SITYPE~F.\AMODULE[x], \SIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\
+      \land & \X{si} = \{\SITYPE~F.\AMODULE.\MITYPES[x], \SIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\
       \land & S' = S \with \SSTRUCTS = S.\SSTRUCTS~\X{si})
      \end{array} \\
    \end{array}
@@ -447,7 +474,27 @@ Reference Instructions
 :math:`\STRUCTNEWDEFAULT~\typeidx`
 ..................................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-struct.new_default>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-struct.new_default>`, :math:`\deftype` is a :ref:`structure type <syntax-structtype>`.
+
+4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`structure type <syntax-structtype>` :math:`\deftype`. (todo: unroll)
+
+5. Let :math:`n` be the length of the :ref:`field type <syntax-fieldtype>` sequence :math:`\X{ft}^\ast`.
+
+6. For every :ref:`field type <syntax-fieldtype>` :math:`\X{ft}_i` in :math:`\X{ft}^\ast`:
+
+   a. Let :math:`t_i` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\X{ft}_i)`.
+
+   b. Assert: due to :ref:`validation <valid-struct.new_default>`, :math:`\default_{t_i}` is defined.
+
+   c. Push the :ref:`value <syntax-val>` :math:`\default_{t_i}` to the stack.
+
+7. Execute the instruction :math:`(\STRUCTNEW~\typeidx)`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -465,7 +512,7 @@ Reference Instructions
         \\&&
         \begin{array}[t]{@{}r@{~}l@{}}
          (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\
-         \land & \X{si} = \{\SITYPE~F.\AMODULE[x], \SIFIELDS~(\packval_{\X{ft}}(\default_{\unpacktype(\X{ft})}))^n\} \\
+         \land & \X{si} = \{\SITYPE~F.\AMODULE.\MITYPES[x], \SIFIELDS~(\packval_{\X{ft}}(\default_{\unpacktype(\X{ft})}))^n\} \\
          \land & S' = S \with \SSTRUCTS = S.\SSTRUCTS~\X{si})
         \end{array} \\
       \end{array}
@@ -477,15 +524,45 @@ Reference Instructions
 :math:`\STRUCTGET\K{\_}\sx^?~\typeidx~i`
 ........................................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-struct.get>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-struct.get>`, :math:`\deftype` is a :ref:`structure type <syntax-structtype>` with at least :math:`i + 1` fields.
+
+4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`structure type <syntax-structtype>` :math:`\deftype`. (todo: unroll)
+
+5. Let :math:`\X{ft}_i` be the :math:`i`-th :ref:`field type <syntax-fieldtype>` of :math:`\X{ft}^\ast`.
+
+6. Assert: due to :ref:`validation <valid-struct.get>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~x)` is on the top of the stack.
+
+7. Pop the value :math:`\reff` from the stack.
+
+8. If :math:`\reff` is :math:`\REFNULL~t`, then:
+
+   a. Trap.
+
+9. Assert: due to validation, a :math:`\reff` is a :ref:`structure reference <syntax-ref.struct>`.
+
+10. Let :math:`(\REFSTRUCTADDR~a)` be the reference value :math:`\reff`.
+
+11. Assert: due to :ref:`validation <valid-struct.get>`, the :ref:`structure instance <syntax-structinst>` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`i + 1` fields.
+
+12. Let :math:`\fieldval` be the :ref:`field value <syntax-fieldval>` :math:`S.\SSTRUCTS[a].\SIFIELDS[i]`.
+
+13. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}_i}(\fieldval))`.
+
+14. Push the value :math:`\val` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
    S; F; (\REFSTRUCTADDR~a)~(\STRUCTGET\K{\_}\sx^?~x~i) &\stepto& \val
      &
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\
-      \land & \val = \unpackval^{\sx^?}_{\X{ft}[i]}(S.\SSTRUCTS[a].\SIFIELDS[i]))
+      (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^\ast \\
+      \land & \val = \unpackval^{\sx^?}_{\X{ft}^\ast[i]}(S.\SSTRUCTS[a].\SIFIELDS[i]))
      \end{array} \\
    S; F; (\REFNULL~t)~(\STRUCTGET\K{\_}\sx^?~x~i) &\stepto& \TRAP
    \end{array}
@@ -496,15 +573,47 @@ Reference Instructions
 :math:`\STRUCTSET~\typeidx~i`
 .............................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-struct.set>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-struct.set>`, :math:`\deftype` is a :ref:`structure type <syntax-structtype>` with at least :math:`i + 1` fields.
+
+4. Let :math:`\TSTRUCT~\X{ft}^\ast` be the :ref:`structure type <syntax-structtype>` :math:`\deftype`. (todo: unroll)
+
+5. Let :math:`\X{ft}_i` be the :math:`i`-th :ref:`field type <syntax-fieldtype>` of :math:`\X{ft}^\ast`.
+
+6. Assert: due to :ref:`validation <valid-struct.set>`, a :ref:`value <syntax-val>` is on the top of the stack.
+
+7. Pop the value :math:`\val` from the stack.
+
+8. Assert: due to :ref:`validation <valid-struct.set>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~x)` is on the top of the stack.
+
+9. Pop the value :math:`\reff` from the stack.
+
+10. If :math:`\reff` is :math:`\REFNULL~t`, then:
+
+   a. Trap.
+
+11. Assert: due to validation, a :math:`\reff` is a :ref:`structure reference <syntax-ref.struct>`.
+
+12. Let :math:`(\REFSTRUCTADDR~a)` be the reference value :math:`\reff`.
+
+13. Assert: due to :ref:`validation <valid-struct.set>`, the :ref:`structure instance <syntax-structinst>` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`i + 1` fields.
+
+14. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}_i}(\val))`.
+
+15. Replace the :ref:`field value <syntax-fieldval>` :math:`S.\SSTRUCTS[a].\SIFIELDS[i]` with :math:`\fieldval`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
    S; F; (\REFSTRUCTADDR~a)~\val~(\STRUCTSET~x~i) &\stepto& S'; \epsilon
      &
      \begin{array}[t]{@{}r@{~}l@{}}
-     (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\
-      \land & S' = S \with \SSTRUCTS[a].\SIFIELDS[i] = \packval_{\X{ft}[i]}(\val))
+     (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^\ast \\
+      \land & S' = S \with \SSTRUCTS[a].\SIFIELDS[i] = \packval_{\X{ft}^\ast[i]}(\val))
      \end{array} \\
    S; F; (\REFNULL~t)~\val~(\STRUCTSET~x~i) &\stepto& \TRAP
    \end{array}
@@ -515,7 +624,27 @@ Reference Instructions
 :math:`\ARRAYNEW~\typeidx`
 ..........................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.new>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.new>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-array.new>`, a :ref:`value <syntax-val>` of type :math:`\I32` is on the top of the stack.
+
+6. Pop the value :math:`(\I32.\CONST~n)` from the stack.
+
+7. Assert: due to :ref:`validation <valid-array.new>`, a :ref:`value <syntax-val>` is on the top of the stack.
+
+8. Pop the value :math:`\val` from the stack.
+
+9. Push the value :math:`\val` to the stack :math:`n` times.
+
+10. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -529,7 +658,7 @@ Reference Instructions
         \\&&
         \begin{array}[t]{@{}r@{~}l@{}}
          (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\
-         \land & \X{ai} = \{\AITYPE~F.\AMODULE[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\
+         \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\
          \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai})
         \end{array} \\
       \end{array}
@@ -540,14 +669,34 @@ Reference Instructions
 :math:`\ARRAYNEWDEFAULT~\typeidx`
 ..................................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.new_default>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.new_default>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-array.new_default>`, a :ref:`value <syntax-val>` of type :math:`\I32` is on the top of the stack.
+
+6. Pop the value :math:`(\I32.\CONST~n)` from the stack.
+
+7. Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\X{ft})`.
+
+8. Assert: due to :ref:`validation <valid-array.new_default>`, :math:`\default_t` is defined.
+
+9. Push the :ref:`value <syntax-val>` :math:`\default_t` to the stack :math:`n` times.
+
+10. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
    F; (\I32.\CONST~n)~(\ARRAYNEWDEFAULT~x) &\stepto& (\default_{\unpacktype(\X{ft}}))^n~(\ARRAYNEWFIXED~x~n)
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft})
+      (\iff & F.\AMODULE.\MITYPES.\MITYPES[x] = \TARRAY~\X{ft})
      \end{array} \\
    \end{array}
 
@@ -558,7 +707,7 @@ Reference Instructions
         \\&&
         \begin{array}[t]{@{}r@{~}l@{}}
          (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\
-         \land & \X{ai} = \{\AITYPE~F.\AMODULE[x], \AIFIELDS~(\packval_{\X{ft}}(\default_{\unpacktype(\X{ft}}))^n\} \\
+         \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\default_{\unpacktype(\X{ft}}))^n\} \\
          \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai})
         \end{array} \\
       \end{array}
@@ -566,18 +715,44 @@ Reference Instructions
 
 .. _exec-array.new_fixed:
 
-:math:`\ARRAYNEWFIXED~\typeidx`
-...............................
+:math:`\ARRAYNEWFIXED~\typeidx~n`
+.................................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.new_fixed>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.new_fixed>`, :math:`\deftype` is a :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-struct.new_fixed>`, :math:`n` :ref:`values <syntax-val>` are on the top of the stack.
+
+6. Pop the :math:`n` values :math:`\val^\ast` from the stack.
+
+7. For every value :math:`\val_i` in :math:`\val^\ast`:
+
+   a. Let :math:`\fieldval_i` be the result of computing :math:`\packval_{\X{ft}}(\val_i))`.
+
+8. Let :math:`\fieldval^\ast` be the concatenation of all field values :math:`\fieldval_i`.
+
+9. Let :math:`\X{ai}` be the :ref:`array instance <syntax-arrayinst>` :math:`\{\AITYPE~\deftype, \AIFIELDS~\fieldval^\ast\}`.
+
+10. Let :math:`a` be the length of :math:`S.\SARRAYS`.
+
+11. Append :math:`\X{ai}` to :math:`S.\SARRAYS`.
+
+12. Return the :ref:`array reference <syntax-ref.array>` :math:`\REFARRAYADDR~a`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   S; F; \val^n~(\I32.\CONST~n)~(\ARRAYNEWFIXED~x) &\stepto& S'; F; (\REFARRAYADDR~|S.\SARRAYS|)
+   S; F; \val^n~(\ARRAYNEWFIXED~x~n) &\stepto& S'; F; (\REFARRAYADDR~|S.\SARRAYS|)
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft}^n \\
-      \land & \X{ai} = \{\AITYPE~F.\AMODULE[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\
+      (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\
+      \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\
       \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai})
      \end{array} \\
    \end{array}
@@ -588,8 +763,50 @@ Reference Instructions
 :math:`\ARRAYNEWDATA~\typeidx~\dataidx`
 .......................................
 
-.. todo:: Prose
 .. todo:: extend type size convention to field types
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.new_data>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.new_data>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-array.new_data>`, the :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[\dataidx]` exists.
+
+6. Let :math:`\X{da}` be the :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[\dataidx]`.
+
+7. Assert: due to :ref:`validation <valid-array.new_data>`, the :ref:`data instance <syntax-datainst>` :math:`S.\SDATAS[\X{da}]` exists.
+
+8. Let :math:`\datainst` be the :ref:`data instance <syntax-datainst>` :math:`S.\SDATAS[\X{da}]`.
+
+9. Assert: due to :ref:`validation <valid-array.new_data>`, two :ref:`values <syntax-val>` of type :math:`\I32` are on the top of the stack.
+
+10. Pop the value :math:`(\I32.\CONST~n)` from the stack.
+
+11. Pop the value :math:`(\I32.\CONST~s)` from the stack.
+
+12. Assert: due to :ref:`validation <valid-array.new_data>`, the :ref:`field type <syntax-fieldtype>` :math:`\X{ft}` has a defined :ref:`size <aux-size-fieldtype>`.
+
+13. Let :math:`z` be the :ref:`size <aux-size-fieldtype>` of :ref:`field type <syntax-fieldtype>` :math:`\X{ft}`.
+
+14. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then:
+
+    a. Trap.
+
+15. Let :math:`b^\ast` be the :ref:`byte <syntax-byte>` sequence :math:`\datainst.\DIDATA[s \slice n \cdot z]`.
+
+16. Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\X{ft})`.
+
+17. For each consecutive subsequence :math:`{b'}^n` of :math:`b^\ast`:
+
+    a. Let :math:`c_i` be the constant for which :math:`\bytes_{\X{ft}}(k_i)` is :math:`{b'}^n`.
+
+    b. Push the value :math:`(t.\CONST~c_i)` to the stack.
+
+18. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`.
 
 .. math::
    ~\\[-1ex]
@@ -601,12 +818,12 @@ Reference Instructions
       \land & s + n\cdot|\X{ft}| > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|)
      \end{array} \\
    \\[1ex]
-   S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& (t.\CONST~i)^n~(\ARRAYNEWFIXED~x)
+   S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& (t.\CONST~c)^n~(\ARRAYNEWFIXED~x~n)
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
       (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft}^n \\
       \land & t = \unpacktype(\X{ft}) \\
-      \land & (\bytes_{\X{ft}}(i))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|] \\
+      \land & (\bytes_{\X{ft}}(c))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|] \\
      \end{array} \\
    \end{array}
 
@@ -616,7 +833,39 @@ Reference Instructions
 :math:`\ARRAYNEWELEM~\typeidx~\elemidx`
 .......................................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.new_elem>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.new_elem>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-array.new_elem>`, the :ref:`element address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[\elemidx]` exists.
+
+6. Let :math:`\X{ea}` be the :ref:`element address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[\elemidx]`.
+
+7. Assert: due to :ref:`validation <valid-array.new_elem>`, the :ref:`element instance <syntax-eleminst>` :math:`S.\SELEMS[\X{ea}]` exists.
+
+8. Let :math:`\eleminst` be the :ref:`element instance <syntax-eleminst>` :math:`S.\SELEMS[\X{ea}]`.
+
+9. Assert: due to :ref:`validation <valid-array.new_elem>`, two :ref:`values <syntax-val>` of type :math:`\I32` are on the top of the stack.
+
+10. Pop the value :math:`(\I32.\CONST~n)` from the stack.
+
+11. Pop the value :math:`(\I32.\CONST~s)` from the stack.
+
+12. If the sum of :math:`s` and :math:`n` is larger than the length of :math:`\eleminst.\EIELEM`, then:
+
+    a. Trap.
+
+13. Let :math:`\reff^\ast` be the :ref:`reference <syntax-ref>` sequence :math:`\eleminst.\EIELEM[s \slice n]`.
+
+14. Push the references :math:`\reff^\ast` to the stack.
+
+15. Execute the instruction :math:`(\ARRAYNEWFIXED~\typeidx~n)`.
 
 .. math::
    ~\\[-1ex]
@@ -625,7 +874,7 @@ Reference Instructions
      \\&&
      (\iff s + n > |S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM|)
    \\[1ex]
-   S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWELEM~x~y) &\stepto& \reff^n~(\ARRAYNEWFIXED~x)
+   S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWELEM~x~y) &\stepto& \reff^n~(\ARRAYNEWFIXED~x~n)
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
       (\iff & \reff^n = S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM[s \slice n])
@@ -639,7 +888,43 @@ Reference Instructions
 :math:`\ARRAYGET\K{\_}\sx^?~\typeidx`
 .....................................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.get>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.get>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-array.get>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`\I32` is on the top of the stack.
+
+6. Pop the value :math:`(\I32.\CONST~i)` from the stack.
+
+7. Assert: due to :ref:`validation <valid-array.get>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~x)` is on the top of the stack.
+
+8. Pop the value :math:`\reff` from the stack.
+
+9. If :math:`\reff` is :math:`\REFNULL~t`, then:
+
+   a. Trap.
+
+10. Assert: due to validation, a :math:`\reff` is an :ref:`array reference <syntax-ref.array>`.
+
+11. Let :math:`(\REFARRAYADDR~a)` be the reference value :math:`\reff`.
+
+12. Assert: due to :ref:`validation <valid-array.get>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a]` exists.
+
+13. If :math:`n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then:
+
+    a. Trap.
+
+14. Let :math:`\fieldval` be the :ref:`field value <syntax-fieldval>` :math:`S.\SARRAYS[a].\AIFIELDS[i]`.
+
+15. Let :math:`\val` be the result of computing :math:`\unpackval^{\sx^?}_{\X{ft}}(\fieldval))`.
+
+16. Push the value :math:`\val` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -649,6 +934,8 @@ Reference Instructions
       (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\
       \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i]))
      \end{array} \\
+   S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \val
+     & (\otherwise) \\
    S; F; (\REFNULL~t)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP
    \end{array}
 
@@ -658,7 +945,45 @@ Reference Instructions
 :math:`\ARRAYSET~\typeidx`
 ..........................
 
-.. todo:: Prose
+.. todo:: unroll type
+
+1. Assert: due to :ref:`validation <valid-array.set>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]` exists.
+
+2. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[\typeidx]`.
+
+3. Assert: due to :ref:`validation <valid-array.set>`, :math:`\deftype` is an :ref:`array type <syntax-arraytype>`.
+
+4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type <syntax-arraytype>` :math:`\deftype`. (todo: unroll)
+
+5. Assert: due to :ref:`validation <valid-array.set>`, a :ref:`value <syntax-val>` is on the top of the stack.
+
+6. Pop the value :math:`\val` from the stack.
+
+7. Assert: due to :ref:`validation <valid-array.get>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`\I32` is on the top of the stack.
+
+8. Pop the value :math:`(\I32.\CONST~i)` from the stack.
+
+9. Assert: due to :ref:`validation <valid-array.set>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~x)` is on the top of the stack.
+
+10. Pop the value :math:`\reff` from the stack.
+
+11. If :math:`\reff` is :math:`\REFNULL~t`, then:
+
+   a. Trap.
+
+12. Assert: due to validation, a :math:`\reff` is an :ref:`array reference <syntax-ref.array>`.
+
+13. Let :math:`(\REFARRAYADDR~a)` be the reference value :math:`\reff`.
+
+14. Assert: due to :ref:`validation <valid-array.set>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a]` exists.
+
+15. If :math:`n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then:
+
+    a. Trap.
+
+16. Let :math:`\fieldval` be the result of computing :math:`\packval_{\X{ft}}(\val))`.
+
+17. Replace the :ref:`field value <syntax-fieldval>` :math:`S.\SARRAYS[a].\AIFIELDS[i]` with :math:`\fieldval`.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -677,7 +1002,23 @@ Reference Instructions
 :math:`\ARRAYLEN`
 .................
 
-.. todo:: Prose
+1. Assert: due to :ref:`validation <valid-array.len>`, a :ref:`value <syntax-val>` of :ref:`type <syntax-valtype>` :math:`(\REF~\NULL~\ARRAY)` is on the top of the stack.
+
+2. Pop the value :math:`\reff` from the stack.
+
+3. If :math:`\reff` is :math:`\REFNULL~t`, then:
+
+   a. Trap.
+
+4. Assert: due to validation, a :math:`\reff` is an :ref:`array reference <syntax-ref.array>`.
+
+5. Let :math:`(\REFARRAYADDR~a)` be the reference value :math:`\reff`.
+
+6. Assert: due to :ref:`validation <valid-array.len>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a]` exists.
+
+7. Let :math:`n` be the length of :math:`S.\SARRAYS[a].\AIFIELDS`.
+
+8. Push the :ref:`value <syntax-val>` :math:`(\I32.\CONST~n)` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -799,14 +1140,14 @@ Reference Instructions
      \quad\stepto
      \\ \quad S; F;
      \begin{array}[t]{@{}l@{}}
-     (\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST i)~(\ARRAYSET~x) \\
+     (\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST c)~(\ARRAYSET~x) \\
      (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+|\X{ft}|)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \\
      \end{array}
      \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\otherwise, \iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\
       \land & t = \unpacktype(\X{ft}) \\
-      \land & \bytes_{\X{ft}}(i) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice |\X{ft}|]
+      \land & \bytes_{\X{ft}}(c) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice |\X{ft}|]
      \end{array}
    \\[1ex]
    S; F; (\REFNULL~t)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \quad\stepto\quad \TRAP
diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst
index 2ec090eb2..c21f2c44d 100644
--- a/document/core/exec/values.rst
+++ b/document/core/exec/values.rst
@@ -40,6 +40,7 @@ The following auxiliary typing rules specify this typing relation relative to a
      S \vdashval t.\CONST~c : t
    }
 
+
 .. _valid-ref:
 
 :ref:`Null References <syntax-ref>` :math:`\REFNULL~t`
@@ -65,6 +66,8 @@ The following auxiliary typing rules specify this typing relation relative to a
    That ensures that it is compatible with any nullable type in that hierarchy.
 
 
+.. _valid-ref.i31:
+
 :ref:`Scalar References <syntax-ref>` :math:`\REFI31~i`
 .......................................................
 
@@ -77,6 +80,8 @@ The following auxiliary typing rules specify this typing relation relative to a
    }
 
 
+.. _valid-ref.struct:
+
 :ref:`Structure References <syntax-ref>` :math:`\REFSTRUCTADDR~a`
 .................................................................
 
@@ -96,6 +101,8 @@ The following auxiliary typing rules specify this typing relation relative to a
    }
 
 
+.. _valid-ref.array:
+
 :ref:`Array References <syntax-ref>` :math:`\REFARRAYADDR~a`
 ............................................................