From 2ca8cdd96bcd3db89f33ca8ca86ae4ca7625988a Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 7 Jul 2026 18:35:22 -0700 Subject: [PATCH 1/2] Exact func externtypes types Update the syntax of func externtypes and func types in the typing context to include exactness. This allows specifying exact function imports and properly typing ref.func as exact for exact imports and defined functions and otherwise as inexact. --- document/core/util/macros.def | 3 +++ .../wasm-latest/1.2-syntax.types.spectec | 22 ++++++++++++++----- .../2.0-validation.contexts.spectec | 2 +- .../wasm-latest/2.1-validation.types.spectec | 2 +- .../2.2-validation.subtyping.spectec | 4 ++-- .../2.3-validation.instructions.spectec | 16 ++++++++++---- .../2.4-validation.modules.spectec | 12 +++++----- .../wasm-latest/4.1-execution.values.spectec | 2 +- .../wasm-latest/5.2-binary.types.spectec | 3 ++- .../wasm-latest/6.2-text.types.spectec | 3 ++- 10 files changed, 48 insertions(+), 21 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 35413fb95..8676c91fe 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -239,6 +239,7 @@ .. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}} .. |EXACT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{exact}} +.. |INEXACT| mathdef:: {} .. |ANY| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{any}} .. |EQT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{eq}} .. |I31| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{i\scriptstyle31}} @@ -309,6 +310,7 @@ .. |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}} +.. |exact| mathdef:: \X{exact} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} @@ -349,6 +351,7 @@ .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}} +.. |exactheaptype| mathdef:: \F{exactheaptype} .. |funcsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}} .. |tablesxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index 25990998e..0502851e4 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -7,6 +7,9 @@ ;; TODO(3, rossberg): add ability to do this inline syntax null hint(show NULL) hint(macro "%" "%") = NULL +syntax exact hint(desc "exactness") = + | EXACT | INEXACT + syntax addrtype hint(desc "address type") = | I32 | I64 @@ -32,6 +35,8 @@ syntax rectype hint(desc "recursive type") ;; forward decl syntax deftype hint(desc "defined type") = | _DEF rectype n hint(show %.%) +syntax exactdeftype hint(show (exact deftype)) = exact deftype + syntax typeuse/syn hint(desc "type use") = | _IDX typeidx | ... syntax typeuse/sem = @@ -85,6 +90,12 @@ def $NULLEXNREF = (REF NULL NOEXN) def $NULLEXTERNREF = (REF NULL NOEXTERN) +def $exactheaptype(exact, typeuse) : heaptype + +def $exactheaptype(EXACT, typeuse) = EXACT typeuse +def $exactheaptype(INEXACT, typeuse) = typeuse + + ;; Packed types syntax packtype hint(desc "packed type") = I8 | I16 @@ -141,7 +152,7 @@ syntax datatype hint(desc "data type") = OK hint(macro "%data") syntax elemtype hint(desc "element type") = reftype syntax externtype hint(desc "external type") hint(macro "%" "XT%") = - | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC typeuse + | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC exact typeuse syntax moduletype hint(desc "module type") = externtype* -> externtype* hint(macro "toM") @@ -156,6 +167,7 @@ var at : addrtype ;; var bt : blocktype ;; defined below var ct : comptype var dt : deftype +var edt : exactdeftype var et : elemtype var ft : fieldtype var gt : globaltype @@ -315,7 +327,7 @@ def $tagsxt(externtype*) : tagtype* hint(show $tags(%)) hint(macro "ta def $globalsxt(externtype*) : globaltype* hint(show $globals(%)) hint(macro "globalsxt") def $memsxt(externtype*) : memtype* hint(show $mems(%)) hint(macro "memsxt") def $tablesxt(externtype*) : tabletype* hint(show $tables(%)) hint(macro "tablesxt") -def $funcsxt(externtype*) : deftype* hint(show $funcs(%)) hint(macro "funcsxt") +def $funcsxt(externtype*) : exactdeftype* hint(show $funcs(%)) hint(macro "funcsxt") def $tagsxt(eps) = eps def $tagsxt((TAG jt) xt*) = jt $tagsxt(xt*) @@ -334,7 +346,7 @@ def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*) def $tablesxt(externtype xt*) = $tablesxt(xt*) -- otherwise def $funcsxt(eps) = eps -def $funcsxt((FUNC dt) xt*) = dt $funcsxt(xt*) +def $funcsxt((FUNC exact dt) xt*) = (exact dt) $funcsxt(xt*) def $funcsxt(externtype xt*) = $funcsxt(xt*) -- otherwise @@ -436,7 +448,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*) def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*) def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*) def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*) -def $subst_externtype((FUNC dt), tv*, tu*) = FUNC $subst_deftype(dt, tv*, tu*) +def $subst_externtype((FUNC exact dt), tv*, tu*) = FUNC exact $subst_deftype(dt, tv*, tu*) def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)* @@ -598,7 +610,7 @@ def $free_externtype(TAG tagtype) = $free_tagtype(tagtype) def $free_externtype(GLOBAL globaltype) = $free_globaltype(globaltype) def $free_externtype(MEM memtype) = $free_memtype(memtype) def $free_externtype(TABLE tabletype) = $free_tabletype(tabletype) -def $free_externtype(FUNC typeuse) = $free_typeuse(typeuse) +def $free_externtype(FUNC exact typeuse) = $free_typeuse(typeuse) def $free_moduletype(externtype_1* -> externtype_2*) = $free_list($free_externtype(externtype_1)*) ++ diff --git a/specification/wasm-latest/2.0-validation.contexts.spectec b/specification/wasm-latest/2.0-validation.contexts.spectec index e9205fa2b..a48d50338 100644 --- a/specification/wasm-latest/2.0-validation.contexts.spectec +++ b/specification/wasm-latest/2.0-validation.contexts.spectec @@ -28,7 +28,7 @@ syntax context hint(desc "context") hint(macro "%" "C%") = GLOBALS globaltype* hint(desc "global"), MEMS memtype* hint(desc "memory"), TABLES tabletype* hint(desc "table"), - FUNCS deftype* hint(desc "function"), + FUNCS exactdeftype* hint(desc "function"), DATAS datatype* hint(desc "data segment"), ELEMS elemtype* hint(desc "element segment"), LOCALS localtype* hint(desc "local"), diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec index ddb81eb2f..c1089a135 100644 --- a/specification/wasm-latest/2.1-validation.types.spectec +++ b/specification/wasm-latest/2.1-validation.types.spectec @@ -265,6 +265,6 @@ rule Externtype_ok/table: -- Tabletype_ok: C |- tabletype : OK rule Externtype_ok/func: - C |- FUNC typeuse : OK + C |- FUNC exact typeuse : OK -- Typeuse_ok: C |- typeuse : OK -- Expand_use: typeuse ~~_C $($(FUNC t_1* -> t_2*)) diff --git a/specification/wasm-latest/2.2-validation.subtyping.spectec b/specification/wasm-latest/2.2-validation.subtyping.spectec index 9bd60602f..3c7fd4bf2 100644 --- a/specification/wasm-latest/2.2-validation.subtyping.spectec +++ b/specification/wasm-latest/2.2-validation.subtyping.spectec @@ -260,5 +260,5 @@ rule Externtype_sub/table: -- Tabletype_sub: C |- tabletype_1 <: tabletype_2 rule Externtype_sub/func: - C |- FUNC deftype_1 <: FUNC deftype_2 - -- Deftype_sub: C |- deftype_1 <: deftype_2 + C |- FUNC exact_1 deftype_1 <: FUNC exact_2 deftype_2 + -- Heaptype_sub: C |- $exactheaptype(exact_1, deftype_1) <: $exactheaptype(exact_2, deftype_2) diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 2e042e76f..0da536a45 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -120,7 +120,8 @@ rule Instr_ok/br_on_cast_fail: rule Instr_ok/call: C |- CALL x : t_1* -> t_2* - -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2* + -- if C.FUNCS[x] = exact dt + -- Expand: dt ~~ FUNC t_1* -> t_2* rule Instr_ok/call_ref: C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2* @@ -140,7 +141,8 @@ rule Instr_ok/return: ;; TODO(3, rossberg): enable t_2* <: C.RETURN rule Instr_ok/return_call: C |- RETURN_CALL x : t_3* t_1* -> t_4* - -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2* + -- if C.FUNCS[x] = exact dt + -- Expand: dt ~~ FUNC t_1* -> t_2* -- if C.RETURN = (t'_2*) -- Resulttype_sub: C |- t_2* <: t'_2* -- Instrtype_ok: C |- t_3* -> t_4* : OK @@ -210,8 +212,14 @@ rule Instr_ok/ref.null: -- Heaptype_ok: C |- ht : OK rule Instr_ok/ref.func: - C |- REF.FUNC x : eps -> (REF dt) - -- if C.FUNCS[x] = dt + C |- REF.FUNC x : eps -> (REF ht) + -- if C.FUNCS[x] = exact dt + -- if ht = $exactheaptype(exact, dt) + -- if x <- C.REFS + +rule Instr_ok/ref.func-exact: + C |- REF.FUNC x : eps -> (REF (EXACT dt)) + -- if C.FUNCS[x] = EXACT dt -- if x <- C.REFS rule Instr_ok/ref.i31: diff --git a/specification/wasm-latest/2.4-validation.modules.spectec b/specification/wasm-latest/2.4-validation.modules.spectec index a78814662..2d021afe2 100644 --- a/specification/wasm-latest/2.4-validation.modules.spectec +++ b/specification/wasm-latest/2.4-validation.modules.spectec @@ -90,7 +90,8 @@ rule Elemmode_ok/active: rule Start_ok: C |- START x : OK - -- Expand: C.FUNCS[x] ~~ FUNC eps -> eps + -- if C.FUNCS[x] = exact dt + -- Expand: dt ~~ FUNC eps -> eps ;; Im/exports @@ -125,8 +126,8 @@ rule Externidx_ok/table: -- if C.TABLES[x] = tt rule Externidx_ok/func: - C |- FUNC x : FUNC dt - -- if C.FUNCS[x] = dt + C |- FUNC x : FUNC exact dt + -- if C.FUNCS[x] = exact dt ;; Modules @@ -159,14 +160,15 @@ rule Module_ok: ---- -- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*} ---- - -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*} + -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS edt_I* edt*, REFS x*} + -- if edt* = (EXACT dt)* -- if x* = $funcidx_nonfuncs(global* mem* table* elem*) ---- -- if jt_I* = $tagsxt(xt_I*) -- if gt_I* = $globalsxt(xt_I*) -- if mt_I* = $memsxt(xt_I*) -- if tt_I* = $tablesxt(xt_I*) - -- if dt_I* = $funcsxt(xt_I*) + -- if edt_I* = $funcsxt(xt_I*) rule Types_ok/empty: diff --git a/specification/wasm-latest/4.1-execution.values.spectec b/specification/wasm-latest/4.1-execution.values.spectec index 1b38a0623..03cef8d5a 100644 --- a/specification/wasm-latest/4.1-execution.values.spectec +++ b/specification/wasm-latest/4.1-execution.values.spectec @@ -102,7 +102,7 @@ rule Externaddr_ok/table: -- if s.TABLES[a] = tableinst rule Externaddr_ok/func: - s |- FUNC a : FUNC funcinst.TYPE + s |- FUNC a : FUNC EXACT funcinst.TYPE -- if s.FUNCS[a] = funcinst rule Externaddr_ok/sub: diff --git a/specification/wasm-latest/5.2-binary.types.spectec b/specification/wasm-latest/5.2-binary.types.spectec index 743ff8785..c44cdb5b6 100644 --- a/specification/wasm-latest/5.2-binary.types.spectec +++ b/specification/wasm-latest/5.2-binary.types.spectec @@ -100,7 +100,8 @@ grammar Btabletype : tabletype = grammar Bexterntype : externtype = - | 0x00 x:Btypeidx => FUNC (_IDX x) + | 0x00 x:Btypeidx => FUNC INEXACT (_IDX x) + | 0x20 x:Btypeidx => FUNC EXACT (_IDX x) | 0x01 tt:Btabletype => TABLE tt | 0x02 mt:Bmemtype => MEM mt | 0x03 gt:Bglobaltype => GLOBAL gt diff --git a/specification/wasm-latest/6.2-text.types.spectec b/specification/wasm-latest/6.2-text.types.spectec index 2afedafc9..ee285b8fa 100644 --- a/specification/wasm-latest/6.2-text.types.spectec +++ b/specification/wasm-latest/6.2-text.types.spectec @@ -152,7 +152,8 @@ grammar Texterntype_(I) : (externtype, idctxt) = | "(" "global" id?:Tid? gt:Tglobaltype_(I) ")" => (GLOBAL gt, {GLOBALS (id?)}) | "(" "memory" id?:Tid? mt:Tmemtype_(I) ")" => (MEM mt, {MEMS (id?)}) | "(" "table" id?:Tid? tt:Ttabletype_(I) ")" => (TABLE tt, {TABLES (id?)}) - | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC $($(_IDX x)), {FUNCS (id?)}) + | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC INEXACT $($(_IDX x)), {FUNCS (id?)}) + | "(" "func" id?:Tid? "(" "exact" (x,I'):Ttypeuse_(I) ")" ")" => (FUNC EXACT $($(_IDX x)), {FUNCS (id?)}) ;; Type uses From ca049ee91d58f8eb202fb51b51169f0288390cef Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Wed, 8 Jul 2026 19:07:55 -0700 Subject: [PATCH 2/2] cleanup old Instr_ok/ref.func-exact --- .../wasm-latest/2.3-validation.instructions.spectec | 5 ----- 1 file changed, 5 deletions(-) diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 0da536a45..a41160bf6 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -217,11 +217,6 @@ rule Instr_ok/ref.func: -- if ht = $exactheaptype(exact, dt) -- if x <- C.REFS -rule Instr_ok/ref.func-exact: - C |- REF.FUNC x : eps -> (REF (EXACT dt)) - -- if C.FUNCS[x] = EXACT dt - -- if x <- C.REFS - rule Instr_ok/ref.i31: C |- REF.I31 : I32 -> (REF I31)