Index of Semantic Rules¶
Well-formedness of Types¶
Construct |
Judgement |
---|---|
\(C \href{../valid/types.html#valid-numtype}{\vdash} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-vectype}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-packedtype}{\vdash} \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-storagetype}{\vdash} \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-fieldtype}{\vdash} \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-resulttype}{\vdash} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-instrtype}{\vdash} \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-structtype}{\vdash} \href{../syntax/types.html#syntax-structtype}{\mathit{structtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-arraytype}{\vdash} \href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathit{comptype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-subtype}{\vdash} \href{../syntax/types.html#syntax-subtype}{\mathit{subtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{rectype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\) |
|
\(C \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} \mathrel{\mbox{ok}}\) |
|
\(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 |
---|---|
\(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}}\) |
|
\(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}}\) |
|
\(C \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} : \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\) |
|
\(C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) |
|
\(C \href{../valid/modules.html#valid-local}{\vdash} \href{../syntax/modules.html#syntax-local}{\mathit{local}} : \href{../valid/conventions.html#syntax-localtype}{\mathit{localtype}}\) |
|
\(C \href{../valid/modules.html#valid-table}{\vdash} \href{../syntax/modules.html#syntax-table}{\mathit{table}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) |
|
\(C \href{../valid/modules.html#valid-mem}{\vdash} \href{../syntax/modules.html#syntax-mem}{\mathit{mem}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) |
|
\(C \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : k\) |
|
\(C \href{../valid/modules.html#valid-global}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) |
|
\(C \href{../valid/modules.html#valid-elem}{\vdash} \href{../syntax/modules.html#syntax-elem}{\mathit{elem}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\) |
|
\(C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\) |
|
\(C \href{../valid/modules.html#valid-data}{\vdash} \href{../syntax/modules.html#syntax-data}{\mathit{data}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/modules.html#valid-datamode}{\vdash} \href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/modules.html#valid-start}{\vdash} \href{../syntax/modules.html#syntax-start}{\mathit{start}} \mathrel{\mbox{ok}}\) |
|
\(C \href{../valid/modules.html#valid-export}{\vdash} \href{../syntax/modules.html#syntax-export}{\mathit{export}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) |
|
\(C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) |
|
\(C \href{../valid/modules.html#valid-import}{\vdash} \href{../syntax/modules.html#syntax-import}{\mathit{import}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) |
|
\(C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) |
|
\(\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 |
---|---|
\(S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) |
|
\(S \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-result}{\mathit{result}} : \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}\) |
|
\(S \href{../appendix/properties.html#valid-packedval}{\vdash} \href{../exec/runtime.html#syntax-packedval}{\mathit{packedval}} : \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}\) |
|
\(S \href{../appendix/properties.html#valid-fieldval}{\vdash} \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}} : \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) |
|
\(S \href{../exec/values.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) |
|
\(S \href{../appendix/properties.html#valid-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) |
|
\(S \href{../appendix/properties.html#valid-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) |
|
\(S \href{../appendix/properties.html#valid-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) |
|
\(S \href{../appendix/properties.html#valid-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) |
|
\(S \href{../appendix/properties.html#valid-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} : t\) |
|
\(S \href{../appendix/properties.html#valid-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} \mathrel{\mbox{ok}}\) |
|
\(S \href{../appendix/properties.html#valid-structinst}{\vdash} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}} \mathrel{\mbox{ok}}\) |
|
\(S \href{../appendix/properties.html#valid-arrayinst}{\vdash} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}} \mathrel{\mbox{ok}}\) |
|
\(S \href{../appendix/properties.html#valid-exportinst}{\vdash} \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} \mathrel{\mbox{ok}}\) |
|
\(S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C\) |
|
\(\href{../appendix/properties.html#valid-store}{\vdash} \href{../exec/runtime.html#syntax-store}{\mathit{store}} \mathrel{\mbox{ok}}\) |
|
\(\href{../appendix/properties.html#valid-config}{\vdash} \href{../exec/runtime.html#syntax-config}{\mathit{config}} \mathrel{\mbox{ok}}\) |
|
\(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}}\) |
|
\(S \href{../appendix/properties.html#valid-frame}{\vdash} \href{../exec/runtime.html#syntax-frame}{\mathit{frame}} : C\) |
Defaultability¶
Construct |
Judgement |
---|---|
\(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 |
---|---|
\(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}}}\) |
|
\(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 |
---|---|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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\) |
|
\(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 |
---|---|
\(\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\) |
|
\(\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\) |
|
\(\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\) |
|
\(\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\) |
|
\(\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\) |
|
\(\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\) |
|
\(\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\) |
|
\(\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\) |
|
\(\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 |
---|---|
\(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\) |
|
\(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}}'\) |