Merge pull request #54 from dhil/merge

Merge with upstreams

.github/workflows/ci-interpreter.yml

@@ -2,11 +2,11 @@ name: CI for interpreter & tests
 
 on:
   push:
-    branches: [ main ]
+    branches: [ main, wasm-3.0 ]
     paths: [ .github/**, interpreter/**, test/** ]
 
   pull_request:
-    branches: [ main ]
+    branches: [ main, wasm-3.0 ]
     paths: [ .github/**, interpreter/**, test/** ]
 
   # Allows you to run this workflow manually from the Actions tab

.github/workflows/ci-spec.yml

@@ -2,11 +2,11 @@ name: CI for specs
 
 on:
   push:
-    branches: [ main ]
+    branches: [ main, wasm-3.0 ]
     paths: [ .github/**, document/** ]
 
   pull_request:
-    branches: [ main ]
+    branches: [ main, wasm-3.0 ]
     paths: [ .github/**, document/** ]
 
   # Allows you to run this workflow manually from the Actions tab

.github/workflows/w3c-publish.yml

@@ -15,6 +15,10 @@ on:
   # Candidate Recommendation Snapshot).
   workflow_dispatch:
     inputs:
+      dry-run:
+        required: true
+        type: boolean
+        description: If set, Echidna will validate but not publish.
       w3c-status:
         required: true
         type: choice
@@ -60,7 +64,9 @@ 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 }}
-          ECHIDNA_DRYRUN: ${{ !(github.event_name == 'push' && github.repository == 'WebAssembly/spec' && github.ref == 'refs/heads/main') }}
+          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
         if: env.W3C_USERNAME
         run: cd document && make -e -C ${{ matrix.spec }} WD-echidna

README.md

@@ -1,35 +1,13 @@
+[![CI for specs](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-spec.yml/badge.svg)](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-spec.yml)
+[![CI for interpreter & tests](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-interpreter.yml/badge.svg)](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-interpreter.yml)
+
 # Stack-Switching Proposal for WebAssembly
 
 This repository is a clone of [`WebAssembly/spec`](https://github.com/WebAssembly/spec/). It is meant for discussion, prototype specification, and implementation of a proposal to add
 support for stack-switching.
 
 See the [explainer](proposals/stack-switching/Explainer.md) for a high-level summary of the proposal.
 
-## Previous proposals
-
-The current explainer represents the unification of two previous proposals: Typed Continuations (wasmfx) and Bag of Stacks (bos). (The explainers have now been unified. Once the reference interpreter and examples are adapted for the unified proposal this section will be removed from the README.)
-
-#### Typed Continuations
-
-* See the [explainer](proposals/continuations/Explainer.md) for a high-level summary of the proposal.
-
-* See the [overview](proposals/continuations/Overview.md) for a more formal description of the proposal.
-
-* An [implementation](https://github.com/WebAssembly/stack-switching/tree/wasmfx) is available as an extension to the reference interpreter. It is accesible from the `wasmfx` branch of this repository.
-
-* See the [examples](proposals/continuations/examples) for Wasm code for implementing various different features including lightweight threads, actors, and async/await.
-
-#### Bag of Stacks Proposal
-
-* See the [explainer](proposals/bag-o-stacks/Explainer.md) for a high-level summary of the proposal.
-
-Original README from upstream repository follows.
-
---------------------------------------------------------------------------------
-
-[![CI for specs](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-spec.yml/badge.svg)](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-spec.yml)
-[![CI for interpreter & tests](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-interpreter.yml/badge.svg)](https://github.com/WebAssembly/stack-switching/actions/workflows/ci-interpreter.yml)
-
 # spec
 
 This repository holds the sources for the WebAssembly specification,

document/core/appendix/changes.rst

@@ -308,7 +308,7 @@ Allowed basic numeric computations in constant expressions. [#proposal-extconst]
   - |GLOBALGET| for any previously declared immutable :ref:`global <syntax-global>`
 
 .. note::
-   The :ref:`garbage collection <extension-gc>` added further constant instructions.
+   The :ref:`garbage collection <extension-gc>` extension added further constant instructions.
 
 
 .. index:: instruction, function, call
@@ -389,6 +389,44 @@ Added the ability to use multiple memories per module. [#proposal-multimem]_
 * :ref:`Data segments <syntax-elem>` take a :ref:`memory index <syntax-memidx>`
 
 
+.. index:: address type, number type, table, memory, instruction
+
+64-bit Address Space
+....................
+
+Added the ability to declare an :math:`\I64` :ref:`address type <syntax-addrtype>` for :ref:`tables <syntax-tabletype>` and :ref:`memories <syntax-memtype>`. [#proposal-addr64]_
+
+* :ref:`Address types <syntax-addrtype>` denote a subset of the integral :ref:`number types <syntax-numtype>`
+
+* :ref:`Table types <syntax-tabletype>` include an :ref:`address type <syntax-addrtype>`
+
+* :ref:`Memory types <syntax-memtype>` include an :ref:`address type <syntax-addrtype>`
+
+* Operand types of :ref:`table <syntax-instr-table>` and :ref:`memory <syntax-instr-memory>` instructions now depend on the subject's declared address type:
+
+  - |TABLEGET|
+  - |TABLESET|
+  - |TABLESIZE|
+  - |TABLEGROW|
+  - |TABLEFILL|
+  - |TABLECOPY|
+  - |TABLEINIT|
+  - |MEMORYSIZE|
+  - |MEMORYGROW|
+  - |MEMORYFILL|
+  - |MEMORYCOPY|
+  - |MEMORYINIT|
+  - :math:`t\K{.load}`
+  - :math:`t\K{.store}`
+  - :math:`t\K{.load}\!N\!\K{\_}\sx`
+  - :math:`t\K{.store}\!N`
+  - :math:`\K{v128.load}\!N\!\K{x}\!M\!\K{\_}\sx`
+  - :math:`\K{v128.load}\!N\!\K{\_zero}`
+  - :math:`\K{v128.load}\!N\!\K{\_splat}`
+  - :math:`\K{v128.load}\!N\!\K{\_lane}`
+  - :math:`\K{v128.store}\!N\!\K{\_lane}`
+
+
 .. index:: reference, reference type, heap type, value type, local, local type, instruction, instruction type, table, function, function type, matching, subtyping
 
 Typeful References
@@ -584,7 +622,7 @@ mirroring the role of custom sections in the binary format. [#proposal-annot]_
 
 
 .. [#proposal-extconst]
-   https://github.com/WebAssembly/spec/blob/main/proposals/extended-const/
+   https://github.com/WebAssembly/spec/tree/main/proposals/extended-const/
 
 .. [#proposal-tailcall]
    https://github.com/WebAssembly/spec/tree/main/proposals/tail-call/
@@ -593,7 +631,10 @@ mirroring the role of custom sections in the binary format. [#proposal-annot]_
    https://github.com/WebAssembly/spec/tree/main/proposals/exception-handling/
 
 .. [#proposal-multimem]
-   https://github.com/WebAssembly/spec/blob/main/proposals/multi-memory/
+   https://github.com/WebAssembly/spec/tree/main/proposals/multi-memory/
+
+.. [#proposal-addr64]
+   https://github.com/WebAssembly/spec/tree/main/proposals/memory64/
 
 .. [#proposal-typedref]
    https://github.com/WebAssembly/spec/tree/main/proposals/function-references/

document/core/appendix/embedding.rst

@@ -21,7 +21,7 @@ Types
 In the description of the embedder interface, syntactic classes from the :ref:`abstract syntax <syntax>` and the :ref:`runtime's abstract machine <syntax-runtime>` are used as names for variables that range over the possible objects from that class.
 Hence, these syntactic classes can also be interpreted as types.
 
-For numeric parameters, notation like :math:`n:\u32` is used to specify a symbolic name in addition to the respective value range.
+For numeric parameters, notation like :math:`i:\u64` is used to specify a symbolic name in addition to the respective value range.
 
 
 .. _embed-bool:
@@ -165,7 +165,7 @@ Modules
 .. _embed-module-instantiate:
 
 :math:`\F{module\_instantiate}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \exception ~|~ \error)`
-....................................................................................................
+...................................................................................................................
 
 1. Try :ref:`instantiating <exec-instantiation>` :math:`\module` in :math:`\store` with :ref:`external values <syntax-externval>` :math:`\externval^\ast` as imports:
 
@@ -383,7 +383,7 @@ Tables
 
 .. _embed-table-read:
 
-:math:`\F{table\_read}(\store, \tableaddr, i:\u32) : \reff ~|~ \error`
+:math:`\F{table\_read}(\store, \tableaddr, i:\u64) : \reff ~|~ \error`
 ......................................................................
 
 1. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`.
@@ -401,7 +401,7 @@ Tables
 
 .. _embed-table-write:
 
-:math:`\F{table\_write}(\store, \tableaddr, i:\u32, \reff) : \store ~|~ \error`
+:math:`\F{table\_write}(\store, \tableaddr, i:\u64, \reff) : \store ~|~ \error`
 ...............................................................................
 
 1. Let :math:`\X{ti}` be the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]`.
@@ -421,7 +421,7 @@ Tables
 
 .. _embed-table-size:
 
-:math:`\F{table\_size}(\store, \tableaddr) : \u32`
+:math:`\F{table\_size}(\store, \tableaddr) : \u64`
 ..................................................
 
 1. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`.
@@ -437,7 +437,7 @@ Tables
 
 .. _embed-table-grow:
 
-:math:`\F{table\_grow}(\store, \tableaddr, n:\u32, \reff) : \store ~|~ \error`
+:math:`\F{table\_grow}(\store, \tableaddr, n:\u64, \reff) : \store ~|~ \error`
 ..............................................................................
 
 1. Try :ref:`growing <grow-table>` the :ref:`table instance <syntax-tableinst>` :math:`\store.\STABLES[\tableaddr]` by :math:`n` elements with initialization value :math:`\reff`:
@@ -495,7 +495,7 @@ Memories
 
 .. _embed-mem-read:
 
-:math:`\F{mem\_read}(\store, \memaddr, i:\u32) : \byte ~|~ \error`
+:math:`\F{mem\_read}(\store, \memaddr, i:\u64) : \byte ~|~ \error`
 ..................................................................
 
 1. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`.
@@ -513,12 +513,12 @@ Memories
 
 .. _embed-mem-write:
 
-:math:`\F{mem\_write}(\store, \memaddr, i:\u32, \byte) : \store ~|~ \error`
+:math:`\F{mem\_write}(\store, \memaddr, i:\u64, \byte) : \store ~|~ \error`
 ...........................................................................
 
 1. Let :math:`\X{mi}` be the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]`.
 
-2. If :math:`\u32` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`.
+2. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`.
 
 3. Replace :math:`\X{mi}.\MIDATA[i]` with :math:`\byte`.
 
@@ -533,7 +533,7 @@ Memories
 
 .. _embed-mem-size:
 
-:math:`\F{mem\_size}(\store, \memaddr) : \u32`
+:math:`\F{mem\_size}(\store, \memaddr) : \u64`
 ..............................................
 
 1. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size <page-size>`.
@@ -549,7 +549,7 @@ Memories
 
 .. _embed-mem-grow:
 
-:math:`\F{mem\_grow}(\store, \memaddr, n:\u32) : \store ~|~ \error`
+:math:`\F{mem\_grow}(\store, \memaddr, n:\u64) : \store ~|~ \error`
 ...................................................................
 
 1. Try :ref:`growing <grow-mem>` the :ref:`memory instance <syntax-meminst>` :math:`\store.\SMEMS[\memaddr]` by :math:`n` :ref:`pages <page-size>`:

document/core/appendix/properties.rst

@@ -513,10 +513,10 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 .. index:: table type, table instance, limits, function address
 .. _valid-tableinst:
 
-:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~(\limits~t), \TIELEM~\reff^\ast \}`
-...............................................................................................
+:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~\addrtype~\limits~t, \TIELEM~\reff^\ast \}`
+.......................................................................................................
 
-* The :ref:`table type <syntax-tabletype>` :math:`\limits~t` must be :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
+* The :ref:`table type <syntax-tabletype>` :math:`\addrtype~\limits~t` must be :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
 
 * The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`.
 
@@ -526,49 +526,49 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
   * The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.
 
-* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\limits~t`.
+* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\addrtype~\limits~t`.
 
 .. math::
    \frac{
-     \vdashtabletype \limits~t \ok
+     \vdashtabletype \addrtype~\limits~t \ok
      \qquad
      n = \limits.\LMIN
      \qquad
      (S \vdash \reff : t')^n
      \qquad
      (\vdashreftypematch t' \matchesvaltype t)^n
    }{
-     S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t
+     S \vdashtableinst \{ \TITYPE~\addrtype~\limits~t, \TIELEM~\reff^n \} : \addrtype~\limits~t
    }
 
 
 .. index:: memory type, memory instance, limits, byte
 .. _valid-meminst:
 
-:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}`
-......................................................................................
+:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\addrtype~\limits, \MIDATA~b^\ast \}`
+................................................................................................
 
-* The :ref:`memory type <syntax-memtype>` :math:`\limits` must be :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
+* The :ref:`memory type <syntax-memtype>` :math:`\addrtype~\limits` must be :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
 
 * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.
 
-* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\limits`.
+* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\addrtype~\limits`.
 
 .. math::
    \frac{
-     \vdashmemtype \limits \ok
+     \vdashmemtype \addrtype~\limits \ok
      \qquad
      n = \limits.\LMIN \cdot 64\,\F{Ki}
    }{
-     S \vdashmeminst \{ \MITYPE~\limits, \MIDATA~b^n \} : \limits
+     S \vdashmeminst \{ \MITYPE~\addrtype~\limits, \MIDATA~b^n \} : \addrtype~\limits
    }
 
 
 .. index:: global type, global instance, value, mutability
 .. _valid-globalinst:
 
-:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~(\mut~t), \GIVALUE~\val \}`
-.........................................................................................
+:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~\mut~t, \GIVALUE~\val \}`
+.......................................................................................
 
 * The :ref:`global type <syntax-globaltype>` :math:`\mut~t` must be :ref:`valid <valid-globaltype>` under the empty :ref:`context <context>`.
 
@@ -586,7 +586,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
      \qquad
      \vdashvaltypematch t' \matchesvaltype t
    }{
-     S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t
+     S \vdashglobalinst \{ \GITYPE~\mut~t, \GIVALUE~\val \} : \mut~t
    }
 
 

document/core/binary/instructions.rst

@@ -290,9 +290,9 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
 .. math::
    \begin{array}{llcllll}
    \production{memory argument} & \Bmemarg &::=&
-     a{:}\Bu32~~o{:}\Bu32 &\Rightarrow& 0~\{ \ALIGN~a,~\OFFSET~o \}
+     a{:}\Bu32~~o{:}\Bu64 &\Rightarrow& 0~\{ \ALIGN~a,~\OFFSET~o \}
        & (\iff a < 2^6) \\ &&|&
-     a{:}\Bu32~~x{:}\memidx~~o{:}\Bu32 &\Rightarrow& x~\{ \ALIGN~(a - 2^6),~\OFFSET~o \}
+     a{:}\Bu32~~x{:}\memidx~~o{:}\Bu64 &\Rightarrow& x~\{ \ALIGN~(a - 2^6),~\OFFSET~o \}
        & (\iff 2^6 \leq a < 2^7) \\
    \production{instruction} & \Binstr &::=& \dots \\ &&|&
      \hex{28}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD~m \\ &&|&

document/core/binary/types.rst

@@ -251,13 +251,15 @@ Additional shorthands are recognized for unary recursions and sub types without
 Limits
 ~~~~~~
 
-:ref:`Limits <syntax-limits>` are encoded with a preceding flag indicating whether a maximum is present.
+:ref:`Limits <syntax-limits>` are encoded with a preceding flag indicating whether a maximum is present, and a flag for the :ref:`address type <syntax-addrtype>`.
 
 .. math::
    \begin{array}{llclll}
    \production{limits} & \Blimits &::=&
-     \hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|&
-     \hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\
+     \hex{00}~~n{:}\Bu64 &\Rightarrow& (\I32, \{ \LMIN~n, \LMAX~\epsilon \}) \\ &&|&
+     \hex{01}~~n{:}\Bu64~~m{:}\Bu64 &\Rightarrow& (\I32, \{ \LMIN~n, \LMAX~m \}) \\ &&|&
+     \hex{04}~~n{:}\Bu64 &\Rightarrow& (\I64, \{ \LMIN~n, \LMAX~\epsilon \}) \\ &&|&
+     \hex{05}~~n{:}\Bu64~~m{:}\Bu64 &\Rightarrow& (\I64, \{ \LMIN~n, \LMAX~m \})
    \end{array}
 
 
@@ -273,7 +275,7 @@ Memory Types
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{memory type} & \Bmemtype &::=&
-     \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\
+     (\X{at},\X{lim}){:}\Blimits &\Rightarrow& \X{at}~\X{lim} \\
    \end{array}
 
 
@@ -289,7 +291,7 @@ Table Types
 .. math::
    \begin{array}{llclll}
    \production{table type} & \Btabletype &::=&
-     \X{et}{:}\Breftype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\
+     \X{et}{:}\Breftype~~(\X{at},\X{lim}){:}\Blimits &\Rightarrow& \X{at}~\X{lim}~\X{et} \\
    \end{array}