diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 0000000000..3171e9030e
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1,7 @@
+*.rst linguist-documentation=false
+document/* linguist-documentation=false
+document/*.rst linguist-documentation=false
+document/*/*.rst linguist-documentation=false
+test/harness/wast.js linguist-vendored
+test/harness/testharness* linguist-vendored
+
diff --git a/document/Makefile b/document/Makefile
index 8a3c4d3c04..5df0df135e 100644
--- a/document/Makefile
+++ b/document/Makefile
@@ -94,6 +94,7 @@ html:
sed s:BASEDIR:..:g <$$file >$$file.out; \
sed 's;
MathJax.Hub.Config({TeX: {MAXBUFFER: 10*1024}})$$file; \
+ rm -f $$file.out; \
done
@echo
@echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html."
diff --git a/document/index.rst b/document/index.rst
index 83ba5cf642..6060619a7d 100644
--- a/document/index.rst
+++ b/document/index.rst
@@ -6,7 +6,7 @@ WebAssembly Specification
Release |release| (work in progress, last updated |today|)
.. toctree::
- :maxdepth: 2
+ :maxdepth: 3
introduction/index
syntax/index
@@ -20,6 +20,14 @@ WebAssembly Specification
appendix-textual/index
appendix-names/index
+.. only:: latex
+
+ .. toctree::
+
+ syntax/instrindex
+
.. only:: html
+ * :ref:`instrindex`
+
* :ref:`genindex`
diff --git a/document/instructions/group-control-blocks.rst b/document/instructions/group-control-blocks.rst
deleted file mode 100644
index 61fba99af6..0000000000
--- a/document/instructions/group-control-blocks.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-Block Instructions
-------------------
-
-.. toctree::
- :maxdepth: 2
-
- block
- loop
- if
diff --git a/document/instructions/group-control-branches.rst b/document/instructions/group-control-branches.rst
deleted file mode 100644
index 4f8c17f593..0000000000
--- a/document/instructions/group-control-branches.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-Branch Instructions
--------------------
-
-.. toctree::
- :maxdepth: 2
-
- br
- br_if
- br_table
diff --git a/document/instructions/group-control-calls.rst b/document/instructions/group-control-calls.rst
deleted file mode 100644
index bb5d74616a..0000000000
--- a/document/instructions/group-control-calls.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-Call Instructions
------------------
-
-.. toctree::
- :maxdepth: 2
-
- call
- call_indirect
- return
diff --git a/document/instructions/group-control-others.rst b/document/instructions/group-control-others.rst
deleted file mode 100644
index a1cf89b40c..0000000000
--- a/document/instructions/group-control-others.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Miscellaneous Control Instructions
-----------------------------------
-
-.. toctree::
- :maxdepth: 2
-
- nop
- unreachable
diff --git a/document/instructions/group-control.rst b/document/instructions/group-control.rst
deleted file mode 100644
index 11d136c57f..0000000000
--- a/document/instructions/group-control.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-Control Instructions
---------------------
-
-.. toctree::
- :maxdepth: 2
-
- group-control-blocks
- group-control-branches
- group-control-calls
- group-control-others
diff --git a/document/instructions/group-memory-load.rst b/document/instructions/group-memory-load.rst
deleted file mode 100644
index 949d897581..0000000000
--- a/document/instructions/group-memory-load.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Load Instructions
------------------
-
-.. toctree::
- :maxdepth: 2
-
- t.load
- ixx.loadn_sx
diff --git a/document/instructions/group-memory-size.rst b/document/instructions/group-memory-size.rst
deleted file mode 100644
index 7f78f3e22d..0000000000
--- a/document/instructions/group-memory-size.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Store Instructions
-------------------
-
-.. toctree::
- :maxdepth: 2
-
- current_memory
- grow_memory
diff --git a/document/instructions/group-memory-store.rst b/document/instructions/group-memory-store.rst
deleted file mode 100644
index aeb870f850..0000000000
--- a/document/instructions/group-memory-store.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Memory Instructions
--------------------
-
-.. toctree::
- :maxdepth: 2
-
- t.store
- ixx.storen
diff --git a/document/instructions/group-memory.rst b/document/instructions/group-memory.rst
deleted file mode 100644
index e0ddb6a4e0..0000000000
--- a/document/instructions/group-memory.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-Memory Instructions
--------------------
-
-.. toctree::
- :maxdepth: 2
-
- group-memory-load
- group-memory-store
- group-memory-size
diff --git a/document/instructions/group-numeric-binary-float.rst b/document/instructions/group-numeric-binary-float.rst
deleted file mode 100644
index 90de6332fa..0000000000
--- a/document/instructions/group-numeric-binary-float.rst
+++ /dev/null
@@ -1,13 +0,0 @@
-Binary Floating Point Instructions
-----------------------------------
-
-.. toctree::
- :maxdepth: 2
-
- fxx.add
- fxx.sub
- fxx.mul
- fxx.div
- fxx.min
- fxx.max
- fxx.copysign
diff --git a/document/instructions/group-numeric-binary-int.rst b/document/instructions/group-numeric-binary-int.rst
deleted file mode 100644
index e8f207e508..0000000000
--- a/document/instructions/group-numeric-binary-int.rst
+++ /dev/null
@@ -1,18 +0,0 @@
-Binary Integer Instructions
----------------------------
-
-.. toctree::
- :maxdepth: 2
-
- ixx.add
- ixx.sub
- ixx.mul
- ixx.div_sx
- ixx.rem_sx
- ixx.and
- ixx.or
- ixx.xor
- ixx.shl
- ixx.shr_sx
- ixx.rol
- ixx.ror
diff --git a/document/instructions/group-numeric-compare-float.rst b/document/instructions/group-numeric-compare-float.rst
deleted file mode 100644
index 0709457b47..0000000000
--- a/document/instructions/group-numeric-compare-float.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-Floating Point Comparison Instructions
---------------------------------------
-
-.. toctree::
- :maxdepth: 2
-
- fxx.eq
- fxx.ne
- fxx.lt
- fxx.gt
- fxx.le
- fxx.gt
diff --git a/document/instructions/group-numeric-compare-int.rst b/document/instructions/group-numeric-compare-int.rst
deleted file mode 100644
index abd304a02d..0000000000
--- a/document/instructions/group-numeric-compare-int.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-Integer Comparison Instructions
--------------------------------
-
-.. toctree::
- :maxdepth: 2
-
- ixx.eq
- ixx.ne
- ixx.lt_sx
- ixx.gt_sx
- ixx.le_sx
- ixx.gt_sx
diff --git a/document/instructions/group-numeric-const.rst b/document/instructions/group-numeric-const.rst
deleted file mode 100644
index 20788aa211..0000000000
--- a/document/instructions/group-numeric-const.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Numeric Instructions
---------------------
-
-.. toctree::
- :maxdepth: 2
-
- ixx.const
- fxx.const
diff --git a/document/instructions/group-numeric-convert.rst b/document/instructions/group-numeric-convert.rst
deleted file mode 100644
index 06613d4890..0000000000
--- a/document/instructions/group-numeric-convert.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-Conversion Instructions
------------------------
-
-.. toctree::
- :maxdepth: 2
-
- i32.wrap.i64
- i64.extend_sx.i32
- ixx.trunc_sx.fyy
- f32.demote.f64
- f64.promote.f32
- fxx.convert_sx.iyy
diff --git a/document/instructions/group-numeric-reinterpret.rst b/document/instructions/group-numeric-reinterpret.rst
deleted file mode 100644
index 384471ffaf..0000000000
--- a/document/instructions/group-numeric-reinterpret.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Reinterpretation Instructions
------------------------------
-
-.. toctree::
- :maxdepth: 2
-
- ixx.reinterpret.fxx
- fxx.reinterpret.ixx
diff --git a/document/instructions/group-numeric-test-int.rst b/document/instructions/group-numeric-test-int.rst
deleted file mode 100644
index e8ee032c35..0000000000
--- a/document/instructions/group-numeric-test-int.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-Integer Test Instructions
--------------------------
-
-.. toctree::
- :maxdepth: 2
-
- ixx.eqz
diff --git a/document/instructions/group-numeric-unary-float.rst b/document/instructions/group-numeric-unary-float.rst
deleted file mode 100644
index baf95333da..0000000000
--- a/document/instructions/group-numeric-unary-float.rst
+++ /dev/null
@@ -1,13 +0,0 @@
-Unary Floating Point Instructions
----------------------------------
-
-.. toctree::
- :maxdepth: 2
-
- fxx.neg
- fxx.abs
- fxx.ceil
- fxx.floor
- fxx.trunc
- fxx.nearest
- fxx.sqrt
diff --git a/document/instructions/group-numeric-unary-int.rst b/document/instructions/group-numeric-unary-int.rst
deleted file mode 100644
index ea6d206bcd..0000000000
--- a/document/instructions/group-numeric-unary-int.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-Unary Integer Instructions
---------------------------
-
-.. toctree::
- :maxdepth: 2
-
- ixx.clz
- ixx.ctz
- ixx.popcnt
diff --git a/document/instructions/group-numeric.rst b/document/instructions/group-numeric.rst
deleted file mode 100644
index 7d432d517a..0000000000
--- a/document/instructions/group-numeric.rst
+++ /dev/null
@@ -1,16 +0,0 @@
-Numeric Instructions
---------------------
-
-.. toctree::
- :maxdepth: 2
-
- group-numeric-const
- group-numeric-test-int
- group-numeric-compare-int
- group-numeric-compare-float
- group-numeric-unary-int
- group-numeric-unary-float
- group-numeric-binary-int
- group-numeric-binary-float
- group-numeric-convert
- group-numeric-reinterpret
diff --git a/document/instructions/group-parametric.rst b/document/instructions/group-parametric.rst
deleted file mode 100644
index d9e65e40c9..0000000000
--- a/document/instructions/group-parametric.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Parametric Instructions
------------------------
-
-.. toctree::
- :maxdepth: 2
-
- drop
- select
diff --git a/document/instructions/group-variables.rst b/document/instructions/group-variables.rst
deleted file mode 100644
index 5b56328754..0000000000
--- a/document/instructions/group-variables.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-Variable Instructions
----------------------
-
-.. toctree::
- :maxdepth: 2
-
- get_local
- set_local
- tee_local
- get_global
- set_global
diff --git a/document/instructions/index.rst b/document/instructions/index.rst
deleted file mode 100644
index ae92bfac73..0000000000
--- a/document/instructions/index.rst
+++ /dev/null
@@ -1,15 +0,0 @@
-Instructions
-============
-
-.. index:: !instructions
-
-.. toctree::
- :maxdepth: 3
-
- overview
- group-control
- group-variables
- group-parametric
- group-numeric
- group-memory
- sequences
diff --git a/document/instructions/overview.rst b/document/instructions/overview.rst
deleted file mode 100644
index 9bfd5db257..0000000000
--- a/document/instructions/overview.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Overview
---------
-
-.. todo::
-
- Describe
diff --git a/document/instructions/sequences.rst b/document/instructions/sequences.rst
deleted file mode 100644
index 0a1609e4e4..0000000000
--- a/document/instructions/sequences.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-Instruction Sequences
----------------------
-
-.. todo::
-
- Describe
diff --git a/document/math.def b/document/math.def
index 27a1654869..d8e23dba9a 100644
--- a/document/math.def
+++ b/document/math.def
@@ -1,3 +1,5 @@
+.. MATH
+
.. To comment out stuff
.. |void#1| mathdef:: {}
@@ -27,7 +29,7 @@
.. Values, non-terminals
-.. |by| mathdef:: \xref{syntax/values}{syntax-byte}{byte}
+.. |by| mathdef:: \xref{syntax/values}{syntax-byte}{\X{byte}}
.. |uX#1| mathdef:: {\X{uint}_{#1}}
.. |sX#1| mathdef:: {\X{sint}_{#1}}
@@ -82,7 +84,7 @@
.. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
.. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
.. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
-.. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mutability}}
+.. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
.. Indices
@@ -144,8 +146,17 @@
.. |export| mathdef:: \xref{syntax/modules}{syntax-export}{\X{export}}
.. |importdesc| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\X{importdesc}}
.. |exportdesc| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\X{exportdesc}}
-.. |elemseg| mathdef:: \xref{syntax/modules}{syntax-elemseg}{\X{elemseg}}
-.. |dataseg| mathdef:: \xref{syntax/modules}{syntax-dataseg}{\X{dataseg}}
+.. |elem| mathdef:: \xref{syntax/modules}{syntax-elemseg}{\X{elem}}
+.. |data| mathdef:: \xref{syntax/modules}{syntax-dataseg}{\X{data}}
+.. |start| mathdef:: \xref{syntax/modules}{syntax-dataseg}{\X{start}}
+
+
+.. Modules, meta functions
+
+.. |funcs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
+.. |tables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}
+.. |mems| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}}
+.. |globals| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}}
.. Instructions, terminals
@@ -153,36 +164,86 @@
.. |OFFSET| mathdef:: \K{offset}
.. |ALIGN| mathdef:: \K{align}
-.. |UNREACHABLE| mathdef:: \K{unreachable}
-.. |NOP| mathdef:: \K{nop}
-.. |BLOCK| mathdef:: \K{block}
-.. |LOOP| mathdef:: \K{loop}
-.. |IF| mathdef:: \K{if}
-.. |ELSE| mathdef:: \K{else}
-.. |END| mathdef:: \K{end}
-.. |BR| mathdef:: \K{br}
-.. |BRIF| mathdef:: \K{br\_if}
-.. |BRTABLE| mathdef:: \K{br\_table}
-.. |RETURN| mathdef:: \K{return}
-.. |CALL| mathdef:: \K{call}
-.. |CALLINDIRECT| mathdef:: \K{call\_indirect}
-.. |DROP| mathdef:: \K{drop}
-.. |SELECT| mathdef:: \K{select}
-.. |GETLOCAL| mathdef:: \K{get\_local}
-.. |SETLOCAL| mathdef:: \K{set\_local}
-.. |TEELOCAL| mathdef:: \K{tee\_local}
-.. |GETGLOBAL| mathdef:: \K{get\_global}
-.. |SETGLOBAL| mathdef:: \K{set\_global}
-.. |LOAD| mathdef:: \K{load}
-.. |STORE| mathdef:: \K{store}
-.. |CURRENTMEMORY| mathdef:: \K{current\_memory}
-.. |GROWMEMORY| mathdef:: \K{grow\_memory}
-.. |CONST| mathdef:: \K{const}
+.. |UNREACHABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{unreachable}}
+.. |NOP| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{nop}}
+.. |BLOCK| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{block}}
+.. |LOOP| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{loop}}
+.. |IF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{if}}
+.. |ELSE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{else}}
+.. |END| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{end}}
+.. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}}
+.. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}}
+.. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}}
+.. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
+.. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
+.. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}
+
+.. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}
+.. |SELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{select}}
+
+.. |GETLOCAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{get\_local}}
+.. |SETLOCAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{set\_local}}
+.. |TEELOCAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{tee\_local}}
+.. |GETGLOBAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{get\_global}}
+.. |SETGLOBAL| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{set\_global}}
+
+.. |LOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}}
+.. |STORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}}
+.. |CURRENTMEMORY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{current\_memory}}
+.. |GROWMEMORY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{grow\_memory}}
+
+.. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}}
+.. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}}
+.. |EQ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eq}}
+.. |NE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ne}}
+.. |LT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{lt}}
+.. |GT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{gt}}
+.. |LE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{le}}
+.. |GE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ge}}
+.. |CLZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{clz}}
+.. |CTZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ctz}}
+.. |POPCNT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{popcnt}}
+.. |ABS| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{abs}}
+.. |NEG| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{neg}}
+.. |CEIL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ceil}}
+.. |FLOOR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{floor}}
+.. |TRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{trunc}}
+.. |NEAREST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{nearest}}
+.. |SQRT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sqrt}}
+.. |ADD| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{add}}
+.. |SUB| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sub}}
+.. |MUL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{mul}}
+.. |DIV| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{div}}
+.. |REM| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rem}}
+.. |FMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{min}}
+.. |FMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{max}}
+.. |AND| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{and}}
+.. |OR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{or}}
+.. |XOR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{xor}}
+.. |SHL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{shl}}
+.. |SHR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{shr}}
+.. |ROTL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rotl}}
+.. |ROTR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rotr}}
+.. |COPYSIGN| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{copysign}}
+
+.. |CONVERT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{convert}}
+.. |EXTEND| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{extend}}
+.. |WRAP| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{wrap}}
+.. |PROMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{promote}}
+.. |DEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{demote}}
+.. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}}
.. Instructions, non-terminals
+.. |unop| mathdef:: \X{unop}
+.. |binop| mathdef:: \X{binop}
+.. |testop| mathdef:: \X{testop}
+.. |relop| mathdef:: \X{relop}
+.. |cvtop| mathdef:: \X{cvtop}
+
.. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}}
.. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}}
+
.. |instr| mathdef:: \xref{syntax/instructions}{syntax-instr}{\X{instr}}
-.. |expr| mathdef:: \xref{syntax/modules}{syntax-expr}{\X{expr}}
+.. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}}
diff --git a/document/mathdef.py b/document/mathdef.py
index 655f6c895c..9dace41837 100644
--- a/document/mathdef.py
+++ b/document/mathdef.py
@@ -65,8 +65,6 @@ def lookup_mathdef(defs, name):
auxcounter = auxcounter + 1
name = "\\mathdef%d" % auxcounter
s = "\\def%s#%d{%s}%s" % (name, arity, s, name)
- # DEBUG
- print("EXPAND %s %d = %s" % (name, arity, s))
return s
return name
diff --git a/document/syntax/conventions.rst b/document/syntax/conventions.rst
index d540339f4d..63413f5459 100644
--- a/document/syntax/conventions.rst
+++ b/document/syntax/conventions.rst
@@ -34,6 +34,8 @@ The following conventions are adopted in defining grammar rules for abstract syn
(This is a shorthand for :math:`A^n` where :math:`n \leq 1`.)
+.. _syntax-record:
+
Auxiliary Notation
~~~~~~~~~~~~~~~~~~
diff --git a/document/syntax/index.rst b/document/syntax/index.rst
index f8fb18b8a6..0eb625b358 100644
--- a/document/syntax/index.rst
+++ b/document/syntax/index.rst
@@ -7,5 +7,5 @@ Structure
conventions
values
types
- modules
instructions
+ modules
diff --git a/document/syntax/instrindex.rst b/document/syntax/instrindex.rst
new file mode 100644
index 0000000000..1f0076dbd9
--- /dev/null
+++ b/document/syntax/instrindex.rst
@@ -0,0 +1,201 @@
+.. _instrindex:
+
+Index of Instructions
+---------------------
+
+=================================== ================ ========================================== ======================================== ================
+Instruction Opcode Type Validation Execution
+=================================== ================ ========================================== ======================================== ================
+:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation `
+:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation `
+:math:`\BLOCK~[t^?]` :math:`\hex{02}` :math:`[] \to [t^\ast]` :ref:`validation `
+:math:`\LOOP~[t^?]` :math:`\hex{03}` :math:`[] \to [t^\ast]` :ref:`validation `
+:math:`\IF~[t^?]` :math:`\hex{04}` :math:`[] \to [t^\ast]` :ref:`validation `
+:math:`\ELSE` :math:`\hex{05}`
+(reserved) :math:`\hex{06}`
+(reserved) :math:`\hex{07}`
+(reserved) :math:`\hex{08}`
+(reserved) :math:`\hex{09}`
+(reserved) :math:`\hex{0A}`
+:math:`\END` :math:`\hex{0B}`
+:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation `
+:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^?~\I32] \to [t^?]` :ref:`validation `
+:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]` :ref:`validation `
+:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation `
+:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation `
+:math:`\CALLINDIRECT~x` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation `
+(reserved) :math:`\hex{12}`
+(reserved) :math:`\hex{13}`
+(reserved) :math:`\hex{14}`
+(reserved) :math:`\hex{15}`
+(reserved) :math:`\hex{16}`
+(reserved) :math:`\hex{17}`
+(reserved) :math:`\hex{18}`
+(reserved) :math:`\hex{19}`
+:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation `
+:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation `
+(reserved) :math:`\hex{1C}`
+(reserved) :math:`\hex{1D}`
+(reserved) :math:`\hex{1E}`
+(reserved) :math:`\hex{1F}`
+:math:`\GETLOCAL~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation `
+:math:`\SETLOCAL~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation `
+:math:`\TEELOCAL~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation `
+:math:`\GETGLOBAL~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation `
+:math:`\SETGLOBAL~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation `
+(reserved) :math:`\hex{25}`
+(reserved) :math:`\hex{26}`
+(reserved) :math:`\hex{27}`
+:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation `
+:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation `
+:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation `
+:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation `
+:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation `
+:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation `
+:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation `
+:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation `
+:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation `
+:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation `
+:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation `
+:math:`\CURRENTMEMORY` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation `
+:math:`\GROWMEMORY` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation `
+:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation `
+:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation `
+:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation `
+:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation `
+:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation `
+:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation `
+:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation `
+:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation `
+:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation `
+:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation `
+:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation `
+:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation `
+:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation `
+:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation `
+:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation `
+:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation `
+:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation `
+:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation `
+:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation `
+:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation `
+:math:`\I32.\WRAP\K{/}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation `
+:math:`\I32.\TRUNC\K{\_s/}\F32` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation `
+:math:`\I32.\TRUNC\K{\_u/}\F32` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation `
+:math:`\I32.\TRUNC\K{\_s/}\F64` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation `
+:math:`\I32.\TRUNC\K{\_u/}\F64` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation `
+:math:`\I64.\EXTEND\K{\_s/}\I32` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\EXTEND\K{\_u/}\I32` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation `
+:math:`\I64.\TRUNC\K{\_s/}\F32` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation `
+:math:`\I64.\TRUNC\K{\_u/}\F32` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation `
+:math:`\I64.\TRUNC\K{\_s/}\F64` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation `
+:math:`\I64.\TRUNC\K{\_u/}\F64` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation `
+:math:`\F32.\CONVERT\K{\_s/}\I32` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation `
+:math:`\F32.\CONVERT\K{\_u/}\I32` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation `
+:math:`\F32.\CONVERT\K{\_s/}\I64` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation `
+:math:`\F32.\CONVERT\K{\_u/}\I64` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation `
+:math:`\F32.\DEMOTE\K{/}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation `
+:math:`\F64.\CONVERT\K{\_s/}\I32` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation `
+:math:`\F64.\CONVERT\K{\_u/}\I32` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation `
+:math:`\F64.\CONVERT\K{\_s/}\I64` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation `
+:math:`\F64.\CONVERT\K{\_u/}\I64` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation `
+:math:`\F64.\PROMOTE\K{/}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation `
+:math:`\I32.\REINTERPRET\K{/}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation `
+:math:`\I64.\REINTERPRET\K{/}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation `
+:math:`\F32.\REINTERPRET\K{/}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation `
+:math:`\F64.\REINTERPRET\K{/}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation `
+=================================== ================ ========================================== ======================================== ================
diff --git a/document/syntax/instructions.rst b/document/syntax/instructions.rst
index ef255356b9..4e2bc9d9fa 100644
--- a/document/syntax/instructions.rst
+++ b/document/syntax/instructions.rst
@@ -25,7 +25,7 @@ The following sections group instructions into a number of different categories.
.. _syntax-sx:
.. _syntax-instr-numeric:
-.. index:: ! memory instructions
+.. index:: ! numeric instruction
pair: abstract syntax; instruction
Numeric Instructions
@@ -117,7 +117,7 @@ For the other integer instructions, the use of 2's complement for the signed int
.. _syntax-instr-parametric:
-.. index:: ! parametric instructions
+.. index:: ! parametric instruction
pair: abstract syntax; instruction
Parametric Instructions
@@ -139,7 +139,7 @@ The |SELECT| operator selects one of its first two operands based on whether its
.. _syntax-instr-variable:
-.. index:: ! variable instructions, local, global, local index, global index
+.. index:: ! variable instruction, local, global, local index, global index
pair: abstract syntax; instruction
Variable Instructions
@@ -164,7 +164,7 @@ The |TEELOCAL| instruction is like |SETLOCAL| but also returns its argument.
.. _syntax-instr-memory:
.. _syntax-memarg:
-.. index:: ! memory instructions, memory index
+.. index:: ! memory instruction, memory index
pair: abstract syntax; instruction
Memory Instructions
@@ -192,7 +192,7 @@ Instructions in this group are concerned with :ref:`linear memory `.
\GROWMEMORY \\
\end{array}
-Memory is accessed with :math:`\K{load}` and :math:`\K{store}` instructions for the different :ref:`value types `.
+Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`value types `.
They all take a *memory immediate* |memarg| that contains an address *offset* and an *alignment* hint.
Integer loads and stores can optionally specify a *storage size* that is smaller than the width of the respective value type.
In the case of loads, a sign extension mode |sx| is then required to select appropriate behavior.
@@ -218,7 +218,7 @@ The precise semantics of memory instructions is :ref:`described ` and :r
\TABLES~\vec(\table), \\&&&&
\MEMS~\vec(\mem), \\&&&&
\GLOBALS~\vec(\global), \\&&&&
- \ELEM~\vec(\elemseg), \\&&&&
- \DATA~\vec(\dataseg), \\&&&&
- \START~\funcidx^?, \\&&&&
+ \ELEM~\vec(\elem), \\&&&&
+ \DATA~\vec(\data), \\&&&&
+ \START~\start^?, \\&&&&
\IMPORTS~\vec(\import), \\&&&&
\EXPORTS~\vec(\export) \quad\} \\
\end{array}
@@ -29,6 +29,7 @@ and provide initialization logic in the form of :ref:`data ` and :r
Each of the vectors -- and thus the entire module -- may be empty.
+.. _syntax-index:
.. _syntax-typeidx:
.. _syntax-funcidx:
.. _syntax-tableidx:
@@ -82,26 +83,7 @@ Conventions
* The meta variable :math:`l` ranges over label indices.
-* The meta variable :math:`x` ranges over indices in any of the other index spaces.
-
-
-.. _syntax-expr:
-.. index:: ! expression
- pair: abstract syntax; expression
- single: expression; constant
-
-Expressions
-~~~~~~~~~~~
-
-:ref:`Function ` bodies, initialization values for :ref:`globals ` and offsets of :ref:`element ` or :ref:`data ` segments are given as expressions, which are sequences of :ref:`instructions ` terminated by an |END| marker.
-
-.. math::
- \begin{array}{llll}
- \production{expressions} & \expr &::=&
- \instr^\ast~\END \\
- \end{array}
-
-In some places, validation :ref:`restricts ` expressions to be *constant*, which limits the set of allowable insructions.
+* The meta variables :math:`x, y` ranges over indices in any of the other index spaces.
.. _syntax-type:
@@ -123,7 +105,7 @@ They are referenced by :ref:`type indices `.
.. _syntax-func:
.. _syntax-local:
-.. index:: ! function, ! local, function index, type index, value type, expression, import
+.. index:: ! function, ! local, function index, local index, type index, value type, expression, import
pair: abstract syntax; function
Functions
@@ -228,7 +210,7 @@ The |GLOBALS| component of a module defines a vector of *global variables* (or *
Each global stores a single value of the given :ref:`global type `.
Its |TYPE| also specifies whether a global is immutable or mutable.
-Moreover, each global is initialized with an |INIT| value given by a :ref:`constant ` initializer :ref:`expression `.
+Moreover, each global is initialized with an |INIT| value given by a :ref:`constant ` initializer :ref:`expression `.
Globals are referenced through :ref:`global indices `,
starting with the smallest index not referencing a global :ref:`import `.
@@ -248,11 +230,11 @@ The |ELEM| component of a module defines a vector of *element segments* that ini
.. math::
\begin{array}{llll}
- \production{element segments} & \elemseg &::=&
+ \production{element segments} & \elem &::=&
\{ \TABLE~\tableidx, \OFFSET~\expr, \INIT~\vec(\funcidx) \} \\
\end{array}
-The |OFFSET| is given by a :ref:`constant ` :ref:`expression `.
+The |OFFSET| is given by a :ref:`constant ` :ref:`expression `.
.. note::
In the current version of WebAssembly, at most one table is allowed in a module.
@@ -273,11 +255,11 @@ The |DATA| component of a module defines a vector of *data segments* that initia
.. math::
\begin{array}{llll}
- \production{data segments} & \dataseg &::=&
+ \production{data segments} & \data &::=&
\{ \MEM~\memidx, \OFFSET~\expr, \INIT~\vec(\by) \} \\
\end{array}
-The |OFFSET| is given by a :ref:`constant ` :ref:`expression `.
+The |OFFSET| is given by a :ref:`constant ` :ref:`expression `.
.. note::
In the current version of WebAssembly, at most one memory is allowed in a module.
@@ -291,7 +273,13 @@ The |OFFSET| is given by a :ref:`constant ` :ref:`expression ` of an optional *start function* that is automatically invoked when the module is :ref:`instantiated `, after tables and memories have been initialized.
+The |START| component of a module optionally declares the :ref:`function index ` of a *start function* that is automatically invoked when the module is :ref:`instantiated `, after tables and memories have been initialized.
+
+.. math::
+ \begin{array}{llll}
+ \production{start function} & \start &::=&
+ \{ \FUNC~\funcidx \} \\
+ \end{array}
.. _syntax-export:
diff --git a/document/syntax/types.rst b/document/syntax/types.rst
index 75ee225fcd..a35fb4c99d 100644
--- a/document/syntax/types.rst
+++ b/document/syntax/types.rst
@@ -33,6 +33,9 @@ Conventions
* The meta variable :math:`t` ranges over value types where clear from context.
+* The notation :math:`|t|` denotes the *width* of a value type in bytes.
+ (That is, :math:`|\I32| = |\F32| = 4` and :math:`|\I64| = |\F64| = 8`.)
+
.. _syntax-resulttype:
.. index:: ! result type, value type
@@ -48,7 +51,7 @@ which is a sequence of values.
.. math::
\begin{array}{llll}
\production{result types} & \resulttype &::=&
- \valtype^? \\
+ [\valtype^?] \\
\end{array}
.. note::
@@ -57,7 +60,7 @@ which is a sequence of values.
.. _syntax-functype:
-.. index:: ! function type, valut type, result type
+.. index:: ! function type, value type, result type
pair: abstract syntax; function type
pair: function; type
@@ -65,20 +68,43 @@ Function Types
~~~~~~~~~~~~~~
*Function types* classify the signature of functions,
-mapping a sequence of parameters to a sequence of results.
+mapping a vector of parameters to a vector of results.
.. math::
\begin{array}{llll}
\production{function types} & \functype &::=&
- \valtype^\ast \to \resulttype \\
+ [\vec(\valtype)] \to [\vec(\valtype)] \\
\end{array}
+.. note::
+ In the current version of WebAssembly,
+ the length of the result type vector of a function may be at most :math:`1`.
+ This restriction may be removed in future versions.
+
-.. _syntax-memtype:
.. _syntax-limits:
-.. index:: ! memory type, ! limits, page size
- pair: abstract syntax; memory type
+.. index:: ! limits, memory type, table type
pair: abstract syntax; limits
+ single: memory; limits
+ single: table; limits
+
+Limits
+~~~~~~
+
+*Limits* classify the size range of resizeable storage like associated with :ref:`memory types ` and :ref:`table types `.
+
+.. math::
+ \begin{array}{llll}
+ \production{limits} & \limits &::=&
+ \{ \MIN~\u32, \MAX~\u32^? \} \\
+ \end{array}
+
+If no maximum is given, the respective storage can grow to any size.
+
+
+.. _syntax-memtype:
+.. index:: ! memory type, limits, page size
+ pair: abstract syntax; memory type
pair: memory; type
pair: memory; limits
@@ -91,13 +117,10 @@ Memory Types
\begin{array}{llll}
\production{memory types} & \memtype &::=&
\limits \\
- \production{limits} & \limits &::=&
- \{ \MIN~\u32, \MAX~\u32^? \} \\
\end{array}
-The limits constrain the minimum and optionally the maximum size of a table.
-If no maximum is given, the table can grow to any size.
-Both values are given in units of :ref:`page size `.
+The limits constrain the minimum and optionally the maximum size of a memory.
+The limits are given in units of :ref:`page size `.
.. _syntax-tabletype:
@@ -122,8 +145,8 @@ Table Types
\ANYFUNC \\
\end{array}
-Like memories, tables are constrained by limits for their minimum and optionally the maximum size.
-These sizes are given in numbers of entries.
+Like memories, tables are constrained by limits for their minimum and optionally maximum size.
+The limits are given in numbers of entries.
The element type |ANYFUNC| is the infinite union of all `function types`.
A table of that type thus contains references to functions of heterogeneous type.
@@ -133,7 +156,7 @@ A table of that type thus contains references to functions of heterogeneous type
.. _syntax-globaltype:
-.. index:: ! global type, value type
+.. index:: ! global type, ! mutability, value type
pair: abstract syntax; global type
pair: abstract syntax; mutability
pair: global; type
@@ -147,7 +170,10 @@ Global Types
.. math::
\begin{array}{llll}
\production{global types} & \globaltype &::=&
- \MUT^?~\valtype \\
+ \mut^?~\valtype \\
+ \production{mutability} & \mut &::=&
+ \CONST ~|~
+ \MUT \\
\end{array}
@@ -169,3 +195,17 @@ External Types
\MEM~\memtype ~|~ \\&&&
\GLOBAL~\globaltype \\
\end{array}
+
+
+Conventions
+...........
+
+The following auxiliary notation is defined for sequences of external types, filtering out entries of a specific kind in an order-preserving fashion:
+
+* :math:`\funcs(\externtype^\ast) = [\functype ~|~ \FUNC~\functype \in \externtype^\ast]`
+
+* :math:`\tables(\externtype^\ast) = [\tabletype ~|~ \TABLE~\tabletype \in \externtype^\ast]`
+
+* :math:`\mems(\externtype^\ast) = [\memtype ~|~ \MEM~\memtype \in \externtype^\ast]`
+
+* :math:`\globals(\externtype^\ast) = [\globaltype ~|~ \GLOBAL~\globaltype \in \externtype^\ast]`
diff --git a/document/syntax/values.rst b/document/syntax/values.rst
index b6c4c21aea..1dc03f8b87 100644
--- a/document/syntax/values.rst
+++ b/document/syntax/values.rst
@@ -78,10 +78,10 @@ Conventions
.. index:: ! floating-point number
pair: abstract syntax; floating-point number
-Floating-point Data
-~~~~~~~~~~~~~~~~~~~
+Floating-Point
+~~~~~~~~~~~~~~
-*Floating-point data* consists of values in binary floating-point format according to the `IEEE 754 `_ standard.
+*Floating-point* data consists of values in binary floating-point format according to the `IEEE 754 `_ standard.
.. math::
\begin{array}{llll}
@@ -111,14 +111,6 @@ A vector can have at most :math:`2^{32}-1` elements.
\end{array}
-Conventions
-...........
-
-* :math:`|V|` denotes the length of a vector :math:`V`.
-
-* :math:`V[i]` denotes the :math:`i`-th element of a vector :math:`V`, starting from :math:`0`.
-
-
.. _syntax-name:
.. index:: ! name, byte
pair: abstract syntax; name
diff --git a/document/validation/conventions.rst b/document/validation/conventions.rst
new file mode 100644
index 0000000000..f05c46b2b2
--- /dev/null
+++ b/document/validation/conventions.rst
@@ -0,0 +1,177 @@
+.. index:: ! validation, ! type system, function type, table type, memory type, globaltype, valtype, resulttype, index space
+
+Conventions
+-----------
+
+Validation checks that a WebAssembly module is well-formed.
+Only valid modules can be :ref:`instantiated `.
+
+Validity is defined by a *type system* over the :ref:`abstract syntax ` of both instructions and modules.
+For each piece of abstract syntax, there is a typing rule that specifies the constraints that apply to it.
+All rules are given in two *equivalent* forms:
+
+1. In *prose*, describing the meaning in intuitive form.
+2. In *formal notation*, describing the rule in mathematical form.
+
+.. note::
+ The prose and formal rules are equivalent,
+ so that understanding of the formal notation is *not* required to read this specification.
+ The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.
+
+In both cases, the rules are formulated in a *declarative* manner.
+That is, they only formulate the constraints, they do not define an algorithm.
+A sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the :ref:`appendix `.
+
+
+.. _context:
+.. index:: ! context, function type, table type, memory type, global type, value type, result type, index space
+
+Contexts
+~~~~~~~~
+
+Validity of an individual definition is specified relative to a *context*,
+which collects relevant information about the surrounding :ref:`module ` and other definitions in scope:
+
+* *Types*: the list of types defined in the current module.
+* *Functions*: the list of functions declared in the current module, represented by their function type.
+* *Tables*: the list of tables declared in the current module, represented by their table type.
+* *Memories*: the list of memories declared in the current module, represented by their memory type.
+* *Globals*: the list of globals declared in the current module, represented by their global type.
+* *Locals*: the list of locals declared in the current function (including parameters), represented by their value type.
+* *Labels*: the stack of labels accessible from the current position, represented by their result type.
+
+In other words, a context contains a sequence of suitable :ref:`types ` for each :ref:`index space `,
+describing each defined entry in that space.
+Locals and labels are only used for validating :ref:`instructions ` in :ref:`function bodies `, and are left empty elsewhere.
+The label stack is the only part of the context that changes as validation of an instruction sequence proceeds.
+
+It is convenient to define contexts as :ref:`records ` :math:`C` with abstract syntax:
+
+.. math::
+ \begin{array}{llll}
+ \production{(context)} & C &::=&
+ \begin{array}[t]{l@{~}ll}
+ \{ & \TYPES & \functype^\ast, \\
+ & \FUNCS & \functype^\ast, \\
+ & \TABLES & \tabletype^\ast, \\
+ & \MEMS & \memtype^\ast, \\
+ & \GLOBALS & \globaltype^\ast, \\
+ & \LOCALS & \valtype^\ast, \\
+ & \LABELS & \resulttype^\ast ~\} \\
+ \end{array}
+ \end{array}
+
+.. note::
+ The fields of a context are not defined as :ref:`vectors `,
+ since their lengths are not bounded by the maximum vector size.
+
+In addition to field access :math:`C.\K{field}` the following notation is adopted for manipulating contexts:
+
+* When spelling out a context, empty fields are omitted.
+
+* :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence.
+
+.. note::
+ This notation is defined to *prepend* not *append*.
+ It is only used in situations where the original :math:`C.\K{field}` is either empty
+ or :math:`\K{field}` is :math:`\K{labels}`.
+ In the latter case adding to the front is desired
+ because the :ref:`label index ` space is indexed relatively, that is, in reverse order of addition.
+
+
+Textual Notation
+~~~~~~~~~~~~~~~~
+
+Validation is specified by stylised rules for each relevant part of the :ref:`abstract syntax `.
+The rules not only state constraints defining when a phrase is valid,
+they also classify it with a type.
+A phrase :math:`A` is said to be "valid with type :math:`T`",
+if all constraints expressed by the respective rules are met.
+The form of :math:`T` depends on what :math:`A` is.
+
+.. note::
+ For example, if :math:`A` is a :ref:`function `,
+ then :math:`T` is a :ref:`function type `;
+ for an :math:`A` that is a :ref:`global `,
+ :math:`T` is a :ref:`global type `;
+ and so on.
+
+The rules implicitly assume a given :ref:`context ` :math:`C`.
+In some places, this context is locally extended to a context :math:`C'` with additional entries.
+The formulation "Under context :math:`C'`, ... *statement* ..." is adopted to express that the following statement must apply under the assumptions embodied in the extended context.
+
+
+Formal Notation
+~~~~~~~~~~~~~~~
+
+.. note::
+ This section gives a brief explanation of the notation for specifying typing rules formally.
+ For the interested reader, a more thorough introduction can be found in respective text books. [#tapl]_
+
+The proposition that a phrase :math:`A` has a respective type :math:`T` is written :math:`A : T`.
+In general, however, typing is dependent on the context :math:`C`.
+To express this explicitly, the complete form is a *judgement* :math:`C \vdash A : T`,
+which says that :math:`A : T` holds under the assumptions encoded in :math:`C`.
+
+The formal typing rules use a standard approach for specifying type systems, rendering them into *deduction rules*.
+Every rule has the following general form:
+
+.. math::
+ \frac{
+ \X{premise}_1 \qquad \X{premise}_2 \qquad \dots \qquad \X{premise}_n
+ }{
+ \X{conclusion}
+ }
+
+Such a rule is read as a big implication: if all premises hold, then the conclusion holds.
+Some rules have no premises; they are *axioms* whose conclusion holds unconditionally.
+The conclusion always is a judgment :math:`C \vdash A : T`,
+and there is one respective rule for each relevant construct :math:`A` of the abstract syntax.
+
+.. note::
+ For example, the typing rule for the :ref:`instruction ` :math:`\I32.\ADD` can be given as an axiom:
+
+ .. math::
+ \frac{
+ }{
+ C \vdash \I32.\ADD : [\I32~\I32] \to [\I32]
+ }
+
+ The instruction is always valid with type :math:`[\I32~\I32] \to [\I32`]
+ (saying that it consumes two |I32| values and produces one),
+ independent from any side conditions.
+
+ An instruction like |GETLOCAL| can be typed as follows:
+
+ .. math::
+ \frac{
+ C.\LOCAL[x] = t
+ }{
+ C \vdash \GETLOCAL~x : [] \to [t]
+ }
+
+ Here, the premise enforces that the immediate :ref:`local index ` :math:`x` exists in the context.
+ The instruction produces a value of its respective type :math:`t`
+ (and does not consume any values).
+ If :math:`C.\LOCAL[x]` does not exist then the premise does not hold,
+ and the instruction is ill-typed.
+
+ Finally, a :ref:`structured ` instruction requires
+ a recursive rule, where the premise is itself a typing judgement:
+
+ .. math::
+ \frac{
+ C,\LABEL\,[t^?] \vdash \instr^\ast : [] \to [t^?]
+ }{
+ C \vdash \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?]
+ }
+
+ A |BLOCK| instruction is only valid when the instruction sequence in its body is.
+ Moreover, the result type must match the block's annotation :math:`t^?`.
+ If so, then the |BLOCK| instruction has the same type as the body.
+ Inside the body an additional label of the same type is available,
+ which is expressed by locally extending the context :math:`C` with the additional label information for the premise.
+
+
+.. [#tapl]
+ For example: Benjamin Pierce. `Types and Programming Languages `_. The MIT Press 2002
diff --git a/document/validation/index.rst b/document/validation/index.rst
index 40c9eaee1f..3606f529fc 100644
--- a/document/validation/index.rst
+++ b/document/validation/index.rst
@@ -5,5 +5,5 @@ Validation
:maxdepth: 2
conventions
- modules
instructions
+ modules
diff --git a/document/validation/instructions.rst b/document/validation/instructions.rst
new file mode 100644
index 0000000000..ad3664533c
--- /dev/null
+++ b/document/validation/instructions.rst
@@ -0,0 +1,843 @@
+.. _valid-instr:
+.. index:: instruction, function type, context
+
+Instructions
+------------
+
+:ref:`Instructions ` are classified by :ref:`function types ` :math:`[t_1^\ast] \to [t_2^\ast]`
+that describe how they manipulate the :ref:`operand stack `.
+The types describe the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off
+and the provided output stack with result values of types :math:`t_2^\ast` that it pushes back.
+
+.. note::
+ For example, the instruction :math:`\I32.\ADD` has type :math:`[\I32~\I32] \to [\I32]`,
+ consuming two |I32| values and producing one.
+
+Typing extends to :ref:`instruction sequences ` :math:`\instr^\ast`.
+Such a sequence has a :ref:`function types ` :math:`[t_1^\ast] \to [t_2^\ast]` if the accumulative effect of executing the instructions is consuming values of types :math:`t_1^\ast` off the operand stack and pushing new values of types :math:`t_2^\ast`.
+
+.. _polymorphism:
+
+For some instructions, the typing rules do not fully constrain the type,
+and therefor allow for multiple types.
+Such instructions are called *polymorphic*.
+Two degrees of polymorphism can be distinguished:
+
+* *value-polymorphic*:
+ the :ref:`value type ` :math:`t` of one or several individual operands is unconstrained.
+ That is the case for all :ref:`parametric instructions ` like |DROP| and |SELECT|.
+
+
+* *stack-polymorphic*:
+ the entire (or most of the) :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]` of the instruction is unconstrained.
+ That is the case for all :ref:`control instructions ` that perform an *unconditional control transfer*, such as |UNREACHABLE|, |BR|, |BRTABLE|, and |RETURN|.
+
+In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.
+
+.. note::
+ For example, the |SELECT| instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any possible :ref:`value type ` :math:`t`. Consequently, both instruction sequences
+
+ .. math::
+ (\I32.\CONST~1)~~(\I32.\CONST~2)~~(\I32.\CONST~3)~~\SELECT{}
+
+ and
+
+ .. math::
+ (\F64.\CONST~1.0)~~(\F64.\CONST~2.0)~~(\I32.\CONST~3)~~\SELECT{}
+
+ are valid, with :math:`t` in the typing of |SELECT| being instantiated to |I32| or |F64|, respectively.
+
+ The |UNREACHABLE| instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]` for any possible sequences of value types :math:`t_1^\ast` and :math:`t_2^\ast`.
+ Consequently,
+
+ .. math::
+ \UNREACHABLE~~\I32.\ADD
+
+ is valid by assuming type :math:`[] \to [\I32~\I32]` for the |UNREACHABLE| instruction.
+ In contrast,
+
+ .. math::
+ \UNREACHABLE~~(\I64.\CONST~0)~~\I32.\ADD
+
+ is invalid, because there is no possible type to pick for the |UNREACHABLE| instruction that would make the sequence well-typed.
+
+
+.. _valid-instr-numeric:
+.. index:: numeric instruction
+ pair: validation; instruction
+ single: abstract syntax; instruction
+
+Numeric Instructions
+~~~~~~~~~~~~~~~~~~~~
+
+In this section, the following grammar shorthands are adopted:
+
+.. math::
+ \begin{array}{llll}
+ \production{unary operators} & \unop &::=&
+ \CLZ ~|~
+ \CTZ ~|~
+ \POPCNT ~|~
+ \ABS ~|~
+ \NEG ~|~
+ \SQRT ~|~
+ \CEIL ~|~
+ \FLOOR ~|~
+ \TRUNC ~|~
+ \NEAREST \\
+ \production{binary operators} & \binop &::=&
+ \ADD ~|~
+ \SUB ~|~
+ \MUL ~|~
+ \DIV ~|~
+ \DIV\K{\_}\sx ~|~
+ \REM\K{\_}\sx ~|~
+ \FMIN ~|~
+ \FMAX ~|~
+ \COPYSIGN ~|~ \\&&&
+ \AND ~|~
+ \OR ~|~
+ \XOR ~|~
+ \SHL ~|~
+ \SHR\K{\_}\sx ~|~
+ \ROTL ~|~
+ \ROTR \\
+ \production{test operators} & \testop &::=&
+ \EQZ \\
+ \production{relational operators} & \relop &::=&
+ \EQ ~|~
+ \NE ~|~
+ \LT ~|~
+ \GT ~|~
+ \LE ~|~
+ \GE ~|~
+ \LT\K{\_}\sx ~|~
+ \GT\K{\_}\sx ~|~
+ \LE\K{\_}\sx ~|~
+ \GE\K{\_}\sx \\
+ \production{conversion operators} & \cvtop &::=&
+ \WRAP ~|~
+ \EXTEND\K{\_}\sx ~|~
+ \TRUNC\K{\_}\sx ~|~
+ \CONVERT\K{\_}\sx ~|~
+ \DEMOTE ~|~
+ \PROMOTE ~|~
+ \REINTERPRET \\
+ \end{array}
+
+
+.. _valid-const:
+
+:math:`t \K{.const}~c`
+......................
+
+* The instruction is valid with type :math:`[] \to [t]`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash t\K{.const}~c : [] \to [t]
+ }
+
+
+.. _valid-unop:
+
+:math:`t\K{.}\unop`
+...................
+
+* The instruction is valid with type :math:`[t] \to [t]`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash t\K{.}\unop : [t] \to [t]
+ }
+
+
+.. _valid-binop:
+
+:math:`t\K{.}\binop`
+....................
+
+* The instruction is valid with type :math:`[t~t] \to [t]`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash t\K{.}\binop : [t~t] \to [t]
+ }
+
+
+.. _valid-testop:
+
+:math:`t\K{.}\testop`
+.....................
+
+* The instruction is valid with type :math:`[t] \to [\I32]`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash t\K{.}\testop : [t] \to [\I32]
+ }
+
+
+.. _valid-relop:
+
+:math:`t\K{.}\relop`
+....................
+
+* The instruction is valid with type :math:`[t~t] \to [\I32]`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash t\K{.}\relop : [t~t] \to [\I32]
+ }
+
+
+.. _valid-cvtop:
+
+:math:`t_2\K{.}\cvtop/t_1`
+..........................
+
+* The instruction is valid with type :math:`[t_1] \to [t_2]`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash t_2\K{.}\cvtop/t_1 : [t_1] \to [t_2]
+ }
+
+
+.. _valid-instr-parametric:
+.. index:: parametric instructions, value type, polymorphism
+ pair: validation; instruction
+ single: abstract syntax; instruction
+
+Parametric Instructions
+~~~~~~~~~~~~~~~~~~~~~~~
+
+.. _valid-drop:
+
+:math:`\DROP`
+.............
+
+* The instruction is valid with type :math:`[t] \to []`, for any :ref:`value type ` :math:`t`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash \DROP : [t] \to []
+ }
+
+
+.. _valid-select:
+
+:math:`\SELECT`
+...............
+
+* The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`value type ` :math:`t`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash \SELECT : [t~t~\I32] \to [t]
+ }
+
+.. note::
+ Both |DROP| and |SELECT| are :ref:`value-polymorphic ` instructions.
+
+
+.. _valid-instr-variable:
+.. index:: variable instructions, local index, global index
+ pair: validation; instruction
+ single: abstract syntax; instruction
+
+Variable Instructions
+~~~~~~~~~~~~~~~~~~~~~
+
+.. _valid-get_local:
+
+:math:`\GETLOCAL~x`
+...................
+
+* The local :math:`C.\LOCALS[x]` must be defined in the context.
+
+* Let :math:`t` be the :ref:`value type ` :math:`C.\LOCALS[x]`.
+
+* Then the instruction is valid with type :math:`[] \to [t]`.
+
+.. math::
+ \frac{
+ C.\LOCALS[x] = t
+ }{
+ C \vdash \GETLOCAL~x : [] \to [t]
+ }
+
+
+.. _valid-set_local:
+
+:math:`\SETLOCAL~x`
+...................
+
+* The local :math:`C.\LOCALS[x]` must be defined in the context.
+
+* Let :math:`t` be the :ref:`value type ` :math:`C.\LOCALS[x]`.
+
+* Then the instruction is valid with type :math:`[t] \to []`.
+
+.. math::
+ \frac{
+ C.\LOCALS[x] = t
+ }{
+ C \vdash \SETLOCAL~x : [t] \to []
+ }
+
+
+.. _valid-tee_local:
+
+:math:`\TEELOCAL~x`
+...................
+
+* The local :math:`C.\LOCALS[x]` must be defined in the context.
+
+* Let :math:`t` be the :ref:`value type ` :math:`C.\LOCALS[x]`.
+
+* Then the instruction is valid with type :math:`[t] \to [t]`.
+
+.. math::
+ \frac{
+ C.\LOCALS[x] = t
+ }{
+ C \vdash \TEELOCAL~x : [t] \to [t]
+ }
+
+
+.. _valid-get_global:
+
+:math:`\GETGLOBAL~x`
+....................
+
+* The global :math:`C.\GLOBALS[x]` must be defined in the context.
+
+* Let :math:`\mut~t` be the :ref:`value type ` :math:`C.\LOCALS[x]`.
+
+* Then the instruction is valid with type :math:`[] \to [t]`.
+
+.. math::
+ \frac{
+ C.\GLOBALS[x] = \mut~t
+ }{
+ C \vdash \GETGLOBAL~x : [] \to [t]
+ }
+
+
+.. _valid-set_global:
+
+:math:`\SETGLOBAL~x`
+....................
+
+* The global :math:`C.\GLOBALS[x]` must be defined in the context.
+
+* Let :math:`\mut~t` be the :ref:`global type ` :math:`C.\GLOBALS[x]`.
+
+* The mutability :math:`\mut` must be |MUT|.
+
+* Then the instruction is valid with type :math:`[t] \to []`.
+
+.. math::
+ \frac{
+ C.\GLOBALS[x] = \MUT~t
+ }{
+ C \vdash \SETGLOBAL~x : [t] \to []
+ }
+
+
+.. _valid-instr-memory:
+.. _valid-memarg:
+.. index:: memory instruction, memory index
+ pair: validation; instruction
+ single: abstract syntax; instruction
+
+Memory Instructions
+~~~~~~~~~~~~~~~~~~~
+
+.. _valid-load:
+
+:math:`t\K{.load}~\memarg`
+..........................
+
+* The memory :math:`C.\MEMS[0]` must be defined in the context.
+
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`width ` of :math:`t`.
+
+* Then the instruction is valid with type :math:`[\I32] \to [t]`.
+
+.. math::
+ \frac{
+ C.\MEMS[0] = \memtype
+ \qquad
+ 2^{\memarg.\ALIGN} \leq |t|
+ }{
+ C \vdash t\K{.load}~\memarg : [\I32] \to [t]
+ }
+
+
+.. _valid-loadn:
+
+:math:`t\K{.load}N\K{\_}\sx~\memarg`
+....................................
+
+* The memory :math:`C.\MEMS[0]` must be defined in the context.
+
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N`.
+
+* Then the instruction is valid with type :math:`[\I32] \to [t]`.
+
+.. math::
+ \frac{
+ C.\MEMS[0] = \memtype
+ \qquad
+ 2^{\memarg.\ALIGN} \leq N
+ }{
+ C \vdash t\K{.load}N\K{\_}\sx~\memarg : [\I32] \to [t]
+ }
+
+
+.. _valid-store:
+
+:math:`t\K{.store}~\memarg`
+...........................
+
+* The memory :math:`C.\MEMS[0]` must be defined in the context.
+
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`width ` of :math:`t`.
+
+* Then the instruction is valid with type :math:`[\I32~t] \to []`.
+
+.. math::
+ \frac{
+ C.\MEMS[0] = \memtype
+ \qquad
+ 2^{\memarg.\ALIGN} \leq |t|
+ }{
+ C \vdash t\K{.store}~\memarg : [\I32~t] \to []
+ }
+
+
+.. _valid-storen:
+
+:math:`t\K{.store}N~\memarg`
+............................
+
+* The memory :math:`C.\MEMS[0]` must be defined in the context.
+
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N`.
+
+* Then the instruction is valid with type :math:`[\I32~t] \to []`.
+
+.. math::
+ \frac{
+ C.\MEMS[0] = \memtype
+ \qquad
+ 2^{\memarg.\ALIGN} \leq N
+ }{
+ C \vdash t\K{.store}N~\memarg : [\I32~t] \to []
+ }
+
+
+.. _valid-current_memory:
+
+:math:`\CURRENTMEMORY`
+......................
+
+* The memory :math:`C.\MEMS[0]` must be defined in the context.
+
+* Then the instruction is valid with type :math:`[] \to [\I32]`.
+
+.. math::
+ \frac{
+ C.\MEMS[0] = \memtype
+ }{
+ C \vdash \CURRENTMEMORY : [] \to [\I32]
+ }
+
+
+.. _valid-grow_memory:
+
+:math:`\GROWMEMORY`
+...................
+
+* The memory :math:`C.\MEMS[0]` must be defined in the context.
+
+* Then the instruction is valid with type :math:`[\I32] \to [\I32]`.
+
+.. math::
+ \frac{
+ C.\MEMS[0] = \memtype
+ }{
+ C \vdash \GROWMEMORY : [\I32] \to [\I32]
+ }
+
+
+.. _valid-instr-control:
+.. _valid-label:
+.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism
+ pair: validation; instruction
+ single: abstract syntax; instruction
+
+Control Instructions
+~~~~~~~~~~~~~~~~~~~~
+
+.. _valid-nop:
+
+:math:`\NOP`
+............
+
+* The instruction is valid with type :math:`[] \to []`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash \NOP : [] \to []
+ }
+
+
+.. _valid-unreachable:
+
+:math:`\UNREACHABLE`
+....................
+
+* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`.
+
+.. math::
+ \frac{
+ }{
+ C \vdash \UNREACHABLE : [t_1^\ast] \to [t_2^\ast]
+ }
+
+.. note::
+ The |UNREACHABLE| instruction is :ref:`stack-polymorphic `.
+
+
+.. _valid-block:
+
+:math:`\BLOCK~[t^?]~\instr^\ast~\END`
+.....................................
+
+* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t^?]` prepended to the |LABELS| vector.
+
+* Under context :math:`C'`,
+ the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^?]`.
+
+* Then the compound instruction is valid with type :math:`[] \to [t^?]`.
+
+.. math::
+ \frac{
+ C,\LABELS\,[t^?] \vdash \instr^\ast : [] \to [t^?]
+ }{
+ C \vdash \BLOCK~[^?]~\instr^\ast~\END : [] \to [t^?]
+ }
+
+.. note::
+ The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the block was entered.
+ This may be generalized in future versions of WebAssembly.
+
+
+.. _valid-loop:
+
+:math:`\LOOP~[t^?]~\instr^\ast~\END`
+....................................
+
+* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the empty :ref:`result type ` :math:`[]` prepended to the |LABELS| vector.
+
+* Under context :math:`C'`,
+ the instruction sequence :math:`\instr^\ast` must be :ref:`valid