diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1dfebf2da..4a20a5950 100644 --- a/document/core/util/macros.def +++ b/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} diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index a4cb28d34..2b2a2e2b5 100644 --- a/document/core/valid/matching.rst +++ b/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: diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 3fd1de4b5..3c36dba8e 100644 --- a/document/core/valid/types.rst +++ b/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} diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index f635bd49b..4b5ba727a 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/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 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)*) diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec index 5325d2cc6..7e85e3d94 100644 --- a/specification/wasm-latest/2.1-validation.types.spectec +++ b/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: diff --git a/specification/wasm-latest/2.2-validation.subtyping.spectec b/specification/wasm-latest/2.2-validation.subtyping.spectec index a38d1f418..9bd60602f 100644 --- a/specification/wasm-latest/2.2-validation.subtyping.spectec +++ b/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,6 +180,13 @@ 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 @@ -186,7 +194,7 @@ rule Deftype_sub/refl: 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