[spec] specify host functions in spectec by zilinc · Pull Request #2210 · WebAssembly/spec

zilinc · 2026-07-15T07:14:59Z

It breaks the prose backend.
The official spec still needs to splice the relevant additions from spectec.

zilinc · 2026-07-15T07:15:41Z

@rossberg We talked about upstreaming this part, and here we go. It should be a good starting point, but there're still TODOs.

rossberg

Thanks, this looks good so far.

rossberg · 2026-07-15T08:35:55Z

+
+def $lift_result(result) : instr*  hint(show %)
+def $lift_result(_VALS val*) = val*
+def $lift_result(`(REF.EXN_ADDR a) THROW_REF) = (REF.EXN_ADDR a) THROW_REF


Note that the representation of exception results changes in #2189.

rossberg · 2026-07-15T08:42:23Z

+rule Step/call_ref-hostfunc-res:
+  s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy)  ~>  s'; f; $lift_result(result)
+  ----
+  -- if $funcinst((s; f))[a] = fi


Does it not work to use pattern matching here, like in the hand-written version?

I think the reason was that there's a MODULE field in the record as well, so it has to appear in the pattern. But otherwise I don't see any problems. I can do it if it's preferred.

Ah, right. In that case leave it as is.

I was wondering why I needed the parens around (s; f) in the $funcinst call. Maybe the reason is in the latex generation:

-\mbox{if}~ (s ; f){.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\ +\mbox{if}~ s ; f{.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\

Yes, exactly. Or more precisely, the show hint for $funcinst removes the call parens..

rossberg · 2026-07-15T10:05:53Z

Quick reminder: please never, ever force-push to a PR branch, since that breaks half of GitHub's review work flow. ;)

zilinc · 2026-07-21T10:37:58Z

@f52985 I'm stuck on the reduction rules. I have a function call on the rhs of a reduction, which is not supported by the AL pipeline. Would you please take a look? @rossberg Do we want to generate prose for them? Currently there's no prose for the manually written rules.

rossberg · 2026-07-22T10:37:03Z

We don't necessarily need prose for these (since they are mostly interesting as part of a formalisation). But of course, the pipeline shouldn't break over them.

…g. $lift_result)

f52985 · 2026-07-23T09:06:10Z

@f52985 I'm stuck on the reduction rules. I have a function call on the rhs of a reduction, which is not supported by the AL pipeline. Would you please take a look?

https://github.com/f52985/spec/tree/hostfunc

In this branch, I implemented a fix that allows function calls—or, more generally, any expression whose type is a list of instructions—on the right-hand side of a reduction rule. It also seems to work correctly with the interpreter backend. Please check if this works, and let me know if something goes wrong.

zilinc · 2026-07-23T09:09:10Z

@f52985 I'm stuck on the reduction rules. I have a function call on the rhs of a reduction, which is not supported by the AL pipeline. Would you please take a look?

https://github.com/f52985/spec/tree/hostfunc

In this branch, I implemented a fix that allows function calls—or, more generally, any expression whose type is a list of instructions—on the right-hand side of a reduction rule. It also seems to work correctly with the interpreter backend. Please check if this works, and let me know if something goes wrong.

Thanks heaps Dongjun. I'll give it a go and let you know.

zilinc · 2026-07-24T09:03:25Z

@f52985 Thanks agian. The pipeline now works without errors. The prose merges the cases in a somewhat unexpected way, but since we are not using the prose for any of the rules here, it should be fine.

zilinc · 2026-07-24T09:06:33Z

@rossberg This should be ready. The new rules look almost identical as before. I edited the doc a bit to reflect some meta-variable changes, and also tried to fix the manual prose for the normal function call case.

rossberg

Ah, it wasn't necessary to change the prose for the normal function case, since that's gone anyway with #2189.

But while you're converting the host function section to SpecTec, would you mind including the inline math as well? For example, :math:`(s, \val^n)` becomes ${:(s, val^n)}.

rossberg

Thanks! Two minor oversights, I believe.

rossberg · 2026-07-24T11:45:43Z

 which means that it adheres to suitable pre- and post-conditions:
-under a :ref:`valid store <valid-store>` :math:`S`, and given arguments :math:`\val^n` matching the ascribed parameter types :math:`t_1^n`,
-executing the host function must yield a non-empty set of possible outcomes each of which is either divergence or consists of a valid store :math:`S'` that is an :ref:`extension <extend-store>` of :math:`S` and a result matching the ascribed return types :math:`t_2^m`.
+under a :ref:`valid store <valid-store>` ${:s}, and given arguments ${:\val^n} matching the ascribed parameter types ${:t_1^n},


Suggested change

under a :ref:`valid store <valid-store>` ${:s}, and given arguments ${:\val^n} matching the ascribed parameter types ${:t_1^n},

under a :ref:`valid store <valid-store>` ${:s}, and given arguments ${:val^n} matching the ascribed parameter types ${:t_1^n},

rossberg · 2026-07-24T11:46:43Z

-Here, :math:`\X{hf}(S; \val^n)` denotes the implementation-defined execution of host function :math:`\X{hf}` in current store :math:`S` with arguments :math:`\val^n`.
-It yields a set of possible outcomes, where each element is either a pair of a modified store :math:`S'` and a :ref:`result <syntax-result>`
-or the special value :math:`\bot` indicating divergence.
+Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:_HOSTFUNC hf} in current store ${:s} with arguments ${:val^n}.


Suggested change

Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:_HOSTFUNC hf} in current store ${:s} with arguments ${:val^n}.

Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:hf} in current store ${:s} with arguments ${:val^n}.

Thanks for spotting them. The other one was an oversight; this one was intentional, but the intention was not quite correct.

rossberg reviewed Jul 15, 2026

View reviewed changes

[spec] upstream host functions changes

58e434e

zilinc force-pushed the zilinc/hostfunc branch from 2e45c1b to 58e434e Compare July 15, 2026 10:00

[spectec] Handle function calls returning instr* on reduction rhs (e.…

1f2302b

…g. $lift_result)

zilinc added 2 commits July 24, 2026 15:12

update test expects

5af3aaf

fix rendering and edit document

80f8d1e

rossberg reviewed Jul 24, 2026

View reviewed changes

use inline spectec code in doc

5f7200b

rossberg reviewed Jul 24, 2026

View reviewed changes

fix typos

ec56131

rossberg approved these changes Jul 24, 2026

View reviewed changes

rossberg merged commit dfa3f32 into WebAssembly:main Jul 24, 2026
10 checks passed

	under a :ref:`valid store <valid-store>` ${:s}, and given arguments ${:\val^n} matching the ascribed parameter types ${:t_1^n},
	under a :ref:`valid store <valid-store>` ${:s}, and given arguments ${:val^n} matching the ascribed parameter types ${:t_1^n},

	Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:_HOSTFUNC hf} in current store ${:s} with arguments ${:val^n}.
	Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:hf} in current store ${:s} with arguments ${:val^n}.

Uh oh!

Conversation

zilinc commented Jul 15, 2026

Uh oh!

zilinc commented Jul 15, 2026

Uh oh!

rossberg left a comment

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!

zilinc Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

rossberg commented Jul 15, 2026

Uh oh!

zilinc commented Jul 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

rossberg commented Jul 22, 2026

Uh oh!

f52985 commented Jul 23, 2026

Uh oh!

zilinc commented Jul 23, 2026

Uh oh!

zilinc commented Jul 24, 2026

Uh oh!

zilinc commented Jul 24, 2026

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

rossberg left a comment

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!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

zilinc Jul 15, 2026 •

edited

Loading

zilinc commented Jul 21, 2026 •

edited

Loading