Update EIP-5450: Align with EOF megaspec #8388

gumb0 · 2024-04-04T12:56:58Z

Stack validation algorithm is updated to be less restrictive.

eth-bot · 2024-04-04T12:57:26Z

✅ All reviewers have approved.

pdobacz

LGTM, I left some comments. However, I would still opt for not mentioning JUMPF. To me it seems it can just be left out and this EIP is well formed. EIP-6206 does a good job in building upon this foundation. To add to this, mentioning JUMPF requires referencing EIP-6206, we should not weasel around it, and then if we do mention, we get more circular deps :(

pdobacz · 2024-04-04T13:31:34Z

EIPS/eip-5450.md

+      - for any other instruction the recodrded stack height lower bound must be at least the number of inputs required by instruction
+      -  there is no additional check for terminating instructions other than `RETF` and `JUMPF`, this implies that extra items left on stack at instruction ending EVM execution are allowed.
+   2. For `CALLF` and `JUMPF` **check** for possible stack overflow: if recorded stack height upper bound is greater than `1024 - types[target_section_index].max_stack_height + types[target_section_index].inputs`, validation fails.
+   3. Compute new stack height bounds after the instruction execution. Upper and lower bound are updated by the same value.


specify the value of the update, esp. for CALLF

pdobacz · 2024-04-04T13:33:09Z

EIPS/eip-5450.md

-      2. Add the instruction to the *worklist*.
-   3. Otherwise, **check** if the recorded stack height equals the value computed in 1.2.
+   2. If the successor is reached via forwards jump or sequential flow from previous instruction:
+      1. If the instruction does not have stack height bounds recorded (visited for the first time), record the instruction stack height bound as the value computed in 2.2.


Suggested change

1. If the instruction does not have stack height bounds recorded (visited for the first time), record the instruction stack height bound as the value computed in 2.2.

1. If the instruction does not have stack height bounds recorded (visited for the first time), record the instruction stack height bound as the value computed in 2.3.

pdobacz · 2024-04-04T13:33:57Z

EIPS/eip-5450.md

-   3. Otherwise, **check** if the recorded stack height equals the value computed in 1.2.
+   2. If the successor is reached via forwards jump or sequential flow from previous instruction:
+      1. If the instruction does not have stack height bounds recorded (visited for the first time), record the instruction stack height bound as the value computed in 2.2.
+      2. Otherwise instruction was already visited (by previously seen forward jump). Update this instruction's recorded stack height bounds so that they contain the bounds computed in 2.2, i.e. `target_stack_min = min(target_stack_min, current_stack_min)` and `target_stack_max = max(target_stack_max, current_stack_min)`, where `(target_stack_min, target_stack_max)` are successor bounds and `(current_stack_min, current_stack_max)` are bounds computed in 2.2.


Suggested change

2. Otherwise instruction was already visited (by previously seen forward jump). Update this instruction's recorded stack height bounds so that they contain the bounds computed in 2.2, i.e. `target_stack_min = min(target_stack_min, current_stack_min)` and `target_stack_max = max(target_stack_max, current_stack_min)`, where `(target_stack_min, target_stack_max)` are successor bounds and `(current_stack_min, current_stack_max)` are bounds computed in 2.2.

2. Otherwise instruction was already visited (by previously seen forward jump). Update this instruction's recorded stack height bounds so that they contain the bounds computed in 2.3, i.e. `target_stack_min = min(target_stack_min, current_stack_min)` and `target_stack_max = max(target_stack_max, current_stack_min)`, where `(target_stack_min, target_stack_max)` are successor bounds and `(current_stack_min, current_stack_max)` are bounds computed in 2.3.

some more occurrences of this below

pdobacz · 2024-04-04T13:37:08Z

EIPS/eip-5450.md

-      - for `RETF` instruction the recorded stack height must be exactly the number of outputs of the function matching the code.
-   2. Compute new stack height after the instruction execution.
-2. Determine the list of successor instructions that can follow the current instructions:
+1. **Check** if this instruction has recorded stack height bounds. If it does not, it means it was neither referenced by previous forward jump, nor is part of sequential instruction flow, and this code fails validation. 


We should mention the ordering of blocks as in eof.md, somewhere above: "Code basic blocks must be ordered in a way that every block is reachable either by a forward jump or sequential flow of instructions. In other words, there is no basic block reachable only by a backward jump."

I mentioned it, but decided to put it into as a sub-point.

It feels not as important for implementers of the algorithm, and mainly important for code generators, so I thought it fits as a note. wdyt?

totally can be a note 👍

pdobacz · 2024-04-04T13:37:41Z

EIPS/eip-5450.md

   2. **Check** if the maximum stack height does not exceed the limit of 1023 (`0x3FF`).
   3. **Check** if the maximum stack height matches the corresponding code section's `max_stack_height` within the type section.

 The computational and space complexity of this pass is *O(len(code))*. Each instruction is visited at most once.

 ### Execution

-Given the deploy-time validation guarantees, an EVM implementation is not required anymore to have run-time stack underflow nor overflow checks for each executed instruction. The exception is the `CALLF` performing operand stack overflow check for the entire called function.
+Given the deploy-time validation guarantees, an EVM implementation is not required anymore to have run-time stack underflow nor overflow checks for each executed instruction. The exception is the `CALLF` and `JUMPF` performing operand stack overflow check for the entire called function.

 ## Rationale


Once we're done with the specifications part, needs adding justification of going down the relaxed validation path

Added in Rationale.

Spec out new stack validation algorithm.

github-actions · 2024-04-11T13:32:11Z

The commit cdc54ac (as a parent of 09172eb) contains errors.
Please inspect the Run Summary for details.

pdobacz

Nice, just some nitpicks/suggestions to consider

pdobacz · 2024-04-15T08:06:43Z

EIPS/eip-5450.md

@@ -27,14 +27,16 @@ and preventing the execution and deployment of any invalid code.
 The operand stack validation provides several benefits:

 - removes the run-time stack underflow check for all instructions,
- removes the run-time stack overflow check for all instruction except `CALLF`,
+- removes the run-time stack overflow check for all instructions except `CALLF` and `JUMPF`,


reference a "separate EIP" for JUMPF, like in 4750?

pdobacz · 2024-04-15T08:11:09Z

EIPS/eip-5450.md

+- allows for multiple forward jump instructions executing at different stack heights to target the same instruction; the stack of target basic stack is validated for all possible heights,
+- does not allow backwards jump instructions to target an instruction, that can be executed with different stack height; this prevents deployment of the loops with unbounded stack pushing or popping,


these two bullets belong more in the Rationale section IMO, unless they are already covered there. At most this "prevents deployment of the loops with unbounded stack pushing or popping" sentence is a Motivation of the EIP as a whole.

I just wanted to have a neat list of all code properties achieved by validation. I put it now into Rationale, but this way it duplicates a bit what is said in other parts, ptal

IMO, much better this way, thank you. Allowing for "multiple forwards jump instructions... etc" sounded weird in Motivation, as it is possible with dynamic JUMP. As such, it is motivation for choosing a certain design over alternatives, rather than the entire EIP over status quo.

pdobacz · 2024-04-15T08:12:40Z

EIPS/eip-5450.md

@@ -58,50 +60,59 @@ In the second validation phase control-flow analysis is performed on the code.

 *Terminating instructions* refers to the instructions either:

- ending function execution: `RETF`, or
- ending whole EVM execution: `STOP`, `RETURN`, `REVERT`, `INVALID`.
+- ending function execution: `RETF`, `JUMPF`, or


"separate EIP" again, the following ones are OK to not have it, but at least once for the Spec section is good to have

should RETURNCONTRACT mention have the same then?

oh boy, I've missed RETURNCONTRACT popping up here... my top-level opinion doesn't really change (should not mention at all), but if we mention, we should consistent in how we mention :(. We cannot leave the reader puzzled whether RETURNCONTRACT is something in legacy EVM, a typo, copy-pasta or leftovers from prev revision or whatnot.

But once more, I really think these EIPs should be as independent as possible, rather than trying to be the megaspec and cover all aspects in each thoroughly

eth-bot

All Reviewers Have Approved; Performing Automatic Merge...

rodiazet · 2024-04-16T11:46:15Z

EIPS/eip-5450.md

+      - for `JUMPF` into non-returning function the recorded stack height lower bound must be at least the number of inputs of the target function according to its type defined in the type section,
+      - for any other instruction the recodrded stack height lower bound must be at least the number of inputs required by instruction,
+      - there is no additional check for terminating instructions other than `RETF` and `JUMPF`, this implies that extra items left on stack at instruction ending EVM execution are allowed.
+   2. For `CALLF` and `JUMPF` **check** for possible stack overflow: if recorded stack height upper bound is greater than `1024 - types[target_section_index].max_stack_height + types[target_section_index].inputs`, validation fails.


It should be inside 2.1 check list.

2.1 are the checks that guarantee no stack underflow,
2.2 is the check that prevents (some) stack overflows.

eth-bot

All Reviewers Have Approved; Performing Automatic Merge...

github-actions bot added c-update Modifies an existing proposal s-review This EIP is in Review t-core labels Apr 4, 2024

github-actions bot added the w-ci Waiting on CI to pass label Apr 4, 2024

gumb0 force-pushed the update-eip-5450 branch from be4300d to d7879cb Compare April 4, 2024 13:08

pdobacz reviewed Apr 4, 2024

View reviewed changes

gumb0 force-pushed the update-eip-5450 branch 2 times, most recently from 56474fc to df368b7 Compare April 4, 2024 14:24

Gemrav approved these changes Apr 4, 2024

View reviewed changes

Update EIP-5450: Align with EOF megaspec

d0204b3

Spec out new stack validation algorithm.

gumb0 force-pushed the update-eip-5450 branch from df368b7 to d0204b3 Compare April 5, 2024 15:09

github-actions bot removed the w-ci Waiting on CI to pass label Apr 5, 2024

Mention ordering of basic blocks as a prerequisite to the algorithm

5de2cbb

github-actions bot added the w-ci Waiting on CI to pass label Apr 10, 2024

gumb0 added 2 commits April 11, 2024 15:04

Add motivation for new algorithm

54a21bd

Specify how stack height is updated on regular instruction flow

cdc54ac

Fix linter errors

6c9f4a3

github-actions bot removed the w-ci Waiting on CI to pass label Apr 11, 2024

gumb0 force-pushed the update-eip-5450 branch from e96d37f to 1060e8e Compare April 12, 2024 13:04

Add two new properties to motivation benefit list

245d5fa

gumb0 force-pushed the update-eip-5450 branch from 1060e8e to 245d5fa Compare April 12, 2024 13:06

Minor polishing

460f1e5

gumb0 requested a review from pdobacz April 12, 2024 13:21

pdobacz approved these changes Apr 15, 2024

View reviewed changes

gumb0 added 3 commits April 15, 2024 14:35

Mention that JUMPF and RETURNCONTRACT are introduced separately

2770e16

Create a section in Rationale with all achieved code properties

6cada0e

Define forward/backwards jump

d20149c

pdobacz approved these changes Apr 16, 2024

View reviewed changes

gumb0 marked this pull request as ready for review April 16, 2024 10:55

gumb0 requested a review from eth-bot as a code owner April 16, 2024 10:55

gumb0 closed this Apr 16, 2024

gumb0 reopened this Apr 16, 2024

eth-bot enabled auto-merge (squash) April 16, 2024 12:11

eth-bot approved these changes Apr 16, 2024

View reviewed changes

rodiazet reviewed Apr 16, 2024

View reviewed changes

eth-bot approved these changes Apr 16, 2024

View reviewed changes

eth-bot merged commit be23113 into ethereum:master Apr 16, 2024
28 checks passed

gumb0 deleted the update-eip-5450 branch April 16, 2024 12:21

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update EIP-5450: Align with EOF megaspec #8388

Update EIP-5450: Align with EOF megaspec #8388

gumb0 commented Apr 4, 2024

eth-bot commented Apr 4, 2024 •

edited

Loading

pdobacz left a comment

pdobacz Apr 4, 2024

gumb0 Apr 12, 2024

pdobacz Apr 4, 2024

gumb0 Apr 12, 2024

pdobacz Apr 4, 2024

pdobacz Apr 4, 2024

gumb0 Apr 12, 2024

pdobacz Apr 15, 2024

pdobacz Apr 4, 2024

gumb0 Apr 12, 2024

github-actions bot commented Apr 11, 2024

pdobacz left a comment

pdobacz Apr 15, 2024

pdobacz Apr 15, 2024

gumb0 Apr 16, 2024

pdobacz Apr 16, 2024

pdobacz Apr 15, 2024

gumb0 Apr 15, 2024

pdobacz Apr 15, 2024

eth-bot left a comment

rodiazet Apr 16, 2024

gumb0 Apr 16, 2024

rodiazet Apr 16, 2024

eth-bot left a comment

	1. If the instruction does not have stack height bounds recorded (visited for the first time), record the instruction stack height bound as the value computed in 2.2.
	1. If the instruction does not have stack height bounds recorded (visited for the first time), record the instruction stack height bound as the value computed in 2.3.

		- allows for multiple forward jump instructions executing at different stack heights to target the same instruction; the stack of target basic stack is validated for all possible heights,
		- does not allow backwards jump instructions to target an instruction, that can be executed with different stack height; this prevents deployment of the loops with unbounded stack pushing or popping,

Update EIP-5450: Align with EOF megaspec #8388

Update EIP-5450: Align with EOF megaspec #8388

Conversation

gumb0 commented Apr 4, 2024

eth-bot commented Apr 4, 2024 • edited Loading

pdobacz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

github-actions bot commented Apr 11, 2024

pdobacz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eth-bot left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eth-bot left a comment

Choose a reason for hiding this comment

eth-bot commented Apr 4, 2024 •

edited

Loading