iframe-proxy

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:32:06Z

  ----
-  -- 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)*


It would be appropriate if Func_ok itself returned the edt now, since that's what functions are classified with.

(Nice side effect: you can rename dt' to plain dt.)

rossberg · 2026-10-15T10:33:48Z

             MEMS memtype*,
             TABLES tabletype*,
-             FUNCS deftype_F*,
+             FUNCS edt_F*,


For consistency:

Suggested change

FUNCS edt_F*,

FUNCS exactdeftype*,

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.

rossberg · 2026-10-15T10:36:03Z

         \CMEMS & \memtype^\ast, \\
         \CTABLES & \tabletype^\ast, \\
-         \CFUNCS & {\deftype'}^\ast, \\
+         \CFUNCS & (\exact^?~\deftype')^\ast, \\


Suggested change

\CFUNCS & (\exact^?~\deftype')^\ast, \\

\CFUNCS & \exactdeftype^\ast, \\

rossberg · 2026-10-15T10:52:03Z

-  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 |- (_HT exact_1? deftype_1) <: (_HT exact_2? deftype_2)


Suggested change

-- Heaptype_sub: C |- (_HT exact_1? deftype_1) <: (_HT exact_2? deftype_2)

-- Heaptype_sub: C |- _HT exact_1? deftype_1 <: _HT exact_2? deftype_2

rossberg · 2026-10-15T10:54:56Z

 syntax deftype hint(desc "defined type") =
  | _DEF rectype n hint(show %.%)

+syntax exactdeftype hint(desc "function type") hint(show (exact? deftype)) = exact? deftype


Hm, this show hint is rather hacky, it won't work correctly if somebody needs to use something like exactdeftype_i anywhere. I see that you avoid that by always expanding it out, but it would probably be cleaner if we introduced exactdeftype properly as a new type form.

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

      MEMS mt*,
      TABLES tt*,
-      FUNCS dt_F*,
+      FUNCS edt_F*,


Suggested change

FUNCS edt_F*,

FUNCS edt*,

rossberg · 2026-10-15T10:56:49Z

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


Suggested change

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

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

rossberg · 2026-10-15T10:57:03Z

  -- (Resulttype_ok: C_0 |- t*: OK)*
  -- (Resulttype_ok: C_0 |- t'* : OK)?
-  -- (if x < |dt_F*|)*
+  -- (if x < |edt_F*|)*


Suggested change

-- (if x < |edt_F*|)*

-- (if x < |edt*|)*

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.

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

4 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

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

	\CFUNCS & (\exact^?~\deftype')^\ast, \\
	\CFUNCS & \exactdeftype^\ast, \\

	-- Heaptype_sub: C \|- (_HT exact_1? deftype_1) <: (_HT exact_2? deftype_2)
	-- Heaptype_sub: C \|- _HT exact_1? deftype_1 <: _HT exact_2? deftype_2

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

Sunbelt Computer Software

PL/B Language Development and Support

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!

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!

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!

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants