diff --git a/papers/README.md b/papers/README.md
index ecccea677d..9a59614009 100644
--- a/papers/README.md
+++ b/papers/README.md
@@ -13,3 +13,11 @@
   ACM-SIGPLAN Conference on Object-Oriented Programming, Systems, Language and Architectures (OOSPLA 2019)
 
   *Describes and formalises the extension of WebAssembly with threads and a suitable memory model.*
+
+* [Bringing the WebAssembly Standard up to Speed with SpecTec](pldi2024.pdf)
+
+  Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Rao Xiaojia, Conrad Watt, Andreas Rossberg
+
+  ACM-SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024)
+
+  *Describes the design and implementation of Wasm SpecTec.*
diff --git a/papers/pldi2024.pdf b/papers/pldi2024.pdf
new file mode 100644
index 0000000000..a1fc4ef388
Binary files /dev/null and b/papers/pldi2024.pdf differ
diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup
index 9a39bd228f..64b5018412 100644
--- a/spectec/spec/wasm-2.0/1-syntax.watsup
+++ b/spectec/spec/wasm-2.0/1-syntax.watsup
@@ -419,7 +419,7 @@ syntax instr/vec hint(desc "vector instruction") = ...
     ;; TODO: /\ (vextbinop =/= DOT \/ sx = S)
   | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%)
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= 32)
-  | VCVTOP shape vcvtop half? shape sx? zero?
+  | VCVTOP shape shape vcvtop half? sx? zero?
     hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%#_#%)
     ;; TODO: missing constraints
   | ...
diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup
index ad6d66fd90..100c523a76 100644
--- a/spectec/spec/wasm-2.0/6-typing.watsup
+++ b/spectec/spec/wasm-2.0/6-typing.watsup
@@ -354,7 +354,7 @@ rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128
 
 rule Instr_ok/vcvtop:
-  C |- VCVTOP sh_1 vcvtop hf? sh_2 sx? zero? : V128 -> V128
+  C |- VCVTOP sh_1 sh_2 vcvtop hf? sx? zero? : V128 -> V128
 
 
 ;; Local instructions
diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup
index 7a3c859026..e0e8f6951f 100644
--- a/spectec/spec/wasm-2.0/8-reduction.watsup
+++ b/spectec/spec/wasm-2.0/8-reduction.watsup
@@ -323,18 +323,18 @@ rule Step_pure/vnarrow:
 
 
 rule Step_pure/vcvtop-full:
-  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) vcvtop eps (lnn_1 X N_1) sx) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) (lnn_1 X N_1) vcvtop eps sx) ~> (VCONST V128 c)
   -- if c'* = $lanes_(lnn_1 X N_1, c_1)
   -- if c = $invlanes_(lnn_2 X N_2, $vcvtop(lnn_1 X N_1, lnn_2 X N_2, vcvtop, sx, c')*)
 
 var hf : half  ;; TODO: this declaration shouldn't be needed
 rule Step_pure/vcvtop-half:
-  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) vcvtop hf (lnn_1 X N_1) sx?) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (lnn_2 X N_2) (lnn_1 X N_1) vcvtop hf sx?) ~> (VCONST V128 c)
   -- if ci* = $lanes_(lnn_1 X N_1, c_1)[$halfop(hf, 0, N_2) : N_2]
   -- if c = $invlanes_(lnn_2 X N_2, $vcvtop(lnn_1 X N_1, lnn_2 X N_2, vcvtop, sx?, ci)*)
 
 rule Step_pure/vcvtop-zero:
-  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) vcvtop eps (nt_1 X N_1) sx? ZERO) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) (nt_1 X N_1) vcvtop eps sx? ZERO) ~> (VCONST V128 c)
   -- if ci* = $lanes_(nt_1 X N_1, c_1)
   -- if c = $invlanes_(nt_2 X N_2, $vcvtop(nt_1 X N_1, nt_2 X N_2, vcvtop, sx?, ci)* $zero(nt_2)^N_1)
 
diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup
index bb69987199..449e19fd7c 100644
--- a/spectec/spec/wasm-2.0/A-binary.watsup
+++ b/spectec/spec/wasm-2.0/A-binary.watsup
@@ -615,10 +615,10 @@ grammar Binstr/vector-v-i16x8 : instr = ...
   | 0xFD 132:Bu32 => VBITMASK (I16 X 8)
   | 0xFD 133:Bu32 => VNARROW (I16 X 8) (I32 X 4) S
   | 0xFD 134:Bu32 => VNARROW (I16 X 8) (I32 X 4) U
-  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) EXTEND LOW (I8 X 16) S
-  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) EXTEND HIGH (I8 X 16) S
-  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) EXTEND LOW (I8 X 16) U
-  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) EXTEND HIGH (I8 X 16) U
+  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND LOW S
+  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND HIGH S
+  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND LOW U
+  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) (I8 X 16) EXTEND HIGH U
   | 0xFD 139:Bu32 => VSHIFTOP (I16 X 8) SHL
   | 0xFD 140:Bu32 => VSHIFTOP (I16 X 8) (SHR S)
   | 0xFD 141:Bu32 => VSHIFTOP (I16 X 8) (SHR U)
@@ -647,10 +647,10 @@ grammar Binstr/vector-v-i32x4 : instr = ...
   | 0xFD 161:Bu32 => VUNOP (I32 X 4) NEG
   | 0xFD 163:Bu32 => VTESTOP (I32 X 4) ALL_TRUE
   | 0xFD 164:Bu32 => VBITMASK (I32 X 4)
-  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) EXTEND LOW (I16 X 8) S
-  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) EXTEND HIGH (I16 X 8) S
-  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) EXTEND LOW (I16 X 8) U
-  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) EXTEND HIGH (I16 X 8) U
+  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND LOW S
+  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND HIGH S
+  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND LOW U
+  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) (I16 X 8) EXTEND HIGH U
   | 0xFD 171:Bu32 => VSHIFTOP (I32 X 4) SHL
   | 0xFD 172:Bu32 => VSHIFTOP (I32 X 4) (SHR S)
   | 0xFD 173:Bu32 => VSHIFTOP (I32 X 4) (SHR U)
@@ -673,10 +673,10 @@ grammar Binstr/vector-v-i64x2 : instr = ...
   | 0xFD 193:Bu32 => VUNOP (I64 X 2) NEG
   | 0xFD 195:Bu32 => VTESTOP (I64 X 2) ALL_TRUE
   | 0xFD 196:Bu32 => VBITMASK (I64 X 2)
-  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) EXTEND LOW (I32 X 4) S
-  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) EXTEND HIGH (I32 X 4) S
-  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) EXTEND LOW (I32 X 4) U
-  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) EXTEND HIGH (I32 X 4) U
+  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND LOW S
+  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND HIGH S
+  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND LOW U
+  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) (I32 X 4) EXTEND HIGH U
   | 0xFD 203:Bu32 => VSHIFTOP (I64 X 2) SHL
   | 0xFD 204:Bu32 => VSHIFTOP (I64 X 2) (SHR S)
   | 0xFD 205:Bu32 => VSHIFTOP (I64 X 2) (SHR U)
@@ -726,16 +726,16 @@ grammar Binstr/vector-v-f64x2 : instr = ...
   | ...
 
 grammar Binstr/vector-cvt : instr = ...
-  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F32 X 4) S
-  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F32 X 4) U
-  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) CONVERT (I32 X 4) S
-  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) CONVERT (I32 X 4) U
-  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F64 X 2) S ZERO
-  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) TRUNC_SAT (F64 X 2) U ZERO
-  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) S
-  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) CONVERT LOW (I32 X 4) U
-  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) DEMOTE (F64 X 2) ZERO
-  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) PROMOTE LOW (F32 X 4)
+  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) (F32 X 4) TRUNC_SAT S
+  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) (F32 X 4) TRUNC_SAT U
+  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) (I32 X 4) CONVERT S
+  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) (I32 X 4) CONVERT U
+  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) (F64 X 2) TRUNC_SAT S ZERO
+  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) (F64 X 2) TRUNC_SAT U ZERO
+  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) (I32 X 4) CONVERT LOW S
+  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) (I32 X 4) CONVERT LOW U
+  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) (F64 X 2) DEMOTE ZERO
+  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) (F32 X 4) PROMOTE LOW
 
 
 ;; Expressions
diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml
index 780b0f8a30..ddf8f29996 100644
--- a/spectec/src/il2al/il2il.ml
+++ b/spectec/src/il2al/il2il.ml
@@ -107,66 +107,72 @@ let _unified_idx = ref 0
 let init_unified_idx () = _unified_idx := 0
 let get_unified_idx () = let i = !_unified_idx in _unified_idx := (i+1); i
 let gen_new_unified ty = (type_to_id ty) ^ "_" ^ unified_prefix ^ (string_of_int (get_unified_idx())) $ no_region
-let to_iter e iterexp = IterE (e, iterexp)
 let is_unified_id id = String.split_on_char '_' id |> Util.Lib.List.last |> String.starts_with ~prefix:unified_prefix
 
 let rec overlap e1 e2 = if eq_exp e1 e2 then e1 else
-  let it =
-    match e1.it, e2.it with
-    | VarE id, _
-    | IterE ({ it = VarE id; _}, _) , _
-      when is_unified_id id.it -> e1.it
+  let replace_it it = { e1 with it = it } in
+  match e1.it, e2.it with
+    (* Already unified *)
+    | VarE id, _ when is_unified_id id.it ->
+      e1
+    | IterE ({ it = VarE id; _} as e, (iter, _)), _  when is_unified_id id.it ->
+      let t = overlap_typ e1.note e2.note in
+      let i = (iter, [(id, t)]) in
+      { e1 with it = IterE (e, i); note = t }
+    (* Not unified *)
     | UnE (unop1, e1), UnE (unop2, e2) when unop1 = unop2 ->
-      UnE (unop1, overlap e1 e2)
+      UnE (unop1, overlap e1 e2) |> replace_it
     | BinE (binop1, e1, e1'), BinE (binop2, e2, e2') when binop1 = binop2 ->
-      BinE (binop1, overlap e1 e2, overlap e1' e2')
+      BinE (binop1, overlap e1 e2, overlap e1' e2') |> replace_it
     | CmpE (cmpop1, e1, e1'), CmpE (cmpop2, e2, e2') when cmpop1 = cmpop2 ->
-      CmpE (cmpop1, overlap e1 e2, overlap e1' e2')
+      CmpE (cmpop1, overlap e1 e2, overlap e1' e2') |> replace_it
     | IdxE (e1, e1'), IdxE (e2, e2') ->
-      IdxE (overlap e1 e2, overlap e1' e2')
+      IdxE (overlap e1 e2, overlap e1' e2') |> replace_it
     | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') ->
-      SliceE (overlap e1 e2, overlap e1' e2', overlap e1'' e2'')
+      SliceE (overlap e1 e2, overlap e1' e2', overlap e1'' e2'') |> replace_it
     | UpdE (e1, path1, e1'), UpdE (e2, path2, e2') when eq_path path1 path2 ->
-      UpdE (overlap e1 e2, path1, overlap e1' e2')
+      UpdE (overlap e1 e2, path1, overlap e1' e2') |> replace_it
     | ExtE (e1, path1, e1'), ExtE (e2, path2, e2') when eq_path path1 path2 ->
-      ExtE (overlap e1 e2, path1, overlap e1' e2')
+      ExtE (overlap e1 e2, path1, overlap e1' e2') |> replace_it
     | StrE efs1, StrE efs2 when List.map fst efs1 = List.map fst efs2 ->
-      StrE (List.map2 (fun (a1, e1) (_, e2) -> (a1, overlap e1 e2)) efs1 efs2)
+      StrE (List.map2 (fun (a1, e1) (_, e2) -> (a1, overlap e1 e2)) efs1 efs2) |> replace_it
     | DotE (e1, atom1), DotE (e2, atom2) when eq_atom atom1 atom2 ->
-      DotE (overlap e1 e2, atom1)
+      DotE (overlap e1 e2, atom1) |> replace_it
     | CompE (e1, e1'), CompE (e2, e2') ->
-      CompE (overlap e1 e2, overlap e1' e2')
+      CompE (overlap e1 e2, overlap e1' e2') |> replace_it
     | LenE e1, LenE e2 ->
-      LenE (overlap e1 e2)
+      LenE (overlap e1 e2) |> replace_it
     | TupE es1, TupE es2 when List.length es1 = List.length es2 ->
-      TupE (List.map2 overlap es1 es2)
+      TupE (List.map2 overlap es1 es2) |> replace_it
     | CallE (id1, as1), CallE (id2, as2) when eq_id id1 id2 ->
-      CallE (id1, List.map2 overlap_arg as1 as2)
+      CallE (id1, List.map2 overlap_arg as1 as2) |> replace_it
     | IterE (e1, itere1), IterE (e2, itere2) when eq_iterexp itere1 itere2 ->
-      IterE (overlap e1 e2, itere1)
+      IterE (overlap e1 e2, itere1) |> replace_it
     | ProjE (e1, i1), ProjE (e2, i2) when i1 = i2 ->
-      ProjE (overlap e1 e2, i1)
+      ProjE (overlap e1 e2, i1) |> replace_it
     | UncaseE (e1, op1), UncaseE (e2, op2) when eq_mixop op1 op2 ->
-      UncaseE (overlap e1 e2, op1)
+      UncaseE (overlap e1 e2, op1) |> replace_it
     | OptE (Some e1), OptE (Some e2) ->
-      OptE (Some (overlap e1 e2))
+      OptE (Some (overlap e1 e2)) |> replace_it
     | TheE e1, TheE e2 ->
-      TheE (overlap e1 e2)
+      TheE (overlap e1 e2) |> replace_it
     | ListE es1, ListE es2 when List.length es1 = List.length es2 ->
-      ListE (List.map2 overlap es1 es2)
+      ListE (List.map2 overlap es1 es2) |> replace_it
     | CatE (e1, e1'), CatE (e2, e2') ->
-      CatE (overlap e1 e2, overlap e1' e2')
+      CatE (overlap e1 e2, overlap e1' e2') |> replace_it
     | CaseE (mixop1, e1), CaseE (mixop2, e2) when eq_mixop mixop1 mixop2 ->
-      CaseE (mixop1, overlap e1 e2)
+      CaseE (mixop1, overlap e1 e2) |> replace_it
     | SubE (e1, typ1, typ1'), SubE (e2, typ2, typ2') when eq_typ typ1 typ2 && eq_typ typ1' typ2' ->
-      SubE (overlap e1 e2, typ1, typ1')
+      SubE (overlap e1 e2, typ1, typ1') |> replace_it
     | _ ->
-      let ty = e1.note in
+      let ty = overlap_typ e1.note e2.note in
       let id = gen_new_unified ty in
-      match ty.it with
-      | IterT (ty, iter) -> to_iter (VarE id $$ no_region % ty) (iter, [(id, ty)])
-      | _ -> VarE id
-  in { e1 with it }
+      let it =
+        match ty.it with
+        | IterT (ty, iter) -> IterE (VarE id $$ no_region % ty, (iter, [(id, ty)]))
+        | _ -> VarE id
+      in
+      { e1 with it = it; note = ty }
 
 and overlap_arg a1 a2 = if eq_arg a1 a2 then a1 else
   (match a1.it, a2.it with
@@ -175,6 +181,17 @@ and overlap_arg a1 a2 = if eq_arg a1 a2 then a1 else
     | _, _ -> assert false
   ) $ a1.at
 
+and overlap_typ t1 t2 = if eq_typ t1 t2 then t1 else
+  (match t1.it, t2.it with
+    | VarT (id1, args1), VarT (id2, args2) when id1 = id2 ->
+      VarT (id1, List.map2 overlap_arg args1 args2)
+    | TupT ets1, TupT ets2 when List.for_all2 (fun (e1, _) (e2, _) -> eq_exp e1 e2) ets1 ets2 ->
+      TupT (List.map2 (fun (e1, t1) (_, t2) -> (e1, overlap_typ t1 t2)) ets1 ets2)
+    | IterT (t1, iter1), IterT (t2, iter2) when eq_iter iter1 iter2 ->
+      IterT (overlap_typ t1 t2, iter1)
+    | _ -> assert false (* Unreachable due to IL validation *)
+  ) $ t1.at
+
 let pairwise_concat (a,b) (c,d) = (a@c, b@d)
 
 let rec collect_unified template e = if eq_exp template e then [], [] else
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index e988beaa39..2638416221 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -288,79 +288,79 @@ invsigned N ii
 1. Let j be $inverse_of_signed(N, ii).
 2. Return j.
 
-unop valty_u1 unop__u0 val__u2
+unop valty_u1 unop__u0 val__u3
 1. If (unop__u0 is CLZ), then:
-  a. Let iN be val__u2.
+  a. Let iN be val__u3.
   b. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$iclz($size(inn), iN)].
 2. If (unop__u0 is CTZ), then:
-  a. Let iN be val__u2.
+  a. Let iN be val__u3.
   b. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$ictz($size(inn), iN)].
 3. If (unop__u0 is POPCNT), then:
-  a. Let iN be val__u2.
+  a. Let iN be val__u3.
   b. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$ipopcnt($size(inn), iN)].
 4. If (unop__u0 is ABS), then:
-  a. Let fN be val__u2.
+  a. Let fN be val__u3.
   b. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fabs($size(fnn), fN)].
 5. If (unop__u0 is NEG), then:
-  a. Let fN be val__u2.
+  a. Let fN be val__u3.
   b. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fneg($size(fnn), fN)].
 6. If (unop__u0 is SQRT), then:
-  a. Let fN be val__u2.
+  a. Let fN be val__u3.
   b. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fsqrt($size(fnn), fN)].
 7. If (unop__u0 is CEIL), then:
-  a. Let fN be val__u2.
+  a. Let fN be val__u3.
   b. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fceil($size(fnn), fN)].
 8. If (unop__u0 is FLOOR), then:
-  a. Let fN be val__u2.
+  a. Let fN be val__u3.
   b. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$ffloor($size(fnn), fN)].
 9. If (unop__u0 is TRUNC), then:
-  a. Let fN be val__u2.
+  a. Let fN be val__u3.
   b. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$ftrunc($size(fnn), fN)].
 10. Assert: Due to validation, (unop__u0 is NEAREST).
-11. Let fN be val__u2.
+11. Let fN be val__u3.
 12. Assert: Due to validation, the type of valty_u1 is fnn.
 13. Let fnn be valty_u1.
 14. Return [$fnearest($size(fnn), fN)].
 
-binop valty_u1 binop_u0 val__u2 val__u3
+binop valty_u1 binop_u0 val__u3 val__u5
 1. If (binop_u0 is ADD), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$iadd($size(inn), iN_1, iN_2)].
 2. If (binop_u0 is SUB), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$isub($size(inn), iN_1, iN_2)].
 3. If (binop_u0 is MUL), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$imul($size(inn), iN_1, iN_2)].
-4. Let iN_1 be val__u2.
-5. Let iN_2 be val__u3.
+4. Let iN_1 be val__u3.
+5. Let iN_2 be val__u5.
 6. If the type of valty_u1 is inn, then:
   a. Let inn be valty_u1.
   b. If binop_u0 is of the case DIV, then:
@@ -370,87 +370,87 @@ binop valty_u1 binop_u0 val__u2 val__u3
     1) Let (REM sx) be binop_u0.
     2) Return [$irem($size(inn), sx, iN_1, iN_2)].
 7. If (binop_u0 is AND), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$iand($size(inn), iN_1, iN_2)].
 8. If (binop_u0 is OR), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$ior($size(inn), iN_1, iN_2)].
 9. If (binop_u0 is XOR), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$ixor($size(inn), iN_1, iN_2)].
 10. If (binop_u0 is SHL), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$ishl($size(inn), iN_1, iN_2)].
-11. Let iN_1 be val__u2.
-12. Let iN_2 be val__u3.
+11. Let iN_1 be val__u3.
+12. Let iN_2 be val__u5.
 13. If the type of valty_u1 is inn, then:
   a. Let inn be valty_u1.
   b. If binop_u0 is of the case SHR, then:
     1) Let (SHR sx) be binop_u0.
     2) Return [$ishr($size(inn), sx, iN_1, iN_2)].
 14. If (binop_u0 is ROTL), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$irotl($size(inn), iN_1, iN_2)].
 15. If (binop_u0 is ROTR), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return [$irotr($size(inn), iN_1, iN_2)].
 16. If (binop_u0 is ADD), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fadd($size(fnn), fN_1, fN_2)].
 17. If (binop_u0 is SUB), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fsub($size(fnn), fN_1, fN_2)].
 18. If (binop_u0 is MUL), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fmul($size(fnn), fN_1, fN_2)].
 19. If (binop_u0 is DIV), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fdiv($size(fnn), fN_1, fN_2)].
 20. If (binop_u0 is MIN), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fmin($size(fnn), fN_1, fN_2)].
 21. If (binop_u0 is MAX), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return [$fmax($size(fnn), fN_1, fN_2)].
 22. Assert: Due to validation, (binop_u0 is COPYSIGN).
-23. Let fN_1 be val__u2.
-24. Let fN_2 be val__u3.
+23. Let fN_1 be val__u3.
+24. Let fN_2 be val__u5.
 25. Assert: Due to validation, the type of valty_u1 is fnn.
 26. Let fnn be valty_u1.
 27. Return [$fcopysign($size(fnn), fN_1, fN_2)].
@@ -458,21 +458,21 @@ binop valty_u1 binop_u0 val__u2 val__u3
 testop inn EQZ iN
 1. Return $ieqz($size(inn), iN).
 
-relop valty_u1 relop_u0 val__u2 val__u3
+relop valty_u1 relop_u0 val__u3 val__u5
 1. If (relop_u0 is EQ), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return $ieq($size(inn), iN_1, iN_2).
 2. If (relop_u0 is NE), then:
-  a. Let iN_1 be val__u2.
-  b. Let iN_2 be val__u3.
+  a. Let iN_1 be val__u3.
+  b. Let iN_2 be val__u5.
   c. If the type of valty_u1 is inn, then:
     1) Let inn be valty_u1.
     2) Return $ine($size(inn), iN_1, iN_2).
-3. Let iN_1 be val__u2.
-4. Let iN_2 be val__u3.
+3. Let iN_1 be val__u3.
+4. Let iN_2 be val__u5.
 5. If the type of valty_u1 is inn, then:
   a. Let inn be valty_u1.
   b. If relop_u0 is of the case LT, then:
@@ -488,53 +488,53 @@ relop valty_u1 relop_u0 val__u2 val__u3
     1) Let (GE sx) be relop_u0.
     2) Return $ige($size(inn), sx, iN_1, iN_2).
 6. If (relop_u0 is EQ), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return $feq($size(fnn), fN_1, fN_2).
 7. If (relop_u0 is NE), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return $fne($size(fnn), fN_1, fN_2).
 8. If (relop_u0 is LT), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return $flt($size(fnn), fN_1, fN_2).
 9. If (relop_u0 is GT), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return $fgt($size(fnn), fN_1, fN_2).
 10. If (relop_u0 is LE), then:
-  a. Let fN_1 be val__u2.
-  b. Let fN_2 be val__u3.
+  a. Let fN_1 be val__u3.
+  b. Let fN_2 be val__u5.
   c. If the type of valty_u1 is fnn, then:
     1) Let fnn be valty_u1.
     2) Return $fle($size(fnn), fN_1, fN_2).
 11. Assert: Due to validation, (relop_u0 is GE).
-12. Let fN_1 be val__u2.
-13. Let fN_2 be val__u3.
+12. Let fN_1 be val__u3.
+13. Let fN_2 be val__u5.
 14. Assert: Due to validation, the type of valty_u1 is fnn.
 15. Let fnn be valty_u1.
 16. Return $fge($size(fnn), fN_1, fN_2).
 
-cvtop valty_u0 valty_u1 cvtop_u4 sx_u2? val__u3
-1. If ((valty_u0 is I32) and ((valty_u1 is I64) and (cvtop_u4 is CONVERT))), then:
-  a. Let iN be val__u3.
+cvtop valty_u0 valty_u1 cvtop_u5 sx_u2? val__u4
+1. If ((valty_u0 is I32) and ((valty_u1 is I64) and (cvtop_u5 is CONVERT))), then:
+  a. Let iN be val__u4.
   b. If sx_u2? is defined, then:
     1) Let ?(sx) be sx_u2?.
     2) Return [$ext(32, 64, sx, iN)].
-2. If ((valty_u0 is I64) and ((valty_u1 is I32) and (cvtop_u4 is CONVERT))), then:
-  a. Let iN be val__u3.
+2. If ((valty_u0 is I64) and ((valty_u1 is I32) and (cvtop_u5 is CONVERT))), then:
+  a. Let iN be val__u4.
   b. Return [$wrap(64, 32, iN)].
-3. If (cvtop_u4 is CONVERT), then:
-  a. Let fN be val__u3.
+3. If (cvtop_u5 is CONVERT), then:
+  a. Let fN be val__u4.
   b. If the type of valty_u0 is fnn, then:
     1) Let fnn be valty_u0.
     2) If the type of valty_u1 is inn, then:
@@ -542,29 +542,29 @@ cvtop valty_u0 valty_u1 cvtop_u4 sx_u2? val__u3
       b) If sx_u2? is defined, then:
         1. Let ?(sx) be sx_u2?.
         2. Return [$trunc($size(fnn), $size(inn), sx, fN)].
-4. If ((valty_u0 is F32) and ((valty_u1 is F64) and (cvtop_u4 is CONVERT))), then:
-  a. Let fN be val__u3.
+4. If ((valty_u0 is F32) and ((valty_u1 is F64) and (cvtop_u5 is CONVERT))), then:
+  a. Let fN be val__u4.
   b. Return [$promote(32, 64, fN)].
-5. If ((valty_u0 is F64) and ((valty_u1 is F32) and (cvtop_u4 is CONVERT))), then:
-  a. Let fN be val__u3.
+5. If ((valty_u0 is F64) and ((valty_u1 is F32) and (cvtop_u5 is CONVERT))), then:
+  a. Let fN be val__u4.
   b. Return [$demote(64, 32, fN)].
-6. If ((cvtop_u4 is CONVERT) and the type of valty_u1 is fnn), then:
+6. If ((cvtop_u5 is CONVERT) and the type of valty_u1 is fnn), then:
   a. Let fnn be valty_u1.
-  b. Let iN be val__u3.
+  b. Let iN be val__u4.
   c. If the type of valty_u0 is inn, then:
     1) Let inn be valty_u0.
     2) If sx_u2? is defined, then:
       a) Let ?(sx) be sx_u2?.
       b) Return [$convert($size(inn), $size(fnn), sx, iN)].
-7. Assert: Due to validation, (cvtop_u4 is REINTERPRET).
+7. Assert: Due to validation, (cvtop_u5 is REINTERPRET).
 8. If the type of valty_u1 is fnn, then:
   a. Let fnn be valty_u1.
-  b. Let iN be val__u3.
+  b. Let iN be val__u4.
   c. If the type of valty_u0 is inn, then:
     1) Let inn be valty_u0.
     2) If ($size(inn) is $size(fnn)), then:
       a) Return [$reinterpret(inn, fnn, iN)].
-9. Let fN be val__u3.
+9. Let fN be val__u4.
 10. Assert: Due to validation, the type of valty_u0 is fnn.
 11. Let fnn be valty_u0.
 12. Assert: Due to validation, the type of valty_u1 is inn.
@@ -1420,7 +1420,7 @@ validation_of_VEXTBINOP sh_1 sh_2 vextbinop sx
 validation_of_VNARROW sh_1 sh_2 sx
 - The instruction is valid with type ([V128, V128] -> [V128]).
 
-validation_of_VCVTOP sh_1 vcvtop hf? sh_2 sx? zero?
+validation_of_VCVTOP sh_1 sh_2 vcvtop hf? sx? zero?
 - The instruction is valid with type ([V128] -> [V128]).
 
 validation_of_LOCAL.GET x
@@ -1790,85 +1790,85 @@ invsigned N i
 1. Let j be $inverse_of_signed(N, i).
 2. Return j.
 
-unop numty_u1 unop__u0 num__u2
+unop numty_u1 unop__u0 num__u3
 1. If (unop__u0 is CLZ), then:
-  a. Let iN be num__u2.
+  a. Let iN be num__u3.
   b. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$iclz($size(inn), iN)].
 2. If (unop__u0 is CTZ), then:
-  a. Let iN be num__u2.
+  a. Let iN be num__u3.
   b. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ictz($size(inn), iN)].
 3. If (unop__u0 is POPCNT), then:
-  a. Let iN be num__u2.
+  a. Let iN be num__u3.
   b. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ipopcnt($size(inn), iN)].
 4. If unop__u0 is of the case EXTEND, then:
   a. Let (EXTEND N) be unop__u0.
-  b. Let iN be num__u2.
+  b. Let iN be num__u3.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ext(N, $size(inn), S, $wrap($size(inn), N, iN))].
 5. If (unop__u0 is ABS), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fabs($size(fnn), fN)].
 6. If (unop__u0 is NEG), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fneg($size(fnn), fN)].
 7. If (unop__u0 is SQRT), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fsqrt($size(fnn), fN)].
 8. If (unop__u0 is CEIL), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fceil($size(fnn), fN)].
 9. If (unop__u0 is FLOOR), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$ffloor($size(fnn), fN)].
 10. If (unop__u0 is TRUNC), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$ftrunc($size(fnn), fN)].
 11. Assert: Due to validation, (unop__u0 is NEAREST).
-12. Let fN be num__u2.
+12. Let fN be num__u3.
 13. Assert: Due to validation, the type of numty_u1 is fnn.
 14. Let fnn be numty_u1.
 15. Return [$fnearest($size(fnn), fN)].
 
-binop numty_u1 binop_u0 num__u2 num__u3
+binop numty_u1 binop_u0 num__u3 num__u5
 1. If (binop_u0 is ADD), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$iadd($size(inn), iN_1, iN_2)].
 2. If (binop_u0 is SUB), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$isub($size(inn), iN_1, iN_2)].
 3. If (binop_u0 is MUL), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$imul($size(inn), iN_1, iN_2)].
-4. Let iN_1 be num__u2.
-5. Let iN_2 be num__u3.
+4. Let iN_1 be num__u3.
+5. Let iN_2 be num__u5.
 6. If the type of numty_u1 is inn, then:
   a. Let inn be numty_u1.
   b. If binop_u0 is of the case DIV, then:
@@ -1878,87 +1878,87 @@ binop numty_u1 binop_u0 num__u2 num__u3
     1) Let (REM sx) be binop_u0.
     2) Return [$irem($size(inn), sx, iN_1, iN_2)].
 7. If (binop_u0 is AND), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$iand($size(inn), iN_1, iN_2)].
 8. If (binop_u0 is OR), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ior($size(inn), iN_1, iN_2)].
 9. If (binop_u0 is XOR), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ixor($size(inn), iN_1, iN_2)].
 10. If (binop_u0 is SHL), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ishl($size(inn), iN_1, iN_2)].
-11. Let iN_1 be num__u2.
-12. Let iN_2 be num__u3.
+11. Let iN_1 be num__u3.
+12. Let iN_2 be num__u5.
 13. If the type of numty_u1 is inn, then:
   a. Let inn be numty_u1.
   b. If binop_u0 is of the case SHR, then:
     1) Let (SHR sx) be binop_u0.
     2) Return [$ishr($size(inn), sx, iN_1, iN_2)].
 14. If (binop_u0 is ROTL), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$irotl($size(inn), iN_1, iN_2)].
 15. If (binop_u0 is ROTR), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$irotr($size(inn), iN_1, iN_2)].
 16. If (binop_u0 is ADD), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fadd($size(fnn), fN_1, fN_2)].
 17. If (binop_u0 is SUB), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fsub($size(fnn), fN_1, fN_2)].
 18. If (binop_u0 is MUL), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fmul($size(fnn), fN_1, fN_2)].
 19. If (binop_u0 is DIV), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fdiv($size(fnn), fN_1, fN_2)].
 20. If (binop_u0 is MIN), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fmin($size(fnn), fN_1, fN_2)].
 21. If (binop_u0 is MAX), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fmax($size(fnn), fN_1, fN_2)].
 22. Assert: Due to validation, (binop_u0 is COPYSIGN).
-23. Let fN_1 be num__u2.
-24. Let fN_2 be num__u3.
+23. Let fN_1 be num__u3.
+24. Let fN_2 be num__u5.
 25. Assert: Due to validation, the type of numty_u1 is fnn.
 26. Let fnn be numty_u1.
 27. Return [$fcopysign($size(fnn), fN_1, fN_2)].
@@ -1966,21 +1966,21 @@ binop numty_u1 binop_u0 num__u2 num__u3
 testop inn EQZ iN
 1. Return $ieqz($size(inn), iN).
 
-relop numty_u1 relop_u0 num__u2 num__u3
+relop numty_u1 relop_u0 num__u3 num__u5
 1. If (relop_u0 is EQ), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return $ieq($size(inn), iN_1, iN_2).
 2. If (relop_u0 is NE), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return $ine($size(inn), iN_1, iN_2).
-3. Let iN_1 be num__u2.
-4. Let iN_2 be num__u3.
+3. Let iN_1 be num__u3.
+4. Let iN_2 be num__u5.
 5. If the type of numty_u1 is inn, then:
   a. Let inn be numty_u1.
   b. If relop_u0 is of the case LT, then:
@@ -1996,53 +1996,53 @@ relop numty_u1 relop_u0 num__u2 num__u3
     1) Let (GE sx) be relop_u0.
     2) Return $ige($size(inn), sx, iN_1, iN_2).
 6. If (relop_u0 is EQ), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $feq($size(fnn), fN_1, fN_2).
 7. If (relop_u0 is NE), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $fne($size(fnn), fN_1, fN_2).
 8. If (relop_u0 is LT), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $flt($size(fnn), fN_1, fN_2).
 9. If (relop_u0 is GT), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $fgt($size(fnn), fN_1, fN_2).
 10. If (relop_u0 is LE), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $fle($size(fnn), fN_1, fN_2).
 11. Assert: Due to validation, (relop_u0 is GE).
-12. Let fN_1 be num__u2.
-13. Let fN_2 be num__u3.
+12. Let fN_1 be num__u3.
+13. Let fN_2 be num__u5.
 14. Assert: Due to validation, the type of numty_u1 is fnn.
 15. Let fnn be numty_u1.
 16. Return $fge($size(fnn), fN_1, fN_2).
 
-cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
-1. If ((numty_u0 is I32) and ((numty_u1 is I64) and (cvtop_u4 is CONVERT))), then:
-  a. Let iN be num__u3.
+cvtop numty_u0 numty_u1 cvtop_u5 sx_u2? num__u4
+1. If ((numty_u0 is I32) and ((numty_u1 is I64) and (cvtop_u5 is CONVERT))), then:
+  a. Let iN be num__u4.
   b. If sx_u2? is defined, then:
     1) Let ?(sx) be sx_u2?.
     2) Return [$ext(32, 64, sx, iN)].
-2. If ((numty_u0 is I64) and ((numty_u1 is I32) and (cvtop_u4 is CONVERT))), then:
-  a. Let iN be num__u3.
+2. If ((numty_u0 is I64) and ((numty_u1 is I32) and (cvtop_u5 is CONVERT))), then:
+  a. Let iN be num__u4.
   b. Return [$wrap(64, 32, iN)].
-3. If (cvtop_u4 is CONVERT), then:
-  a. Let fN be num__u3.
+3. If (cvtop_u5 is CONVERT), then:
+  a. Let fN be num__u4.
   b. If the type of numty_u0 is fnn, then:
     1) Let fnn be numty_u0.
     2) If the type of numty_u1 is inn, then:
@@ -2050,8 +2050,8 @@ cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
       b) If sx_u2? is defined, then:
         1. Let ?(sx) be sx_u2?.
         2. Return [$trunc($size(fnn), $size(inn), sx, fN)].
-4. If (cvtop_u4 is CONVERT_SAT), then:
-  a. Let fN be num__u3.
+4. If (cvtop_u5 is CONVERT_SAT), then:
+  a. Let fN be num__u4.
   b. If the type of numty_u0 is fnn, then:
     1) Let fnn be numty_u0.
     2) If the type of numty_u1 is inn, then:
@@ -2059,16 +2059,16 @@ cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
       b) If sx_u2? is defined, then:
         1. Let ?(sx) be sx_u2?.
         2. Return [$trunc_sat($size(fnn), $size(inn), sx, fN)].
-5. If ((numty_u0 is F32) and ((numty_u1 is F64) and (cvtop_u4 is CONVERT))), then:
-  a. Let fN be num__u3.
+5. If ((numty_u0 is F32) and ((numty_u1 is F64) and (cvtop_u5 is CONVERT))), then:
+  a. Let fN be num__u4.
   b. Return [$promote(32, 64, fN)].
-6. If ((numty_u0 is F64) and ((numty_u1 is F32) and (cvtop_u4 is CONVERT))), then:
-  a. Let fN be num__u3.
+6. If ((numty_u0 is F64) and ((numty_u1 is F32) and (cvtop_u5 is CONVERT))), then:
+  a. Let fN be num__u4.
   b. Return [$demote(64, 32, fN)].
-7. Assert: Due to validation, (cvtop_u4 is CONVERT).
+7. Assert: Due to validation, (cvtop_u5 is CONVERT).
 8. If the type of numty_u1 is fnn, then:
   a. Let fnn be numty_u1.
-  b. Let iN be num__u3.
+  b. Let iN be num__u4.
   c. If the type of numty_u0 is inn, then:
     1) Let inn be numty_u0.
     2) If sx_u2? is defined, then:
@@ -2076,7 +2076,7 @@ cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
       b) Return [$convert($size(inn), $size(fnn), sx, iN)].
     3) If ($size(inn) is $size(fnn)), then:
       a) Return [$reinterpret(inn, fnn, iN)].
-9. Let fN be num__u3.
+9. Let fN be num__u4.
 10. Assert: Due to validation, the type of numty_u0 is fnn.
 11. Let fnn be numty_u0.
 12. Assert: Due to validation, the type of numty_u1 is inn.
@@ -2387,59 +2387,59 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
 16. Let v128 be $invlanes_((inn X N), lane_3*).
 17. Return v128.
 
-vcvtop (lanet_u0 X N_1) (lanet_u1 X N_2) vcvto_u3 sx_u4? lane__u2
-1. If ((lanet_u0 is I8) and ((lanet_u1 is I16) and (vcvto_u3 is EXTEND))), then:
-  a. Let i8 be lane__u2.
-  b. If sx_u4? is defined, then:
-    1) Let ?(sx) be sx_u4?.
+vcvtop (lanet_u0 X N_1) (lanet_u1 X N_2) vcvto_u4 sx_u5? lane__u3
+1. If ((lanet_u0 is I8) and ((lanet_u1 is I16) and (vcvto_u4 is EXTEND))), then:
+  a. Let i8 be lane__u3.
+  b. If sx_u5? is defined, then:
+    1) Let ?(sx) be sx_u5?.
     2) Let i16 be $ext(8, 16, sx, i8).
     3) Return i16.
-2. If ((lanet_u0 is I16) and ((lanet_u1 is I32) and (vcvto_u3 is EXTEND))), then:
-  a. Let i16 be lane__u2.
-  b. If sx_u4? is defined, then:
-    1) Let ?(sx) be sx_u4?.
+2. If ((lanet_u0 is I16) and ((lanet_u1 is I32) and (vcvto_u4 is EXTEND))), then:
+  a. Let i16 be lane__u3.
+  b. If sx_u5? is defined, then:
+    1) Let ?(sx) be sx_u5?.
     2) Let i32 be $ext(16, 32, sx, i16).
     3) Return i32.
 3. If (lanet_u0 is I32), then:
-  a. If ((lanet_u1 is I64) and (vcvto_u3 is EXTEND)), then:
-    1) Let i32 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  a. If ((lanet_u1 is I64) and (vcvto_u4 is EXTEND)), then:
+    1) Let i32 be lane__u3.
+    2) If sx_u5? is defined, then:
+      a) Let ?(sx) be sx_u5?.
       b) Let i64 be $ext(32, 64, sx, i32).
       c) Return i64.
-  b. If ((lanet_u1 is F32) and (vcvto_u3 is CONVERT)), then:
-    1) Let i32 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  b. If ((lanet_u1 is F32) and (vcvto_u4 is CONVERT)), then:
+    1) Let i32 be lane__u3.
+    2) If sx_u5? is defined, then:
+      a) Let ?(sx) be sx_u5?.
       b) Let f32 be $convert(32, 32, sx, i32).
       c) Return f32.
-  c. If ((lanet_u1 is F64) and (vcvto_u3 is CONVERT)), then:
-    1) Let i32 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  c. If ((lanet_u1 is F64) and (vcvto_u4 is CONVERT)), then:
+    1) Let i32 be lane__u3.
+    2) If sx_u5? is defined, then:
+      a) Let ?(sx) be sx_u5?.
       b) Let f64 be $convert(32, 64, sx, i32).
       c) Return f64.
-4. If ((lanet_u0 is F32) and ((lanet_u1 is I32) and (vcvto_u3 is TRUNC_SAT))), then:
-  a. Let f32 be lane__u2.
-  b. If sx_u4? is defined, then:
-    1) Let ?(sx) be sx_u4?.
+4. If ((lanet_u0 is F32) and ((lanet_u1 is I32) and (vcvto_u4 is TRUNC_SAT))), then:
+  a. Let f32 be lane__u3.
+  b. If sx_u5? is defined, then:
+    1) Let ?(sx) be sx_u5?.
     2) Let i32 be $trunc_sat(32, 32, sx, f32).
     3) Return i32.
 5. If (lanet_u0 is F64), then:
-  a. If ((lanet_u1 is I32) and (vcvto_u3 is TRUNC_SAT)), then:
-    1) Let f64 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  a. If ((lanet_u1 is I32) and (vcvto_u4 is TRUNC_SAT)), then:
+    1) Let f64 be lane__u3.
+    2) If sx_u5? is defined, then:
+      a) Let ?(sx) be sx_u5?.
       b) Let i32 be $trunc_sat(64, 32, sx, f64).
       c) Return i32.
-  b. If ((lanet_u1 is F32) and (vcvto_u3 is DEMOTE)), then:
-    1) Let f64 be lane__u2.
+  b. If ((lanet_u1 is F32) and (vcvto_u4 is DEMOTE)), then:
+    1) Let f64 be lane__u3.
     2) Let f32 be $demote(64, 32, f64).
     3) Return f32.
 6. Assert: Due to validation, (lanet_u0 is F32).
 7. Assert: Due to validation, (lanet_u1 is F64).
-8. Assert: Due to validation, (vcvto_u3 is PROMOTE).
-9. Let f32 be lane__u2.
+8. Assert: Due to validation, (vcvto_u4 is PROMOTE).
+9. Let f32 be lane__u3.
 10. Let f64 be $promote(32, 64, f32).
 11. Return f64.
 
@@ -3197,7 +3197,7 @@ execution_of_VNARROW (imm_2 X N_2) (imm_1 X N_1) sx
 9. Let c be $invlanes_((imm_2 X N_2), cj_1* ++ cj_2*).
 10. Push the value (V128.CONST c) to the stack.
 
-execution_of_VCVTOP (lanet_u2 X N_2) vcvtop half_u0? (lanet_u3 X N_1) sx_u1? zero_u4?
+execution_of_VCVTOP (lanet_u2 X N_2) (lanet_u3 X N_1) vcvtop half_u0? sx_u1? zero_u4?
 1. Assert: Due to validation, a value is on the top of the stack.
 2. Pop the value (V128.CONST c_1) from the stack.
 3. If (half_u0? is not defined and zero_u4? is not defined), then:
@@ -3725,8 +3725,8 @@ watsup 0.4 generator
 6-typing.watsup:803.6-803.40: prem_to_instrs: Yet `Reftype_sub: `%|-%<:%`(C, C.ELEMS_context[y!`%`_idx.0], rt)`
 6-typing.watsup:832.6-832.40: prem_to_instrs: Yet `Storagetype_sub: `%|-%<:%`(C, zt_2, zt_1)`
 6-typing.watsup:837.6-837.44: prem_to_instrs: Yet `Storagetype_sub: `%|-%<:%`(C, (C.ELEMS_context[y!`%`_idx.0] : reftype <: storagetype), zt)`
-6-typing.watsup:974.6-974.36: prem_to_instrs: Yet `Reftype_sub: `%|-%<:%`(C, rt_2, rt_1)`
-6-typing.watsup:980.6-980.36: prem_to_instrs: Yet `Reftype_sub: `%|-%<:%`(C, rt_2, rt_1)`
+6-typing.watsup:976.6-976.36: prem_to_instrs: Yet `Reftype_sub: `%|-%<:%`(C, rt_2, rt_1)`
+6-typing.watsup:982.6-982.36: prem_to_instrs: Yet `Reftype_sub: `%|-%<:%`(C, rt_2, rt_1)`
 =================
  Generated prose
 =================
@@ -4089,7 +4089,8 @@ validation_of_VEXTBINOP sh_1 sh_2 vextbinop sx
 validation_of_VNARROW sh_1 sh_2 sx
 - The instruction is valid with type ([V128, V128] ->_ [] ++ [V128]).
 
-validation_of_VCVTOP sh_1 vcvtop hf? sh_2 sx? zero?
+validation_of_VCVTOP sh_1 sh_2 vcvtop hf? sx? zero?
+- ((((($lanetype(sh_1) is imm_1) and ($lanetype(sh_2) is imm_2)) and ($lsize(imm_1) > $lsize(imm_2))) or (($lanetype(sh_1) is fnn_1) and ($lanetype(sh_2) is fnn_2)))) if and only if ((sx? is ?())).
 - The instruction is valid with type ([V128] ->_ [] ++ [V128]).
 
 validation_of_LOCAL.GET x
@@ -4694,85 +4695,85 @@ invsigned N i
 1. Let j be $inverse_of_signed(N, i).
 2. Return j.
 
-unop numty_u1 unop__u0 num__u2
+unop numty_u1 unop__u0 num__u3
 1. If (unop__u0 is CLZ), then:
-  a. Let iN be num__u2.
+  a. Let iN be num__u3.
   b. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$iclz($size(inn), iN)].
 2. If (unop__u0 is CTZ), then:
-  a. Let iN be num__u2.
+  a. Let iN be num__u3.
   b. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ictz($size(inn), iN)].
 3. If (unop__u0 is POPCNT), then:
-  a. Let iN be num__u2.
+  a. Let iN be num__u3.
   b. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ipopcnt($size(inn), iN)].
 4. If unop__u0 is of the case EXTEND, then:
   a. Let (EXTEND N) be unop__u0.
-  b. Let iN be num__u2.
+  b. Let iN be num__u3.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ext(N, $size(inn), S, $wrap($size(inn), N, iN))].
 5. If (unop__u0 is ABS), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fabs($size(fnn), fN)].
 6. If (unop__u0 is NEG), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fneg($size(fnn), fN)].
 7. If (unop__u0 is SQRT), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fsqrt($size(fnn), fN)].
 8. If (unop__u0 is CEIL), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fceil($size(fnn), fN)].
 9. If (unop__u0 is FLOOR), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$ffloor($size(fnn), fN)].
 10. If (unop__u0 is TRUNC), then:
-  a. Let fN be num__u2.
+  a. Let fN be num__u3.
   b. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$ftrunc($size(fnn), fN)].
 11. Assert: Due to validation, (unop__u0 is NEAREST).
-12. Let fN be num__u2.
+12. Let fN be num__u3.
 13. Assert: Due to validation, the type of numty_u1 is fnn.
 14. Let fnn be numty_u1.
 15. Return [$fnearest($size(fnn), fN)].
 
-binop numty_u1 binop_u0 num__u2 num__u3
+binop numty_u1 binop_u0 num__u3 num__u5
 1. If (binop_u0 is ADD), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$iadd($size(inn), iN_1, iN_2)].
 2. If (binop_u0 is SUB), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$isub($size(inn), iN_1, iN_2)].
 3. If (binop_u0 is MUL), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$imul($size(inn), iN_1, iN_2)].
-4. Let iN_1 be num__u2.
-5. Let iN_2 be num__u3.
+4. Let iN_1 be num__u3.
+5. Let iN_2 be num__u5.
 6. If the type of numty_u1 is inn, then:
   a. Let inn be numty_u1.
   b. If binop_u0 is of the case DIV, then:
@@ -4782,87 +4783,87 @@ binop numty_u1 binop_u0 num__u2 num__u3
     1) Let (REM sx) be binop_u0.
     2) Return [$irem($size(inn), sx, iN_1, iN_2)].
 7. If (binop_u0 is AND), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$iand($size(inn), iN_1, iN_2)].
 8. If (binop_u0 is OR), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ior($size(inn), iN_1, iN_2)].
 9. If (binop_u0 is XOR), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ixor($size(inn), iN_1, iN_2)].
 10. If (binop_u0 is SHL), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$ishl($size(inn), iN_1, iN_2)].
-11. Let iN_1 be num__u2.
-12. Let iN_2 be num__u3.
+11. Let iN_1 be num__u3.
+12. Let iN_2 be num__u5.
 13. If the type of numty_u1 is inn, then:
   a. Let inn be numty_u1.
   b. If binop_u0 is of the case SHR, then:
     1) Let (SHR sx) be binop_u0.
     2) Return [$ishr($size(inn), sx, iN_1, iN_2)].
 14. If (binop_u0 is ROTL), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$irotl($size(inn), iN_1, iN_2)].
 15. If (binop_u0 is ROTR), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return [$irotr($size(inn), iN_1, iN_2)].
 16. If (binop_u0 is ADD), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fadd($size(fnn), fN_1, fN_2)].
 17. If (binop_u0 is SUB), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fsub($size(fnn), fN_1, fN_2)].
 18. If (binop_u0 is MUL), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fmul($size(fnn), fN_1, fN_2)].
 19. If (binop_u0 is DIV), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fdiv($size(fnn), fN_1, fN_2)].
 20. If (binop_u0 is MIN), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fmin($size(fnn), fN_1, fN_2)].
 21. If (binop_u0 is MAX), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return [$fmax($size(fnn), fN_1, fN_2)].
 22. Assert: Due to validation, (binop_u0 is COPYSIGN).
-23. Let fN_1 be num__u2.
-24. Let fN_2 be num__u3.
+23. Let fN_1 be num__u3.
+24. Let fN_2 be num__u5.
 25. Assert: Due to validation, the type of numty_u1 is fnn.
 26. Let fnn be numty_u1.
 27. Return [$fcopysign($size(fnn), fN_1, fN_2)].
@@ -4870,21 +4871,21 @@ binop numty_u1 binop_u0 num__u2 num__u3
 testop inn EQZ iN
 1. Return $ieqz($size(inn), iN).
 
-relop numty_u1 relop_u0 num__u2 num__u3
+relop numty_u1 relop_u0 num__u3 num__u5
 1. If (relop_u0 is EQ), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return $ieq($size(inn), iN_1, iN_2).
 2. If (relop_u0 is NE), then:
-  a. Let iN_1 be num__u2.
-  b. Let iN_2 be num__u3.
+  a. Let iN_1 be num__u3.
+  b. Let iN_2 be num__u5.
   c. If the type of numty_u1 is inn, then:
     1) Let inn be numty_u1.
     2) Return $ine($size(inn), iN_1, iN_2).
-3. Let iN_1 be num__u2.
-4. Let iN_2 be num__u3.
+3. Let iN_1 be num__u3.
+4. Let iN_2 be num__u5.
 5. If the type of numty_u1 is inn, then:
   a. Let inn be numty_u1.
   b. If relop_u0 is of the case LT, then:
@@ -4900,53 +4901,53 @@ relop numty_u1 relop_u0 num__u2 num__u3
     1) Let (GE sx) be relop_u0.
     2) Return $ige($size(inn), sx, iN_1, iN_2).
 6. If (relop_u0 is EQ), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $feq($size(fnn), fN_1, fN_2).
 7. If (relop_u0 is NE), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $fne($size(fnn), fN_1, fN_2).
 8. If (relop_u0 is LT), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $flt($size(fnn), fN_1, fN_2).
 9. If (relop_u0 is GT), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $fgt($size(fnn), fN_1, fN_2).
 10. If (relop_u0 is LE), then:
-  a. Let fN_1 be num__u2.
-  b. Let fN_2 be num__u3.
+  a. Let fN_1 be num__u3.
+  b. Let fN_2 be num__u5.
   c. If the type of numty_u1 is fnn, then:
     1) Let fnn be numty_u1.
     2) Return $fle($size(fnn), fN_1, fN_2).
 11. Assert: Due to validation, (relop_u0 is GE).
-12. Let fN_1 be num__u2.
-13. Let fN_2 be num__u3.
+12. Let fN_1 be num__u3.
+13. Let fN_2 be num__u5.
 14. Assert: Due to validation, the type of numty_u1 is fnn.
 15. Let fnn be numty_u1.
 16. Return $fge($size(fnn), fN_1, fN_2).
 
-cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
-1. If ((numty_u0 is I32) and ((numty_u1 is I64) and (cvtop_u4 is CONVERT))), then:
-  a. Let iN be num__u3.
+cvtop numty_u0 numty_u1 cvtop_u5 sx_u2? num__u4
+1. If ((numty_u0 is I32) and ((numty_u1 is I64) and (cvtop_u5 is CONVERT))), then:
+  a. Let iN be num__u4.
   b. If sx_u2? is defined, then:
     1) Let ?(sx) be sx_u2?.
     2) Return [$ext(32, 64, sx, iN)].
-2. If ((numty_u0 is I64) and ((numty_u1 is I32) and (cvtop_u4 is CONVERT))), then:
-  a. Let iN be num__u3.
+2. If ((numty_u0 is I64) and ((numty_u1 is I32) and (cvtop_u5 is CONVERT))), then:
+  a. Let iN be num__u4.
   b. Return [$wrap(64, 32, iN)].
-3. If (cvtop_u4 is CONVERT), then:
-  a. Let fN be num__u3.
+3. If (cvtop_u5 is CONVERT), then:
+  a. Let fN be num__u4.
   b. If the type of numty_u0 is fnn, then:
     1) Let fnn be numty_u0.
     2) If the type of numty_u1 is inn, then:
@@ -4954,8 +4955,8 @@ cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
       b) If sx_u2? is defined, then:
         1. Let ?(sx) be sx_u2?.
         2. Return [$trunc($size(fnn), $size(inn), sx, fN)].
-4. If (cvtop_u4 is CONVERT_SAT), then:
-  a. Let fN be num__u3.
+4. If (cvtop_u5 is CONVERT_SAT), then:
+  a. Let fN be num__u4.
   b. If the type of numty_u0 is fnn, then:
     1) Let fnn be numty_u0.
     2) If the type of numty_u1 is inn, then:
@@ -4963,29 +4964,29 @@ cvtop numty_u0 numty_u1 cvtop_u4 sx_u2? num__u3
       b) If sx_u2? is defined, then:
         1. Let ?(sx) be sx_u2?.
         2. Return [$trunc_sat($size(fnn), $size(inn), sx, fN)].
-5. If ((numty_u0 is F32) and ((numty_u1 is F64) and (cvtop_u4 is CONVERT))), then:
-  a. Let fN be num__u3.
+5. If ((numty_u0 is F32) and ((numty_u1 is F64) and (cvtop_u5 is CONVERT))), then:
+  a. Let fN be num__u4.
   b. Return [$promote(32, 64, fN)].
-6. If ((numty_u0 is F64) and ((numty_u1 is F32) and (cvtop_u4 is CONVERT))), then:
-  a. Let fN be num__u3.
+6. If ((numty_u0 is F64) and ((numty_u1 is F32) and (cvtop_u5 is CONVERT))), then:
+  a. Let fN be num__u4.
   b. Return [$demote(64, 32, fN)].
-7. If ((cvtop_u4 is CONVERT) and the type of numty_u1 is fnn), then:
+7. If ((cvtop_u5 is CONVERT) and the type of numty_u1 is fnn), then:
   a. Let fnn be numty_u1.
-  b. Let iN be num__u3.
+  b. Let iN be num__u4.
   c. If the type of numty_u0 is inn, then:
     1) Let inn be numty_u0.
     2) If sx_u2? is defined, then:
       a) Let ?(sx) be sx_u2?.
       b) Return [$convert($size(inn), $size(fnn), sx, iN)].
-8. Assert: Due to validation, (cvtop_u4 is REINTERPRET).
+8. Assert: Due to validation, (cvtop_u5 is REINTERPRET).
 9. If the type of numty_u1 is fnn, then:
   a. Let fnn be numty_u1.
-  b. Let iN be num__u3.
+  b. Let iN be num__u4.
   c. If the type of numty_u0 is inn, then:
     1) Let inn be numty_u0.
     2) If ($size(inn) is $size(fnn)), then:
       a) Return [$reinterpret(inn, fnn, iN)].
-10. Let fN be num__u3.
+10. Let fN be num__u4.
 11. Assert: Due to validation, the type of numty_u0 is fnn.
 12. Let fnn be numty_u0.
 13. Assert: Due to validation, the type of numty_u1 is inn.
@@ -5310,59 +5311,59 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
 16. Let v128 be $invlanes_((inn X N), lane_3*).
 17. Return v128.
 
-vcvtop (lanet_u0 X N_1) (lanet_u1 X N_2) vcvto_u3 sx_u4? lane__u2
-1. If ((lanet_u0 is I8) and ((lanet_u1 is I16) and (vcvto_u3 is EXTEND))), then:
-  a. Let i8 be lane__u2.
-  b. If sx_u4? is defined, then:
-    1) Let ?(sx) be sx_u4?.
+vcvtop (lanet_u0 X N_1) (lanet_u1 X N_2) vcvto_u6 sx_u7? lane__u3
+1. If ((lanet_u0 is I8) and ((lanet_u1 is I16) and (vcvto_u6 is EXTEND))), then:
+  a. Let i8 be lane__u3.
+  b. If sx_u7? is defined, then:
+    1) Let ?(sx) be sx_u7?.
     2) Let i16 be $ext(8, 16, sx, i8).
     3) Return i16.
-2. If ((lanet_u0 is I16) and ((lanet_u1 is I32) and (vcvto_u3 is EXTEND))), then:
-  a. Let i16 be lane__u2.
-  b. If sx_u4? is defined, then:
-    1) Let ?(sx) be sx_u4?.
+2. If ((lanet_u0 is I16) and ((lanet_u1 is I32) and (vcvto_u6 is EXTEND))), then:
+  a. Let i16 be lane__u3.
+  b. If sx_u7? is defined, then:
+    1) Let ?(sx) be sx_u7?.
     2) Let i32 be $ext(16, 32, sx, i16).
     3) Return i32.
 3. If (lanet_u0 is I32), then:
-  a. If ((lanet_u1 is I64) and (vcvto_u3 is EXTEND)), then:
-    1) Let i32 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  a. If ((lanet_u1 is I64) and (vcvto_u6 is EXTEND)), then:
+    1) Let i32 be lane__u3.
+    2) If sx_u7? is defined, then:
+      a) Let ?(sx) be sx_u7?.
       b) Let i64 be $ext(32, 64, sx, i32).
       c) Return i64.
-  b. If ((lanet_u1 is F32) and (vcvto_u3 is CONVERT)), then:
-    1) Let i32 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  b. If ((lanet_u1 is F32) and (vcvto_u6 is CONVERT)), then:
+    1) Let i32 be lane__u3.
+    2) If sx_u7? is defined, then:
+      a) Let ?(sx) be sx_u7?.
       b) Let f32 be $convert(32, 32, sx, i32).
       c) Return f32.
-  c. If ((lanet_u1 is F64) and (vcvto_u3 is CONVERT)), then:
-    1) Let i32 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  c. If ((lanet_u1 is F64) and (vcvto_u6 is CONVERT)), then:
+    1) Let i32 be lane__u3.
+    2) If sx_u7? is defined, then:
+      a) Let ?(sx) be sx_u7?.
       b) Let f64 be $convert(32, 64, sx, i32).
       c) Return f64.
-4. If ((lanet_u0 is F32) and ((lanet_u1 is I32) and (vcvto_u3 is TRUNC_SAT))), then:
-  a. Let f32 be lane__u2.
-  b. If sx_u4? is defined, then:
-    1) Let ?(sx) be sx_u4?.
+4. If ((lanet_u0 is F32) and ((lanet_u1 is I32) and (vcvto_u6 is TRUNC_SAT))), then:
+  a. Let f32 be lane__u3.
+  b. If sx_u7? is defined, then:
+    1) Let ?(sx) be sx_u7?.
     2) Let i32 be $trunc_sat(32, 32, sx, f32).
     3) Return i32.
 5. If (lanet_u0 is F64), then:
-  a. If ((lanet_u1 is I32) and (vcvto_u3 is TRUNC_SAT)), then:
-    1) Let f64 be lane__u2.
-    2) If sx_u4? is defined, then:
-      a) Let ?(sx) be sx_u4?.
+  a. If ((lanet_u1 is I32) and (vcvto_u6 is TRUNC_SAT)), then:
+    1) Let f64 be lane__u3.
+    2) If sx_u7? is defined, then:
+      a) Let ?(sx) be sx_u7?.
       b) Let i32 be $trunc_sat(64, 32, sx, f64).
       c) Return i32.
-  b. If ((lanet_u1 is F32) and (vcvto_u3 is DEMOTE)), then:
-    1) Let f64 be lane__u2.
+  b. If ((lanet_u1 is F32) and (vcvto_u6 is DEMOTE)), then:
+    1) Let f64 be lane__u3.
     2) Let f32 be $demote(64, 32, f64).
     3) Return f32.
 6. Assert: Due to validation, (lanet_u0 is F32).
 7. Assert: Due to validation, (lanet_u1 is F64).
-8. Assert: Due to validation, (vcvto_u3 is PROMOTE).
-9. Let f32 be lane__u2.
+8. Assert: Due to validation, (vcvto_u6 is PROMOTE).
+9. Let f32 be lane__u3.
 10. Let f64 be $promote(32, 64, f32).
 11. Return f64.
 
@@ -6287,23 +6288,23 @@ execution_of_VNARROW (imm_2 X N_2) (imm_1 X N_1) sx
 9. Let c be $invlanes_((imm_2 X N_2), cj_1* ++ cj_2*).
 10. Push the value (V128.CONST c) to the stack.
 
-execution_of_VCVTOP (lanet_u1 X N_2) vcvtop half_u0? (lanet_u2 X N_1) sx? zero_u3?
+execution_of_VCVTOP (lanet_u1 X N_2) (lanet_u2 X N_1) vcvtop half__u0? sx? zero__u7?
 1. Assert: Due to validation, a value is on the top of the stack.
 2. Pop the value (V128.CONST c_1) from the stack.
-3. If (half_u0? is not defined and zero_u3? is not defined), then:
+3. If (half__u0? is not defined and zero__u7? is not defined), then:
   a. Let lnn_1 be lanet_u2.
   b. Let lnn_2 be lanet_u1.
   c. Let c'* be $lanes_((lnn_1 X N_1), c_1).
   d. Let c be $invlanes_((lnn_2 X N_2), $vcvtop((lnn_1 X N_1), (lnn_2 X N_2), vcvtop, sx?, c')*).
   e. Push the value (V128.CONST c) to the stack.
-4. If (zero_u3? is not defined and half_u0? is defined), then:
-  a. Let ?(hf) be half_u0?.
+4. If (zero__u7? is not defined and half__u0? is defined), then:
+  a. Let ?(half) be half__u0?.
   b. Let lnn_1 be lanet_u2.
   c. Let lnn_2 be lanet_u1.
-  d. Let ci* be $lanes_((lnn_1 X N_1), c_1)[$halfop(hf, 0, N_2) : N_2].
+  d. Let ci* be $lanes_((lnn_1 X N_1), c_1)[$halfop(half, 0, N_2) : N_2].
   e. Let c be $invlanes_((lnn_2 X N_2), $vcvtop((lnn_1 X N_1), (lnn_2 X N_2), vcvtop, sx?, ci)*).
   f. Push the value (V128.CONST c) to the stack.
-5. If (half_u0? is not defined and ((zero_u3? is ?(ZERO)) and the type of lanet_u2 is numtype)), then:
+5. If (half__u0? is not defined and ((zero__u7? is ?(ZERO)) and the type of lanet_u2 is numtype)), then:
   a. Let nt_1 be lanet_u2.
   b. If the type of lanet_u1 is numtype, then:
     1) Let nt_2 be lanet_u1.