Index of Semantic Rules

Well-formedness of Types

Construct	Judgement
Numeric type	\(C \href{../valid/types.html#valid-numtype}{\vdash} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} : \href{../valid/types.html#valid-numtype}{\mathsf{ok}}\)
Vector type	\(C \href{../valid/types.html#valid-vectype}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} : \href{../valid/types.html#valid-vectype}{\mathsf{ok}}\)
Heap type	\(C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}}\)
Reference type	\(C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}}\)
Value type	\(C \href{../valid/types.html#valid-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\)
Packed type	\(C \href{../valid/types.html#valid-packtype}{\vdash} \href{../syntax/types.html#syntax-packtype}{\mathit{packtype}} : \href{../valid/types.html#valid-packtype}{\mathsf{ok}}\)
Storage type	\(C \href{../valid/types.html#valid-storagetype}{\vdash} \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}} : \href{../valid/types.html#valid-storagetype}{\mathsf{ok}}\)
Field type	\(C \href{../valid/types.html#valid-fieldtype}{\vdash} \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}}\)
Result type	\(C \href{../valid/types.html#valid-resulttype}{\vdash} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}\)
Instruction type	\(C \href{../valid/types.html#valid-instrtype}{\vdash} \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}}\)
Composite type	\(C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathit{comptype}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}\)
Sub type	\(C \href{../valid/types.html#valid-subtype}{\vdash} \href{../syntax/types.html#syntax-subtype}{\mathit{subtype}} : \href{../valid/types.html#valid-subtype}{\mathsf{ok}}\)
Recursive type	\(C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{rectype}} : \href{../valid/types.html#valid-rectype}{\mathsf{ok}}\)
Defined type	\(C \href{../appendix/properties.html#valid-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}}\)
Block type	\(C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/types.html#syntax-blocktype}{\mathit{blocktype}} : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\)
Tag type	\(C \href{../valid/types.html#valid-tagtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} : \href{../valid/types.html#valid-tagtype}{\mathsf{ok}}\)
Global type	\(C \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}}\)
Memory type	\(C \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} : \href{../valid/types.html#valid-memtype}{\mathsf{ok}}\)
Table type	\(C \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} : \href{../valid/types.html#valid-tabletype}{\mathsf{ok}}\)
External type	\(C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}\)
Type definitions	\(C \href{../valid/modules.html#valid-types}{\vdash} \href{../syntax/modules.html#syntax-type}{\mathit{type}}^\ast : \href{../valid/modules.html#valid-types}{\mathsf{ok}}\)

Typing of Static Constructs

Construct	Judgement
Instruction	\(S;C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\)
Instruction sequence	\(S;C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\)
Catch clause	\(C \href{../valid/instructions.html#valid-catch}{\vdash} \href{../syntax/instructions.html#syntax-catch}{\mathit{catch}} : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}}\)
Expression	\(C \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} : \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\)
Limits	\(C \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : k\)
Tag	\(C \href{../valid/modules.html#valid-tag}{\vdash} \href{../syntax/modules.html#syntax-tag}{\mathit{tag}} : \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\)
Global	\(C \href{../valid/modules.html#valid-global}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)
Memory	\(C \href{../valid/modules.html#valid-mem}{\vdash} \href{../syntax/modules.html#syntax-mem}{\mathit{mem}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)
Table	\(C \href{../valid/modules.html#valid-table}{\vdash} \href{../syntax/modules.html#syntax-table}{\mathit{table}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)
Function	\(C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\)
Local	\(C \href{../valid/modules.html#valid-local}{\vdash} \href{../syntax/modules.html#syntax-local}{\mathit{local}} : \href{../valid/conventions.html#syntax-localtype}{\mathit{localtype}}\)
Element segment	\(C \href{../valid/modules.html#valid-elem}{\vdash} \href{../syntax/modules.html#syntax-elem}{\mathit{elem}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\)
Element mode	\(C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\)
Data segment	\(C \href{../valid/modules.html#valid-data}{\vdash} \href{../syntax/modules.html#syntax-data}{\mathit{data}} : \href{../valid/modules.html#valid-data}{\mathsf{ok}}\)
Data mode	\(C \href{../valid/modules.html#valid-datamode}{\vdash} \href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}} : \href{../valid/modules.html#valid-datamode}{\mathsf{ok}}\)
Start function	\(C \href{../valid/modules.html#valid-start}{\vdash} \href{../syntax/modules.html#syntax-start}{\mathit{start}} : \href{../valid/modules.html#valid-start}{\mathsf{ok}}\)
Import	\(C \href{../valid/modules.html#valid-import}{\vdash} \href{../syntax/modules.html#syntax-import}{\mathit{import}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\)
Export	\(C \href{../valid/modules.html#valid-export}{\vdash} \href{../syntax/modules.html#syntax-export}{\mathit{export}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\)
Module	\(\href{../valid/modules.html#valid-module}{\vdash} \href{../syntax/modules.html#syntax-module}{\mathit{module}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \rightarrow \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\)

Typing of Runtime Constructs

Construct	Judgement
Value	\(S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)
Result	\(S \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-result}{\mathit{result}} : \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\)