diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup
index 33d10c9b34..fba3b79526 100644
--- a/spectec/spec/wasm-3.0/8-reduction.watsup
+++ b/spectec/spec/wasm-3.0/8-reduction.watsup
@@ -39,10 +39,13 @@ rule Eval_expr:
 
 ;; Context
 
+rule Step/ctxt-vals:
+  z; val+ instr*  ~>  z'; val+ instr'*
+  -- Step: z; instr* ~> z'; instr'*
+
 rule Step/ctxt-instrs:
-  z; val* instr* instr_1*  ~>  z'; val* instr'* instr_1*
+  z; instr* instr_1+  ~>  z'; instr'* instr_1+
   -- Step: z; instr* ~> z'; instr'*
-  -- if val* =/= eps \/ instr_1* =/= eps
 
 rule Step/ctxt-label:
   z; (LABEL_ n `{instr_0*} instr*)  ~>  z'; (LABEL_ n `{instr_0*} instr'*)
@@ -244,9 +247,11 @@ rule Step/throw:
 rule Step_read/throw_ref-null:
   z; (REF.NULL ht) THROW_REF  ~>  TRAP
 
+rule Step_read/throw_ref-vals:
+  z; val+ (REF.EXN_ADDR a) THROW_REF  ~>  (REF.EXN_ADDR a) THROW_REF
+
 rule Step_read/throw_ref-instrs:
-  z; val* (REF.EXN_ADDR a) THROW_REF instr*  ~>  (REF.EXN_ADDR a) THROW_REF
-  -- if val* =/= eps \/ instr* =/= eps
+  z; (REF.EXN_ADDR a) THROW_REF instr+  ~>  (REF.EXN_ADDR a) THROW_REF
 
 rule Step_read/throw_ref-label:
   z; (LABEL_ n `{instr'*} (REF.EXN_ADDR a) THROW_REF)  ~>  (REF.EXN_ADDR a) THROW_REF
@@ -288,9 +293,11 @@ rule Step_pure/handler-vals:
 
 ;; Traps
 
+rule Step_pure/trap-vals:
+  val+ TRAP  ~>  TRAP
+
 rule Step_pure/trap-instrs:
-  val* TRAP instr*  ~>  TRAP
-  -- if val* =/= eps \/ instr* =/= eps
+  TRAP instr+  ~>  TRAP
 
 rule Step_pure/trap-label:
   (LABEL_ n `{instr'*} TRAP)  ~>  TRAP