Exact func externtype types by tlively · Pull Request #102 · WebAssembly/custom-descriptors

tlively · 2026-07-08T01:37:35Z

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.

And struct.new_default_desc. Also update the valiation for struct.new and struct.new_default to require empty descriptors. Add an explanation of expansion to desctype to the validation conventions section and teach SpecTec about the new ExpandDesc relation to avoid errors during rendering.

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.

tlively · 2026-07-08T01:47:53Z

+def $exactheaptype(exact, typeuse) : heaptype
+
+def $exactheaptype(EXACT, typeuse) = EXACT typeuse
+def $exactheaptype(INEXACT, typeuse) = typeuse


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 :/

I figured something out in #106

Previously the definition of `heaptype` was `... | EXACT typeuse | typeuse`, but this made it impossible to treat the exactness as a variable. Refactor the definition to `... | _HT exact? typeuse` instead. This is similar to how nullability is treated in reference types, except that the `_HT` tag will not be displayed in the rendered spec.

…lidation

…nctype Update the typing context to store heap types for functions.

…lidation

…nctype

…lidation

…nctype

rossberg

Generalising the syntax of function types to arbitrary heaptypes is a bit nasty. Maybe we need an auxiliary form of type representing qualified type uses like exact? typeuse? Having a name and meta variable for that might also avoid the intrusive appearance of the _HT constructor everywhere, like in the other PR.

tlively · 2026-07-24T02:59:11Z

Oh interesting, I used to have an exacttypeuse production similar to what you're describing, but then I switched to using heaptype because it seemed simpler. I can play around with it more, though.

…x-validation

…nctype

# Conflicts: # specification/wasm-latest/1.2-syntax.types.spectec # specification/wasm-latest/1.3-syntax.instructions.spectec # spectec/src/backend-prose/gen.ml # spectec/test-frontend/TEST.md

…nctype # Conflicts: # document/core/valid/conventions.rst # specification/wasm-latest/1.2-syntax.types.spectec # specification/wasm-latest/2.4-validation.modules.spectec # spectec/test-frontend/TEST.md

tlively · 2026-10-15T03:09:31Z

@rossberg, I updated the approach here to match your suggestion in #102 (review). This is ready for another look.

rossberg · 2026-10-15T10:28:40Z

+  C |- FUNC x : FUNC exact? dt
+  -- if C.FUNCS[x] = exact? dt


Suggested change

C |- FUNC x : FUNC exact? dt

-- if C.FUNCS[x] = exact? dt

C |- FUNC x : FUNC edt

-- if C.FUNCS[x] = edt

Same issue here. We can't use an exactdeftype here because externtype is defined as ... | FUNC exact? typeuse. The same fix might apply.

rossberg · 2026-10-15T10:34:35Z

+  -- (Externaddr_ok: s |- FUNC funcaddr : FUNC exact? dt_F)*
+  -- if edt_F* = (exact? dt_F)*


Suggested change

-- (Externaddr_ok: s |- FUNC funcaddr : FUNC exact? dt_F)*

-- if edt_F* = (exact? dt_F)*

-- (Externaddr_ok: s |- FUNC funcaddr : FUNC exactdeftype)*

Same problem here.

tlively · 2026-10-21T01:40:43Z

AI explanation for the change here, if you're interested:

Defining syntax exacttypeuse = exact? typeuse and using _HT exacttypeuse in heaptype causes non-exact heap types like _HT x to elaborate with a nested CaseE for exacttypeuse, whose mixop ([None; None; None]) has no leading constructor atom (hd = None).

Previously in spectec/src/backend-prose/render.ml:

case_to_el_exprs only stripped EpsE (omitted optional arguments) when hd <> None (in order to preserve \epsilon on the LHS of infix notations like \epsilon \rightarrow t^\ast, where elal is None :: Some _ :: _).

al_to_el_expr wrapped any non-infix CaseE with non-empty elel in ParenE.

As a result, headless juxtaposition types like exacttypeuse rendered omitted optionals as (\epsilon~x) in generated prose (the same issue also affected globaltype = mut? valtype and fieldtype = mut? storagetype in test-prose/TEST.md, which rendered immutable types as (\epsilon~t) and (\epsilon~zt)).

Stripping EpsE for all non-infix mixops (not is_infix, where is_infix is None :: Some _ :: _) and omitting ParenE when a headless mixop reduces to a single element (None :: _, , []) fixes the prose rendering.

rossberg · 2026-10-21T13:52:25Z

  -- (Memtype_ok: C_0 |- mt : OK)*
  -- (Tabletype_ok: C_0 |- tt : OK)*
-  -- if edt_F* = (exact? dt_F)*
+  -- if edt* = (exact? dt_F)*


This line might suggest that we should introduce Exactdeftype_ok for completeness.

Unless we also add Expand_exactdt, we'll still need this destructing line. The Exactdeftype_ok line would just replace the Deftype_ok line below. I'm not sure that's worth it.

I uploaded #117 so you can see what that looks like. I'm happy to include those changes here or drop them, whatever you prefer.

Ah okay, you're right. In that case I agree it's not worth it.

rossberg · 2026-10-21T14:06:00Z

+  C |- REF.FUNC x : eps -> (REF (_HT exact? dt))
+  -- if C.FUNCS[x] = exact? dt


The crash shouldn't be, but yes, you can only combine proper variant types that way.

The trick would be to move the _HT constructor (under some appropriate rename) into exacttypeuse, which turns it into a variant type. Then the constructor is only needed when an exacttypeuse is de/composed, and not each time a typeuse is injected into heaptype.

tlively · 2026-10-22T14:57:55Z

@rossberg, any other comments on this one?

rossberg

Ah, sorry, I wasn't sure if you planned to also do the _HT change here. LGTM

tlively · 2026-10-23T05:20:55Z

The trick would be to move the _HT constructor (under some appropriate rename) into exacttypeuse, which turns it into a variant type. Then the constructor is only needed when an exacttypeuse is de/composed, and not each time a typeuse is injected into heaptype.

I looked into this, but typeuse isn't a subtype of exacttypeuse, so injecting a typeuse into heaptype still requires using a constructor. As a result, we can remove the constructor in the two places that inject an exactdeftype variable into heaptype (REF.FUNC and Externtype_sub/func), but it is required it in ~14 new places where exacttypeuse/exactdeftype are composed or decomposed outside heaptype (like FUNC exact? typeuse). Overall this seems not worth it, but you can see what it looks like in #118.

Alternatively, #119 hacks up spectec to make the _HT unnecessary.

rossberg · 2026-10-23T09:27:14Z

Yeah, I suppose the rules rarely ever care about typeuses that are not type indices, because those don't arise during validation. But thanks for looking into it anyway.

tlively added 3 commits July 6, 2026 20:33

const expr

47b07b7

Exact func externtypes types

2ca8cdd

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.

tlively requested a review from rossberg July 8, 2026 01:37

tlively commented Jul 8, 2026

View reviewed changes

cleanup old Instr_ok/ref.func-exact

ca049ee

tlively mentioned this pull request Jul 9, 2026

Core spec authoring checklist #94

Open

11 of 51 tasks

tlively added 14 commits July 13, 2026 04:49

Merge branch 'exact-heaptype-refactor' into struct-new-desc-syntax-va…

6a76272

…lidation

show EXACT

e7acc8d

Merge branch 'exact-heaptype-refactor' into struct-new-desc-syntax-va…

8b09b7f

…lidation

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

b9ebd33

…nctype Update the typing context to store heap types for functions.

update tests

34f1e65

Merge branch 'exact-heaptype-refactor' into struct-new-desc-syntax-va…

64a8276

…lidation

update tests

c3b35c6

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

c2bc74b

…nctype

update tests

e4fd1bd

fix parens

f1b94b8

update tests

de6816f

Merge branch 'exact-heaptype-refactor' into struct-new-desc-syntax-va…

f245509

…lidation

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

abf31f3

…nctype

rossberg reviewed Jul 22, 2026

View reviewed changes

tlively added 7 commits July 24, 2026 11:48

Merge remote-tracking branch 'origin/main' into struct-new-desc-synta…

290131a

…x-validation

Update prose and ExpandDesc => Expand_desc

29dcc39

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

942e17c

…nctype

Merge branch 'main' into struct-new-desc-syntax-validation

e132360

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

655de1f

…nctype

Merge branch 'main' into struct-new-desc-syntax-validation

93c99a4

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

d4e6d66

…nctype

tlively added 2 commits October 5, 2026 16:13

Merge branch 'main' into struct-new-desc-syntax-validation

c47c2df

# Conflicts: # specification/wasm-latest/1.2-syntax.types.spectec # specification/wasm-latest/1.3-syntax.instructions.spectec # spectec/src/backend-prose/gen.ml # spectec/test-frontend/TEST.md

Merge branch 'struct-new-desc-syntax-validation' into exact-extern-fu…

606e534

…nctype # Conflicts: # document/core/valid/conventions.rst # specification/wasm-latest/1.2-syntax.types.spectec # specification/wasm-latest/2.4-validation.modules.spectec # spectec/test-frontend/TEST.md

Base automatically changed from struct-new-desc-syntax-validation to main October 14, 2026 14:34

tlively added 5 commits October 14, 2026 17:39

Merge remote-tracking branch 'origin/main' into exact-extern-functype

a5a0919

whitespace errors

f0381c2

fixes

3668460

rewrite to use exact deftype and exact typeuse

f0ce19a

nit

d662b68

tlively changed the title ~~Exact func externtypes types~~ Exact func externtype types Oct 15, 2026

tlively requested a review from rossberg October 15, 2026 03:09

rossberg reviewed Oct 15, 2026

View reviewed changes

tlively added 8 commits October 15, 2026 22:53

Introduce exactdeftype as a proper type form

6afb348

Return exactdeftype from Func_ok

0798901

Clean up subtyping and soundness rules

95b8e46

Merge branch 'main' into exact-extern-functype

cc7c0a5

link to exactdeftype and update desc hint

27ff8ea

update conventions.rst

6475f4a

Add exacttypeuse and simplify rules using exactdeftype

b366fd5

Fix prose rendering for exacttypeuse and update docs

aa52cad

tlively commented Oct 21, 2026

View reviewed changes

tlively requested a review from rossberg October 21, 2026 01:40

rossberg reviewed Oct 21, 2026

View reviewed changes

rossberg approved these changes Oct 22, 2026

View reviewed changes

tlively merged commit f55437d into main Oct 22, 2026
11 of 12 checks passed

tlively deleted the exact-extern-functype branch October 22, 2026 16:36

		-- (Externaddr_ok: s \|- FUNC funcaddr : FUNC exact? dt_F)*
		-- if edt_F* = (exact? dt_F)*

		C \|- REF.FUNC x : eps -> (REF (_HT exact? dt))
		-- if C.FUNCS[x] = exact? dt

Conversation

tlively commented Jul 8, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

tlively commented Jul 24, 2026

Uh oh!

tlively commented Oct 15, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tlively commented Oct 22, 2026

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tlively commented Oct 23, 2026

Uh oh!

rossberg commented Oct 23, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants