Update EIP-3540: Move to Review

EIPS/eip-3540.md

@@ -110,28 +110,29 @@ header :=
     kind_data, data_size,
     terminator
 body := types_section, code_section+, container_section*, data_section
-types_section := (inputs, outputs, max_stack_height)+
+types_section := (inputs, outputs, max_stack_increase)+
 ```
 
 *note: `,` is a concatenation operator, `+` should be interpreted as "one or more" of the preceding item, `*` should be interpreted as "zero or more" of the preceding item, and `[item]` should be interpreted as an optional item.*
 
 #### Header
 
-| name                   | length   | value         | description                                                                                                  |
-|------------------------|----------|---------------|--------------------------------------------------------------------------------------------------------------|
-| magic                  | 2 bytes  | 0xEF00        |                                                                                                              |
-| version                | 1 byte   | 0x01          | EOF version                                                                                                  |
-| kind_type              | 1 byte   | 0x01          | kind marker for type section                                                                                 |
-| type_size              | 2 bytes  | 0x0004-0x1000 | 16-bit unsigned big-endian integer denoting the length of the type section content, 4 bytes per code section |
-| kind_code              | 1 byte   | 0x02          | kind marker for code size section                                                                            |
-| num_code_sections      | 2 bytes  | 0x0001-0x0400 | 16-bit unsigned big-endian integer denoting the number of the code sections                                  |
-| code_size              | 2 bytes  | 0x0001-0xFFFF | 16-bit unsigned big-endian integer denoting the length of the code section content                           |
-| kind_container         | 1 byte   | 0x03          | kind marker for container size section                                                                       |
-| num_container_sections | 2 bytes  | 0x0001-0x0100 | 16-bit unsigned big-endian integer denoting the number of the container sections                             |
-| container_size         | 2 bytes  | 0x0001-0xFFFF | 16-bit unsigned big-endian integer denoting the length of the container section content                      |
-| kind_data              | 1 byte   | 0x04          | kind marker for data size section                                                                            |
-| data_size              | 2 bytes  | 0x0000-0xFFFF | 16-bit unsigned big-endian integer denoting the length of the data section content (*)                       |
-| terminator             | 1 byte   | 0x00          | marks the end of the header                                                                                  |
+| name                   | length  | value                 | description                                                                                                  |
+|------------------------|---------|-----------------------|--------------------------------------------------------------------------------------------------------------|
+| magic                  | 2 bytes | 0xEF00                |                                                                                                              |
+| version                | 1 byte  | 0x01                  | EOF version                                                                                                  |
+| kind_type              | 1 byte  | 0x01                  | kind marker for type section                                                                                 |
+| type_size              | 2 bytes | 0x0004-0x1000         | 16-bit unsigned big-endian integer denoting the length of the type section content, 4 bytes per code section |
+| kind_code              | 1 byte  | 0x02                  | kind marker for code size section                                                                            |
+| num_code_sections      | 2 bytes | 0x0001-0x0400         | 16-bit unsigned big-endian integer denoting the number of the code sections                                  |
+| code_size              | 2 bytes | 0x0001-0xFFFF         | 16-bit unsigned big-endian integer denoting the length of the code section content                           |
+| kind_container         | 1 byte  | 0x03                  | kind marker for container size section                                                                       |
+| num_container_sections | 2 bytes | 0x0001-0x0100         | 16-bit unsigned big-endian integer denoting the number of the container sections                             |
+| container_size         | 4 bytes | 0x00000001-0xFFFFFFFF | 32-bit unsigned big-endian integer denoting the length of the container section content                      |
+| <kind_reserved>        | 1 byte  | 0x04                  | old kind maker for data section size. This section kind should not be reused.                                |
+| kind_data              | 1 byte  | 0xff                  | kind marker for data size section                                                                            |
+| data_size              | 2 bytes | 0x0000-0xFFFF         | 16-bit unsigned big-endian integer denoting the length of the data section content (*)                       |
+| terminator             | 1 byte  | 0x00                  | marks the end of the header                                                                                  |
 
 (*) For not yet deployed containers this can be greater than the actual content length.
 
@@ -142,7 +143,7 @@ types_section := (inputs, outputs, max_stack_height)+
 | types_section     | variable | n/a           | stores code section metadata                                                               |
 | inputs            | 1 byte   | 0x00-0x7F     | number of stack elements the code section consumes                                         |
 | outputs           | 1 byte   | 0x00-0x7F     | number of stack elements the code section returns                                          |
-| max_stack_height  | 2 bytes  | 0x0000-0x03FF | maximum number of elements ever placed onto the operand stack by the code section          |
+| max_stack_increase       | 2 bytes  | 0x0000-0x03FF | Additional number of elements ever placed onto the operand stack by the code section       |
 | code_section      | variable | n/a           | arbitrary bytecode                                                                         |
 | container_section | variable | n/a           | arbitrary EOF-formatted container                                                          |
 | data_section      | variable | n/a           | arbitrary sequence of bytes                                                                |

EIPS/eip-4750.md

@@ -32,7 +32,9 @@ Furthermore, it aims to improve analysis opportunities by encoding the number of
 The type section of EOF containers must adhere to following requirements:
 
 1. The section is comprised of a list of metadata where the metadata index in the type section corresponds to a code section index. Therefore, the type section size MUST be `n * 4` bytes, where `n` is the number of code sections.
-2. Each metadata item has 3 attributes: a uint8 `inputs`, a uint8 `outputs`, and a uint16 `max_stack_height`. *Note:* This implies that there is a limit of 255 stack for the input and in the output. This is further restricted to 127 stack items, because the upper bit of both the input and output bytes are reserved for future use (`outputs == 0x80` is already used in EOF1 to denote non-returning functions, as introduced in a separate EIP). `max_stack_height` is further defined in [EIP-5450](./eip-5450.md).
+2. Each metadata item has 3 attributes: a uint8 `inputs`, a uint8 `outputs`, and a uint16 `max_stack_increase`\
+  *Note:* This implies that there is a limit of 255 stack for the input and in the output. This is further restricted to 127 stack items, because the upper bit of both the input and output bytes are reserved for future use (`outputs == 0x80` is already used in EOF1 to denote non-returning functions, as introduced in a separate EIP). `max_stack_increase` is further defined in [EIP-5450](./eip-5450.md).\
+  *Note:* [EIP-5450](./eip-5450.md) will perform stack validation that will ensure `output` is less than or equal to `inputs` + `max_stack_increase`
 3. The 0th code section MUST have 0 inputs and 0 outputs.
 
 Refer to [EIP-3540](./eip-3540.md) to see the full structure of a well-formed EOF bytecode.
@@ -60,15 +62,15 @@ First we define several helper values:
 
 - `type[i].inputs = type_section_contents[i * 4]` - number of inputs of ith code section
 - `type[i].outputs = type_section_contents[i * 4 + 1]` - number of outputs of ith code section
-- `type[i].max_stack_height = type_section_contents[i * 4 + 2:i * 4 + 4]` - maximum operand stack height of ith code section
+- `type[i].max_stack_increase = type_section_contents[i * 4 + 2:i * 4 + 4]` - extra operand stack height in excess of inputs of ith code section
 
 If the code is valid EOF1, the following execution rules apply:
 
 #### `CALLF`
 
 1. Has one immediate argument,`target_section_index`, encoded as a 16-bit unsigned big-endian value.
 2. *Note:* EOF validation [EIP-5450](./eip-5450.md) guarantees that operand stack has enough items to use as callee's inputs.
-3. If operand stack size exceeds `1024 - type[target_section_index].max_stack_height + type[target_section_index].inputs` (i.e. if the called function may exceed the global stack height limit), execution results in exceptional halt. This also guarantees that the stack height after the call is within the limits.
+3. If operand stack size exceeds `1024 - type[target_section_index].max_stack_increase` (i.e. if the called function may exceed the global stack height limit), execution results in exceptional halt. This also guarantees that the stack height after the call is within the limits.
 4. If return stack already has `1024` items, execution results in exceptional halt.
 5. Charges 5 gas.
 6. Pops nothing and pushes nothing to operand stack.

EIPS/eip-5450.md

@@ -59,9 +59,9 @@ In the second validation phase control-flow analysis is performed on the code.
 *Terminating instructions* refers to the instructions either:
 
 - ending function execution: `RETF`, `JUMPF`, or
-- ending call frame execution: `STOP`, `RETURN`, `RETURNCONTRACT`, `REVERT`, `INVALID`.
+- ending call frame execution: `STOP`, `RETURN`, `RETURNCODE`, `REVERT`, `INVALID`.
 
-*note: `JUMPF` and `RETURNCONTRACT` are introduced in separate EIPs.*
+*note: `JUMPF` and `RETURNCODE` are introduced in separate EIPs.*
 
 *Forward jump* refers to any of `RJUMP`/`RJUMPI`/`RJUMPV` instruction with relative offset greater than or equal to 0. *Backwards jump* refers to any of `RJUMP`/`RJUMPI`/`RJUMPV` instruction with relative offset less than 0, including jumps to the same jump instruction.
 
@@ -81,7 +81,7 @@ For each instruction:
       - 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 recorded 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.
+   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_increase`, validation fails.
    3. Compute new stack height bounds after the instruction execution. Upper and lower bound are updated by the same value:
       - after `CALLF` stack height bounds are adjusted by adding `types[target_section_index].outputs - types[target_section_index].inputs`,
       - after any other non-terminating instruction stack height bounds are adjusted by subtracting the number of instruction inputs and adding the number of instruction outputs,
@@ -100,7 +100,7 @@ After all instructions are visited, determine the function maximum operand stack
 
 1. Compute the maximum stack height as the maximum of all recorded stack height upper bounds.
 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.
+3. **Check** if the maximum stack height matches the corresponding code section's maximum stack height (which is `inputs` + `max_stack_increase`) within the type section.
 
 The computational and space complexity of this pass is *O(len(code))*. Each instruction is visited at most once.
 
@@ -124,7 +124,7 @@ Any code section validated according to operand stack validation has the followi
 
 ### Stack overflow check only in CALLF/JUMPF
 
-In this EIP, we provide a more efficient variant of the EVM where stack overflow check is performed only in `CALLF` and `JUMPF` instructions using the called function's `max_stack_height` information. This decreases flexibility of an EVM program because `max_stack_height` corresponds to the worst-case control-flow path in the function.
+In this EIP, we provide a more efficient variant of the EVM where stack overflow check is performed only in `CALLF` and `JUMPF` instructions using the called function's `inputs` and `max_stack_increase` information. This decreases flexibility of an EVM program because the calculated maximum stack corresponds to the worst-case control-flow path in the function.
 
 ### Unreachable code
 

EIPS/eip-6206.md

@@ -38,7 +38,7 @@ The first code section MUST have 0 inputs and be non-returning.
 A new instruction, `JUMPF (0xe5)`, is introduced.
 
 1. `JUMPF` has one immediate argument, `target_section_index`, encoded as a 16-bit unsigned big-endian value.
-2. If the operand stack size exceeds `1024 - type[target_section_index].max_stack_height + type[target_section_index].inputs` (i.e. if the called function may exceed the global stack height limit), execution results in an exceptional halt. This guarantees that the target function does not exceed global stack height limit.
+2. If the operand stack size exceeds `1024 - type[target_section_index].max_stack_increase (i.e. if the called function may exceed the global stack height limit), execution results in an exceptional halt. This guarantees that the target function does not exceed global stack height limit.
 3. `JUMPF` sets `current_section_index` to `target_section_index` and `PC` to `0`, but does not change the return stack. Execution continues in the target section. 
 4. `JUMPF` costs 5 gas.
 5. `JUMPF` neither pops nor pushes anything to the operand stack.
@@ -54,7 +54,7 @@ Let the definition of `type[i]` be inherited from [EIP-4750](./eip-4750.md) and
 * The stack height validation at `JUMPF` depends on whether the target section is non-returning:
   * `JUMPF` into returning section (`type[target_section_index].outputs` does not equal `0x80`):  `stack_height_min` and `stack_height_max` MUST be equal to `type[current_section_index].outputs - type[target_section_index].outputs + type[target_section_index].inputs`. This means that target section can output less stack elements than the original code section called by the top element on the return stack, if the current code section leaves the delta `type[current_section_index].outputs - type[target_section_index].outputs` element(s) on the stack.
   * `JUMPF` into non-returning section (`type[target_section_index].outputs` equals `0x80`): `stack_height_min` MUST be greater than or equal to `type[target_section_index].inputs`.
-* Stack overflow check at `JUMPF`: `stack_height_max` MUST be less than or equal to `1024 - types[target_section_index].max_stack_height + types[target_section_index].inputs`.
+* Stack overflow check at `JUMPF`: `stack_height_max` MUST be less than or equal to `1024 - types[target_section_index].max_stack_increase`.
 * `JUMPF` is considered terminating instruction, i.e. does not have successor instructions in code validation and MAY be final instruction in the section. 
 * The code validation defined in [EIP-4200](./eip-4200.md) also fails if any `RJUMP*` offset points to one of the two bytes directly following a `JUMPF` instruction.