[spec] Syntax for descriptor types

document/core/util/macros.def

@@ -268,6 +268,8 @@
 .. |TSUB| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{sub}}
 .. |TREC| mathdef:: \xref{syntax/types}{syntax-rectype}{\K{rec}}
 .. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{final}}
+.. |TDESCRIBES| mathdef:: \xref{syntax/types}{syntax-desctype}{\K{describes}}
+.. |TDESCRIPTOR| mathdef:: \xref{syntax/types}{syntax-desctype}{\K{descriptor}}
 
 .. |TMUT| mathdef:: \xref{syntax/types}{syntax-mut}{\K{mut}}
 
@@ -301,6 +303,7 @@
 .. |fieldtype| mathdef:: \xref{syntax/types}{syntax-fieldtype}{\X{fieldtype}}
 .. |storagetype| mathdef:: \xref{syntax/types}{syntax-storagetype}{\X{storagetype}}
 .. |comptype| mathdef:: \xref{syntax/types}{syntax-comptype}{\X{comptype}}
+.. |desctype| mathdef:: \xref{syntax/types}{syntax-desctype}{\X{desctype}}
 .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}}
 .. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}}
 .. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}}
@@ -1177,6 +1180,7 @@
 .. |vdashfieldtype| mathdef:: \xref{valid/types}{valid-fieldtype}{\vdash}
 .. |vdashpacktype| mathdef:: \xref{valid/types}{valid-packtype}{\vdash}
 .. |vdashstoragetype| mathdef:: \xref{valid/types}{valid-storagetype}{\vdash}
+.. |vdashdesctype| mathdef:: \xref{valid/types}{valid-descype}{\vdash}
 .. |vdashsubtype| mathdef:: \xref{valid/types}{valid-subtype}{\vdash}
 .. |vdashsubtypeext| mathdef:: \xref{valid/types}{valid-subtype}{\vdash}
 .. |vdashrectype| mathdef:: \xref{valid/types}{valid-rectype}{\vdash}
@@ -1201,6 +1205,7 @@
 .. |OKfieldtype| mathdef:: \xref{valid/types}{valid-fieldtype}{\K{ok}}
 .. |OKpacktype| mathdef:: \xref{valid/types}{valid-packtype}{\K{ok}}
 .. |OKstoragetype| mathdef:: \xref{valid/types}{valid-storagetype}{\K{ok}}
+.. |OKdesctype| mathdef:: \xref{valid/types}{valid-desctype}{\K{ok}}
 .. |OKsubtype| mathdef:: \xref{valid/types}{valid-subtype}{\K{ok}}
 .. |OKsubtypeext| mathdef:: \xref{valid/types}{valid-subtype}{\K{ok}}
 .. |OKrectype| mathdef:: \xref{valid/types}{valid-rectype}{\K{ok}}
@@ -1227,6 +1232,7 @@
 .. |vdashstoragetypematch| mathdef:: \xref{valid/matching}{match-storagetype}{\vdash}
 .. |vdashpacktypematch| mathdef:: \xref{valid/matching}{match-packtype}{\vdash}
 .. |vdashcomptypematch| mathdef:: \xref{valid/matching}{match-comptype}{\vdash}
+.. |vdashdesctypematch| mathdef:: \xref{valid/matching}{match-desctype}{\vdash}
 .. |vdashdeftypematch| mathdef:: \xref{valid/matching}{match-deftype}{\vdash}
 .. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash}
 .. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash}
@@ -1246,6 +1252,7 @@
 .. |substoragetypematch| mathdef:: \xref{valid/matching}{match-storagetype}{\leq}
 .. |subpacktypematch| mathdef:: \xref{valid/matching}{match-packtype}{\leq}
 .. |subcomptypematch| mathdef:: \xref{valid/matching}{match-comptype}{\leq}
+.. |subdesctypematch| mathdef:: \xref{valid/matching}{match-desctype}{\leq}
 .. |subdeftypematch| mathdef:: \xref{valid/matching}{match-deftype}{\leq}
 .. |subtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\leq}
 .. |submemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\leq}

document/core/valid/matching.rst

@@ -143,6 +143,19 @@ $${rule-prose: Packtype_sub}
 $${rule: Packtype_sub}
 
 
+.. index:: descriptor type, describes, descriptor
+.. _match-desctype:
+
+Descriptor Types
+~~~~~~~~~~~~~~~~
+
+.. note:: TODO: Complete these rules.
+
+$${rule-prose: Desctype_sub}
+
+$${rule: Desctype_sub}
+
+
 .. index:: defined type, recursive type, unroll, type equivalence
    pair: abstract syntax; defined type
 .. _match-deftype:

document/core/valid/types.rst

@@ -189,7 +189,20 @@ $${rule-prose: Packtype_ok}
 $${rule: Packtype_ok}
 
 
-.. index:: recursive type, sub type, composite type, final, subtyping
+.. index:: descriptor type, describes, descriptor
+   pair: validation; descriptor type
+   single: abstract syntax; descriptor type
+.. _valid-desctype:
+
+Descriptor Types
+~~~~~~~~~~~~~~~~
+
+$${rule-prose: Desctype_ok}
+
+$${rule: Desctype_ok}
+
+
+.. index:: recursive type, sub type,final, subtyping
    pair: abstract syntax; recursive type
    pair: abstract syntax; sub type
 .. _valid-rectype:
@@ -208,7 +221,7 @@ $${rule-prose: Rectype_ok}
 $${rule: {Rectype_ok/empty Rectype_ok/cons}}
 
 
-:math:`\TSUB~\TFINAL^?~y^\ast~\comptype`
+:math:`\TSUB~\TFINAL^?~y^\ast~\desctype`
 ........................................
 
 $${rule-prose: Subtype_ok}

specification/wasm-latest/1.2-syntax.types.spectec

@@ -116,8 +116,15 @@ syntax comptype hint(desc "composite type") hint(macro "%" "T%") =
   | ARRAY fieldtype
   | FUNC resulttype -> resulttype
 
+syntax describes hint(show DESCRIBES %) hint(macro "%" "T%") = DESCRIBES typeuse
+syntax descriptor hint(show DESCRIPTOR %) hint(macro "%" "T%") = DESCRIPTOR typeuse
+
+syntax desctype hint(desc "descriptor type") =
+  | describes? descriptor? comptype
+  hint(show % % %)
+
 syntax subtype hint(desc "sub type") hint(macro "%" "T%") =
-  | SUB final? typeuse* comptype
+  | SUB final? typeuse* desctype
 
 syntax rectype hint(desc "recursive type") hint(macro "%" "T%") =
   | REC list(subtype)
@@ -162,6 +169,7 @@ var mt : memtype
 var nt : numtype
 var pt : packtype
 var rt : reftype
+var dct : desctype
 var st : subtype
 var tt : tabletype
 var vt : vectype
@@ -347,8 +355,11 @@ def $subst_valtype(valtype, typevar*, typeuse*) : valtype             hint(show
 def $subst_packtype(packtype, typevar*, typeuse*) : packtype          hint(show %#`[%:=%]) hint(macro "%subst")
 def $subst_storagetype(storagetype, typevar*, typeuse*) : storagetype hint(show %#`[%:=%]) hint(macro "%subst")
 def $subst_fieldtype(fieldtype, typevar*, typeuse*) : fieldtype       hint(show %#`[%:=%]) hint(macro "%subst")
+def $subst_describes(describes, typevar*, typeuse*) : describes       hint(show %#`[%:=%]) hint(macro "%subst")
+def $subst_descriptor(descriptor, typevar*, typeuse*) : descriptor    hint(show %#`[%:=%]) hint(macro "%subst")
 
 def $subst_comptype(comptype, typevar*, typeuse*) : comptype          hint(show %#`[%:=%]) hint(macro "%subst")
+def $subst_desctype(desctype, typevar*, typeuse*) : desctype          hint(show %#`[%:=%]) hint(macro "%subst")
 def $subst_subtype(subtype, typevar*, typeuse*) : subtype             hint(show %#`[%:=%]) hint(macro "%subst")
 def $subst_rectype(rectype, typevar*, typeuse*) : rectype             hint(show %#`[%:=%]) hint(macro "%subst")
 def $subst_deftype(deftype, typevar*, typeuse*) : deftype             hint(show %#`[%:=%]) hint(macro "%subst")
@@ -395,8 +406,14 @@ def $subst_comptype((STRUCT ft*), tv*, tu*) = STRUCT $subst_fieldtype(ft, tv*, t
 def $subst_comptype((ARRAY ft), tv*, tu*) = ARRAY $subst_fieldtype(ft, tv*, tu*)
 def $subst_comptype((FUNC t_1* -> t_2*), tv*, tu*) = FUNC $subst_valtype(t_1, tv*, tu*)* -> $subst_valtype(t_2, tv*, tu*)*
 
-def $subst_subtype((SUB final? tu'* ct), tv*, tu*) =
-  SUB final? $subst_typeuse(tu', tv*, tu*)* $subst_comptype(ct, tv*, tu*)
+def $subst_describes(DESCRIBES tu, tv*, tu*) = DESCRIBES $subst_typeuse(tu, tv*, tu*)
+def $subst_descriptor(DESCRIPTOR tu, tv*, tu*) = DESCRIPTOR $subst_typeuse(tu, tv*, tu*)
+
+def $subst_desctype(dc1? dc2? ct, tv*, tu*) =
+  $subst_describes(dc1, tv*, tu*)? $subst_descriptor(dc2, tv*, tu*)? $subst_comptype(ct, tv*, tu*)
+
+def $subst_subtype((SUB final? tu'* dct), tv*, tu*) =
+  SUB final? $subst_typeuse(tu', tv*, tu*)* $subst_desctype(dct, tv*, tu*)
 
 def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*)
 def $minus_recs(eps, eps) = (eps, eps)
@@ -459,6 +476,7 @@ def $rollrt(typeidx, rectype) : rectype  hint(show $roll_(%, %))   hint(macro "r
 def $unrollrt(rectype) : rectype         hint(show $unroll(%))     hint(macro "unrollrt")
 def $rolldt(typeidx, rectype) : deftype* hint(show $roll_(%)*#((%))) hint(macro "rolldt")
 def $unrolldt(deftype) : subtype         hint(show $unroll(%))     hint(macro "unrolldt")
+def $expanddt_to_desctype(deftype) : desctype  hint(show $expand_desc(%))
 def $expanddt(deftype) : comptype        hint(show $expand(%))     hint(macro "expanddt")
 
 def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ((_IDX $(x + i)))^(i<n), (REC i)^(i<n)))^n
@@ -469,7 +487,8 @@ def $unrollrt(rectype) = REC ($subst_subtype(subtype, (REC i)^(i<n), (_DEF recty
 def $rolldt(x, rectype) = (_DEF (REC subtype^n) i)^(i<n)  -- if $rollrt(x, rectype) = REC subtype^n
 def $unrolldt(_DEF rectype i) = subtype*[i]               -- if $unrollrt(rectype) = REC subtype*
 
-def $expanddt(deftype) = comptype                         -- if $unrolldt(deftype) = SUB final? typeuse* comptype
+def $expanddt_to_desctype(deftype) = dct                  -- if $unrolldt(deftype) = SUB final? typeuse* dct
+def $expanddt(deftype) = ct                               -- if $expanddt_to_desctype(deftype) = dc1? dc2? ct
 
 
 ;; Free indices
@@ -491,6 +510,9 @@ def $free_resulttype(resulttype) : free
 def $free_storagetype(storagetype) : free
 def $free_fieldtype(fieldtype) : free
 def $free_comptype(comptype) : free
+def $free_describes(describes) : free
+def $free_descriptor(descriptor) : free
+def $free_desctype(desctype) : free
 def $free_subtype(subtype) : free
 def $free_rectype(rectype) : free
 
@@ -550,8 +572,14 @@ def $free_comptype(STRUCT fieldtype*) = $free_list($free_fieldtype(fieldtype)*)
 def $free_comptype(ARRAY fieldtype) = $free_fieldtype(fieldtype)
 def $free_comptype(FUNC resulttype_1 -> resulttype_2) = $free_resulttype(resulttype_1) ++ $free_resulttype(resulttype_2)
 
-def $free_subtype(SUB final? typeuse* comptype) =
-  $free_list($free_typeuse(typeuse)*) ++ $free_comptype(comptype)
+def $free_describes(DESCRIBES tu) = $free_typeuse(tu)
+def $free_descriptor(DESCRIPTOR tu) = $free_typeuse(tu)
+
+def $free_desctype(dc1? dc2? ct) =
+  $free_list($free_describes(dc1)?) ++ $free_list($free_descriptor(dc2)?) ++ $free_comptype(ct)
+
+def $free_subtype(SUB final? typeuse* dct) =
+  $free_list($free_typeuse(typeuse)*) ++ $free_desctype(dct)
 
 def $free_rectype(REC subtype*) = $free_list($free_subtype(subtype)*)
 

specification/wasm-latest/2.1-validation.types.spectec

@@ -89,6 +89,7 @@ relation Packtype_ok: context |- packtype : OK          hint(name "K-pack")    h
 relation Fieldtype_ok: context |- fieldtype : OK        hint(name "K-field")   hint(macro "%fieldtype")
 relation Storagetype_ok: context |- storagetype : OK    hint(name "K-storage") hint(macro "%storagetype")
 relation Comptype_ok: context |- comptype : OK          hint(name "K-comp")    hint(macro "%comptype")
+relation Desctype_ok: context |- desctype : OK          hint(name "K-desc")    hint(macro "%desctype")
 relation Subtype_ok: context |- subtype : oktypeidx     hint(name "K-sub")     hint(macro "%subtype")     hint(prosepp "for")
 relation Rectype_ok: context |- rectype : oktypeidx     hint(name "K-rect")    hint(macro "%rectype")     hint(prosepp "for")
 relation Subtype_ok2: context |- subtype : oktypeidxnat hint(name "K-sub2")    hint(macro "%subtypeext")  hint(prosepp "for")
@@ -97,6 +98,7 @@ relation Deftype_ok: context |- deftype : OK            hint(name "K-def")     h
 
 ;; Forward declarations for validation.subtyping
 relation Comptype_sub: context |- comptype <: comptype  hint(name "S-comp")    hint(macro "%comptypematch")
+relation Desctype_sub: context |- desctype <: desctype  hint(name "S-desc")    hint(macro "%desctypematch")
 relation Deftype_sub: context |- deftype <: deftype     hint(name "S-def")     hint(macro "%deftypematch")
 
 
@@ -143,14 +145,21 @@ rule Comptype_ok/func:
   -- Resulttype_ok: C |- t_2* : OK
 
 
+rule Desctype_ok:
+  C |- (DESCRIBES tu_1)? (DESCRIPTOR tu_2)? ct : OK
+  -- (Typeuse_ok: C |- tu_1 : OK)?
+  -- (Typeuse_ok: C |- tu_2 : OK)?
+  -- Comptype_ok: C |- ct : OK
+
+
 rule Subtype_ok:
-  C |- SUB FINAL? (_IDX x)* comptype : OK(x_0)
+  C |- SUB FINAL? (_IDX x)* dct : OK(x_0)
   -- if |x*| <= 1
   -- (if x < x_0)*
-  -- (if $unrolldt(C.TYPES[x]) = SUB (_IDX x')* comptype')*
+  -- (if $unrolldt(C.TYPES[x]) = SUB (_IDX x')* dct')*
   ----
-  -- Comptype_ok: C |- comptype : OK
-  -- (Comptype_sub: C |- comptype <: comptype')*
+  -- Desctype_ok: C |- dct : OK
+  -- (Desctype_sub: C |- dct <: dct')*
 
 def $before(typeuse, typeidx, nat) : bool   hint(show % << %,%) hint(macro "before")
 def $before(deftype, x, i) = true
@@ -163,13 +172,13 @@ def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
 def $unrollht(C, REC i) = C.RECS[i]
 
 rule Subtype_ok2:
-  C |- SUB FINAL? typeuse* compttype : OK x i
+  C |- SUB FINAL? typeuse* desctype : OK x i
   -- if |typeuse*| <= 1
   -- (if $before(typeuse, x, i))*
-  -- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
+  -- (if $unrollht(C, typeuse) = SUB typeuse'* desctype')*
   ----
-  -- Comptype_ok: C |- comptype : OK
-  -- (Comptype_sub: C |- comptype <: comptype')*
+  -- Desctype_ok: C |- desctype : OK
+  -- (Desctype_sub: C |- desctype <: desctype')*
 
 
 rule Rectype_ok/empty:

specification/wasm-latest/2.2-validation.subtyping.spectec

@@ -68,7 +68,7 @@ rule Heaptype_sub/typeidx-r:
 
 rule Heaptype_sub/rec:
   C |- REC i <: typeuse*[j]
-  -- if C.RECS[i] = SUB final? typeuse* ct
+  -- if C.RECS[i] = SUB final? typeuse* desctype
 
 rule Heaptype_sub/none:
   C |- NONE <: heaptype
@@ -139,6 +139,7 @@ relation Storagetype_sub: context |- storagetype <: storagetype hint(name "S-sto
 relation Fieldtype_sub: context |- fieldtype <: fieldtype       hint(name "S-field")   hint(macro "%fieldtypematch")
 
 ;; Forward declared in validation.types
+;;relation Desctype_sub: context |- desctype <: desctype        hint(name "S-desc")    hint(macro "%desctypematch")
 ;;relation Comptype_sub: context |- comptype <: comptype        hint(name "S-comp")    hint(macro "%comptypematch")
 ;;relation Deftype_sub: context |- deftype <: deftype           hint(name "S-def")     hint(macro "%deftypematch")
 
@@ -179,14 +180,21 @@ rule Comptype_sub/func:
   -- Resulttype_sub: C |- t_21* <: t_11*
   -- Resulttype_sub: C |- t_12* <: t_22*
 
+;; TODO: Check descriptor square rules
+rule Desctype_sub:
+  C |- (DESCRIBES tu_11) (DESCRIPTOR tu_12) ct_1 <: (DESCRIBES tu_21) (DESCRIPTOR tu_22) ct_2
+  -- Heaptype_sub: C |- tu_11 <: tu_21
+  -- Heaptype_sub: C |- tu_12 <: tu_22
+  -- Comptype_sub: C |- ct_1 <: ct_2
+
 
 rule Deftype_sub/refl:
   C |- deftype_1 <: deftype_2
   -- if $clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2)
 
 rule Deftype_sub/super:
   C |- deftype_1 <: deftype_2
-  -- if $unrolldt(deftype_1) = SUB final? typeuse* ct
+  -- if $unrolldt(deftype_1) = SUB final? typeuse* desctype
   -- Heaptype_sub: C |- typeuse*[i] <: deftype_2