Give native support to host function imports

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.

Start by reviewing the host-module approach in the referenced pull request and the KEwasm embedding definition. Then trace how imports and function-call instructions are represented in the Wasm semantics. Done would mean host modules and host calls are represented natively, with embeddings able to declare their host modules and rules without wrapper modules.