Merge branch 'main' into walker2

Wasm-DSL · Sep 13, 2024 · 31e52cf · 31e52cf
2 parents 521eb00 + 3156bce
commit 31e52cf
Show file tree

Hide file tree

Showing 106 changed files with 11,047 additions and 10,159 deletions.
diff --git a/.github/workflows/ci-spec.yml b/.github/workflows/ci-spec.yml
@@ -40,10 +40,10 @@ jobs:
         run: cd spectec && opam exec make
       - name: Build main spec
         run: cd document/core && opam exec make main
-      - name: Run Bikeshed
+      #- name: Run Bikeshed
       #  run: cd document/core && opam exec make bikeshed
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: core-rendered
           path: document/core/_build/html
@@ -56,9 +56,9 @@ jobs:
       - name: Setup Bikeshed
         run: pip install bikeshed && bikeshed update
       - name: Run Bikeshed
-      #  run: bikeshed spec "document/js-api/index.bs" "document/js-api/index.html"
+        run: bikeshed spec "document/js-api/index.bs" "document/js-api/index.html"
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: js-api-rendered
           path: document/js-api/index.html
@@ -71,9 +71,9 @@ jobs:
       - name: Setup Bikeshed
         run: pip install bikeshed && bikeshed update
       - name: Run Bikeshed
-      #  run: bikeshed spec "document/web-api/index.bs" "document/web-api/index.html"
+        run: bikeshed spec "document/web-api/index.bs" "document/web-api/index.html"
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: web-api-rendered
           path: document/web-api/index.html
@@ -93,7 +93,7 @@ jobs:
       - name: Build main spec
         run: cd document/metadata/code && make main
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: code-metadata-rendered
           path: document/metadata/code/_build/html
@@ -112,7 +112,7 @@ jobs:
       - name: Build main spec
         run: cd document/legacy/exceptions/core && make main
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: legacy-exceptions-core-rendered
           path: document/legacy/exceptions/core/_build/html
@@ -125,9 +125,9 @@ jobs:
       - name: Setup Bikeshed
         run: pip install bikeshed && bikeshed update
       - name: Run Bikeshed
-      #  run: bikeshed spec "document/legacy/exceptions/js-api/index.bs" "document/legacy/exceptions/js-api/index.html"
+        run: bikeshed spec "document/legacy/exceptions/js-api/index.bs" "document/legacy/exceptions/js-api/index.html"
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: legacy-exceptions-js-api-rendered
           path: document/legacy/exceptions/js-api/index.html
@@ -141,32 +141,32 @@ jobs:
       - name: Create output directory
         run: mkdir _output && cp document/index.html _output/index.html
       - name: Download core spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: core-rendered
           path: _output/core
       - name: Download JS API spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: js-api-rendered
           path: _output/js-api
       - name: Download Web API spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: web-api-rendered
           path: _output/web-api
       - name: Download code metadata spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: code-metadata-rendered
           path: _output/metadata/code
       - name: Download legacy exceptions core spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: legacy-exceptions-core-rendered
           path: _output/legacy/exceptions/core
       - name: Download legacy exceptions JS API spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: legacy-exceptions-js-api-rendered
           path: _output/legacy/exceptions/js-api

diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py
@@ -349,7 +349,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{12}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'),
     Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{13}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'),
     Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{14}', r"[(\REF~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
-    Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{15}', r"[(REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
+    Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{15}', r"[(\REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
     Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{16}', r"[(\REF~t')] \to [(\REF~t)]", r'valid-ref.cast', r'exec-ref.cast'),
     Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{17}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'),
     Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{18}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'),

diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
@@ -595,11 +595,11 @@ $${rule-prose: Step_read/array.new_data}
 
 17. Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpack(\X{ft})`.
 
-18. For each consecutive subsequence :math:`{b'}^n` of :math:`b^\ast`:
+18. For each of the :math:`n` consecutive subsequences :math:`{b'}^z` of :math:`b^\ast`:
 
     a. Assert: due to :ref:`validation <valid-array.new_data>`, :math:`\bytes_{\X{ft}}` is defined.
 
-    b. Let :math:`c_i` be the constant for which :math:`\bytes_{\X{ft}}(c_i)` is :math:`{b'}^n`.
+    b. Let :math:`c_i` be the constant for which :math:`\bytes_{\X{ft}}(c_i)` is :math:`{b'}^z`.
 
     c. Push the value :math:`t.\CONST~c_i` to the stack.
 

diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst
@@ -479,19 +479,17 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
 14. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode <syntax-datamode>` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do:
 
-    a. Assert: :math:`\memidx_i` is :math:`0`.
+    a. Let :math:`n` be the length of the list :math:`\data_i.\DINIT`.
 
-    b. Let :math:`n` be the length of the list :math:`\data_i.\DINIT`.
+    b. :ref:`Execute <exec-instrs>` the instruction sequence :math:`\X{dinstr}^\ast_i`.
 
-    c. :ref:`Execute <exec-instrs>` the instruction sequence :math:`\X{dinstr}^\ast_i`.
-
-    d. :ref:`Execute <exec-const>` the instruction :math:`\I32.\CONST~0`.
+    c. :ref:`Execute <exec-const>` the instruction :math:`\I32.\CONST~0`.
 
-    e. :ref:`Execute <exec-const>` the instruction :math:`\I32.\CONST~n`.
+    d. :ref:`Execute <exec-const>` the instruction :math:`\I32.\CONST~n`.
 
-    f. :ref:`Execute <exec-memory.init>` the instruction :math:`\MEMORYINIT~i`.
+    e. :ref:`Execute <exec-memory.init>` the instruction :math:`\MEMORYINIT~i`.
 
-    g. :ref:`Execute <exec-data.drop>` the instruction :math:`\DATADROP~i`.
+    f. :ref:`Execute <exec-data.drop>` the instruction :math:`\DATADROP~i`.
 
 15. If the :ref:`start function <syntax-start>` :math:`\module.\MSTART` is not empty, then:
 

diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst
@@ -239,7 +239,7 @@ $${syntax: context}
 Convention
 ..........
 
-A type of any shape can be *closed* to bring it into :ref:`closed <type-closed>` form relative to a :ref:`context <context>` it is :ref:`valid <valid-type>` in by :ref:`substituting <notation-subst>` each :ref:`type index <syntax-typeidx>` ${:x} occurring in it with its own corresponding :ref:`defined type <syntax-deftype>` ${deftype: C.TYPES[x]}, after first closing the the types in ${deftype*: C.TYPES} themselves.
+A type of any shape can be *closed* to bring it into :ref:`closed <type-closed>` form relative to a :ref:`context <context>` it is :ref:`valid <valid-type>` in, by :ref:`substituting <notation-subst>` each :ref:`type index <syntax-typeidx>` ${:x} occurring in it with its own corresponding :ref:`defined type <syntax-deftype>` ${deftype: C.TYPES[x]}, after first closing the types in ${deftype*: C.TYPES} themselves.
 
 $${definition: clos_valtype clos_deftypes}
 

diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst
@@ -255,7 +255,7 @@ $${rule: Deftype_sub/refl Deftype_sub/super}
 .. note::
    Note that there is no explicit definition of type *equivalence*,
    since it coincides with syntactic equality,
-   as used in the premise of the fomer rule above.
+   as used in the premise of the former rule above.
 
 
 .. index:: limits

diff --git a/document/js-api/index.bs b/document/js-api/index.bs
@@ -62,8 +62,6 @@ urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
         text: 𝔽; url: #𝔽
         text: ℤ; url: #ℤ
         text: SameValue; url: sec-samevalue
-    type: abstract-op
-        text: CreateMethodProperty; url: sec-createmethodproperty
 urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: dfn
     url: valid/modules.html#valid-module
         text: valid
@@ -395,7 +393,7 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje
                 1. Let |index| be the number of external functions in |imports|. This value |index| is known as the <dfn>index of the host function</dfn> |funcaddr|.
             1. Let |externfunc| be the [=external value=] [=external value|func=] |funcaddr|.
             1. [=list/Append=] |externfunc| to |imports|.
-        1. If |externtype| is of the form [=global=] <var ignore>mut</var> |valtype|,
+        1. If |externtype| is of the form [=external-type/global=] <var ignore>mut</var> |valtype|,
             1. If |v| [=implements=] {{Global}},
                 1. Let |globaladdr| be |v|.\[[Global]].
             1. Otherwise,
@@ -411,16 +409,16 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje
                 1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
             1. Let |externglobal| be [=external value|global=] |globaladdr|.
             1. [=list/Append=] |externglobal| to |imports|.
-        1. If |externtype| is of the form [=mem=] <var ignore>memtype</var>,
+        1. If |externtype| is of the form [=external-type/mem=] <var ignore>memtype</var>,
             1. If |v| does not [=implement=] {{Memory}}, throw a {{LinkError}} exception.
             1. Let |externmem| be the [=external value=] [=external value|mem=] |v|.\[[Memory]].
             1. [=list/Append=] |externmem| to |imports|.
-        1. If |externtype| is of the form [=table=] <var ignore>tabletype</var>,
+        1. If |externtype| is of the form [=external-type/table=] <var ignore>tabletype</var>,
             1. If |v| does not [=implement=] {{Table}}, throw a {{LinkError}} exception.
             1. Let |tableaddr| be |v|.\[[Table]].
             1. Let |externtable| be the [=external value=] [=external value|table=] |tableaddr|.
             1. [=list/Append=] |externtable| to |imports|.
-        1. If |externtype| is of the form [=externtype/tag=] |attribute| <var ignore>functype</var>,
+        1. If |externtype| is of the form [=external-type/tag=] |attribute| <var ignore>functype</var>,
             1. Assert: |attribute| is [=tagtype/attribute/exception=].
             1. If |v| does not [=implement=] {{Tag}}, throw a {{LinkError}} exception.
             1. Let |tagaddr| be |v|.\[[Address]].
@@ -444,22 +442,22 @@ The verification of WebAssembly type requirements is deferred to the
             1. Let [=external value|func=] |funcaddr| be |externval|.
             1. Let |func| be the result of creating [=a new Exported Function=] from |funcaddr|.
             1. Let |value| be |func|.
-        1. If |externtype| is of the form [=global=] <var ignore>mut</var> <var ignore>globaltype</var>,
+        1. If |externtype| is of the form [=external-type/global=] <var ignore>mut</var> <var ignore>globaltype</var>,
             1. Assert: |externval| is of the form [=external value|global=] |globaladdr|.
             1. Let [=external value|global=] |globaladdr| be |externval|.
             1. Let |global| be [=create a global object|a new Global object=] created from |globaladdr|.
             1. Let |value| be |global|.
-        1. If |externtype| is of the form [=mem=] <var ignore>memtype</var>,
+        1. If |externtype| is of the form [=external-type/mem=] <var ignore>memtype</var>,
             1. Assert: |externval| is of the form [=external value|mem=] |memaddr|.
             1. Let [=external value|mem=] |memaddr| be |externval|.
             1. Let |memory| be [=create a memory object|a new Memory object=] created from |memaddr|.
             1. Let |value| be |memory|.
-        1. If |externtype| is of the form [=table=] <var ignore>tabletype</var>,
+        1. If |externtype| is of the form [=external-type/table=] <var ignore>tabletype</var>,
             1. Assert: |externval| is of the form [=external value|table=] |tableaddr|.
             1. Let [=external value|table=] |tableaddr| be |externval|.
             1. Let |table| be [=create a Table object|a new Table object=] created from |tableaddr|.
             1. Let |value| be |table|.
-        1. If |externtype| is of the form [=externtype/tag=] |attribute| <var ignore>functype</var>,
+        1. If |externtype| is of the form [=external-type/tag=] |attribute| <var ignore>functype</var>,
             1. Assert: |attribute| is [=tagtype/attribute/exception=].
             1. Assert: |externval| is of the form [=external value/tag=] |tagaddr|.
             1. Let [=external value/tag=] |tagaddr| be |externval|.
@@ -582,10 +580,10 @@ interface Module {
 <div algorithm>
   The <dfn>string value of the extern type</dfn> |type| is
     * "function" if |type| is of the form [=external-type/func=] <var ignore>functype</var>
-    * "table" if |type| is of the form [=table=] <var ignore>tabletype</var>
-    * "memory" if |type| is of the form [=mem=] <var ignore>memtype</var>
-    * "global" if |type| is of the form [=global=] <var ignore>globaltype</var>
-    * "tag" if |type| is of the form [=externtype/tag=] <var ignore>tag</var>
+    * "table" if |type| is of the form [=external-type/table=] <var ignore>tabletype</var>
+    * "memory" if |type| is of the form [=external-type/mem=] <var ignore>memtype</var>
+    * "global" if |type| is of the form [=external-type/global=] <var ignore>globaltype</var>
+    * "tag" if |type| is of the form [=external-type/tag=] <var ignore>tag</var>
 </div>
 
 <div algorithm>
@@ -818,7 +816,8 @@ Immediately after a WebAssembly [=memory.grow=] instruction executes, perform th
 {{ArrayBuffer}} objects returned by a {{Memory}} object must have a size that is a multiple of a WebAssembly [=page size=] (the constant 65536). For this reason [=HostResizeArrayBuffer=] is redefined as follows.
 
 <div algorithm>
-    The <dfn>abstract operation [=HostResizeArrayBuffer=]</dfn> takes arguments |buffer| (an {{ArrayBuffer}}) and |newLength|. It performs the following steps when called.
+
+    The <dfn id=HostResizeArrayBuffer export>abstract operation [=HostResizeArrayBuffer=]</dfn> takes arguments |buffer| (an {{ArrayBuffer}}) and |newLength|. It performs the following steps when called.
 
     1. If |buffer|.\[[ArrayBufferDetachKey]] is "WebAssembly.Memory",
         1. Let |map| be the [=surrounding agent=]'s associated [=Memory object cache=].
@@ -1149,7 +1148,7 @@ This slot holds a [=function address=] relative to the [=surrounding agent=]'s [
         1. Let |payload| be [=exn_read=](|store|, |exnaddr|).
         1. Let |jsTagAddr| be the result of [=get the JavaScript exception tag |getting the JavaScript exception tag=].
         1. If |tagaddr| is equal to |jsTagAddr|,
-            1. Throw the result of [=retrieving an extern value=] from |payload|[0].
+            1. Throw the result of [=retrieving a host value=] from |payload|[0].
         1. Otherwise,
             1. Let |exception| be [=create an Exception object|a new Exception=] created from |exnaddr|.
             1. Throw |exception|.
@@ -1180,7 +1179,7 @@ Note: Exported Functions do not have a \[[Construct]] method and thus it is not
     1. If |resultsSize| is 0, return « ».
     1. Otherwise, if |resultsSize| is 1, return « [=?=] [=ToWebAssemblyValue=](|ret|, |results|[0]) ».
     1. Otherwise,
-        1. Let |method| be [=?=] [$GetMethod$](|ret|, {{@@iterator}}).
+        1. Let |method| be [=?=] [$GetMethod$](|ret|, {{%Symbol.iterator%}}).
         1. If |method| is undefined, [=throw=] a {{TypeError}}.
         1. Let |values| be [=?=] [$IteratorToList$]([=?=] [$GetIteratorFromMethod$](|ret|, |method|)).
         1. Let |wasmValues| be a new, empty [=list=].
@@ -1229,7 +1228,7 @@ The algorithm <dfn>ToJSValue</dfn>(|w|) coerces a [=WebAssembly value=] to a Jav
 1. If |w| is of the form [=i64.const=] |u64|,
     1. Let |i64| be [=signed_64=](|u64|).
     1. Return [=ℤ=](|i64| interpreted as a mathematical value).
-1. If |w| is of the form [=i32.const=] |u32|,
+1. If |w| is of the form [=i32.const=] |i32|,
     1. Let |i32| be [=signed_32=](|i32|).
     2. Return [=𝔽=](|i32| interpreted as a mathematical value).
 1. If |w| is of the form [=f32.const=] |f32|,
@@ -1240,15 +1239,15 @@ The algorithm <dfn>ToJSValue</dfn>(|w|) coerces a [=WebAssembly value=] to a Jav
     1. If |f64| is [=+∞=] or [=−∞=], return **+∞**<sub>𝔽</sub> or **-∞**<sub>𝔽</sub>, respectively.
     1. If |f64| is [=nan=], return **NaN**.
     1. Return [=𝔽=](|f64| interpreted as a mathematical value).
-1. If |w| is of the form [=ref.null=] |t|, return null.
+1. If |w| is of the form [=ref.null=] <var ignore>t</var>, return null.
 1. If |w| is of the form [=ref.i31=] |u31|,
     1. Let |i31| be [=signed_31=](|u31|).
     1. Let return [=𝔽=](|i31|).
 1. If |w| is of the form [=ref.struct=] |structaddr|, return the result of creating [=a new Exported GC Object=] from |structaddr| and "struct".
 1. If |w| is of the form [=ref.array=] |arrayaddr|, return the result of creating [=a new Exported GC Object=] from |arrayaddr| and "array".
 1. If |w| is of the form [=ref.func=] |funcaddr|, return the result of creating [=a new Exported Function=] from |funcaddr|.
 1. If |w| is of the form [=ref.host=] |hostaddr|, return the result of [=retrieving a host value=] from |hostaddr|.
-1. If |w| is of the form [=ref.extern=] <var ignore>ref</var>, return [=ToJSValue=](|ref|).
+1. If |w| is of the form [=ref.extern=] |ref|, return [=ToJSValue=](|ref|).
 
 
 Note: Number values which are equal to NaN may have various observable NaN payloads; see [$NumericToRawBytes$] for details.
@@ -1334,8 +1333,6 @@ The algorithm <dfn>ToWebAssemblyValue</dfn>(|v|, |type|) coerces a JavaScript va
 
 The <dfn>tag_alloc</dfn>(|store|, |parameters|) algorithm creates a new [=tag address=] for |parameters| in |store| and returns the updated store and the [=tag address=].
 
-The <dfn>tag_parameters</dfn>(|store|, |tagAddress|) algorithm returns the [=list=] of types for |tagAddress| in |store|.
-
 <h4 id="tag-types">Tag types</h4>
 
 <pre class="idl">
@@ -1494,7 +1491,7 @@ The internal methods of an [=Exported GC Object=] use the following implementati
     1. Set |object|.\[[OwnPropertyKeys]] as specified in [=[[OwnPropertyKeys]] internal method of an Exported GC Object=].
     1. [=map/Set=] |map|[|objectaddr|] to |object|.
     1. Return |object|.
-
+</div>
 
 <h3 id="exceptions">Exceptions</h3>
 
@@ -1639,7 +1636,7 @@ When the [=namespace object=] for the {{WebAssembly}} namespace is [=create a na
 1.  Let |namespaceObject| be the [=namespace object=].
 1.  [=list/iterate|For each=] |error| of « "CompileError", "LinkError", "RuntimeError" »,
     1.  Let |constructor| be a new object, implementing the [=NativeError Object Structure=], with <var ignore>NativeError</var> set to |error|.
-    1.  [=!=] [$CreateMethodProperty$](|namespaceObject|, |error|,  |constructor|).
+    1.  [=!=] [$DefineMethodProperty$](|namespaceObject|, |error|,  |constructor|, false).
 
 </div>