Add explicit RTT support for casts

proposals/gc/MVP.md

@@ -27,6 +27,10 @@ Based on [reference types proposal](https://github.com/WebAssembly/reference-typ
 * `i31ref` is a new reference type
   - `reftype ::= ... | i31ref`
 
+* `rtt <reftype>` is a new reference type that is a runtime representation of type `<reftype>` (see [overview](Overview.md#casting-and-runtime-types))
+  - `reftype ::= ... | rtt <reftype>`
+  - `rtt t ok` iff `t ok`
+
 
 #### Type Definitions
 
@@ -53,9 +57,12 @@ Based on [reference types proposal](https://github.com/WebAssembly/reference-typ
 #### Imports
 
 * `type <typetype>` is an import description with an upper bound
-  - `importdesc ::= ... | type <reftype>`
+  - `importdesc ::= ... | type <typetype>`
   - Note: `type` may get additional parameters in the future
 
+* `typetype` describes the type of a type import, and is either an upper bound or a type equivalence
+  - `typetype ::= sub <reftype> | eq <reftype>`
+
 * Type imports have indices prepended to the type index space, similar to other imports.
   - Note: due to bounds, type imports can be mutually recursive with other type imports as well as regular type definitions. Hence they have to be validated together with the type section.
 
@@ -75,7 +82,7 @@ In addition to the rules for basic reference types:
 
 * `eqref` is a subtype of `anyref`
   - `eqref <: anyref`
-  - Note: `i31ref` and `anyfunc` are *not* a subtypes of `eqref`, i.e., those types do not expose reference equality
+  - Note: `i31ref` and `funcref` are *not* a subtypes of `eqref`, i.e., those types do not expose reference equality
 
 * `nullref` is a subtype of `eqref`
   - `nullref <: eqref`
@@ -92,8 +99,8 @@ In addition to the rules for basic reference types:
   - `ref $t <: optref $t`
   - Note: concrete reference types are *not* supertypes of `nullref`, i.e., not nullable
 
-* Any function reference type is a subtype of `anyfunc`
-  - `ref $t <: anyfunc`
+* Any function reference type is a subtype of `funcref`
+  - `ref $t <: funcref`
      - iff `$t = <functype>`
 
 * Any optional reference type (and thereby respective concrete reference type) is a subtype of `eqref` if its not a function
@@ -122,6 +129,10 @@ In addition to the rules for basic reference types:
   - `var <valtype> <: var <valtype>`
   - Note: mutable fields are *not* subtypes of immutable ones, so `const` really means constant, not read-only
 
+* `rtt t` is a subtype of `anyref`
+  - `rtt t <: anyref`
+  - Note: `rtt t1` is *not* a subtype of `rtt t2`, even if `t1` is a subtype of `t2`; such subtyping would be unsound, since RTTs are used in both co- and contravariant roles (e.g., both when constructing and consuming a reference)
+
 
 #### Defaultability
 
@@ -159,6 +170,12 @@ In addition to the rules for basic reference types:
 * `struct.new <typeidx>` allocates a structure of type `$t` and initialises its fields with given values
   - `struct.new $t : [t*] -> [(ref $t)]`
     - iff `$t = struct (mut t)*`
+  - equivalent to `struct.new_rtt $t anyref (rtt.anyref)`
+
+* `struct.new_rtt <typeidx> <reftype>` allocates a structure of type `$t` with RTT information and initialises its fields with given values
+  - `struct.new_rtt $t t' : [(rtt t') t*] -> [(ref $t)]`
+    - iff `$t = struct (mut t)*`
+    - and `ref $t <: t'`
 
 * `struct.new_default <typeidx>` allocates a structure of type `$t` and initialises its fields with default values
   - `struct.new_default $t : [] -> [(ref $t)]`
@@ -183,6 +200,12 @@ In addition to the rules for basic reference types:
 * `array.new <typeidx>` allocates an array of type `$t` and initialises its fields with a given value
   - `array.new $t : [t i32] -> [(ref $t)]`
     - iff `$t = array (mut t)`
+  - equivalent to `array.new_rtt $t anyref (rtt.anyref)`
+
+* `array.new_rtt <typeidx>` allocates a array of type `$t` with RTT information
+  - `array.new_rtt $t t' : [(rtt t') t i32] -> [(ref $t)]`
+    - iff `$t = array (mut t)`
+    - and `ref $t <: t'`
 
 * `array.new_default <typeidx>` allocates an array of type `$t` and initialises its fields with the default value
   - `array.new_default $t : [i32] -> [(ref $t)]`
@@ -222,18 +245,34 @@ TODO: Is 31 bit value range the right choice?
   - `i31ref.get_s : [i31ref] -> [i32]`
 
 
-#### Casts
+#### Runtime Types
+
+* `rtt.anyref` returns the RTT of type `anyref` as a subtype of only itself
+  - `rtt.anyref : [] -> [(rtt anyref)]`
 
-TODO. Want to introduce explicit runtime type values to support casts in a pay-as-you-go manner. Deferred to a separate PR. Casts themselves could then look something like this:
+* `rtt.funcref` returns the RTT of type `funcref` as a subtype of `anyref`
+  - `rtt.funcref : [] -> [(rtt funcref)]`
 
-* `cast <reftype> <reftype>` casts a value down to a given reference type
-  - `cast t t' : [t (rtti t')] -> [t']`
+* `rtt.eqref` returns the RTT of type `eqref` as a subtype of `anyref`
+  - `rtt.eqref : [] -> [(rtt eqref)]`
+
+* `rtt.new <reftype> <reftype>` returns the RTT of the specified type as a subtype of a given RTT operand
+  - `rtt.new t t' : [(rtt t')] -> [(rtt t)]`
+    - iff `t <: t'`
+  - multiple invocations of this instruction yield fresh RTTs
+
+* All RTT instructions are considered *constant expressions*.
+
+
+#### Casts
+
+* `cast <reftype> <reftype>` casts a reference value down to a type given by a RTT representation
+  - `cast t t' : [t (rtt t')] -> [t']`
      - iff `t' <: t <: anyref`
-  - traps if the operand is not of type `t'` at runtime
-  - equivalent to `block [t (rtti t')]->[t'] (br_on_cast 0 t t') unreachable end`
+  - traps if the operand's (runtime) type is not defined to be a (transitive) subtype of `t`
 
 * `br_on_cast <labelidx> <reftype> <reftype>` branches if a value can be cast down to a given reference type
-  - `br_on_cast $l t t' : [t (rtti t')] -> [t]`
+  - `br_on_cast $l t t' : [t (rtt t')] -> [t]`
     - iff `t' <: t <: anyref`
     - and `$l : [t']`
   - passes cast operand along with branch
@@ -301,14 +340,16 @@ In addition to the rules for basic reference types:
 
 #### `Type`
 
+* The `Type` constructor constructs an RTT value.
+
 TODO.
 
 
 ## Questions
 
-* Have explicit RTTI representations?
-
-* Distinguish reference types that are castable (and therefore have RTTI)?
+* Should RTT presence be made explicit in struct types and ref types?
+  - for example, `(struct rtt ...)` and `rttref <: anyref`
+  - only these types would be castable
 
 * Provide a way to make data types non-eq, especially immutable ones?