SMTChecker与形式验证
使用形式验证，可以执行自动的数学证明，证明您的源代码满足特定的形式规范。规范仍然是正式的(就像源代码一样)，但通常要简单得多。
请注意，正式验证本身只能帮助您理解您做了什么(规范)和如何做(实际实现)之间的区别。您仍然需要检查规范是否符合您的要求，并且没有遗漏任何意想不到的影响。
SOLIDITY实现了一种形式化的验证方法，该方法基于 SMT (Satisfiability Modulo Theories) 和 Horn 解决问题。SMTChecker模块自动尝试证明代码满足给定的规范 require 和 assert 结算单。就是它认为 require 作为假设的陈述，并试图证明其中的条件 assert 陈述总是正确的。如果发现断言失败，则可以向用户提供反例，说明如何违反断言。如果SMTChecker没有对属性发出警告，则表示该属性是安全的。
SMTChecker在编译时检查的其他验证目标包括：
算术下溢和上溢。
除以零。
琐碎的条件和无法访问的代码。
弹出空数组。
索引访问越界。
转账资金不足。
默认情况下，如果启用所有引擎，则会自动检查上述所有目标，但稠度>=0.8.7的下溢和溢流除外。
SMTChecker报告的潜在警告包括：
<failing property> happens here.。这意味着SMTChecker证明某个属性失败。可以举出反例，但在复杂情况下也可能不显示反例。在某些情况下，当SMT编码添加难以表达或不可能表达的坚固性代码的抽象时，该结果也可能是假阳性。<failing property> might happen here。这意味着求解器无法在给定的超时时间内证明这两种情况中的任何一种。由于结果未知，SMTChecker将报告潜在的可靠性故障。这可以通过增加查询超时来解决，但是这个问题对于引擎来说也可能太难解决了。
要启用SMTChecker，您必须选择 which engine should run ，其中默认设置为无引擎。选择引擎将在所有文件上启用SMTChecker。
注解
在Solidity 0.8.4之前，启用SMTChecker的默认方式是通过 pragma experimental SMTChecker; 并且只会分析包含杂注的合同。该编译指示已被弃用，尽管它仍然启用SMTChecker以实现向后兼容性，但它将在Solidity 0.9.0中被删除。另请注意，现在即使在单个文件中使用杂注也会启用所有文件的SMTChecker。
注解
假设SMTChecker和底层求解器中没有错误，则没有针对验证目标的警告代表了无可争议的数学正确性证明。请记住，这些问题是 非常辛苦 而且有时候 不可能 在一般情况下自动解决。因此，一些属性可能无法解决或可能导致大型合同的误报。每一处已探明的财产都应该被视为一项重要的成就。对于高级用户，请参见 SMTChecker Tuning 学习一些可能有助于证明更复杂性质的选项。
教程
溢出
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Overflow {
uint immutable x;
uint immutable y;
function add(uint _x, uint _y) internal pure returns (uint) {
return _x + _y;
}
constructor(uint _x, uint _y) {
(x, y) = (_x, _y);
}
function stateAdd() public view returns (uint) {
return add(x, y);
}
}
上面的合同显示了一个溢出检查示例。缺省情况下，SMTChecker不会检查稠度>=0.8.7的下溢和上溢，因此我们需要使用命令行选项 --model-checker-targets "underflow,overflow" 或JSON选项 settings.modelChecker.targets = ["underflow", "overflow"] 。看见 this section for targets configuration 。在这里，它报告以下内容：
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
= 0
Transaction trace:
Overflow.constructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
State: x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
Overflow.stateAdd()
Overflow.add(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call
--> o.sol:9:20:
|
9 | return _x + _y;
| ^^^^^^^
如果我们加上 require 对于过滤溢出的语句，SMT检查器证明没有溢出可达(通过不报告警告)：
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Overflow {
uint immutable x;
uint immutable y;
function add(uint _x, uint _y) internal pure returns (uint) {
return _x + _y;
}
constructor(uint _x, uint _y) {
(x, y) = (_x, _y);
}
function stateAdd() public view returns (uint) {
require(x < type(uint128).max);
require(y < type(uint128).max);
return add(x, y);
}
}
断言
断言表示代码中的一个不变量：一个必须为真的属性 对于所有事务，包括所有输入值和存储值 ，否则就会出现错误。
下面的代码定义了一个函数 f 这保证了不会溢出。功能 inv 定义符合以下条件的规范 f 是单调递增的：对于每一个可能的配对 (_a, _b) ，如果 _b > _a 然后 f(_b) > f(_a) 。因为 f 确实是单调增加的，SMTChecker证明我们的属性是正确的。我们鼓励您尝试属性和函数定义，看看会有什么结果！
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Monotonic {
function f(uint _x) internal pure returns (uint) {
require(_x < type(uint128).max);
return _x * 42;
}
function inv(uint _a, uint _b) public pure {
require(_b > _a);
assert(f(_b) > f(_a));
}
}
我们还可以在循环中添加断言来验证更复杂的属性。下面的代码搜索不受限制的数字数组的最大元素，并断言找到的元素必须大于或等于数组中的每个元素的属性。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
uint m = 0;
for (uint i = 0; i < _a.length; ++i)
if (_a[i] > m)
m = _a[i];
for (uint i = 0; i < _a.length; ++i)
assert(m >= _a[i]);
return m;
}
}
请注意，在此示例中，SMTChecker将自动尝试证明三个属性：
++i在第一个循环中不会溢出。++i在第二个循环中不会溢出。断言总是正确的。
注解
属性涉及循环，这使得 多得多 比前面的示例更难，所以要小心循环！
所有的属性都被正确地证明是安全的。您可以随意更改属性和/或添加对数组的限制，以查看不同的结果。例如，将代码更改为
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
require(_a.length >= 5);
uint m = 0;
for (uint i = 0; i < _a.length; ++i)
if (_a[i] > m)
m = _a[i];
for (uint i = 0; i < _a.length; ++i)
assert(m > _a[i]);
return m;
}
}
为我们提供了：
Warning: CHC: Assertion violation happens here.
Counterexample:
_a = [0, 0, 0, 0, 0]
= 0
Transaction trace:
Test.constructor()
Test.max([0, 0, 0, 0, 0])
--> max.sol:14:4:
|
14 | assert(m > _a[i]);
状态属性
到目前为止，这些示例仅演示了SMTChecker在纯代码上的使用，证明了特定操作或算法的属性。智能合约中的一种常见属性类型是涉及合约状态的属性。可能需要多个事务才能使此类属性的断言失败。
例如，假设一个2D网格，其中两个轴的坐标都在(-2^128，2^128-1)范围内。让我们把机器人放在(0，0)位置。机器人只能沿对角线移动，一次走一步，不能移出栅格。机器人的状态机可以由下面的智能合同表示。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Robot {
int x = 0;
int y = 0;
modifier wall {
require(x > type(int128).min && x < type(int128).max);
require(y > type(int128).min && y < type(int128).max);
_;
}
function moveLeftUp() wall public {
--x;
++y;
}
function moveLeftDown() wall public {
--x;
--y;
}
function moveRightUp() wall public {
++x;
++y;
}
function moveRightDown() wall public {
++x;
--y;
}
function inv() public view {
assert((x + y) % 2 == 0);
}
}
功能 inv 表示状态机的不变量，该状态机 x + y 必须是平坦的。SMTChecker设法证明，无论我们给机器人发出多少命令，即使是无限多的命令，不变量也可以 绝不可能 失败了。感兴趣的读者可能也想手动证明这一事实。提示：这个不变量是归纳的。
我们还可以欺骗SMTChecker为我们提供一条通往我们认为可能可以到达的特定位置的路径。我们可以将(2，4)是 not 可以通过添加以下函数来访问。
function reach_2_4() public view {
assert(!(x == 2 && y == 4));
}
此属性为FALSE，在证明该属性为FALSE的同时，SMTChecker准确地告诉我们 how 达到(2，4)：
Warning: CHC: Assertion violation happens here.
Counterexample:
x = 2, y = 4
Transaction trace:
Robot.constructor()
State: x = 0, y = 0
Robot.moveLeftUp()
State: x = (- 1), y = 1
Robot.moveRightUp()
State: x = 0, y = 2
Robot.moveRightUp()
State: x = 1, y = 3
Robot.moveRightUp()
State: x = 2, y = 4
Robot.reach_2_4()
--> r.sol:35:4:
|
35 | assert(!(x == 2 && y == 4));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
请注意，上面的路径不一定是确定性的，因为还有其他路径可以到达(2，4)。显示哪条路径的选择可能会根据使用的求解器、其版本或随机更改。
外部呼叫和重入性
SMTChecker将每个外部调用视为对未知代码的调用。背后的原因是，即使调用的约定的代码在编译时可用，也不能保证部署的约定确实与接口在编译时来自的约定相同。
在某些情况下，即使外部调用的代码可以执行任何操作(包括重新输入调用方协定)，也可以自动推断仍然为真的状态变量的属性。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
interface Unknown {
function run() external;
}
contract Mutex {
uint x;
bool lock;
Unknown immutable unknown;
constructor(Unknown _u) {
require(address(_u) != address(0));
unknown = _u;
}
modifier mutex {
require(!lock);
lock = true;
_;
lock = false;
}
function set(uint _x) mutex public {
x = _x;
}
function run() mutex public {
uint xPre = x;
unknown.run();
assert(xPre == x);
}
}
上面的示例显示了一个使用互斥标志来禁止重入的协定。求解器能够推断出 unknown.run() 调用时，合同已经“锁定”，因此不可能更改 x ，而不管未知的调用代码做什么。
如果我们“忘记”使用 mutex 函数上的修饰符 set ，SMTChecker能够合成外部调用代码的行为，从而使断言失败：
Warning: CHC: Assertion violation happens here.
Counterexample:
x = 1, lock = true, unknown = 1
Transaction trace:
Mutex.constructor(1)
State: x = 0, lock = false, unknown = 1
Mutex.run()
unknown.run() -- untrusted external call, synthesized as:
Mutex.set(1) -- reentrant call
--> m.sol:32:3:
|
32 | assert(xPre == x);
| ^^^^^^^^^^^^^^^^^
SMTChecker选项和调整
超时
SMTChecker使用硬编码的资源限制 (rlimit )每个解算器选择，这与时间不完全相关。我们选择了 rlimit 选项作为默认值，因为它提供的确定性保证比求解器内的时间更多。
此选项大致相当于每个查询“几秒超时”。当然，许多属性非常复杂，需要大量时间来解决，其中决定论并不重要。如果SMTChecker无法使用默认值求解合同属性 rlimit ，可以通过CLI选项提供以毫秒为单位的超时 --model-checker-timeout <time> 或JSON选项 settings.modelChecker.timeout=<time> ，其中0表示无超时。
核查目标
SMTChecker创建的验证目标类型也可以通过CLI选项进行自定义 --model-checker-target <targets> 或JSON选项 settings.modelChecker.targets=<targets> 。在CLI情况下， <targets> 是一个或多个验证目标的无空格逗号分隔列表，以及JSON输入中作为字符串的一个或多个目标数组。代表目标的关键字包括：
断言：
assert。算术下溢：
underflow。算术溢出：
overflow。除以零：
divByZero。琐碎的条件和无法访问的代码：
constantCondition。弹出空数组：
popEmptyArray。超出界限的数组/固定字节索引访问：
outOfBounds。转账资金不足：
balance。以上所有内容：
default(仅限CLI)。
常见的目标子集可能是，例如： --model-checker-targets assert,overflow 。
默认情况下，所有目标都处于选中状态，但稠度>=0.8.7的下溢和上溢除外。
对于如何以及何时拆分验证目标，没有精确的启发式方法，但它在处理大型合同时可能特别有用。
未经证实的目标
如果有任何未经证实的目标，SMTChecker会发出一个警告，说明有多少未经证实的目标。如果用户希望查看所有特定的未经验证的目标，则CLI选项 --model-checker-show-unproved 和JSON选项 settings.modelChecker.showUnproved = true 可以使用。
已验证的合同
默认情况下，给定源中的所有可部署契约作为将要部署的契约被单独分析。这意味着，如果一份合同有许多直接和间接继承父代，那么所有这些父代都会被自己分析，即使区块链上只会直接访问派生最多的父代。这会给SMTChecker和求解器带来不必要的负担。为了帮助这种情况，用户可以指定应该将哪些合同分析为已部署的合同。当然，仍然分析父约定，但仅在派生最多的约定的上下文中分析，从而降低了编码和生成的查询的复杂性。请注意，默认情况下，SMTChecker不会将抽象契约作为派生最多的契约进行分析。
所选合同可以通过CLI中的<source>：<Contract>对的逗号分隔列表(不允许使用空格)提供： --model-checker-contracts "<source1.sol:contract1>,<source2.sol:contract2>,<source2.sol:contract3>" ，并通过该对象 settings.modelChecker.contracts 在 JSON input ，它具有以下形式：
"contracts": {
"source1.sol": ["contract1"],
"source2.sol": ["contract2", "contract3"]
}
带松弛变量的除法和模运算
间隔程序是SMTChecker使用的默认Horn解算器，它通常不喜欢Horn规则中的除法和模运算。因此，默认情况下，使用约束对实度除法和模运算进行编码 a = b * d + m 哪里 d = a / b 和 m = a % b 。但是，其他解算器(如Eldarica)更喜欢语法精确的运算。命令行标志 --model-checker-div-mod-no-slacks 和JSON选项 settings.modelChecker.divModNoSlacks 可用于根据使用的解算器首选项切换编码。
NatSpec函数抽象
某些函数，包括常用的数学方法，如 pow 和 sqrt 可能过于复杂，无法以全自动方式进行分析。这些函数可以用NatSpec标记进行注释，这些标记向SMTChecker指示这些函数应该被抽象。这意味着不使用函数体，并且在调用时，函数将：
返回一个不确定的值，如果抽象的函数是视图/纯函数，则保持状态变量不变，否则也将状态变量设置为不确定的值。这可以通过注释使用
/// @custom:smtchecker abstract-function-nondet。充当未解释的函数。这意味着函数的语义(由主体给出)被忽略，并且该函数具有的唯一属性是给定相同的输入，它保证相同的输出。目前正在开发中，将通过注释提供
/// @custom:smtchecker abstract-function-uf。
模型检查引擎
SMTChecker模块实现了两个不同的推理引擎，一个是有界模型检查器(BMC)，另一个是约束Horn子句系统(CHC)。这两款发动机目前都在开发中，各自有不同的特点。引擎是独立的，每个属性警告都会声明它来自哪个引擎。请注意，上面的所有示例和反例都是由更强大的引擎CHC报告的。
默认情况下，两个引擎都使用，其中CHC首先运行，每个未经验证的属性都会传递给BMC。您可以通过CLI选项选择特定引擎 --model-checker-engine {{all,bmc,chc,none}} 或JSON选项 settings.modelChecker.engine={{all,bmc,chc,none}} 。
有界模型检查器(BMC)
BMC引擎孤立地分析函数，即，在分析每个函数时，它不会考虑多个事务上的合同的整体行为。此时此刻，此引擎中的循环也被忽略。只要内部函数调用不是直接或间接递归的，它们就是内联的。如果可能，外部函数调用是内联的。可能受可重入性影响的知识将被擦除。
上述特征使得BMC容易报告误报，但它也是轻量级的，应该能够快速找到小的本地错误。
受约束的Horn子句(CHC)
合同的控制流图(CFG)被建模为一个Horn条款系统，其中合同的生命周期由一个循环表示，该循环可以不确定地访问每个公共/外部函数。这样，在分析任何函数时，都会考虑整个合约在无限数量的事务上的行为。此引擎完全支持循环。支持内部函数调用，而外部函数调用假定调用的代码未知，可以执行任何操作。
就其所能证明的内容而言，CHC引擎比BMC强大得多，并且可能需要更多的计算资源。
SMT和角点求解器
上面详述的两个引擎使用自动定理证明器作为它们的逻辑后端。BMC使用SMT解算器，而CHC使用Horn解算器。通常，同一工具可以同时充当两者，如中所示 z3 ，它主要是SMT求解器，并使 Spacer 可用作角点解算器，并且 Eldarica 两者兼而有之。
用户可以通过CLI选项选择应使用的求解程序(如果可用 --model-checker-solvers {{all,cvc4,smtlib2,z3}} 或JSON选项 settings.modelChecker.solvers=[smtlib2,z3] ，其中：
cvc4仅在以下情况下才可用solc二进制文件是用它编译的。只有BMC使用cvc4。smtlib2将SMT/Horn查询输出到 smtlib2 格式化。它们可以与编译器的 callback mechanism 从而可以使用来自系统的任何求解器二进制文件来同步地将查询结果返回给编译器。例如，这是目前使用Eldarica的唯一方式，因为它没有C++API。这可以由BMC和CHC使用，具体取决于调用的解算器。z3有空房吗？如果
solc是用它编译的；如果一个动态的
z3在Linux系统中安装4.8.x版的库(从Solidity 0.7.6开始)；静态输入
soljson.js(从实度0.6.9开始)，即编译器的Javascript二进制文件。
由于BMC和CHC都使用 z3 ，以及 z3 在包括浏览器在内的更多环境中都可用，因此大多数用户几乎不需要关心此选项。更高级的用户可能会应用此选项，以尝试在更复杂的问题上使用替代解算器。
请注意，所选引擎和求解器的某些组合将导致SMTChecker不执行任何操作，例如选择CHC和 cvc4 。
抽象和假阳性
SMTChecker以一种不完整且合理的方式实现抽象：如果报告了一个bug，它可能是由抽象引入的假阳性(由于擦除知识或使用非精确类型)。如果它确定验证目标是安全的，那么它确实是安全的，也就是说，没有假阴性(除非SMTChecker中有bug)。
如果无法验证目标，您可以尝试使用上一节中的调优选项来帮助解算器。如果您确定有误报，请添加 require 代码中包含更多信息的语句也可以为求解器提供更多功能。
SMT编码和类型
SMTChecker编码尝试尽可能精确，将固体类型和表达式映射到最接近的类型和表达式 SMT-LIB 表示，如下表所示。
实心型 |
SMT排序 |
理论 |
|---|---|---|
布尔值 |
布尔尔 |
布尔尔 |
intn，uintN，地址，bytesN，枚举，协定 |
整数 |
利亚，NIA |
数组、映射、字节、字符串 |
元组(数组元素，整数长度) |
数据类型、数组、LIA |
结构 |
元组 |
数据类型 |
其他类型 |
整数 |
LIA |
尚不支持的类型由单个256位无符号整数抽象，其中忽略其不受支持的操作。
有关SMT编码内部工作方式的更多详细信息，请参阅白皮书 SMT-based Verification of Solidity Smart Contracts 。
函数调用
在BMC引擎中，对相同协定(或基础协定)的函数调用在可能的情况下(即当它们的实现可用时)是内联的。即使其他契约中的函数的代码可用，对它们的调用也不会内联，因为我们不能保证实际部署的代码是相同的。
CHC引擎创建使用被调用函数的摘要来支持内部函数调用的非线性Horn子句。外部函数调用被视为对未知代码的调用，包括潜在的可重入调用。
复杂的纯函数由参数上的未解释函数(UF)抽象。
功能 |
BMC/CHC行为 |
|---|---|
|
验证目标。 |
|
假设。 |
内部呼叫 |
BMC：内联函数调用。CHC：函数摘要。 |
已知代码的外部调用 |
BMC：内联函数调用或擦除有关状态变量和本地存储引用的知识。CHC：假设被调用的代码未知。尝试推断在调用返回后保持的不变量。 |
存储阵列推送/弹出 |
精确支撑。检查它是否弹出空数组。 |
ABI函数 |
用UF提取。 |
|
精确支撑。 |
|
用UF提取。 |
没有实现的纯函数(外部或复杂) |
用UF抽象 |
未实现的外部函数 |
BMC：擦除状态知识，并假设结果不确定。CHC：非确定性总结。尝试推断在调用返回后保持的不变量。 |
转接 |
bmc：检查合同余额是否充足。CHC：尚未执行检查。 |
其他 |
当前不受支持 |
使用抽象意味着失去精确的知识，但在许多情况下，这并不意味着失去证明力。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Recover
{
function f(
bytes32 hash,
uint8 _v1, uint8 _v2,
bytes32 _r1, bytes32 _r2,
bytes32 _s1, bytes32 _s2
) public pure returns (address) {
address a1 = ecrecover(hash, _v1, _r1, _s1);
require(_v1 == _v2);
require(_r1 == _r2);
require(_s1 == _s2);
address a2 = ecrecover(hash, _v2, _r2, _s2);
assert(a1 == a2);
return a1;
}
}
在上面的示例中，SMTChecker的表现力不足以实际计算 ecrecover ，但是通过将函数调用建模为未解释的函数，我们知道在调用等效参数时返回值是相同的。这足以证明上述断言总是正确的。
使用UF抽象函数调用可以针对已知为确定性的函数进行，并且可以很容易地针对纯函数进行。但是，使用常规外部函数很难做到这一点，因为它们可能依赖于状态变量。
引用类型和别名
Solidity为引用类型实现别名，引用类型具有相同的 data location 。这意味着可以通过引用相同的数据区来修改一个变量。SMTChecker不跟踪哪些引用引用了相同的数据。这意味着无论何时分配引用类型的局部引用或状态变量，关于相同类型和数据位置的变量的所有知识都会被擦除。如果类型是嵌套的，则知识移除还包括所有前缀基类型。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Aliasing
{
uint[] array1;
uint[][] array2;
function f(
uint[] memory a,
uint[] memory b,
uint[][] memory c,
uint[] storage d
) internal {
array1[0] = 42;
a[0] = 2;
c[0][0] = 2;
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
assert(array1[0] == 42);
// However, an assignment to a storage reference will erase
// storage knowledge accordingly.
d[0] = 2;
// Fails as false positive because of the assignment above.
assert(array1[0] == 42);
// Fails because `a == b` is possible.
assert(a[0] == 2);
// Fails because `c[i] == b` is possible.
assert(c[0][0] == 2);
assert(d[0] == 2);
assert(b[0] == 1);
}
function g(
uint[] memory a,
uint[] memory b,
uint[][] memory c,
uint x
) public {
f(a, b, c, array2[x]);
}
}
在分配给 b[0] ，我们需要清楚地了解 a 因为它具有相同的类型 (uint[] )和数据位置(存储器)。我们还需要清楚地了解 c ，因为它的基类型也是 uint[] 位于内存中。这意味着有些人 c[i] 可以引用与 b 或 a 。
请注意，我们不清楚关于以下内容的知识 array 和 d 因为它们位于仓库中，即使它们也有类型 uint[] 。但是，如果 d 被指派，我们需要清楚地了解 array 反之亦然。
合同余额
在以下情况下，可以部署合同并向其发送资金 msg.value >0在部署事务中。但是，合同的地址在部署之前可能已经有资金，这些资金由合同保留。因此，SMTChecker假定 address(this).balance >= msg.value 以符合EVM规则。在以下情况下，合同余额也可以增加，而不会触发对合同的任何调用
selfdestruct以解析出的合同为剩余资金的标的的另一合同执行，合同是Coinbase(即，
block.coinbase)一些挡路。
为了对此进行适当的建模，SMTChecker假设在每次新的交易中，合约的余额至少可以增长 msg.value 。
现实世界的假设
有些情况可以用稳固性和EVM来表示，但预计在实践中永远不会发生。其中一种情况是推送期间动态存储阵列溢出的长度：如果 push 运算应用于长度为2^256-1的数组，其长度静默溢出。但是，这在实践中不太可能发生，因为将阵列扩展到该点所需的操作将需要数十亿年才能执行。SMTChecker采用的另一个类似假设是地址余额永远不会溢出。
类似的想法在 EIP-1985 。