Merge pull request #147 from WebAssembly/fix-dynamic-cast

Move resource type tag to handle

Author: lukewagner

design/mvp/CanonicalABI.md

@@ -258,40 +258,38 @@ defined by its parent component).
 The `HandleTable` class is defined in terms of a collection of supporting
 runtime bookkeeping classes that we'll go through first.
 
-The `Resource` class represents a runtime instance of a resource type:
+The `Resource` class represents a runtime instance of a resource type, storing
+the core representation value (which is currently fixed to `i32`):
 ```python
+@dataclass
 class Resource:
-  t: ResourceType
   rep: int
-
-  def __init__(self, t, rep):
-    self.t = t
-    self.rep = rep
 ```
-The `t` field points to the [`resourcetype`](Explainer.md#type-definitions)
-used to create this `Resource` and is used to perform dynamic type checking
-below. The `rep` field stores the representation value of this `Resource` whose
-type is currently fixed to `i32` as described in the Explainer.
 
 The `OwnHandle` and `BorrowHandle` classes represent runtime handle values of
 `own` and `borrow` type, resp:
 ```python
 class Handle:
   resource: Resource
+  rt: ResourceType
   lend_count: int
 
-  def __init__(self, resource):
+  def __init__(self, resource, rt):
     self.resource = resource
+    self.rt = rt
     self.lend_count = 0
 
 class OwnHandle(Handle): pass
 class BorrowHandle(Handle): pass
 ```
 The `resource` field points to the resource instance this handle refers to. The
-`lend_count` field maintains a count of the outstanding handles that were lent
-from this handle (by calls to `borrow`-taking functions). This count is used
-below to dynamically enforce the invariant that a handle cannot be dropped
-while it has currently lent out a `borrow`.
+`rt` field points to a runtime value representing the static
+[`resourcetype`](Explainer.md#type-definitions) of this handle and is used by
+dynamic type checking below. Lastly, the `lend_count` field maintains a count
+of the outstanding handles that were lent from this handle (by calls to
+`borrow`-taking functions). This count is used below to dynamically enforce the
+invariant that a handle cannot be dropped while it has currently lent out a
+`borrow`.
 
 The `Call` class represents a single runtime call (activation) of a
 component-level function. A `Call` is finished in two steps by `finish_lift`
@@ -368,13 +366,16 @@ use-after-free:
   def get(self, i, rt):
     trap_if(i >= len(self.array))
     trap_if(self.array[i] is None)
-    trap_if(self.array[i].resource.t is not rt)
+    trap_if(self.array[i].rt is not rt)
     return self.array[i]
 ```
 Additionally, the `get` method takes the runtime resource type tag and checks
-a tag match before returning the handle with this new-valid resource type. Note
-that this is a non-structural, pointer-equality-based check to implement the
-[type-checking rules](Explainer.md) of resource types.
+a tag match before returning the handle with this new-valid resource type. This
+check is a non-structural, pointer-equality-based test used to enforce the
+[type-checking rules](Explainer.md) of resource types at runtime. Importantly,
+this check keeps type imports abstract, considering each type import to have a
+unique `rt` value distinct from every other type import even if the two imports
+happen to be instantiated with the same resource type at runtime.
 
 The `lend` method is called when borrowing a handle. `lend` uses `Call.lenders`
 to decrement the handle's `lend_count` at the end of the call.
@@ -978,16 +979,18 @@ Finally, `own` and `borrow` handles are lowered by inserting them into the
 current component instance's `HandleTable`:
 ```python
 def lower_own(cx, resource, rt):
-  assert(resource.t is rt)
-  h = OwnHandle(resource)
+  h = OwnHandle(resource, rt)
   return cx.inst.handles.insert(cx, h)
 
 def lower_borrow(cx, resource, rt):
-  assert(resource.t is rt)
-  h = BorrowHandle(resource)
+  h = BorrowHandle(resource, rt)
   return cx.inst.handles.insert(cx, h)
 ```
-The assertions are ensured by validation.
+Note that the `rt` value that is stored in the runtime `Handle` captures what
+is statically known about the handle right before losing this information in
+the homogeneous `HandleTable`. Moreoever, as described above, distinct type
+imports are given distinct `rt` values so that handles produced by lowering
+different type imports are never interchangeable.
 
 ### Flattening
 
@@ -1564,7 +1567,7 @@ Calling `$f` invokes the following function, which creates a resource object
 and inserts it into the current instance's handle table:
 ```python
 def canon_resource_new(cx, rt, rep):
-  h = OwnHandle(Resource(rt, rep))
+  h = OwnHandle(Resource(rep), rt)
   return cx.inst.handles.insert(cx, h)
 ```
 

design/mvp/Explainer.md

@@ -995,6 +995,14 @@ replaced by `$R` when validating the instantiations of `$c1` and `$c2`. These
 type-checking rules for instantiating type imports mirror the *elimination*
 rule of [universal types]  (∀T).
 
+Importantly, this type substitution performed by the parent is not visible to
+the child at validation- or run-time. In particular, the type checks performed
+by the [Canonical ABI](CanonicalABI.md#context) use distinct type tags for
+distinct type imports and associate type tags with *handles*, not the underlying
+*resource*, leveraging the shared-nothing nature of components to type-tag handles
+at component boundaries and avoid the usual [type-exposure problems with
+dynamic casts][non-parametric parametricity].
+
 In summary: all type constructors are *structural* with the exception of
 `resource`, which is *abstract* and *generative*. Type imports and exports that
 have a subtype bound also introduce abstract types and follow the standard
@@ -1816,8 +1824,10 @@ and will be added over the coming months to complete the MVP proposal:
 [Subtyping]: https://en.wikipedia.org/wiki/Subtyping
 [Universal Types]: https://en.wikipedia.org/wiki/System_F
 [Existential Types]: https://en.wikipedia.org/wiki/System_F
+
 [Generative]: https://www.researchgate.net/publication/2426300_A_Syntactic_Theory_of_Type_Generativity_and_Sharing
 [Avoidance Problem]: https://counterexamples.org/avoidance.html
+[Non-Parametric Parametricity]: https://people.mpi-sws.org/~dreyer/papers/npp/main.pdf
 
 [URL Standard]: https://url.spec.whatwg.org
 [URI]: https://en.wikipedia.org/wiki/Uniform_Resource_Identifier

design/mvp/canonical-abi/definitions.py

@@ -315,22 +315,20 @@ def __init__(self):
 
 #
 
+@dataclass
 class Resource:
-  t: ResourceType
   rep: int
 
-  def __init__(self, t, rep):
-    self.t = t
-    self.rep = rep
-
 #
 
 class Handle:
   resource: Resource
+  rt: ResourceType
   lend_count: int
 
-  def __init__(self, resource):
+  def __init__(self, resource, rt):
     self.resource = resource
+    self.rt = rt
     self.lend_count = 0
 
 class OwnHandle(Handle): pass
@@ -381,7 +379,7 @@ def insert(self, cx, h):
   def get(self, i, rt):
     trap_if(i >= len(self.array))
     trap_if(self.array[i] is None)
-    trap_if(self.array[i].resource.t is not rt)
+    trap_if(self.array[i].rt is not rt)
     return self.array[i]
 
 #
@@ -845,13 +843,11 @@ def pack_flags_into_int(v, labels):
 #
 
 def lower_own(cx, resource, rt):
-  assert(resource.t is rt)
-  h = OwnHandle(resource)
+  h = OwnHandle(resource, rt)
   return cx.inst.handles.insert(cx, h)
 
 def lower_borrow(cx, resource, rt):
-  assert(resource.t is rt)
-  h = BorrowHandle(resource)
+  h = BorrowHandle(resource, rt)
   return cx.inst.handles.insert(cx, h)
 
 ### Flattening
@@ -1215,7 +1211,7 @@ def canon_lower(cx, callee, ft, flat_args):
 ### `resource.new`
 
 def canon_resource_new(cx, rt, rep):
-  h = OwnHandle(Resource(rt, rep))
+  h = OwnHandle(Resource(rep), rt)
   return cx.inst.handles.insert(cx, h)
 
 ### `resource.drop`

design/mvp/canonical-abi/run_tests.py

@@ -381,15 +381,15 @@ def dtor(x):
     nonlocal dtor_value
     dtor_value = x
   rt = ResourceType(dtor)
-  r1 = Resource(rt, 42)
-  r2 = Resource(rt, 43)
-  r3 = Resource(rt, 44)
+  r1 = Resource(42)
+  r2 = Resource(43)
+  r3 = Resource(44)
 
   def host_import(act, args):
     assert(len(args) == 2)
     assert(args[0] is r1)
     assert(args[1] is r3)
-    return ([Resource(rt, 45)], lambda:())
+    return ([Resource(45)], lambda:())
 
   cx = mk_cx()
   def core_wasm(args):