Subroutines and Static Jumps for the EVM
EIP 615 introduces new EVM opcodes and conditions on EVM code to support subroutines and static jumps, disallow dynamic jumps, and thereby make EVM code amenable to linear-time static analysis. This would provide for better formal analysis of EVM code.
- EIP 615 in Draft mode, please see the
ethereum/EIPsrepo for further discussion, or reference the published draft
- EIP 615 implemented in Aleth by Greg Colvin
- Propose EIP 615 for the Istanbul hard fork
- Talk to client teams, open tracking PRs (some discussions already completed)
- Get Aleth with 615 plugged into EVMC to connect into Geth on mainnet / testnet
From EIP-615, the Abstract and Motivation:
This EIP introduces new EVM opcodes and conditions on EVM code to support subroutines and static jumps, disallow dynamic jumps, and thereby make EVM code amenable to linear-time static analysis. This will provide for better compilation, interpretation, transpilation, and formal analysis of EVM code.
All current implementations of the Ethereum Virtual Machine, including the just-in-time compilers, are much too slow. This proposal identifies a major reason for this and proposes changes to the EVM specification to address the problem.
In particular, it imposes restrictions on current EVM code and proposes new instructions to help provide for:
- better-optimized compilation to native code
- faster interpretation
- faster transpilation to eWASM
- better compilation from other languages, including eWASM and Solidity
- better formal analysis tools
These goals are achieved by
- disallowing dynamic jumps
- introducing subroutines - jumps with return support
- disallowing pathological control flow and uses of the stack
We also propose to validate - in linear time - that EVM contracts correctly use subroutines, avoid misuse of the stack, and meet other safety conditions before placing them on the blockchain. Validated code precludes most runtime exceptions and the need to test for them. And well-behaved control flow and use of the stack makes life easier for interpreters, compilers, formal analysis, and other tools.