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}} \mathrel{\mbox{ok}}\)

Vector type

\(C \href{../valid/types.html#valid-vectype}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} \mathrel{\mbox{ok}}\)

Heap type

\(C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \mathrel{\mbox{ok}}\)

Reference type

\(C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}}\)

Value type

\(C \href{../valid/types.html#valid-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\mbox{ok}}\)

Packed type

\(C \href{../valid/types.html#valid-packedtype}{\vdash} \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}} \mathrel{\mbox{ok}}\)

Storage type

\(C \href{../valid/types.html#valid-storagetype}{\vdash} \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}} \mathrel{\mbox{ok}}\)

Field type

\(C \href{../valid/types.html#valid-fieldtype}{\vdash} \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}} \mathrel{\mbox{ok}}\)

Result type

\(C \href{../valid/types.html#valid-resulttype}{\vdash} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} \mathrel{\mbox{ok}}\)

Instruction type

\(C \href{../valid/types.html#valid-instrtype}{\vdash} \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}} \mathrel{\mbox{ok}}\)

Function type

\(C \href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}}\)

Structure type

\(C \href{../valid/types.html#valid-structtype}{\vdash} \href{../syntax/types.html#syntax-structtype}{\mathit{structtype}} \mathrel{\mbox{ok}}\)

Array type

\(C \href{../valid/types.html#valid-arraytype}{\vdash} \href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}} \mathrel{\mbox{ok}}\)

Composite type

\(C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathit{comptype}} \mathrel{\mbox{ok}}\)

Sub type

\(C \href{../valid/types.html#valid-subtype}{\vdash} \href{../syntax/types.html#syntax-subtype}{\mathit{subtype}} \mathrel{\mbox{ok}}\)

Recursive type

\(C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{rectype}} \mathrel{\mbox{ok}}\)

Defined type

\(C \href{../valid/types.html#valid-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} \mathrel{\mbox{ok}}\)

Block type

\(C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\)

Table type

\(C \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}}\)

Memory type

\(C \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}}\)

Global type

\(C \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}}\)

External type

\(C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} \mathrel{\mbox{ok}}\)

Type definitions

\(C \href{../valid/modules.html#valid-types}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{type}}^\ast \mathrel{\mbox{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{../syntax/types.html#syntax-functype}{\mathit{functype}}\)

Instruction sequence

\(S;C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)

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}}\)

Function

\(C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)

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}}\)

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}}\)

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}}\)

Limits

\(C \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : k\)

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}}\)

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}} \mathrel{\mbox{ok}}\)

Data mode

\(C \href{../valid/modules.html#valid-datamode}{\vdash} \href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}} \mathrel{\mbox{ok}}\)

Start function

\(C \href{../valid/modules.html#valid-start}{\vdash} \href{../syntax/modules.html#syntax-start}{\mathit{start}} \mathrel{\mbox{ok}}\)

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}}\)

Export description

\(C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\)

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}}\)

Import description

\(C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}} : \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}}\)

Packed value

\(S \href{../appendix/properties.html#valid-packedval}{\vdash} \href{../exec/runtime.html#syntax-packedval}{\mathit{packedval}} : \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}\)

Field value

\(S \href{../appendix/properties.html#valid-fieldval}{\vdash} \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}} : \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\)

External value

\(S \href{../exec/values.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\)

Function instance

\(S \href{../appendix/properties.html#valid-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)

Table instance

\(S \href{../appendix/properties.html#valid-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)

Memory instance

\(S \href{../appendix/properties.html#valid-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)

Global instance

\(S \href{../appendix/properties.html#valid-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)

Element instance

\(S \href{../appendix/properties.html#valid-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} : t\)

Data instance

\(S \href{../appendix/properties.html#valid-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} \mathrel{\mbox{ok}}\)

Structure instance

\(S \href{../appendix/properties.html#valid-structinst}{\vdash} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}} \mathrel{\mbox{ok}}\)

Array instance

\(S \href{../appendix/properties.html#valid-arrayinst}{\vdash} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}} \mathrel{\mbox{ok}}\)

Export instance

\(S \href{../appendix/properties.html#valid-exportinst}{\vdash} \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} \mathrel{\mbox{ok}}\)

Module instance

\(S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C\)

Store

\(\href{../appendix/properties.html#valid-store}{\vdash} \href{../exec/runtime.html#syntax-store}{\mathit{store}} \mathrel{\mbox{ok}}\)

Configuration

\(\href{../appendix/properties.html#valid-config}{\vdash} \href{../exec/runtime.html#syntax-config}{\mathit{config}} \mathrel{\mbox{ok}}\)

Thread

\(S;\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../appendix/properties.html#valid-thread}{\vdash} \href{../exec/runtime.html#syntax-thread}{\mathit{thread}} : \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\)

Frame

\(S \href{../appendix/properties.html#valid-frame}{\vdash} \href{../exec/runtime.html#syntax-frame}{\mathit{frame}} : C\)

Defaultability

Construct

Judgement

Defaultable value type

\(C \href{../valid/types.html#valid-defaultable}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \href{../valid/types.html#valid-defaultable}{\mathrel{\mbox{defaultable}}}\)

Constantness

Construct

Judgement

Constant expression

\(C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}}\)

Constant instruction

\(C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}}\)

Matching

Construct

Judgement

Number type

\(C \href{../valid/matching.html#match-numtype}{\vdash} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}_1 \href{../valid/matching.html#match-numtype}{\leq} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}_2\)

Vector type

\(C \href{../valid/matching.html#match-vectype}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}_1 \href{../valid/matching.html#match-vectype}{\leq} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}_2\)

Heap type

\(C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1 \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\)

Reference type

\(C \href{../valid/matching.html#match-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2\)

Value type

\(C \href{../valid/matching.html#match-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1 \href{../valid/matching.html#match-valtype}{\leq} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\)

Packed type

\(C \href{../valid/matching.html#match-packedtype}{\vdash} \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_1 \href{../valid/matching.html#match-packedtype}{\leq} \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_2\)

Storage type

\(C \href{../valid/matching.html#match-storagetype}{\vdash} \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1 \href{../valid/matching.html#match-storagetype}{\leq} \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\)

Field type

\(C \href{../valid/matching.html#match-fieldtype}{\vdash} \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1 \href{../valid/matching.html#match-fieldtype}{\leq} \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2\)

Result type

\(C \href{../valid/matching.html#match-resulttype}{\vdash} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_1 \href{../valid/matching.html#match-resulttype}{\leq} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}_2\)

Instruction type

\(C \href{../valid/matching.html#match-instrtype}{\vdash} \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_1 \href{../valid/matching.html#match-instrtype}{\leq} \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_2\)

Function type

\(C \href{../valid/matching.html#match-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1 \href{../valid/matching.html#match-functype}{\leq} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\)

Structure type

\(C \href{../valid/matching.html#match-structtype}{\vdash} \href{../syntax/types.html#syntax-structtype}{\mathit{structtype}}_1 \href{../valid/matching.html#match-structtype}{\leq} \href{../syntax/types.html#syntax-structtype}{\mathit{structtype}}_2\)

Array type

\(C \href{../valid/matching.html#match-arraytype}{\vdash} \href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}}_1 \href{../valid/matching.html#match-arraytype}{\leq} \href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}}_2\)

Composite type

\(C \href{../valid/matching.html#match-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_1 \href{../valid/matching.html#match-comptype}{\leq} \href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_2\)

Defined type

\(C \href{../valid/matching.html#match-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1 \href{../valid/matching.html#match-deftype}{\leq} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\)

Table type

\(C \href{../valid/matching.html#match-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_1 \href{../valid/matching.html#match-tabletype}{\leq} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_2\)

Memory type

\(C \href{../valid/matching.html#match-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_1 \href{../valid/matching.html#match-memtype}{\leq} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_2\)

Global type

\(C \href{../valid/matching.html#match-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1 \href{../valid/matching.html#match-globaltype}{\leq} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\)

External type

\(C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_2\)

Limits

\(C \href{../valid/matching.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/matching.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\)

Store Extension

Construct

Judgement

Function instance

\(\href{../appendix/properties.html#extend-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_2\)

Table instance

\(\href{../appendix/properties.html#extend-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_2\)

Memory instance

\(\href{../appendix/properties.html#extend-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_2\)

Global instance

\(\href{../appendix/properties.html#extend-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_2\)

Element instance

\(\href{../appendix/properties.html#extend-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_2\)

Data instance

\(\href{../appendix/properties.html#extend-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_2\)

Structure instance

\(\href{../appendix/properties.html#extend-structinst}{\vdash} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}_2\)

Array instance

\(\href{../appendix/properties.html#extend-arrayinst}{\vdash} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}_2\)

Store

\(\href{../appendix/properties.html#extend-store}{\vdash} \href{../exec/runtime.html#syntax-store}{\mathit{store}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-store}{\mathit{store}}_2\)

Execution

Construct

Judgement

Instruction

\(S;F;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S';F';{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast\)

Expression

\(S;F;\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S';F';\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}'\)