[spec] Specify that host call results must not be empty

[rossberg]

Addresses this (comment)[https://github.com//issues/2279#issuecomment-6192474895].

@zilinc, PTAL.

[zilinc]

Adding a trap rule sounds more correct to me. If a host call returns an empty set, it models that the host call has failed in an irrecoverable way. Requiring non-empty result set would effectively assume host call cannot fail.
EDIT: Ah I see. Yeah, requiring non-empty makes sense. The result type already contains a TRAP outcome, which is correctly propagated to the reduction result of rule rule Step/call_ref-hostfunc-res.
EDIT 2: Actually, I'm not entirely sure. In this rule, if the host call returns a set that contains TRAP, and some good results, do we want the TRAP to dominate? Is there a kind of failure that is more catastrophic than TRAP? It's a similar situation to the discussion at the bottom of page 3 of this paper Secure Microkernels, State Monads and Scalable Refinement .

[zilinc]

With that said, I don't fully get your remark in the discussion in the other issue:

(Theoretically, we could have a rule that traps in that case, but that wouldn't reflect any behaviour possible in reality.)

[rossberg]

An adequate model of non-deterministic failure would make it an element of the set, e.g. by extending the domain to include not just bottom but also TRAP. An empty set of behaviours OTOH means that there is no possible outcome at all, not even failure, which is meaningless. (Note that for numerics the model is different, because failure is always deterministic.)

It probably makes sense to add this, but that's orthogonal to this clarification. For Wasm 3.0 I think we also need to allow exceptions as a possible outcome.