Fix typos

Author: yamt

document/core/appendix/index-instructions.py

@@ -340,7 +340,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\ARRAYINITDATA~x~y', r'\hex{FB}~\hex{12}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_data', r'exec-array.init_data'),
     Instruction(r'\ARRAYINITELEM~x~y', r'\hex{FB}~\hex{13}', r'[(\REF~\NULL~x)~\I32~\I32~\I32] \to []', r'valid-array.init_elem', r'exec-array.init_elem'),
     Instruction(r'\REFTEST~(\REF~t)', r'\hex{FB}~\hex{14}', r"[(\REF~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
-    Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{15}', r"[(REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
+    Instruction(r'\REFTEST~(\REF~\NULL~t)', r'\hex{FB}~\hex{15}', r"[(\REF~\NULL~t')] \to [\I32]", r'valid-ref.test', r'exec-ref.test'),
     Instruction(r'\REFCAST~(\REF~t)', r'\hex{FB}~\hex{16}', r"[(\REF~t')] \to [(\REF~t)]", r'valid-ref.cast', r'exec-ref.cast'),
     Instruction(r'\REFCAST~(\REF~\NULL~t)', r'\hex{FB}~\hex{17}', r"[(\REF~\NULL~t')] \to [(\REF~\NULL~t)]", r'valid-ref.cast', r'exec-ref.cast'),
     Instruction(r'\BRONCAST~t_1~t_2', r'\hex{FB}~\hex{18}', r'[t_1] \to [t_1\reftypediff t_2]', r'valid-br_on_cast', r'exec-br_on_cast'),

document/core/valid/conventions.rst

@@ -306,7 +306,7 @@ In addition to field access written :math:`C.\K{field}` the following notation i
 Convention
 ..........
 
-Any form of :ref:`type <syntax-type>` can be *closed* to bring it into :ref:`closed <type-closed>` form relative to a :ref:`context <context>` it is :ref:`valid <valid-type>` in by :ref:`substituting <notation-subst>` each :ref:`type index <syntax-typeidx>` :math:`x` occurring in it with the corresponding :ref:`defined type <syntax-deftype>` :math:`C.\CTYPES[x]`, after first closing the the types in :math:`C.\CTYPES` themselves.
+Any form of :ref:`type <syntax-type>` can be *closed* to bring it into :ref:`closed <type-closed>` form relative to a :ref:`context <context>` it is :ref:`valid <valid-type>` in by :ref:`substituting <notation-subst>` each :ref:`type index <syntax-typeidx>` :math:`x` occurring in it with the corresponding :ref:`defined type <syntax-deftype>` :math:`C.\CTYPES[x]`, after first closing the types in :math:`C.\CTYPES` themselves.
 
 .. math::
    \begin{array}{@{}lcll@{}}

document/core/valid/matching.rst

@@ -456,7 +456,7 @@ A :ref:`defined type <syntax-deftype>` :math:`\deftype_1` matches a type :math:`
 .. note::
    Note that there is no explicit definition of type _equivalence_,
    since it coincides with syntactic equality,
-   as used in the premise of the fomer rule above.
+   as used in the premise of the former rule above.
 
 
 .. index:: limits

proposals/gc/Overview.md

@@ -437,8 +437,8 @@ For now, we assume that all array types have a ([flexible](#flexible-aggregates)
 Elements are accessed with generic load/store instructions that take a reference to an array:
 ```
 (func $f (param $v (ref $vector))
-  (array.get $vector (local.get $v) (i32.const 1)
-    (array.set $vector (local.get $v) (i32.const 2))
+  (array.set $vector (local.get $v) (i32.const 1)
+    (array.get $vector (local.get $v) (i32.const 2))
   )
 )
 ```
@@ -717,7 +717,7 @@ Another alternative would be a three-point mutability lattice with readonly as a
 
 The Wasm type system is intentionally simple.
 That implies that it cannot be expressive enough to track all type information that is available in a source program.
-To allow producers to work around the inevitable limitations of the type system, down casts have to provided as an "escape hatch".
+To allow producers to work around the inevitable limitations of the type system, down casts have to be provided as an "escape hatch".
 For example, that allows the use of type `anyref` to represent reference values whose type is not locally known.
 When such a value is used in a context where the producer knows its real type, it can use a down cast to recover it.
 
@@ -776,7 +776,7 @@ There are a number of reasons to make RTTs explicit:
 
 * It allows more choice in producers' use of RTT information, including making it optional (post-MVP), in accordance with the pay-as-you-go principle: for example, structs that are not involved in any casts do not need to pay the overhead of carrying runtime type information (depending on specifics of the GC implementation strategy). Some languages may never need to introduce any RTTs at all.
 
-* Most importantly, making RTTs explicit separates the concerns of casting from Wasm-level polymorphism, i.e., [type parameters](Post-MVP.md#type-parameters). Type parameters can thus be treated as purely a validation artifact with no bearing on runtime. This property, known as parametricity, drastically simplifies the implementation of such type parameterisation and avoids the substantial hidden costs of reified generics that would otherwise hvae to be paid for every single use of type parameters (short of non-trivial cross-procedural dataflow analysis in the engine).
+* Most importantly, making RTTs explicit separates the concerns of casting from Wasm-level polymorphism, i.e., [type parameters](Post-MVP.md#type-parameters). Type parameters can thus be treated as purely a validation artifact with no bearing on runtime. This property, known as parametricity, drastically simplifies the implementation of such type parameterisation and avoids the substantial hidden costs of reified generics that would otherwise have to be paid for every single use of type parameters (short of non-trivial cross-procedural dataflow analysis in the engine).
 
 
 ## Future Extensions