diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 2006287534..8a14069457 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -44,7 +44,7 @@ $${rule: {Heaptype_sub/struct Heaptype_sub/array Heaptype_sub/func} {Heaptype_sub/typeidx-l Heaptype_sub/typeidx-r} {Heaptype_sub/rec} - {Heaptype_sub/none Heaptype_sub/nofunc Heaptype_sub/noexn Heaptype_sub/noextern} + {Heaptype_sub/none Heaptype_sub/nofunc} {Heaptype_sub/noexn Heaptype_sub/noextern} {Heaptype_sub/bot} } $${rule-ignore: Heaptype_sub/def} diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index e82706478b..3e0ce830bc 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -83,10 +83,10 @@ let rec match_heaptype c t1 t2 = | I31HT, EqHT -> true | StructHT, EqHT -> true | ArrayHT, EqHT -> true - | NoneHT, t -> match_heaptype c t AnyHT - | NoFuncHT, t -> match_heaptype c t FuncHT - | NoExnHT, t -> match_heaptype c t ExnHT - | NoExternHT, t -> match_heaptype c t ExternHT + | NoneHT, t when t <> BotHT -> match_heaptype c t AnyHT + | NoFuncHT, t when t <> BotHT -> match_heaptype c t FuncHT + | NoExnHT, t when t <> BotHT -> match_heaptype c t ExnHT + | NoExternHT, t when t <> BotHT -> match_heaptype c t ExternHT | UseHT (Idx x1), _ -> match_heaptype c (UseHT (Def (lookup c x1))) t2 | _, UseHT (Idx x2) -> match_heaptype c t1 (UseHT (Def (lookup c x2))) | UseHT (Def dt1), UseHT (Def dt2) -> match_deftype c dt1 dt2 diff --git a/specification/wasm-3.0/2.2-validation.subtyping.spectec b/specification/wasm-3.0/2.2-validation.subtyping.spectec index 3c2aead035..7940772239 100644 --- a/specification/wasm-3.0/2.2-validation.subtyping.spectec +++ b/specification/wasm-3.0/2.2-validation.subtyping.spectec @@ -69,18 +69,22 @@ rule Heaptype_sub/rec: rule Heaptype_sub/none: C |- NONE <: heaptype -- Heaptype_sub: C |- heaptype <: ANY + -- if heaptype =/= BOT rule Heaptype_sub/nofunc: C |- NOFUNC <: heaptype -- Heaptype_sub: C |- heaptype <: FUNC + -- if heaptype =/= BOT rule Heaptype_sub/noexn: C |- NOEXN <: heaptype -- Heaptype_sub: C |- heaptype <: EXN + -- if heaptype =/= BOT rule Heaptype_sub/noextern: C |- NOEXTERN <: heaptype -- Heaptype_sub: C |- heaptype <: EXTERN + -- if heaptype =/= BOT rule Heaptype_sub/bot: C |- BOT <: heaptype diff --git a/specification/wasm-latest/2.2-validation.subtyping.spectec b/specification/wasm-latest/2.2-validation.subtyping.spectec index 3c2aead035..7940772239 100644 --- a/specification/wasm-latest/2.2-validation.subtyping.spectec +++ b/specification/wasm-latest/2.2-validation.subtyping.spectec @@ -69,18 +69,22 @@ rule Heaptype_sub/rec: rule Heaptype_sub/none: C |- NONE <: heaptype -- Heaptype_sub: C |- heaptype <: ANY + -- if heaptype =/= BOT rule Heaptype_sub/nofunc: C |- NOFUNC <: heaptype -- Heaptype_sub: C |- heaptype <: FUNC + -- if heaptype =/= BOT rule Heaptype_sub/noexn: C |- NOEXN <: heaptype -- Heaptype_sub: C |- heaptype <: EXN + -- if heaptype =/= BOT rule Heaptype_sub/noextern: C |- NOEXTERN <: heaptype -- Heaptype_sub: C |- heaptype <: EXTERN + -- if heaptype =/= BOT rule Heaptype_sub/bot: C |- BOT <: heaptype diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 55a94fd237..772ae3066b 100644 Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index fd20528ef7..f31ebb4d67 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -2941,17 +2941,17 @@ relation Deftype_ok: `%|-%:OK`(context, deftype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.108 relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:165.1-167.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.41 rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}: `%|-%<:%`(C, STRUCT_comptype(`%`_list(ft_1*{ft_1 <- `ft_1*`} ++ ft'_1*{ft'_1 <- `ft'_1*`})), STRUCT_comptype(`%`_list(ft_2*{ft_2 <- `ft_2*`}))) -- (Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2))*{ft_1 <- `ft_1*`, ft_2 <- `ft_2*`} - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.38 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-175.38 rule array{C : context, ft_1 : fieldtype, ft_2 : fieldtype}: `%|-%<:%`(C, ARRAY_comptype(ft_1), ARRAY_comptype(ft_2)) -- Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-176.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:177.1-180.41 rule func{C : context, `t_11*` : valtype*, `t_12*` : valtype*, `t_21*` : valtype*, `t_22*` : valtype*}: `%|-%<:%`(C, `FUNC%->%`_comptype(`%`_resulttype(t_11*{t_11 <- `t_11*`}), `%`_resulttype(t_12*{t_12 <- `t_12*`})), `FUNC%->%`_comptype(`%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`}))) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`})) @@ -2959,12 +2959,12 @@ relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.107 relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:179.1-181.66 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-185.66 rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-186.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:187.1-190.49 rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, `final?` : final?, `typeuse*` : typeuse*, ct : comptype, i : nat}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($unrolldt(deftype_1) = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) @@ -3034,90 +3034,94 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) `%|-%<:%`(C, REC_heaptype(i), (typeuse*{typeuse <- `typeuse*`}[j] : typeuse <: heaptype)) -- if (C.RECS_context[i] = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-71.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-72.25 rule none{C : context, heaptype : heaptype}: `%|-%<:%`(C, NONE_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, ANY_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:73.1-75.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:74.1-77.25 rule nofunc{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOFUNC_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, FUNC_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:77.1-79.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:79.1-82.25 rule noexn{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:81.1-83.43 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:84.1-87.25 rule noextern{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXTERN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXTERN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:85.1-86.23 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-90.23 rule bot{C : context, heaptype : heaptype}: `%|-%<:%`(C, BOT_heaptype, heaptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:10.1-10.103 relation Reftype_sub: `%|-%<:%`(context, reftype, reftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-91.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 rule nonnull{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(?(), ht_1), REF_reftype(?(), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:97.1-99.37 rule null{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(NULL_null?{}, ht_1), REF_reftype(?(NULL_null), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:11.1-11.103 relation Valtype_sub: `%|-%<:%`(context, valtype, valtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:98.1-100.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 rule num{C : context, numtype_1 : numtype, numtype_2 : numtype}: `%|-%<:%`(C, (numtype_1 : numtype <: valtype), (numtype_2 : numtype <: valtype)) -- Numtype_sub: `%|-%<:%`(C, numtype_1, numtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 rule vec{C : context, vectype_1 : vectype, vectype_2 : vectype}: `%|-%<:%`(C, (vectype_1 : vectype <: valtype), (vectype_2 : vectype <: valtype)) -- Vectype_sub: `%|-%<:%`(C, vectype_1, vectype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-112.46 rule ref{C : context, reftype_1 : reftype, reftype_2 : reftype}: `%|-%<:%`(C, (reftype_1 : reftype <: valtype), (reftype_2 : reftype <: valtype)) -- Reftype_sub: `%|-%<:%`(C, reftype_1, reftype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-111.22 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:114.1-115.22 rule bot{C : context, valtype : valtype}: `%|-%<:%`(C, BOT_valtype, valtype) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:116.1-116.115 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:120.1-120.115 relation Resulttype_sub: `%|-%<:%`(context, resulttype, resulttype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:119.1-121.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:123.1-125.37 rule _{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%<:%`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`})) -- (Valtype_sub: `%|-%<:%`(C, t_1, t_2))*{t_1 <- `t_1*`, t_2 <- `t_2*`} -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:134.1-134.119 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:138.1-138.119 relation Storagetype_sub: `%|-%<:%`(context, storagetype, storagetype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:146.1-148.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.46 rule val{C : context, valtype_1 : valtype, valtype_2 : valtype}: `%|-%<:%`(C, (valtype_1 : valtype <: storagetype), (valtype_2 : valtype <: storagetype)) -- Valtype_sub: `%|-%<:%`(C, valtype_1, valtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:154.1-156.49 rule pack{C : context, packtype_1 : packtype, packtype_2 : packtype}: `%|-%<:%`(C, (packtype_1 : packtype <: storagetype), (packtype_2 : packtype <: storagetype)) -- Packtype_sub: `%|-%<:%`(C, packtype_1, packtype_2) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:135.1-135.117 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:139.1-139.117 relation Fieldtype_sub: `%|-%<:%`(context, fieldtype, fieldtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:155.1-157.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-161.40 rule const{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(), zt_1), `%%`_fieldtype(?(), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-162.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:163.1-166.40 rule var{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(MUT_mut), zt_1), `%%`_fieldtype(?(MUT_mut), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index aa7136b61d..e917bf6722 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -5341,6 +5341,8 @@ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ C \vdash {\mathit{heaptype}} \leq \mathsf{any} + \qquad +{\mathit{heaptype}} \neq \mathsf{bot} }{ C \vdash \mathsf{none} \leq {\mathit{heaptype}} } \, {[\textsc{\scriptsize S{-}heap{-}none}]} @@ -5352,6 +5354,8 @@ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ C \vdash {\mathit{heaptype}} \leq \mathsf{func} + \qquad +{\mathit{heaptype}} \neq \mathsf{bot} }{ C \vdash \mathsf{nofunc} \leq {\mathit{heaptype}} } \, {[\textsc{\scriptsize S{-}heap{-}nofunc}]} @@ -5363,6 +5367,8 @@ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ C \vdash {\mathit{heaptype}} \leq \mathsf{exn} + \qquad +{\mathit{heaptype}} \neq \mathsf{bot} }{ C \vdash \mathsf{noexn} \leq {\mathit{heaptype}} } \, {[\textsc{\scriptsize S{-}heap{-}noexn}]} @@ -5374,6 +5380,8 @@ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ C \vdash {\mathit{heaptype}} \leq \mathsf{extern} + \qquad +{\mathit{heaptype}} \neq \mathsf{bot} }{ C \vdash \mathsf{noextern} \leq {\mathit{heaptype}} } \, {[\textsc{\scriptsize S{-}heap{-}noextern}]} diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 0a4552419a..9fb823c64c 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -2931,17 +2931,17 @@ relation Deftype_ok: `%|-%:OK`(context, deftype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.108 relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:165.1-167.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.41 rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}: `%|-%<:%`(C, STRUCT_comptype(`%`_list(ft_1*{ft_1 <- `ft_1*`} ++ ft'_1*{ft'_1 <- `ft'_1*`})), STRUCT_comptype(`%`_list(ft_2*{ft_2 <- `ft_2*`}))) -- (Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2))*{ft_1 <- `ft_1*`, ft_2 <- `ft_2*`} - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.38 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-175.38 rule array{C : context, ft_1 : fieldtype, ft_2 : fieldtype}: `%|-%<:%`(C, ARRAY_comptype(ft_1), ARRAY_comptype(ft_2)) -- Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-176.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:177.1-180.41 rule func{C : context, `t_11*` : valtype*, `t_12*` : valtype*, `t_21*` : valtype*, `t_22*` : valtype*}: `%|-%<:%`(C, `FUNC%->%`_comptype(`%`_resulttype(t_11*{t_11 <- `t_11*`}), `%`_resulttype(t_12*{t_12 <- `t_12*`})), `FUNC%->%`_comptype(`%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`}))) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`})) @@ -2949,12 +2949,12 @@ relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.107 relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:179.1-181.66 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-185.66 rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-186.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:187.1-190.49 rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, `final?` : final?, `typeuse*` : typeuse*, ct : comptype, i : nat}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($unrolldt(deftype_1) = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) @@ -3024,90 +3024,94 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) `%|-%<:%`(C, REC_heaptype(i), (typeuse*{typeuse <- `typeuse*`}[j] : typeuse <: heaptype)) -- if (C.RECS_context[i] = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-71.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-72.25 rule none{C : context, heaptype : heaptype}: `%|-%<:%`(C, NONE_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, ANY_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:73.1-75.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:74.1-77.25 rule nofunc{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOFUNC_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, FUNC_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:77.1-79.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:79.1-82.25 rule noexn{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:81.1-83.43 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:84.1-87.25 rule noextern{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXTERN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXTERN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:85.1-86.23 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-90.23 rule bot{C : context, heaptype : heaptype}: `%|-%<:%`(C, BOT_heaptype, heaptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:10.1-10.103 relation Reftype_sub: `%|-%<:%`(context, reftype, reftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-91.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 rule nonnull{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(?(), ht_1), REF_reftype(?(), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:97.1-99.37 rule null{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(NULL_null?{}, ht_1), REF_reftype(?(NULL_null), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:11.1-11.103 relation Valtype_sub: `%|-%<:%`(context, valtype, valtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:98.1-100.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 rule num{C : context, numtype_1 : numtype, numtype_2 : numtype}: `%|-%<:%`(C, (numtype_1 : numtype <: valtype), (numtype_2 : numtype <: valtype)) -- Numtype_sub: `%|-%<:%`(C, numtype_1, numtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 rule vec{C : context, vectype_1 : vectype, vectype_2 : vectype}: `%|-%<:%`(C, (vectype_1 : vectype <: valtype), (vectype_2 : vectype <: valtype)) -- Vectype_sub: `%|-%<:%`(C, vectype_1, vectype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-112.46 rule ref{C : context, reftype_1 : reftype, reftype_2 : reftype}: `%|-%<:%`(C, (reftype_1 : reftype <: valtype), (reftype_2 : reftype <: valtype)) -- Reftype_sub: `%|-%<:%`(C, reftype_1, reftype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-111.22 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:114.1-115.22 rule bot{C : context, valtype : valtype}: `%|-%<:%`(C, BOT_valtype, valtype) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:116.1-116.115 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:120.1-120.115 relation Resulttype_sub: `%|-%<:%`(context, resulttype, resulttype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:119.1-121.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:123.1-125.37 rule _{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%<:%`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`})) -- (Valtype_sub: `%|-%<:%`(C, t_1, t_2))*{t_1 <- `t_1*`, t_2 <- `t_2*`} -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:134.1-134.119 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:138.1-138.119 relation Storagetype_sub: `%|-%<:%`(context, storagetype, storagetype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:146.1-148.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.46 rule val{C : context, valtype_1 : valtype, valtype_2 : valtype}: `%|-%<:%`(C, (valtype_1 : valtype <: storagetype), (valtype_2 : valtype <: storagetype)) -- Valtype_sub: `%|-%<:%`(C, valtype_1, valtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:154.1-156.49 rule pack{C : context, packtype_1 : packtype, packtype_2 : packtype}: `%|-%<:%`(C, (packtype_1 : packtype <: storagetype), (packtype_2 : packtype <: storagetype)) -- Packtype_sub: `%|-%<:%`(C, packtype_1, packtype_2) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:135.1-135.117 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:139.1-139.117 relation Fieldtype_sub: `%|-%<:%`(context, fieldtype, fieldtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:155.1-157.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-161.40 rule const{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(), zt_1), `%%`_fieldtype(?(), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-162.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:163.1-166.40 rule var{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(MUT_mut), zt_1), `%%`_fieldtype(?(MUT_mut), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) @@ -14346,17 +14350,17 @@ relation Deftype_ok: `%|-%:OK`(context, deftype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.108 relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:165.1-167.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.41 rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}: `%|-%<:%`(C, STRUCT_comptype(`%`_list(ft_1*{ft_1 <- `ft_1*`} ++ ft'_1*{ft'_1 <- `ft'_1*`})), STRUCT_comptype(`%`_list(ft_2*{ft_2 <- `ft_2*`}))) -- (Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2))*{ft_1 <- `ft_1*`, ft_2 <- `ft_2*`} - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.38 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-175.38 rule array{C : context, ft_1 : fieldtype, ft_2 : fieldtype}: `%|-%<:%`(C, ARRAY_comptype(ft_1), ARRAY_comptype(ft_2)) -- Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-176.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:177.1-180.41 rule func{C : context, `t_11*` : valtype*, `t_12*` : valtype*, `t_21*` : valtype*, `t_22*` : valtype*}: `%|-%<:%`(C, `FUNC%->%`_comptype(`%`_resulttype(t_11*{t_11 <- `t_11*`}), `%`_resulttype(t_12*{t_12 <- `t_12*`})), `FUNC%->%`_comptype(`%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`}))) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`})) @@ -14364,12 +14368,12 @@ relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.107 relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:179.1-181.66 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-185.66 rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-186.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:187.1-190.49 rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, `final?` : final?, `typeuse*` : typeuse*, ct : comptype, i : nat}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($unrolldt(deftype_1) = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) @@ -14439,90 +14443,94 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) `%|-%<:%`(C, REC_heaptype(i), (typeuse*{typeuse <- `typeuse*`}[j] : typeuse <: heaptype)) -- if (C.RECS_context[i] = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-71.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-72.25 rule none{C : context, heaptype : heaptype}: `%|-%<:%`(C, NONE_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, ANY_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:73.1-75.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:74.1-77.25 rule nofunc{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOFUNC_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, FUNC_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:77.1-79.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:79.1-82.25 rule noexn{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:81.1-83.43 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:84.1-87.25 rule noextern{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXTERN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXTERN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:85.1-86.23 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-90.23 rule bot{C : context, heaptype : heaptype}: `%|-%<:%`(C, BOT_heaptype, heaptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:10.1-10.103 relation Reftype_sub: `%|-%<:%`(context, reftype, reftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-91.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 rule nonnull{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(?(), ht_1), REF_reftype(?(), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:97.1-99.37 rule null{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(NULL_null?{}, ht_1), REF_reftype(?(NULL_null), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:11.1-11.103 relation Valtype_sub: `%|-%<:%`(context, valtype, valtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:98.1-100.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 rule num{C : context, numtype_1 : numtype, numtype_2 : numtype}: `%|-%<:%`(C, (numtype_1 : numtype <: valtype), (numtype_2 : numtype <: valtype)) -- Numtype_sub: `%|-%<:%`(C, numtype_1, numtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 rule vec{C : context, vectype_1 : vectype, vectype_2 : vectype}: `%|-%<:%`(C, (vectype_1 : vectype <: valtype), (vectype_2 : vectype <: valtype)) -- Vectype_sub: `%|-%<:%`(C, vectype_1, vectype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-112.46 rule ref{C : context, reftype_1 : reftype, reftype_2 : reftype}: `%|-%<:%`(C, (reftype_1 : reftype <: valtype), (reftype_2 : reftype <: valtype)) -- Reftype_sub: `%|-%<:%`(C, reftype_1, reftype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-111.22 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:114.1-115.22 rule bot{C : context, valtype : valtype}: `%|-%<:%`(C, BOT_valtype, valtype) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:116.1-116.115 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:120.1-120.115 relation Resulttype_sub: `%|-%<:%`(context, resulttype, resulttype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:119.1-121.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:123.1-125.37 rule _{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%<:%`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`})) -- (Valtype_sub: `%|-%<:%`(C, t_1, t_2))*{t_1 <- `t_1*`, t_2 <- `t_2*`} -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:134.1-134.119 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:138.1-138.119 relation Storagetype_sub: `%|-%<:%`(context, storagetype, storagetype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:146.1-148.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.46 rule val{C : context, valtype_1 : valtype, valtype_2 : valtype}: `%|-%<:%`(C, (valtype_1 : valtype <: storagetype), (valtype_2 : valtype <: storagetype)) -- Valtype_sub: `%|-%<:%`(C, valtype_1, valtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:154.1-156.49 rule pack{C : context, packtype_1 : packtype, packtype_2 : packtype}: `%|-%<:%`(C, (packtype_1 : packtype <: storagetype), (packtype_2 : packtype <: storagetype)) -- Packtype_sub: `%|-%<:%`(C, packtype_1, packtype_2) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:135.1-135.117 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:139.1-139.117 relation Fieldtype_sub: `%|-%<:%`(context, fieldtype, fieldtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:155.1-157.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-161.40 rule const{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(), zt_1), `%%`_fieldtype(?(), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-162.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:163.1-166.40 rule var{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(MUT_mut), zt_1), `%%`_fieldtype(?(MUT_mut), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) @@ -25770,18 +25778,18 @@ relation Deftype_ok: `%|-%:OK`(context, deftype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.108 relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:165.1-167.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.41 rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}: `%|-%<:%`(C, STRUCT_comptype(`%`_list(ft_1*{ft_1 <- `ft_1*`} ++ ft'_1*{ft'_1 <- `ft'_1*`})), STRUCT_comptype(`%`_list(ft_2*{ft_2 <- `ft_2*`}))) -- if (|`ft_1*`| = |`ft_2*`|) -- (Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2))*{ft_1 <- `ft_1*`, ft_2 <- `ft_2*`} - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.38 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-175.38 rule array{C : context, ft_1 : fieldtype, ft_2 : fieldtype}: `%|-%<:%`(C, ARRAY_comptype(ft_1), ARRAY_comptype(ft_2)) -- Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-176.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:177.1-180.41 rule func{C : context, `t_11*` : valtype*, `t_12*` : valtype*, `t_21*` : valtype*, `t_22*` : valtype*}: `%|-%<:%`(C, `FUNC%->%`_comptype(`%`_resulttype(t_11*{t_11 <- `t_11*`}), `%`_resulttype(t_12*{t_12 <- `t_12*`})), `FUNC%->%`_comptype(`%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`}))) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`})) @@ -25789,12 +25797,12 @@ relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.107 relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:179.1-181.66 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-185.66 rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-186.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:187.1-190.49 rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, `final?` : final?, `typeuse*` : typeuse*, ct : comptype, i : nat}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($unrolldt(deftype_1) = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) @@ -25869,91 +25877,95 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) -- if (i < |C.RECS_context|) -- if (C.RECS_context[i] = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-71.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-72.25 rule none{C : context, heaptype : heaptype}: `%|-%<:%`(C, NONE_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, ANY_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:73.1-75.41 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:74.1-77.25 rule nofunc{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOFUNC_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, FUNC_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:77.1-79.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:79.1-82.25 rule noexn{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:81.1-83.43 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:84.1-87.25 rule noextern{C : context, heaptype : heaptype}: `%|-%<:%`(C, NOEXTERN_heaptype, heaptype) -- Heaptype_sub: `%|-%<:%`(C, heaptype, EXTERN_heaptype) + -- if (heaptype =/= BOT_heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:85.1-86.23 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-90.23 rule bot{C : context, heaptype : heaptype}: `%|-%<:%`(C, BOT_heaptype, heaptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:10.1-10.103 relation Reftype_sub: `%|-%<:%`(context, reftype, reftype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-91.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 rule nonnull{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(?(), ht_1), REF_reftype(?(), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:97.1-99.37 rule null{C : context, ht_1 : heaptype, ht_2 : heaptype}: `%|-%<:%`(C, REF_reftype(NULL_null?{}, ht_1), REF_reftype(?(NULL_null), ht_2)) -- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:11.1-11.103 relation Valtype_sub: `%|-%<:%`(context, valtype, valtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:98.1-100.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 rule num{C : context, numtype_1 : numtype, numtype_2 : numtype}: `%|-%<:%`(C, (numtype_1 : numtype <: valtype), (numtype_2 : numtype <: valtype)) -- Numtype_sub: `%|-%<:%`(C, numtype_1, numtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 rule vec{C : context, vectype_1 : vectype, vectype_2 : vectype}: `%|-%<:%`(C, (vectype_1 : vectype <: valtype), (vectype_2 : vectype <: valtype)) -- Vectype_sub: `%|-%<:%`(C, vectype_1, vectype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-112.46 rule ref{C : context, reftype_1 : reftype, reftype_2 : reftype}: `%|-%<:%`(C, (reftype_1 : reftype <: valtype), (reftype_2 : reftype <: valtype)) -- Reftype_sub: `%|-%<:%`(C, reftype_1, reftype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-111.22 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:114.1-115.22 rule bot{C : context, valtype : valtype}: `%|-%<:%`(C, BOT_valtype, valtype) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:116.1-116.115 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:120.1-120.115 relation Resulttype_sub: `%|-%<:%`(context, resulttype, resulttype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:119.1-121.37 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:123.1-125.37 rule _{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%<:%`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`})) -- if (|`t_1*`| = |`t_2*`|) -- (Valtype_sub: `%|-%<:%`(C, t_1, t_2))*{t_1 <- `t_1*`, t_2 <- `t_2*`} -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:134.1-134.119 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:138.1-138.119 relation Storagetype_sub: `%|-%<:%`(context, storagetype, storagetype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:146.1-148.46 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.46 rule val{C : context, valtype_1 : valtype, valtype_2 : valtype}: `%|-%<:%`(C, (valtype_1 : valtype <: storagetype), (valtype_2 : valtype <: storagetype)) -- Valtype_sub: `%|-%<:%`(C, valtype_1, valtype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:154.1-156.49 rule pack{C : context, packtype_1 : packtype, packtype_2 : packtype}: `%|-%<:%`(C, (packtype_1 : packtype <: storagetype), (packtype_2 : packtype <: storagetype)) -- Packtype_sub: `%|-%<:%`(C, packtype_1, packtype_2) -;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:135.1-135.117 +;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:139.1-139.117 relation Fieldtype_sub: `%|-%<:%`(context, fieldtype, fieldtype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:155.1-157.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-161.40 rule const{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(), zt_1), `%%`_fieldtype(?(), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-162.40 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:163.1-166.40 rule var{C : context, zt_1 : storagetype, zt_2 : storagetype}: `%|-%<:%`(C, `%%`_fieldtype(?(MUT_mut), zt_1), `%%`_fieldtype(?(MUT_mut), zt_2)) -- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 7f19a5e8f6..7c98571b8f 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -14347,21 +14347,29 @@ The heap type :math:`{\mathit{heaptype}}_1` :ref:`matches ` the heap type * The heap type :math:`{\mathit{heaptype}}_1` is of the form :math:`\mathsf{none}`. * The heap type :math:`{\mathit{heaptype}}_2` :ref:`matches ` the heap type :math:`\mathsf{any}`. + + * The heap type :math:`{\mathit{heaptype}}_2` is not of the form :math:`\mathsf{bot}`. * Or: * The heap type :math:`{\mathit{heaptype}}_1` is of the form :math:`\mathsf{nofunc}`. * The heap type :math:`{\mathit{heaptype}}_2` :ref:`matches ` the heap type :math:`\mathsf{func}`. + + * The heap type :math:`{\mathit{heaptype}}_2` is not of the form :math:`\mathsf{bot}`. * Or: * The heap type :math:`{\mathit{heaptype}}_1` is of the form :math:`\mathsf{noexn}`. * The heap type :math:`{\mathit{heaptype}}_2` :ref:`matches ` the heap type :math:`\mathsf{exn}`. + + * The heap type :math:`{\mathit{heaptype}}_2` is not of the form :math:`\mathsf{bot}`. * Or: * The heap type :math:`{\mathit{heaptype}}_1` is of the form :math:`\mathsf{noextern}`. * The heap type :math:`{\mathit{heaptype}}_2` :ref:`matches ` the heap type :math:`\mathsf{extern}`. + + * The heap type :math:`{\mathit{heaptype}}_2` is not of the form :math:`\mathsf{bot}`. * Or: * The heap type :math:`{\mathit{heaptype}}_1` is of the form :math:`\mathsf{bot}`. @@ -14475,6 +14483,8 @@ The heap type :math:`\mathsf{none}` :ref:`matches ` the heap type :math:` * The heap type :math:`{\mathit{heaptype}}` :ref:`matches ` the heap type :math:`\mathsf{any}`. + * The heap type :math:`{\mathit{heaptype}}` is not of the form :math:`\mathsf{bot}`. + @@ -14483,6 +14493,8 @@ The heap type :math:`\mathsf{nofunc}` :ref:`matches ` the heap type :math * The heap type :math:`{\mathit{heaptype}}` :ref:`matches ` the heap type :math:`\mathsf{func}`. + * The heap type :math:`{\mathit{heaptype}}` is not of the form :math:`\mathsf{bot}`. + @@ -14491,6 +14503,8 @@ The heap type :math:`\mathsf{noexn}` :ref:`matches ` the heap type :math: * The heap type :math:`{\mathit{heaptype}}` :ref:`matches ` the heap type :math:`\mathsf{exn}`. + * The heap type :math:`{\mathit{heaptype}}` is not of the form :math:`\mathsf{bot}`. + @@ -14499,6 +14513,8 @@ The heap type :math:`\mathsf{noextern}` :ref:`matches ` the heap type :ma * The heap type :math:`{\mathit{heaptype}}` :ref:`matches ` the heap type :math:`\mathsf{extern}`. + * The heap type :math:`{\mathit{heaptype}}` is not of the form :math:`\mathsf{bot}`. + @@ -27151,15 +27167,19 @@ Heaptype_sub - Or: - heaptype_1 is NONE. - heaptype_2 matches the heap type ANY. + - heaptype_2 is not BOT. - Or: - heaptype_1 is NOFUNC. - heaptype_2 matches the heap type FUNC. + - heaptype_2 is not BOT. - Or: - heaptype_1 is NOEXN. - heaptype_2 matches the heap type EXN. + - heaptype_2 is not BOT. - Or: - heaptype_1 is NOEXTERN. - heaptype_2 matches the heap type EXTERN. + - heaptype_2 is not BOT. - Or: - heaptype_1 is BOT. @@ -27219,18 +27239,22 @@ Heaptype_sub/rec Heaptype_sub/none - the heap type NONE matches the heap type heaptype if: - heaptype matches the heap type ANY. + - heaptype is not BOT. Heaptype_sub/nofunc - the heap type NOFUNC matches the heap type heaptype if: - heaptype matches the heap type FUNC. + - heaptype is not BOT. Heaptype_sub/noexn - the heap type NOEXN matches the heap type heaptype if: - heaptype matches the heap type EXN. + - heaptype is not BOT. Heaptype_sub/noextern - the heap type NOEXTERN matches the heap type heaptype if: - heaptype matches the heap type EXTERN. + - heaptype is not BOT. Heaptype_sub/bot - the heap type BOT matches heaptype. diff --git a/test/core/gc/type-subtyping.wast b/test/core/gc/type-subtyping.wast index c48669ed5e..41ac0cf7a7 100644 --- a/test/core/gc/type-subtyping.wast +++ b/test/core/gc/type-subtyping.wast @@ -224,6 +224,60 @@ ) +;; Invalid abstract subtyping + +(assert_invalid + (module (func (param (ref null nofunc)) (result (ref null none)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null nofunc)) (result (ref null any)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null none)) (result (ref null nofunc)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null none)) (result (ref null func)) (local.get 0))) + "type mismatch" +) + +(assert_invalid + (module (func (param (ref null none)) (result (ref null noextern)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null none)) (result (ref null extern)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null noextern)) (result (ref null none)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null noextern)) (result (ref null any)) (local.get 0))) + "type mismatch" +) + +(assert_invalid + (module (func (param (ref null nofunc)) (result (ref null noextern)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null nofunc)) (result (ref null extern)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null noextern)) (result (ref null nofunc)) (local.get 0))) + "type mismatch" +) +(assert_invalid + (module (func (param (ref null noextern)) (result (ref null func)) (local.get 0))) + "type mismatch" +) + + ;; Runtime types (module @@ -757,7 +811,6 @@ ) - ;; Invalid subtyping definitions (assert_invalid