[spec] Update syntax spec for memory64

I updated `instructions.rst` and make a start on `types.rst` but could
use some help on how to parameterize `limits` on the index type.

document/core/binary/instructions.rst

@@ -278,7 +278,7 @@ 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 \}
        & (\iff 2^6 \leq a < 2^7) \\

document/core/binary/types.rst

@@ -249,13 +249,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 the corresponsing index type.
 
 .. 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}
 
 
@@ -271,7 +273,7 @@ Memory Types
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{memory type} & \Bmemtype &::=&
-     \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\
+     (\X{it}, \X{lim}){:}\Blimits &\Rightarrow& \X{it}~~\X{lim} \\
    \end{array}
 
 
@@ -287,7 +289,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{it}, \X{lim}){:}\Blimits &\Rightarrow& \X{it}~~\X{lim}~\X{et} \\
    \end{array}
 
 

document/core/exec/instructions.rst

@@ -3682,65 +3682,71 @@ Memory Instructions
 
 9. Let :math:`\X{mem}_s` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[\X{sa}]`.
 
-10. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+10. Let :math:`\X{it}_d~\limits` be the :math:`\X{mem}_d.\MITYPE`.
 
-11. Pop the value :math:`\I32.\CONST~n` from the stack.
+11. Let :math:`\X{it}_s~\limits` be the :math:`\X{mem}_s.\MITYPE`.
 
-12. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+12. Let :math:`\X{it}_{min}` be ....?
 
-13. Pop the value :math:`\I32.\CONST~s` from the stack.
+13. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` :math:`\X{it}_{min}` is on the top of the stack.
 
-14. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+14. Pop the value :math:`\X{it}_{min}.\CONST~n` from the stack.
 
-15. Pop the value :math:`\I32.\CONST~d` from the stack.
+15. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` :math:`\X{it}_s` is on the top of the stack.
+
+16. Pop the value :math:`\X{it}_s.\CONST~s` from the stack.
+
+17. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` :math:`\X{it}_d` is on the top of the stack.
 
-16. If :math:`s + n` is larger than the length of :math:`\X{mem}_s.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}_d.\MIDATA`, then:
+18. Pop the value :math:`\X{it}_d.\CONST~d` from the stack.
+
+19. If :math:`s + n` is larger than the length of :math:`\X{mem}_s.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}_d.\MIDATA`, then:
 
     a. Trap.
 
-17. If :math:`n = 0`, then:
+20. If :math:`n = 0`, then:
 
    a. Return.
 
-18. If :math:`d \leq s`, then:
+21. If :math:`d \leq s`, then:
 
-   a. Push the value :math:`\I32.\CONST~d` to the stack.
+   a. Push the value :math:`\X{it}.\CONST~d` to the stack.
 
-   b. Push the value :math:`\I32.\CONST~s` to the stack.
+   b. Push the value :math:`\X{it}.\CONST~s` to the stack.
 
    c. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`.
 
    d. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`.
 
    e. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`.
 
-   f. Push the value :math:`\I32.\CONST~(d+1)` to the stack.
+   f. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack.
 
    g. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`.
 
-   h. Push the value :math:`\I32.\CONST~(s+1)` to the stack.
+   h. Push the value :math:`\X{it}.\CONST~(s+1)` to the stack.
 
-19. Else:
+22. Else:
 
    a. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`.
 
-   b. Push the value :math:`\I32.\CONST~(d+n-1)` to the stack.
+   b. Push the value :math:`\X{it}.\CONST~(d+n-1)` to the stack.
 
    c. Assert: due to the earlier check against the memory size, :math:`s+n-1 < 2^{32}`.
 
-   d. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack.
+   d. Push the value :math:`\X{it}.\CONST~(s+n-1)` to the stack.
 
    e. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`.
 
    f. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`.
 
-   g. Push the value :math:`\I32.\CONST~d` to the stack.
+   g. Push the value :math:`\X{it}.\CONST~d` to the stack.
 
-   h. Push the value :math:`\I32.\CONST~s` to the stack.
+   h. Push the value :math:`\X{it}.\CONST~s` to the stack.
 
-20. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
+23. Push the value :math:`\X{it}_{min}.\CONST~(n-1)` to the stack.
 
-21. Execute the instruction :math:`\MEMORYCOPY~x~y`.
+24. Execute the instruction :math:`\MEMORYCOPY~x~y`.
 
 .. math::
    ~\\[-1ex]

document/core/syntax/instructions.rst

@@ -650,7 +650,7 @@ Instructions in this group are concerned with linear :ref:`memory <syntax-mem>`.
 .. math::
    \begin{array}{llrl}
    \production{memory immediate} & \memarg &::=&
-     \{ \OFFSET~\u32, \ALIGN~\u32 \} \\
+     \{ \OFFSET~\u64, \ALIGN~\u32 \} \\
    \production{lane width} & \X{ww} &::=&
      8 ~|~ 16 ~|~ 32 ~|~ 64 \\
    \production{instruction} & \instr &::=&
@@ -696,9 +696,6 @@ The static address offset is added to the dynamic address operand, yielding a 33
 All values are read and written in |LittleEndian|_ byte order.
 A :ref:`trap <trap>` results if any of the accessed memory bytes lies outside the address range implied by the memory's current size.
 
-.. note::
-   Future versions of WebAssembly might provide memory instructions with 64 bit address ranges.
-
 The |MEMORYSIZE| instruction returns the current size of a memory.
 The |MEMORYGROW| instruction grows a memory by a given delta and returns the previous size, or :math:`-1` if enough memory cannot be allocated.
 Both instructions operate in units of :ref:`page size <page-size>`.

document/core/syntax/types.rst

@@ -349,6 +349,25 @@ In a :ref:`module <syntax-module>`, each member of a recursive type is assigned
 The syntax of sub types is :ref:`generalized <syntax-heaptype-ext>` for the purpose of specifying :ref:`validation <valid>` and :ref:`execution <exec>`.
 
 
+.. _index:: ! index type
+   pair: abstract syntax; index type
+   single: memory; index type
+   single: table; index type
+.. _syntax-idxtype:
+
+Index Type
+~~~~~~~~~~
+
+*Index types* classify the values that can be used to index into
+:ref:`memories <syntax-mem>` and :ref:`tables <syntax-table>`.
+
+.. math::
+   \begin{array}{llll}
+   \production{index type} & \idxtype &::=&
+     \I32 ~|~ \I64 \\
+   \end{array}
+
+
 .. index:: ! limits, memory type, table type
    pair: abstract syntax; limits
    single: memory; limits
@@ -363,7 +382,7 @@ Limits
 .. math::
    \begin{array}{llrl}
    \production{limits} & \limits &::=&
-     \{ \LMIN~\u32, \LMAX~\u32^? \} \\
+     \{ \LMIN~\u64, \LMAX~\u64^? \} \\
    \end{array}
 
 If no maximum is given, the respective storage can grow to any size.
@@ -383,7 +402,7 @@ Memory Types
 .. math::
    \begin{array}{llrl}
    \production{memory type} & \memtype &::=&
-     \limits \\
+     ~\idxtype~\limits \\
    \end{array}
 
 The limits constrain the minimum and optionally the maximum size of a memory.
@@ -404,7 +423,7 @@ Table Types
 .. math::
    \begin{array}{llrl}
    \production{table type} & \tabletype &::=&
-     \limits~\reftype \\
+     ~\idxtype~\limits ~\reftype \\
    \end{array}
 
 Like memories, tables are constrained by limits for their minimum and optionally maximum size.

document/core/text/modules.rst

@@ -365,11 +365,13 @@ A :ref:`data segment <text-data>` can be given inline with a memory definition,
 .. math::
    \begin{array}{llclll}
    \production{module field} &
-     \text{(}~\text{memory}~~\Tid^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad
-       \text{(}~\text{memory}~~\Tid'~~m~~m~\text{)} \\ & \qquad
-       \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)}
+     \text{(}~\text{memory}~~\Tid^?~~\X{it}^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad
+       \text{(}~\text{memory}~~\Tid'~~\X{it}^?~~m~~m~\text{)} \\ & \qquad
+       \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{it}'~\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)}
        \\ & \qquad\qquad
-       (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, m = \F{ceil}(n / 64\,\F{Ki})) \\
+       (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad
+        \iff it^? \neq \epsilon \wedge \X{it}' = \X{it}^? \vee \X{it}^? = \epsilon \wedge \X{it}' = \text{i32}, \\ & \qquad\qquad
+        m = \F{ceil}(n / 64\,\F{Ki})), \\
    \end{array}
 
 Memories can be defined as :ref:`imports <text-import>` or :ref:`exports <text-export>` inline:

document/core/text/types.rst

@@ -282,6 +282,32 @@ Similarly, final sub types with no super-types can omit the |Tsub| keyword and a
    \end{array}
 
 
+.. index:: index type
+   pair: text format; index type
+.. _text-idxtype:
+
+Index Type
+~~~~~~~~~~
+
+.. math::
+   \begin{array}{llclll}
+   \production{index type} & \Tidxtype &::=&
+     \text{i32} &\Rightarrow& \I32 \\ &&|&
+     \text{i64} &\Rightarrow& \I64 \\
+   \end{array}
+
+Abbreviations
+.............
+
+The index type can be omited, in which case it defaults :math:`\I32`:
+
+.. math::
+   \begin{array}{llclll}
+   \production{index type} &
+     \text{} &\equiv& \text{i32}
+   \end{array}
+
+
 .. index:: limits
    pair: text format; limits
 .. _text-limits:
@@ -307,7 +333,7 @@ Memory Types
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{memory type} & \Tmemtype_I &::=&
-     \X{lim}{:}\Tlimits &\Rightarrow& \X{lim} \\
+     \X{it}{:}\Tidxtype~~\X{lim}{:}\Tlimits &\Rightarrow& \X{it}~\X{lim} \\
    \end{array}
 
 
@@ -321,7 +347,7 @@ Table Types
 .. math::
    \begin{array}{llclll}
    \production{table type} & \Ttabletype_I &::=&
-     \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{lim}~\X{et} \\
+     \X{it}{:}\Tidxtype~~\X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{it}~\X{lim}~\X{et} \\
    \end{array}
 
 

document/core/util/macros.def

@@ -269,6 +269,7 @@
 
 .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
 .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
+.. |idxtype| mathdef:: \xref{syntax/types}{syntax-idxtype}{\X{idxtype}}
 .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
 
 .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
@@ -913,6 +914,7 @@
 
 .. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}}
 .. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}}
+.. |Tidxtype| mathdef:: \xref{text/types}{text-idxtype}{\T{idxtype}}
 .. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}}
 .. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}}
 

document/core/valid/instructions.rst

@@ -1753,15 +1753,17 @@ Memory Instructions
 
 * The memory :math:`C.\CMEMS[y]` must be defined in the context.
 
-* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
+* Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[0]`.
+
+* Then the instruction is valid with type :math:`[it~it~it] \to []`.
 
 .. math::
    \frac{
-     C.\CMEMS[x] = \memtype
+     C.\CMEMS[x] = \X{it1}~\limits1
      \qquad
-     C.\CMEMS[x] = \memtype
+     C.\CMEMS[y] = \X{it2}~\limits2
    }{
-     C \vdashinstr \MEMORYCOPY~x~y : [\I32~\I32~\I32] \to []
+     C \vdashinstr \MEMORYCOPY~x~y : [\X{it}~\X{it}~\X{it}] \to []
    }