[spec] Fix instr sequence typing rules to actually be composable (WebAssembly#2197)

Author: rossberg

document/core/valid/instructions.rst

@@ -1358,22 +1358,28 @@ $${rule-prose: Instrs_ok}
 
 $${rule: Instrs_ok/empty}
 
+$${rule: Instrs_ok/instr}
+
 $${rule: Instrs_ok/seq}
 
-$${rule: {Instrs_ok/sub Instrs_ok/frame}}
+$${rule: Instrs_ok/sub}
 
 .. note::
-   In combination with the previous rule,
-   subsumption allows to compose instructions whose types would not directly fit otherwise.
+   This *subsumption rule* allows to weaken the type of an instruction sequence to a supertype,
+   which includes the ability to drop init variables ${:x*} from the instruction type in a context where they are not needed, for example, at the end of the body of a :ref:`block <valid-block>`.
+
+$${rule: Instrs_ok/frame}
+
+.. note::
+   In combination with the previous two rules,
+   this *frame rule* allows to compose instructions whose types would not directly fit otherwise.
    For example, consider the instruction sequence
 
    $${instr*: (CONST I32 1) (CONST I32 2) (BINOP I32 ADD)}
 
    To type this sequence, its subsequence ${instr*: (CONST I32 2) (BINOP I32 ADD)} needs to be valid with an intermediate type.
    But the direct type of ${instr: (CONST I32 2)} is ${instrtype: eps -> I32}, not matching the two inputs expected by ${instr: $($(BINOP I32 ADD))}.
-   The subsumption rule allows to weaken the type of ${instr: (CONST I32 2)} to the supertype ${instrtype: I32 -> I32 I32}, such that it can be composed with ${instr: $($(BINOP I32 ADD))} and yields the intermediate type ${instrtype: I32 -> I32 I32} for the subsequence. That can in turn be composed with the first constant.
-
-   Furthermore, subsumption allows to drop init variables ${:x*} from the instruction type in a context where they are not needed, for example, at the end of the body of a :ref:`block <valid-block>`.
+   The rule allows to weaken the type of ${instr: (CONST I32 2)} to the supertype ${instrtype: I32 -> I32 I32}, such that it can be composed with ${instr: $($(BINOP I32 ADD))} and yields the intermediate type ${instrtype: I32 -> I32 I32} for the subsequence. That can in turn be composed with the first constant.
 
 
 .. index:: expression, result type

specification/wasm-1.0/6-typing.spectec

@@ -134,9 +134,13 @@ rule Expr_ok:
 rule Instrs_ok/empty:
   C |- eps : eps -> eps
 
+rule Instrs_ok/instr:
+  C |- instr : t_1* -> t_2*
+  -- Instr_ok: C |- instr : t_1* -> t_2*
+
 rule Instrs_ok/seq:
-  C |- instr_1 instr_2* : t_1* -> t_3*
-  -- Instr_ok: C |- instr_1 : t_1* -> t_2*
+  C |- instr_1* instr_2* : t_1* -> t_3*
+  -- Instrs_ok: C |- instr_1* : t_1* -> t_2*
   -- Instrs_ok: C |- instr_2* : t_2* -> t_3*
 
 rule Instrs_ok/frame:

specification/wasm-2.0/6-typing.spectec

@@ -151,9 +151,13 @@ rule Expr_ok:
 rule Instrs_ok/empty:
   C |- eps : eps -> eps
 
+rule Instrs_ok/instr:
+  C |- instr : t_1* -> t_2*
+  -- Instr_ok: C |- instr : t_1* -> t_2*
+
 rule Instrs_ok/seq:
-  C |- instr_1 instr_2* : t_1* -> t_3*
-  -- Instr_ok: C |- instr_1 : t_1* -> t_2*
+  C |- instr_1* instr_2* : t_1* -> t_3*
+  -- Instrs_ok: C |- instr_1* : t_1* -> t_2*
   -- Instrs_ok: C |- instr_2* : t_2* -> t_3*
 
 rule Instrs_ok/sub:

specification/wasm-3.0/2.3-validation.instructions.spectec

@@ -613,10 +613,14 @@ rule Instr_ok/vcvtop:
 rule Instrs_ok/empty:
   C |- eps : eps -> eps
 
+rule Instrs_ok/instr:
+  C |- instr : t_1* ->_(x*) t_2*
+  -- Instr_ok: C |- instr : t_1* ->_(x*) t_2*
+
 ;; TODO(3, rossberg): enable x_1*#x_2* to avoid space
 rule Instrs_ok/seq:
-  C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
-  -- Instr_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
+  C |- instr_1* instr_2* : t_1* ->_(x_1* x_2*) t_3*
+  -- Instrs_ok: C |- instr_1* : t_1* ->_(x_1*) t_2*
   -- (if C.LOCALS[x_1] = init t)*
   -- Instrs_ok: $with_locals(C, x_1*, (SET t)*) |- instr_2* : t_2* ->_(x_2*) t_3*
 

specification/wasm-latest/2.3-validation.instructions.spectec

@@ -613,10 +613,14 @@ rule Instr_ok/vcvtop:
 rule Instrs_ok/empty:
   C |- eps : eps -> eps
 
+rule Instrs_ok/instr:
+  C |- instr : t_1* ->_(x*) t_2*
+  -- Instr_ok: C |- instr : t_1* ->_(x*) t_2*
+
 ;; TODO(3, rossberg): enable x_1*#x_2* to avoid space
 rule Instrs_ok/seq:
-  C |- instr_1 instr_2* : t_1* ->_(x_1* x_2*) t_3*
-  -- Instr_ok: C |- instr_1 : t_1* ->_(x_1*) t_2*
+  C |- instr_1* instr_2* : t_1* ->_(x_1* x_2*) t_3*
+  -- Instrs_ok: C |- instr_1* : t_1* ->_(x_1*) t_2*
   -- (if C.LOCALS[x_1] = init t)*
   -- Instrs_ok: $with_locals(C, x_1*, (SET t)*) |- instr_2* : t_2* ->_(x_2*) t_3*