---
eip: 6888
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
type: Standards Track
category: Core
created: 2023-04-16
---

## Abstract

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

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     |
| -------------------- | --------- | --------- |
| `HARDFORK_TIMESTAMP` | `uint64`  | `TBD`     |
| `UINT_MAX`           | `uint256` | `2 ** 256 - 1` |
| `INT_MIN`            | `int256`  | `-(2**255)` |

### Flags

|     Variable        | Type      | Initial Value |
| ------------------- | --------- |:------------- |
| `carry`             | `bool`    | false         |
| `overflow`          | `bool`    | false         |

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

### Conditions

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`
 - 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 MUST be set in the following circumstances:

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

### Opcodes

#### `JUMPC`

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 `overflow` flag. `J_JUMPO = carry ? µ_s[0] : µ_pc + 1` 
Clears both flags. `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`.

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](../LICENSE.md).