语义规则索引

静态构造的类型化

构造	判断
限制	$⊢\mathit{limits}:k$
函数类型	$⊢\mathit{functype}\text{ok}$
块类型	$⊢\mathit{blocktype}\text{ok}$
表类型	$⊢\mathit{tabletype}\text{ok}$
内存类型	$⊢\mathit{memtype}\text{ok}$
全局类型	$⊢\mathit{globaltype}\text{ok}$
外部类型	$⊢\mathit{externtype}\text{ok}$
指令	$S;C⊢\mathit{instr}:\mathit{stacktype}$
指令序列	$S;C⊢{\mathit{instr}}^{\ast }:\mathit{stacktype}$
表达式	$C⊢\mathit{expr}:\mathit{resulttype}$
函数	$C⊢\mathit{func}:\mathit{functype}$
表	$C⊢\mathit{table}:\mathit{tabletype}$
内存	$C⊢\mathit{mem}:\mathit{memtype}$
全局	$C⊢\mathit{global}:\mathit{globaltype}$
元素段	$C⊢\mathit{elem}:\mathit{reftype}$
元素模式	$C⊢\mathit{elemmode}:\mathit{reftype}$
数据段	$C⊢\mathit{data}\text{ok}$
数据模式	$C⊢\mathit{datamode}\text{ok}$
开始函数	$C⊢\mathit{start}\text{ok}$
导出	$C⊢\mathit{export}:\mathit{externtype}$
导出描述	$C⊢\mathit{exportdesc}:\mathit{externtype}$
导入	$C⊢\mathit{import}:\mathit{externtype}$
导入描述	$C⊢\mathit{importdesc}:\mathit{externtype}$
模块	$⊢\mathit{module}:{\mathit{externtype}}^{\ast }\to {\mathit{externtype}}^{\ast }$

运行时构造的类型化

构造	判断
值	$S⊢\mathit{val}:\mathit{valtype}$
结果	$S⊢\mathit{result}:\mathit{resulttype}$
外部值	$S⊢\mathit{externval}:\mathit{externtype}$
函数实例	$S⊢\mathit{funcinst}:\mathit{functype}$
表实例	$S⊢\mathit{tableinst}:\mathit{tabletype}$
内存实例	$S⊢\mathit{meminst}:\mathit{memtype}$
全局实例	$S⊢\mathit{globalinst}:\mathit{globaltype}$
元素实例	$S⊢\mathit{eleminst}:t$
数据实例	$S⊢\mathit{datainst}\text{ok}$
导出实例	$S⊢\mathit{exportinst}\text{ok}$
模块实例	$S⊢\mathit{moduleinst}:C$
存储	$⊢\mathit{store}\text{ok}$
配置	$⊢\mathit{config}\text{ok}$
线程	$S;{\mathit{resulttype}}^{?}⊢\mathit{thread}:\mathit{resulttype}$
帧	$S⊢\mathit{frame}:C$

常量性

构造	判断
常量表达式	$C⊢\mathit{expr}\text{const}$
常量指令	$C⊢\mathit{instr}\text{const}$

匹配

构造	判断
外部类型	$⊢{\mathit{externtype}}_1\le {\mathit{externtype}}_2$
限制	$⊢{\mathit{limits}}_1\le {\mathit{limits}}_2$

存储扩展

构造	判断
函数实例	$⊢{\mathit{funcinst}}_1⪯{\mathit{funcinst}}_2$
表实例	$⊢{\mathit{tableinst}}_1⪯{\mathit{tableinst}}_2$
内存实例	$⊢{\mathit{meminst}}_1⪯{\mathit{meminst}}_2$
全局实例	$⊢{\mathit{globalinst}}_1⪯{\mathit{globalinst}}_2$
元素实例	$⊢{\mathit{eleminst}}_1⪯{\mathit{eleminst}}_2$
数据实例	$⊢{\mathit{datainst}}_1⪯{\mathit{datainst}}_2$
存储	$⊢{\mathit{store}}_1⪯{\mathit{store}}_2$

执行

构造	判断
指令	$S;F;{\mathit{instr}}^{\ast }\hookrightarrow S^{\prime };F^{\prime };{{\mathit{instr}}^{\prime }}^{\ast }$
表达式	$S;F;\mathit{expr}\hookrightarrow S^{\prime };F^{\prime };{\mathit{expr}}^{\prime }$