主页EIPs
EIPsEIP-6888
EIP-6888

Math checking in EVM

Check for math underflows overflows and division by zero at EVM level
StagnantStandards Track: Core
创建时间: 2023-04-16
Renan Rodrigues de Souza (@RenanSouza2)
社区讨论原文链接编辑
1 分钟了解

相关视频
欢迎补充好内容
去提交
正文

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_TIMESAMP >= HARDFORK_TIMESTAMP

Constants

ConstantTypeValue
INT_MINint-(2**255)
UINT_MAXuint2 ** 256

Flags

VariableTypeInitial Value
carryboolfalse
overflowboolfalse

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.

ValueMnemonicδαDescription
JUMPC0x5B10Conditionally alter the program counter.
J_JUMPC = carry ? µ_s[0] : µ_pc + 1
carry = overflow = false
JUMPO0x5C10Conditionally 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 and related rights waived via CC0.

扩展阅读
欢迎补充好内容
去提交
相关项目
欢迎补充好内容
去提交

不想错过最新的 EIP 动态?

订阅 EIPs Fun 周刊以跟进相关更新,建⽴你与 EIP 之间的连接 ,更好地建设以太坊。

详情
聚集 EIP 贡献者, 扩展以太坊
资源
GitHub
支持社区