Allow `verbatim` in Solidity `assembly` blocks

[dessaya]

There is currently support for verbatim, allowing to instert arbitrary bytecode, but only when compiling in strict assembly mode. But the verbatim group of functions ios not available inside assembly blocks in Solidity code. Example:

function f() {
	assembly {
		verbatim_0i_0o(hex"c0")
	}
}

When compiling with solc:

Error: Function "verbatim_0i_0o" not found.

What is the motivation for disabling verbatim in Solidity? I understand that it must be used with care and only for very specific reasons. My use case is that I am targetting a forked version of the EVM interpreter with new opcodes. I'm currently unable to use solc to compile contracts targetting this fork.

Thanks!

[chriseth]

The reason is that we have to think about which optimizer steps to disable, and probably we have to disable almost all of them. Can you tell us more about the new opcodes in the fork?

[dessaya]

For now it's a proof of concept, and it's not even clear that this approach is the correct one.

We want to add support for Solidity as a language for an experimental language-agnostic smart contracts platform. We don't need or want to emulate a whole Ethereum blockchain, since our smart contracts run in level 2; we only need to run the Solidity code and store the current state. What we need is some way to bridge the Solidity code with the underlying sandbox; and for that one idea is to add some custom opcodes, like some form of "syscalls", like "obtain the chain ID" or "publish an event". Again, maybe there is a better approach but for now we are experimenting with this.

Thanks again!

[chriseth]

Wouldn't it be better to do this on the yul level instead? Plese feel free to schedule a call to discuss in more detail!

[dessaya]

What do you mean exactly? I know that I can write a contract in yul, and I can inject arbitrary bytecode with verbatim. This is what we are doing right now; but it would be nice to be able to write Solidity, and have a few small Yul blocks with assembly {...} where needed.

[hrkrshnn]

@dessaya To summarize why we haven't done this so far, the Yul optimizer wasn't designed keeping verbatim in mind. This means that if the Yul optimizer is enabled, then verbatim has to be used with extreme caution. We assume that users of pure Yul already are in a position to make this judgement (we have added some example situations that would lead to undefined behaviour: https://docs.soliditylang.org/en/latest/yul.html#verbatim).

We can of course allow it in Solidity's inline assembly. The question is if the Yul optimizer should be completely disabled or partly; if partly, which ones? It would be useful if you can give a list of additional opcodes that you would like to add this way, to get an idea of how this would work for your case.

[chriseth]

What I meant is to compile solidity to yul using solc --ir and then modify the resulting yul code where you can freely inject verbatim. It would be nice for us to know what exactly these syscalls are and how you want to link them to the solidity code.

[dessaya]

We are still evaluating options, so we haven't settled on what the opcodes will look like exactly. But an example would be something very simple to retrieve a value from the context:

let x := verbatim_0i_1o(hex"c1")

where the return value is provided by our sandbox; for example the (non-ethereum) address of the contract creator.

@chriseth I was not aware that solc --ir actually produced Yul code. It looks like this could be useful for our use case. I'll explore this approach. I think we can close this issue for now. Thanks!

[axic]

Instead of special opcodes it is also possible to use special addresses to exchange data (i.e. precompiles or system contract on some chains). If you have complete control over your system, that may be a nicer way because all EVM compatible languages (Vyper, Fe, etc.) could be made to work with it without changes.

[axic]

As mentioned we wanted to have this enabled originally, but the main problem here is somehow signalling what commitments the verbatim code makes against various EVM properties (e.g. "reads state", "modifies state", "terminates", etc.)

Since we have the memory-safe annotation, we could think about introducing more of such annotations (eventually somewhat resembling SemanticInformation). In that case would could enabled it "rather safely".

Additionally we could think about introducing a "clobbered variables" list.