diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py
index bd18368b8f..0e9d6b9ee4 100755
--- a/document/core/appendix/index-instructions.py
+++ b/document/core/appendix/index-instructions.py
@@ -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'),
@@ -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'),
@@ -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'),
diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
index 2af9e9e64e..7dbaabb2de 100644
--- a/document/core/exec/instructions.rst
+++ b/document/core/exec/instructions.rst
@@ -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}
 
@@ -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.
 
@@ -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`
 ................................................
@@ -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.
 
@@ -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`
 .................................................
@@ -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.
 
@@ -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`
 ..................................................
@@ -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.
 
diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index 67cbf7ac04..3b0e493c4c 100644
--- a/document/core/valid/instructions.rst
+++ b/document/core/valid/instructions.rst
@@ -1134,7 +1134,7 @@ $${rule: Instr_ok/elem.drop}
 Memory Instructions
 ~~~~~~~~~~~~~~~~~~~
 
-.. _valid-load:
+.. _valid-load-val:
 
 :math:`t\K{.}\LOAD~x~\memarg`
 .............................
@@ -1145,19 +1145,10 @@ Memory Instructions
 
 * Then the instruction is valid with type :math:`[\I32] \to [t]`.
 
-$${rule: Instr_ok/load}
+$${rule: Instr_ok/load-val}
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq |t|/8
-   }{
-     C \vdashinstr t\K{.load}~x~\memarg : [\I32] \to [t]
-   }
 
-
-.. _valid-loadn:
+.. _valid-load-pack:
 
 :math:`t\K{.}\LOAD{N}\K{\_}\sx~x~\memarg`
 .........................................
@@ -1168,15 +1159,10 @@ $${rule: Instr_ok/load}
 
 * Then the instruction is valid with type :math:`[\I32] \to [t]`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq N/8
-   }{
-     C \vdashinstr t\K{.load}N\K{\_}\sx~x~\memarg : [\I32] \to [t]
-   }
+$${rule: Instr_ok/load-pack}
+
 
+.. _valid-store-val:
 
 :math:`t\K{.}\STORE~x~\memarg`
 ..............................
@@ -1187,19 +1173,10 @@ $${rule: Instr_ok/load}
 
 * Then the instruction is valid with type :math:`[\I32~t] \to []`.
 
-$${rule: Instr_ok/store}
+$${rule: Instr_ok/store-val}
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq |t|/8
-   }{
-     C \vdashinstr t\K{.store}~x~\memarg : [\I32~t] \to []
-   }
 
-
-.. _valid-storen:
+.. _valid-store-pack:
 
 :math:`t\K{.}\STORE{N}~x~\memarg`
 .................................
@@ -1210,17 +1187,24 @@ $${rule: Instr_ok/store}
 
 * Then the instruction is valid with type :math:`[\I32~t] \to []`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq N/8
-   }{
-     C \vdashinstr t\K{.store}N~x~\memarg : [\I32~t] \to []
-   }
+$${rule: Instr_ok/store-pack}
+
+
+.. _valid-vload-val:
+
+:math:`\K{v128.}\K{.}\LOAD~x~\memarg`
+.....................................
+
+* The memory :math:`C.\CMEMS[x]` must be defined in the context.
+
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width <syntax-numtype>` of :math:`t` divided by :math:`8`.
+
+* Then the instruction is valid with type :math:`[\I32] \to [t]`.
 
+$${rule: Instr_ok/vload-val}
 
-.. _valid-vload-ext:
+
+.. _valid-vload-pack:
 
 :math:`\K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg`
 ..............................................
@@ -1231,14 +1215,7 @@ $${rule: Instr_ok/store}
 
 * Then the instruction is valid with type :math:`[\I32] \to [\V128]`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq N/8 \cdot M
-   }{
-     C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg : [\I32] \to [\V128]
-   }
+$${rule: Instr_ok/vload-pack}
 
 
 .. _valid-vload-splat:
@@ -1252,14 +1229,7 @@ $${rule: Instr_ok/store}
 
 * Then the instruction is valid with type :math:`[\I32] \to [\V128]`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq N/8
-   }{
-     C \vdashinstr \K{v128.}\LOAD{N}\K{\_splat}~x~\memarg : [\I32] \to [\V128]
-   }
+$${rule: Instr_ok/vload-splat}
 
 
 .. _valid-vload-zero:
@@ -1273,17 +1243,10 @@ $${rule: Instr_ok/store}
 
 * Then the instruction is valid with type :math:`[\I32] \to [\V128]`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} \leq N/8
-   }{
-     C \vdashinstr \K{v128.}\LOAD{N}\K{\_zero}~x~\memarg : [\I32] \to [\V128]
-   }
+$${rule: Instr_ok/vload-zero}
 
 
-.. _valid-vload-lane:
+.. _valid-vload_lane:
 
 :math:`\K{v128.}\LOAD{N}\K{\_lane}~x~\memarg~\laneidx`
 ......................................................
@@ -1296,19 +1259,24 @@ $${rule: Instr_ok/store}
 
 * Then the instruction is valid with type :math:`[\I32~\V128] \to [\V128]`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} < N/8
-     \qquad
-     \laneidx < 128/N
-   }{
-     C \vdashinstr \K{v128.}\LOAD{N}\K{\_lane}~x~\memarg~\laneidx : [\I32~\V128] \to [\V128]
-   }
+$${rule: Instr_ok/vload_lane}
+
+
+.. _valid-vstore:
+
+:math:`\K{v128.}\STORE~x~\memarg`
+.................................
+
+* The memory :math:`C.\CMEMS[x]` must be defined in the context.
+
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width <syntax-numtype>` of :math:`t` divided by :math:`8`.
+
+* Then the instruction is valid with type :math:`[\I32~t] \to []`.
+
+$${rule: Instr_ok/vstore}
 
 
-.. _valid-vstore-lane:
+.. _valid-vstore_lane:
 
 :math:`\K{v128.}\STORE{N}\K{\_lane}~x~\memarg~\laneidx`
 .......................................................
@@ -1321,16 +1289,7 @@ $${rule: Instr_ok/store}
 
 * Then the instruction is valid with type :math:`[\I32~\V128] \to [\V128]`.
 
-.. math::
-   \frac{
-     C.\CMEMS[x] = \memtype
-     \qquad
-     2^{\memarg.\ALIGN} < N/8
-     \qquad
-     \laneidx < 128/N
-   }{
-     C \vdashinstr \K{v128.}\STORE{N}\K{\_lane}~x~\memarg~\laneidx : [\I32~\V128] \to []
-   }
+$${rule: Instr_ok/vstore_lane}
 
 
 .. _valid-memory.size:
@@ -1698,7 +1657,7 @@ $${rule: Instr_ok/return}
 .. note::
    The ${:RETURN} instruction is :ref:`stack-polymorphic <polymorphism>`.
 
-   ${:C.RETURN} is absent (set to ${:eps}) when validating an :ref:`expression <valid-expr>` that is not a function body.
+   ${resulttype?: C.RETURN} is absent (set to ${:eps}) when validating an :ref:`expression <valid-expr>` that is not a function body.
    This differs from it being set to the empty result type ${:(eps)},
    which is the case for functions not returning anything.
 
diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
index 711c91d99a..e83d1b608d 100644
--- a/spectec/spec/wasm-3.0/6-typing.watsup
+++ b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -1023,40 +1023,69 @@ rule Instr_ok/data.drop:
   C |- DATA.DROP x : eps -> eps
   -- if C.DATAS[x] = OK
 
+(;
 rule Instr_ok/load:
-  C |- LOAD nt (n _ sx)? x memarg : I32 -> nt
+  C |- LOAD nt (N _ sx)? x memarg : I32 -> nt
   -- if C.MEMS[x] = mt
   -- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-  -- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
-  -- if n? = eps \/ nt = Inn
+  -- if $(2^(memarg.ALIGN) <= N/8 < $size(nt)/8)?
+  -- if N? = eps \/ nt = Inn
+;)
 
+rule Instr_ok/load-val:
+  C |- LOAD nt x memarg : I32 -> nt
+  -- if C.MEMS[x] = mt
+  -- if $(2^(memarg.ALIGN) <= $size(nt)/8)
+
+rule Instr_ok/load-pack:
+  C |- LOAD Inn (M _ sx) x memarg : I32 -> Inn
+  -- if C.MEMS[x] = mt
+  -- if $(2^(memarg.ALIGN) <= M/8)
+
+(;
 rule Instr_ok/store:
-  C |- STORE nt n? x memarg : I32 nt -> eps
+  C |- STORE nt N? x memarg : I32 nt -> eps
   -- if C.MEMS[x] = mt
   -- if $(2^(memarg.ALIGN) <= $size(nt)/8)
-  -- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)?
-  -- if n? = eps \/ nt = Inn
+  -- if $(2^(memarg.ALIGN) <= N/8 < $size(nt)/8)?
+  -- if N? = eps \/ nt = Inn
+;)
+
+rule Instr_ok/store-val:
+  C |- STORE nt x memarg : I32 nt -> eps
+  -- if C.MEMS[x] = mt
+  -- if $(2^(memarg.ALIGN) <= $size(nt)/8)
+
+rule Instr_ok/store-pack:
+  C |- STORE Inn M x memarg : I32 Inn -> eps
+  -- if C.MEMS[x] = mt
+  -- if $(2^(memarg.ALIGN) <= M/8)
+
+rule Instr_ok/vload-val:
+  C |- VLOAD V128 x memarg : I32 -> V128
+  -- if C.MEMS[x] = mt
+  -- if $(2^(memarg.ALIGN) <= $vsize(V128)/8)
 
-rule Instr_ok/vload:
+rule Instr_ok/vload-pack:
   C |- VLOAD V128 (SHAPE M X N sx) x memarg : I32 -> V128
   -- if C.MEMS[x] = mt
   -- if $(2^(memarg.ALIGN) <= M/8 * N)
 
 rule Instr_ok/vload-splat:
-  C |- VLOAD V128 (SPLAT n) x memarg : I32 -> V128
+  C |- VLOAD V128 (SPLAT N) x memarg : I32 -> V128
   -- if C.MEMS[x] = mt
-  -- if $(2^(memarg.ALIGN) <= n/8)
+  -- if $(2^(memarg.ALIGN) <= N/8)
 
 rule Instr_ok/vload-zero:
-  C |- VLOAD V128 (ZERO n) x memarg : I32 -> V128
+  C |- VLOAD V128 (ZERO N) x memarg : I32 -> V128
   -- if C.MEMS[x] = mt
-  -- if $(2^(memarg.ALIGN) < n/8)
+  -- if $(2^(memarg.ALIGN) < N/8)
 
 rule Instr_ok/vload_lane:
-  C |- VLOAD_LANE V128 n x memarg laneidx : I32 V128 -> V128
+  C |- VLOAD_LANE V128 N x memarg i : I32 V128 -> V128
   -- if C.MEMS[x] = mt
-  -- if $(2^(memarg.ALIGN) < n/8)
-  -- if $(laneidx < 128 / n)
+  -- if $(2^(memarg.ALIGN) < N/8)
+  -- if $(i < 128/N)
 
 rule Instr_ok/vstore:
   C |- VSTORE V128 x memarg : I32 V128 -> eps
@@ -1064,10 +1093,10 @@ rule Instr_ok/vstore:
   -- if $(2^(memarg.ALIGN) <= $vsize(V128)/8)
 
 rule Instr_ok/vstore_lane:
-  C |- VSTORE_LANE V128 n x memarg laneidx : I32 V128 -> eps
+  C |- VSTORE_LANE V128 N x memarg i : I32 V128 -> eps
   -- if C.MEMS[x] = mt
-  -- if $(2^(memarg.ALIGN) < n/8)
-  -- if $(laneidx < 128 / n)
+  -- if $(2^(memarg.ALIGN) < N/8)
+  -- if $(i < 128/N)
 
 
 ;;
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index d6db2a7cdc..2fd9c92987 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -4036,59 +4036,73 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([])))
     -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype)
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1035.1-1038.43
+  rule load-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1040.1-1043.35
+  rule load-pack{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr((Inn : Inn <: numtype), ?((`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1054.1-1057.43
+  rule store-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1040.1-1043.39
-  rule vload{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+  ;; 6-typing.watsup:1059.1-1062.35
+  rule store-pack{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1064.1-1067.46
+  rule vload-val{C : context, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
+
+  ;; 6-typing.watsup:1069.1-1072.39
+  rule vload-pack{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N))
 
-  ;; 6-typing.watsup:1045.1-1048.35
-  rule vload-splat{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1074.1-1077.35
+  rule vload-splat{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8))
 
-  ;; 6-typing.watsup:1050.1-1053.34
-  rule vload-zero{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1079.1-1082.34
+  rule vload-zero{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
 
-  ;; 6-typing.watsup:1055.1-1059.29
-  rule vload_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1084.1-1088.21
+  rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
-  ;; 6-typing.watsup:1061.1-1064.46
+  ;; 6-typing.watsup:1090.1-1093.46
   rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
 
-  ;; 6-typing.watsup:1066.1-1070.29
-  rule vstore_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1095.1-1099.21
+  rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
 ;; 6-typing.watsup:516.1-516.96
 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
@@ -4127,22 +4141,22 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1126.1-1126.86
+;; 6-typing.watsup:1155.1-1155.86
 def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1127.1-1127.42
+  ;; 6-typing.watsup:1156.1-1156.42
   def $in_binop{nt : numtype, binop : binop_(nt), epsilon : binop_(nt)*}(nt, binop, epsilon) = false
-  ;; 6-typing.watsup:1128.1-1128.99
+  ;; 6-typing.watsup:1157.1-1157.99
   def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
 }
 
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1122.1-1122.63
+;; 6-typing.watsup:1151.1-1151.63
 def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1123.1-1123.37
+  ;; 6-typing.watsup:1152.1-1152.37
   def $in_numtype{nt : numtype, epsilon : numtype*}(nt, epsilon) = false
-  ;; 6-typing.watsup:1124.1-1124.68
+  ;; 6-typing.watsup:1153.1-1153.68
   def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
 }
 
@@ -4366,13 +4380,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1269.1-1269.100
+;; 6-typing.watsup:1298.1-1298.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1306.1-1307.17
+  ;; 6-typing.watsup:1335.1-1336.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1309.1-1312.55
+  ;; 6-typing.watsup:1338.1-1341.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -4382,13 +4396,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1268.1-1268.98
+;; 6-typing.watsup:1297.1-1297.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1298.1-1299.17
+  ;; 6-typing.watsup:1327.1-1328.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1301.1-1304.50
+  ;; 6-typing.watsup:1330.1-1333.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, [dt_1])
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index c77cedddb8..580b322f98 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -5811,13 +5811,22 @@ $$
 {\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
 {2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {|{\mathit{nt}}|} / 8
+}{
+{\mathit{{\scriptstyle C}}} \vdash {\mathit{nt}}{.}\mathsf{load}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow {\mathit{nt}}
+} \, {[\textsc{\scriptsize T{-}load{-}val}]}
+\qquad
+\end{array}
+$$
+
+$$
+\begin{array}{@{}c@{}}\displaystyle
+\frac{
+{\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-({2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq n / 8 < {|{\mathit{nt}}|} / 8)^?
- \qquad
-{n^?} = \epsilon \lor {\mathit{nt}} = {\mathsf{i}}{{\mathit{{\scriptstyle N}}}}
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {\mathit{{\scriptstyle M}}} / 8
 }{
-{\mathit{{\scriptstyle C}}} \vdash {{\mathit{nt}}{.}\mathsf{load}}{{({n}{\mathsf{\_}}{{\mathit{sx}}})^?}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow {\mathit{nt}}
-} \, {[\textsc{\scriptsize T{-}load}]}
+{\mathit{{\scriptstyle C}}} \vdash {{\mathsf{i}}{{\mathit{{\scriptstyle N}}}}{.}\mathsf{load}}{{{\mathit{{\scriptstyle M}}}}{\mathsf{\_}}{{\mathit{sx}}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow {\mathsf{i}}{{\mathit{{\scriptstyle N}}}}
+} \, {[\textsc{\scriptsize T{-}load{-}pack}]}
 \qquad
 \end{array}
 $$
@@ -5828,13 +5837,35 @@ $$
 {\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
 {2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {|{\mathit{nt}}|} / 8
+}{
+{\mathit{{\scriptstyle C}}} \vdash {\mathit{nt}}{.}\mathsf{store}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}}~{\mathit{nt}} \rightarrow \epsilon
+} \, {[\textsc{\scriptsize T{-}store{-}val}]}
+\qquad
+\end{array}
+$$
+
+$$
+\begin{array}{@{}c@{}}\displaystyle
+\frac{
+{\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-({2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq n / 8 < {|{\mathit{nt}}|} / 8)^?
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {\mathit{{\scriptstyle M}}} / 8
+}{
+{\mathit{{\scriptstyle C}}} \vdash {{\mathsf{i}}{{\mathit{{\scriptstyle N}}}}{.}\mathsf{store}}{{\mathit{{\scriptstyle M}}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}}~{\mathsf{i}}{{\mathit{{\scriptstyle N}}}} \rightarrow \epsilon
+} \, {[\textsc{\scriptsize T{-}store{-}pack}]}
+\qquad
+\end{array}
+$$
+
+$$
+\begin{array}{@{}c@{}}\displaystyle
+\frac{
+{\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-{n^?} = \epsilon \lor {\mathit{nt}} = {\mathsf{i}}{{\mathit{{\scriptstyle N}}}}
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {|\mathsf{v{\scriptstyle 128}}|} / 8
 }{
-{\mathit{{\scriptstyle C}}} \vdash {{\mathit{nt}}{.}\mathsf{store}}{{n^?}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}}~{\mathit{nt}} \rightarrow \epsilon
-} \, {[\textsc{\scriptsize T{-}store}]}
+{\mathit{{\scriptstyle C}}} \vdash \mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{v{\scriptstyle 128}}
+} \, {[\textsc{\scriptsize T{-}vload{-}val}]}
 \qquad
 \end{array}
 $$
@@ -5847,7 +5878,7 @@ $$
 {2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {\mathit{{\scriptstyle M}}} / 8 \cdot {\mathit{{\scriptstyle N}}}
 }{
 {\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{{\mathit{{\scriptstyle M}}}}{\mathsf{x}}{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{{\mathit{sx}}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{v{\scriptstyle 128}}
-} \, {[\textsc{\scriptsize T{-}vload}]}
+} \, {[\textsc{\scriptsize T{-}vload{-}pack}]}
 \qquad
 \end{array}
 $$
@@ -5857,9 +5888,9 @@ $$
 \frac{
 {\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-{2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq n / 8
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq {\mathit{{\scriptstyle N}}} / 8
 }{
-{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{n}{\mathsf{\_}}{\mathsf{splat}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{v{\scriptstyle 128}}
+{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\mathsf{splat}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{v{\scriptstyle 128}}
 } \, {[\textsc{\scriptsize T{-}vload{-}splat}]}
 \qquad
 \end{array}
@@ -5870,9 +5901,9 @@ $$
 \frac{
 {\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-{2^{{\mathit{memarg}}{.}\mathsf{align}}} < n / 8
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} < {\mathit{{\scriptstyle N}}} / 8
 }{
-{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{n}{\mathsf{\_}}{\mathsf{zero}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{v{\scriptstyle 128}}
+{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\mathsf{zero}}}~x~{\mathit{memarg}} : \mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{v{\scriptstyle 128}}
 } \, {[\textsc{\scriptsize T{-}vload{-}zero}]}
 \qquad
 \end{array}
@@ -5883,11 +5914,11 @@ $$
 \frac{
 {\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-{2^{{\mathit{memarg}}{.}\mathsf{align}}} < n / 8
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} < {\mathit{{\scriptstyle N}}} / 8
  \qquad
-{\mathit{laneidx}} < 128 / n
+i < 128 / {\mathit{{\scriptstyle N}}}
 }{
-{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{n}{\mathsf{\_}}{\mathsf{lane}}~x~{\mathit{memarg}}~{\mathit{laneidx}} : \mathsf{i{\scriptstyle 32}}~\mathsf{v{\scriptstyle 128}} \rightarrow \mathsf{v{\scriptstyle 128}}
+{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}}{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\mathsf{lane}}~x~{\mathit{memarg}}~i : \mathsf{i{\scriptstyle 32}}~\mathsf{v{\scriptstyle 128}} \rightarrow \mathsf{v{\scriptstyle 128}}
 } \, {[\textsc{\scriptsize T{-}vload\_lane}]}
 \qquad
 \end{array}
@@ -5911,11 +5942,11 @@ $$
 \frac{
 {\mathit{{\scriptstyle C}}}{.}\mathsf{mems}{}[x] = {\mathit{mt}}
  \qquad
-{2^{{\mathit{memarg}}{.}\mathsf{align}}} < n / 8
+{2^{{\mathit{memarg}}{.}\mathsf{align}}} < {\mathit{{\scriptstyle N}}} / 8
  \qquad
-{\mathit{laneidx}} < 128 / n
+i < 128 / {\mathit{{\scriptstyle N}}}
 }{
-{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{store}}{n}{\mathsf{\_}}{\mathsf{lane}}~x~{\mathit{memarg}}~{\mathit{laneidx}} : \mathsf{i{\scriptstyle 32}}~\mathsf{v{\scriptstyle 128}} \rightarrow \epsilon
+{\mathit{{\scriptstyle C}}} \vdash {\mathsf{v{\scriptstyle 128}}{.}\mathsf{store}}{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\mathsf{lane}}~x~{\mathit{memarg}}~i : \mathsf{i{\scriptstyle 32}}~\mathsf{v{\scriptstyle 128}} \rightarrow \epsilon
 } \, {[\textsc{\scriptsize T{-}vstore\_lane}]}
 \qquad
 \end{array}
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index b26ee59e21..62cbb14e56 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -4026,59 +4026,73 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([])))
     -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype)
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1035.1-1038.43
+  rule load-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1040.1-1043.35
+  rule load-pack{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr((Inn : Inn <: numtype), ?((`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1054.1-1057.43
+  rule store-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1040.1-1043.39
-  rule vload{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+  ;; 6-typing.watsup:1059.1-1062.35
+  rule store-pack{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1064.1-1067.46
+  rule vload-val{C : context, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
+
+  ;; 6-typing.watsup:1069.1-1072.39
+  rule vload-pack{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N))
 
-  ;; 6-typing.watsup:1045.1-1048.35
-  rule vload-splat{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1074.1-1077.35
+  rule vload-splat{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8))
 
-  ;; 6-typing.watsup:1050.1-1053.34
-  rule vload-zero{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1079.1-1082.34
+  rule vload-zero{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
 
-  ;; 6-typing.watsup:1055.1-1059.29
-  rule vload_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1084.1-1088.21
+  rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
-  ;; 6-typing.watsup:1061.1-1064.46
+  ;; 6-typing.watsup:1090.1-1093.46
   rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
 
-  ;; 6-typing.watsup:1066.1-1070.29
-  rule vstore_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1095.1-1099.21
+  rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
 ;; 6-typing.watsup:516.1-516.96
 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
@@ -4117,22 +4131,22 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1126.1-1126.86
+;; 6-typing.watsup:1155.1-1155.86
 def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1127.1-1127.42
+  ;; 6-typing.watsup:1156.1-1156.42
   def $in_binop{nt : numtype, binop : binop_(nt), epsilon : binop_(nt)*}(nt, binop, epsilon) = false
-  ;; 6-typing.watsup:1128.1-1128.99
+  ;; 6-typing.watsup:1157.1-1157.99
   def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
 }
 
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1122.1-1122.63
+;; 6-typing.watsup:1151.1-1151.63
 def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1123.1-1123.37
+  ;; 6-typing.watsup:1152.1-1152.37
   def $in_numtype{nt : numtype, epsilon : numtype*}(nt, epsilon) = false
-  ;; 6-typing.watsup:1124.1-1124.68
+  ;; 6-typing.watsup:1153.1-1153.68
   def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
 }
 
@@ -4356,13 +4370,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1269.1-1269.100
+;; 6-typing.watsup:1298.1-1298.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1306.1-1307.17
+  ;; 6-typing.watsup:1335.1-1336.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1309.1-1312.55
+  ;; 6-typing.watsup:1338.1-1341.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -4372,13 +4386,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1268.1-1268.98
+;; 6-typing.watsup:1297.1-1297.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1298.1-1299.17
+  ;; 6-typing.watsup:1327.1-1328.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1301.1-1304.50
+  ;; 6-typing.watsup:1330.1-1333.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, [dt_1])
@@ -9803,59 +9817,73 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([])))
     -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype)
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1035.1-1038.43
+  rule load-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1040.1-1043.35
+  rule load-pack{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr((Inn : Inn <: numtype), ?((`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1054.1-1057.43
+  rule store-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1040.1-1043.39
-  rule vload{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+  ;; 6-typing.watsup:1059.1-1062.35
+  rule store-pack{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1064.1-1067.46
+  rule vload-val{C : context, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
+
+  ;; 6-typing.watsup:1069.1-1072.39
+  rule vload-pack{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N))
 
-  ;; 6-typing.watsup:1045.1-1048.35
-  rule vload-splat{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1074.1-1077.35
+  rule vload-splat{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8))
 
-  ;; 6-typing.watsup:1050.1-1053.34
-  rule vload-zero{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1079.1-1082.34
+  rule vload-zero{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
 
-  ;; 6-typing.watsup:1055.1-1059.29
-  rule vload_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1084.1-1088.21
+  rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
-  ;; 6-typing.watsup:1061.1-1064.46
+  ;; 6-typing.watsup:1090.1-1093.46
   rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
 
-  ;; 6-typing.watsup:1066.1-1070.29
-  rule vstore_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1095.1-1099.21
+  rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
 ;; 6-typing.watsup:516.1-516.96
 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
@@ -9894,22 +9922,22 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1126.1-1126.86
+;; 6-typing.watsup:1155.1-1155.86
 def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1127.1-1127.42
+  ;; 6-typing.watsup:1156.1-1156.42
   def $in_binop{nt : numtype, binop : binop_(nt), epsilon : binop_(nt)*}(nt, binop, epsilon) = false
-  ;; 6-typing.watsup:1128.1-1128.99
+  ;; 6-typing.watsup:1157.1-1157.99
   def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
 }
 
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1122.1-1122.63
+;; 6-typing.watsup:1151.1-1151.63
 def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1123.1-1123.37
+  ;; 6-typing.watsup:1152.1-1152.37
   def $in_numtype{nt : numtype, epsilon : numtype*}(nt, epsilon) = false
-  ;; 6-typing.watsup:1124.1-1124.68
+  ;; 6-typing.watsup:1153.1-1153.68
   def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
 }
 
@@ -10133,13 +10161,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1269.1-1269.100
+;; 6-typing.watsup:1298.1-1298.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1306.1-1307.17
+  ;; 6-typing.watsup:1335.1-1336.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1309.1-1312.55
+  ;; 6-typing.watsup:1338.1-1341.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -10149,13 +10177,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1268.1-1268.98
+;; 6-typing.watsup:1297.1-1297.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1298.1-1299.17
+  ;; 6-typing.watsup:1327.1-1328.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1301.1-1304.50
+  ;; 6-typing.watsup:1330.1-1333.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, [dt_1])
@@ -15580,59 +15608,73 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([])))
     -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype)
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1035.1-1038.43
+  rule load-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1040.1-1043.35
+  rule load-pack{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr((Inn : Inn <: numtype), ?((`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1054.1-1057.43
+  rule store-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1040.1-1043.39
-  rule vload{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+  ;; 6-typing.watsup:1059.1-1062.35
+  rule store-pack{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1064.1-1067.46
+  rule vload-val{C : context, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
+
+  ;; 6-typing.watsup:1069.1-1072.39
+  rule vload-pack{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N))
 
-  ;; 6-typing.watsup:1045.1-1048.35
-  rule vload-splat{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1074.1-1077.35
+  rule vload-splat{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8))
 
-  ;; 6-typing.watsup:1050.1-1053.34
-  rule vload-zero{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1079.1-1082.34
+  rule vload-zero{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
 
-  ;; 6-typing.watsup:1055.1-1059.29
-  rule vload_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1084.1-1088.21
+  rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
-  ;; 6-typing.watsup:1061.1-1064.46
+  ;; 6-typing.watsup:1090.1-1093.46
   rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
 
-  ;; 6-typing.watsup:1066.1-1070.29
-  rule vstore_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1095.1-1099.21
+  rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
 ;; 6-typing.watsup:516.1-516.96
 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
@@ -15671,22 +15713,22 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1126.1-1126.86
+;; 6-typing.watsup:1155.1-1155.86
 def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1127.1-1127.42
+  ;; 6-typing.watsup:1156.1-1156.42
   def $in_binop{nt : numtype, binop : binop_(nt), epsilon : binop_(nt)*}(nt, binop, epsilon) = false
-  ;; 6-typing.watsup:1128.1-1128.99
+  ;; 6-typing.watsup:1157.1-1157.99
   def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
 }
 
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1122.1-1122.63
+;; 6-typing.watsup:1151.1-1151.63
 def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1123.1-1123.37
+  ;; 6-typing.watsup:1152.1-1152.37
   def $in_numtype{nt : numtype, epsilon : numtype*}(nt, epsilon) = false
-  ;; 6-typing.watsup:1124.1-1124.68
+  ;; 6-typing.watsup:1153.1-1153.68
   def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
 }
 
@@ -15910,13 +15952,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1269.1-1269.100
+;; 6-typing.watsup:1298.1-1298.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1306.1-1307.17
+  ;; 6-typing.watsup:1335.1-1336.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1309.1-1312.55
+  ;; 6-typing.watsup:1338.1-1341.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -15926,13 +15968,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1268.1-1268.98
+;; 6-typing.watsup:1297.1-1297.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1298.1-1299.17
+  ;; 6-typing.watsup:1327.1-1328.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1301.1-1304.50
+  ;; 6-typing.watsup:1330.1-1333.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, [dt_1])
@@ -21440,68 +21482,84 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     -- if (x!`%`_idx.0 < |C.DATAS_context|)
     -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype)
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1035.1-1038.43
+  rule load-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((n?{n : n} = ?()) <=> (sx?{sx : sx} = ?()))
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1040.1-1043.35
+  rule load-pack{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr((Inn : Inn <: numtype), ?((`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)])))
+    -- if (x!`%`_idx.0 < |C.MEMS_context|)
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1054.1-1057.43
+  rule store-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if ((n?{n : n} = ?()) \/ (nt = (Inn : Inn <: numtype)))
 
-  ;; 6-typing.watsup:1040.1-1043.39
-  rule vload{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+  ;; 6-typing.watsup:1059.1-1062.35
+  rule store-pack{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([])))
+    -- if (x!`%`_idx.0 < |C.MEMS_context|)
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+
+  ;; 6-typing.watsup:1064.1-1067.46
+  rule vload-val{C : context, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+    -- if (x!`%`_idx.0 < |C.MEMS_context|)
+    -- if (C.MEMS_context[x!`%`_idx.0] = mt)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
+
+  ;; 6-typing.watsup:1069.1-1072.39
+  rule vload-pack{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N))
 
-  ;; 6-typing.watsup:1045.1-1048.35
-  rule vload-splat{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1074.1-1077.35
+  rule vload-splat{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8))
 
-  ;; 6-typing.watsup:1050.1-1053.34
-  rule vload-zero{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1079.1-1082.34
+  rule vload-zero{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
 
-  ;; 6-typing.watsup:1055.1-1059.29
-  rule vload_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1084.1-1088.21
+  rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
-  ;; 6-typing.watsup:1061.1-1064.46
+  ;; 6-typing.watsup:1090.1-1093.46
   rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
 
-  ;; 6-typing.watsup:1066.1-1070.29
-  rule vstore_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1095.1-1099.21
+  rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if (C.MEMS_context[x!`%`_idx.0] = mt)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
 
 ;; 6-typing.watsup:516.1-516.96
 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
@@ -21543,22 +21601,22 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1126.1-1126.86
+;; 6-typing.watsup:1155.1-1155.86
 def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1127.1-1127.42
+  ;; 6-typing.watsup:1156.1-1156.42
   def $in_binop{nt : numtype, binop : binop_(nt), epsilon : binop_(nt)*}(nt, binop, epsilon) = false
-  ;; 6-typing.watsup:1128.1-1128.99
+  ;; 6-typing.watsup:1157.1-1157.99
   def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
 }
 
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1122.1-1122.63
+;; 6-typing.watsup:1151.1-1151.63
 def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1123.1-1123.37
+  ;; 6-typing.watsup:1152.1-1152.37
   def $in_numtype{nt : numtype, epsilon : numtype*}(nt, epsilon) = false
-  ;; 6-typing.watsup:1124.1-1124.68
+  ;; 6-typing.watsup:1153.1-1153.68
   def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
 }
 
@@ -21792,13 +21850,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1269.1-1269.100
+;; 6-typing.watsup:1298.1-1298.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1306.1-1307.17
+  ;; 6-typing.watsup:1335.1-1336.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1309.1-1312.55
+  ;; 6-typing.watsup:1338.1-1341.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -21808,13 +21866,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1268.1-1268.98
+;; 6-typing.watsup:1297.1-1297.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1298.1-1299.17
+  ;; 6-typing.watsup:1327.1-1328.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1301.1-1304.50
+  ;; 6-typing.watsup:1330.1-1333.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, [dt_1])
@@ -27404,86 +27462,83 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     -- if (x!`%`_idx.0 < |C.DATAS_context|)
     -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype)
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load-0{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1035.1-1038.43
+  rule load-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((n?{n : n} = ?()) <=> (sx?{sx : sx} = ?()))
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if (n?{n : n} = ?())
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1026.1-1031.29
-  rule load-1{C : context, nt : numtype, n? : n?, sx? : sx?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, `LOAD%(_)%?%%`_instr(nt, (`%`_sz(n), sx)?{n : nat, sx : sx}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(nt : numtype <: valtype)])))
+  ;; 6-typing.watsup:1040.1-1043.35
+  rule load-pack{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, `LOAD%(_)%?%%`_instr((Inn : Inn <: numtype), ?((`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([(Inn : Inn <: valtype)])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((n?{n : n} = ?()) <=> (sx?{sx : sx} = ?()))
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- where (Inn : Inn <: numtype) = nt
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store-0{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1054.1-1057.43
+  rule store-val{C : context, nt : numtype, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- if (n?{n : n} = ?())
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1033.1-1038.29
-  rule store-1{C : context, nt : numtype, n? : n?, x : idx, memarg : memarg, mt : memtype, Inn : Inn}:
-    `%|-%:%`(C, STORE_instr(nt, `%`_sz(n)?{n : nat}, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (nt : numtype <: valtype)]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1059.1-1062.35
+  rule store-pack{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_sz(M)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype (Inn : Inn <: valtype)]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($size(nt) / 8))
-    -- (if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8)) /\ ((n / 8) < ($size(nt) / 8))))?{n : nat}
-    -- where (Inn : Inn <: numtype) = nt
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (M / 8))
+    -- where mt = C.MEMS_context[x!`%`_idx.0]
+
+  ;; 6-typing.watsup:1064.1-1067.46
+  rule vload-val{C : context, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+    -- if (x!`%`_idx.0 < |C.MEMS_context|)
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1040.1-1043.39
-  rule vload{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
+  ;; 6-typing.watsup:1069.1-1072.39
+  rule vload-pack{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ((M / 8) * N))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1045.1-1048.35
-  rule vload-splat{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1074.1-1077.35
+  rule vload-splat{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= (N / 8))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1050.1-1053.34
-  rule vload-zero{C : context, n : n, x : idx, memarg : memarg, mt : memtype}:
-    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(n))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1079.1-1082.34
+  rule vload-zero{C : context, N : N, x : idx, memarg : memarg, mt : memtype}:
+    `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1055.1-1059.29
-  rule vload_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
+  ;; 6-typing.watsup:1084.1-1088.21
+  rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([V128_valtype])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1061.1-1064.46
+  ;; 6-typing.watsup:1090.1-1093.46
   rule vstore{C : context, x : idx, memarg : memarg, mt : memtype}:
     `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
     -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) <= ($vsize(V128_vectype) / 8))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
-  ;; 6-typing.watsup:1066.1-1070.29
-  rule vstore_lane{C : context, n : n, x : idx, memarg : memarg, laneidx : laneidx, mt : memtype}:
-    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(n), x, memarg, laneidx), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
+  ;; 6-typing.watsup:1095.1-1099.21
+  rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : nat, mt : memtype}:
+    `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, `%`_laneidx(i)), `%->_%%`_instrtype(`%`_resulttype([I32_valtype V128_valtype]), [], `%`_resulttype([])))
     -- if (x!`%`_idx.0 < |C.MEMS_context|)
-    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (n / 8))
-    -- if (laneidx!`%`_laneidx.0 < (128 / n))
+    -- if ((2 ^ memarg.ALIGN_memarg!`%`_u32.0) < (N / 8))
+    -- if (i < (128 / N))
     -- where mt = C.MEMS_context[x!`%`_idx.0]
 
 ;; 6-typing.watsup:516.1-516.96
@@ -27526,22 +27581,22 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1126.1-1126.86
+;; 6-typing.watsup:1155.1-1155.86
 def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1127.1-1127.42
+  ;; 6-typing.watsup:1156.1-1156.42
   def $in_binop{nt : numtype, binop : binop_(nt), epsilon : binop_(nt)*}(nt, binop, epsilon) = false
-  ;; 6-typing.watsup:1128.1-1128.99
+  ;; 6-typing.watsup:1157.1-1157.99
   def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
 }
 
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1122.1-1122.63
+;; 6-typing.watsup:1151.1-1151.63
 def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1123.1-1123.37
+  ;; 6-typing.watsup:1152.1-1152.37
   def $in_numtype{nt : numtype, epsilon : numtype*}(nt, epsilon) = false
-  ;; 6-typing.watsup:1124.1-1124.68
+  ;; 6-typing.watsup:1153.1-1153.68
   def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
 }
 
@@ -27775,13 +27830,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1269.1-1269.100
+;; 6-typing.watsup:1298.1-1298.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1306.1-1307.17
+  ;; 6-typing.watsup:1335.1-1336.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1309.1-1312.55
+  ;; 6-typing.watsup:1338.1-1341.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -27791,13 +27846,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1268.1-1268.98
+;; 6-typing.watsup:1297.1-1297.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1298.1-1299.17
+  ;; 6-typing.watsup:1327.1-1328.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1301.1-1304.50
+  ;; 6-typing.watsup:1330.1-1333.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1 : deftype, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, [dt_1])
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index e434a72891..877bd2d4d1 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -4128,37 +4128,28 @@ validation_of_DATA.DROP x
 - C.DATAS[x] must be equal to OK.
 - The instruction is valid with type ([] ->_ [] ++ []).
 
-validation_of_LOAD nt (n, sx)? x memarg
+validation_of_LOAD nt ?() x memarg
 - |C.MEMS| must be greater than x.
-- ((sx? is ?())) if and only if ((n? is ?())).
 - (2 ^ memarg.ALIGN) must be less than or equal to ($size(nt) / 8).
-- If n is defined,
-  - (2 ^ memarg.ALIGN) must be less than or equal to (n / 8).
-  - (n / 8) must be less than ($size(nt) / 8).
-- n? must be equal to ?().
 - Let mt be C.MEMS[x].
 - The instruction is valid with type ([I32] ->_ [] ++ [nt]).
 
-validation_of_STORE nt n? x memarg
+validation_of_STORE nt ?() x memarg
 - |C.MEMS| must be greater than x.
 - (2 ^ memarg.ALIGN) must be less than or equal to ($size(nt) / 8).
-- If n is defined,
-  - (2 ^ memarg.ALIGN) must be less than or equal to (n / 8).
-  - (n / 8) must be less than ($size(nt) / 8).
-- n? must be equal to ?().
 - Let mt be C.MEMS[x].
 - The instruction is valid with type ([I32, nt] ->_ [] ++ []).
 
-validation_of_VLOAD V128 ?((SHAPE M N sx)) x memarg
+validation_of_VLOAD V128 ?() x memarg
 - |C.MEMS| must be greater than x.
-- (2 ^ memarg.ALIGN) must be less than or equal to ((M / 8) · N).
+- (2 ^ memarg.ALIGN) must be less than or equal to ($vsize(V128) / 8).
 - Let mt be C.MEMS[x].
 - The instruction is valid with type ([I32] ->_ [] ++ [V128]).
 
-validation_of_VLOAD_LANE V128 n x memarg laneidx
+validation_of_VLOAD_LANE V128 N x memarg i
 - |C.MEMS| must be greater than x.
-- (2 ^ memarg.ALIGN) must be less than (n / 8).
-- laneidx must be less than (128 / n).
+- (2 ^ memarg.ALIGN) must be less than (N / 8).
+- i must be less than (128 / N).
 - Let mt be C.MEMS[x].
 - The instruction is valid with type ([I32, V128] ->_ [] ++ [V128]).
 
@@ -4168,10 +4159,10 @@ validation_of_VSTORE V128 x memarg
 - Let mt be C.MEMS[x].
 - The instruction is valid with type ([I32, V128] ->_ [] ++ []).
 
-validation_of_VSTORE_LANE V128 n x memarg laneidx
+validation_of_VSTORE_LANE V128 N x memarg i
 - |C.MEMS| must be greater than x.
-- (2 ^ memarg.ALIGN) must be less than (n / 8).
-- laneidx must be less than (128 / n).
+- (2 ^ memarg.ALIGN) must be less than (N / 8).
+- i must be less than (128 / N).
 - Let mt be C.MEMS[x].
 - The instruction is valid with type ([I32, V128] ->_ [] ++ []).
 
diff --git a/spectec/test-prose/doc/valid/instructions-in.rst b/spectec/test-prose/doc/valid/instructions-in.rst
index 5399cb6134..47ab5071bf 100644
--- a/spectec/test-prose/doc/valid/instructions-in.rst
+++ b/spectec/test-prose/doc/valid/instructions-in.rst
@@ -597,7 +597,8 @@ $${rule-prose: valid/load}
 
 \
 
-$${rule: Instr_ok/load}
+$${rule: Instr_ok/load-val}
+$${rule: Instr_ok/load-pack}
 
 .. _valid-store:
 
@@ -605,7 +606,8 @@ $${rule-prose: valid/store}
 
 \
 
-$${rule: Instr_ok/store}
+$${rule: Instr_ok/store-val}
+$${rule: Instr_ok/store-pack}
 
 .. _valid-vload:
 
@@ -613,7 +615,8 @@ $${rule-prose: valid/vload}
 
 \
 
-$${rule: Instr_ok/vload}
+$${rule: Instr_ok/vload-val}
+$${rule: Instr_ok/vload-pack}
 $${rule: Instr_ok/vload-splat}
 $${rule: Instr_ok/vload-zero}
 
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index d7cdab761a..6ebc196106 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -808,9 +808,12 @@ warning: rule `Instr_ok/memory.fill` was never spliced
 warning: rule `Instr_ok/memory.copy` was never spliced
 warning: rule `Instr_ok/memory.init` was never spliced
 warning: rule `Instr_ok/data.drop` was never spliced
-warning: rule `Instr_ok/load` was never spliced
-warning: rule `Instr_ok/store` was never spliced
-warning: rule `Instr_ok/vload` was never spliced
+warning: rule `Instr_ok/load-val` was never spliced
+warning: rule `Instr_ok/load-pack` was never spliced
+warning: rule `Instr_ok/store-val` was never spliced
+warning: rule `Instr_ok/store-pack` was never spliced
+warning: rule `Instr_ok/vload-val` was never spliced
+warning: rule `Instr_ok/vload-pack` was never spliced
 warning: rule `Instr_ok/vload-splat` was never spliced
 warning: rule `Instr_ok/vload-zero` was never spliced
 warning: rule `Instr_ok/vload_lane` was never spliced