🚧 Stagnant Standards Track: Core

EIP-6888: EVM 级别的算术验证

在 EVM 级别检查数学溢出和除零错误

Authors	Renan Rodrigues de Souza (@RenanSouza2)
Created	2023-04-16
Discussion Link	https://ethereum-magicians.org/t/eip-math-checking/13846

摘要
动机
规范
- 常量
- 标志
- 定义
- 条件
- 操作码
- gas
理由
向后兼容性
测试用例
参考实现
安全注意事项
版权

摘要

此 EIP 将算术检查添加到 EVM 算术运算，并添加一个新的操作码，以便在发生事件时有条件地跳转。检查列表包括溢出、除零错误。

动机

数学检查在智能合约项目中的重要性非常明显。它曾经是 OpenZeppelin 的一个库，后来被纳入 Solidity 的默认行为中。将其引入 EVM 级别可以兼顾 gas 效率和安全性。

规范

本文档中使用的关键词“必须 (MUST)”，“禁止 (MUST NOT)”，“需要 (REQUIRED)”，“应该 (SHALL)”，“不应该 (SHALL NOT)”，“推荐 (RECOMMENDED)”，“不推荐 (NOT RECOMMENDED)”，“可以 (MAY)”和“可选 (OPTIONAL)”应按照 RFC 2119 和 RFC 8174 中的描述进行解释。

从 BLOCK_TIMESTAMP >= HARDFORK_TIMESTAMP 开始

常量

Constant	Type	Value
`HARDFORK_TIMESTAMP`	`uint64`	`TBD`
`UINT_MAX`	`uint256`	`2 ** 256 - 1`
`INT_MIN`	`int256`	`-(2**255)`

标志

Variable	Type	Initial Value
`carry`	`bool`	false
`overflow`	`bool`	false

在 EVM 状态中添加两个新标志：无符号警告 (carry) 和有符号警告 (overflow)。这些标志的作用域与程序计数器相同。

定义

从现在开始，a，b和c引用数学运算中的参数，res引用输出。仅当运算采用 3 个输入时才使用c。

函数 sign(x) 定义在 uint256 -> {NEGATIVE, ZERO, POSITIVE} 集合中

条件

在以下情况下，carry 标志必须 (MUST) 设置：

当操作码为 ADD (0x01) 且 res < a 时
当操作码为 MUL (0x02) 且 a != 0 ∧ res / a != b 时
当操作码为 SUB (0x03) 且 b > a 时
当操作码为 DIV (0x04) 或 MOD (0x06) 且 b == 0 时
当操作码为 ADDMOD (0x08) 且 c == 0 时
当操作码为 MULMOD (0x08) 且 c == 0 时
当操作码为 EXP (0x0A) 且 a ** b > UINT_MAX 时
当操作码为 SHL (0x1b) 且 res >> a != b 时

在以下情况下，overflow 标志必须 (MUST) 设置：

当操作码为 ADD (0x01) 且 a != 0 ∧ b != 0 ∧ sign(a) == sign(b) ∧ sign(a) != sign(res) 时
当操作码为 SUB (0x03) 且 (a != 0 ∧ b != 0 ∧ sign(a) != sign(b) ∧ sign(a) != sign(res)) ∨ (a == 0 ^ b == INT_MIN) 时
当操作码为 MUL (0x02) 且 (a == -1 ∧ b == INT_MIN) ∨ (a == INT_MIN ∧ b == -1) ∨ (a != 0 ∧ (res / a != b)) (此处的 / 表示 SDIV) 时
当操作码为 SDIV (0x05) 或 SMOD (0x06) 且 b == 0 ∨ (a == INT_MIN ∧ b == -1) 时
当操作码为 SHL (0x1b) 且 res >> a != b (此处的 >> 表示 SAR) 时

操作码

`JUMPC`

从堆栈中使用一个参数，即可能的 pc 目标地址。根据 carry 标志有条件地更改程序计数器。 J_JUMPC = carry ? µ_s[0] : µ_pc + 1 清除两个标志。 carry = overflow = false

`JUMPO`

从堆栈中使用一个参数，即可能的 pc 目标地址。根据 ovewflow 标志有条件地更改程序计数器。 J_JUMPO = carry ? µ_s[0] : µ_pc + 1 清除两个标志。 carry = overflow = false

gas

这两个指令的 gas 成本均为 G_high，与 JUMPI 相同。

理由

EVM 对负数使用二进制补码。上面列出的操作码会触发一个或两个标志，具体取决于它们是否用于有符号和无符号数字。

为每个操作码描述的条件都考虑到了易于实施。唯一的例外是 EXP，因为它很难给出一个简洁的测试，因为大多数其他测试都依赖于逆运算，并且没有原生的 LOG。大多数 EXP 的内部实现都会使用 MUL，因此标志 carry 可以从该指令中得出，而不是从 overflow 得出。

两个标志同时清除，因为预期指令会在代码之间转换时使用，在这些代码中，数字被视为有符号或无符号。

向后兼容性

此 EIP 引入了一个新的操作码并改变了 EVM 行为。

测试用例

待定

参考实现

待定

安全注意事项

这是一种新的 EVM 行为，但是每个代码都将决定如何与之交互。

版权

通过 CC0 放弃版权及相关权利。

Citation

Please cite this document as:

Renan Rodrigues de Souza (@RenanSouza2), "EIP-6888: EVM 级别的算术验证 [DRAFT]," Ethereum Improvement Proposals, no. 6888, April 2023. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-6888.