This is a minimal change to the EVM to support calls and returns.
This proposal introduces three new control-flow instructions to the EVM:
CALLSUB transfers control to the destination on the data stack.ENTERSUB marks a subroutine entry: the destination of a CALLSUB, or of a JUMP that eliminates a call.RETURNSUB returns to the PC after the most recent CALLSUB.Code can also be prefixed with MAGIC bytes. MAGIC code is validated at CREATE time to ensure that it cannot execute invalid instructions, jump to invalid locations, underflow stack, or, in the absence of recursion, overflow stack.
The complete control flow of MAGIC code can be traversed in time and space linear in the size of the code, enabling tools for validation, automated proofs of correctness, and ahead-of-time and just-in-time compilers.
These changes are backwards compatible: all instructions behave as specified whether or not they appear in MAGIC code.
Note: Significant assistance from Anthropic's Claude is acknowledged, primarily for Vyper code.
The EVM currently lacks explicit call and return instructions. Instead, calls and returns must be synthesized using the dynamic JUMP instruction, which takes its destination from the stack. This creates two fundamental problems:
For detailed historical context, technical foundations of static control flow, and their impact on Ethereum's scaling roadmap, see EIP-8173: "Foundations of EVM Control Flow."
The key words MUST and MUST NOT in this Specification are to be interpreted as described in RFC 2119 and RFC 8174.
Conventions: backticks mark literal code — opcodes, bytecode, and identifiers from the reference implementation. Italics mark technical terms defined in this Specification, most of them under Validity, below.
The EVM's machine state includes a data stack of 256-bit words, at most 1024 deep, and the program counter, PC, whose value is a position in the code — the index of the next byte to execute. This EIP adds a return stack of return addresses, pushed only by CALLSUB, popped only by RETURNSUB, and not otherwise accessible to EVM code.
CALLSUB (0x..)Transfers control to a subroutine.
If the destination is not an ENTERSUB instruction, or the return stack
already holds 1024 items, execution is in an exceptional halting state.
(These are the analogues, for CALLSUB, of the invalid-jump-destination and
stack-overflow conditions.)
The gas cost is mid (8).
ENTERSUB (0x..)Marks a destination for CALLSUB. Like JUMPDEST, it is otherwise a
no-op: execution falls through. The destination of every CALLSUB MUST
be an ENTERSUB.
An ENTERSUB is also, like a JUMPDEST, a valid destination for JUMP
and JUMPI. Jumping to an ENTERSUB enters the subroutine without
pushing to the return stack, so the subroutine's RETURNSUB returns to
the original caller.
The gas cost is jumpdest (1).
RETURNSUB (0x..)Returns control to the caller of a subroutine.
If the return stack is empty, execution is in an exceptional halting state.
The gas cost is low (5).
MAGIC (0xEF....)After this EIP has been activated, code beginning with the MAGIC bytes MUST be a valid program. Execution begins immediately after the MAGIC bytes.
Notes:
CALLSUB and RETURNSUB.CALLSUB to unobservably push the PC on the return stack rather than PC + 1, which is allowed so long as RETURNSUB observably returns control to the PC + 1 location.)MAGIC values are still to be determined, but the MAGIC bytes will begin with 0xEF.A mid cost for CALLSUB is justified by it taking very little more work than the mid cost of JUMP — just pushing an integer to the return stack.
A jumpdest cost for ENTERSUB is justified by it being, like JUMPDEST, a mere label.
A low cost for RETURNSUB is justified by needing only to pop the return stack into the PC — less work than a jump.
Benchmarking will be needed to tell if the costs are well-balanced.
Execution is defined in the Yellow Paper as a sequence of changes to the EVM state. Exceptional halting conditions are properties of the machine state, checked before each instruction executes: if executing an instruction would violate a condition, execution halts instead — as the Yellow Paper puts it (§9.4.2), "no instruction can, through its execution, cause an exceptional halt." Because the conditions are checked state by state, proving that no reachable state of a program violates them proves that no execution of the program can reach an exceptional halting state. That is what validation does — once, at CREATE time. The Yellow Paper defines six such conditions:
We would like to consider EVM code valid if and only if no execution of the program can lead to an exceptional halting state. In practice, we must test at runtime for the first three conditions — we don't know whether we will be called statically, how much gas there will be, or how deep a recursion may go. (However, we can validate that non-recursive programs do not overflow stack.) All of the remaining conditions MUST be validated statically.
To allow for efficient algorithms, our validation considers only the code's control flow and stack use, not its data and computations. This means we will reject programs with invalid code paths, even if data values would prevent those paths from ever being taken.
The constraints below are stated in terms of the following definitions.
An instruction is a byte of code that is not PUSH immediate data. A path
is a possible sequence of executed instructions, starting at PC 0;
validation follows both arms of every JUMPI, without regard to data values.
An instruction is reachable if it lies on some path. Bytes on no path are
data, and are ignored.
frame: the span of a path from a CALLSUB to the RETURNSUB that
pops the return address it pushed. Frames nest; execution begins in an
implicit outermost frame.
entry: an ENTERSUB. Every frame begun by a CALLSUB starts
at an entry; an entry may also be entered without a call — by falling
through, or by jump — so subroutines may have multiple entry points.
region: the reachable instructions governed by a given entry —
those whose most recent ENTERSUB within their frame is that entry;
the entry is said to govern them. Regions partition the reachable
instructions; the outermost region, governed by no entry, begins at
PC 0.
baseline: the depth of the data stack at the start of the current
region on a given path — at its entry's ENTERSUB, or at the start
of execution in the outermost region. Baselines vary from call to call;
stack offsets, measured from them, do not.
stack offset: the depth of the data stack, minus the current baseline.
net stack effect: of an entry, the stack offset at the
RETURNSUB that closes a frame begun at that entry. Items pushed
minus items popped: positive, negative, or zero.
Code beginning with MAGIC MUST be valid. Constraints 1–4 restate, in
static form, the exceptional halting conditions of the Yellow Paper that do
not depend on gas or call context. Constraint 5 makes them statically
decidable in a single linear pass.
Every reachable instruction MUST be a valid opcode:
INVALID opcode is valid.Every reachable JUMP and JUMPI MUST be immediately preceded by a
PUSH, whose immediate value is the destination. The destination MUST
be a JUMPDEST or an ENTERSUB instruction — immediate data is not an
instruction. A jump to an ENTERSUB enters the subroutine.
Every reachable CALLSUB MUST be immediately preceded by a PUSH, whose
immediate value is the destination. The destination MUST be an ENTERSUB
instruction.
On every path: each instruction MUST find at least as many items on the
data stack as it removes, and MUST NOT leave more than 1024; each
CALLSUB MUST NOT leave more than 1024 items on the return stack;
each RETURNSUB MUST find at least one.
Stack offsets MUST be path-independent:
Constraint 5 is what makes one-pass validation possible. A subroutine is validated once, in terms of stack offsets, no matter how many call sites invoke it at different absolute depths. Each entry's net stack effect is a constant, so the stack height at every return point is static. Loops must be stack-neutral per iteration — a backward branch arrives at the stack offset it left — so each instruction need be visited only once. Together with Constraint 4, this prevents stack underflow, and prevents stack overflow in the absence of recursion.
Constraints on MAGIC code MUST be validated at CREATE time, in time and space linear in the size of the code. To this end, a canonical EVM implementation of the validation algorithm MUST be placed on the blockchain and identified in the MAGIC header. This validation code or its equivalent MUST be run on the output of the initialization code before it is executed by the interpreter, and failure of validation is an exceptional halting state.
Constraint 1 is evaluated as of validation time: the canonical contract MUST be updated at each fork that adds or deprecates opcodes. Contracts validated under earlier forks remain deployed; reaching a deprecated opcode in one is an exceptional halting state.
The layout of the MAGIC header is explicitly deferred to a follow-on specification: other EIPs also need to carry information in the header, and the layouts will need to be reconciled. That specification will also decide how the header identifies the canonical validation contract, and whether future versions may identify other validators. For this EIP it suffices that the header identifies the canonical contract unambiguously.
Clients need not implement the validation algorithm — they can simply call the canonical contract on the blockchain. Clients are of course free to implement equivalent algorithms themselves.
Note: The JVM, Wasm, and .NET VMs enforce similar constraints for similar reasons.
The above is a purely semantic specification, placing no constraints on the syntax of bytecode beyond being an array of opcodes and immediate data. Subroutines here are not contiguous sequences of bytecode: they are subgraphs of the bytecode's full control-flow graph. The EVM is a simple state machine, and the control-flow graph for a program represents every possible change of state. Each instruction simply advances the machine one state, and the instructions and state have minimal syntactic structure. We only promise that valid code will not, as it were, jam up the gears of the machine.
Rather than enforce semantic constraints via syntax — as is done by higher-level languages — this proposal enforces them via validation: MAGIC code is proven valid at CREATE time.
With no syntactic constraints and minimal semantic constraints, we maximize opportunities for optimizations, including call elimination, multiple-entry calls, efficient register allocation, and inter-procedural optimizations. Since we want to support online compilation of EVM code to native code, it is crucial that the EVM code be as well optimized as possible by high-level-language compilers — upfront and offline.
Primarily backwards compatibility. Other reasons include:
See EIP-3540: EOF - EVM Object Format and EIP-4750: EOF - Functions for complementary proposals that provide function descriptors for code sections and immediate arguments for relative jumps within code sections. Those proposals needed to introduce special-purpose opcodes to allow for important uses of cross-subroutine jumps.
By marking MAGIC contracts as valid we are promising that their control flow is static, and the many tools that traverse the control flow can know this without inspecting the code for themselves. The intention is to end a vicious cycle: tools work around the EVM's dynamic control flow to recover subroutines, compilers work around it to implement them, and neither group is much aware of the other's needs — needless complexity and technical debt all around. With this proposal it will at least and at last become possible to write static EVM code, and break the cycle.
As a demonstration, extract_cfg.py, provided with the reference implementation, recovers the complete control-flow graph of validated code — basic blocks, branches, calls, and returns — in a single linear pass, trusting validity and performing no checks of its own.
Backwards compatibility. We obviously cannot require existing code to become valid, and in a large, open ecosystem we cannot force an adoption schedule.
The creator. Validation runs as part of CREATE, and in this draft it is charged like any other execution: the canonical contract's gas is metered as usual and paid by the creating transaction. A contract that fails validation consumes its gas, exactly as initialization code that reverts consumes its gas. Alternative charging schemes — such as a flat per-byte price in the style of the initcode rules, which the linear bound would justify — are left for review.
Placing consensus-critical code on the blockchain follows the system-contract pattern established by EIP-4788 and EIP-2935. Note that the reference implementation below is written for clarity, not gas: a production validator — or a client's native equivalent — would pack its arrays and be substantially cheaper.
CALLSUB, ENTERSUB, and RETURNSUB allowed in ordinary code?Primarily backwards compatibility. We need MAGIC code to run unaltered in ordinary contracts. Also, these instructions have legitimate uses in code that will not pass validation. For example, a compiler might make good use of calls and returns, but still need dynamic jumps to implement efficient virtual functions. EOF - Functions or a similar proposal could provide them, but in the interim the compiler must choose between efficiency and MAGIC.
JUMP and JUMPI restricted in MAGIC code?Constraint 2 requires that JUMP and JUMPI in MAGIC code be immediately preceded by a PUSH instruction, making their destinations compile-time constants. This converts them from dynamic to static jumps, preserving their use for intra-subroutine branching — loops, conditionals — while ensuring that all control flow in MAGIC code is statically resolvable in a single linear pass.
The destination may be a JUMPDEST or an ENTERSUB. A jump to an ENTERSUB enters the subroutine without a call: where a CALLSUB would be the last action before a RETURNSUB, the jump does the same work with no return address pushed — the call is eliminated. This makes ENTERSUB a safe cross-region label: within a region, jumps go to JUMPDESTs; between regions, control enters at an entry, by call or by jump. Call elimination in this form supports tail recursion, mutual recursion and state machines, shared epilogues, and the outlining of repeated code — the transformations optimizing compilers rely on — while leaving computed dispatch out: destinations remain compile-time constants, so the path-explosion door stays shut. Jumping into the middle of another region remains invalid; the one-byte ENTERSUB is the price of making a point enterable, and it keeps every cross-region transfer visible to one-pass analysis.
Recovering a program's control flow is a fundamental first step for many analyses. When all jumps are static, the number of analysis steps is linear in the number of instructions: a fixed number of paths must be explored for each jump. With dynamic jumps, every possible destination must be explored at every jump. Intuitively, the number of possible paths through code just explodes. At worst, the number of paths in the control flow can go up as the square of the number of instructions, and symbolic execution of the paths can go up exponentially. See EIP-8173 for a more detailed explanation and example exploit.
This behavior is not merely a theoretical concern. For Ethereum, it represents a denial-of-service vulnerability for many tools — including bytecode validation and AOT or JIT compilation at runtime. And even offline it renders many analyses impractical, intractable, or impossible.
This proposal aims to be a minimal change to the EVM. We introduce two abstract operations — call and return — implemented by three instructions: CALLSUB, ENTERSUB, and RETURNSUB. These suffice to eliminate the need for dynamic jumps. (Note: ENTERSUB and JUMPDEST are not mere conveniences. The two kinds of label make every destination self-describing: a JUMPDEST marks a branch target within a region, while an ENTERSUB marks an entry, where the baseline resets and a jump eliminates a call. Without the distinction, the validator could not tell a merge from an entrance.)
Register machines like x86, ARM, and RISC-V typically use a single stack and dedicated registers for both data and return addresses. Stack machines like Turing's ACE, Forth, the JVM, Wasm, and .NET use separate data and return stacks. The EVM is a stack machine, and we adopt the same proven approach: a separate return stack isolated from the data stack. Another reason to maintain a separate stack is that data stack items are 32 bytes, but jump destinations will not need more than one or two.
The return addresses, being on their own stack, are not accessible to EVM code. They cannot be read, modified, or moved by ordinary stack operations. This eliminates an entire class of vulnerabilities where code could corrupt its own control flow.
Because return addresses are controlled exclusively by CALLSUB and RETURNSUB, they are intrinsically safe to validate. Unlike data-stack values (which may depend on arbitrary computation), return-stack values are guaranteed to be valid PC values — we can validate all return addresses at compile time.
The difference these instructions make can be seen in this very simple code for calling a routine that squares a number. The distinct opcodes make it easier for both people and tools to understand the code, and there are modest savings in code size and gas costs as well.
That's 29% fewer bytes and 32% less gas using CALLSUB versus using JUMP. So we can see that these instructions provide a simpler, more efficient mechanism. As code becomes larger and better optimized the gains become smaller, but code using CALLSUB always takes less space and gas than equivalent code without it.
Some real-time interpreter performance gains are reflected in the lower gas costs. But larger gains come from AOT and JIT compilers. The constraint that stack depths be constant means that in MAGIC code, a JIT can traverse the control flow in one pass, generating machine code on the fly, and an AOT can emit better code in linear time. (The Wasm, JVM, and .NET VMs share this property.)
The EVM is a stack machine, but most real machines are register machines. Generating virtual register code for a faster interpreter can yield significant gains (4X speedups are possible on JVM code), and generating good machine code can yield orders of magnitude improvements. However, for most transactions, storage dominates execution time, and gas counting and other overhead always take their toll. So such gains would be most visible in contexts where overhead is minimal, such as L1 precompiles, some L2s, and some EVM-compatible chains.
Measurements of ZK-proving for EOF - Functions showed many improvements to ZK-proof efficiency. See EIP-8173 for details on how static control flow improves ZK-rollup and optimistic rollup efficiency, and enables future migrations to ZK-friendly execution environments like RISC-V.
These changes are backwards compatible. The new opcodes are available in both ordinary and MAGIC code. Opcode semantics are not affected by whether the contract is MAGIC, so valid code will execute identically in any contract. Validation of MAGIC code is done before the interpreter runs, such that the interpreter never sees MAGIC code that is not valid. There are no changes to the semantics of existing EVM code. (With the caveat that code with unspecified behavior might behave in different, unspecified ways. Such code was always broken.)
Therefore this proposal does not require a client to maintain two interpreters. Neither does this proposal require a client to implement validation code — it will already be on the blockchain. So the implementation can come down to a push and a jump to call, and a pop and another jump to return.
These changes do not preclude running the EVM in zero knowledge; neither do they foreclose EOF, RISC-V, or other changes.
Note: the bytecode strings in these tests use placeholder opcode values
0xB0=CALLSUB, 0xB1=ENTERSUB, 0xB2=RETURNSUB, which are to be
confirmed when final opcode assignments are made. The traces, gas totals,
and pass/fail outcomes are correct for the semantics defined in this EIP.
The Stack column shows the data stack before the instruction executes. The RStack column shows the return stack before the instruction executes.
This should call a subroutine, return from it, and stop.
Bytecode: 0x6004B000B1B2 (PUSH1 0x04, CALLSUB, STOP, ENTERSUB, RETURNSUB)
| PC | Op | Cost | Stack | RStack |
|---|---|---|---|---|
| 0 | PUSH1 | 3 | [] | [] |
| 2 | CALLSUB | 8 | [4] | [] |
| 4 | ENTERSUB | 1 | [] | [3] |
| 5 | RETURNSUB | 5 | [] | [3] |
| 3 | STOP | 0 | [] | [] |
Output: 0x
Consumed gas: 17
This should execute fine, going into two depths of subroutines.
Bytecode: 0x6004B000B16009B0B2B1B2 (PUSH1 0x04, CALLSUB, STOP, ENTERSUB, PUSH1 0x09, CALLSUB, RETURNSUB, ENTERSUB, RETURNSUB)
| PC | Op | Cost | Stack | RStack |
|---|---|---|---|---|
| 0 | PUSH1 | 3 | [] | [] |
| 2 | CALLSUB | 8 | [4] | [] |
| 4 | ENTERSUB | 1 | [] | [3] |
| 5 | PUSH1 | 3 | [] | [3] |
| 7 | CALLSUB | 8 | [9] | [3] |
| 9 | ENTERSUB | 1 | [] | [3,8] |
| 10 | RETURNSUB | 5 | [] | [3,8] |
| 8 | RETURNSUB | 5 | [] | [3] |
| 3 | STOP | 0 | [] | [] |
Consumed gas: 34
This should fail because the destination is outside the code range.
Bytecode: 0x60FFB000B1B2 (PUSH1 0xFF, CALLSUB, STOP, ENTERSUB, RETURNSUB)
| PC | Op | Cost | Stack | RStack |
|---|---|---|---|---|
| 0 | PUSH1 | 3 | [] | [] |
| 2 | CALLSUB | 8 | [0xFF] | [] |
Error: at pc=2, op=CALLSUB: invalid destination
This should fail at the first opcode because the return stack is empty.
Bytecode: 0xB2 (RETURNSUB)
| PC | Op | Cost | Stack | RStack |
|---|---|---|---|---|
| 0 | RETURNSUB | 5 | [] | [] |
Error: at pc=0, op=RETURNSUB: invalid return stack
In this example, CALLSUB is the last byte of code. When the subroutine
returns, it should hit the implicit STOP after the bytecode and not exit
with error.
Bytecode: 0x600556B1B25B6003B0 (PUSH1 0x05, JUMP, ENTERSUB, RETURNSUB, JUMPDEST, PUSH1 0x03, CALLSUB)
| PC | Op | Cost | Stack | RStack |
|---|---|---|---|---|
| 0 | PUSH1 | 3 | [] | [] |
| 2 | JUMP | 8 | [5] | [] |
| 5 | JUMPDEST | 1 | [] | [] |
| 6 | PUSH1 | 3 | [] | [] |
| 8 | CALLSUB | 8 | [3] | [] |
| 3 | ENTERSUB | 1 | [] | [9] |
| 4 | RETURNSUB | 5 | [] | [9] |
| 9 | (implicit STOP) | 0 | [] | [] |
Consumed gas: 29
The following bytecodes exercise the validator itself: the last column is
the expected result of validate(). They are run by test_validator.py,
which accompanies the reference implementation. The overflow tests are run
with STACK_LIMIT reduced to 16, so that the bounds are reachable with
small vectors; the algorithm is independent of the limit.
The test cases above
| Test | Bytecode | Valid |
|---|---|---|
| simple routine | 0x6004B000B1B2 | yes |
| two levels of subroutines | 0x6004B000B16009B0B2B1B2 | yes |
| destination outside code | 0x60FFB000B1B2 | no |
bare RETURNSUB | 0xB2 | no |
| subroutine at end of code | 0x600556B1B25B6003B0 | yes |
Constraint 1: opcodes
| Test | Bytecode | Valid |
|---|---|---|
lone STOP | 0x00 | yes |
| undefined opcode | 0x21 | no |
INVALID is valid | 0xFE | yes |
| undefined opcode at return point | 0x6004B021B1B2 | no |
Constraints 2 and 3: destinations
| Test | Bytecode | Valid |
|---|---|---|
JUMP into PUSH immediate | 0x600156 | no |
JUMP to visited non-JUMPDEST | 0x5F5F01600256 | no |
JUMP not preceded by PUSH | 0x365B56 | no |
PUSH0-preceded JUMP | 0x5B5F56 | yes |
CALLSUB to JUMPDEST | 0x6004B0005B | no |
Constraint 4: underflow and return stack
| Test | Bytecode | Valid |
|---|---|---|
ADD on empty stack | 0x01 | no |
POP on empty stack | 0x50 | no |
| subroutine consumes caller argument | 0x6002600BB06003600BB000B18002B2 | yes |
| subroutine underflows caller | 0x6004B000B15050B2 | no |
fall into subroutine, then RETURNSUB | 0xB1B2 | no |
Constraint 5: offsets and net effects
| Test | Bytecode | Valid |
|---|---|---|
JUMPI arms disagree at join | 0x366005575F5B00 | no |
JUMPI diamond, consistent | 0x366006575F005B5F00 | yes |
two RETURNSUBs disagree | 0x6004B000B136600A57B25B5FB2 | no |
two RETURNSUBs agree | 0x6004B000B136600A57B25B5F50B2 | yes |
| stack-neutral loop | 0x5B600056 | yes |
Reuse and multiple entry points
| Test | Bytecode | Valid |
|---|---|---|
| called at two depths | 0x6002600BB06003600BB000B18002B2 | yes |
| fall-through second entry | 0x6008B05F600AB000B15FB150B2 | yes |
Recursion
| Test | Bytecode | Valid |
|---|---|---|
| recursion, no base case | 0x6004B000B16004B0B2 | yes |
| recursion eats caller stack | 0x6004B000B1506004B0 | no |
Jumps to an ENTERSUB (call elimination)
| Test | Bytecode | Valid |
|---|---|---|
jump to an ENTERSUB | 0x6004B000B15F600956B150B2 | yes |
conditional jump to an ENTERSUB | 0x6004B000B136600A57B2B1B2 | yes |
jump to an ENTERSUB, net effects disagree | 0x6004B000B15F36600B57B2B150B2 | no |
| unframed jump to a called subroutine | 0x6006B0600656B1B2 | no |
Overflow (run with STACK_LIMIT = 16)
| Test | Bytecode | Valid |
|---|---|---|
| 17 pushes overflow | 17 × PUSH0, STOP | no |
| 16 pushes fit | 16 × PUSH0, STOP | yes |
| subroutine high amplified, two calls | 0x6007B06007B000B15F5F5F5F5F5F5F5F5FB2 | no |
| subroutine high fits, one call | 0x6004B000B15F5F5F5F5F5F5F5F5FB2 | yes |
| call chain, depth 17 | call_chain(17) in the test file | no |
| call chain, depth 16 | call_chain(16) in the test file | yes |
| growing recursion allowed | 0x6004B000B15F6004B0 | yes |
The following is a Vyper implementation of the validation algorithm for MAGIC code. It validates EVM bytecode against the five constraints defined above in time and space linear in the size of the code.
A canonical deployment of this contract MUST be placed on the blockchain and its address included in the MAGIC header. This contract or its equivalent MUST be called on the output of the initialization code before it is executed by the interpreter; failure of validation is an exceptional halting state.
Clients need not implement the validation algorithm — they can simply call the canonical contract on the blockchain.
The contract is embedded below — with the opcode table abridged to a stub — so that this EIP reads as a single document. The complete contract is provided as a separate file, together with the test suite test_validator.py, which runs all of the validation test cases above, and the one-pass control-flow-graph extractor extract_cfg.py.
Validation is a worklist traversal of the control-flow graph, in the terms of the Definitions above. It tracks stack offsets, not absolute heights, so a subroutine is validated once no matter how many call sites invoke it at different depths.
Each item on the worklist is a continuation: a PC, its stack offset, its
governing entry (the most recent ENTERSUB in the current frame, or
the implicit outermost region), a framed flag (whether an unreturned
CALLSUB is on the path), and a record of the immediately preceding
PUSH. The traversal is seeded at PC 0 with stack offset 0, in the
outermost region, unframed. Each instruction is expanded once: the first
visit records its stack offset, entry, and framed flag, and every
later arrival must agree with all three or validation fails. This is
Constraint 5's path-independence, strengthened to require a common baseline
— paths may not merge unless the same entry governs them.
At each reachable instruction the validator enforces: the opcode is valid and
non-deprecated (Constraint 1); JUMP, JUMPI, and CALLSUB are immediately
preceded by a PUSH giving a destination of the required type (Constraints
2, 3), checked directly if the destination is already visited and otherwise
recorded in required_at[] and enforced on first visit; and the
instruction's stack effect raises its entry's inputs — the greatest
number of items the region uses from its caller's stack, below its
baseline — and its stack growth — the greatest offset it reaches above
it (Constraint 4). These, with the entry's net stack effect (hereafter
its net effect; Constraint 5) and its call depth — the greatest
return-stack growth while executing its region — are the four summaries
the validator computes per entry.
The three subroutine instructions receive specific handling:
ENTERSUB resets the baseline: it is always visited in the canonical
state — stack offset 0, itself the entry. An arrival without a call
— by fall-through or by jump — at offset d records an enter edge: the arriving entry's net effect is d plus this
entry's, composing net effects across multiple entry points, and its
inputs are at least this entry's inputs minus d.
CALLSUB records a call edge (for the summaries, likewise) and seeds
the callee in its canonical state, framed. The return point — the next
instruction, at the call-site stack offset plus the callee's
net effect — is enqueued as soon as that net effect is known:
immediately if already resolved, otherwise it is parked on the callee's
pending list.
RETURNSUB must be framed: a matching CALLSUB on every path, since
an unmatched RETURNSUB would underflow the return stack (Constraint 4).
It resolves its entry's net effect as the current stack offset, or
checks agreement with the already-resolved value (Constraint 5).
Resolving an entry releases its pending return points and, in
cascade, resolves the entries that enter it without a call.
A subroutine that never returns leaves its callers' return points pending forever: they are unreachable, and correctly never validated.
After the traversal, the summaries propagate over the recorded edges from child to parent — the child being the callee of a call edge, or the entry entered by an enter edge; the parent, the region that called or entered it: inputs(parent) ≥ inputs(child) − offset at the edge; stack growth(parent) ≥ offset + stack growth(child); call depth(parent) ≥ call depth(child), plus one frame per call edge. The entry graph — the regions, connected by these edges — is sorted topologically. If it is acyclic — the program is not recursive — one pass in topological order computes the summaries exactly, and the outermost region's stack growth and call depth must not exceed 1024: the overflow bounds are decided statically. A cycle in the graph is recursion: overflow is then left to the runtime checks — the "absence of recursion" qualifier on the overflow guarantee — and inputs are resolved by a worklist relaxation instead. In either case the outermost region's inputs must be zero — top-level code has no caller — and inputs above 1024, as when recursion consumes caller stack on each cycle, are rejected.
Falling past the end of the code is an implicit STOP and terminates that
path validly. Bytes never reached by the traversal are data: never
examined, never constrained. A destination inside PUSH immediates or
other data fails Constraint 1 or the destination-type check when visited.
Each instruction is expanded once, each expansion enqueues at most two continuations and records at most one edge or pending return point, and each entry resolves once, so the traversal runs in time and space linear in code size. The propagation of the summaries is a topological pass, one relaxation per edge; under recursion the inputs relaxation re-visits an entry only when its inputs strictly increase, at most 1024 times — a protocol constant — so the whole validation is linear in code size, worst case.
Validated contracts are more secure than ordinary contracts: they cannot execute invalid instructions, jump to invalid locations, underflow stack, or, in the absence of recursion, overflow stack. And their return addresses are isolated from the data stack, so code cannot corrupt its own control flow.
The canonical validation contract is consensus-critical, and correcting a faulty validator is hard: invalid contracts it admitted are already on the blockchain and cannot be removed. A mechanism to retroactively invalidate them may be needed; like the header layout, it is deferred. (Fork-driven changes to validity — see Validation — need no such mechanism: contracts validated under earlier forks simply remain deployed.)
Validation is linear in the size of the code and its gas is paid by the creator, so it cannot be used to amplify work.
Copyright and related rights waived via CC0.