diff --git a/AstSemantics.md b/AstSemantics.md
index c7df3aa1..80890f2c 100644
--- a/AstSemantics.md
+++ b/AstSemantics.md
@@ -1,14 +1,19 @@
 # Abstract Syntax Tree Semantics
 
-WebAssembly code is represented as an Abstract Syntax Tree (AST) where each node
-represents an expression. Each function body consists of a list of expressions.
-All expressions and operators are typed, with no implicit conversions, subtyping, or overloading rules.
+This document describes WebAssembly semantics. The description here is written
+in terms of an Abstract Syntax Tree (AST), however it is also possible to
+understand WebAssembly semantics in terms of a stack machine. (In practice,
+implementations need not build an actual AST or maintain an actual stack; they
+need only behave [as if](https://en.wikipedia.org/wiki/As-if_rule) they did so.)
 
 This document explains the high-level design of the AST: its types, constructs, and
 semantics. For full details consult [the formal Specification](https://github.com/WebAssembly/spec),
 for file-level encoding details consult [Binary Encoding](BinaryEncoding.md),
 and for the human-readable text representation consult [Text Format](TextFormat.md).
 
+Each function body consists of a list of expressions. All expressions and
+operators are typed, with no implicit conversions or overloading rules.
+
 Verification of WebAssembly code requires only a single pass with constant-time
 type checking and well-formedness checking.
 
@@ -104,10 +109,9 @@ default linear memories but [new memory operators](FutureFeatures.md#multiple-ta
 may be added after the MVP which can also access non-default memories.
 
 Linear memories (default or otherwise) can either be [imported](Modules.md#imports)
-or [defined inside the module](Modules.md#linear-memory-section), with defaultness
-indicated by a flag on the import or definition. After import or definition,
-there is no difference when accessing a linear memory whether it was imported or
-defined internally.
+or [defined inside the module](Modules.md#linear-memory-section). After import
+or definition, there is no difference when accessing a linear memory whether it
+was imported or defined internally.
 
 In the MVP, linear memory cannot be shared between threads of execution.
 The addition of [threads](PostMVP.md#threads) will allow this.
@@ -265,10 +269,9 @@ defined by the host environment.
 Every WebAssembly [instance](Modules.md) has one specially-designated *default*
 table which is indexed by [`call_indirect`](#calls) and other future
 table operators. Tables can either be [imported](Modules.md#imports) or 
-[defined inside the module](Modules.md#table-section), with defaultness
-indicated by a flag on the import or definition. After import or definition,
-there is no difference when calling into a table whether it was imported or
-defined internally.
+[defined inside the module](Modules.md#table-section). After import or
+definition, there is no difference when calling into a table whether it was
+imported or defined internally.
 
 In the MVP, the primary purpose of tables is to implement indirect function
 calls in C/C++ using an integer index as the pointer-to-function and the table
@@ -343,9 +346,12 @@ a value and may appear as children of other expressions.
 ### Branches and nesting
 
 The `br` and `br_if` constructs express low-level branching.
-Branches may only reference labels defined by an outer *enclosing construct*.
-This means that, for example, references to a `block`'s label can only occur 
-within the `block`'s body.
+Branches may only reference labels defined by an outer *enclosing construct*,
+which can be a `block` (with a label at the `end`), `loop` (with a label at the
+beginning), `if` (with a label at the `end` or `else`), `else` (with a label at
+the `end`), or the function body (with a label at the `end`). This means that,
+for example, references to a `block`'s label can only occur within the
+`block`'s body.
 
 In practice, outer `block`s can be used to place labels for any given branching
 pattern, except for one restriction: one can't branch into the middle of a loop
@@ -365,7 +371,7 @@ The `nop`, `br`, `br_if`, `br_table`, and `return` constructs do not yield value
 Other control constructs may yield values if their subexpressions yield values:
 
 * `block`: yields either the value of the last expression in the block or the result of an inner branch that targeted the label of the block
-* `loop`: yields either the value of the last expression in the loop or the result of an inner branch that targeted the end label of the loop
+* `loop`: yields the value of the last expression in the loop
 * `if`: yields either the value of the last *then* expression or the last *else* expression or the result of an inner branch that targeted the label of one of these.
 
 In all constructs containing block-like sequences of expressions, all expressions but the last must not yield a value.
diff --git a/BinaryEncoding.md b/BinaryEncoding.md
index 90e6638b..d6fdbdcb 100644
--- a/BinaryEncoding.md
+++ b/BinaryEncoding.md
@@ -8,7 +8,7 @@ See the [rationale document](Rationale.md#why-a-binary-encoding) for more detail
 
 The encoding is split into three layers:
 
-* **Layer 0** is a simple post-order encoding of the AST and related data structures.
+* **Layer 0** is a simple binary encoding of the bytecode instructions and related data structures.
   The encoding is dense and trivial to interact with, making it suitable for
   scenarios like JIT, instrumentation tools, and debugging.
 * **Layer 1** provides structural compression on top of layer 0, exploiting
@@ -31,50 +31,67 @@ for a proposal for layer 1 structural compression.
 
 # Data types
 
-### uint8
-A single-byte unsigned integer.
+### `uintN`
+An unsigned integer of _N_ bits,
+represented in _N_/8 bytes in [little endian](https://en.wikipedia.org/wiki/Endianness#Little-endian) order.
+_N_ is either 8, 16, or 32.
 
-### uint32
-A four-byte little endian unsigned integer.
+### `varuintN`
+A [LEB128](https://en.wikipedia.org/wiki/LEB128) variable-length integer, limited to _N_ bits (i.e., the values [0, 2^_N_-1]),
+represented by _at most_ ceil(_N_/7) bytes that may contain padding `0x80` bytes.
 
-### varint32
-A [Signed LEB128](https://en.wikipedia.org/wiki/LEB128#Signed_LEB128) variable-length integer, limited to int32 values.
+Note: Currently, the only sizes used are `varuint1`, `varuint7`, and `varuint32`,
+where the former two are used for compatibility with potential future extensions.
 
-### varuint1
-A [LEB128](https://en.wikipedia.org/wiki/LEB128) variable-length integer, limited to the values 0 or 1. `varuint1` values may contain leading zeros. (This type is mainly used for compatibility with potential future extensions.)
+### `varintN`
+A [Signed LEB128](https://en.wikipedia.org/wiki/LEB128#Signed_LEB128) variable-length integer, limited to _N_ bits (i.e., the values [-2^(_N_-1), +2^(_N_-1)-1]),
+represented by _at most_ ceil(_N_/7) bytes that may contain padding `0x80` or `0xFF` bytes.
 
-### varuint7
-A [LEB128](https://en.wikipedia.org/wiki/LEB128) variable-length integer, limited to the values [0, 127]. `varuint7` values may contain leading zeros. (This type is mainly used for compatibility with potential future extensions.)
+Note: Currently, the only sizes used are `varint32` and `varint64`.
 
-### varuint32
-A [LEB128](https://en.wikipedia.org/wiki/LEB128) variable-length integer, limited to uint32 values. `varuint32` values may contain leading zeros.
-
-### varint64
-A [Signed LEB128](https://en.wikipedia.org/wiki/LEB128#Signed_LEB128) variable-length integer, limited to int64 values.
-
-### value_type
+### `value_type`
 A single-byte unsigned integer indicating a [value type](AstSemantics.md#types). These types are encoded as:
 * `1` indicating type `i32` 
 * `2` indicating type `i64` 
 * `3` indicating type `f32` 
 * `4` indicating type `f64`
 
+### `inline_signature_type`
+A single-byte unsigned integer indicating a signature. These types are encoded as:
+* `0` indicating a signature with 0 results.
+* `1` indicating a signature with 1 result of type `i32`.
+* `2` indicating a signature with 1 result of type `i64`.
+* `3` indicating a signature with 1 result of type `f32`.
+* `4` indicating a signature with 1 result of type `f64`.
+
+### `external_kind`
+A single-byte unsigned integer indicating the kind of definition being imported or defined:
+* `0` indicating a `Function` [import](Modules.md#imports) or [definition](Modules.md#function-and-code-sections)
+* `1` indicating a `Table` [import](Modules.md#imports) or [definition](Modules.md#table-section)
+* `2` indicating a `Memory` [import](Modules.md#imports) or [definition](Modules.md#linear-memory-section)
+* `3` indicating a `Global` [import](Modules.md#imports) or [definition](Modules.md#global-section)
+
+### `resizable_limits`
+A packed tuple that describes the limits of a
+[table](AstSemantics.md#table) or [memory](AstSemantics.md#resizing):
 
-# Definitions
+| Field | Type | Description |
+| ----- |  ----- | ----- |
+| flags | `varuint32` | bit `0x1` is set if the maximum field is present |
+| initial | `varuint32` | initial length (in units of table elements or wasm pages) |
+| maximum | `varuint32`? | only present if specified by `flags` |
 
-### Post-order encoding
-Refers to an approach for encoding syntax trees, where each node begins with an identifying binary
-sequence, then followed recursively by any child nodes. 
+The "flags" field may later be extended to include a flag for sharing (between
+threads).
 
-* Examples
-  * Given a simple AST node: `i32.add(left: AstNode, right: AstNode)`
-    * First recursively write the left and right child nodes.
-    * Then write the opcode for `i32.add` (uint8)
+### `init_expr`
+The encoding of an [initializer expression](Modules.md#initializer-expression)
+is the normal encoding of the expression followed by the `end` opcode as a
+delimiter.
 
-  * Given a call AST node: `call(args: AstNode[], callee_index: varuint32)`
-    * First recursively write each argument node.
-    * Then write the (variable-length) integer `callee_index` (varuint32)
-    * Finally write the opcode of `Call` (uint8)
+Note that `get_global` in an initializer expression can only refer to immutable
+imported globals and all uses of `init_expr` can only appear after the Imports
+section.
 
 # Module structure
 
@@ -87,34 +104,41 @@ The module starts with a preamble of two fields:
 | Field | Type | Description |
 | ----- |  ----- | ----- |
 | magic number | `uint32` |  Magic number `0x6d736100` (i.e., '\0asm') |
-| version | `uint32` | Version number, currently 10. The version for MVP will be reset to 1. |
+| version | `uint32` | Version number, currently 12. The version for MVP will be reset to 1. |
 
-This preamble is followed by a sequence of sections. Each section is identified by an
-immediate string. Sections whose identity is unknown to the WebAssembly
-implementation are ignored and this is supported by including the size in bytes
-for all sections. The encoding of sections is structured as follows:
+The module preamble is followed by a sequence of sections.
+Each section is identified by a 1-byte *section code* that encodes either a known section or a user-defined section.
+The section length and payload data then follow.
+Known sections have non-zero ids, while unknown sections have a `0` id followed by an identifying string as
+part of the payload.
+Unknown sections are ignored by the WebAssembly implementation, and thus validation errors within them do not
+invalidate a module.
 
 | Field | Type | Description |
 | ----- |  ----- | ----- |
-| id_len | `varuint32` | section identifier string length |
-| id_str | `bytes` | section identifier string of id_len bytes |
+| id | `varuint7` | section code |
 | payload_len  | `varuint32` | size of this section in bytes |
-| payload_str  | `bytes` | content of this section, of length payload_len |
+| name_len | `varuint32` ? | length of the section name in bytes, present if `id == 0` |
+| name | `bytes` ? | section name string, present if `id == 0` |
+| payload_data  | `bytes` | content of this section, of length `payload_len - sizeof(name) - sizeof(name_len)` |
 
 Each section is optional and may appear at most once.
-Known sections (from this list) may not appear out of order.
-The content of each section is encoded in its `payload_str`.
-
-* [Type](#type-section) section
-* [Import](#import-section) section
-* [Function](#function-section) section
-* [Table](#table-section) section
-* [Memory](#memory-section) section
-* [Export](#export-section) section
-* [Start](#start-section) section
-* [Code](#code-section) section
-* [Data](#data-section) section
-* [Name](#name-section) section
+Known sections from this list may not appear out of order.
+The content of each section is encoded in its `payload_data`.
+
+| Section Name | Code | Description |
+| ------------ | ---- | ----------- |
+| [Type](#type-section) | `1` | Function signature declarations |
+| [Import](#import-section) | `2` | Import declarations |
+| [Function](#function-section) | `3` | Function declarations |
+| [Table](#table-section) | `4` | Indirect function table and other tables |
+| [Memory](#memory-section) | `5` | Memory attributes |
+| [Global](#global-section) | `6` | Global declarations |
+| [Export](#export-section) | `7` | Exports | 
+| [Start](#start-section) | `8` | Start function declaration |
+| [Element](#element-section) | `9` | Elements section |
+| [Code](#code-section) | `10` | Function bodies (code) |
+| [Data](#data-section) | `11` | Data segments |
 
 The end of the last present section must coincide with the last byte of the
 module. The shortest valid module is 8 bytes (`magic number`, `version`,
@@ -122,18 +146,16 @@ followed by zero sections).
 
 ### Type section
 
-ID: `type`
-
 The type section declares all function signatures that will be used in the module.
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of type entries to follow |
 | entries | `type_entry*` | repeated type entries as described below |
 
 #### Type entry
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | form | `varuint7` | `0x40`, indicating a function type |
 | param_count | `varuint32` | the number of parameters to the function |
 | param_types | `value_type*` | the parameter types of the function |
@@ -144,89 +166,163 @@ The type section declares all function signatures that will be used in the modul
 
 ### Import section
 
-ID: `import`
-
 The import section declares all imports that will be used in the module.
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of import entries to follow |
 | entries | `import_entry*` | repeated import entries as described below |
 
 #### Import entry
 | Field | Type | Description |
-| ----- |  ----- | ----- |
-| sig_index | `varuint32` | signature index of the import |
+| ----- | ---- | ----------- |
 | module_len | `varuint32` | module string length |
 | module_str | `bytes` | module string of `module_len` bytes |
-| function_len | `varuint32` | function string length |
-| function_str | `bytes` | function string of `function_len` bytes |
+| field_len | `varuint32` | field name length |
+| field_str | `bytes` | field name string of `field_len` bytes |
+| kind | `external_kind` | the kind of definition being imported |
 
-### Function section
+Followed by, if the `kind` is `Function`:
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| sig_index | `varuint32` | signature index of the import |
+
+or, if the `kind` is `Table`:
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| element_type | `varuint7` | `0x20`, indicating [`anyfunc`](AstSemantics.md#table) |
+| | `resizable_limits` | see [above](#resizable_limits) |
+
+or, if the `kind` is `Memory`:
 
-ID: `function`
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| | `resizable_limits` | see [above](#resizable_limits) |
+
+or, if the `kind` is `Global`:
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| type | `value_type` | type of the imported global |
+| mutability | `varuint1` | `0` if immutable, `1` if mutable; must be `0` in the MVP |
+
+### Function section
 
 The function section _declares_ the signatures of all functions in the
 module (their definitions appear in the [code section](#code-section)).
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of signature indices to follow |
 | types | `varuint32*` | sequence of indices into the type section |
 
 ### Table section
 
-ID: `table`
-
-The table section defines the module's
-[indirect function table](AstSemantics.md#calls).
+The encoding of a [Table section](Modules.md#table-section):
 
 | Field | Type | Description |
 | ----- |  ----- | ----- |
-| count | `varuint32` | count of entries to follow |
-| entries | `varuint32*` | repeated indexes into the function section |
+| count | `varuint32` | indicating the number of tables defined by the module |
+| entries | `table_type*` | repeated `table_type` entries as described below |
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| element_type | `varuint7` | `0x20`, indicating [`anyfunc`](AstSemantics.md#table) |
+| | `resizable_limits` | see [above](#resizable_limits) |
+
+In the MVP, the number of tables must be no more than 1.
 
 ### Memory section
 
 ID: `memory`
 
-The memory section declares the size and characteristics of the memory
-associated with the module.
+The encoding of a [Memory section](Modules.md#linear-memory-section):
 
 | Field | Type | Description |
 | ----- |  ----- | ----- |
-| initial | `varuint32` | initial memory size in 64KiB pages |
-| maximum | `varuint32` | maximum memory size in 64KiB pages |
-| exported | `uint8` | `1` if the memory is visible outside the module |
+| count | `varuint32` | indicating the number of memories defined by the module |
+| entries | `memory_type*` | repeated `memory_type` entries as described below |
 
-### Export section
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| | `resizable_limits` | see [above](#resizable_limits) |
+
+Note that the initial/maximum fields are specified in units of 
+[WebAssembly pages](AstSemantics.md#linear-memory).
 
-ID: `export`
+In the MVP, the number of memories must be no more than 1.
 
-The export section declares all exports from the module.
+### Global section
+
+The encoding of the [Global section](Modules.md#global-section):
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
+| count | `varuint32` | count of global variable entries |
+| globals | `global_variable*` | global variables, as described below |
+
+#### Global Entry
+
+Each `global_variable` declares a single global variable of a given type, mutability
+and with the given initializer.
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| type | `value_type` | type of the variables |
+| mutability | `varuint1` | `0` if immutable, `1` if mutable |
+| init | `init_expr` | the initial value of the global |
+
+Note that, in the MVP, only immutable global variables can be exported.
+
+### Export section
+
+The encoding of the [Export section](Modules.md#exports):
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of export entries to follow |
 | entries | `export_entry*` | repeated export entries as described below |
 
 #### Export entry
 | Field | Type | Description |
-| ----- |  ----- | ----- |
-| func_index | `varuint32` | index into the function table |
-| function_len | `varuint32` | function string length |
-| function_str | `bytes` | function string of `function_len` bytes |
+| ----- | ---- | ----------- |
+| field_len | `varuint32` | field name string length |
+| field_str | `bytes` | field name string of `field_len` bytes |
+| kind | `external_kind` | the kind of definition being exported |
+| index | `varuint32` | the index into the corresponding [index space](Modules.md) |
 
-### Start section
+For example, if the "kind" is `Function`, then "index" is a 
+[function index](Modules.md#function-index-space). Note that, in the MVP, the
+only valid index value for a memory or table export is 0.
 
-ID: `start`
+### Start section
 
 The start section declares the [start function](Modules.md#module-start-function).
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | index | `varuint32` | start function index |
 
+### Element section
+
+The encoding of the [Elements section](Modules.md#elements-section):
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| count | `varuint32` | count of element segments to follow |
+| entries | `elem_segment*` | repeated element segments as described below |
+
+a `elem_segment` is:
+
+| Field | Type | Description |
+| ----- | ---- | ----------- |
+| index | `varuint32` | the [table index](Modules.md#table-index-space) (0 in the MVP) |
+| offset | `init_expr` | an `i32` initializer expression that computes the offset at which to place the elements |
+| num_elem | `varuint32` | number of elements to follow |
+| elems | `varuint32*` | sequence of [function indices](Modules.md#function-index-space) |
+
 ### Code section
 
 ID: `code`
@@ -236,44 +332,43 @@ The count of function declared in the [function section](#function-section)
 and function bodies defined in this section must be the same and the `i`th
 declaration corresponds to the `i`th function body.
 
-| Field | Type |  Description |
-| ----- |  ----- |  ----- |  ----- |
+| Field | Type | Description |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of function bodies to follow |
 | bodies | `function_body*` | sequence of [Function Bodies](#function-bodies) |
 
 ### Data section
 
-ID: `data`
-
 The data section declares the initialized data that is loaded
 into the linear memory.
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of data segments to follow |
 | entries | `data_segment*` | repeated data segments as described below |
 
 a `data_segment` is:
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
-| offset | `varuint32` | the offset in linear memory at which to store the data |
+| ----- | ---- | ----------- |
+| index | `varuint32` | the [linear memory index](Modules.md#linear-memory-index-space) (0 in the MVP) |
+| offset | `init_expr` | an `i32` initializer expression that computes the offset at which to place the data |
 | size | `varuint32` | size of `data` (in bytes) |
 | data | `bytes` | sequence of `size` bytes |
 
 ### Name section
 
-ID: `name`
+User-defined section string: `"name"`
 
-The names section does not change execution semantics and a validation error in
-this section does not cause validation for the whole module to fail and is
-instead treated as if the section was absent. The expectation is that, when a
-binary WebAssembly module is viewed in a browser or other development
+The names section does not change execution semantics, and thus is not allocated a section code.
+It is encoded as an unknown section (id `0`) followed by the identification string `"name"`.
+Like all unknown sections, a validation error in this section does not cause validation of the module to fail.
+The expectation is that, when a binary WebAssembly module is viewed in a browser or other development
 environment, the names in this section will be used as the names of functions
 and locals in the [text format](TextFormat.md).
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | count | `varuint32` | count of entries to follow |
 | entries | `function_names*` | sequence of names |
 
@@ -284,7 +379,7 @@ functions.
 #### Function names
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | fun_name_len | `varuint32` | string length, in bytes |
 | fun_name_str | `bytes` | valid utf8 encoding |
 | local_count | `varuint32` | count of local names to follow |
@@ -296,25 +391,23 @@ count may be greater or less than the actual number of locals.
 #### Local name
 
 | Field | Type | Description |
-| ----- |  ----- | ----- |
+| ----- | ---- | ----------- |
 | local_name_len | `varuint32` | string length, in bytes |
 | local_name_str | `bytes` | valid utf8 encoding |
 
 
 # Function Bodies
 
-Function bodies consist of a sequence of local variable declarations followed by a 
-dense post-order encoding of an [Abstract Syntax Tree](AstSemantics.md).
-Each node in the abstract syntax tree corresponds to an operator, such as `i32.add` or `if` or `block`.
-Operators are encoding by an opcode byte followed by immediate bytes (if any), followed by children 
-nodes (if any).
+Function bodies consist of a sequence of local variable declarations followed by 
+[bytecode instructions](AstSemantics.md). Each function body must end with the `end` opcode.
 
-| Field | Type |Description |
-| ----- | ----- | ----- |
+| Field | Type | Description |
+| ----- | ---- | ----------- |
 | body_size | `varuint32` | size of function body to follow, in bytes |
 | local_count | `varuint32` | number of local entries |
 | locals | `local_entry*` | local variables |
-| ast    | `byte*` | post-order encoded AST |
+| code | `byte*` | bytecode of the function |
+| end | `byte` | `0x0f`, indicating the end of the body |
 
 #### Local Entry
 
@@ -322,7 +415,7 @@ Each local entry declares a number of local variables of a given type.
 It is legal to have several entries with the same type.
 
 | Field | Type | Description |
-| ----- | ----- | ----- |
+| ----- | ---- | ----------- |
 | count | `varuint32` | number of local variables of the following type |
 | type | `value_type` | type of the variables |
 
@@ -331,32 +424,30 @@ It is legal to have several entries with the same type.
 
 | Name | Opcode | Immediates | Description |
 | ---- | ---- | ---- | ---- |
-| `nop` | `0x00` | | no operation |
-| `block` | `0x01` |  | begin a sequence of expressions, the last of which yields a value |
-| `loop` | `0x02` |  | begin a block which can also form control flow loops |
-| `if` | `0x03` | | begin if expression |
+| `unreachable` | `0x00` | | trap immediately |
+| `block` | `0x01` | sig : `inline_signature_type` | begin a sequence of expressions, yielding 0 or 1 values |
+| `loop` | `0x02` |  sig : `inline_signature_type` | begin a block which can also form control flow loops |
+| `if` | `0x03` | sig : `inline_signature_type` | begin if expression |
 | `else` | `0x04` | | begin else expression of if |
 | `select` | `0x05` | | select one of two values based on condition |
-| `br` | `0x06` | argument_count : `varuint1`, relative_depth : `varuint32` | break that targets an outer nested block |
-| `br_if` | `0x07` | argument_count : `varuint1`, relative_depth : `varuint32` | conditional break that targets an outer nested block |
+| `br` | `0x06` | relative_depth : `varuint32` | break that targets an outer nested block |
+| `br_if` | `0x07` | relative_depth : `varuint32` | conditional break that targets an outer nested block |
 | `br_table` | `0x08` | see below | branch table control flow construct |
-| `return` | `0x09` | argument_count : `varuint1` | return zero or one value from this function |
-| `unreachable` | `0x0a` | | trap immediately |
+| `return` | `0x09` | | return zero or one value from this function |
 | `drop` | `0x0b` | | ignore value |
+| `nop` | `0x0a` | | no operation |
 | `end` | `0x0f` | | end a block, loop, or if |
 
-Note that there is no explicit `if_else` opcode, as the else clause is encoded with the `else` bytecode.
-
-The counts following the break and return operators specify how many preceding operands are taken as transfer arguments; in the MVP, all these values must be either 0 or 1.
+The _sig_ fields of `block` and `if` operators specify function signatures
+which describe their use of the operand stack.
 
 The `br_table` operator has an immediate operand which is encoded as follows:
 
 | Field | Type | Description |
 | ---- | ---- | ---- |
-| arity | `varuint1` | number of arguments |
-| target_count | `varuint32` | number of targets in the target_table |
-| target_table | `uint32*` | target entries that indicate an outer block or loop to which to break |
-| default_target | `uint32` | an outer block or loop to which to break in the default case |
+| target_count | `varuint32` | number of entries in the target_table |
+| target_table | `varuint32*` | target entries that indicate an outer block or loop to which to break |
+| default_target | `varuint32` | an outer block or loop to which to break in the default case |
 
 The `br_table` operator implements an indirect branch. It accepts an optional value argument
 (like other branches) and an additional `i32` expression as input, and 
@@ -374,11 +465,12 @@ out of range, `br_table` branches to the default target.
 | `get_local` | `0x14` | local_index : `varuint32` | read a local variable or parameter |
 | `set_local` | `0x15` | local_index : `varuint32` | write a local variable or parameter |
 | `tee_local` | `0x19` | local_index : `varuint32` | write a local variable or parameter and return the same value |
-| `call` | `0x16` | argument_count : `varuint1`, function_index : `varuint32` | call a function by its index |
-| `call_indirect` | `0x17` | argument_count : `varuint1`, type_index : `varuint32` | call a function indirect with an expected signature |
-| `call_import` | `0x18` | argument_count : `varuint1`, import_index : `varuint32` | call an imported function by its index |
+| `get_global` | `0xbb` | global_index : `varuint32` | read a global variable |
+| `set_global` | `0xbc` | global_index : `varuint32` | write a global variable |
+| `call` | `0x16` | function_index : `varuint32` | call a function by its [index](Modules.md#function-index-space) |
+| `call_indirect` | `0x17` | type_index : `varuint32` | call a function indirect with an expected signature |
 
-The counts following the different call opcodes specify the number of preceding operands taken as arguments.
+The `call_indirect` operator takes a list of function arguments and as the last operand the index into the table.
 
 ## Memory-related operators ([described here](AstSemantics.md#linear-memory-accesses))
 
diff --git a/FutureFeatures.md b/FutureFeatures.md
index 0ae0a631..3f373bd8 100644
--- a/FutureFeatures.md
+++ b/FutureFeatures.md
@@ -315,7 +315,7 @@ operators the possibility of having side effects.
 Debugging techniques are also important, but they don't necessarily need to be
 in the spec itself. Implementations are welcome (and encouraged) to support
 non-standard execution modes, enabled only from developer tools, such as modes
-with alternate rounding, or evaluation of floating point expressions at greater
+with alternate rounding, or evaluation of floating point operators at greater
 precision, to support [techniques for detecting numerical instability]
 (https://www.cs.berkeley.edu/~wkahan/Mindless.pdf), or modes using alternate
 NaN bitpattern rules, to carry diagnostic information and help developers track
@@ -370,8 +370,8 @@ general-purpose use on several of today's popular hardware architectures.
 ## Better feature testing support
 
 The [MVP feature testing situation](FeatureTest.md) could be improved by
-allowing unknown/unsupported AST operators to decode and validate. The runtime
-semantics of these unknown operators could either be to trap or call a
+allowing unknown/unsupported instructions to decode and validate. The runtime
+semantics of these unknown instructions could either be to trap or call a
 same-signature module-defined polyfill function. This feature could provide a
 lighter-weight alternative to load-time polyfilling (approach 2 in
 [FeatureTest.md](FeatureTest.md)), especially if the [specific layer](BinaryEncoding.md)
@@ -442,7 +442,7 @@ see [JavaScript's `WebAssembly.Table` API](JS.md#webassemblytable-objects)).
 It would be useful to be able to do everything from within WebAssembly so, e.g.,
 it was possible to write a WebAssembly dynamic loader in WebAssembly. As a
 prerequisite, WebAssembly would need first-class support for 
-[GC references](GC.md) in expressions and locals. Given that, the following
+[GC references](GC.md) on the stack and in locals. Given that, the following
 could be added:
 * `get_table`/`set_table`: get or set the table element at a given dynamic
   index; the got/set value would have a GC reference type
diff --git a/JS.md b/JS.md
index 5d01edb0..1c235f7e 100644
--- a/JS.md
+++ b/JS.md
@@ -66,7 +66,7 @@ asynchronous, background, streaming compilation.
 A `WebAssembly.Module` object represents the stateless result of compiling a
 WebAssembly binary-format module and contains one internal slot:
  * [[Module]] : an [`Ast.module`](https://github.com/WebAssembly/spec/blob/master/ml-proto/spec/ast.ml#L208)
-   which is the spec definition of a validated module AST
+   which is the spec definition of a validated module
 
 ### `WebAssembly.Module` Constructor
 
@@ -82,8 +82,8 @@ If the given `bytes` argument is not a
 a `TypeError` exception is thrown.
 
 Otherwise, this function performs synchronous compilation of the `BufferSource`:
-* The byte range delimited by the `BufferSource` is first logically decoded into
-  an AST according to [BinaryEncoding.md](BinaryEncoding.md) and then validated
+* The byte range delimited by the `BufferSource` is first logically decoded 
+  according to [BinaryEncoding.md](BinaryEncoding.md) and then validated
   according to the rules in [spec/check.ml](https://github.com/WebAssembly/spec/blob/master/ml-proto/spec/check.ml#L325).
 * The spec `string` values inside `Ast.module` are decoded as UTF8 as described in 
   [Web.md](Web.md#names).
diff --git a/MVP.md b/MVP.md
index 7340c565..1d3a978c 100644
--- a/MVP.md
+++ b/MVP.md
@@ -12,14 +12,14 @@ The major design components of the MVP have been broken up into separate
 documents:
 * The distributable, loadable and executable unit of code in WebAssembly
   is called a [module](Modules.md).
-* The behavior of WebAssembly code in a module is specified in terms of an
-  [AST](AstSemantics.md).
+* The behavior of WebAssembly code in a module is specified in terms of 
+  [instructions](AstSemantics.md) for a structured stack machine.
 * The WebAssembly binary format, which is designed to be natively decoded by 
   WebAssembly implementations, is specified as a 
-  [binary serialization](BinaryEncoding.md) of a module's AST.
+  [binary encoding](BinaryEncoding.md) of a module's structure and code.
 * The WebAssembly text format, which is designed to be read and written when
   using tools (e.g., assemblers, debuggers, profilers), is specified as a
-  [textual projection](TextFormat.md) of a module's AST.
+  [textual projection](TextFormat.md) of a module's structure and code.
 * WebAssembly is designed to be implemented both [by web browsers](Web.md)
   and [completely different execution environments](NonWeb.md).
 * To ease the transition to WebAssembly while native support is still
diff --git a/Modules.md b/Modules.md
index ffaedaf1..9c24365d 100644
--- a/Modules.md
+++ b/Modules.md
@@ -64,7 +64,7 @@ of the global variable. These fields have the same meaning as in the
 [Global section](#global-section).
 
 A *linear memory import* includes the same set of fields defined in the
-[Linear Memory section](#linear-memory-section): *default flag*, *initial
+[Linear Memory section](#linear-memory-section):  *initial
 length* and optional *maximum length*. The host environment must only allow
 imports of WebAssembly linear memories that have initial length
 *greater-or-equal* than the initial length declared in the import and that have
@@ -72,20 +72,17 @@ maximum length *less-or-equal* than the maximum length declared in the import.
 This ensures that separate compilation can assume: memory accesses below the
 declared initial length are always in-bounds, accesses above the declared
 maximum length are always out-of-bounds and if initial equals maximum, the
-length is fixed. If the default flag is set, the imported memory is used as
-the [default memory](AstSemantics.md#linear-memory) and at most one linear
-memory definition (import or internal) may have the default flag set. In the
-MVP, it is a validation error not to set the default flag.
+length is fixed. In the MVP, every memory is a [default memory](AstSemantics.md#linear-memory)
+and thus there may be at most one linear memory import or linear memory
+section.
 
 A *table import* includes the same set of fields defined in the 
-[Table section](#table-section): *default flag*, *element type*, *initial
+[Table section](#table-section): *element type*, *initial
 length* and optional *maximum length*. As with the linear memory section, the
 host environment must ensure only WebAssembly tables are imported with
 exactly-matching element type, greater-or-equal initial length, and
-less-or-equal maximum length. If the default flag is set, the imported table
-is used as the [default table](AstSemantics.md#table) and at most one table
-definition (import or internal) may have the default flag set. In the MVP, it is
-a validation error not to set the default flag.
+less-or-equal maximum length. In the MVP, every table is a [default table](AstSemantics.md#table)
+and thus there may be at most one table import or table section.
 
 Since the WebAssembly spec does not define how import names are interpreted:
 * the [Web environment](Web.md#names) defines names to be UTF8-encoded strings;
@@ -207,16 +204,10 @@ Each global variable internal definition declares its *type*
 
 ## Linear memory section
 
-The *linear memory section* provides an internal definition of zero or more
-[linear memories](AstSemantics.md#linear-memory). In the MVP, the total number
-of linear memory definitions is limited to 1, but this may be relaxed in the
-[future](FutureFeatures.md#multiple-tables-and-memories).
-
-A linear memory definition may declare itself to be the 
-[default](AstSemantics.md#linear-memory) linear memory of the module. At most
-one linear memory definition may declare itself to be the default. In the MVP,
-if there is a linear memory definition, it *must* declare itself the default
-(there is no way to access non-default linear memories anyhow).
+The *linear memory section* provides an internal definition of one
+[linear memory](AstSemantics.md#linear-memory). In the MVP, every memory is a
+default memory and thus there may be at most one linear memory import or linear
+memory section.
 
 Each linear memory section declares an *initial* [memory size](AstSemantics.md#linear-memory)
 (which may be subsequently increased by [`grow_memory`](AstSemantics.md#resizing)) and an
@@ -243,17 +234,10 @@ value (defining the length of the given segment). The `offset` is an
 ## Table section
 
 The *table section* contains zero or more definitions of distinct 
-[tables](AstSemantics.md#table). In the MVP, the total number
-of table definitions is limited to 1, but this may be relaxed in the
-[future](FutureFeatures.md#multiple-tables-and-memories).
-
-A table definition may declare itself to be the
-[default](AstSemantics.md#table) table of the module. At most
-one table definition may declare itself to be the default. In the MVP,
-if there is a table definition, it *must* declare itself the default
-(there is no way to access non-default tables anyhow).
+[tables](AstSemantics.md#table). In the MVP, every table is a 
+default table and thus there may be at most one table import or table section.
 
-Each table definition also includes an *element type*, *initial length*, and
+Each table definition declares an *element type*, *initial length*, and
 optional *maximum length*.
 
 In the MVP, the only valid element type is `"anyfunc"`, but in the
@@ -285,9 +269,7 @@ specify the initial contents of fixed `(offset, length)` ranges of a given
 table, specified by its [table index](#table-index-space). The `length` is an
 integer constant value (defining the length of the given segment). The `offset`
 is an [initializer expression](#initializer-expression). Elements are specified
-with a `(type, index)` pair where `type` is the element type of an
-[index space](Modules.md) that is compatible with the table's element type and
-`index` is an integer immediate into `type`s index space.
+by their index into the corresponding [index space](Modules.md).
 
 ## Function and Code sections
 
diff --git a/Rationale.md b/Rationale.md
index ee29f952..fd194bd0 100644
--- a/Rationale.md
+++ b/Rationale.md
@@ -13,10 +13,18 @@ codebases, we'll revisit the alternatives listed below, reevaluate the tradeoffs
 and update the [design](AstSemantics.md) before the MVP is finalized.
 
 
-## Why AST?
-
-Why not a register- or SSA-based bytecode?
-* Trees allow a smaller binary encoding: [JSZap][], [Slim Binaries][].
+## Why a stack machine?
+
+Why not an AST, or a register- or SSA-based bytecode?
+
+* We started with an AST and generalized to a [structured stack machine](AstSemantics.md). ASTs allow a 
+  dense encoding and efficient decoding, compilation, and interpretation.
+  The structured stack machine of WebAssembly is a generalization of ASTs allowed in previous versions while allowing
+  efficiency gains in interpretation and baseline compilation, as well as a straightforward 
+  design for multi-return functions.
+* The stack machine allows smaller binary encoding than registers or SSA [JSZap][], [Slim Binaries][],
+  and structured control flow allows simpler and more efficient verification, including decoding directly
+  to a compiler's internal SSA form.
 * [Polyfill prototype][] shows simple and efficient translation to asm.js.
 
   [JSZap]: https://research.microsoft.com/en-us/projects/jszap/
@@ -26,15 +34,12 @@ Why not a register- or SSA-based bytecode?
 
 ## Why not a fully-general stack machine?
 
-Stack machines have all the code size advantages as expression trees represented
-in post-order. However, we wish to avoid requiring an explicit expression stack at
-runtime, because many implementations will want to use registers rather than an
-actual stack for evaluation. Consequently, while it's possible to think about
-wasm expression evaluation in terms of a conceptual stack machine, the stack
-machine would be constrained such that one can always statically know the types,
-definitions, and uses of all operands on the stack, so that an implementation can
-connect definitions with their uses through whatever mechanism they see fit.
-
+The WebAssembly stack machine is restricted to structured control flow and structured
+use of the stack. This greatly simplifies one-pass verification, avoiding a fixpoint computation
+like that of other stack machines such as the Java Virtual Machine (prior to [stack maps](https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html)).
+This also simplifies compilation and manipulation of WebAssembly code by other tools.
+Further generalization of the WebAssembly stack machine is planned post-MVP, such as the
+addition of multiple return values from control flow constructs and function calls.
 
 ## Basic Types Only
 
@@ -44,7 +49,7 @@ WebAssembly only represents [a few types](AstSemantics.md#Types).
   language compiler to express its own types in terms of the basic machine
   types. This allows WebAssembly to present itself as a virtual ISA, and lets
   compilers target it as they would any other ISA.
-* These types are efficiently executed by all modern CPU architectures.
+* These types are directly representable on all modern CPU architectures.
 * Smaller types (such as `i8` and `i16`) are usually no more efficient and in
   languages like C/C++ are only semantically meaningful for memory accesses
   since arithmetic get widened to `i32` or `i64`. Avoiding them at least for MVP
@@ -177,7 +182,7 @@ See [#107](https://github.com/WebAssembly/spec/pull/107).
 ## Control Flow
 
 Structured control flow provides simple and size-efficient binary encoding and
-compilation. Any control flow—even irreducible—can be transformed into structured
+compilation. Any control flow--even irreducible--can be transformed into structured
 control flow with the
 [Relooper](https://github.com/kripken/emscripten/raw/master/docs/paper.pdf)
 [algorithm](http://dl.acm.org/citation.cfm?id=2048224&CFID=670868333&CFTOKEN=46181900),
@@ -280,17 +285,18 @@ segregating the table per signature to require only a bounds check could be cons
 in the future. Also, if tables are small enough, an engine can internally use per-signature
 tables filled with failure handlers to avoid one check.
 
-## Expressions with Control Flow
+## Control Flow Instructions with Values
 
-Expression trees offer significant size reduction by avoiding the need for
-`set_local`/`get_local` pairs in the common case of an expression with only one
-immediate use. Control flow "statements" are in fact expressions with result
-values, thus allowing even more opportunities to build bigger
-expression trees and further reduce `set_local`/`get_local` usage (which
-constitute 30-40% of total bytes in the
+Control flow instructions such as `br`, `br_if`, `br_table`, `if` and `if-else` can 
+transfer stack values in WebAssembly. These primitives are useful building blocks for 
+WebAssembly producers, e.g. in compiling expression languages. It offers significant 
+size reduction by avoiding the need for `set_local`/`get_local` pairs in the common case 
+of an expression with only one immediate use. Control flow instructions can then model
+expressions with result values, thus allowing even more opportunities to further reduce
+`set_local`/`get_local` usage (which constitute 30-40% of total bytes in the
 [polyfill prototype](https://github.com/WebAssembly/polyfill-prototype-1)).
-Additionally, these primitives are useful building blocks for
-WebAssembly-generators (including the JavaScript polyfill prototype).
+`br`-with-value and `if` constructs that return values can model also model `phis` which
+appear in SSA representations of programs.
 
 
 ## Limited Local Nondeterminism
@@ -324,12 +330,11 @@ and local manner. This prevents the entire program from being invalid, as would
 be the case with C++ undefined behavior.
 
 As WebAssembly gets implemented and tested with multiple languages on multiple
-architectures there may be a need to revisit some of the decisions:
+architectures we may revisit some of the design decisions:
 
-* When all relevant hardware implement features the same way then there's no
-  need to add nondeterminism to WebAssembly when realistically there's only one
-  mapping from WebAssembly expression to ISA-specific operators. One such
-  example is floating-point: at a high-level most basic instructions follow
+* When all relevant hardware implements an operation the same way, there's no
+  need for nondeterminism in WebAssembly semantics. One such
+  example is floating-point: at a high-level most operators follow
   IEEE-754 semantics, it is therefore not necessary to specify WebAssembly's
   floating-point operators differently from IEEE-754.
 * When different languages have different expectations then it's unfortunate if
@@ -470,20 +475,20 @@ Yes:
     [this demo](https://github.com/lukewagner/AngryBotsPacked), comparing
     *just* parsing in SpiderMonkey (no validation, IR generation) to *just*
     decoding in the polyfill (no asm.js code generation).
-* A binary format enables optimizations that reduce the memory usage of decoded
-  ASTs without increasing size or reducing decode speed.
+* A binary format allows many optimizations for code size and decoding speed that would
+  not be possible on a source form.
 
 
 ## Why a layered binary encoding?
-* We can do better than generic compression because we are aware of the AST
+* We can do better than generic compression because we are aware of the code
   structure and other details:
   * For example, macro compression that
     [deduplicates AST trees](https://github.com/WebAssembly/design/issues/58#issuecomment-101863032)
-    can focus on AST nodes + their children, thus having `O(nodes)` entities
+    can focus on ASTs + their children, thus having `O(nodes)` entities
     to worry about, compared to generic compression which in principle would
     need to look at `O(bytes*bytes)` entities.  Such macros would allow the
     logical equivalent of `#define ADD1(x) (x+1)`, i.e., to be
-    parametrized. Simpler macros (`#define ADDX1 (x+1)`) can implement useful
+    parameterized. Simpler macros (`#define ADDX1 (x+1)`) can implement useful
     features like constant pools.
   * Another example is reordering of functions and some internal nodes, which
     we know does not change semantics, but