Internalise sx into vcvtop

Wasm-DSL · Jul 26, 2024 · 30a3ab5 · 30a3ab5
1 parent 40190d1
commit 30a3ab5
Show file tree

Hide file tree

Showing 16 changed files with 340 additions and 363 deletions.
diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup
@@ -322,16 +322,7 @@ syntax vrelop_(Jnn X N) = EQ | NE
   | GE sx  -- if $lsizenn(Jnn) =/= `64 \/ sx = S
 syntax vrelop_(Fnn X N) = EQ | NE | LT | GT | LE | GE
 
-syntax vcvtop = EXTEND | TRUNC_SAT | CONVERT | DEMOTE | PROMOTE
-;; TODO: analogous to cvtop, this could just universally be CONVERT.
-;; Otherwise, it needs to be indexed by 2 shapes.
-;; TODO: the following syntactic constraints apply:
-;; iNxM <- iN'xM'  N < N'  -- (NARROW as binop)
-;; iNxM <- iN'xM'  N > N'  EXTEND half sx
-;; iNxM <- fN'xM'          TRUNC_SAT sx ZERO? (N = 32)
-;; fNxM <- iN'xM'          CONVERT LOW? sx    (N = 32)
-;; fNxM <- fN'xM'  N < N'  DEMOTE ZERO
-;; fNxM <- fN'xM'  N > N'  PROMOTE LOW
+syntax vcvtop = EXTEND sx | TRUNC_SAT sx | CONVERT sx | DEMOTE | PROMOTE
 
 syntax vshiftop_(ishape)
 syntax vshiftop_(Jnn X N) = SHL | SHR sx
@@ -434,7 +425,7 @@ syntax instr/vec hint(desc "vector instruction") = ...
     -- if $($lsize($lanetype(ishape_1)) = 2*$lsize($lanetype(ishape_2)))
   | VNARROW ishape_1 ishape_2 sx        hint(show %.NARROW#_#%#_#%)
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= 32)
-  | VCVTOP shape shape vcvtop half? sx? zero?
+  | VCVTOP shape shape vcvtop half? zero?
     hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%#_#%)
     ;; TODO: missing constraints
   | ...

diff --git a/spectec/spec/wasm-2.0/3-numerics.watsup b/spectec/spec/wasm-2.0/3-numerics.watsup
@@ -222,7 +222,7 @@ def $vbinop_(shape, vbinop_(shape), vec_(V128), vec_(V128)) : vec_(V128)*
     hint(show %2#$_(%1)#(%3, %4))
 def $vrelop_(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#$_(%1)#(%3, %4))
-def $vcvtop__(shape_1, shape_2, vcvtop, sx?, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))*
+def $vcvtop__(shape_1, shape_2, vcvtop, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))*
     hint(show %3#$__(%1,%2)^(%4)#((%5)))
 
 def $vunop_(Jnn X M, ABS, v128_1) = v128
@@ -395,15 +395,15 @@ def $vrelop_(Fnn X M, GE, v128_1, v128_2) = v128
     -- if $isize(Inn) = $size(Fnn)
     -- if v128 = $invlanes_(Inn X M, lane_3*)
 
-def $vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTEND, sx, iN_1) = iN_2
+def $vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTEND sx, iN_1) = iN_2
     -- if iN_2 = $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, iN_1)
-def $vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2, CONVERT, sx, iN_1) = fN_2
+def $vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2, CONVERT sx, iN_1) = fN_2
     -- if fN_2 = $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, iN_1)
-def $vcvtop__(Fnn_1 X M_1, Inn_2 X M_2, TRUNC_SAT, sx, fN_1) = $list_(lane_(Inn_2), iN_2?)
+def $vcvtop__(Fnn_1 X M_1, Inn_2 X M_2, TRUNC_SAT sx, fN_1) = $list_(lane_(Inn_2), iN_2?)
     -- if iN_2? = $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, fN_1)
-def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, DEMOTE, eps, fN_1) = fN_2*
+def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, DEMOTE, fN_1) = fN_2*
     -- if fN_2* = $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1)
-def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, PROMOTE, eps, fN_1) = fN_2*
+def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, PROMOTE, fN_1) = fN_2*
     -- if fN_2* = $promote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1)
 
 

diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup
@@ -353,7 +353,7 @@ rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128
 
 rule Instr_ok/vcvtop:
-  C |- VCVTOP sh_1 sh_2 vcvtop hf? sx? zero? : V128 -> V128
+  C |- VCVTOP sh_1 sh_2 vcvtop hf? 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
@@ -351,20 +351,20 @@ rule Step_pure/vnarrow:
 
 
 rule Step_pure/vcvtop-full:
-  (VCONST V128 c_1) (VCVTOP (Lnn_2 X N_2) (Lnn_1 X N_1) vcvtop eps sx) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (Lnn_2 X N_2) (Lnn_1 X N_1) vcvtop) ~> (VCONST V128 c)
   -- if c'* = $lanes_(Lnn_1 X N_1, c_1)
-  -- if c <- $mapinvlanes_(Lnn_2 X N_2, $vcvtop__(Lnn_1 X N_1, Lnn_2 X N_2, vcvtop, sx, c')*)
+  -- if c <- $mapinvlanes_(Lnn_2 X N_2, $vcvtop__(Lnn_1 X N_1, Lnn_2 X N_2, vcvtop, 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) (Lnn_1 X N_1) vcvtop hf sx?) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (Lnn_2 X N_2) (Lnn_1 X N_1) vcvtop hf) ~> (VCONST V128 c)
   -- if ci* = $lanes_(Lnn_1 X N_1, c_1)[$half(hf, 0, N_2) : N_2]
-  -- if c <- $mapinvlanes_(Lnn_2 X N_2, $vcvtop__(Lnn_1 X N_1, Lnn_2 X N_2, vcvtop, sx?, ci)*)
+  -- if c <- $mapinvlanes_(Lnn_2 X N_2, $vcvtop__(Lnn_1 X N_1, Lnn_2 X N_2, vcvtop, ci)*)
 
 rule Step_pure/vcvtop-zero:
-  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) (nt_1 X N_1) vcvtop eps sx? ZERO) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (nt_2 X N_2) (nt_1 X N_1) vcvtop ZERO) ~> (VCONST V128 c)
   -- if ci* = $lanes_(nt_1 X N_1, c_1)
-  -- if c <- $mapinvlanes_(nt_2 X N_2, $vcvtop__(nt_1 X N_1, nt_2 X N_2, vcvtop, sx?, ci)* $zero(nt_2)^N_1)
+  -- if c <- $mapinvlanes_(nt_2 X N_2, $vcvtop__(nt_1 X N_1, nt_2 X N_2, vcvtop, ci)* $zero(nt_2)^N_1)
 
 
 ;; Local instructions

diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup
@@ -625,10 +625,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) (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 135:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND S) LOW
+  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND S) HIGH
+  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND U) LOW
+  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND U) HIGH
   | 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)
@@ -657,10 +657,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) (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 167:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND S) LOW
+  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND S) HIGH
+  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND U) LOW
+  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND U) HIGH
   | 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)
@@ -683,10 +683,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) (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 199:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND S) LOW
+  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND S) HIGH
+  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND U) LOW
+  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND U) HIGH
   | 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)
@@ -736,14 +736,14 @@ grammar Binstr/vector-v-f64x2 : instr = ...
   | ...
 
 grammar Binstr/vector-cvt : instr = ...
-  | 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 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 S) LOW
+  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) (I32 X 4) (CONVERT U) LOW
   | 0xFD 94:Bu32 => VCVTOP (F32 X 4) (F64 X 2) DEMOTE ZERO
   | 0xFD 95:Bu32 => VCVTOP (F64 X 2) (F32 X 4) PROMOTE LOW
 

diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup
@@ -426,14 +426,17 @@ syntax vrelop_(Jnn X M) = EQ | NE
   | GE sx hint(show GE#_#%)  -- if $lsizenn(Jnn) =/= `64 \/ sx = S
 syntax vrelop_(Fnn X M) = EQ | NE | LT | GT | LE | GE
 
-;; TODO(1, rossberg): move sx into here
+;; TODO(1, rossberg): internalise half and zero
 syntax vcvtop__(shape_1, shape_2) hint(macro "%" "V%")
 syntax vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2) =
-  | EXTEND    -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
+  | EXTEND sx hint(show EXTEND#_#%)
+    -- if $lsizenn2(Jnn_2) = $(2 * $lsizenn1(Jnn_1))
 syntax vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2) =
-  | CONVERT   -- if $sizenn2(Fnn_2) >= $lsizenn1(Jnn_1) = `32
+  | CONVERT sx hint(show CONVERT#_#%)
+    -- if $sizenn2(Fnn_2) >= $lsizenn1(Jnn_1) = `32
 syntax vcvtop__(Fnn_1 X M_1, Jnn_2 X M_2) =
-  | TRUNC_SAT -- if $sizenn1(Fnn_1) >= $lsizenn2(Jnn_2) = `32
+  | TRUNC_SAT sx hint(show TRUNC_SAT#_#%)
+    -- if $sizenn1(Fnn_1) >= $lsizenn2(Jnn_2) = `32
 syntax vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2) =
   | DEMOTE    -- if $sizenn1(Fnn_1) > $sizenn2(Fnn_2)
   | PROMOTE   -- if $sizenn1(Fnn_1) < $sizenn2(Fnn_2)
@@ -553,12 +556,11 @@ syntax instr/vec hint(desc "vector instruction") = ...
     hint(show ##%1.##%3#_# ##%2)
   | VNARROW ishape_1 ishape_2 sx        hint(show ##%.NARROW#_# ##%#_#%) hint(macro "VNARROW")
     -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= `32)
-  | VCVTOP shape_1 shape_2 vcvtop__(shape_2, shape_1) half__(shape_2, shape_1)? sx? zero__(shape_2, shape_1)?
+  | VCVTOP shape_1 shape_2 vcvtop__(shape_2, shape_1) half__(shape_2, shape_1)? zero__(shape_2, shape_1)?
     hint(show ##%1.%3#_# ##%2)
     hint(show ##%1.%3#_# ##%2#_#%4)        ;; TODO(2, rossberg): this is wrong when half is absent
     hint(show ##%1.%3#_#%5#_# ##%2#_#%4)   ;; TODO(2, rossberg): this is wrong when half is present
     -- if $lanetype(shape_1) =/= $lanetype(shape_2)
-    -- if sx? =/= eps <=> $lanetype(shape_1) = Jnn_1 /\ $lanetype(shape_2) = Jnn_2 /\ $lsizenn1(Jnn_1) > $lsizenn2(Jnn_2)
   | VSPLAT shape                        hint(show ##%.SPLAT) hint(macro "VSPLAT")
   | VEXTRACT_LANE shape sx? laneidx     hint(show ##%.EXTRACT_LANE %) hint(show ##%.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE")
     -- if sx? = eps <=> $lanetype(shape) = numtype

diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup
@@ -360,7 +360,7 @@ def $free_instr(VEXTBINOP ishape_1 ishape_2 vextbinop) =
   $free_shape(ishape_1) ++ $free_shape(ishape_2)
 def $free_instr(VNARROW ishape_1 ishape_2 sx) =
   $free_shape(ishape_1) ++ $free_shape(ishape_2)
-def $free_instr(VCVTOP shape_1 shape_2 vcvtop half? sx? zero?) =
+def $free_instr(VCVTOP shape_1 shape_2 vcvtop half? zero?) =
   $free_shape(shape_1) ++ $free_shape(shape_2)
 def $free_instr(VSPLAT shape) = $free_shape(shape)
 def $free_instr(VEXTRACT_LANE shape sx? laneidx) = $free_shape(shape)

diff --git a/spectec/spec/wasm-3.0/3-numerics.watsup b/spectec/spec/wasm-3.0/3-numerics.watsup
@@ -239,7 +239,7 @@ def $vbinop_(shape, vbinop_(shape), vec_(V128), vec_(V128)) : vec_(V128)*
     hint(show %2#$_(%1,%3,%4))
 def $vrelop_(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
     hint(show %2#$_(%1,%3,%4))
-def $vcvtop__(shape_1, shape_2, vcvtop__(shape_1, shape_2), sx?, lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))*
+def $vcvtop__(shape_1, shape_2, vcvtop__(shape_1, shape_2), lane_($lanetype(shape_1))) : lane_($lanetype(shape_2))*
     hint(show %3#$__(%1,%2)^(%4)#((%5)))
 
 def $vunop_(Jnn X M, ABS, v128_1) = v128
@@ -412,15 +412,15 @@ def $vrelop_(Fnn X M, GE, v128_1, v128_2) = v128
     -- if $isize(Inn) = $size(Fnn)  ;; TODO(rossberg, 3): make implicit
     -- if v128 = $invlanes_(Inn X M, lane_3*)
 
-def $vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTEND, sx, iN_1) = iN_2
+def $vcvtop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTEND sx, iN_1) = iN_2
     -- if iN_2 = $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, iN_1)
-def $vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2, CONVERT, sx, iN_1) = fN_2
+def $vcvtop__(Jnn_1 X M_1, Fnn_2 X M_2, CONVERT sx, iN_1) = fN_2
     -- if fN_2 = $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, iN_1)
-def $vcvtop__(Fnn_1 X M_1, Inn_2 X M_2, TRUNC_SAT, sx, fN_1) = $list_(lane_(Inn_2), iN_2?)
+def $vcvtop__(Fnn_1 X M_1, Inn_2 X M_2, TRUNC_SAT sx, fN_1) = $list_(lane_(Inn_2), iN_2?)
     -- if iN_2? = $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, fN_1)
-def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, DEMOTE, eps, fN_1) = fN_2*
+def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, DEMOTE, fN_1) = fN_2*
     -- if fN_2* = $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1)
-def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, PROMOTE, eps, fN_1) = fN_2*
+def $vcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, PROMOTE, fN_1) = fN_2*
     -- if fN_2* = $promote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), fN_1)
 
 def $vextunop__(ishape_1, ishape_2, vextunop__(ishape_1, ishape_2), vec_(V128)) : vec_(V128)

diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -924,7 +924,7 @@ rule Instr_ok/vnarrow:
   C |- VNARROW sh_1 sh_2 sx : V128 V128 -> V128
 
 rule Instr_ok/vcvtop:
-  C |- VCVTOP sh_1 sh_2 vcvtop half? sx? zero? : V128 -> V128
+  C |- VCVTOP sh_1 sh_2 vcvtop half? zero? : V128 -> V128
 
 
 ;; Local instructions

diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup
@@ -716,19 +716,19 @@ rule Step_pure/vnarrow:
 
 
 rule Step_pure/vcvtop-full:
-  (VCONST V128 c_1) (VCVTOP (Lnn_2 X M) (Lnn_1 X M) vcvtop sx?) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (Lnn_2 X M) (Lnn_1 X M) vcvtop) ~> (VCONST V128 c)
   -- if c'* = $lanes_(Lnn_1 X M, c_1)
-  -- if c <- $mapinvlanes_(Lnn_2 X M, $vcvtop__(Lnn_1 X M, Lnn_2 X M, vcvtop, sx?, c')*)
+  -- if c <- $mapinvlanes_(Lnn_2 X M, $vcvtop__(Lnn_1 X M, Lnn_2 X M, vcvtop, c')*)
 
 rule Step_pure/vcvtop-half:
-  (VCONST V128 c_1) (VCVTOP (Lnn_2 X M_2) (Lnn_1 X M_1) vcvtop half sx?) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (Lnn_2 X M_2) (Lnn_1 X M_1) vcvtop half eps) ~> (VCONST V128 c)
   -- if ci* = $lanes_(Lnn_1 X M_1, c_1)[$half__(Lnn_1 X M_1, Lnn_2 X M_2, half, 0, M_2) : M_2]
-  -- if c <- $mapinvlanes_(Lnn_2 X M_2, $vcvtop__(Lnn_1 X M_1, Lnn_2 X M_2, vcvtop, sx?, ci)*)
+  -- if c <- $mapinvlanes_(Lnn_2 X M_2, $vcvtop__(Lnn_1 X M_1, Lnn_2 X M_2, vcvtop, ci)*)
 
 rule Step_pure/vcvtop-zero:
-  (VCONST V128 c_1) (VCVTOP (nt_2 X M_2) (nt_1 X M_1) vcvtop sx? zero) ~> (VCONST V128 c)
+  (VCONST V128 c_1) (VCVTOP (nt_2 X M_2) (nt_1 X M_1) vcvtop eps zero) ~> (VCONST V128 c)
   -- if ci* = $lanes_(nt_1 X M_1, c_1)
-  -- if c <- $mapinvlanes_(nt_2 X M_2, $vcvtop__(nt_1 X M_1, nt_2 X M_2, vcvtop, sx?, ci)* $zero(nt_2)^M_1)
+  -- if c <- $mapinvlanes_(nt_2 X M_2, $vcvtop__(nt_1 X M_1, nt_2 X M_2, vcvtop, ci)* $zero(nt_2)^M_1)
 
 
 ;; Local instructions

diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup
@@ -787,10 +787,10 @@ grammar Binstr/vec-narrow-i16x8 : instr = ...
   | ...
 
 grammar Binstr/vec-ext-i16x8 : instr = ...
-  | 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 135:Bu32 => VCVTOP (I16 X `8) (I8 X `16) (EXTEND S) LOW
+  | 0xFD 136:Bu32 => VCVTOP (I16 X `8) (I8 X `16) (EXTEND S) HIGH
+  | 0xFD 137:Bu32 => VCVTOP (I16 X `8) (I8 X `16) (EXTEND U) LOW
+  | 0xFD 138:Bu32 => VCVTOP (I16 X `8) (I8 X `16) (EXTEND U) HIGH
   | ...
 
 grammar Binstr/vec-shift-i16x8 : instr = ...
@@ -840,10 +840,10 @@ grammar Binstr/vec-bitmask-i32x4 : instr = ...
   | ...
 
 grammar Binstr/vec-ext-i32x4 : instr = ...
-  | 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 167:Bu32 => VCVTOP (I32 X `4) (I16 X `8) (EXTEND S) LOW
+  | 0xFD 168:Bu32 => VCVTOP (I32 X `4) (I16 X `8) (EXTEND S) HIGH
+  | 0xFD 169:Bu32 => VCVTOP (I32 X `4) (I16 X `8) (EXTEND U) LOW
+  | 0xFD 170:Bu32 => VCVTOP (I32 X `4) (I16 X `8) (EXTEND U) HIGH
   | ...
 
 grammar Binstr/vec-shift-i32x4 : instr = ...
@@ -884,10 +884,10 @@ grammar Binstr/vec-bitmask-i64x2 : instr = ...
   | ...
 
 grammar Binstr/vec-ext-i64x2 : instr = ...
-  | 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 199:Bu32 => VCVTOP (I64 X `2) (I32 X `4) (EXTEND S) LOW
+  | 0xFD 200:Bu32 => VCVTOP (I64 X `2) (I32 X `4) (EXTEND S) HIGH
+  | 0xFD 201:Bu32 => VCVTOP (I64 X `2) (I32 X `4) (EXTEND U) LOW
+  | 0xFD 202:Bu32 => VCVTOP (I64 X `2) (I32 X `4) (EXTEND U) HIGH
   | ...
 
 grammar Binstr/vec-shift-i64x2 : instr = ...
@@ -963,14 +963,14 @@ grammar Binstr/vec-bin-f64x2 : instr = ...
 grammar Binstr/vec-cvt : instr = ...
   | 0xFD 94:Bu32 => VCVTOP (F32 X `4) (F64 X `2) DEMOTE ZERO
   | 0xFD 95:Bu32 => VCVTOP (F64 X `2) (F32 X `4) PROMOTE LOW
-  | 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 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 S) LOW
+  | 0xFD 255:Bu32 => VCVTOP (F64 X `2) (I32 X `4) (CONVERT U) LOW
 
 
 ;; Expressions