Solidity 优化规则的形式化验证：test/formal 目录的 SMT 证明框架实战指南

Solidity 优化规则的形式化验证：test/formal 目录的 SMT 证明框架实战指南

【免费下载链接】soliditySolidity, the Smart Contract Programming Language项目地址: https://gitcode.com/GitHub_Trending/so/solidity

导读

Solidity 编译器内置了一套基于模式匹配的 EVM 汇编优化规则（simplification rules），用于在代码生成阶段对指令序列做常量折叠、代数化简等变换。本文围绕仓库 test/formal 目录展开，讲解该目录如何用 Z3 SMT 求解器对这些优化规则进行形式化证明：通过把"优化前"与"优化后"的表达式翻译成位向量（BitVector）逻辑并断言两者必然相等，一旦求解器找到反例即证明规则有误。读完本文，你将掌握该证明框架的核心组件（Rule、util、opcodes三个模块）、经典证明用例的写法，以及 run_proofs.sh 如何把证明流程接入 CI，从而具备为编译器优化规则编写与运行形式化验证脚本的能力。

为什么需要形式化验证优化规则

Solidity 编译器在 libevmasm/RuleList.h 中以模板化的方式维护了一张庞大的化简规则表，例如对常量操作数直接求值：

• ADD(A, B) -> A + B（常数相加）
• DIV(A, B) -> B == 0 ? 0 : A / B（除零语义）
• BYTE(A, B)的按字节提取逻辑
• SIGNEXTEND(A, B)的符号扩展实现

这些规则被用于 libevmasm 的简化规则（SimplificationRules）以及 libyul 优化器，直接影响最终生成的字节码质量。但一条"看起来正确"的代数变换在 256 位 EVM 字长、溢出回绕、有符号/无符号语义、除零特殊行为等边界条件下很容易出错。例如MOD(ADD(X, Y), A) -> ADDMOD(X, Y, A)只有在A > 0且A是 2 的幂时才成立（见 mod_add_to_addmod.py），若缺少前置条件就会得到错误结果。

因此，test/formal/README.md 明确指出：该目录是对这些优化规则正确性的形式化证明努力，分为两条路线：

• 在 HOL（高阶逻辑）层面使用 EthIsabelle 进行定理证明；
• 在一阶逻辑（FOL）层面，使用 SMT 求解器对Integers 和 BitVectors（SMT-LIB 整数与位向量理论）进行可满足性检查。

仓库中实际落地的是第二条路线：约 40 个 Python 证明脚本，统一依赖 Z3 求解器（from z3 import ...），把每条优化规则编码成一个"优化前后必然等价"的约束，交给 Z3 判定不可满足（unsat），从而证明等价性。

证明框架的三个核心模块

整个目录是一个极简但完整的证明框架，由三个可复用模块加若干按规则拆分的证明脚本组成。理解它们就理解了所有用例。

rule.py：证明主控与反例报告

rule.py 定义了Rule类，封装了"前置条件 + 等价断言 + 求解"的完整流程：

• require(_r)：向求解器加入前置条件（requirements），例如A > 0、A & (A - 1) == 0；
• __lshift__(_c)：向约束列表追加"优化前 ≠ 优化后"的否定断言；
• check(_nonopt, _opt)：核心验证方法，分两步求解：
  1. 先检查前置条件本身是否可满足（unsat说明条件自相矛盾，脚本设计有误；unknown说明求解器无法判定）；
  2. 在满足前置条件的模型上，再断言_nonopt != _opt，若结果为sat则打印 Z3 给出的反例模型并退出（Rule is incorrect. Model: ...）；若为unsat则说明在全部满足前置条件的输入下，优化前后结果必然一致，证明成立。
• setTimeout(60000)：默认给求解器设置 60 秒超时，防止复杂位向量约束导致求解时间失控。

一个值得注意的工程细节：check通过solver.push()/solver.pop()隔离两次检查，避免前置条件污染第二次等价性判定。

util.py：EVM 语义的位向量建模辅助

util.py 提供在证明脚本中复用的位向量构造函数，用于把 Solidity 类型宽度与 EVM 行为翻译成 Z3 表达式：

• BVUnsignedUpCast(x, n_bits)/BVSignedUpCast(x, n_bits)：将type_bits宽的短位向量无符号/符号扩展为n_bits（默认 256）位，模拟类型提升；
• BVUnsignedMax/BVSignedMax/BVSignedMin：生成各类型宽度的上下界常量；
• BVSignedCleanupFunction(x, type_bits)/BVUnsignedCleanupFunction(x, type_bits)：精确复刻编译器的"整数清理函数"（cleanup function）语义——按type_bits对值做符号位感知的位掩码或扩展，保证高位垃圾位被清除。

这些函数在证明signed_integer_cleanup_function.py、unsigned_integer_cleanup_function.py这类"清理函数与类型转换等价"的规则时是核心依赖。

opcodes.py：EVM 指令的语义化翻译

opcodes.py 把 RuleList 中用到的 EVM 指令逐条翻译成 Z3 位向量操作，注意它严格保留了 EVM 的特殊语义：

• DIV(x, y)：If(y == 0, 0, UDiv(x, y))——除零返回 0，而非数学上的未定义；
• MOD/ADDMOD/MULMOD：除零/模零同样返回 0，且ADDMOD用ZeroExt先扩位再取模，规避加法溢出；
• SMOD：完整复刻有符号取模的四象限符号规则（见 SMOD 定义）；
• BYTE(i, x)：索引越界返回 0，否则按字节移位提取；
• SIGNEXTEND(i, x)：按i*8+7位做符号扩展，越界时原样返回；
• SHL/SHR/SAR：分别对应算术左移、逻辑右移、算术右移。

正是因为这层翻译与 EVM 实际执行语义逐位对应，MOD(ADD(X, Y), A) == ADDMOD(X, Y, A)这类规则才可能在除零、溢出等边界上被严格检验。

典型证明用例剖析

用例一：带检查的无符号加法（checked_uint_add.py）

checked_uint_add.py 证明编译器overflowCheckedIntAddFunction生成的溢出检查逻辑与 Z3 内置的BVAddNoOverflow完全一致：

• 对type_bits从 8 到 256 逐档遍历（每次 +8）；
• 对 256 位情形使用 EVM 式检测GT(X, sum_)（和小于任一加数即溢出）；
• 对更窄类型使用GT(sum_, maxValue)（结果超过类型上限即溢出）；
• 最后断言这两种检测方式与 Z3 的溢出谓词等价。

对应地，checked_int_add.py 证明有符号加法，同时覆盖上溢与下溢两个方向，并用SLT/SGT复刻编译器对符号溢出的判断。其余checked_int_sub、checked_int_mul_12、checked_uint_mul_12、checked_int_div等脚本覆盖减、乘、除等带检查算术的同类证明。

用例二：MOD/ADD 到 ADDMOD 的改写（mod_add_to_addmod.py）

mod_add_to_addmod.py 是"带前置条件的化简规则"的典型样本：

rule.require(A > 0) rule.require(((A & (A - 1)) == 0)) rule.check(nonopt, opt) # nonopt = MOD(ADD(X, Y), A)，opt = ADDMOD(X, Y, A)

它证明：当且仅当模数A为正且为 2 的幂时，先加后取模可以安全改写为 EVM 的ADDMOD指令。若缺了这两个前置条件，Z3 会立刻找到反例（例如A不是 2 的幂时两者不等价）。这正体现了形式化证明对"规则适用条件"的严格把关。同类还有 mod_mul_to_mulmod.py。

用例三：SIGNEXTEND 与移位组合（signextend_shl.py）

signextend_shl.py 证明如下规则：

SHL(A, SIGNEXTEND(B, X)) -> SIGNEXTEND((A >> 3) + B, SHL(A, X)) 前置条件：A & 7 == 0 且 A <= 256 且 B <= 32

要点在于A必须是 8 的倍数（A & 7 == 0），否则移位量与符号扩展的字节边界不对齐，变换不成立。该目录还配套了 signextend.py、signextend_and.py、signextend_equivalence.py、signextend_shr.py 等一整套围绕SIGNEXTEND的证明。

用例四：移位抵消与掩码（combine_shl_shr_by_constant_64.py）

combine_shl_shr_by_constant_64.py 证明"先左移再右移"可以折叠为一次移位加一次掩码操作（在 64 位字长上验证）：

SHR(B, SHL(A, X)) -> 根据 A 与 B 的大小关系，化简为 AND(SHL(A - B, X), Mask) 或 AND(SHR(B - A, X), Mask) 或 AND(X, Mask) 前置条件：A < 64 且 B < 64

其中Mask = SHR(B, SHL(A, -1))恰好是shlWorkaround(u256(-1), A) >> B的位向量版本——与 RuleList.h 中shlWorkaround的掩码计算一一对应，是"证明脚本与 C++ 实现逐行对照"的绝佳例证。同类用例还包括 combine_shr_shl_by_constant_64.py、combine_byte_shl.py、combine_div_shl_one_32.py 等。

用例五：幂等化简（repeated_or.py）

repeated_or.py 证明OR的幂等性化简（OR(OR(X, Y), Y) -> OR(X, Y)等四种排列），并通过 4 次rule.check逐一验证。类似的 repeated_and.py、and_distributed_over_shl.py、move_and_across_shl_128.py 覆盖了位运算分配律与移动规则。

运行证明与接入 CI

手动运行单个证明

所有证明脚本都是可直接执行的 Python 程序，唯一的运行时依赖是 Z3（pip install z3-solver）。以目录内最常见写法为例：

python3 test/formal/mod_add_to_addmod.py

脚本内部通过rule.check(...)触发求解：若规则成立则静默退出（退出码 0）；若 Z3 找到反例，rule.py会打印Rule is incorrect. Model: ...并以退出码 1 结束。因此证明脚本本身就是"可自证"的测试程序，无需额外断言框架。

CI 中的批量证明

scripts/run_proofs.sh 提供了面向 CI 的批量执行逻辑：

1. git fetch origin并计算git diff origin/develop --name-only test/formal/，只针对本次变更涉及的证明脚本；
2. 对每个*.py证明文件执行python3 "$new_proof"；
3. 若任一条证明失败（退出码非 0），打印Proof <name> failed并累计错误；
4. 全部通过时输出All proofs succeeded.。

也就是说，任何对test/formal/目录中证明脚本的新增或修改，都会在合并到 develop 前被自动重新验证，确保"优化规则的证明"与"优化规则本身"同步演进、始终可信。

目录速览：已覆盖的规则族

从 test/formal 目录结构可以系统梳理出已被形式化证明覆盖的规则族（对应 RuleList.h 中的相关规则）：

如何为一条新规则编写证明

结合上述框架，为 RuleList.h 中一条新优化规则补充形式化证明的标准流程如下：

1. 翻译指令语义：若规则涉及opcodes.py中尚未覆盖的指令，先按 EVM 规范（注意除零、溢出、越界等特殊分支）在opcodes.py中补充对应函数；
2. 编写证明脚本：新建test/formal/<rule_name>.py，参照 mod_add_to_addmod.py 的结构——导入Rule、opcodes、util，构造输入位向量，用require声明前置条件，用rule.check(nonopt, opt)断言优化前后等价；
3. 用反例校正前置条件：如果求解器返回sat并给出模型，说明当前前置条件不足或规则本身在边界下不成立，需要回到 RuleList.h 核对规则的实际守卫条件；
4. 运行验证：本地执行python3 test/formal/<rule_name>.py确认退出码为 0，再通过 scripts/run_proofs.sh 在 CI 上随变更自动复验。

小结

test/formal 目录展示了把"编译器优化规则的形式化验证"落地为可执行、可回归的工程实践：以 Z3 位向量逻辑精确复刻 EVM 指令语义，以Rule类统一"前置条件 + 等价断言"的证明协议，以约 40 个按规则拆分的脚本覆盖带检查算术、取模改写、SIGNEXTEND、移位掩码、幂等化简等规则族，并借助 run_proofs.sh 接入 develop 分支的差异检查。这套框架既为 libevmasm/RuleList.h 中的每条规则提供了可审计的正确性证据，也为后续新增优化规则提供了标准化的验证入口，是"用 SMT 求解器守护编译器优化正确性"的完整范本。

【免费下载链接】soliditySolidity, the Smart Contract Programming Language项目地址: https://gitcode.com/GitHub_Trending/so/solidity