Update embedding and execution specs for memory64 (WebAssembly#74)

* Convert table and memory instance storage to sequences

Vectors in the spec are syntactically limited to a maximum size of 2^32.
This is incompatible with memory64, so the storage has been changed to
use sequences instead of vectors. The execution semantics are
unaffected.

* Update memory/table validation/execution/embedding to u64

Memory and table operations in the embedding section have been updated
to use u64 instead of u32, reflecting the changes to `limits`. Various
operations in the execution section were also updated to reflect
`idxtype`'s inclusion in `memtype` and `tabletype`, as well as the
supporting validation rules.

Author: bvisness

document/core/appendix/embedding.rst

@@ -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/exec/modules.rst

@@ -94,11 +94,11 @@ are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the fo
 
 1. Let :math:`\tabletype` be the :ref:`table type <syntax-tabletype>` of the table to allocate and :math:`\reff` the initialization value.
 
-2. Let :math:`(\{\LMIN~n, \LMAX~m^?\}~\reftype)` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tabletype`.
+2. Let :math:`(\idxtype~\{\LMIN~n, \LMAX~m^?\}~\reftype)` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tabletype`.
 
 3. Let :math:`a` be the first free :ref:`table address <syntax-tableaddr>` in :math:`S`.
 
-4. Let :math:`\tableinst` be the :ref:`table instance <syntax-tableinst>` :math:`\{ \TITYPE~\tabletype', \TIELEM~\reff^n \}` with :math:`n` elements set to :math:`\reff`.
+4. Let :math:`\tableinst` be the :ref:`table instance <syntax-tableinst>` :math:`\{ \TITYPE~\tabletype, \TIELEM~\reff^n \}` with :math:`n` elements set to :math:`\reff`.
 
 5. Append :math:`\tableinst` to the |STABLES| of :math:`S`.
 
@@ -108,7 +108,7 @@ are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the fo
    \begin{array}{rlll}
    \alloctable(S, \tabletype, \reff) &=& S', \tableaddr \\[1ex]
    \mbox{where:} \hfill \\
-   \tabletype &=& \{\LMIN~n, \LMAX~m^?\}~\reftype \\
+   \tabletype &=& \idxtype~\{\LMIN~n, \LMAX~m^?\}~\reftype \\
    \tableaddr &=& |S.\STABLES| \\
    \tableinst &=& \{ \TITYPE~\tabletype, \TIELEM~\reff^n \} \\
    S' &=& S \compose \{\STABLES~\tableinst\} \\
@@ -123,7 +123,7 @@ are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the fo
 
 1. Let :math:`\memtype` be the :ref:`memory type <syntax-memtype>` of the memory to allocate.
 
-2. Let :math:`\{\LMIN~n, \LMAX~m^?\}` be the structure of :ref:`memory type <syntax-memtype>` :math:`\memtype`.
+2. Let :math:`(\idxtype~\{\LMIN~n, \LMAX~m^?\})` be the structure of :ref:`memory type <syntax-memtype>` :math:`\memtype`.
 
 3. Let :math:`a` be the first free :ref:`memory address <syntax-memaddr>` in :math:`S`.
 
@@ -137,7 +137,7 @@ are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the fo
    \begin{array}{rlll}
    \allocmem(S, \memtype) &=& S', \memaddr \\[1ex]
    \mbox{where:} \hfill \\
-   \memtype &=& \{\LMIN~n, \LMAX~m^?\} \\
+   \memtype &=& \idxtype~\{\LMIN~n, \LMAX~m^?\} \\
    \memaddr &=& |S.\SMEMS| \\
    \meminst &=& \{ \MITYPE~\memtype, \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \} \\
    S' &=& S \compose \{\SMEMS~\meminst\} \\
@@ -284,28 +284,25 @@ Growing :ref:`tables <syntax-tableinst>`
 
 2. Let :math:`\X{len}` be :math:`n` added to the length of :math:`\tableinst.\TIELEM`.
 
-3. If :math:`\X{len}` is larger than or equal to :math:`2^{32}`, then fail.
+3. Let :math:`(\idxtype~\limits~\reftype)` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tableinst.\TITYPE`.
 
-4. Let :math:`\limits~t` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tableinst.\TITYPE`.
+4. Let :math:`\limits'` be :math:`\limits` with :math:`\LMIN` updated to :math:`\X{len}`.
 
-5. Let :math:`\limits'` be :math:`\limits` with :math:`\LMIN` updated to :math:`\X{len}`.
-
-6. If :math:`\limits'` is not :ref:`valid <valid-limits>`, then fail.
+5. If the :ref:`table type <syntax-tabletype>` :math:`(\idxtype~\limits'~\reftype)` is not :ref:`valid <valid-tabletype>`, then fail.
 
-7. Append :math:`\reff^n` to :math:`\tableinst.\TIELEM`.
+6. Append :math:`\reff^n` to :math:`\tableinst.\TIELEM`.
 
-8. Set :math:`\tableinst.\TITYPE` to the :ref:`table type <syntax-tabletype>` :math:`\limits'~t`.
+7. Set :math:`\tableinst.\TITYPE` to the :ref:`table type <syntax-tabletype>` :math:`(\idxtype~\limits'~\reftype)`.
 
 .. math::
    \begin{array}{rllll}
-   \growtable(\tableinst, n, \reff) &=& \tableinst \with \TITYPE = \limits'~t \with \TIELEM = \tableinst.\TIELEM~\reff^n \\
+   \growtable(\tableinst, n, \reff) &=& \tableinst \with \TITYPE = \idxtype~\limits'~\reftype \with \TIELEM = \tableinst.\TIELEM~\reff^n \\
      && (
        \begin{array}[t]{@{}r@{~}l@{}}
        \iff & \X{len} = n + |\tableinst.\TIELEM| \\
-       \wedge & \X{len} < 2^{32} \\
-       \wedge & \limits~t = \tableinst.\TITYPE \\
+       \wedge & \idxtype~\limits~\reftype = \tableinst.\TITYPE \\
        \wedge & \limits' = \limits \with \LMIN = \X{len} \\
-       \wedge & \vdashlimits \limits' \ok) \\
+       \wedge & \vdashtabletype \idxtype~\limits'~\reftype \ok) \\
        \end{array} \\
    \end{array}
 
@@ -322,28 +319,25 @@ Growing :ref:`memories <syntax-meminst>`
 
 3. Let :math:`\X{len}` be :math:`n` added to the length of :math:`\meminst.\MIDATA` divided by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.
 
-4. If :math:`\X{len}` is larger than :math:`2^{16}`, then fail.
+4. Let :math:`(\idxtype~\limits)` be the structure of :ref:`memory type <syntax-memtype>` :math:`\meminst.\MITYPE`.
 
-5. Let :math:`\limits` be the structure of :ref:`memory type <syntax-memtype>` :math:`\meminst.\MITYPE`.
-
-6. Let :math:`\limits'` be :math:`\limits` with :math:`\LMIN` updated to :math:`\X{len}`.
+5. Let :math:`\limits'` be :math:`\limits` with :math:`\LMIN` updated to :math:`\X{len}`.
 
-7. If :math:`\limits'` is not :ref:`valid <valid-limits>`, then fail.
+6. If the :ref:`memory type <syntax-memtype>` :math:`(\idxtype~\limits')` is not :ref:`valid <valid-memtype>`, then fail.
 
-8. Append :math:`n` times :math:`64\,\F{Ki}` :ref:`bytes <syntax-byte>` with value :math:`\hex{00}` to :math:`\meminst.\MIDATA`.
+7. Append :math:`n` times :math:`64\,\F{Ki}` :ref:`bytes <syntax-byte>` with value :math:`\hex{00}` to :math:`\meminst.\MIDATA`.
 
-9. Set :math:`\meminst.\MITYPE` to the :ref:`memory type <syntax-memtype>` :math:`\limits'`.
+8. Set :math:`\meminst.\MITYPE` to the :ref:`memory type <syntax-memtype>` :math:`(\idxtype~\limits')`.
 
 .. math::
    \begin{array}{rllll}
-   \growmem(\meminst, n) &=& \meminst \with \MITYPE = \limits' \with \MIDATA = \meminst.\MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \\
+   \growmem(\meminst, n) &=& \meminst \with \MITYPE = \idxtype~\limits' \with \MIDATA = \meminst.\MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \\
      && (
        \begin{array}[t]{@{}r@{~}l@{}}
        \iff & \X{len} = n + |\meminst.\MIDATA| / 64\,\F{Ki} \\
-       \wedge & \X{len} \leq 2^{16} \\
-       \wedge & \limits = \meminst.\MITYPE \\
+       \wedge & \idxtype~\limits = \meminst.\MITYPE \\
        \wedge & \limits' = \limits \with \LMIN = \X{len} \\
-       \wedge & \vdashlimits \limits' \ok) \\
+       \wedge & \vdashmemtype \idxtype~\limits' \ok) \\
        \end{array} \\
    \end{array}
 

document/core/exec/runtime.rst

@@ -356,18 +356,18 @@ Table Instances
 ~~~~~~~~~~~~~~~
 
 A *table instance* is the runtime representation of a :ref:`table <syntax-table>`.
-It records its :ref:`type <syntax-tabletype>` and holds a vector of :ref:`reference values <syntax-ref>`.
+It records its :ref:`type <syntax-tabletype>` and holds a sequence of :ref:`reference values <syntax-ref>`.
 
 .. math::
    \begin{array}{llll}
    \production{table instance} & \tableinst &::=&
-     \{ \TITYPE~\tabletype, \TIELEM~\vec(\reff) \} \\
+     \{ \TITYPE~\tabletype, \TIELEM~\reff^\ast \} \\
    \end{array}
 
 Table elements can be mutated through :ref:`table instructions <syntax-instr-table>`, the execution of an active :ref:`element segment <syntax-elem>`, or by external means provided by the :ref:`embedder <embedder>`.
 
 It is an invariant of the semantics that all table elements have a type :ref:`matching <match-reftype>` the element type of :math:`\tabletype`.
-It also is an invariant that the length of the element vector never exceeds the maximum size of :math:`\tabletype`, if present.
+It also is an invariant that the length of the element sequence never exceeds the maximum size of :math:`\tabletype`, if present.
 
 
 .. index:: ! memory instance, memory, byte, ! page size, memory type, embedder, data segment, instruction
@@ -380,15 +380,15 @@ Memory Instances
 ~~~~~~~~~~~~~~~~
 
 A *memory instance* is the runtime representation of a linear :ref:`memory <syntax-mem>`.
-It records its :ref:`type <syntax-memtype>` and holds a vector of :ref:`bytes <syntax-byte>`.
+It records its :ref:`type <syntax-memtype>` and holds a sequence of :ref:`bytes <syntax-byte>`.
 
 .. math::
    \begin{array}{llll}
    \production{memory instance} & \meminst &::=&
-     \{ \MITYPE~\memtype, \MIDATA~\vec(\byte) \} \\
+     \{ \MITYPE~\memtype, \MIDATA~\byte^\ast \} \\
    \end{array}
 
-The length of the vector always is a multiple of the WebAssembly *page size*, which is defined to be the constant :math:`65536` -- abbreviated :math:`64\,\F{Ki}`.
+The length of the sequence always is a multiple of the WebAssembly *page size*, which is defined to be the constant :math:`65536` -- abbreviated :math:`64\,\F{Ki}`.
 
 The bytes can be mutated through :ref:`memory instructions <syntax-instr-memory>`, the execution of an active :ref:`data segment <syntax-data>`, or by external means provided by the :ref:`embedder <embedder>`.
 

document/core/valid/types.rst

@@ -501,22 +501,22 @@ Limits
 Table Types
 ~~~~~~~~~~~
 
-:math:`\limits~\reftype`
-........................
+:math:`\idxtype~\limits~\reftype`
+.................................
 
-* The limits :math:`\limits` must be :ref:`valid <valid-limits>` within range :math:`2^{32}-1`.
+* The limits :math:`\limits` must be :ref:`valid <valid-limits>` within range :math:`2^{|\idxtype|}-1`.
 
 * The reference type :math:`\reftype` must be :ref:`valid <valid-reftype>`.
 
 * Then the table type is valid.
 
 .. math::
    \frac{
-     C \vdashlimits \limits : 2^{32} - 1
+     C \vdashlimits \limits : 2^{|\idxtype|}-1
      \qquad
      C \vdashreftype \reftype \ok
    }{
-     C \vdashtabletype \limits~\reftype \ok
+     C \vdashtabletype \idxtype~\limits~\reftype \ok
    }
 
 
@@ -528,16 +528,16 @@ Table Types
 Memory Types
 ~~~~~~~~~~~~
 
-:math:`\limits`
-...............
+:math:`\idxtype~\limits`
+........................
 
-* The limits :math:`\limits` must be :ref:`valid <valid-limits>` within range :math:`2^{16}`.
+* The limits :math:`\limits` must be :ref:`valid <valid-limits>` within range :math:`2^{|\idxtype|-16}`.
 
 * Then the memory type is valid.
 
 .. math::
    \frac{
-     C \vdashlimits \limits : 2^{16}
+     C \vdashlimits \limits : 2^{|\idxtype|-16}
    }{
      C \vdashmemtype \limits \ok
    }