[spec] Fix subtyping rules for bottom heaptypes

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}

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

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

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

spectec/test-frontend/TEST.md

@@ -2941,30 +2941,30 @@ 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*`}))
     -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_12*{t_12 <- `t_12*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`}))
 
 ;; ../../../../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)

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}]}