Merge with WebAssembly/{stack-switching,spec/wasm-3.0,spec/main}

.github/workflows/ci-spec.yml

@@ -24,23 +24,24 @@ jobs:
         uses: actions/setup-node@v4
         with:
           node-version: 16
-      - name: Setup Bikeshed
-        run: pip install bikeshed && bikeshed update
+      # - name: Setup Bikeshed
+      #   run: pip install bikeshed && bikeshed update
       - name: Setup TexLive
         run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended
       - name: Setup Sphinx
         run: pip install six && pip install sphinx==5.1.0
       - name: Build main spec
         run: cd document/core && make main
-      - name: Run Bikeshed
-        run: cd document/core && make bikeshed
+      # - name: Run Bikeshed
+      #   run: cd document/core && make bikeshed
       - name: Upload artifact
         uses: actions/upload-artifact@v4
         with:
           name: core-rendered
           path: document/core/_build/html
 
   build-js-api-spec:
+    if: false
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
@@ -56,6 +57,7 @@ jobs:
           path: document/js-api/index.html
 
   build-web-api-spec:
+    if: false
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
@@ -71,11 +73,12 @@ jobs:
           path: document/web-api/index.html
 
   build-code-metadata-spec:
+    if: false
     runs-on: ubuntu-latest
     needs: [build-core-spec]
     steps:
       - name: Checkout repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           submodules: "recursive"
       - name: Setup TexLive
@@ -91,10 +94,11 @@ jobs:
           path: document/metadata/code/_build/html
 
   build-legacy-exceptions-core-spec:
+    if: false
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           submodules: "recursive"
       - name: Setup TexLive
@@ -110,6 +114,7 @@ jobs:
           path: document/legacy/exceptions/core/_build/html
 
   build-legacy-exceptions-js-api-spec:
+    if: false
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
@@ -125,6 +130,7 @@ jobs:
           path: document/legacy/exceptions/js-api/index.html
 
   build-spec-versions:
+    if: false
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
@@ -136,6 +142,7 @@ jobs:
           path: document/versions/
 
   publish-spec:
+    if: false
     runs-on: ubuntu-latest
     needs:
       - build-core-spec

.github/workflows/w3c-publish.yml

@@ -31,7 +31,7 @@ on:
 
 env:
   YARN_ENABLE_IMMUTABLE_INSTALLS: false
-  W3C_STATUS: ${{ github.event_name == 'workflow_dispatch' && inputs.w3c-status || 'WD' }}
+  W3C_STATUS: ${{ github.event_name == 'workflow_dispatch' && inputs.w3c-status || 'CRD' }}
 
 jobs:
   publish-to-w3c-TR:
@@ -64,9 +64,10 @@ jobs:
           W3C_ECHIDNA_TOKEN_CORE: ${{ secrets.W3C_ECHIDNA_TOKEN_CORE }}
           W3C_ECHIDNA_TOKEN_JSAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_JSAPI }}
           W3C_ECHIDNA_TOKEN_WEBAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_WEBAPI }}
+          # Publish the draft on manual dispatches without dry-run set, or on pushes to the main branch.
           ECHIDNA_DRYRUN: |-
-            ${{ (github.event_name == 'workflow_dispatch' && inputs.dry-run) ||
-                !(github.event_name == 'push' && github.repository == 'WebAssembly/spec' && github.ref == 'refs/heads/main') }}
+            ${{ !((github.event_name == 'workflow_dispatch' && !inputs.dry-run) ||
+                  (github.event_name == 'push' && github.repository == 'WebAssembly/spec' && github.ref == 'refs/heads/main')) }}
       - name: Validate ${{ matrix.spec }} spec with Echidna
         if: env.W3C_USERNAME
         run: cd document && make -e -C ${{ matrix.spec }} WD-echidna

document/core/appendix/changes.rst

@@ -462,6 +462,8 @@ Added more precise types for references. [#proposal-typedref]_
 
 * Refined typing of :ref:`local instructions <valid-instr-variable>` and :ref:`instruction sequences <valid-instr-seq>` to track the :ref:`initialization status <syntax-init>` of :ref:`locals <syntax-local>` with non-:ref:`defaultable <valid-defaultable>` type
 
+* Refined decoding of :ref:`active <syntax-elemmode>` :ref:`element segments <binary-elem>` with implicit element type and plain function indices (opcode :math:`0`) to produce :ref:`non-nullable <syntax-nullable>` :ref:`reference type <syntax-reftype>`.
+
 * Extended :ref:`table definitions <syntax-table>` with optional initializer expression
 
 

document/core/appendix/index-instructions.py

@@ -334,7 +334,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\STRUCTGETS~x~y', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
     Instruction(r'\STRUCTGETU~x~y', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
     Instruction(r'\STRUCTSET~x~y', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'),
-    Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
+    Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t~\I32] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
     Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{07}', r'[\I32] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
     Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{08}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'),
     Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{09}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'),

document/core/binary/modules.rst

@@ -611,5 +611,5 @@ where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`,
    The version of the WebAssembly binary format may increase in the future
    if backward-incompatible changes have to be made to the format.
    However, such changes are expected to occur very infrequently, if ever.
-   The binary format is intended to be forward-compatible,
-   such that future extensions can be made without incrementing its version.
+   The binary format is intended to be extensible,
+   such that future features can be added without incrementing its version.

document/core/exec/instructions.rst

@@ -4753,7 +4753,7 @@ Control Instructions
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \REFFUNCADDR~a \\
      \wedge & S.\SFUNCS[a] = f \\
-     \wedge & S \vdashdeftypematch F.\AMODULE.\MITYPES[y] \matchesdeftype f.\FITYPE)
+     \wedge & S \vdashdeftypematch f.\FITYPE \matchesdeftype F.\AMODULE.\MITYPES[y])
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}

document/core/exec/modules.rst

@@ -364,7 +364,7 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
 
 8. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS`, do:
 
-   a. Let :math:`\reftype_i` be the element :ref:`reference type <syntax-reftype>` obtained by `instantiating <type-inst>` :math:`\elem_i.\ETYPE` in :math:`\moduleinst` defined below.
+   a. Let :math:`\reftype_i` be the element :ref:`reference type <syntax-reftype>` obtained by :ref:`instantiating <type-inst>` :math:`\elem_i.\ETYPE` in :math:`\moduleinst` defined below.
 
    b. Let :math:`\elemaddr_i` be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` a :ref:`element instance <syntax-eleminst>` of :ref:`reference type <syntax-reftype>` :math:`\reftype_i` with contents :math:`(\reff_{\F{e}}^\ast)^\ast[i]`.
 

document/core/exec/numerics.rst

@@ -1717,7 +1717,7 @@ It computes :math:`(z_1 \cdot z_2) + z_3` as if with unbounded range and precisi
 
 * Else if both :math:`z_1` and :math:`z_2` are zeroes, then return :math:`1`.
 
-* Else if :math:`z_1` is smaller than or equal to :math:`z_2`, then return :math:`1`.
+* Else if :math:`z_1` is larger than or equal to :math:`z_2`, then return :math:`1`.
 
 * Else return :math:`0`.
 

document/core/syntax/types.rst

@@ -483,11 +483,11 @@ Global Types
 Tag Types
 ~~~~~~~~~
 
-*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a function type.
+*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a defined type |deftype|, which expands to a function type |functype|.
 
 .. math::
    \begin{array}{llll}
-   \production{tag type} &\tagtype &::=& \functype \\
+   \production{tag type} &\tagtype &::=& \deftype \\
    \end{array}
 
 Currently tags are only used for categorizing exceptions.

document/core/util/bikeshed_fixup.py

@@ -65,7 +65,7 @@ def Main():
   # get carried over into the resulting bikeshed output and then end up causing
   # the W3C pubrules checker to refuse to autopublish that bikeshed output.
   data = re.sub(r'.+?(<div class="toctree-wrapper compound">.+)',
-                r'<!doctype HTML>\n<meta charset="utf-8">\n<body>\1',
+                r'<!doctype HTML>\n<meta charset="utf-8">\n<body><section id="webassembly-specification">\1',
                 data, flags=re.DOTALL)
 
   # Drop spurious navigation from footer.

document/core/valid/instructions.rst

@@ -2601,15 +2601,15 @@ Control Instructions
 
 * The tag :math:`C.\CTAGS[x]` must be defined in the context.
 
-* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
 
 * The :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]` must be empty.
 
-* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of  :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
+* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
 .. math::
    \frac{
-     C.\CTAGS[x] = [t^\ast] \to []
+     \expanddt(C.\CTAGS[x]) = [t^\ast] \to []
    }{
      C \vdashinstr \THROW~x : [t_1^\ast~t^\ast] \to [t_2^\ast]
    }

document/core/valid/matching.rst

@@ -580,14 +580,22 @@ A :ref:`global type <syntax-globaltype>` :math:`(\mut_1~t_1)` matches :math:`(\m
 Tag Types
 ~~~~~~~~~
 
-A :ref:`tag type <syntax-tagtype>` :math:`\tagtype_1` matches :math:`\tagtype_2` if and only if they are the same.
+A :ref:`tag type <syntax-tagtype>` :math:`\deftype_1` matches :math:`\deftype_2` if and only if the :ref:`defined type <syntax-deftype>` :math:`\deftype_1` :ref:`matches <match-deftype>` :math:`\deftype_2`, and vice versa.
 
 .. math::
    \frac{
+     C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2
+     \qquad
+     C \vdashdeftypematch \deftype_2 \matchesdeftype \deftype_1
    }{
-     C \vdashtagtypematch \tagtype \matchestagtype \tagtype
+     C \vdashtagtypematch \deftype_1 \matchestagtype \deftype_2
    }
 
+.. note::
+   Although the conclusion of this rule looks identical to its premise,
+   they in fact describe different relations:
+   the premise invokes subtyping on defined types,
+   while the conclusion defines it on tag types that happen to be expressed as defined types.
 
 .. index:: external type, function type, table type, memory type, global type
 .. _match-externtype:

document/core/valid/types.rst

@@ -551,19 +551,25 @@ Memory Types
 Tag Types
 ~~~~~~~~~
 
-:math:`[t_1^n] \to [t_2^m]`
-...........................
+:math:`\deftype`
+................
 
-* The :ref:`function type <syntax-functype>` :math:`[t_1^n] \to [t_2^m]` must be :ref:`valid <valid-functype>`.
+
+* The :ref:`defined type <syntax-deftype>` :math:`\deftype` must be :ref:`valid <valid-deftype>`.
+
+* The :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^n] \toF [t_2^m]`.
 
 * The type sequence :math:`t_2^m` must be empty.
 
 * Then the tag type is valid.
 
 .. math::
    \frac{
+     C \vdashdeftype \deftype \ok
+     \qquad
+     \expanddt(\deftype) = \TFUNC~[t^\ast] \to []
    }{
-     \vdashtagtype [t^\ast] \to [] \ok
+     C \vdashtagtype \deftype \ok
    }
 
 

document/js-api/index.bs

@@ -1350,7 +1350,7 @@ The algorithm <dfn>ToWebAssemblyValue</dfn>(|v|, |type|) coerces a JavaScript va
         1. Let |n| be an implementation-defined integer such that [=canon=]<sub>32</sub> &leq; |n| &lt; 2<sup>[=signif=](32)</sup>.
         1. Let |f32| be [=nan=](n).
     1. Otherwise,
-        1. Let |f32| be |number| rounded to the nearest representable value using IEEE 754-2008 round to nearest, ties to even mode. [[IEEE-754]]
+        1. Let |f32| be |number| rounded to the nearest representable value using IEEE 754-2019 round to nearest, ties to even mode. [[IEEE-754]]
     1. Return [=f32.const=] |f32|.
 1. If |type| is [=f64=],
     1. Let |number| be [=?=] [$ToNumber$](|v|).
@@ -1820,7 +1820,8 @@ In practice, an implementation may run out of resources for valid modules below
 
 <ul>
 <li>The maximum size of a table is 10,000,000.</li>
-<li>The maximum number of pages of a memory is 65,536.</li>
+<li>The maximum size of a 32-bit memory is 65,536 pages (4 GiB).</li>
+<li>The maximum size of a 64-bit memory is 262,144 pages (16 GiB).</li>
 </ul>
 
 <h2 id="security-considerations">Security and Privacy Considerations</h2>

interpreter/exec/eval.ml

@@ -72,8 +72,8 @@ and admin_instr' =
   | Label of int * instr list * code
   | Frame of int * frame * code
   | Handler of int * catch list * code
-  | Handle of handle_table * code
-  | Suspending of tag_inst * value stack * ref_ option * ctxt
+  | Prompt of handle_table * code
+  | Suspending of tag_inst * value stack * (int32 * ref_) option * ctxt
 
 and ctxt = code -> code
 and handle_table = (tag_inst * idx) list * tag_inst list
@@ -391,7 +391,7 @@ let rec step (c : config) : config =
         let hs = handle_table c xls in
         let args, vs' = i32_split n vs e.at in
         cont := None;
-        vs', [Handle (hs, ctxt (args, [])) @@ e.at]
+        vs', [Prompt (hs, ctxt (args, [])) @@ e.at]
 
       | ResumeThrow (x, y, xls), Ref (NullRef _) :: vs ->
         vs, [Trapping "null continuation reference" @@ e.at]
@@ -405,18 +405,21 @@ let rec step (c : config) : config =
         let hs = handle_table c xls in
         let args, vs' = i32_split (Lib.List32.length ts) vs e.at in
         cont := None;
-        vs', [Handle (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at]
+        vs', [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at]
 
       | Switch (x, y), Ref (NullRef _) :: vs ->
          vs, [Trapping "null continuation reference" @@ e.at]
 
       | Switch (x, y), Ref (ContRef {contents = None}) :: vs ->
          vs, [Trapping "continuation already consumed" @@ e.at]
 
-      | Switch (x, y), Ref (ContRef {contents = Some (n, ctxt)} as cont) :: vs ->
+      | Switch (x, y), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
+         let FuncT (ts, _) = func_type_of_cont_type c.frame.inst (cont_type c.frame.inst x) in
+         let FuncT (ts', _) = as_cont_func_ref_type (Lib.List.last ts) in
+         let arity = Lib.List32.length ts' in
          let tagt = tag c.frame.inst y in
          let args, vs' = i32_split (Int32.sub n 1l) vs e.at in
-         vs', [Suspending (tagt, args, Some cont, fun code -> code) @@ e.at]
+         vs', [Suspending (tagt, args, Some (arity, ContRef cont), fun code -> code) @@ e.at]
 
       | ReturnCall x, vs ->
         (match (step {c with code = (vs, [Plain (Call x) @@ e.at])}).code with
@@ -1282,35 +1285,34 @@ let rec step (c : config) : config =
         with Crash (_, msg) -> Crash.error e.at msg)
       )
 
-    | Handle (hso, (vs', [])), vs ->
+    | Prompt (hso, (vs', [])), vs ->
       vs' @ vs, []
 
-    | Handle ((hs, _), (vs', {it = Suspending (tagt, vs1, None, ctxt); at} :: es')), vs
+    | Prompt ((hs, _), (vs', {it = Suspending (tagt, vs1, None, ctxt); at} :: es')), vs
       when List.mem_assq tagt hs ->
       let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
       let ctxt' code = compose (ctxt code) (vs', es') in
       [Ref (ContRef (ref (Some (Lib.List32.length ts, ctxt'))))] @ vs1 @ vs,
       [Plain (Br (List.assq tagt hs)) @@ e.at]
 
-    | Handle ((_, hs) as hso, (vs', {it = Suspending (tagt, vs1, Some (ContRef ({contents = Some (_, ctxt)} as cont)), ctxt'); at} :: es')), vs
+    | Prompt ((_, hs) as hso, (vs', {it = Suspending (tagt, vs1, Some (ar, ContRef ({contents = Some (_, ctxt)} as cont)), ctxt'); at} :: es')), vs
        when List.memq tagt hs ->
-       let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
        let ctxt'' code = compose (ctxt' code) (vs', es') in
-       let cont' = Ref (ContRef (ref (Some (Int32.add (Lib.List32.length ts) 1l, ctxt'')))) in
+       let cont' = Ref (ContRef (ref (Some (ar, ctxt'')))) in
        let args = cont' :: vs1 in
        cont := None;
-       vs' @ vs, [Handle (hso, ctxt (args, [])) @@ e.at]
+       vs' @ vs, [Prompt (hso, ctxt (args, [])) @@ e.at]
 
-    | Handle (hso, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
-      let ctxt' code = [], [Handle (hso, compose (ctxt code) (vs', es')) @@ e.at] in
+    | Prompt (hso, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
+      let ctxt' code = [], [Prompt (hso, compose (ctxt code) (vs', es')) @@ e.at] in
       vs, [Suspending (tagt, vs1, contref, ctxt') @@ at]
 
-    | Handle (hso, (vs', e' :: es')), vs when is_jumping e' ->
+    | Prompt (hso, (vs', e' :: es')), vs when is_jumping e' ->
       vs, [e']
 
-    | Handle (hso, code'), vs ->
+    | Prompt (hso, code'), vs ->
       let c' = step {c with code = code'} in
-      vs, [Handle (hso, c'.code) @@ e.at]
+      vs, [Prompt (hso, c'.code) @@ e.at]
 
     | Suspending (_, _, _, _), _ -> assert false