Update EIP-6206: adjust for new stack validation algorithm

Merged by EIP-Bot.

EIPS/eip-6206.md

@@ -45,21 +45,22 @@ A new instruction, `JUMPF (0xe5)`, is introduced.
 
 ### Code Validation
 
-Let the definition of `type[i]` be inherited from [EIP-4750](./eip-4750.md) and define `stack_height` to be the height of the stack at a certain instruction during the instruction flow traversal if the operand stack at the start of the function were equal to `type[i].inputs`.
+Let the definition of `type[i]` be inherited from [EIP-4750](./eip-4750.md) and define `stack_height_min` and `stack_height_max` to be the stack height bounds at a certain instruction during the instruction flow traversal.
 
 * The immediate argument of `JUMPF` MUST be less than the total number of code sections.
 * For each `JUMPF` instruction:
   * either `type[current_section_index].outputs` MUST be greater or equal `type[target_section_index].outputs`,
   * or `type[target_section_index].outputs` MUST be `0x80`
 * 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 MUST be equal to `type[current_section_index].outputs + type[target_section_index].inputs  - type[target_section_index].outputs`. 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 must be greater or equal than `type[target_section_index].inputs`.
+  * `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].inputs  - type[target_section_index].outputs`. 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`.
 * `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.
 
 `CALLF` instruction validation is extended to include the rule:
 
-* Code section is invalid in case an immediate argument `target_section_index` of any `CALLF` targets a non-returning section, i.e. `type[target_section_index` equals `0x80`.
+* Code section is invalid in case an immediate argument `target_section_index` of any `CALLF` targets a non-returning section, i.e. `type[target_section_index]` equals `0x80`.
 
 #### Non-returning status validation