Update EIP-6888: Move to Draft

Merged by EIP-Bot.

EIPS/eip-6888.md

@@ -1,18 +1,18 @@
 ---
 eip: 6888
-title: Math checking in EVM
-description: Check for math underflows overflows and division by zero at EVM level
+title: Arithmetic verification at EVM level
+description: Check for math overflows and division by zero at EVM level
 author: Renan Rodrigues de Souza (@RenanSouza2)
 discussions-to: https://ethereum-magicians.org/t/eip-math-checking/13846
-status: Stagnant
+status: Draft
 type: Standards Track
 category: Core
 created: 2023-04-16
 ---
 
 ## Abstract
 
-This EIP adds many checks to EVM arithmetic and a new opcode to get the corresponding flags and clear them. The list of check includes underflows, overflows, division by zero.
+This EIP adds arithmetics checks to EVM arithmetic and a new opcode jump conditionally if there were events. The list of check includes overflows, division by zero.
 
 ## Motivation
 
@@ -26,10 +26,11 @@ Starting from `BLOCK_TIMESTAMP >= HARDFORK_TIMESTAMP`
 
 ### Constants
 
-|     Constant        | Type      | Value         |
-| ------------------- | --------- |:------------- |
-| `INT_MIN`           | `int`     | -(2**255)     |
-| `UINT_MAX`          | `uint`    | 2 ** 256      |
+|     Constant         | Type      | Value     |
+| -------------------- | --------- | --------- |
+| `HARDFORK_TIMESTAMP` | `uint64`  | `TBD`     |
+| `UINT_MAX`           | `uint256` | `2 ** 256 - 1` |
+| `INT_MIN`            | `int256`  | `-(2**255)` |
 
 ### Flags
 
@@ -38,39 +39,49 @@ Starting from `BLOCK_TIMESTAMP >= HARDFORK_TIMESTAMP`
 | `carry`             | `bool`    | false         |
 | `overflow`          | `bool`    | false         |
 
-Two new flags are added to the EVM state: unsigned error (`carry`) and signed error (`overflow`). The scope of those flags are the same as the program counter. Each frame of execution has their own flags. At the frame creation they are unset and they are updated in call.
+Two new flags are added to the EVM state: unsigned warning (`carry`) and signed warning (`overflow`). The scope of those flags are the same as the program counter.
+
+### Definitions
 
 From this point forward  `a`, `b` and `c` references the arguments in a math operation and `res` the output. `c` is only used if the operation takes 3 inputs.
 
+The function `sign(x)` is defined in the set of `uint256 -> {NEGATIVE, ZERO, POSITIVE}`
+
+### Contidions
+
 The `carry` flag MUST be set in the following circumstances:
 
  - When opcode is `ADD` (`0x01`) and `res < a`
  - When opcode is `MUL` (`0x02`) and `a != 0 ∧ res / a != b`
  - When opcode is `SUB` (`0x03`) and `b > a`
  - When opcode is `DIV` (`0x04`) or `MOD` (`0x06`); and `b == 0`
- - When opcode is `ADDMOD` (`0x08`) and `c == 0 ∨ ((a + b) / UINT_MAX > c)`
- - When opcode is `MULMOD` (`0x08`) and `c == 0 ∨ ((a * b) / UINT_MAX > c)`
- - When opcode is `EXP` (`0x0A`) and ideal `a ** b > UINT_MAX`
+ - When opcode is `ADDMOD` (`0x08`) and `c == 0`
+ - When opcode is `MULMOD` (`0x08`) and `c == 0`
+ - When opcode is `EXP` (`0x0A`) and `a ** b > UINT_MAX`
  - When opcode is `SHL` (`0x1b`) and `res >> a != b`
 
-The `overflow` flag is MUST set in the following circumstances:
+The `overflow` flag MUST be set in the following circumstances:
 
- - When opcode is `SUB` (`0x03`) and `a != 0 ∧ sgn(a) != sgn(b) ∧ sgn(b) == sgn(res)`
- - When opcode is `ADD` (`0x01`) and `a != 0 ∧ sgn(a) == sgn(b) ∧ sgn(a) != sgn(res)` 
+ - When opcode is `ADD` (`0x01`) and `a != 0 ∧ b != 0 ∧ sign(a) == sign(b) ∧ sign(a) != sign(res)`
+ - When opcode is `SUB` (`0x03`) and `(a != 0 ∧ b != 0 ∧ sign(a) != sign(b) ∧ sign(a) != sign(res)) ∨ (a == 0 ^ b == INT_MIN)`
  - When opcode is `MUL` (`0x02`) and `(a == -1 ∧ b == INT_MIN) ∨ (a == INT_MIN ∧ b == -1) ∨ (a != 0 ∧ (res / a != b))` (this `/` represents `SDIV`)
  - When opcode is `SDIV` (`0x05`)  or `SMOD` (`0x06`); and `b == 0 ∨ (a == INT_MIN ∧ b == -1)`
  - When opcode is `SHL` (`0x1b`) and `res >> a != b` (this `>>` represents `SAR`)
 
-The function `sgn(num)` returns the sign of the number, it can be negative, zero or positive.
+### Opcodes
+
+#### `JUMPC`
 
-| Value | Mnemonic | δ | α | Description |
-|-------|----------|---|---|---------------------------------------------------------------------------------------|
-| `JUMPC` | `0x5B` | 1 | 0 | Conditionally alter the program counter.
-|||||```J_JUMPC = carry ? µ_s[0] : µ_pc + 1```
-|||||```carry = overflow = false``` |
-| `JUMPO` | `0x5C` | 1 | 0 | Conditionally alter the program counter.
-|||||```J_JUMPO = ovewrflow ? µ_s[0] : µ_pc + 1```
-|||||```carry = overflow = false``` |
+Consumes one argument from the stack, the possible pc dest,
+Conditionally alter the program counter depending on the `carry` flag. `J_JUMPC = carry ? µ_s[0] : µ_pc + 1` 
+Clears both flags. `carry = overflow = false`
+
+
+#### `JUMPO`
+
+Consumes one argument from the stack, the possible pc dest,
+Conditionally alter the program counter depending on the `ovewflow` flag. `J_JUMPO = carry ? µ_s[0] : µ_pc + 1` 
+Clears both flags. `carry = overflow = false`
 
 ### gas
 
@@ -82,8 +93,6 @@ EVM uses two's complement for negative numbers. The opcodes listed above trigger
 
 The conditions described for each opcode is made with implementation friendliness in mind. The only exception is EXP as it is hard to give a concise test as most of the others relied on the inverse operation and there is no native `LOG`. Most `EXP` implementations will internally use `MUL` so the flag `carry` can be drawn from that instruction, not the `overflow`.
 
-The divisions by `UINT_MAX` used in the `ADDMOD` and `MULMOD` is another way to represent the higher 256 bits of the internal 512 number representation.
-
 Both flags are cleaned at the same time because the instructions are expected to be used when transitioning between codes where numbers are treated as signed or unsigned.
 
 ## Backwards Compatibility