Continations or Recursion?

[DavePearce]

At the moment, the DafnyEVM implements contract calls (e.g. CALL, DELEGATECALL, CREATE, etc) using a mechanism based on continuations. The primary reason this decision was originally made was to support verification. However, its not clear whether that is strictly necessary. Furthermore, using a more natural recursive approach would make the DafnyEVM more appealing as a formal specification to be read and understood by others.

The purpose of this issue is to revisit the decision around using continuations to see whether or not it still makes sense. For the record, here are the main points for/against of using continuations:

• (FOR) Using continuations means that the execution of every bytecode is a unit operation (i.e. does not result in the execution of any other bytecodes). This is advantageous from a verification perspective, as continuations allow us to reason about the code in the contract being called and avoid an unknown recursive execution of arbitrary depth (which would presumably be difficult for Z3 to reason about). Examples which illustrate this can be found here.

• (AGAINST) Continuations significantly impact the overall comprehensibility of the specification. They do not give a natural implementation of contract calls, as would be found in clients such as Geth. Furthermore, it maybe possible to reason about contract calls with a similar level of expressivity even if continuations are not being used.

The key question here is whether or not using a natural recursive approach actually limits what can be verified, and it seems prudent to investigate this further.