[spec] Update br_on_cast validation (#92)

As described in the overview, relax validation so that the input and
output types need only be in the same hierarchy rather than requiring
that the output type be a subtype of the input type.

In addition to updating the SpecTec source of truth, add notes about
what the extra supertypes in the formal rules are achieving. These notes
are modeled on the similar note that already exists for ref.cast_desc.

Author: tlively

document/core/valid/instructions.rst

@@ -235,6 +235,9 @@ $${rule-prose: Instr_ok/br_on_cast}
 
 $${rule: Instr_ok/br_on_cast}
 
+.. note::
+   The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy.
+
 
 .. _valid-br_on_cast_fail:
 
@@ -245,6 +248,9 @@ $${rule-prose: Instr_ok/br_on_cast_fail}
 
 $${rule: Instr_ok/br_on_cast_fail}
 
+.. note::
+   The existence of a common supertype ${:rt_3} means that ${:rt_1} and ${:rt_2} must be in the same heap subtyping hierarchy.
+
 
 .. _valid-call:
 

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

@@ -98,15 +98,21 @@ rule Instr_ok/br_on_cast:
   -- if C.LABELS[l] = t* rt
   -- Reftype_ok: C |- rt_1 : OK
   -- Reftype_ok: C |- rt_2 : OK
-  -- Reftype_sub: C |- rt_2 <: rt_1
+  -- Reftype_ok: C |- rt_3 : OK
+  ----
+  -- Reftype_sub: C |- rt_1 <: rt_3
+  -- Reftype_sub: C |- rt_2 <: rt_3
   -- Reftype_sub: C |- rt_2 <: rt
 
 rule Instr_ok/br_on_cast_fail:
   C |- BR_ON_CAST_FAIL l rt_1 rt_2 : t* rt_1 -> t* rt_2
   -- if C.LABELS[l] = t* rt
   -- Reftype_ok: C |- rt_1 : OK
   -- Reftype_ok: C |- rt_2 : OK
-  -- Reftype_sub: C |- rt_2 <: rt_1
+  -- Reftype_ok: C |- rt_3 : OK
+  ----
+  -- Reftype_sub: C |- rt_1 <: rt_3
+  -- Reftype_sub: C |- rt_2 <: rt_3
   -- Reftype_sub: C |- $diffrt(rt_1, rt_2) <: rt