diff --git a/core/.buildinfo b/core/.buildinfo index e34fcdb0f4..54a88cb15c 100644 --- a/core/.buildinfo +++ b/core/.buildinfo @@ -1,4 +1,4 @@ # Sphinx build info version 1 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. -config: 481b579e82989517d9aadaa2d99f0f6d +config: 4b9e1609c8862c0d941260ee6a065d63 tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/core/_download/WebAssembly.pdf b/core/_download/WebAssembly.pdf index c1ccb78e1e..01d3bc8180 100644 Binary files a/core/_download/WebAssembly.pdf and b/core/_download/WebAssembly.pdf differ diff --git a/core/_static/documentation_options.js b/core/_static/documentation_options.js index 0b734f425b..617dc5737d 100644 --- a/core/_static/documentation_options.js +++ b/core/_static/documentation_options.js @@ -1,6 +1,6 @@ var DOCUMENTATION_OPTIONS = { URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'), - VERSION: '3.0 (Draft 2024-05-30)', + VERSION: '3.0 (Draft 2024-06-01)', LANGUAGE: 'en', COLLAPSE_INDEX: false, BUILDER: 'html', diff --git a/core/appendix/algorithm.html b/core/appendix/algorithm.html index 3f9f182ace..29e2183307 100644 --- a/core/appendix/algorithm.html +++ b/core/appendix/algorithm.html @@ -6,7 +6,7 @@ - Validation Algorithm — WebAssembly 3.0 (Draft 2024-05-30) + Validation Algorithm — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/changes.html b/core/appendix/changes.html index 9f099cc422..a706a48f58 100644 --- a/core/appendix/changes.html +++ b/core/appendix/changes.html @@ -6,7 +6,7 @@ - Change History — WebAssembly 3.0 (Draft 2024-05-30) + Change History — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/custom.html b/core/appendix/custom.html index 354fb38681..7aad592a59 100644 --- a/core/appendix/custom.html +++ b/core/appendix/custom.html @@ -6,7 +6,7 @@ - Custom Sections — WebAssembly 3.0 (Draft 2024-05-30) + Custom Sections — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/embedding.html b/core/appendix/embedding.html index c1e71ca1dc..1fc6502b52 100644 --- a/core/appendix/embedding.html +++ b/core/appendix/embedding.html @@ -6,7 +6,7 @@ - Embedding — WebAssembly 3.0 (Draft 2024-05-30) + Embedding — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/implementation.html b/core/appendix/implementation.html index 41dad58399..f5cb308b59 100644 --- a/core/appendix/implementation.html +++ b/core/appendix/implementation.html @@ -6,7 +6,7 @@ - Implementation Limitations — WebAssembly 3.0 (Draft 2024-05-30) + Implementation Limitations — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/index-instructions.html b/core/appendix/index-instructions.html index d908dca69e..e5f7ee0179 100644 --- a/core/appendix/index-instructions.html +++ b/core/appendix/index-instructions.html @@ -6,7 +6,7 @@ - Index of Instructions — WebAssembly 3.0 (Draft 2024-05-30) + Index of Instructions — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/index-rules.html b/core/appendix/index-rules.html index ca02d1f99f..564edb9509 100644 --- a/core/appendix/index-rules.html +++ b/core/appendix/index-rules.html @@ -6,7 +6,7 @@ - Index of Semantic Rules — WebAssembly 3.0 (Draft 2024-05-30) + Index of Semantic Rules — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/index-types.html b/core/appendix/index-types.html index 601d96b453..066cfd166f 100644 --- a/core/appendix/index-types.html +++ b/core/appendix/index-types.html @@ -6,7 +6,7 @@ - Index of Types — WebAssembly 3.0 (Draft 2024-05-30) + Index of Types — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/index.html b/core/appendix/index.html index 7c644fdfa9..02912adc59 100644 --- a/core/appendix/index.html +++ b/core/appendix/index.html @@ -6,7 +6,7 @@ - Appendix — WebAssembly 3.0 (Draft 2024-05-30) + Appendix — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/appendix/properties.html b/core/appendix/properties.html index bdb2849882..2264bb7822 100644 --- a/core/appendix/properties.html +++ b/core/appendix/properties.html @@ -6,7 +6,7 @@ - Type Soundness — WebAssembly 3.0 (Draft 2024-05-30) + Type Soundness — WebAssembly 3.0 (Draft 2024-06-01) @@ -407,8 +407,8 @@

-
-

Host Function Instances \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf}\}\)

+
+

Host Function Instances \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\mathit{hf}\}\)

  • The function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) must be valid under an empty context.

  • Let \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) be the function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).

  • @@ -447,7 +447,7 @@

-
-

\(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)

+
+

\(\href{../exec/instructions.html#exec-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)

  • The external function value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) must be valid with external function type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}'\).

  • Let \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast])\) be the function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).

  • @@ -811,7 +811,7 @@

diff --git a/core/binary/conventions.html b/core/binary/conventions.html index 82d4f7878d..0bd37d39ed 100644 --- a/core/binary/conventions.html +++ b/core/binary/conventions.html @@ -6,7 +6,7 @@ - Conventions — WebAssembly 3.0 (Draft 2024-05-30) + Conventions — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/binary/index.html b/core/binary/index.html index e449c7b3c5..95fdc6ab14 100644 --- a/core/binary/index.html +++ b/core/binary/index.html @@ -6,7 +6,7 @@ - Binary Format — WebAssembly 3.0 (Draft 2024-05-30) + Binary Format — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/binary/instructions.html b/core/binary/instructions.html index 8c90145e5f..8f5b8bdd9f 100644 --- a/core/binary/instructions.html +++ b/core/binary/instructions.html @@ -6,7 +6,7 @@ - Instructions — WebAssembly 3.0 (Draft 2024-05-30) + Instructions — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/binary/modules.html b/core/binary/modules.html index 10248a796c..ccf54a2533 100644 --- a/core/binary/modules.html +++ b/core/binary/modules.html @@ -6,7 +6,7 @@ - Modules — WebAssembly 3.0 (Draft 2024-05-30) + Modules — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/binary/types.html b/core/binary/types.html index f5fe9dde38..c52be1132e 100644 --- a/core/binary/types.html +++ b/core/binary/types.html @@ -6,7 +6,7 @@ - Types — WebAssembly 3.0 (Draft 2024-05-30) + Types — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/binary/values.html b/core/binary/values.html index 303e3f0443..3a1864dbe2 100644 --- a/core/binary/values.html +++ b/core/binary/values.html @@ -6,7 +6,7 @@ - Values — WebAssembly 3.0 (Draft 2024-05-30) + Values — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/exec/conventions.html b/core/exec/conventions.html index 28d1a05a11..6c67c61f88 100644 --- a/core/exec/conventions.html +++ b/core/exec/conventions.html @@ -6,7 +6,7 @@ - Conventions — WebAssembly 3.0 (Draft 2024-05-30) + Conventions — WebAssembly 3.0 (Draft 2024-06-01) @@ -162,7 +162,8 @@

Quick search

\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow} \epsilon\]

Labels and frames are similarly defined to be part of an instruction sequence.

-

The order of reduction is determined by the definition of an appropriate evaluation context.

+

The order of reduction is determined by the details of the reduction rules. +Usually, the left-most instruction that is not a constant will be the subject of the next reduction step.

Reduction terminates when no more reduction rules are applicable. Soundness of the WebAssembly type system guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of \(\mathsf{const}\) instructions, which can be interpreted as the values of the resulting operand stack, or if a trap occurred.

diff --git a/core/exec/index.html b/core/exec/index.html index 4eb2ae2e49..1c4fb69010 100644 --- a/core/exec/index.html +++ b/core/exec/index.html @@ -6,7 +6,7 @@ - Execution — WebAssembly 3.0 (Draft 2024-05-30) + Execution — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/exec/instructions.html b/core/exec/instructions.html index 3bea8e81d1..89f0ef6a8e 100644 --- a/core/exec/instructions.html +++ b/core/exec/instructions.html @@ -6,7 +6,7 @@ - Instructions — WebAssembly 3.0 (Draft 2024-05-30) + Instructions — WebAssembly 3.0 (Draft 2024-06-01) @@ -613,18 +613,18 @@

Quick search

\({\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{i{\scriptstyle31}.get}}}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}\)

  1. Assert: Due to validation, a value is on the top of the stack.

  2. -
  3. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

  4. -
  5. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

    +
  6. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

  7. +
  8. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

    1. Trap.

  9. -
  10. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}\), then:

    +
  11. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}\), then:

      -
    1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~i)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

    2. +
    3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~i)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

    4. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{{{{\href{../exec/numerics.html#op-ext}{\mathrm{extend}}}}_{31, 32}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{(i)})\) to the stack.

    @@ -752,8 +752,8 @@

    Quick search

    1. Let \(z\) be the current state.

    2. Assert: Due to validation, a value is on the top of the stack.

    3. -
    4. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

    5. -
    6. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

      +
    7. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

    8. +
    9. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

      1. Trap.

      2. @@ -763,10 +763,10 @@

        Quick search

      3. Assert: Due to validation, \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}\).

      4. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\).

      5. Let \({({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}})^\ast}\) be \(y_0\).

      6. -
      7. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}\), then:

        +
      8. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}\), then:

          -
        1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

        2. +
        3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

        4. If \(i\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}{}[a]{.}\href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}|}\) and \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}|}\) and \({|{{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}^\ast}|}\) is \({|{{\mathit{zt}}^\ast}|}\) and \(i\) is less than \({|{{\mathit{zt}}^\ast}|}\), then:

            @@ -819,8 +819,8 @@

            Quick search

          1. Assert: Due to validation, a value is on the top of the stack.

          2. Pop the value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) from the stack.

          3. Assert: Due to validation, a value is on the top of the stack.

          4. -
          5. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

          6. -
          7. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

            +
          8. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

          9. +
          10. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

            1. Trap.

            2. @@ -830,9 +830,9 @@

              Quick search

            3. Assert: Due to validation, \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}\).

            4. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\).

            5. Let \({({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}})^\ast}\) be \(y_0\).

            6. -
            7. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}\), then:

              +
            8. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}\), then:

                -
              1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

              2. +
              3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

              4. If \({|{{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}^\ast}|}\) is \({|{{\mathit{zt}}^\ast}|}\) and \(i\) is less than \({|{{\mathit{zt}}^\ast}|}\), then:

                  @@ -983,14 +983,14 @@

                  Quick search

                  \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x],\; \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~{({{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\mathit{zt}}}({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}))^{n}} \}\end{array}} \\ \end{array}\end{split}\]
-
-

\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array.new\_data}}~x~y\)

+
+

\(\mathsf{array.new\_data}~x~y\)

  1. Let \(z\) be the current state.

  2. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

  3. -
  4. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)\) from the stack.

  5. +
  6. Pop the value \((\mathsf{const}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~n)\) from the stack.

  7. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

  8. -
  9. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) from the stack.

  10. +
  11. Pop the value \((\mathsf{const}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~i)\) from the stack.

  12. If \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}\), then:

      @@ -1007,8 +1007,8 @@

      Quick search

    1. Let \({b^\ast}\) be \(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}{}[y]{.}\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}{}[i : n \cdot {|{\mathit{zt}}|} / 8]\).

    2. Let \({{\mathit{gb}}^\ast}\) be \({\mathrm{group}}_{{\mathit{bytes}}_{\mathit{by}}}({|{\mathit{zt}}|} / 8, {b^\ast})\).

    3. Let \({c^{n}}\) be \({{\mathrm{inverse}}_{{\mathit{of}}_{\mathit{ibytes}}}({|{\mathit{zt}}|}, {\mathit{gb}})^\ast}\).

    4. -
    5. Push the values \({({\mathit{cnn}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)^{n}}\) to the stack.

    6. -
    7. Execute the instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array.new\_fixed}}~x~n)\).

    8. +
    9. Push the values \({(\mathsf{const}~{\mathit{cnn}}~c)^{n}}\) to the stack.

    10. +
    11. Execute the instruction \((\mathsf{array.new\_fixed}~x~n)\).

  13. @@ -1093,18 +1093,18 @@

    Quick search

  14. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

  15. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) from the stack.

  16. Assert: Due to validation, a value is on the top of the stack.

  17. -
  18. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

  19. -
  20. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

    +
  21. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

  22. +
  23. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

    1. Trap.

  24. -
  25. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

    +
  26. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

      -
    1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

    2. +
    3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

    4. If \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i\) is greater than or equal to \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

        @@ -1118,9 +1118,9 @@

        Quick search

      1. Assert: Due to validation, \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}\).

      2. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\).

      3. Let \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}})\) be \(y_0\).

      4. -
      5. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

        +
      6. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

          -
        1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

        2. +
        3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

        4. If \(i\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\) and \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\), then:

            @@ -1185,18 +1185,18 @@

            Quick search

          1. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

          2. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) from the stack.

          3. Assert: Due to validation, a value is on the top of the stack.

          4. -
          5. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

          6. -
          7. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

            +
          8. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

          9. +
          10. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

            1. Trap.

          11. -
          12. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

            +
          13. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

              -
            1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

            2. +
            3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

            4. If \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i\) is greater than or equal to \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

                @@ -1210,9 +1210,9 @@

                Quick search

              1. Assert: Due to validation, \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}\).

              2. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\).

              3. Let \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}})\) be \(y_0\).

              4. -
              5. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                +
              6. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                  -
                1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                2. +
                3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                4. Perform \(z{}[{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}{}[i] = {{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\mathit{zt}}}({\href{../exec/runtime.html#syntax-val}{\mathit{val}}})]\).

              7. @@ -1268,18 +1268,18 @@

                Quick search

                1. Let \(z\) be the current state.

                2. Assert: Due to validation, a value is on the top of the stack.

                3. -
                4. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                5. -
                6. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                  +
                7. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                8. +
                9. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                  1. Trap.

                10. -
                11. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                  +
                12. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                    -
                  1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                  2. +
                  3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                  4. If \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\), then:

                      @@ -1314,15 +1314,15 @@

                      Quick search

                    1. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

                    2. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) from the stack.

                    3. Assert: Due to validation, a value is on the top of the stack.

                    4. -
                    5. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                    6. -
                    7. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                      +
                    8. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                    9. +
                    10. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                      1. Trap.

                    11. -
                    12. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                      +
                    13. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                        -
                      1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                      2. +
                      3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                      4. If \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i + n\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

                          @@ -1340,7 +1340,7 @@

                          Quick search

                        1. Else:

                            -
                          1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                          2. +
                          3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                          4. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) to the stack.

                          5. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) to the stack.

                          6. Push the value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) to the stack.

                          7. @@ -1383,25 +1383,25 @@

                            Quick search

                          8. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

                          9. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i_2)\) from the stack.

                          10. Assert: Due to validation, a value is on the top of the stack.

                          11. -
                          12. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) from the stack.

                          13. +
                          14. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) from the stack.

                          15. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

                          16. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i_1)\) from the stack.

                          17. Assert: Due to validation, a value is on the top of the stack.

                          18. -
                          19. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                          20. -
                          21. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\) and the type of \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is ref, then:

                            +
                          22. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                          23. +
                          24. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\) and the type of \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is ref, then:

                            1. Trap.

                          25. -
                          26. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\) and the type of \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is ref, then:

                            +
                          27. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\) and the type of \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is ref, then:

                            1. Trap.

                          28. -
                          29. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                            +
                          30. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                              -
                            1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                            2. -
                            3. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                              +
                            4. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                            5. +
                            6. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                              1. If \(a_1\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i_1 + n\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a_1]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

                                @@ -1411,7 +1411,7 @@

                                Quick search

                            7. -
                            8. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_2)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\).

                            9. +
                            10. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_2)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\).

                            11. If \(a_2\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i_2 + n\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a_2]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

                                @@ -1425,7 +1425,7 @@

                                Quick search

                              1. If \(n\) is \(0\), then:

                                  -
                                1. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                  +
                                2. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                  1. Do nothing.

                                  2. @@ -1441,11 +1441,11 @@

                                    Quick search

                                  3. Assert: Due to validation, \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x_2])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}\).

                                  4. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x_2])\).

                                  5. Let \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}}_2)\) be \(y_0\).

                                  6. -
                                  7. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                  8. -
                                  9. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                    +
                                  10. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                  11. +
                                  12. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                      -
                                    1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_2)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\).

                                    2. +
                                    3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_2)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\).

                                    4. Let \({{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}\) be \({\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}({\mathit{zt}}_2)\).

                                    5. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) to the stack.

                                    6. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i_1 + n - 1)\) to the stack.

                                    7. @@ -1471,11 +1471,11 @@

                                      Quick search

                                    8. Assert: Due to validation, \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x_2])\) is of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}\).

                                    9. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x_2])\).

                                    10. Let \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}}_2)\) be \(y_0\).

                                    11. -
                                    12. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                    13. -
                                    14. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                      +
                                    15. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                    16. +
                                    17. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                        -
                                      1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_2)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\).

                                      2. +
                                      3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_2)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\).

                                      4. Let \({{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}\) be \({\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}({\mathit{zt}}_2)\).

                                      5. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_1)\) to the stack.

                                      6. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i_1)\) to the stack.

                                      7. @@ -1629,15 +1629,15 @@

                                        Quick search

                                      8. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

                                      9. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) from the stack.

                                      10. Assert: Due to validation, a value is on the top of the stack.

                                      11. -
                                      12. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                      13. -
                                      14. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                        +
                                      15. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                      16. +
                                      17. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                        1. Trap.

                                      18. -
                                      19. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                        +
                                      20. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                          -
                                        1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                        2. +
                                        3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                        4. If \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i + n\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

                                            @@ -1649,7 +1649,7 @@

                                            Quick search

                                          1. If \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\) is not of the case \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}\), then:

                                              -
                                            1. If \(n\) is \(0\) and \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                              +
                                            2. If \(n\) is \(0\) and \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                              1. Do nothing.

                                              2. @@ -1662,7 +1662,7 @@

                                                Quick search

                                                1. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\).

                                                2. Let \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}})\) be \(y_0\).

                                                3. -
                                                4. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                  +
                                                5. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                  1. If \(j + n \cdot {|{\mathit{zt}}|} / 8\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}{}[y]{.}\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}|}\), then:

                                                    @@ -1684,7 +1684,7 @@

                                                    Quick search

                                                    1. Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~y_0)\) be \({\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}}(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x])\).

                                                    2. Let \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?},\, {\mathit{zt}})\) be \(y_0\).

                                                    3. -
                                                    4. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                    5. +
                                                    6. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                    7. Let \(c\) be \({\mathrm{inverse}}_{{\mathit{of}}_{\mathit{zbytes}}}({\mathit{zt}}, z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}{}[y]{.}\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}{}[j : {|{\mathit{zt}}|} / 8])\).

                                                    8. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) to the stack.

                                                    9. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) to the stack.

                                                    10. @@ -1789,15 +1789,15 @@

                                                      Quick search

                                                    11. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

                                                    12. Pop the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) from the stack.

                                                    13. Assert: Due to validation, a value is on the top of the stack.

                                                    14. -
                                                    15. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                                    16. -
                                                    17. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                                      +
                                                    18. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                                    19. +
                                                    20. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                                      1. Trap.

                                                    21. -
                                                    22. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                      +
                                                    23. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                        -
                                                      1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                      2. +
                                                      3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                      4. If \(a\) is less than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}|}\) and \(i + n\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}|}\), then:

                                                          @@ -1809,7 +1809,7 @@

                                                          Quick search

                                                        1. If \(j + n\) is greater than \({|z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}{}[y]{.}\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}|}\), then:

                                                            -
                                                          1. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                            +
                                                          2. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                            1. Trap.

                                                            2. @@ -1820,10 +1820,10 @@

                                                              Quick search

                                                              1. Let \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) be \(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}{}[y]{.}\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}{}[j]\).

                                                              2. -
                                                              3. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                                +
                                                              4. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                                  -
                                                                1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                2. +
                                                                3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                4. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) to the stack.

                                                                5. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) to the stack.

                                                                6. Push the value \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) to the stack.

                                                                7. @@ -1843,7 +1843,7 @@

                                                                  Quick search

                                                                8. Else if \(n\) is \(0\), then:

                                                                    -
                                                                  1. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                                    +
                                                                  2. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                                    1. Do nothing.

                                                                    2. @@ -1858,10 +1858,10 @@

                                                                      Quick search

                                                                      1. Let \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) be \(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}{}[y]{.}\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}{}[j]\).

                                                                      2. -
                                                                      3. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                                        +
                                                                      4. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\), then:

                                                                          -
                                                                        1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                        2. +
                                                                        3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                        4. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) to the stack.

                                                                        5. Push the value \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)\) to the stack.

                                                                        6. Push the value \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) to the stack.

                                                                        7. @@ -1904,18 +1904,18 @@

                                                                          Quick search

                                                                          \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any.convert\_extern}}\)

                                                                          1. Assert: Due to validation, a value is on the top of the stack.

                                                                          2. -
                                                                          3. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                                                          4. -
                                                                          5. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                                                            +
                                                                          6. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                                                          7. +
                                                                          8. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                                                            1. Push the value \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}})\) to the stack.

                                                                          9. -
                                                                          10. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}\), then:

                                                                            +
                                                                          11. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}\), then:

                                                                              -
                                                                            1. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}})\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                            2. +
                                                                            3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}})\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                            4. Push the value \({\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}}\) to the stack.

                                                                            @@ -1937,18 +1937,18 @@

                                                                            Quick search

                                                                            \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern.convert\_any}}\)

                                                                            1. Assert: Due to validation, a value is on the top of the stack.

                                                                            2. -
                                                                            3. Pop the value \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                                                            4. -
                                                                            5. If \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                                                              +
                                                                            6. Pop the value \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) from the stack.

                                                                            7. +
                                                                            8. If \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is of the case \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\), then:

                                                                              1. Push the value \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}})\) to the stack.

                                                                            9. -
                                                                            10. If the type of \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is addrref, then:

                                                                              +
                                                                            11. If the type of \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is addrref, then:

                                                                                -
                                                                              1. Let \({\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}}\) be \({\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                              2. +
                                                                              3. Let \({\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}}\) be \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\).

                                                                              4. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}})\) to the stack.

                                                                              @@ -3855,7 +3855,7 @@

                                                                              \(t_2\mathsf{x}N\mathsf{.}\href{.

                                                                              \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\)

                                                                              1. Let \(z\) be the current state.

                                                                              2. -
                                                                              3. Let \({t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}}\) be \({{\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}}}_{z}({\mathit{bt}})\).

                                                                              4. +
                                                                              5. Let \({t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}}\) be \({{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}({\mathit{bt}})\).

                                                                              6. Assert: Due to validation, there are at least \(m\) values on the top of the stack.

                                                                              7. Pop the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{m}}\) from the stack.

                                                                              8. Let \(L\) be the label whose arity is \(n\) and whose continuation is \(\epsilon\).

                                                                              9. @@ -3864,14 +3864,14 @@

                                                                                \(t_2\mathsf{x}N\mathsf{.}\href{.
                                                                                \[\begin{split}\begin{array}{@{}l@{}rcl@{}l@{}} & z ; {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{m}}~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& ({{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ \epsilon \}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{m}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}) - &\qquad \mbox{if}~{{\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}}}_{z}({\mathit{bt}}) = {t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}} \\ + &\qquad \mbox{if}~{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}({\mathit{bt}}) = {t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}} \\ \end{array}\end{split}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\)

  1. Let \(z\) be the current state.

  2. -
  3. Let \({t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}}\) be \({{\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}}}_{z}({\mathit{bt}})\).

  4. +
  5. Let \({t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}}\) be \({{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}({\mathit{bt}})\).

  6. Assert: Due to validation, there are at least \(m\) values on the top of the stack.

  7. Pop the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{m}}\) from the stack.

  8. Let \(L\) be the label whose arity is \(m\) and whose continuation is \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\).

  9. @@ -3880,7 +3880,7 @@

    \(t_2\mathsf{x}N\mathsf{.}\href{.
    \[\begin{split}\begin{array}{@{}l@{}rcl@{}l@{}} & z ; {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{m}}~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& ({{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{m}}{\{ \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{m}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}) - &\qquad \mbox{if}~{{\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}}}_{z}({\mathit{bt}}) = {t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}} \\ + &\qquad \mbox{if}~{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}({\mathit{bt}}) = {t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}} \\ \end{array}\end{split}\]

@@ -3919,11 +3919,11 @@

\(t_2\mathsf{x}N\mathsf{.}\href{.
  • Let \(n\) be the arity of \(L\).

  • Let \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) be the continuation of \(L\).

  • Pop the current label from the stack.

  • -
  • Let \({{\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}\) be \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\).

  • -
  • If \(l\) is \(0\) and \({|{{\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}|}\) is greater than or equal to \(n\), then:

    +
  • Let \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}\) be \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\).

  • +
  • If \(l\) is \(0\) and \({|{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}|}\) is greater than or equal to \(n\), then:

      -
    1. Let \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{n}}\) be \({{\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}\).

    2. +
    3. Let \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{n}}\) be \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}\).

    4. Push the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^{n}}\) to the stack.

    5. Execute the sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\).

    @@ -3932,7 +3932,7 @@

    \(t_2\mathsf{x}N\mathsf{.}\href{.
  • If \(l\) is greater than \(0\), then:

      -
    1. Let \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\) be \({{\mathit{admin}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}\).

    2. +
    3. Let \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\) be \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}^\ast}\).

    4. Push the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\) to the stack.

    5. Execute the instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l - 1)\).

    @@ -4499,20 +4499,20 @@

    \(t_2\mathsf{x}N\mathsf{.}\href{. \[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} -S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; \href{../exec/runtime.html#syntax-result}{\mathit{result}} +S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/instructions.html#exec-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; \href{../exec/runtime.html#syntax-result}{\mathit{result}} \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf} \} \\ + (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\mathit{hf} \} \\ \wedge & \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ \wedge & (S'; \href{../exec/runtime.html#syntax-result}{\mathit{result}}) \in \mathit{hf}(S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n)) \\ \end{array} \\ \begin{array}{lcl@{\qquad}l} -S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) +S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/instructions.html#exec-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/instructions.html#exec-invoke}{\mathsf{invoke}}~a) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf} \} \\ + (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\mathit{hf} \} \\ \wedge & \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ \wedge & \bot \in \mathit{hf}(S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n)) \\ \end{array} \\ diff --git a/core/exec/modules.html b/core/exec/modules.html index bea0e634a3..7b8f3238a0 100644 --- a/core/exec/modules.html +++ b/core/exec/modules.html @@ -6,7 +6,7 @@ - Modules — WebAssembly 3.0 (Draft 2024-05-30) + Modules — WebAssembly 3.0 (Draft 2024-06-01) @@ -121,7 +121,7 @@

    Modules
  • Let \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\) be the host function to allocate and \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) its defined type.

  • Let \(a\) be the first free function address in \(S\).

  • -
  • Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(\{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \}\).

  • +
  • Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(\{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \}\).

  • Append \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) of \(S\).

  • Return \(a\).

  • @@ -131,7 +131,7 @@

    Modules @@ -642,7 +642,7 @@

    Modules \[\begin{split}~\\[-1ex] \begin{array}{@{}lcl} -\href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n) &=& S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \\ +\href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n) &=& S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/instructions.html#exec-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \\ &(\mathrel{\mbox{if}} & \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ &\wedge& (S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t_1)^n \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}) \\ diff --git a/core/exec/numerics.html b/core/exec/numerics.html index 01a083d493..ddb4cc7b8a 100644 --- a/core/exec/numerics.html +++ b/core/exec/numerics.html @@ -6,7 +6,7 @@ - Numerics — WebAssembly 3.0 (Draft 2024-05-30) + Numerics — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/exec/runtime.html b/core/exec/runtime.html index e7e91b9287..9bd8a356dc 100644 --- a/core/exec/runtime.html +++ b/core/exec/runtime.html @@ -6,7 +6,7 @@ - Runtime Structure — WebAssembly 3.0 (Draft 2024-05-30) + Runtime Structure — WebAssembly 3.0 (Draft 2024-06-01) @@ -91,11 +91,11 @@

    Quick search

    Runtime Structure

    Store, stack, and other runtime structure forming the WebAssembly abstract machine, such as values or module instances, are made precise in terms of additional auxiliary syntax.

    -

    Values

    +

    Values

    WebAssembly computations manipulate values of either the four basic number types, i.e., integers and floating-point data of 32 or 64 bit width each, or vectors of 128 bit width, or of reference type.

    In most places of the semantics, values of different types can occur. In order to avoid ambiguities, values are therefore represented with an abstract syntax that makes their type explicit. -It is convenient to reuse the same notation as for the \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) instructions and \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\) producing them.

    +It is convenient to reuse the same notation as for the \(\mathsf{const}\) instructions and \(\mathsf{ref.null}\) producing them.

    References other than null are represented with additional administrative instructions. They either are scalar references, containing a 31-bit integer, structure references, pointing to a specific structure address, @@ -104,38 +104,33 @@

    Quick search

    or host references pointing to an uninterpreted form of host address defined by the embedder. Any of the aformentioned references can furthermore be wrapped up as an external reference.

    -\[\begin{split}\begin{array}{llcl} -\def\mathdef2446#1{{}}\mathdef2446{number} & \href{../exec/runtime.html#syntax-num}{\mathit{num}} &::=& - \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i\scriptstyle\kern-0.1em32}} \\&&|& - \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i\scriptstyle\kern-0.1em64}} \\&&|& - \href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-float}{\mathit{f\scriptstyle\kern-0.15em32}} \\&&|& - \href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-float}{\mathit{f\scriptstyle\kern-0.15em64}} \\ -\def\mathdef2446#1{{}}\mathdef2446{vector} & \href{../exec/runtime.html#syntax-vec}{\mathit{vec}} &::=& - \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i\scriptstyle\kern-0.1em128}} \\ -\def\mathdef2446#1{{}}\mathdef2446{reference} & \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} &::=& - \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~(\href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}}~|~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~\href{../syntax/values.html#syntax-int}{\mathit{u\scriptstyle\kern-0.1em31}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~\href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~\href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}~\href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}} \\ -\def\mathdef2446#1{{}}\mathdef2446{value} & \href{../exec/runtime.html#syntax-val}{\mathit{val}} &::=& - \href{../exec/runtime.html#syntax-num}{\mathit{num}} ~|~ \href{../exec/runtime.html#syntax-vec}{\mathit{vec}} ~|~ \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} &::=& {\href{../exec/runtime.html#syntax-num}{\mathit{num}}} ~|~ {\href{../exec/runtime.html#syntax-vec}{\mathit{vec}}} ~|~ {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} \\[0.8ex] +& {\href{../exec/runtime.html#syntax-num}{\mathit{num}}} &::=& {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{{\href{../exec/runtime.html#syntax-num}{\mathit{num}}}}_{{\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}} \\[0.8ex] +& {\href{../exec/runtime.html#syntax-vec}{\mathit{vec}}} &::=& {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~{{\href{../exec/runtime.html#syntax-vec}{\mathit{vec}}}}_{{\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}} \\[0.8ex] +& {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} &::=& {\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} \\ &&|& +\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} \\[0.8ex] +& {\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} &::=& \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~{\href{../syntax/values.html#syntax-int}{\mathit{u\scriptstyle\kern-0.1em31}}} \\ &&|& +\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~{\href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}}} \\ &&|& +\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~{\href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}}} \\ &&|& +\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}} \\ &&|& +\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}~{\href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}}} \\ &&|& +\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} \\ \end{array}\end{split}\]

    Note

    -

    Future versions of WebAssembly may add additional forms of reference.

    +

    Future versions of WebAssembly may add additional forms of values.

    Value types can have an associated default value; it is the respective value \(0\) for number types, \(0\) for vector types, and null for nullable reference types. -For other references, no default value is defined, \(\href{../exec/runtime.html#default-val}{\mathrm{default}}_t\) hence is an optional value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^?\).

    -
    -\[\begin{split}\begin{array}{lcl@{\qquad}l} -\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& t{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0 & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}) \\ -\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& t{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0 & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}) \\ -\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~t & (\mathrel{\mbox{if}} t = (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}})) \\ -\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& \epsilon & (\mathrel{\mbox{if}} t = (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}})) \\ +For other references, no default value is defined, \({{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{t}\) hence is an optional value \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^?}\).

    +
    +\[\begin{split}\begin{array}{@{}lcl@{}l@{}} +{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{{\mathsf{i}}{N}} &=& ({\mathsf{i}}{N}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0) \\ +{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{{\mathsf{f}}{N}} &=& ({\mathsf{f}}{N}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+0}) \\ +{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{{\mathsf{v}}{N}} &=& ({\mathsf{v}}{N}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~0) \\ +{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}} &=& (\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~{\mathit{ht}}) \\ +{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}} &=& \epsilon \\ \end{array}\end{split}\]

    Convention

    @@ -149,10 +144,8 @@

    Conventionvalues or a trap.

    -\[\begin{split}\begin{array}{llcl} -\def\mathdef2446#1{{}}\mathdef2446{result} & \href{../exec/runtime.html#syntax-result}{\mathit{result}} &::=& - \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast \\&&|& - \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-result}{\mathit{result}}} &::=& {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast} ~|~ \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \end{array}\end{split}\]

    @@ -162,18 +155,16 @@

    Conventionaddressed from anywhere else but the owning module instances.

    Syntactically, the store is defined as a record listing the existing instances of each category:

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{store} & \href{../exec/runtime.html#syntax-store}{\mathit{store}} &::=& \{~ - \begin{array}[t]{l@{~}ll} - \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} & \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{tables}} & \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{mems}} & \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{globals}} & \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{elems}} & \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{datas}} & \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{structs}} & \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}^\ast, \\ - \href{../exec/runtime.html#syntax-store}{\mathsf{arrays}} & \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}^\ast ~\} - \end{array} +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-store}{\mathit{store}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~{{\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~{{\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~{{\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~{{\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~{{\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~{{\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{structs}}~{{\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}~{{\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}}^\ast} \}\end{array} \\ \end{array}\end{split}\]

    @@ -196,27 +187,17 @@

    Conventionembedder may supply an uninterpreted set of host addresses.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{address} & \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} &::=& - 0 ~|~ 1 ~|~ 2 ~|~ \dots \\ -\def\mathdef2446#1{{}}\mathdef2446{function address} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{table address} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{memory address} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{global address} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{element address} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{data address} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{structure address} & \href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{array address} & \href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ -\def\mathdef2446#1{{}}\mathdef2446{host address} & \href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}} &::=& - \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} &::=& \mathbb{N} \\ +& {\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ +& {\href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}}} &::=& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\ \end{array}\end{split}\]

    An embedder may assign identity to exported store objects corresponding to their addresses, even where this identity is not observable from within WebAssembly code itself @@ -234,7 +215,7 @@

    Convention

    Conventions

      -
    • The notation \(\mathrm{addr}(A)\) denotes the set of addresses from address space \(\mathit{addr}\) occurring free in \(A\). We sometimes reinterpret this set as the list of its elements.

    • +
    • The notation \({\mathrm{addr}}(A)\) denotes the set of addresses from address space \({\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}}\) occurring free in \(A\). We sometimes reinterpret this set as the list of its elements.

  • @@ -244,18 +225,16 @@

    Conventioninstantiating a module, and collects runtime representations of all entities that are imported, defined, or exported by the module.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{module instance} & \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} &::=& \{ - \begin{array}[t]{l@{~}ll} - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} & \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast, \\ - \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} \\ - \end{array} +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~{{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~{{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~{{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~{{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~{{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}~{{\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}~{{\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}}^\ast},\; \\ + \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~{{\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}}^\ast} \}\end{array} \\ \end{array}\end{split}\]

    Each component references runtime instances corresponding to respective declarations from the original module – whether imported or defined – in the order of their static indices. Function instances, table instances, memory instances, and global instances are referenced with an indirection through their respective addresses in the store.

    @@ -267,11 +246,10 @@

    Conventionmodule instance of its originating module. The module instance is used to resolve references to other definitions during execution of the function.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{function instance} & \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} &::=& - \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}} \} \\ &&|& - \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \} \\ -\def\mathdef2446#1{{}}\mathdef2446{host function} & \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} &::=& \dots \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}},\; \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}},\; \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~{{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}} \}\end{array} \\ +& {{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}} &::=& {\href{../syntax/modules.html#syntax-func}{\mathit{func}}} ~|~ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\dots \\ \end{array}\end{split}\]

    A host function is a function expressed outside WebAssembly but passed to a module as an import. The definition and behavior of host functions are outside the scope of this specification. @@ -289,47 +267,47 @@

    Conventiontable. It records its type and holds a list of reference values.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{table instance} & \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} &::=& - \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../syntax/conventions.html#syntax-list}{\mathit{list}}(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}},\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast} \}\end{array} \\ \end{array}\end{split}\]

    Table elements can be mutated through table instructions, the execution of an active element segment, or by external means provided by the embedder.

    -

    It is an invariant of the semantics that all table elements have a type matching the element type of \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\). -It also is an invariant that the length of the element list never exceeds the maximum size of \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\), if present.

    +

    It is an invariant of the semantics that all table elements have a type matching the element type of \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\). +It also is an invariant that the length of the element list never exceeds the maximum size of \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\), if present.

    Memory Instances

    A memory instance is the runtime representation of a linear memory. It records its type and holds a list of bytes.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{memory instance} & \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} &::=& - \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~\href{../syntax/conventions.html#syntax-list}{\mathit{list}}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}) \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}},\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast} \}\end{array} \\ \end{array}\end{split}\]
    -

    The length of the list always is a multiple of the WebAssembly page size, which is defined to be the constant \(65536\) – abbreviated \(64\,\mathrm{Ki}\).

    +

    The length of the list always is a multiple of the WebAssembly page size, which is defined to be the constant \(65536\) – abbreviated \({64^\ast}~{\mathrm{Ki}}\).

    The bytes can be mutated through memory instructions, the execution of an active data segment, or by external means provided by the embedder.

    -

    It is an invariant of the semantics that the length of the byte list, divided by page size, never exceeds the maximum size of \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\), if present.

    +

    It is an invariant of the semantics that the length of the byte list, divided by page size, never exceeds the maximum size of \({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}\).

    Global Instances

    A global instance is the runtime representation of a global variable. It records its type and holds an individual value.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{global instance} & \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} &::=& - \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}},\; \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~{\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \}\end{array} \\ \end{array}\end{split}\]

    The value of mutable globals can be mutated through variable instructions or by external means provided by the embedder.

    -

    It is an invariant of the semantics that the value has a type matching the value type of \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\).

    +

    It is an invariant of the semantics that the value has a type matching the value type of \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\).

    Element Instances

    An element instance is the runtime representation of an element segment. It holds a list of references and their common type.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{element instance} & \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} &::=& - \{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../syntax/conventions.html#syntax-list}{\mathit{list}}(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}},\; \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast} \}\end{array} \\ \end{array}\end{split}\]
    @@ -337,9 +315,9 @@

    Conventiondata segment. It holds a list of bytes.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{data instance} & \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} &::=& - \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\href{../syntax/conventions.html#syntax-list}{\mathit{list}}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}) \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast} \}\end{array} \\ \end{array}\end{split}\]

    @@ -347,9 +325,9 @@

    Conventionexport. It defines the export’s name and the associated external value.

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{export instance} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} &::=& - \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~{\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}} \}\end{array} \\ \end{array}\end{split}\]

    @@ -357,23 +335,32 @@

    Conventionaddress denoting either a function instance, table instance, memory instance, or global instances in the shared store.

    -\[\begin{split}\begin{array}{llcl} -\def\mathdef2446#1{{}}\mathdef2446{external value} & \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} &::=& - \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|& - \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} \\&&|& - \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} \\&&|& - \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}} &::=& \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}} ~|~ \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}} ~|~ \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}} ~|~ \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}} \\ \end{array}\end{split}\]

    Conventions

    The following auxiliary notation is defined for sequences of external values. It filters out entries of a specific kind in an order-preserving fashion:

    -
      -
    • \(\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)

    • -
    • \(\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)

    • -
    • \(\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)

    • -
    • \(\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)

    • -
    +
    +\[\begin{split}\begin{array}{@{}lcl@{}l@{}} +{\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}}(\epsilon) &=& \epsilon \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}}((\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~{\mathit{fa}})~{{\mathit{xv}}^\ast}) &=& {\mathit{fa}}~{\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}}({{\mathit{xv}}^\ast}) \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}}({\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}}~{{\mathit{xv}}^\ast}) &=& {\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}}({{\mathit{xv}}^\ast}) + &\qquad \mbox{otherwise} \\[0.8ex] +{\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}}(\epsilon) &=& \epsilon \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}}((\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~{\mathit{ta}})~{{\mathit{xv}}^\ast}) &=& {\mathit{ta}}~{\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}}({{\mathit{xv}}^\ast}) \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}}({\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}}~{{\mathit{xv}}^\ast}) &=& {\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}}({{\mathit{xv}}^\ast}) + &\qquad \mbox{otherwise} \\[0.8ex] +{\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}}(\epsilon) &=& \epsilon \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}}((\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~{\mathit{ma}})~{{\mathit{xv}}^\ast}) &=& {\mathit{ma}}~{\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}}({{\mathit{xv}}^\ast}) \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}}({\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}}~{{\mathit{xv}}^\ast}) &=& {\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}}({{\mathit{xv}}^\ast}) + &\qquad \mbox{otherwise} \\[0.8ex] +{\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}}(\epsilon) &=& \epsilon \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}}((\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~{\mathit{ga}})~{{\mathit{xv}}^\ast}) &=& {\mathit{ga}}~{\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}}({{\mathit{xv}}^\ast}) \\ +{\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}}({\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}}~{{\mathit{xv}}^\ast}) &=& {\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}}({{\mathit{xv}}^\ast}) + &\qquad \mbox{otherwise} \\ +\end{array}\end{split}\]

    @@ -382,44 +369,42 @@

    Conventionsarray type. Both record their respective defined type and hold a list of the values of their fields.

    -\[\begin{split}\begin{array}{llcl} -\def\mathdef2446#1{{}}\mathdef2446{structure instance} & \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}} &::=& - \{ \href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~\href{../syntax/conventions.html#syntax-list}{\mathit{list}}(\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}) \} \\ -\def\mathdef2446#1{{}}\mathdef2446{array instance} & \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}} &::=& - \{ \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~\href{../syntax/conventions.html#syntax-list}{\mathit{list}}(\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}) \} \\ -\def\mathdef2446#1{{}}\mathdef2446{field value} & \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}} &::=& - \href{../exec/runtime.html#syntax-val}{\mathit{val}} ~|~ \href{../exec/runtime.html#syntax-packval}{\mathit{packval}} \\ -\def\mathdef2446#1{{}}\mathdef2446{packed value} & \href{../exec/runtime.html#syntax-packval}{\mathit{packval}} &::=& - \href{../exec/runtime.html#syntax-packval}{\mathsf{i8.pack}}~\href{../syntax/values.html#syntax-int}{\mathit{u\scriptstyle\kern-0.1em8}} ~|~ \href{../exec/runtime.html#syntax-packval}{\mathsf{i16.pack}}~\href{../syntax/values.html#syntax-int}{\mathit{u\scriptstyle\kern-0.1em16}} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}},\; \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~{{\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}}^\ast} \}\end{array} \\ +& {\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}},\; \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~{{\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}}^\ast} \}\end{array} \\ +& {\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}} &::=& {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} ~|~ {\href{../exec/runtime.html#syntax-packval}{\mathit{packval}}} \\ +& {\href{../exec/runtime.html#syntax-packval}{\mathit{packval}}} &::=& {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~{{\href{../syntax/values.html#syntax-int}{\mathit{i}\kern-0.1em}}}{N} \\ \end{array}\end{split}\]

    Conventions

    • Conversion of a regular value to a field value is defined as follows:

      -\[\begin{split}\begin{array}{@{}lcl} -\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}(\href{../exec/runtime.html#syntax-val}{\mathit{val}}) &=& \href{../exec/runtime.html#syntax-val}{\mathit{val}} \\ -\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}_{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) &=& \href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}.\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~(\href{../exec/numerics.html#op-wrap}{\mathrm{wrap}}_{32,|\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}|}(i)) +\[\begin{split}\begin{array}{@{}lcl@{}l@{}} +{{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}}({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}) &=& {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\ +{{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}}(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) &=& {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~{{{\href{../exec/numerics.html#op-wrap}{\mathrm{wrap}}}}_{32, {|{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}|}}}{(i)} \\ \end{array}\end{split}\]
    • The inverse conversion of a field value to a regular value is defined as follows:

      -\[\begin{split}\begin{array}{@{}lcl} -\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}(\href{../exec/runtime.html#syntax-val}{\mathit{val}}) &=& \href{../exec/runtime.html#syntax-val}{\mathit{val}} \\ -\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}.\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~i) &=& \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(\href{../exec/numerics.html#op-ext}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}|,32}(i)) +\[\begin{split}\begin{array}{@{}lcl@{}l@{}} +{{{{\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}}}_{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}}^{\epsilon}}}{({\href{../exec/runtime.html#syntax-val}{\mathit{val}}})} &=& {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\ +{{{{\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}}}_{{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~i)} &=& \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{{{{\href{../exec/numerics.html#op-ext}{\mathrm{extend}}}}_{{|{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}|}, 32}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{(i)} \\ \end{array}\end{split}\]

    -

    Stack

    +

    Stack

    Besides the store, most instructions interact with an implicit stack. The stack contains three kinds of entries:

    These entries can occur on the stack in any order during the execution of a program. Stack entries are described by abstract syntax as follows.

    @@ -437,134 +422,97 @@

    Values

    Labels

    Labels carry an argument arity \(n\) and their associated branch target, which is expressed syntactically as an instruction sequence:

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{label} & \href{../exec/runtime.html#syntax-label}{\mathit{label}} &::=& - \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-label}{\mathit{label}}} &::=& {{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}} \\ \end{array}\end{split}\]
    -

    Intuitively, \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is the continuation to execute when the branch is taken, in place of the original control construct.

    +

    Intuitively, \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is the continuation to execute when the branch is taken, in place of the original control construct.

    Note

    For example, a loop label has the form

    -\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\dots~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\]
    +\[{{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~\dots) \}}\]

    When performing a branch to this label, this executes the loop, effectively restarting it from the beginning. Conversely, a simple block label has the form

    -\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}\]
    +\[{{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ \epsilon \}}\]

    When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.

    -
    -

    Activation Frames

    -

    Activation frames carry the return arity \(n\) of the respective function, +

    +

    Call Frames

    +

    Call frames carry the return arity \(n\) of the respective function, hold the values of its locals (including arguments) in the order corresponding to their static local indices, and a reference to the function’s own module instance:

    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{frame} & \href{../exec/runtime.html#syntax-frame}{\mathit{frame}} &::=& - \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{ \href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}} \} \\ -\def\mathdef2446#1{{}}\mathdef2446{frame state} & \href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}} &::=& - \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^?)^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} \} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-callframe}{\mathit{callframe}}} &::=& {{\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}}_{n}}{\{ {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} \}} \\ +& {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} &::=& \{ \begin{array}[t]{@{}l@{}l@{}} +\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~{({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^?})^\ast},\; \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} \}\end{array} \\ \end{array}\end{split}\]

    Locals may be uninitialized, in which case they are empty. Locals are mutated by respective variable instructions.

    -
    -

    Conventions

    -
      +
      +

      Conventions

      +
      • The meta variable \(L\) ranges over labels where clear from context.

      • -
      • The meta variable \(F\) ranges over frame states where clear from context.

      • -
      • The following auxiliary definition takes a block type and looks up the instruction type that it denotes in the current frame:

      • -
      -
      -\[\begin{split}\begin{array}{llll} -\href{../exec/runtime.html#aux-fblocktype}{\mathrm{instrtype}}_{S;F}(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}) &=& \href{../syntax/types.html#syntax-functype}{\mathit{functype}} & (\mathrel{\mbox{if}} \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}) \\ -\href{../exec/runtime.html#aux-fblocktype}{\mathrm{instrtype}}_{S;F}([\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]) &=& [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] \\ +
    • The meta variable \(f\) ranges over frame states where clear from context.

    • +
    • The following auxiliary definition takes a block type and looks up the instruction type that it denotes in the current frame:

      +
      +\[\begin{split}\begin{array}{@{}lcl@{}l@{}} +{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}(x) &=& {\mathit{ft}} + &\qquad \mbox{if}~z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x] \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\mathit{ft}} \\ +{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}(t) &=& \epsilon \href{../syntax/types.html#syntax-functype}{\rightarrow} t \\ +{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}(\epsilon) &=& \epsilon \href{../syntax/types.html#syntax-functype}{\rightarrow} \epsilon \\ \end{array}\end{split}\]
      +
    • +
    -

    Administrative Instructions

    +

    Administrative Instructions

    Note

    This section is only relevant for the formal notation.

    In order to express the reduction of traps, calls, and control instructions, the syntax of instructions is extended to include the following administrative instructions:

    -\[\begin{split}\begin{array}{llcl} -\def\mathdef2446#1{{}}\mathdef2446{administrative instruction} & \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} &::=& - \dots \\ &&|& - \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ &&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~\href{../syntax/values.html#syntax-int}{\mathit{u\scriptstyle\kern-0.1em31}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~\href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~\href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}~\href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}} \\&&|& - \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}} \\&&|& - \href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\ &&|& - \href{../exec/runtime.html#syntax-return-invoke}{\mathsf{return\_invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\ &&|& - \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|& - \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{\href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}}\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}} &::=& \dots \\ &&|& +{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} \\ &&|& +{{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\ &&|& +{{\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}}_{n}}{\{ {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\ &&|& +\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \end{array}\end{split}\]
    -

    The \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) instruction represents the occurrence of a trap. -Traps are bubbled up through nested instruction sequences, ultimately reducing the entire program to a single \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) instruction, signalling abrupt termination.

    -

    The \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}\) instruction represents unboxed scalar reference values, -\(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}\) and \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}\) represent structure and array reference values, respectively, -and \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}\) instruction represents function reference values. -Similarly, \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}\) represents host references -and \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}\) represents any externalized reference.

    -

    The \(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}\) instruction represents the imminent invocation of a function instance, identified by its address. -It unifies the handling of different forms of calls. -Analogously, \(\href{../exec/runtime.html#syntax-return-invoke}{\mathsf{return\_invoke}}\) represents the imminent tail invocation of a function instance.

    -

    The \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) and \(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}\) instructions model labels and frames “on the stack”. -Moreover, the administrative syntax maintains the nesting structure of the original structured control instruction or function body and their instruction sequences with an \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) marker. -That way, the end of the inner instruction sequence is known when part of an outer sequence.

    +

    An address reference represents an allocated reference value of respective form “on the stack”.

    +

    The \(\mathsf{label}\) and \(\mathsf{frame}\) instructions model labels and frames “on the stack”. +Moreover, the administrative syntax maintains the nesting structure of the original structured control instruction or function body and their instruction sequences.

    +

    The \(\mathsf{trap}\) instruction represents the occurrence of a trap. +Traps are bubbled up through nested instruction sequences, ultimately reducing the entire program to a single \(\mathsf{trap}\) instruction, signalling abrupt termination.

    Note

    -

    For example, the reduction rule for \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) is:

    +

    For example, the reduction rule for \(\mathsf{block}\) is:

    -\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~[t^n]~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad -\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\]
    -

    This replaces the block with a label instruction, +\[(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}) \href{../exec/conventions.html#exec-notation}{\hookrightarrow} ({{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ \epsilon \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\]

    +

    if the block type \({\mathit{bt}}\) denotes a function type \({t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}}\), +such that \(n\) is the block’s result arity. +This rule replaces the block with a label instruction, which can be interpreted as “pushing” the label on the stack. -When \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence of \(n\) \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) instructions representing the resulting values – then the \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) instruction is eliminated courtesy of its own reduction rule:

    +When its end is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence of \(n\) values representing the results – then the \(\mathsf{label}\) instruction is eliminated courtesy of its own reduction rule:

    -\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_m\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\]
    -

    This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand values.

    +\[({{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}) \href{../exec/conventions.html#exec-notation}{\hookrightarrow} {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\] +

    This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand values. +Validation guarantees that \(n\) matches the number \({|{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}|}\) of resulting values at this point.

    -
    -

    Block Contexts

    -

    In order to specify the reduction of branches, the following syntax of block contexts is defined, indexed by the count \(k\) of labels surrounding a hole \([\_]\) that marks the place where the next step of computation is taking place:

    -
    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^0 &::=& - \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~[\_]~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ -\def\mathdef2446#1{{}}\mathdef2446{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^{k+1} &::=& - \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^k~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ -\end{array}\end{split}\]
    -

    This definition allows to index active labels surrounding a branch or return instruction.

    -
    -

    Note

    -

    For example, the reduction of a simple branch can be defined as follows:

    -
    -\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_0\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^l[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\]
    -

    Here, the hole \([\_]\) of the context is instantiated with a branch instruction. -When a branch occurs, -this rule replaces the targeted label and associated instruction sequence with the label’s continuation. -The selected label is identified through the label index \(l\), which corresponds to the number of surrounding \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) instructions that must be hopped over – which is exactly the count encoded in the index of a block context.

    -
    -
    -

    Configurations

    -

    A configuration consists of the current store and an executing thread.

    -

    A thread is a computation over instructions -that operates relative to the state of a current frame referring to the module instance in which the computation runs, i.e., where the current function originates from.

    -
    -\[\begin{split}\begin{array}{llcl} -\def\mathdef2446#1{{}}\mathdef2446{configuration} & \href{../exec/runtime.html#syntax-config}{\mathit{config}} &::=& - \href{../exec/runtime.html#syntax-store}{\mathit{store}}; \href{../exec/runtime.html#syntax-thread}{\mathit{thread}} \\ -\def\mathdef2446#1{{}}\mathdef2446{thread} & \href{../exec/runtime.html#syntax-thread}{\mathit{thread}} &::=& - \href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}}; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ +

    Configurations

    +

    A configuration describes the current computation. +It consists of the computations’s state and the sequence of instructions left to execute. +The state in turn consists of a global store and a current frame referring to the module instance in which the computation runs, i.e., where the current function originates from.

    +
    +\[\begin{split}\begin{array}{@{}l@{}rrl@{}l@{}} +& {\href{../exec/runtime.html#syntax-config}{\mathit{config}}} &::=& {\href{../exec/runtime.html#syntax-state}{\mathit{state}}} ; {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\[0.8ex] +& {\href{../exec/runtime.html#syntax-state}{\mathit{state}}} &::=& {\href{../exec/runtime.html#syntax-store}{\mathit{store}}} ; {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} \\ \end{array}\end{split}\]

    Note

    @@ -572,40 +520,6 @@

    Activation Frames -

    Evaluation Contexts

    -

    Finally, the following definition of evaluation context and associated structural rules enable reduction inside instruction sequences and administrative forms as well as the propagation of traps:

    -
    -\[\begin{split}\begin{array}{llll} -\def\mathdef2446#1{{}}\mathdef2446{evaluation contexts} & E &::=& - [\_] ~|~ - \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~E~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast ~|~ - \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~E~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ -\end{array}\end{split}\]
    -
    -\[\begin{split}\begin{array}{rcl} -S; F; E[\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast] &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F'; E[{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast] \\ - && (\mathrel{\mbox{if}} S; F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S'; F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast) \\ -S; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F'\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F''\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ - && (\mathrel{\mbox{if}} S; F'; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S'; F''; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast) \\[1ex] -S; F; E[\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}] &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} - \qquad (\mathrel{\mbox{if}} E \neq [\_]) \\ -S; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F'\}~\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ -\end{array}\end{split}\]
    -

    Reduction terminates when a thread’s instruction sequence has been reduced to a result, -that is, either a sequence of values or to a \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\).

    -
    -

    Note

    -

    The restriction on evaluation contexts rules out contexts like \([\_]\) and \(\epsilon~[\_]~\epsilon\) for which \(E[\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}] = \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\).

    -

    For an example of reduction under evaluation contexts, consider the following instruction sequence.

    -
    -\[(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_2)~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{neg}}~(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\]
    -

    This can be decomposed into \(E[(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_2)~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{neg}}]\) where

    -
    -\[E = (\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~[\_]~(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\]
    -

    Moreover, this is the only possible choice of evaluation context where the contents of the hole matches the left-hand side of a reduction rule.

    -
    -

    diff --git a/core/exec/types.html b/core/exec/types.html index 798ee0dd64..441bb542a4 100644 --- a/core/exec/types.html +++ b/core/exec/types.html @@ -6,7 +6,7 @@ - Types — WebAssembly 3.0 (Draft 2024-05-30) + Types — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/exec/values.html b/core/exec/values.html index e32e755001..e0509f2335 100644 --- a/core/exec/values.html +++ b/core/exec/values.html @@ -6,7 +6,7 @@ - Values — WebAssembly 3.0 (Draft 2024-05-30) + Values — WebAssembly 3.0 (Draft 2024-06-01) diff --git a/core/genindex.html b/core/genindex.html index bce14b40b8..a03f1bb943 100644 --- a/core/genindex.html +++ b/core/genindex.html @@ -5,7 +5,7 @@ - Index — WebAssembly 3.0 (Draft 2024-05-30) + Index — WebAssembly 3.0 (Draft 2024-06-01) @@ -141,6 +141,8 @@

    A

  • data index
  • data instance +
  • +
  • data type
  • defined type, [1], [2]
  • @@ -153,6 +155,8 @@

    A

  • element instance
  • element mode +
  • +
  • element type
  • export, [1]
  • @@ -162,7 +166,7 @@

    A

  • external index
  • -
  • external type, [1] +
  • external type, [1]
  • external value
  • @@ -542,8 +546,6 @@

    B

  • type
  • -
  • block context -
  • block type, [1], [2], [3]