# Math checking in EVM

EIP-6888, titled "Math checking in EVM," proposes the addition of checks in the Ethereum Virtual Machine (EVM) for arithmetic underflows, overflows, and division by zero. The proposal introduces two new flags to the EVM state: unsigned error (carry) and signed error (overflow). Each frame of execution has its own flags, which are unset at the frame creation and updated in call.
The proposal also introduces two new opcodes, JUMPC and JUMPO, which conditionally alter the program counter and clear the carry and overflow flags. The gas cost for both instructions is the same as JUMPI.
The rationale behind this proposal is to improve the safety and efficiency of smart contracts by bringing math checks to the EVM level. The document mentions that this proposal introduces backward-incompatible changes to the EVM behavior and must be accompanied by a hard fork. The test cases, reference implementation, and security considerations are yet to be determined.

###### Video

###### Original

## 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.

## Motivation

The importance of math checks in smart contract projects is very clear. It was an OpenZeppelin library and then incorporated in Solidity's default behavior. Bringing this to EVM level can combine both gas efficiency and safety.

## Specification

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119 and RFC 8174.

Starting from `BLOCK_TIMESTAMP >= HARDFORK_TIMESTAMP`

### Constants

Constant | Type | Value |
---|---|---|

`INT_MIN` | `int` | -(2**255) |

`UINT_MAX` | `uint` | 2 ** 256 |

### Flags

Variable | Type | Initial Value |
---|---|---|

`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.

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 `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
`SHL`

(`0x1b`

) and`res >> a != b`

The `overflow`

flag is MUST 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
`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.

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` |

### gas

The gas cost for both instructions is `G_high`

, the same as `JUMPI`

.

## Rationale

EVM uses two's complement for negative numbers. The opcodes listed above triggers one or two flags depending if they are used for signed and unsigned numbers.

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

This EIP introduces a new opcode and changes int EVM behavior.

## Test Cases

TBD

## Reference Implementation

TBD

## Security Considerations

This is a new EVM behavior but each code will decide how to interact with it.

## Copyright

Copyright and related rights waived via CC0.

###### Adopted by projects

### Not miss a beat of EIPs' update?

Subscribe EIPs Fun to receive the latest updates of EIPs Good for Buidlers to follow up.

View all