Give native support to host function imports

[hjorthjort]

The current approach to host functions is to introduce a Wasm module to simulate it, and adding special function call instructions to it. See this file:
https://github.com/runtimeverification/polkadot-verification/pull/103/files/9a535a2332aa82ae15cef0c54bec7c32ed743f6a#diff-0ca3b001e51794c799c189d2e70e6aa0

I believe we can improve on that method a bit. As it stands, we either need to write a Wasm host module the way the script above does (which is frail), or write a K definition of the module as in KEwasm.

Instead of declaring a new instruction for all host functions and wrapping the host functions in a module, we could extend the Wasm semantics, by having each embedder specify which modules should be considered host modules (in this case "env", in the Ewasm case "ethereum"), and adding rules for them:

syntax Set ::= "#HostModules" [function]
syntax Instr ::= #hostCall(WasmSting, WasmString, TypeDecl)

rule (import MODNAME FUNCNAME (func OID:OptionalId T:TypeDecl)) => (func OID T (#hostCall(MODNAME, FUNCNAME, T))
  requires MODNAME in #HostModules

Not saying this is something we should do now, necessarily, but it's something we should open an issue about,because it would make defining new embeddings easier. The concept of a host call would be native to the Wasm semantics, and each embedding would really only need to define the #HostModules set and each #hostCall it cares about. We could also assume any import from an undeclared module is a host function.

[ehildenb]

One thing I don't like about this approach is that it puts the host functions into the same module that is being currently defined, instead of into a separate Wasm module like the import statement expects. Not entirely sure this will cause any problems, but it definitely means different code paths will be executed.

But we could definitely have a mode where we "auto-construct" any implicit imported modules, so that any (import "MODULE_NAME" ...) statements automatically just add the corresponding statement to the module registry in the appropriate place (instead of to the current module).

The current approach is pretty low overhead though, and I don't think it's that frail. The KWASM-POLKADOT-HOST K module is pretty minimal, and the code this script is working over is auto-generated, so it should be uniform enough to be post-processed. But we won't know how frail it actually is until we try it out a bunch. I just tried to codify the process I was using locally to do the updates as a starting point here.

[hjorthjort]

That's a good point. So the best approach would be to allocate missing imports as host imports into the store directly. The good thing is that they don't get reallocated if they are imported in more than one module. And since imports are handled first in a module, it's basically equivalent to pre-allocating them, which is the correct approach.

The frailty comes from it relying on imports and type declarations being declared on one line each. If wasm2wat changes its pretty-printing that breaks. It's not something we need to rush to fix. But since there is a way to deal with this directly in the semantics which also reflectes the official-spec way to do things, I think it's worth fixing at some point.

I think another selling point is that it makes it easier to implement new embeddings. I'd prefer if it wasn't necessary to either set up a script like the one above or to define a file like ewasm.md in the ewasm-semantics repo. With an auto-construct mode, if no host function is called, the regular kwasm runner will work with no changes. If a host function is called, the runner will halt when it reaches it, which is the same as not returning control. If the host function should do something, the behavior can be added as a semantic rule. So an "embedder" file would just be a list of relevant host function rules.