Splice validation prose

[f52985]

This PR splices the validation prose into the official document, mainly focusing on the validation of instructions.

The document contains the automatically generated and the manually written prose side by side, for the ease of comparison. Some of the notable differences are also noted inline.

@rossberg, please take a look and let us know if you have any idea to make it better.

[rossberg]

Sorry for the delay. I made a reading pass, and this looks fabulous! Here are my notes.

Some things we already talked about or you marked them in TODOs:

• Phrases like “t is contained in [numtype; vectype]” (e.g. select) are semantically off, because numtype and vectype are meta-variables that stand for many different types. Note sure there is a decent way to express it in set notation, so some prose “t is either a number type or a vector type” probably works better.

• Can we decompose more complex expressions (e.g. “unpack(zt)*” in struct.new) into auxiliary definitions? Perhaps approximating something akin to A-normal form wrt non-trivial constructs.

• Improve variable names (e.g. “valtype_u0” in select).

In addition, I have the following suggestions and questions:

• Can we unindent all bullet lists by one level, i.e., make the outermost (singular) level a non-bullet?

• Sentences should not start with a formula, since those may be lowercase letters (e.g. ref.test). Can we fix this by always inserting the type description of the expression, as in “The reference type rt matches rt'.”?

• “Matches” conditions are sometimes rendered with and sometimes without the type description, sometimes even in the same rule, which looks a bit odd (e.g. br_on_cast).

• Sometimes the meaning of “is” for equality reads a bit odd or unclear (could e.g. be interpreted as a Let). Maybe “equals” would be clearer?

• In various places (e.g. struct.new) “C.something[x] is defined in the context”, which is a bit redundant, as the C already implies that this is the context. Can we turn that into simply “C.something[x] is defined” (or simply “exists”, since that reads less funny when talking about defined types).

  In addition, there are many cases where the whole condition appears to be redundant, because it is implied by a following condition like “C.something[x] is y”. I noticed that this leads to a lot of bloat in the prose of many rules.

• When “binding” new variables in a comparison (e.g. “init” in local.set or “lim” in table.*), would it be possible to call that out that they are existential by saying something along the lines of “for some limit lim”?

• Instead of “x? is eps”, can we render that as “x is absent” for options (e.g. struct.get)?

• Instead of “default_t is val” can we write “default_t exists” when val isn’t actually used (e.g. struct/array.new_default)?

• In the rules for block instructions, the context composition expression has changed in the prose and does not fit what’s explained in the Note.

• Can we split the prose for catch clauses into separate rules?

• In the rule for ref.func, why is there the condition that C.refs[0] needs to be defined?