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 和 BitVectorsSMT-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)核心验证方法分两步求解先检查前置条件本身是否可满足unsat说明条件自相矛盾脚本设计有误unknown说明求解器无法判定在满足前置条件的模型上再断言_nonopt ! _opt若结果为sat则打印 Z3 给出的反例模型并退出Rule is incorrect. Model: ...若为unsat则说明在全部满足前置条件的输入下优化前后结果必然一致证明成立。setTimeout(60000)默认给求解器设置 60 秒超时防止复杂位向量约束导致求解时间失控。一个值得注意的工程细节check通过solver.push()/solver.pop()隔离两次检查避免前置条件污染第二次等价性判定。util.pyEVM 语义的位向量建模辅助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.pyEVM 指令的语义化翻译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*87位做符号扩展越界时原样返回SHL/SHR/SAR分别对应算术左移、逻辑右移、算术右移。正是因为这层翻译与 EVM 实际执行语义逐位对应MOD(ADD(X, Y), A) ADDMOD(X, Y, A)这类规则才可能在除零、溢出等边界上被严格检验。典型证明用例剖析用例一带检查的无符号加法checked_uint_add.pychecked_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.pymod_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.pysignextend_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.pycombine_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.pyrepeated_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 程序唯一的运行时依赖是 Z3pip 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 的批量执行逻辑git fetch origin并计算git diff origin/develop --name-only test/formal/只针对本次变更涉及的证明脚本对每个*.py证明文件执行python3 $new_proof若任一条证明失败退出码非 0打印Proof name failed并累计错误全部通过时输出All proofs succeeded.。也就是说任何对test/formal/目录中证明脚本的新增或修改都会在合并到 develop 前被自动重新验证确保优化规则的证明与优化规则本身同步演进、始终可信。目录速览已覆盖的规则族从 test/formal 目录结构可以系统梳理出已被形式化证明覆盖的规则族对应 RuleList.h 中的相关规则规则族代表性证明脚本带检查的算术溢出/下溢checked_uint_add.py、checked_int_add.py、checked_int_div.py、checked_int_sub.py、checked_uint_sub.py、checked_int_mul_12.py、checked_uint_mul_12.py取模/乘法改写为 ADDMOD/MULMODmod_add_to_addmod.py、mod_mul_to_mulmod.pySIGNEXTEND 系列signextend.py、signextend_and.py、signextend_equivalence.py、signextend_shl.py、signextend_shr.py移位组合与掩码combine_shl_shr_by_constant_64.py、combine_shr_shl_by_constant_64.py、combine_byte_shl.py、combine_byte_shr_1.py、combine_byte_shr_2.py、combine_div_shl_one_32.py、combine_mul_shl_one_64.py、move_and_across_shl_128.py、move_and_across_shr_128.py、shl_workaround_8.py幂等与代数化简repeated_and.py、repeated_or.py、move_and_inside_or.py、and_distributed_over_shl.py、eq_sub.py、sub_sub.py、sub_not_zero_x_to_not_x_256.py、replace_mul_by_shift.py、exp_to_shl.py、exp_neg_one.pyBYTE 字节提取byte_big.py、byte_equivalence.py有符号取模smod.py类型清理函数signed_integer_cleanup_function.py、unsigned_integer_cleanup_function.py存储相关redundant_store_unrelated.py如何为一条新规则编写证明结合上述框架为 RuleList.h 中一条新优化规则补充形式化证明的标准流程如下翻译指令语义若规则涉及opcodes.py中尚未覆盖的指令先按 EVM 规范注意除零、溢出、越界等特殊分支在opcodes.py中补充对应函数编写证明脚本新建test/formal/rule_name.py参照 mod_add_to_addmod.py 的结构——导入Rule、opcodes、util构造输入位向量用require声明前置条件用rule.check(nonopt, opt)断言优化前后等价用反例校正前置条件如果求解器返回sat并给出模型说明当前前置条件不足或规则本身在边界下不成立需要回到 RuleList.h 核对规则的实际守卫条件运行验证本地执行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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考