Index of Semantic Rules

Well-formedness of Types

Construct	Judgement
Numeric type	$C⊢\mathit{numtype}\text{ok}$
Vector type	$C⊢\mathit{vectype}\text{ok}$
Heap type	$C⊢\mathit{heaptype}\text{ok}$
Reference type	$C⊢\mathit{reftype}\text{ok}$
Value type	$C⊢\mathit{valtype}\text{ok}$
Packed type	$C⊢\mathit{packedtype}\text{ok}$
Storage type	$C⊢\mathit{storagetype}\text{ok}$
Field type	$C⊢\mathit{fieldtype}\text{ok}$
Result type	$C⊢\mathit{resulttype}\text{ok}$
Instruction type	$C⊢\mathit{instrtype}\text{ok}$
Function type	$C⊢\mathit{functype}\text{ok}$
Structure type	$C⊢\mathit{structtype}\text{ok}$
Array type	$C⊢\mathit{arraytype}\text{ok}$
Composite type	$C⊢\mathit{comptype}\text{ok}$
Sub type	$C⊢\mathit{subtype}\text{ok}$
Recursive type	$C⊢\mathit{rectype}\text{ok}$
Defined type	$C⊢\mathit{deftype}\text{ok}$
Block type	$C⊢\mathit{blocktype}:\mathit{instrtype}$
Table type	$C⊢\mathit{tabletype}\text{ok}$
Memory type	$C⊢\mathit{memtype}\text{ok}$
Global type	$C⊢\mathit{globaltype}\text{ok}$
External type	$C⊢\mathit{externtype}\text{ok}$
Type definitions	$C⊢{\mathit{type}}^{\ast }\text{ok}$

Typing of Static Constructs

Construct	Judgement
Instruction	$S;C⊢\mathit{instr}:\mathit{functype}$
Instruction sequence	$S;C⊢{\mathit{instr}}^{\ast }:\mathit{functype}$
Expression	$C⊢\mathit{expr}:\mathit{resulttype}$
Function	$C⊢\mathit{func}:\mathit{functype}$
Local	$C⊢\mathit{local}:\mathit{localtype}$
Table	$C⊢\mathit{table}:\mathit{tabletype}$
Memory	$C⊢\mathit{mem}:\mathit{memtype}$
Limits	$C⊢\mathit{limits}:k$
Global	$C⊢\mathit{global}:\mathit{globaltype}$
Element segment	$C⊢\mathit{elem}:\mathit{reftype}$
Element mode	$C⊢\mathit{elemmode}:\mathit{reftype}$
Data segment	$C⊢\mathit{data}\text{ok}$
Data mode	$C⊢\mathit{datamode}\text{ok}$
Start function	$C⊢\mathit{start}\text{ok}$
Export	$C⊢\mathit{export}:\mathit{externtype}$
Export description	$C⊢\mathit{exportdesc}:\mathit{externtype}$
Import	$C⊢\mathit{import}:\mathit{externtype}$
Import description	$C⊢\mathit{importdesc}:\mathit{externtype}$
Module	$⊢\mathit{module}:{\mathit{externtype}}^{\ast }\to {\mathit{externtype}}^{\ast }$

Typing of Runtime Constructs

Construct	Judgement
Value	$S⊢\mathit{val}:\mathit{valtype}$
Result	$S⊢\mathit{result}:\mathit{resulttype}$
Packed value	$S⊢\mathit{packedval}:\mathit{packedtype}$
Field value	$S⊢\mathit{fieldval}:\mathit{storagetype}$
External value	$S⊢\mathit{externval}:\mathit{externtype}$
Function instance	$S⊢\mathit{funcinst}:\mathit{functype}$
Table instance	$S⊢\mathit{tableinst}:\mathit{tabletype}$
Memory instance	$S⊢\mathit{meminst}:\mathit{memtype}$
Global instance	$S⊢\mathit{globalinst}:\mathit{globaltype}$
Element instance	$S⊢\mathit{eleminst}:t$
Data instance	$S⊢\mathit{datainst}\text{ok}$
Structure instance	$S⊢\mathit{structinst}\text{ok}$
Array instance	$S⊢\mathit{arrayinst}\text{ok}$
Export instance	$S⊢\mathit{exportinst}\text{ok}$
Module instance	$S⊢\mathit{moduleinst}:C$
Store	$⊢\mathit{store}\text{ok}$
Configuration	$⊢\mathit{config}\text{ok}$
Thread	$S;{\mathit{resulttype}}^{?}⊢\mathit{thread}:\mathit{resulttype}$
Frame	$S⊢\mathit{frame}:C$

Defaultability

Construct	Judgement
Defaultable value type	$C⊢\mathit{valtype}\text{defaultable}$

Constantness

Construct	Judgement
Constant expression	$C⊢\mathit{expr}\text{const}$
Constant instruction	$C⊢\mathit{instr}\text{const}$

Matching

Construct	Judgement
Number type	$C⊢{\mathit{numtype}}_1\le {\mathit{numtype}}_2$
Vector type	$C⊢{\mathit{vectype}}_1\le {\mathit{vectype}}_2$
Heap type	$C⊢{\mathit{heaptype}}_1\le {\mathit{heaptype}}_2$
Reference type	$C⊢{\mathit{reftype}}_1\le {\mathit{reftype}}_2$
Value type	$C⊢{\mathit{valtype}}_1\le {\mathit{valtype}}_2$
Packed type	$C⊢{\mathit{packedtype}}_1\le {\mathit{packedtype}}_2$
Storage type	$C⊢{\mathit{storagetype}}_1\le {\mathit{storagetype}}_2$
Field type	$C⊢{\mathit{fieldtype}}_1\le {\mathit{fieldtype}}_2$
Result type	$C⊢{\mathit{resulttype}}_1\le {\mathit{resulttype}}_2$
Instruction type	$C⊢{\mathit{instrtype}}_1\le {\mathit{instrtype}}_2$
Function type	$C⊢{\mathit{functype}}_1\le {\mathit{functype}}_2$
Structure type	$C⊢{\mathit{structtype}}_1\le {\mathit{structtype}}_2$
Array type	$C⊢{\mathit{arraytype}}_1\le {\mathit{arraytype}}_2$
Composite type	$C⊢{\mathit{comptype}}_1\le {\mathit{comptype}}_2$
Defined type	$C⊢{\mathit{deftype}}_1\le {\mathit{deftype}}_2$
Table type	$C⊢{\mathit{tabletype}}_1\le {\mathit{tabletype}}_2$
Memory type	$C⊢{\mathit{memtype}}_1\le {\mathit{memtype}}_2$
Global type	$C⊢{\mathit{globaltype}}_1\le {\mathit{globaltype}}_2$
External type	$C⊢{\mathit{externtype}}_1\le {\mathit{externtype}}_2$
Limits	$C⊢{\mathit{limits}}_1\le {\mathit{limits}}_2$

Store Extension

Construct	Judgement
Function instance	$⊢{\mathit{funcinst}}_1⪯{\mathit{funcinst}}_2$
Table instance	$⊢{\mathit{tableinst}}_1⪯{\mathit{tableinst}}_2$
Memory instance	$⊢{\mathit{meminst}}_1⪯{\mathit{meminst}}_2$
Global instance	$⊢{\mathit{globalinst}}_1⪯{\mathit{globalinst}}_2$
Element instance	$⊢{\mathit{eleminst}}_1⪯{\mathit{eleminst}}_2$
Data instance	$⊢{\mathit{datainst}}_1⪯{\mathit{datainst}}_2$
Structure instance	$⊢{\mathit{structinst}}_1⪯{\mathit{structinst}}_2$
Array instance	$⊢{\mathit{arrayinst}}_1⪯{\mathit{arrayinst}}_2$
Store	$⊢{\mathit{store}}_1⪯{\mathit{store}}_2$

Execution

Construct	Judgement
Instruction	$S;F;{\mathit{instr}}^{\ast }\hookrightarrow S^{\prime };F^{\prime };{{\mathit{instr}}^{\prime }}^{\ast }$
Expression	$S;F;\mathit{expr}\hookrightarrow S^{\prime };F^{\prime };{\mathit{expr}}^{\prime }$