[spec] Remove obsolete notes and fix inaccurate side conditions (#1311)

Author: rossberg

document/core/binary/instructions.rst

@@ -71,9 +71,6 @@ Control Instructions
    Unlike any :ref:`other occurrence <binary-typeidx>`, the :ref:`type index <syntax-typeidx>` in a :ref:`block type <syntax-blocktype>` is encoded as a positive :ref:`signed integer <syntax-sint>`, so that its |SignedLEB128| bit pattern cannot collide with the encoding of :ref:`value types <binary-valtype>` or the special code :math:`\hex{40}`, which correspond to the LEB128 encoding of negative integers.
    To avoid any loss in the range of allowed indices, it is treated as a 33 bit signed integer. 
 
-   In future versions of WebAssembly, the zero byte occurring in the encoding
-   of the |CALLINDIRECT| instruction may be used to index additional tables.
-
 
 .. index:: reference instruction
    pair: binary format; instruction
@@ -95,9 +92,6 @@ Reference Instructions
      \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\
    \end{array}
 
-.. note::
-   These opcode assignments are preliminary.
-
 
 .. index:: parametric instruction, value type, polymorphism
    pair: binary format; instruction

document/core/text/instructions.rst

@@ -71,7 +71,7 @@ However, the special case of a type use that is syntactically empty or consists
    &
    \begin{array}[t]{@{}lcll@{}}
      (t{:}\Tresult)^? &\Rightarrow& t^? \\
-     x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\}) \\
+     x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
    \end{array} \\
    \production{block instruction} & \Tblockinstr_I &::=&
      \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^?
@@ -87,7 +87,7 @@ However, the special case of a type use that is syntactically empty or consists
    \end{array}
 
 .. note::
-   The side condition stating that the :ref:`identifier context <text-context>` :math:`I'` must be empty in the rule for |Ttypeuse| block types enforces that no identifier can be bound in any |Tparam| declaration for a block type.
+   The side condition stating that the :ref:`identifier context <text-context>` :math:`I'` must only contain unnamed entries in the rule for |Ttypeuse| block types enforces that no identifier can be bound in any |Tparam| declaration for a block type.
 
 
 .. _text-nop:
@@ -113,11 +113,11 @@ All other control instruction are represented verbatim.
      \text{return} &\Rightarrow& \RETURN \\ &&|&
      \text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|&
      \text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y
-       & (\iff I' = \{\}) \\
+       & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
    \end{array}
 
 .. note::
-   The side condition stating that the :ref:`identifier context <text-context>` :math:`I'` must be empty in the rule for |CALLINDIRECT| enforces that no identifier can be bound in any |Tparam| declaration appearing in the type annotation.
+   The side condition stating that the :ref:`identifier context <text-context>` :math:`I'` must only contain unnamed entries in the rule for |CALLINDIRECT| enforces that no identifier can be bound in any |Tparam| declaration appearing in the type annotation.
 
 
 Abbreviations