Update testharness.js from upstream.

.github/workflows/ci-interpreter.yml

@@ -24,13 +24,16 @@ jobs:
           ocaml-compiler: 4.14.x
       - name: Setup OCaml tools
         run: opam install --yes ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
-      - name: Setup Node.js
-        uses: actions/setup-node@v4
-        with:
-          node-version: 20.x
       - name: Build interpreter
         run: cd interpreter && opam exec make
+      # Neither V8 nor SpiderMonkey can currently handle all 3.0 tests, so we disable checking JS translation for now.
+      #- name: Setup Node.js
+      #  uses: actions/setup-node@v4
+      #  with:
+      #    node-version: 25-nightly
+      #- name: Setup SpiderMonkey
+      #  run: curl -O https://archive.mozilla.org/pub/firefox/nightly/latest-mozilla-central/jsshell-linux-x86_64.zip && unzip jsshell-linux-x86_64.zip
       - name: Run tests
-        # TODO: reactivate node once it supports all of Wasm 3.0
-        # run: cd interpreter && opam exec make JS=node ci
-        run: cd interpreter && opam exec make ci
+        run: cd interpreter && opam exec make ci           # don't test JS translation
+      # run: cd interpreter && opam exec make JS=node ci   # test with V8
+      # run: cd interpreter && opam exec make JS=../js ci  # test with SM

.github/workflows/w3c-publish.yml

@@ -46,6 +46,13 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: "recursive"
+      - name: Setup OCaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.x
+      - name: Setup Dune
+        if: ${{ matrix.spec == 'core' }}
+        run: opam install --yes dune menhir mdx zarith && opam exec dune --version
       - name: Setup Node.js
         uses: actions/setup-node@v4
         with:
@@ -57,10 +64,13 @@ jobs:
         run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended
       - name: Setup Sphinx
         if: ${{ matrix.spec == 'core' }}
-        run: pip install six && pip install sphinx==8.0.0
-      - name: Publish ${{ matrix.spec }} spec to its https://www.w3.org/TR/ URL
+        run: pip install six && pip install sphinx==8.1.3
+      - name: Build SpecTec
+        if: ${{ matrix.spec == 'core' }}
+        run: cd spectec && opam exec make
+      - name: Publish (or validate) ${{ matrix.spec }} spec to its https://www.w3.org/TR/ URL
         if: env.W3C_ECHIDNA_TOKEN_CORE
-        run: cd document && make -e -C ${{ matrix.spec }} WD-echidna-CI
+        run: cd document/${{ matrix.spec }} && opam exec make W3C_STATUS=${{ env.W3C_STATUS }} ECHIDNA_DRYRUN=${{ env.ECHIDNA_DRYRUN}} WD-echidna-CI
         env:
           W3C_ECHIDNA_TOKEN_CORE: ${{ secrets.W3C_ECHIDNA_TOKEN_CORE }}
           W3C_ECHIDNA_TOKEN_JSAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_JSAPI }}
@@ -69,9 +79,9 @@ jobs:
           ECHIDNA_DRYRUN: |-
             ${{ !((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
+      - name: Validate ${{ matrix.spec }} spec with Echidna using personal credentials
         if: env.W3C_USERNAME
-        run: cd document && make -e -C ${{ matrix.spec }} WD-echidna
+        run: cd document/${{ matrix.spec }} && opam exec make W3C_STATUS=${{ env.W3C_STATUS }} WD-echidna
         env:
           W3C_USERNAME: ${{ secrets.W3C_USERNAME }}
           W3C_PASSWORD: ${{ secrets.W3C_PASSWORD }}

document/core/Makefile

@@ -250,7 +250,7 @@ WD-echidna: WD-tar
 		-F "tar=@$(BUILDDIR)/WD.tar" \
 		-F "decision=$(DECISION_URL)" \
 		-F "dry-run=$(ECHIDNA_DRYRUN)" | tee $(BUILDDIR)/WD-echidna-id.txt
-	python3 ../util/check-echidna-status.py $(BUILDDIR)
+	python3 ../util/check-echidna-status.py --ignore-failure $(BUILDDIR)
 	@echo
 	@echo "Uploaded $(W3C_STATUS). Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`"
 
@@ -266,7 +266,7 @@ WD-echidna-CI: WD-tar
 		-F "token=$(W3C_ECHIDNA_TOKEN_CORE)" \
 		-F "decision=$(DECISION_URL)" \
 		-F "dry-run=$(ECHIDNA_DRYRUN)" | tee $(BUILDDIR)/WD-echidna-id.txt
-	python3 ../util/check-echidna-status.py $(BUILDDIR)
+	python3 ../util/check-echidna-status.py --ignore-failure $(BUILDDIR)
 	@echo
 	@echo "Uploaded $(W3C_STATUS). Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`"
 

document/core/appendix/algorithm.rst

@@ -277,7 +277,7 @@ It allocates a new frame record recording them along with the current height of
 Popping a frame first checks that the control stack is not empty.
 It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack.
 Afterwards, it checks that the stack has shrunk back to its initial height.
-Finally, it undoes all changes to the initialization status of locals that happend inside the block.
+Finally, it undoes all changes to the initialization status of locals that happened inside the block.
 
 The type of the :ref:`label <syntax-label>` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from.
 

document/core/appendix/changes.rst

@@ -367,7 +367,7 @@ Added instructions to perform tail calls. [#proposal-tailcall]_
 Exception Handling
 ..................
 
-Added tag definitions, imports, and exports, and instructions to throw and catch exceptions [#proposal-exn]_
+Added tag definitions, imports, and exports, and instructions to throw and catch exceptions. [#proposal-exn]_
 
 * :ref:`Modules <syntax-module>` may
 
@@ -500,7 +500,7 @@ Added more precise types for references. [#proposal-typedref]_
 
 * Refined typing of :ref:`local instructions <valid-instr-variable>` and :ref:`instruction sequences <valid-instrs>` to track the :ref:`initialization status <syntax-init>` of :ref:`locals <syntax-local>` with non-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-null <syntax-null>` :ref:`reference type <syntax-reftype>`.
+* 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-null <syntax-null>` :ref:`reference type <syntax-reftype>`
 
 * Extended :ref:`table definitions <syntax-table>` with optional initializer expression
 

document/core/appendix/custom.rst

@@ -178,7 +178,7 @@ It consists of an :ref:`indirect name map <binary-indirectnamemap>` assigning fi
 .. math::
    \begin{array}{llclll}
    \production{field name subsection} & \Bfieldnamesubsec &::=&
-     \Bnamesubsection_10(\Bindirectnamemap) \\
+     \Bnamesubsection_{10}(\Bindirectnamemap) \\
    \end{array}
 
 
@@ -194,7 +194,7 @@ It consists of a :ref:`name map <binary-namemap>` assigning tag names to :ref:`t
 .. math::
    \begin{array}{llclll}
    \production{tag name subsection} & \Btagnamesubsec &::=&
-     \Bnamesubsection_1(\Bnamemap) \\
+     \Bnamesubsection_{11}(\Bnamemap) \\
    \end{array}
 
 

document/core/appendix/index-instructions.py

@@ -478,7 +478,7 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non
     Instruction(2.0, r'\I8X16.\VABS', r'\hex{FD}~~\hex{60}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'),
     Instruction(2.0, r'\I8X16.\VNEG', r'\hex{FD}~~\hex{61}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ineg'),
     Instruction(2.0, r'\I8X16.\VPOPCNT', r'\hex{FD}~~\hex{62}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ipopcnt'),
-    Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop', r'op-inez'),
+    Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop'),
     Instruction(2.0, r'\I8X16.\VBITMASK', r'\hex{FD}~~\hex{64}', r'[\V128] \to [\I32]', r'valid-vbitmask', r'exec-vbitmask', r'op-ivbitmask'),
     Instruction(2.0, r'\I8X16.\VNARROW\K{\_i16x8\_s}', r'\hex{FD}~~\hex{65}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vnarrow', r'op-vnarrow'),
     Instruction(2.0, r'\I8X16.\VNARROW\K{\_i16x8\_u}', r'\hex{FD}~~\hex{66}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vnarrow', r'op-vnarrow'),
@@ -616,6 +616,7 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non
     Instruction(2.0, r'\F32X4.\VPMAX', r'\hex{FD}~~\hex{EB}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fpmax'),
     Instruction(2.0, r'\F64X2.\VABS', r'\hex{FD}~~\hex{EC}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-fabs'),
     Instruction(2.0, r'\F64X2.\VNEG', r'\hex{FD}~~\hex{ED}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-fneg'),
+    Instruction(0.0, None, r'\hex{FD}~\hex{EE}~\hex{01}'),
     Instruction(2.0, r'\F64X2.\VSQRT', r'\hex{FD}~~\hex{EF}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-fsqrt'),
     Instruction(2.0, r'\F64X2.\VADD', r'\hex{FD}~~\hex{F0}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fadd'),
     Instruction(2.0, r'\F64X2.\VSUB', r'\hex{FD}~~\hex{F1}~~\hex{01}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fsub'),

document/core/appendix/properties.rst

@@ -1087,27 +1087,6 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    }
 
 
-.. index:: function address, extern value, extern type, function type
-
-:math:`\INVOKE~\funcaddr`
-.........................
-
-* The :ref:`external function address <syntax-externaddr>` :math:`\XAFUNC~\funcaddr` must be :ref:`valid <valid-externaddr-func>` with :ref:`external function type <syntax-externtype>` :math:`\XTFUNC~\deftype'`.
-
-* The :ref:`expansion <aux-expand-deftype>` of the :ref:`defined type <syntax-deftype>` :math:`\deftype` must be some :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^\ast] \Tarrow [t_2^\ast])`.
-
-* Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`.
-
-.. math::
-   \frac{
-     S \vdashexternaddr \XAFUNC~\funcaddr : \XTFUNC~\deftype
-     \qquad
-     \deftype \approx \TFUNC~[t_1^\ast] \Tarrow [t_2^\ast]
-   }{
-     S; C \vdashadmininstr \INVOKE~\funcaddr : [t_1^\ast] \to [t_2^\ast]
-   }
-
-
 .. index:: label, instruction, result type
 
 :math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast`

document/core/exec/instructions.rst

@@ -401,7 +401,7 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
    ~\\[-1ex]
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; \val^n~(\INVOKE~a) &\stepto& S'; \result
+   S; \val^n~(\REFFUNCADDR~a)~\CALLREF &\stepto& S'; \result
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -410,7 +410,7 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
      \wedge & (S'; \result) \in \X{hf}(S; \val^n) \\
      \end{array} \\
    \begin{array}{lcl@{\qquad}l}
-   S; \val^n~(\INVOKE~a) &\stepto& S; \val^n~(\INVOKE~a)
+   S; \val^n~(\REFFUNCADDR~a)~\CALLREF &\stepto& S; \val^n~(\REFFUNCADDR~a)~\CALLREF
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}

document/core/exec/modules.rst

@@ -220,8 +220,6 @@ $${definition: rundata_ runelem_}
 Invocation
 ~~~~~~~~~~
 
-$${definition-prose: invoke}
-
 Once a :ref:`module <syntax-module>` has been :ref:`instantiated <exec-instantiation>`, any exported function can be *invoked* externally via its :ref:`function address <syntax-funcaddr>` ${:funcaddr} in the :ref:`store <syntax-store>` ${:s} and an appropriate list ${:val*} of argument :ref:`values <syntax-val>`.
 
 Invocation may *fail* with an error if the arguments do not fit the :ref:`function type <syntax-functype>`.
@@ -231,42 +229,6 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 .. note::
    If the :ref:`embedder <embedder>` API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps or exceptions can occur.
 
-The following steps are performed:
-
-1. Assert: :math:`S.\SFUNCS[\funcaddr]` exists.
-
-2. Let :math:`\funcinst` be the :ref:`function instance <syntax-funcinst>` :math:`S.\SFUNCS[\funcaddr]`.
-
-3. Let :math:`\TFUNC~[t_1^n] \Tarrow [t_2^m]` be the :ref:`composite type <syntax-comptype>` :math:`\expanddt(\funcinst.\FITYPE)`.
-
-4. If the length :math:`|\val^\ast|` of the provided argument values is different from the number :math:`n` of expected arguments, then:
-
-   a. Fail.
-
-5. For each :ref:`value type <syntax-valtype>` :math:`t_i` in :math:`t_1^n` and corresponding :ref:`value <syntax-val>` :math:`val_i` in :math:`\val^\ast`, do:
-
-   a. If :math:`\val_i` is not :ref:`valid <valid-val>` with value type :math:`t_i`, then:
-
-      i. Fail.
-
-6. Let :math:`F` be the dummy :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~\{\}, \ALOCALS~\epsilon \}`.
-
-7. Push the frame :math:`F` to the stack.
-
-8. Push the values :math:`\val^\ast` to the stack.
-
-9. :ref:`Invoke <exec-invoke>` the function instance at address :math:`\funcaddr`.
-
-Once the function has returned, the following steps are executed:
-
-1. Assert: due to :ref:`validation <valid-func>`, :math:`m` :ref:`values <syntax-val>` are on the top of the stack.
-
-2. Pop :math:`\val_{\F{res}}^m` from the stack.
-
-3. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
-
-4. Pop the frame :math:`F` from the stack.
-
-The values ${:val_RES^m} are returned as the results of the invocation.
+$${definition-prose: invoke}
 
 $${definition: invoke}

document/core/exec/numerics.rst

@@ -592,7 +592,7 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
 
 .. math::
    \begin{array}{@{}lcll}
-   \inez_N(i) &=& \tobool(i =/= 0)
+   \inez_N(i) &=& \tobool(i \neq 0)
    \end{array}
 
 

document/core/exec/runtime.rst

@@ -378,7 +378,7 @@ It is an invariant of the semantics that all elements of a segment have a type :
 Data Instances
 ~~~~~~~~~~~~~~
 
-An *data instance* is the runtime representation of a :ref:`data segment <syntax-data>`.
+A *data instance* is the runtime representation of a :ref:`data segment <syntax-data>`.
 It holds a list of :ref:`bytes <syntax-byte>`.
 
 $${syntax: datainst}

document/core/exec/types.rst

@@ -10,7 +10,7 @@ It is an invariant of the semantics that all types occurring during execution ar
 
 .. note::
    Runtime type checks generally involve types from multiple modules or types not defined by a module at all,
-   such that any module-local :ref:`type indices <syntax-typeidx>` occurring inside them would not geenrally be meaningful.
+   such that any module-local :ref:`type indices <syntax-typeidx>` occurring inside them would not generally be meaningful.
 
 
 

document/core/syntax/instructions.rst

@@ -196,7 +196,7 @@ Instructions in this group are concerned with linear :ref:`memory <syntax-mem>`.
 
 $${syntax: memarg loadop_ storeop_ vloadop_ {instr/memory instr/data}}
 
-Memory is accessed with ${:LOAD} and ${:STORE} instructions for the different :ref:`number types <syntax-numtype>` and `vector types <syntax-vectype>`.
+Memory is accessed with ${:LOAD} and ${:STORE} instructions for the different :ref:`number types <syntax-numtype>` and :ref:`vector types <syntax-vectype>`.
 They all take a :ref:`memory index <syntax-memidx>` and a *memory argument* ${:memarg} that contains an address *offset* and the expected *alignment* (expressed as the exponent of a power of 2).
 
 Integer loads and stores can optionally specify a *storage size* ${:sz} that is smaller than the :ref:`bit width <syntax-numtype>` of the respective value type.
@@ -213,8 +213,8 @@ The ${:MEMORY.SIZE} instruction returns the current size of a memory.
 The ${:MEMORY.GROW} instruction grows a memory by a given delta and returns the previous size, or ${:$(-1)} if enough memory cannot be allocated.
 Both instructions operate in units of :ref:`page size <page-size>`.
 
-The ${:MEMORY.FILL} instruction sets all values in a regionof a memory to a given byte.
-The ${:MEMORY.COPY} instruction copies data from a source memory region to a possibly overlapping destination region in another or the same memory; the first index denotes the destination
+The ${:MEMORY.FILL} instruction sets all values in a region of memory to a given byte.
+The ${:MEMORY.COPY} instruction copies data from a source memory region to a possibly overlapping destination region in another or the same memory; the first index denotes the destination.
 The ${:MEMORY.INIT} instruction copies data from a :ref:`passive data segment <syntax-data>` into a memory.
 
 The ${:DATA.DROP} instruction prevents further use of a passive data segment. This instruction is intended to be used as an optimization hint. After a data segment is dropped its data can no longer be retrieved, so the memory used by this segment may be freed.
@@ -339,9 +339,9 @@ For each type, several subcategories can be distinguished:
 
 * *Constants*: return a static constant.
 
-* *Unary Operations*: consume one operand and produce one result of the respective type.
+* *Unary operations*: consume one operand and produce one result of the respective type.
 
-* *Binary Operations*: consume two operands and produce one result of the respective type.
+* *Binary operations*: consume two operands and produce one result of the respective type.
 
 * *Tests*: consume one operand of the respective type and produce a Boolean integer result.
 

document/core/syntax/types.rst

@@ -302,6 +302,8 @@ $${definition-ignore: psize}
 
 * The auxiliary function :math:`\unpack` maps a storage type to the :ref:`value type <syntax-valtype>` obtained when accessing a field:
 
+$${definition: unpack}
+
 
 .. index:: ! recursive type, ! sub type, composite type, ! final, subtyping, ! roll, ! unroll, recursive type index
    pair: abstract syntax; recursive type

document/core/syntax/values.rst

@@ -125,7 +125,7 @@ Conventions
 
 * The meta variable ${:z} ranges over floating-point values where clear from context.
 
-* Where clear from context, shorthands like ${:+1} denote floating point values like ${f64: POS $($(NORM 1 0))}.
+* Where clear from context, shorthands like ${:+1} denote floating point values like ${f64: POS $($(NORM 0 0))}.
 
 
 .. index:: ! numeric vector, integer, floating-point, lane, SIMD

document/core/text/conventions.rst

@@ -112,6 +112,10 @@ which were denoted by the corresponding :ref:`identifiers <text-id>`.
 Unnamed indices are associated with empty (${:eps}) entries in these lists.
 Fields have *dependent* name spaces, and hence a separate list of field identifiers per type.
 
+In addition, the field ${:TYPEDEFS} records the :ref:`defined type <syntax-deftype>` associated with each :ref:`type index <syntax-typeidx>`.
+They are needed to look up the number of parameters of :ref:`function types <syntax-functype>` when used in a :ref:`function definition <text-func>`,
+in order to produce the correct indices for :ref:`locals <syntax-local>`.
+
 An identifier context is *well-formed* if no index space contains duplicate identifiers.
 For fields, names need only be unique within a single type.