From 509c894028ca17d92a03e93f6c243dfaf3016b85 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 15 Oct 2026 15:00:25 +0200 Subject: [PATCH] [spec] Specify that host call results must not be empty --- document/core/exec/instructions.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a4da2bcc61..7b37f2b40c 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -384,7 +384,7 @@ When the end of a function is reached without a jump (including through |RETURN| $${rule: Step_pure/frame-vals} -.. index:: host function, store +.. index:: host function, store, non-determinism .. _exec-invoke-host: Host Functions @@ -404,7 +404,8 @@ $${rule: {Step/call_ref-hostfunc-*}} Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:hf} in current store ${:s} with arguments ${:val^n}. It yields a set of possible outcomes, where each element is either a pair of a modified store ${:s'} and a :ref:`result ` or the special value ${hostcallresult:BOT} indicating divergence. -A host function is non-deterministic if there is at least one argument for which the set of outcomes is not singular. +This set must not be empty. +A host function is *non-deterministic* if there is at least one argument pair for which the set of outcomes is not singular. For a WebAssembly implementation to be :ref:`sound ` in the presence of host functions, every :ref:`host function instance ` must be :ref:`valid `,