Skip to content

Commit

Permalink
Finish valid instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
@rossberg
rossberg committed May 28, 2024
1 parent bcd0d29 commit 5deded2
Show file tree
Hide file tree
Showing 10 changed files with 569 additions and 482 deletions.
78 changes: 39 additions & 39 deletions document/core/appendix/index-instructions.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,29 +108,29 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(r'\TABLEGET~x', r'\hex{25}', r'[\I32] \to [t]', r'valid-table.get', r'exec-table.get'),
Instruction(r'\TABLESET~x', r'\hex{26}', r'[\I32~t] \to []', r'valid-table.set', r'exec-table.set'),
Instruction(None, r'\hex{27}'),
Instruction(r'\I32.\LOAD~x~\memarg', r'\hex{28}', r'[\I32] \to [\I32]', r'valid-load', r'exec-load'),
Instruction(r'\I64.\LOAD~x~\memarg', r'\hex{29}', r'[\I32] \to [\I64]', r'valid-load', r'exec-load'),
Instruction(r'\F32.\LOAD~x~\memarg', r'\hex{2A}', r'[\I32] \to [\F32]', r'valid-load', r'exec-load'),
Instruction(r'\F64.\LOAD~x~\memarg', r'\hex{2B}', r'[\I32] \to [\F64]', r'valid-load', r'exec-load'),
Instruction(r'\I32.\LOAD\K{8\_s}~x~\memarg', r'\hex{2C}', r'[\I32] \to [\I32]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I32.\LOAD\K{8\_u}~x~\memarg', r'\hex{2D}', r'[\I32] \to [\I32]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I32.\LOAD\K{16\_s}~x~\memarg', r'\hex{2E}', r'[\I32] \to [\I32]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I32.\LOAD\K{16\_u}~x~\memarg', r'\hex{2F}', r'[\I32] \to [\I32]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I64.\LOAD\K{8\_s}~x~\memarg', r'\hex{30}', r'[\I32] \to [\I64]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I64.\LOAD\K{8\_u}~x~\memarg', r'\hex{31}', r'[\I32] \to [\I64]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I64.\LOAD\K{16\_s}~x~\memarg', r'\hex{32}', r'[\I32] \to [\I64]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I64.\LOAD\K{16\_u}~x~\memarg', r'\hex{33}', r'[\I32] \to [\I64]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I64.\LOAD\K{32\_s}~x~\memarg', r'\hex{34}', r'[\I32] \to [\I64]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I64.\LOAD\K{32\_u}~x~\memarg', r'\hex{35}', r'[\I32] \to [\I64]', r'valid-loadn', r'exec-loadn'),
Instruction(r'\I32.\STORE~x~\memarg', r'\hex{36}', r'[\I32~\I32] \to []', r'valid-store', r'exec-store'),
Instruction(r'\I64.\STORE~x~\memarg', r'\hex{37}', r'[\I32~\I64] \to []', r'valid-store', r'exec-store'),
Instruction(r'\F32.\STORE~x~\memarg', r'\hex{38}', r'[\I32~\F32] \to []', r'valid-store', r'exec-store'),
Instruction(r'\F64.\STORE~x~\memarg', r'\hex{39}', r'[\I32~\F64] \to []', r'valid-store', r'exec-store'),
Instruction(r'\I32.\STORE\K{8}~x~\memarg', r'\hex{3A}', r'[\I32~\I32] \to []', r'valid-storen', r'exec-storen'),
Instruction(r'\I32.\STORE\K{16}~x~\memarg', r'\hex{3B}', r'[\I32~\I32] \to []', r'valid-storen', r'exec-storen'),
Instruction(r'\I64.\STORE\K{8}~x~\memarg', r'\hex{3C}', r'[\I32~\I64] \to []', r'valid-storen', r'exec-storen'),
Instruction(r'\I64.\STORE\K{16}~x~\memarg', r'\hex{3D}', r'[\I32~\I64] \to []', r'valid-storen', r'exec-storen'),
Instruction(r'\I64.\STORE\K{32}~x~\memarg', r'\hex{3E}', r'[\I32~\I64] \to []', r'valid-storen', r'exec-storen'),
Instruction(r'\I32.\LOAD~x~\memarg', r'\hex{28}', r'[\I32] \to [\I32]', r'valid-load-val', r'exec-load-val'),
Instruction(r'\I64.\LOAD~x~\memarg', r'\hex{29}', r'[\I32] \to [\I64]', r'valid-load-val', r'exec-load-val'),
Instruction(r'\F32.\LOAD~x~\memarg', r'\hex{2A}', r'[\I32] \to [\F32]', r'valid-load-val', r'exec-load-val'),
Instruction(r'\F64.\LOAD~x~\memarg', r'\hex{2B}', r'[\I32] \to [\F64]', r'valid-load-val', r'exec-load-val'),
Instruction(r'\I32.\LOAD\K{8\_s}~x~\memarg', r'\hex{2C}', r'[\I32] \to [\I32]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I32.\LOAD\K{8\_u}~x~\memarg', r'\hex{2D}', r'[\I32] \to [\I32]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I32.\LOAD\K{16\_s}~x~\memarg', r'\hex{2E}', r'[\I32] \to [\I32]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I32.\LOAD\K{16\_u}~x~\memarg', r'\hex{2F}', r'[\I32] \to [\I32]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I64.\LOAD\K{8\_s}~x~\memarg', r'\hex{30}', r'[\I32] \to [\I64]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I64.\LOAD\K{8\_u}~x~\memarg', r'\hex{31}', r'[\I32] \to [\I64]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I64.\LOAD\K{16\_s}~x~\memarg', r'\hex{32}', r'[\I32] \to [\I64]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I64.\LOAD\K{16\_u}~x~\memarg', r'\hex{33}', r'[\I32] \to [\I64]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I64.\LOAD\K{32\_s}~x~\memarg', r'\hex{34}', r'[\I32] \to [\I64]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I64.\LOAD\K{32\_u}~x~\memarg', r'\hex{35}', r'[\I32] \to [\I64]', r'valid-load-pack', r'exec-load-pack'),
Instruction(r'\I32.\STORE~x~\memarg', r'\hex{36}', r'[\I32~\I32] \to []', r'valid-store-val', r'exec-store-val'),
Instruction(r'\I64.\STORE~x~\memarg', r'\hex{37}', r'[\I32~\I64] \to []', r'valid-store-val', r'exec-store-val'),
Instruction(r'\F32.\STORE~x~\memarg', r'\hex{38}', r'[\I32~\F32] \to []', r'valid-store-val', r'exec-store-val'),
Instruction(r'\F64.\STORE~x~\memarg', r'\hex{39}', r'[\I32~\F64] \to []', r'valid-store-val', r'exec-store-val'),
Instruction(r'\I32.\STORE\K{8}~x~\memarg', r'\hex{3A}', r'[\I32~\I32] \to []', r'valid-store-pack', r'exec-store-pack'),
Instruction(r'\I32.\STORE\K{16}~x~\memarg', r'\hex{3B}', r'[\I32~\I32] \to []', r'valid-store-pack', r'exec-store-pack'),
Instruction(r'\I64.\STORE\K{8}~x~\memarg', r'\hex{3C}', r'[\I32~\I64] \to []', r'valid-store-pack', r'exec-store-pack'),
Instruction(r'\I64.\STORE\K{16}~x~\memarg', r'\hex{3D}', r'[\I32~\I64] \to []', r'valid-store-pack', r'exec-store-pack'),
Instruction(r'\I64.\STORE\K{32}~x~\memarg', r'\hex{3E}', r'[\I32~\I64] \to []', r'valid-store-pack', r'exec-store-pack'),
Instruction(r'\MEMORYSIZE~x', r'\hex{3F}', r'[] \to [\I32]', r'valid-memory.size', r'exec-memory.size'),
Instruction(r'\MEMORYGROW~x', r'\hex{40}', r'[\I32] \to [\I32]', r'valid-memory.grow', r'exec-memory.grow'),
Instruction(r'\I32.\CONST~\i32', r'\hex{41}', r'[] \to [\I32]', r'valid-const', r'exec-const'),
Expand Down Expand Up @@ -370,18 +370,18 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(r'\TABLESIZE~x', r'\hex{FC}~\hex{10}', r'[] \to [\I32]', r'valid-table.size', r'exec-table.size'),
Instruction(r'\TABLEFILL~x', r'\hex{FC}~\hex{11}', r'[\I32~t~\I32] \to []', r'valid-table.fill', r'exec-table.fill'),
Instruction(None, r'\hex{FC}~\hex{1E} \dots'),
Instruction(r'\V128.\VLOAD~x~\memarg', r'\hex{FD}~~\hex{00}', r'[\I32] \to [\V128]', r'valid-load', r'exec-load'),
Instruction(r'\V128.\VLOAD\K{8x8\_s}~x~\memarg', r'\hex{FD}~~\hex{01}', r'[\I32] \to [\V128]', r'valid-vload-ext', r'exec-vload-ext'),
Instruction(r'\V128.\VLOAD\K{8x8\_u}~x~\memarg', r'\hex{FD}~~\hex{02}', r'[\I32] \to [\V128]', r'valid-vload-ext', r'exec-vload-ext'),
Instruction(r'\V128.\VLOAD\K{16x4\_s}~x~\memarg', r'\hex{FD}~~\hex{03}', r'[\I32] \to [\V128]', r'valid-vload-ext', r'exec-vload-ext'),
Instruction(r'\V128.\VLOAD\K{16x4\_u}~x~\memarg', r'\hex{FD}~~\hex{04}', r'[\I32] \to [\V128]', r'valid-vload-ext', r'exec-vload-ext'),
Instruction(r'\V128.\VLOAD\K{32x2\_s}~x~\memarg', r'\hex{FD}~~\hex{05}', r'[\I32] \to [\V128]', r'valid-vload-ext', r'exec-vload-ext'),
Instruction(r'\V128.\VLOAD\K{32x2\_u}~x~\memarg', r'\hex{FD}~~\hex{06}', r'[\I32] \to [\V128]', r'valid-vload-ext', r'exec-vload-ext'),
Instruction(r'\V128.\VLOAD~x~\memarg', r'\hex{FD}~~\hex{00}', r'[\I32] \to [\V128]', r'valid-vload-val', r'exec-vload-val'),
Instruction(r'\V128.\VLOAD\K{8x8\_s}~x~\memarg', r'\hex{FD}~~\hex{01}', r'[\I32] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'),
Instruction(r'\V128.\VLOAD\K{8x8\_u}~x~\memarg', r'\hex{FD}~~\hex{02}', r'[\I32] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'),
Instruction(r'\V128.\VLOAD\K{16x4\_s}~x~\memarg', r'\hex{FD}~~\hex{03}', r'[\I32] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'),
Instruction(r'\V128.\VLOAD\K{16x4\_u}~x~\memarg', r'\hex{FD}~~\hex{04}', r'[\I32] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'),
Instruction(r'\V128.\VLOAD\K{32x2\_s}~x~\memarg', r'\hex{FD}~~\hex{05}', r'[\I32] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'),
Instruction(r'\V128.\VLOAD\K{32x2\_u}~x~\memarg', r'\hex{FD}~~\hex{06}', r'[\I32] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'),
Instruction(r'\V128.\VLOAD\K{8\_splat}~x~\memarg', r'\hex{FD}~~\hex{07}', r'[\I32] \to [\V128]', r'valid-vload-splat', r'exec-vload-splat'),
Instruction(r'\V128.\VLOAD\K{16\_splat}~x~\memarg', r'\hex{FD}~~\hex{08}', r'[\I32] \to [\V128]', r'valid-vload-splat', r'exec-vload-splat'),
Instruction(r'\V128.\VLOAD\K{32\_splat}~x~\memarg', r'\hex{FD}~~\hex{09}', r'[\I32] \to [\V128]', r'valid-vload-splat', r'exec-vload-splat'),
Instruction(r'\V128.\VLOAD\K{64\_splat}~x~\memarg', r'\hex{FD}~~\hex{0A}', r'[\I32] \to [\V128]', r'valid-vload-splat', r'exec-vload-splat'),
Instruction(r'\V128.\VSTORE~x~\memarg', r'\hex{FD}~~\hex{0B}', r'[\I32~\V128] \to []', r'valid-store', r'exec-store'),
Instruction(r'\V128.\VSTORE~x~\memarg', r'\hex{FD}~~\hex{0B}', r'[\I32~\V128] \to []', r'valid-vstore', r'exec-vstore'),
Instruction(r'\V128.\VCONST~\i128', r'\hex{FD}~~\hex{0C}', r'[] \to [\V128]', r'valid-vconst', r'exec-vconst'),
Instruction(r'\I8X16.\VSHUFFLE~\laneidx^{16}', r'\hex{FD}~~\hex{0D}', r'[\V128~\V128] \to [\V128]', r'valid-vshuffle', r'exec-vshuffle'),
Instruction(r'\I8X16.\VSWIZZLE', r'\hex{FD}~~\hex{0E}', r'[\V128~\V128] \to [\V128]', r'valid-vswizzle', r'exec-vswizzle'),
Expand Down Expand Up @@ -454,14 +454,14 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
Instruction(r'\V128.\VXOR', r'\hex{FD}~~\hex{51}', r'[\V128~\V128] \to [\V128]', r'valid-vvbinop', r'exec-vvbinop', r'op-ixor'),
Instruction(r'\V128.\VBITSELECT', r'\hex{FD}~~\hex{52}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-vvternop', r'exec-vvternop', r'op-ibitselect'),
Instruction(r'\V128.\VANYTRUE', r'\hex{FD}~~\hex{53}', r'[\V128] \to [\I32]', r'valid-vvtestop', r'exec-vvtestop'),
Instruction(r'\V128.\VLOAD\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{54}', r'[\I32~\V128] \to [\V128]', r'valid-vload-lane', r'exec-vload-lane'),
Instruction(r'\V128.\VLOAD\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{55}', r'[\I32~\V128] \to [\V128]', r'valid-vload-lane', r'exec-vload-lane'),
Instruction(r'\V128.\VLOAD\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{56}', r'[\I32~\V128] \to [\V128]', r'valid-vload-lane', r'exec-vload-lane'),
Instruction(r'\V128.\VLOAD\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{57}', r'[\I32~\V128] \to [\V128]', r'valid-vload-lane', r'exec-vload-lane'),
Instruction(r'\V128.\VSTORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to []', r'valid-vstore-lane', r'exec-vstore-lane'),
Instruction(r'\V128.\VSTORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-vstore-lane', r'exec-vstore-lane'),
Instruction(r'\V128.\VSTORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-vstore-lane', r'exec-vstore-lane'),
Instruction(r'\V128.\VSTORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-vstore-lane', r'exec-vstore-lane'),
Instruction(r'\V128.\VLOAD\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{54}', r'[\I32~\V128] \to [\V128]', r'valid-vload_lane', r'exec-vload_lane'),
Instruction(r'\V128.\VLOAD\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{55}', r'[\I32~\V128] \to [\V128]', r'valid-vload_lane', r'exec-vload_lane'),
Instruction(r'\V128.\VLOAD\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{56}', r'[\I32~\V128] \to [\V128]', r'valid-vload_lane', r'exec-vload_lane'),
Instruction(r'\V128.\VLOAD\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{57}', r'[\I32~\V128] \to [\V128]', r'valid-vload_lane', r'exec-vload_lane'),
Instruction(r'\V128.\VSTORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to []', r'valid-vstore_lane', r'exec-vstore_lane'),
Instruction(r'\V128.\VSTORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-vstore_lane', r'exec-vstore_lane'),
Instruction(r'\V128.\VSTORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-vstore_lane', r'exec-vstore_lane'),
Instruction(r'\V128.\VSTORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-vstore_lane', r'exec-vstore_lane'),
Instruction(r'\V128.\VLOAD\K{32\_zero}~\memarg', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-vload-zero', r'exec-vload-zero'),
Instruction(r'\V128.\VLOAD\K{64\_zero}~\memarg', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-vload-zero', r'exec-vload-zero'),
Instruction(r'\F32X4.\VDEMOTE\K{\_f64x2\_zero}', r'\hex{FD}~~\hex{5E}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-demote'),
Expand Down
44 changes: 23 additions & 21 deletions document/core/exec/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1817,8 +1817,9 @@ Memory Instructions
However, it may be substantially slower on some hardware.


.. _exec-load:
.. _exec-loadn:
.. _exec-load-val:
.. _exec-load-pack:
.. _exec-vload-val:

$${rule-prose: exec/load}

Expand All @@ -1828,15 +1829,15 @@ $${rule-prose: exec/load}

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-loadn>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.
2. Assert: due to :ref:`validation <valid-load-pack>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.

3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[x]`.

4. Assert: due to :ref:`validation <valid-loadn>`, :math:`S.\SMEMS[a]` exists.
4. Assert: due to :ref:`validation <valid-load-pack>`, :math:`S.\SMEMS[a]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.

6. Assert: due to :ref:`validation <valid-loadn>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
6. Assert: due to :ref:`validation <valid-load-pack>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

7. Pop the value :math:`\I32.\CONST~i` from the stack.

Expand Down Expand Up @@ -1867,7 +1868,7 @@ $${rule-prose: exec/load}
$${rule: {Step_read/load-*}}

.. _exec-vload-ext:
.. _exec-vload-pack:

:math:`\V128\K{.}\VLOAD{M}\K{x}N\_\sx~x~\memarg`
................................................
Expand All @@ -1876,15 +1877,15 @@ $${rule: {Step_read/load-*}}

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-vload-ext>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.
2. Assert: due to :ref:`validation <valid-vload-pack>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.

3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[x]`.

4. Assert: due to :ref:`validation <valid-vload-ext>`, :math:`S.\SMEMS[a]` exists.
4. Assert: due to :ref:`validation <valid-vload-pack>`, :math:`S.\SMEMS[a]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.

6. Assert: due to :ref:`validation <valid-vload-ext>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
6. Assert: due to :ref:`validation <valid-vload-pack>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

7. Pop the value :math:`\I32.\CONST~i` from the stack.

Expand Down Expand Up @@ -2046,7 +2047,7 @@ $${rule: {Step_read/load-*}}
\end{array}
.. _exec-vload-lane:
.. _exec-vload_lane:

:math:`\V128\K{.}\VLOAD{N}\K{\_lane}~x~\memarg~y`
.................................................
Expand All @@ -2055,19 +2056,19 @@ $${rule: {Step_read/load-*}}

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-vload-lane>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.
2. Assert: due to :ref:`validation <valid-vload_lane>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.

3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[x]`.

4. Assert: due to :ref:`validation <valid-vload-lane>`, :math:`S.\SMEMS[a]` exists.
4. Assert: due to :ref:`validation <valid-vload_lane>`, :math:`S.\SMEMS[a]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.

6. Assert: due to :ref:`validation <valid-vload-lane>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
6. Assert: due to :ref:`validation <valid-vload_lane>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.

7. Pop the value :math:`\V128.\CONST~v` from the stack.

8. Assert: due to :ref:`validation <valid-vload-lane>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
8. Assert: due to :ref:`validation <valid-vload_lane>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

9. Pop the value :math:`\I32.\CONST~i` from the stack.

Expand Down Expand Up @@ -2112,15 +2113,16 @@ $${rule: {Step_read/load-*}}
\end{array}
.. _exec-store:
.. _exec-storen:
.. _exec-store-val:
.. _exec-store-pack:
.. _exec-vstore:

$${rule-prose: exec/store}

$${rule: {Step/store-*}}

.. _exec-vstore-lane:
.. _exec-vstore_lane:

:math:`\V128\K{.}\VSTORE{N}\K{\_lane}~x~\memarg~y`
..................................................
Expand All @@ -2129,19 +2131,19 @@ $${rule: {Step/store-*}}

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-vstore-lane>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.
2. Assert: due to :ref:`validation <valid-vstore_lane>`, :math:`F.\AMODULE.\MIMEMS[x]` exists.

3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[x]`.

4. Assert: due to :ref:`validation <valid-storen>`, :math:`S.\SMEMS[a]` exists.
4. Assert: due to :ref:`validation <valid-store-pack>`, :math:`S.\SMEMS[a]` exists.

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.

6. Assert: due to :ref:`validation <valid-vstore-lane>`, a value of :ref:`value type <syntax-valtype>` :math:`\V128` is on the top of the stack.
6. Assert: due to :ref:`validation <valid-vstore_lane>`, a value of :ref:`value type <syntax-valtype>` :math:`\V128` is on the top of the stack.

7. Pop the value :math:`\V128.\CONST~c` from the stack.

8. Assert: due to :ref:`validation <valid-vstore-lane>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
8. Assert: due to :ref:`validation <valid-vstore_lane>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

9. Pop the value :math:`\I32.\CONST~i` from the stack.

Expand Down
Loading

0 comments on commit 5deded2

Please sign in to comment.