[WIP] spec: add <static> cell for flagging execution mode

[ehildenb]

As @pepyakin pointed out, we will need a <static> flag for capturing which EEI methods the current execution is allowed to access.

We could also think of implementing this as a <eeiNamespace> cell, which contains the list of EEI methods the current execution can access. This nicely encapsulates both the static notion, as well as the namespace notion we have discussed for having different methods available to the EVM engines vs the ewasm engines vs the evm2wasm engines.

@chfast and @axic what do you think? Basically, we would have two EVM namespaces, one which is evm, and one which is evm_static, the second not allowing access to the various EEI methods which cannot be accessed during a STATICCALL.

Also tagging @poemm for thoughts.

[ehildenb]

How static mode is decided is here: https://github.com/kframework/evm-semantics/blame/master/evm.md#L447

Looks like the one tricky case is that CALL only is considered to change state if the VALUE is non-zero. To implement this as a namespace, then I think we would need to have separate EEI.callValueZero and EEI.callValueNonZero and the like.

I like the idea of using the namespace concept to implement the static concept because it integrates nicely with ewasm (in terms of just providing the list of "allowed imported eei methods"), and makes it clear what is allowed in which modes.

[chfast]

Still you have to check if you have the access to non-static namespace at runtime, right?

The call separation sounds good to me. At the moment the cost is different depending if it transfers a value.

How about names like EEI.call and EEI.transferCall?

[ehildenb]

Yeah, the EEI would make the check if the current namespace allows for accessing those methods, and the namespace evm_static would not have access to EEI.log, EEI.setAccountStorage, EEI.transferCall, eei.create, or eei.selfDestruct. So we could define evm_static, evm_nonstatic (as the above listed opcodes), and say that evm == evm_static UNION evm_nonstatic to define the normal evm namespace.

The same namespacing trick would allow for limiting the opcodes that either evm, ewasm, ewasm_static, evm2wasm could access as well.