Merge with WebAssembly/spec wasm-3.0 branch

Author: dhil

.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

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}