Sync Explainer.md with Binary.md, add a Subtyping.md

This commit has a few high-level changes:

* The `Binary.md` is sync'd a bit with `Explainer.md` in terms of
  content and links.
* The textual syntax for `alias` directives was tweaked in
  `Explainer.md` to match `Binary.md`
* Actual section numbers were chosen in the binary format. The exception
  handling proposal uses 13 for an event section so the four new
  sections here are getting 14-17.
* Handling of subtyping between instances and modules is now codified in
  `Subtyping.md`. This goes into more detail about how imports are
  elaborated, how instantiation is expected to work, and how to test for
  subtypes.

This is hoped to describe the intended status quo given the discussion
on #7.

Author: alexcrichton

proposals/module-linking/Binary.md

@@ -62,7 +62,8 @@ referencing:
 
 * each `importdesc` is valid according to import section
 * Types can only reference preceding type definitions. This forces everything to
-  be a DAG and forbids cyclic types.
+  be a DAG and forbids cyclic types. TODO: with type imports we may need cyclic
+  types, so this validation will likely change in some form.
 
 ## Import Section updates
 
@@ -89,12 +90,12 @@ importdesc ::=
 * the `module x` production ensures the type `x` is indeed a module type
 * the `instance x` production ensures the type `x` is indeed an instance type
 
-## Module section (100)
+## Module section (14)
 
 A new module section is added
 
 ```
-modulesec ::=  t*:section_100(vec(typeidx))           ->        t*
+modulesec ::=  t*:section_14(vec(typeidx))           ->        t*
 ```
 
 **Validation**
@@ -103,12 +104,12 @@ modulesec ::=  t*:section_100(vec(typeidx))           ->        t*
 * This defines the locally defined set of modules, adding to the module index
   space.
 
-## Instance section (101)
+## Instance section (15)
 
 A new section defining local instances
 
 ```
-instancesec ::=  i*:section_101(vec(instancedef))     ->    i*
+instancesec ::=  i*:section_15(vec(instancedef))     ->    i*
 
 instancedef ::= 0x00 m:moduleidx e*:vec(exportdesc)   ->    {instantiate m, imports e*}
 ```
@@ -125,21 +126,25 @@ the future we'll likely want this binary value to match that.
 * The type index `m` must point to a module type.
 * Indices of items referred to by `exportdesc` are all in-bounds. Can only refer
   to imports/previous aliases, since only those sections can precede.
-* The precise rules of how `e*` is validated against the module type's declare
-  list of imports is being hashed out in
-  [#7](https://github.com/WebAssembly/module-linking/issues/7). For now
-  conservative order-dependent rules are used where the length of `e*` must be
-  the same as the number of imports the module type has. Additionally the type
-  of each element of `e*` must be a subtype of the type that it's being matched
-  with. Matching happens pairwise with the list of imports on the module type
-  for `m`.
+* The `e*` list is validated against the module type's declared list
+  of [imports pairwise and in-order](Explainer.md#module-imports-and-nested-instances).
+  The type of each item must be a supertype of the expected type listed in the
+  module's type.
 
-## Alias section (102)
+**Execution notes**
+
+* The actual module being instantiated does not need to list imports in the
+  exact same order as its type declaration. The `e*` has names based on the
+  local module type's declaration.
+* Be sure to read up on [subtyping](./Subtyping.md) to ensure that instances
+  with a single name can be used to match imports with a two-level namespace.
+
+## Alias section (16)
 
 A new module section is added
 
 ```
-aliassec ::=  a*:section_102(vec(alias))     ->        a*
+aliassec ::=  a*:section_16(vec(alias))     ->        a*
 
 alias ::=
     0x00 i:instanceidx 0x00 e:exportidx      ->       (alias (instance $i) (func $e))
@@ -154,9 +159,10 @@ alias ::=
 
 **Validation**
 
-* Aliased instance indexes are all in bounds
+* Aliased instance indexes are all in bounds. Remember "in bounds" here means it
+  can't refer to instances defined after the `alias` item.
 * Aliased instance export indices are in bounds relative to the instance's
-  *locally-declared* (via module or instance type) list of exports
+  *locally-declared* (via module or instance type) list of exports.
 * Export indices match the actual type of the export
 * Aliases append to the respective index space.
 * Parent aliases can only happen in submodules (not the top-level module) and
@@ -169,6 +175,12 @@ alias ::=
   items were declared after the module's type in the corresponding module
   section.
 
+**Execution notes**
+
+* Note for child aliases that while the export is referred to by index it's
+  actually loaded from the specified instance by name. The name loaded
+  corresponds to the `i`th export's name in the locally defined type.
+
 ## Function section
 
 **Validation**
@@ -191,10 +203,10 @@ exportdesc ::=
 
 * Module/instance indexes must be in-bounds.
 
-## Module Code Section (103)
+## Module Code Section (17)
 
 ```
-modulecodesec ::= m*:section_103(vec(modulecode))       ->    m*
+modulecodesec ::= m*:section_17(vec(modulecode))       ->    m*
 
 modulecode ::= size:u32 mod:module                      ->    mod, size = ||mod||
 ```
@@ -208,31 +220,9 @@ the top-level
 * Module definitions must match their module type exactly, no subtyping (or
   maybe subtyping, see WebAssembly/module-linking#9).
 * Modules themselves validate recursively.
-* Must have the same number of modules as the count of all local module
-  sections.
-* Each submodule is validated with a subset of the parent's context, for example
-  the set of types and instances the current module has defined are available
-  for aliasing in the submodule.
-
-## Subtyping
-
-Subtyping will extend what's currently ["import
-matching"](https://webassembly.github.io/spec/core/exec/modules.html#import-matching)
-
-**Instances**
-
-Instance `{exports e1}` is a subtype of `{exports e2}` if and only if:
-
-* Each name in `e1` is present in `e2`
-* For each corresponding name `n` in the sets
-  * `e1[n]` is a subtype of `e2[n]`
-
-**Instances**
-
-Module `{imports i1, exports e1}` is a subtype of `{imports i2, exports e2}` if and only if:
-
-* Each name in `e1` is present in `e2`
-* For each corresponding name `n` in the sets
-  * `e1[n]` is a subtype of `e2[n]`
-* ... And some condition on imports. For now this is a bit up for debate on
-  WebAssembly/module-linking#7
+* The module code section must have the same number of modules as the count of
+  all local module sections.
+* Each submodule is validated with the parent's context at the time of
+  declaration. For example the set of types and modules the current module
+  has defined are available for aliasing in the submodule, but only those
+  defined before the corresponding module's type declaration.

proposals/module-linking/Explainer.md

@@ -284,7 +284,7 @@ example, an instance type can be defined:
 
 In many examples shown below, type definitions are needed for *both* a module
 type and the instance type produced when that module type is instantiated. In
-such cases, to avoid duplicating all the exports, a new "zero-level export" 
+such cases, to avoid duplicating all the exports, a new "zero-level export"
 `(export $InstanceType)` form is added which injects all the exports of
 `$InstanceType` into the containing module type. For example, here is the type
 of a module which implements the above-defined `$WasiFile` interface via Win32
@@ -363,9 +363,9 @@ version of the same module can be written:
     (export "f1" (func $f1))
     (export "f2" (func $f2 (param i32)))
   ))
-  (alias $i.f1 (func $i $f1))
+  (alias $i.$f1 (instance $i) (func $f1))
   (func (export "run")
-    call $i.f1
+    call $i.$f1
   )
 )
 ```
@@ -377,17 +377,17 @@ how multiple uses of inline function types [desugar][typeuse-abbrev] to the same
 function type definition.
 
 Aliases are not restricted to functions: all exportable definitions can be
-aliased. One situation where an explicit `alias` definition will be required is
-for a default memory or table: because there is no explicit `$i.$j` path used by
-instructions to refer to defaults, they must be explicitly aliased:
+aliased. One situation where an explicit `alias` definition may be required is
+for a default memory or table since if there is no explicit `$i.$j` path used
+by instructions to refer to defaults, they must be explicitly aliased:
 ```wasm
 (module
   (import "libc" (instance $libc
     (export "memory" (memory $mem 1))
     (export "table" (table $tbl 0 funcref))
   ))
-  (alias (memory $libc $mem)) ;; memory index 0 = default memory
-  (alias (table $libc $tbl)) ;; table index 0 = default table
+  (alias (instance $libc) (memory $mem)) ;; memory index 0 = default memory
+  (alias (instance $libc) (table $tbl)) ;; table index 0 = default table
   (func
     ...
     i32.load  ;; accesses $libc.$mem
@@ -544,11 +544,17 @@ the child's type index space:
     (export "read" (func (param i32 i32 i32) (result i32)))
   ))
   (module $child
-    (alias $WasiFile (parent (type $WasiFile)))
+    (alias $WasiFile parent (type $WasiFile))
     (import "wasi_file" (instance (type $WasiFile)))
   )
 )
 ```
+Note that `parent` aliases can only refer to previously-defined items relative
+to the module's own declaration in the module index space. This means that it
+can refer to previously defined imports, modules, instances, or aliases, but it
+cannot refer to imports (for example) that occur after the module's
+declaration. A module is declared with its type and defined later in the binary
+format.
 
 In general, language-independent tools can easily merge multiple `.wasm` files
 in a dependency graph into one `.wasm` file by performing simple transformations
@@ -673,6 +679,9 @@ could be encoded with the binary section sequence:
 10. ModuleCode Section, defining `$M`
 11. Code Section, defining `$x`
 
+This repository also contains an [initial proposal for the binary format
+updates](./Binary.md).
+
 
 ### Summary
 
@@ -764,7 +773,7 @@ More generally, when ESM-integration loads a module with a
 
 With this extension, a single JS app will be able to load multiple wasm
 programs using ESM `import` statements and have these programs safely and
-transparently share library code as described in 
+transparently share library code as described in
 [shared-everything dynamic linking example](Example-SharedEverythingDynamicLinking.md).