Skip to content

Commit

Permalink
Update memory/table embedding and execution to u64
Browse files Browse the repository at this point in the history 
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`.
  • Loading branch information
@bvisness
bvisness committed Aug 2, 2024
1 parent da13da3 commit 42b7239
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 26 deletions.
18 changes: 9 additions & 9 deletions document/core/appendix/embedding.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]`.
Expand All @@ -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]`.
Expand All @@ -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`.
Expand All @@ -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`:
Expand Down Expand Up @@ -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]`.
Expand All @@ -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`.

Expand All @@ -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>`.
Expand All @@ -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>`:
Expand Down
34 changes: 17 additions & 17 deletions document/core/exec/modules.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

Expand All @@ -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\} \\
Expand All @@ -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`.

Expand All @@ -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\} \\
Expand Down Expand Up @@ -284,26 +284,26 @@ 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. If :math:`\X{len}` is larger than or equal to :math:`2^{64}`, then fail.

4. Let :math:`\limits~t` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tableinst.\TITYPE`.
4. Let :math:`(\idxtype~\limits~\reftype)` be the structure of :ref:`table type <syntax-tabletype>` :math:`\tableinst.\TITYPE`.

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.

7. Append :math:`\reff^n` to :math:`\tableinst.\TIELEM`.

8. Set :math:`\tableinst.\TITYPE` to the :ref:`table type <syntax-tabletype>` :math:`\limits'~t`.
8. 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 & \X{len} < 2^{64} \\
\wedge & \idxtype~\limits~\reftype = \tableinst.\TITYPE \\
\wedge & \limits' = \limits \with \LMIN = \X{len} \\
\wedge & \vdashlimits \limits' \ok) \\
\end{array} \\
Expand All @@ -322,26 +322,26 @@ 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. If :math:`\X{len}` is larger than :math:`2^{48}`, then fail.

5. Let :math:`\limits` be the structure of :ref:`memory type <syntax-memtype>` :math:`\meminst.\MITYPE`.
5. Let :math:`(\idxtype~\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}`.

7. If :math:`\limits'` is not :ref:`valid <valid-limits>`, then fail.

8. 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'`.
9. 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 & \X{len} \leq 2^{48} \\
\wedge & \idxtype~\limits = \meminst.\MITYPE \\
\wedge & \limits' = \limits \with \LMIN = \X{len} \\
\wedge & \vdashlimits \limits' \ok) \\
\end{array} \\
Expand Down

0 comments on commit 42b7239

Please sign in to comment.