Fix many miscellaneous spec problems (#77)

* Fix hardcoded use of i32 in call_indirect and return_call_indirect

* Add missing prose for table type in table.size

* Update table and memory type matching

This is used for matching external types.

* Update store integrity section for index types

* Fix rogue backslashes

document/core/appendix/properties.rst

@@ -513,10 +513,10 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 .. index:: table type, table instance, limits, function address
 .. _valid-tableinst:
 
-:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~(\limits~t), \TIELEM~\reff^\ast \}`
-...............................................................................................
+:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~\idxtype~\limits~t, \TIELEM~\reff^\ast \}`
+......................................................................................................
 
-* The :ref:`table type <syntax-tabletype>` :math:`\limits~t` must be :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
+* The :ref:`table type <syntax-tabletype>` :math:`\idxtype~\limits~t` must be :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
 
 * The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`.
 
@@ -526,49 +526,49 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
  * The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.
 
-* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\limits~t`.
+* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\idxtype~\limits~t`.
 
 .. math::
  \frac{
- \vdashtabletype \limits~t \ok
+ \vdashtabletype \idxtype~\limits~t \ok
  \qquad
  n = \limits.\LMIN
  \qquad
  (S \vdash \reff : t')^n
  \qquad
  (\vdashreftypematch t' \matchesvaltype t)^n
  }{
- S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t
+ S \vdashtableinst \{ \TITYPE~\idxtype~\limits~t, \TIELEM~\reff^n \} : \idxtype~\limits~t
  }
 
 
 .. index:: memory type, memory instance, limits, byte
 .. _valid-meminst:
 
-:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}`
-......................................................................................
+:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\idxtype~\limits, \MIDATA~b^\ast \}`
+...............................................................................................
 
-* The :ref:`memory type <syntax-memtype>` :math:`\limits` must be :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
+* The :ref:`memory type <syntax-memtype>` :math:`\idxtype~\limits` must be :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
 
 * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.
 
-* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\limits`.
+* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\idxtype~\limits`.
 
 .. math::
  \frac{
- \vdashmemtype \limits \ok
+ \vdashmemtype \idxtype~\limits \ok
  \qquad
  n = \limits.\LMIN \cdot 64\,\F{Ki}
  }{
- S \vdashmeminst \{ \MITYPE~\limits, \MIDATA~b^n \} : \limits
+ S \vdashmeminst \{ \MITYPE~\idxtype~\limits, \MIDATA~b^n \} : \idxtype~\limits
  }
 
 
 .. index:: global type, global instance, value, mutability
 .. _valid-globalinst:
 
-:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~(\mut~t), \GIVALUE~\val \}`
-.........................................................................................
+:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~\mut~t, \GIVALUE~\val \}`
+.......................................................................................
 
 * The :ref:`global type <syntax-globaltype>` :math:`\mut~t` must be :ref:`valid <valid-globaltype>` under the empty :ref:`context <context>`.
 
@@ -586,7 +586,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
  \qquad
  \vdashvaltypematch t' \matchesvaltype t
  }{
- S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t
+ S \vdashglobalinst \{ \GITYPE~\mut~t, \GIVALUE~\val \} : \mut~t
  }
 
 

document/core/valid/instructions.rst

@@ -1366,6 +1366,8 @@ Table Instructions
 
 * The table :math:`C.\CTABLES[x]` must be defined in the context.
 
+* Let :math:`\X{it}~\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
 * Then the instruction is valid with type :math:`[] \to [\X{it}]`.
 
 .. math::
@@ -2413,7 +2415,7 @@ Control Instructions
 
 * The :ref:`expansion <aux-expand-deftype>` of :math:`C.\CTYPES[y]` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`.
 
-* Then the instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_2^\ast]`.
+* Then the instruction is valid with type :math:`[t_1^\ast~\X{it}] \to [t_2^\ast]`.
 
 .. math::
  \frac{
@@ -2504,7 +2506,7 @@ Control Instructions
 
 * The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` must :ref:`match <match-resulttype>` :math:`C.\CRETURN`.
 
-* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.
+* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\X{it}] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.
 
 .. math::
  \frac{
@@ -2518,7 +2520,7 @@ Control Instructions
  \qquad
  C \vdashinstrtype [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast] \ok
  }{
- C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]
+ C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\X{it}] \to [t_4^\ast]
  }
 
 .. note::

document/core/valid/matching.rst

@@ -502,7 +502,9 @@ Limits
 Table Types
 ~~~~~~~~~~~
 
-A :ref:`table type <syntax-tabletype>` :math:`(\limits_1~\reftype_1)` matches :math:`(\limits_2~\reftype_2)` if and only if:
+A :ref:`table type <syntax-tabletype>` :math:`(\idxtype_1~\limits_1~\reftype_1)` matches :math:`(\idxtype_2~\limits_2~\reftype_2)` if and only if:
+
+* Index types :math:`\idxtype_1` and :math:`\idxtype_2` are the same.
 
 * Limits :math:`\limits_1` :ref:`match <match-limits>` :math:`\limits_2`.
 
@@ -511,13 +513,15 @@ A :ref:`table type <syntax-tabletype>` :math:`(\limits_1~\reftype_1)` matches :m
 .. math::
  ~\\[-1ex]
  \frac{
+ C \vdashnumtypematch \idxtype_1 \matchesnumtype \idxtype_2
+ \qquad
  C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2
  \qquad
  C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2
  \qquad
  C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1
  }{
- C \vdashtabletypematch \limits_1~\reftype_1 \matchestabletype \limits_2~\reftype_2
+ C \vdashtabletypematch \idxtype_1~\limits_1~\reftype_1 \matchestabletype \idxtype_2~\limits_2~\reftype_2
  }
 
 
@@ -527,14 +531,18 @@ A :ref:`table type <syntax-tabletype>` :math:`(\limits_1~\reftype_1)` matches :m
 Memory Types
 ~~~~~~~~~~~~
 
-A :ref:`memory type <syntax-memtype>` :math:`\limits_1` matches :math:`\limits_2` if and only if:
+A :ref:`memory type <syntax-memtype>` :math:`(\idxtype_1~\limits_1)` matches :math:`(\idxtype_2~\limits_2)` if and only if:
+
+* Index types :math:`\idxtype_1` and :math:`\idxtype_2` are the same.
 
 * Limits :math:`\limits_1` :ref:`match <match-limits>` :math:`\limits_2`.
 
 
 .. math::
  ~\\[-1ex]
  \frac{
+ C \vdashnumtypematch \idxtype_1 \matchesnumtype \idxtype_2
+ \qquad
  C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2
  }{
  C \vdashmemtypematch \limits_1 \matchesmemtype \limits_2