Skip to content

Exact func externtypes types #102

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tlively wants to merge 2 commits into
base: struct-new-desc-syntax-validation
Choose a base branch
from
Open

Exact func externtypes types #102

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2ca8cdd
Exact func externtypes types
tlively Jul 8, 2026
ca049ee
cleanup old Instr_ok/ref.func-exact
tlively Jul 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions document/core/util/macros.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,7 @@
.. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}}

.. |EXACT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{exact}}
.. |INEXACT| mathdef:: {}

@tlively tlively Jul 8, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These macros need to be fixed up with proper cross references after some of the questions below are answered.

.. |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}}
Expand Down Expand Up @@ -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}}
Expand Down Expand Up @@ -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}}
Expand Down
22 changes: 17 additions & 5 deletions specification/wasm-latest/1.2-syntax.types.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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 =
Expand Down Expand Up @@ -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
Comment on lines +93 to +96

@tlively tlively Jul 8, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having the externtype and context store explicitly EXACT or INEXACT exactness instead of just containing an EXACT? is important for ensuring that both cases are handled everywhere. At the same time, it is annoying because heaptype has a different representation of exactness (... | typeuse | EXACT typeuse), so we require this auxiliary conversion function.

Do you have a recommendation for how to simplify this? I'm thinking that maybe we should be using heaptype instead of deftype/typeuse in the externtype and context definitions because heaptype already has exactness information built-in, and we would be able to avoid conversions that way. But then we might need a new form of expansion that can fish the type use out of both exact and inexact heap types instead :/



;; Packed types

syntax packtype hint(desc "packed type") = I8 | I16
Expand Down Expand Up @@ -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")
Expand All @@ -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
Expand Down Expand Up @@ -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*)
Expand All @@ -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


Expand Down Expand Up @@ -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*)*

Expand Down Expand Up @@ -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)*) ++
Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-latest/2.0-validation.contexts.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-latest/2.1-validation.types.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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*))
4 changes: 2 additions & 2 deletions specification/wasm-latest/2.2-validation.subtyping.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
11 changes: 7 additions & 4 deletions specification/wasm-latest/2.3-validation.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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*
Expand All @@ -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
Expand Down Expand Up @@ -210,8 +212,9 @@ 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.i31:
Expand Down
12 changes: 7 additions & 5 deletions specification/wasm-latest/2.4-validation.modules.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-latest/4.1-execution.values.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
3 changes: 2 additions & 1 deletion specification/wasm-latest/5.2-binary.types.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion specification/wasm-latest/6.2-text.types.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading