binji · April 12, 2018 21:10
diff --git a/gistfile1.txt b/gistfile1.txt
 4.2.12. Refers to the stack containing three kinds of entries "values", "labels", and "activations". Section 4.2.12.1 is called "Values", section 4.2.12.2 is called "Labels" but section 4.2.12.3 is called "Frames" instead.

 4.2.12.3. The return arity is named but not labeled here. "Activation frames carry the return arity of the respective function". It should be the same as label above where `n` is mentioned explicitly.

 4.2.13. "ultimately reducing the entire program to a single trap instruction", this isn't true when calling out to the embedder, right?

 4.2.13. Note #3. The link for the label reduction rule is broken, it should go to 4.4.6.2. Also, the rule is different in the note.

 4.2.13.2. What does "home" mean in "home module instance"?

 4.2.13.1. Better explanation of "the hole". It's not clear (to me) what it represents and how it works.

 4.2.13.3. What is the purpose of the second reduction rule? (Where a `frame` instruction on the stack is modified)

 4.3. Mention the meta-variable "z"?

 4.3. trunc is defined slightly different here than below in ftrunc_N: there `q` is explicitly annotated with a `+`.

 4.3.1.3. Is this bigendian instead? It looks like it extracts the most significant bits and puts it first in the byte sequence.

 4.3.2.14 - 4.3.2.17. All define the shift amount as `j_2`, but use `k` in the formula.

 4.3.3.1. sp: "correspondence"

 4.3.3.3 and others. it's a bit odd that the prose says `nans_N{z_1, z_2}` where the math says `nans_N{}` for the same thing.

 4.3.3.4. Is there meant to be a difference between fadd and fsub here? fsub has `fsub_N(\pm 0, \pm q_2) = \mp q_2` and fadd has the same thing but with z instead of q.

 4.3.4.4. `trunc` is not defined for `-0`, does it need a special case?

 4.3.4.6. Any "arithmetic" NaN of size N

 4.4.1. It might be nice to have some examples of this mapping, e.g. `add_i32(n1, n2) = iadd_32(n1, n2)`

 4.4.1.2. typo: `unop_t1_t2`

 4.4.1.3. typo: `binop_t1_t2`

 4.4.5.9. Mentioned in review for tailcall, I think -- `B^k` could be `B^\ast` here.

 4.4.8. The evaluation here has a different syntax than elsewhere in this section. Is this deliberate?

 4.5.3.2. typo: `tableinst`

 4.5.3.6 (similar in 4.5.3.7). Phrasing here is ambiguous, "not empty and smaller" doesn't make it clear whether it is `not(empty and smaller)` or `(not empty) and smaller`

 4.5.3.8. The `(where table^* = module.tables)` clause (and others) is a little confusing, since it doesn't seem to be used in the associated equation.

 4.5.3.8. I don't understand the allocx definition, it seems to be a recursive definition... oh, I see, it's actually not.

 4.5.3.8. What's up with `whereforalli`

 4.5.4. Not sure if there's another way, but it is a bit unclear that `val*` matches `val` described below. It is used before definition, and also wrapped differently.

 4.5.5. Discrepancy between prose and formal: formal mentions empty frame. Also, empty frame seems a little strange, maybe some explanation would help.
	4.2.12. Refers to the stack containing three kinds of entries "values", "labels", and "activations". Section 4.2.12.1 is called "Values", section 4.2.12.2 is called "Labels" but section 4.2.12.3 is called "Frames" instead.

	4.2.12.3. The return arity is named but not labeled here. "Activation frames carry the return arity of the respective function". It should be the same as label above where `n` is mentioned explicitly.

	4.2.13. "ultimately reducing the entire program to a single trap instruction", this isn't true when calling out to the embedder, right?

	4.2.13. Note #3. The link for the label reduction rule is broken, it should go to 4.4.6.2. Also, the rule is different in the note.

	4.2.13.2. What does "home" mean in "home module instance"?

	4.2.13.1. Better explanation of "the hole". It's not clear (to me) what it represents and how it works.

	4.2.13.3. What is the purpose of the second reduction rule? (Where a `frame` instruction on the stack is modified)

	4.3. Mention the meta-variable "z"?

	4.3. trunc is defined slightly different here than below in ftrunc_N: there `q` is explicitly annotated with a `+`.

	4.3.1.3. Is this bigendian instead? It looks like it extracts the most significant bits and puts it first in the byte sequence.

	4.3.2.14 - 4.3.2.17. All define the shift amount as `j_2`, but use `k` in the formula.

	4.3.3.1. sp: "correspondence"

	4.3.3.3 and others. it's a bit odd that the prose says `nans_N{z_1, z_2}` where the math says `nans_N{}` for the same thing.

	4.3.3.4. Is there meant to be a difference between fadd and fsub here? fsub has `fsub_N(\pm 0, \pm q_2) = \mp q_2` and fadd has the same thing but with z instead of q.

	4.3.4.4. `trunc` is not defined for `-0`, does it need a special case?

	4.3.4.6. Any "arithmetic" NaN of size N

	4.4.1. It might be nice to have some examples of this mapping, e.g. `add_i32(n1, n2) = iadd_32(n1, n2)`

	4.4.1.2. typo: `unop_t1_t2`

	4.4.1.3. typo: `binop_t1_t2`

	4.4.5.9. Mentioned in review for tailcall, I think -- `B^k` could be `B^\ast` here.

	4.4.8. The evaluation here has a different syntax than elsewhere in this section. Is this deliberate?

	4.5.3.2. typo: `tableinst`

	4.5.3.6 (similar in 4.5.3.7). Phrasing here is ambiguous, "not empty and smaller" doesn't make it clear whether it is `not(empty and smaller)` or `(not empty) and smaller`

	4.5.3.8. The `(where table^* = module.tables)` clause (and others) is a little confusing, since it doesn't seem to be used in the associated equation.

	4.5.3.8. I don't understand the allocx definition, it seems to be a recursive definition... oh, I see, it's actually not.

	4.5.3.8. What's up with `whereforalli`

	4.5.4. Not sure if there's another way, but it is a bit unclear that `val*` matches `val` described below. It is used before definition, and also wrapped differently.

	4.5.5. Discrepancy between prose and formal: formal mentions empty frame. Also, empty frame seems a little strange, maybe some explanation would help.