Improve descriptions and fix examples in Explainer.md, addressing feedback in #276

Author: lukewagner

design/mvp/Binary.md

@@ -48,7 +48,10 @@ Notes:
   WebAssembly 1.0 spec.)
 * The `layer` field is meant to distinguish modules from components early in
   the binary format. (Core WebAssembly modules already implicitly have a
-  `layer` field of `0x0` in their 4 byte [`core:version`] field.)
+  `layer` field of `0x0` if the existing 4-byte [`core:version`] field is
+  reinterpreted as two 2-byte fields. This implies that the Core WebAssembly
+  spec needs to make a backwards-compatible spec change to split `core:version`
+  and fix `layer` to forever be `0x0`.)
 
 
 ## Instance Definitions

design/mvp/CanonicalABI.md

@@ -7,7 +7,7 @@ of modules in Core WebAssembly.
 * [Supporting definitions](#supporting-definitions)
   * [Despecialization](#despecialization)
   * [Alignment](#alignment)
-  * [Size](#size)
+  * [Element Size](#element-size)
   * [Runtime State](#runtime-state)
   * [Loading](#loading)
   * [Storing](#storing)
@@ -156,13 +156,17 @@ Handle types are passed as `i32` indices into the `HandleTable` introduced
 below.
 
 
-### Size
+### Element Size
 
-Each value type is also assigned a `size`, measured in bytes, which corresponds
-the `sizeof` operator in C. Empty types, such as records with no fields, are
-not permitted, to avoid complications in source languages.
+Each value type is also assigned an `elem_size` which is the number of bytes
+used when values of the type are stored as elements of a `list`. Having this
+byte size be a static property of the type instead of attempting to use a
+variable-length element-encoding scheme both simplifies the implementation and
+maps well to languages which represent `list`s as random-access arrays. Empty
+types, such as records with no fields, are not permitted, to avoid
+complications in source languages.
 ```python
-def size(t):
+def elem_size(t):
   match despecialize(t):
     case Bool()             : return 1
     case S8() | U8()        : return 1
@@ -173,33 +177,33 @@ def size(t):
     case F64()              : return 8
     case Char()             : return 4
     case String() | List(_) : return 8
-    case Record(fields)     : return size_record(fields)
-    case Variant(cases)     : return size_variant(cases)
-    case Flags(labels)      : return size_flags(labels)
+    case Record(fields)     : return elem_size_record(fields)
+    case Variant(cases)     : return elem_size_variant(cases)
+    case Flags(labels)      : return elem_size_flags(labels)
     case Own(_) | Borrow(_) : return 4
 
-def size_record(fields):
+def elem_size_record(fields):
   s = 0
   for f in fields:
     s = align_to(s, alignment(f.t))
-    s += size(f.t)
+    s += elem_size(f.t)
   assert(s > 0)
   return align_to(s, alignment_record(fields))
 
 def align_to(ptr, alignment):
   return math.ceil(ptr / alignment) * alignment
 
-def size_variant(cases):
-  s = size(discriminant_type(cases))
+def elem_size_variant(cases):
+  s = elem_size(discriminant_type(cases))
   s = align_to(s, max_case_alignment(cases))
   cs = 0
   for c in cases:
     if c.t is not None:
-      cs = max(cs, size(c.t))
+      cs = max(cs, elem_size(c.t))
   s += cs
   return align_to(s, alignment_variant(cases))
 
-def size_flags(labels):
+def elem_size_flags(labels):
   n = len(labels)
   assert(n > 0)
   if n <= 8: return 1
@@ -430,7 +434,7 @@ the top-level case analysis:
 ```python
 def load(cx, ptr, t):
   assert(ptr == align_to(ptr, alignment(t)))
-  assert(ptr + size(t) <= len(cx.opts.memory))
+  assert(ptr + elem_size(t) <= len(cx.opts.memory))
   match despecialize(t):
     case Bool()         : return convert_int_to_bool(load_int(cx, ptr, 1))
     case U8()           : return load_int(cx, ptr, 1)
@@ -511,6 +515,7 @@ testing that its unsigned integral value is in the valid [Unicode Code Point]
 range and not a [Surrogate]:
 ```python
 def convert_i32_to_char(cx, i):
+  assert(i >= 0)
   trap_if(i >= 0x110000)
   trap_if(0xD800 <= i <= 0xDFFF)
   return chr(i)
@@ -571,18 +576,18 @@ def load_list(cx, ptr, elem_type):
 
 def load_list_from_range(cx, ptr, length, elem_type):
   trap_if(ptr != align_to(ptr, alignment(elem_type)))
-  trap_if(ptr + length * size(elem_type) > len(cx.opts.memory))
+  trap_if(ptr + length * elem_size(elem_type) > len(cx.opts.memory))
   a = []
   for i in range(length):
-    a.append(load(cx, ptr + i * size(elem_type), elem_type))
+    a.append(load(cx, ptr + i * elem_size(elem_type), elem_type))
   return a
 
 def load_record(cx, ptr, fields):
   record = {}
   for field in fields:
     ptr = align_to(ptr, alignment(field.t))
     record[field.label] = load(cx, ptr, field.t)
-    ptr += size(field.t)
+    ptr += elem_size(field.t)
   return record
 ```
 As a technical detail: the `align_to` in the loop in `load_record` is
@@ -599,7 +604,7 @@ implementation can build the appropriate index tables at compile-time so that
 variant-passing is always O(1) and not involving string operations.
 ```python
 def load_variant(cx, ptr, cases):
-  disc_size = size(discriminant_type(cases))
+  disc_size = elem_size(discriminant_type(cases))
   case_index = load_int(cx, ptr, disc_size)
   ptr += disc_size
   trap_if(case_index >= len(cases))
@@ -630,7 +635,7 @@ derived from the ordered labels of the `flags` type. The code here takes
 advantage of Python's support for integers of arbitrary width.
 ```python
 def load_flags(cx, ptr, labels):
-  i = load_int(cx, ptr, size_flags(labels))
+  i = load_int(cx, ptr, elem_size_flags(labels))
   return unpack_flags_from_int(i, labels)
 
 def unpack_flags_from_int(i, labels):
@@ -670,8 +675,13 @@ def lift_borrow(cx, i, t):
     cx.track_owning_lend(h)
   return h.rep
 ```
-The `track_owning_lend` call to `CallContext` participates in the enforcement of
-the dynamic borrow rules.
+The `track_owning_lend` call to `CallContext` participates in the enforcement
+of the dynamic borrow rules, which keep the source `own` handle alive until the
+end of the call (as an intentionally-conservative upper bound on how long the
+`borrow` handle can be held). This tracking is only required when `h` is an
+`own` handle because, when `h` is a `borrow` handle, this tracking has already
+happened (when the originating `own` handle was lifted) for a strictly longer
+call scope than the current call.
 
 
 ### Storing
@@ -682,7 +692,7 @@ The `store` function defines how to write a value `v` of a given value type
 ```python
 def store(cx, v, t, ptr):
   assert(ptr == align_to(ptr, alignment(t)))
-  assert(ptr + size(t) <= len(cx.opts.memory))
+  assert(ptr + elem_size(t) <= len(cx.opts.memory))
   match despecialize(t):
     case Bool()         : store_int(cx, int(bool(v)), ptr, 1)
     case U8()           : store_int(cx, v, ptr, 1)
@@ -990,20 +1000,20 @@ def store_list(cx, v, ptr, elem_type):
   store_int(cx, length, ptr + 4, 4)
 
 def store_list_into_range(cx, v, elem_type):
-  byte_length = len(v) * size(elem_type)
+  byte_length = len(v) * elem_size(elem_type)
   trap_if(byte_length >= (1 << 32))
   ptr = cx.opts.realloc(0, 0, alignment(elem_type), byte_length)
   trap_if(ptr != align_to(ptr, alignment(elem_type)))
   trap_if(ptr + byte_length > len(cx.opts.memory))
   for i,e in enumerate(v):
-    store(cx, e, elem_type, ptr + i * size(elem_type))
+    store(cx, e, elem_type, ptr + i * elem_size(elem_type))
   return (ptr, len(v))
 
 def store_record(cx, v, ptr, fields):
   for f in fields:
     ptr = align_to(ptr, alignment(f.t))
     store(cx, v[f.label], f.t, ptr)
-    ptr += size(f.t)
+    ptr += elem_size(f.t)
 ```
 
 Variants are stored using the `|`-separated list of `refines` cases built
@@ -1015,7 +1025,7 @@ case indices to the consumer's case indices.
 ```python
 def store_variant(cx, v, ptr, cases):
   case_index, case_value = match_case(v, cases)
-  disc_size = size(discriminant_type(cases))
+  disc_size = elem_size(discriminant_type(cases))
   store_int(cx, case_index, ptr, disc_size)
   ptr += disc_size
   ptr = align_to(ptr, max_case_alignment(cases))
@@ -1042,7 +1052,7 @@ to variants.
 ```python
 def store_flags(cx, v, ptr, labels):
   i = pack_flags_into_int(v, labels)
-  store_int(cx, i, ptr, size_flags(labels))
+  store_int(cx, i, ptr, elem_size_flags(labels))
 
 def pack_flags_into_int(v, labels):
   i = 0
@@ -1292,7 +1302,7 @@ def lift_flat_variant(cx, vi, cases):
         case ('i64', 'i32') : return wrap_i64_to_i32(x)
         case ('i64', 'f32') : return decode_i32_as_float(wrap_i64_to_i32(x))
         case ('i64', 'f64') : return decode_i64_as_float(x)
-        case _              : return x
+        case _              : assert(have == want); return x
   c = cases[case_index]
   if c.t is None:
     v = None
@@ -1403,7 +1413,7 @@ def lower_flat_variant(cx, v, cases):
       case ('i32', 'i64') : payload[i] = Value('i64', have.v)
       case ('f32', 'i64') : payload[i] = Value('i64', encode_float_as_i32(have.v))
       case ('f64', 'i64') : payload[i] = Value('i64', encode_float_as_i64(have.v))
-      case _              : pass
+      case _              : assert(have.t == want)
   for want in flat_types:
     payload.append(Value(want, 0))
   return [Value('i32', case_index)] + payload
@@ -1433,7 +1443,7 @@ def lift_values(cx, max_flat, vi, ts):
     ptr = vi.next('i32')
     tuple_type = Tuple(ts)
     trap_if(ptr != align_to(ptr, alignment(tuple_type)))
-    trap_if(ptr + size(tuple_type) > len(cx.opts.memory))
+    trap_if(ptr + elem_size(tuple_type) > len(cx.opts.memory))
     return list(load(cx, ptr, tuple_type).values())
   else:
     return [ lift_flat(cx, vi, t) for t in ts ]
@@ -1451,11 +1461,11 @@ def lower_values(cx, max_flat, vs, ts, out_param = None):
     tuple_type = Tuple(ts)
     tuple_value = {str(i): v for i,v in enumerate(vs)}
     if out_param is None:
-      ptr = cx.opts.realloc(0, 0, alignment(tuple_type), size(tuple_type))
+      ptr = cx.opts.realloc(0, 0, alignment(tuple_type), elem_size(tuple_type))
     else:
       ptr = out_param.next('i32')
     trap_if(ptr != align_to(ptr, alignment(tuple_type)))
-    trap_if(ptr + size(tuple_type) > len(cx.opts.memory))
+    trap_if(ptr + elem_size(tuple_type) > len(cx.opts.memory))
     store(cx, tuple_value, tuple_type, ptr)
     return [ Value('i32', ptr) ]
   else:

design/mvp/Explainer.md

@@ -433,10 +433,10 @@ type and function definitions which are introduced in the next two sections.
 The syntax for defining core types extends the existing core type definition
 syntax, adding a `module` type constructor:
 ```ebnf
-core:type        ::= (type <id>? <core:deftype>)              (GC proposal)
-core:deftype     ::= <core:functype>                          (WebAssembly 1.0)
-                   | <core:structtype>                        (GC proposal)
-                   | <core:arraytype>                         (GC proposal)
+core:rectype     ::= ... from the Core WebAssembly spec
+core:typedef     ::= ... from the Core WebAssembly spec
+core:subtype     ::= ... from the Core WebAssembly spec
+core:comptype    ::= ... from the Core WebAssembly spec
                    | <core:moduletype>
 core:moduletype  ::= (module <core:moduledecl>*)
 core:moduledecl  ::= <core:importdecl>
@@ -452,8 +452,8 @@ core:exportdesc  ::= strip-id(<core:importdesc>)
 where strip-id(X) parses '(' sort Y ')' when X parses '(' sort <id>? Y ')'
 ```
 
-Here, `core:deftype` (short for "defined type") is inherited from the [gc]
-proposal and extended with a `module` type constructor. If [module-linking] is
+Here, `core:comptype` (short for "composite type") as defined in the [gc]
+proposal is extended with a `module` type constructor. If [module-linking] is
 added to Core WebAssembly, an `instance` type constructor would be added as
 well but, for now, it's left out since it's unnecessary. Also, in the MVP,
 validation will reject `core:moduletype` defining or aliasing other
@@ -571,6 +571,8 @@ typebound     ::= (eq <typeidx>)
 
 where bind-id(X) parses '(' sort <id>? Y ')' when X parses '(' sort Y ')'
 ```
+Because there is nothing in this type grammar analogous to the [gc] proposal's
+[`rectype`], none of these types are recursive.
 
 #### Fundamental value types
 
@@ -788,8 +790,8 @@ definitions:
     (export "h" (func (result $U)))
     (import "T" (type $T (sub resource)))
     (import "i" (func (param "x" (list (own $T)))))
-    (export $T' "T2" (type (eq $T)))
-    (export $U' "U" (type (sub resource)))
+    (export "T2" (type $T' (eq $T)))
+    (export "U" (type $U' (sub resource)))
     (export "j" (func (param "x" (borrow $T')) (result (own $U'))))
   ))
 )
@@ -960,7 +962,7 @@ as well. For example, in this component:
 (component
   (import "C" (component $C
     (export "T1" (type (sub resource)))
-    (export $T2 "T2" (type (sub resource)))
+    (export "T2" (type $T2 (sub resource)))
     (export "T3" (type (eq $T2)))
   ))
   (instance $c (instantiate $C))
@@ -1028,7 +1030,7 @@ following component:
 is assigned the following `componenttype`:
 ```wasm
 (component
-  (export $r1 "r1" (type (sub resource)))
+  (export "r1" (type $r1 (sub resource)))
   (export "r2" (type (eq $r1)))
 )
 ```
@@ -1039,7 +1041,7 @@ If a component wants to hide this fact and force clients to assume `r1` and
 `r2` are distinct types (thereby allowing the implementation to actually use
 separate types in the future without breaking clients), an explicit type can be
 ascribed to the export that replaces the `eq` bound with a less-precise `sub`
-bound.
+bound (using syntax introduced [below](#import-and-export-definitions)).
 ```wasm
 (component
   (type $r (resource (rep i32)))
@@ -1991,6 +1993,7 @@ and will be added over the coming months to complete the MVP proposal:
 [stack-switching]: https://github.com/WebAssembly/stack-switching/blob/main/proposals/stack-switching/Overview.md
 [esm-integration]: https://github.com/WebAssembly/esm-integration/tree/main/proposals/esm-integration
 [gc]: https://github.com/WebAssembly/gc/blob/main/proposals/gc/MVP.md
+[`rectype`]: https://webassembly.github.io/gc/core/text/types.html#text-rectype
 [shared-everything-threads]: https://github.com/WebAssembly/shared-everything-threads
 [WASI Preview 2]: https://github.com/WebAssembly/WASI/tree/main/preview2