Foundry 符号执行引擎改进：无符号常量除法比较的完备性优化（foundry-evm-symbolic）-创锋一号

Foundry 符号执行引擎改进：无符号常量除法比较的完备性优化（foundry-evm-symbolic）

【免费下载链接】foundryFoundry is a blazing fast, portable and modular toolkit for Ethereum application development written in Rust.项目地址: https://gitcode.com/GitHub_Trending/fo/foundry

导读

本文围绕 Foundry 原生符号执行引擎（foundry-evm-symbolic，支撑forge test --symbolic）的一次关键补丁展开：在符号化路径探索中，对“与常量除法的商进行比较”这类受限模式（bounded comparisons against unsigned division by constant scales）实现了更完备的求解。文章先交代补丁背景与价值，再深入源码剖析其实现机制（含除法消元重写、无溢出界分析、单调性事实推理等），最后给出可复现验证方式。读完你将理解 Foundry 符号执行器如何在不引入非线性除法项的前提下证明/推翻这类性质，并能在自己的符号化测试中实际运用。

1. 补丁背景：一条 changelog 背后的能力提升

仓库根目录下.changelog/symbolic-udiv-comparisons.md记录了本次变更：

foundry-evm-symbolic: patch Improved symbolic completeness for bounded comparisons against unsigned division by constant scales.

翻译成技术语言即：针对“对无符号除法（UDIV）的商与某个阈值/常量进行比较”的受限模式，提升了符号执行求解的完备性。这是foundry-evm-symboliccrate 的一次 patch 级变更，修复/增强的点位于该 crate 的符号求解与约束归一化路径。

这类模式在真实 Solidity 代码中极其常见，典型形态包括：

缩放换算：uint256 scaled = amount * 1e18 / 1e18;，随后require(scaled >= threshold)；
精度换算：credits = value * creditsPerToken / 1e18；
比例/费率判断：require(total * feeBps / 10000 <= cap)；
各类“乘以常量后再除以常量”的比例逻辑，以及(x + d - 1) / d（向上取整除法）形态。

这些表达式里出现除法（且常伴随乘法），属于符号执行中典型的“硬算术”（hard arithmetic）问题。对 SMT 求解器而言，位向量除法（bvudiv）往往导致求解不稳定、超时或返回unknown。本补丁的目标，就是让这些有界场景不再退化为不完整（incomplete）结果，而是能够被局部推理直接消解，或交给求解器时已转化为更易处理的乘法/比较形式。

该补丁的上下文位于 crates/evm/symbolic：Foundry 原生符号执行器，是forge test --symbolic的后端引擎。大多数用户通过 Forge 间接使用它，其入口是check*/prove*符号化测试函数，以及invariant*/statefulFuzz*的有状态符号化不变量检查。

2. 符号执行中的“硬算术”与除法难题

在进入实现细节前，先理解本补丁所处的技术背景。符号执行器在探索路径时会累积路径约束（path constraints），每条分支条件都会被加入约束集，然后交给 SMT 求解器判断可行性并提取反例模型。

在 hard_arith_fallback.rs 中，is_hard_arith_node明确将以下形态归类为“硬算术”：

fn is_hard_arith_node(expr: &SymExpr) -> bool { match expr.kind() { SymExprKind::BinOp(SymBinOp::Mul, left, right) => { left.contains_var() && right.contains_var() } SymExprKind::BinOp( SymBinOp::UDiv | SymBinOp::URem | SymBinOp::SDiv | SymBinOp::SRem, left, right, ) => left.contains_var() || right.contains_var(), SymExprKind::TernOp(_, left, right, modulus) => { left.contains_var() || right.contains_var() || modulus.contains_var() } _ => false, } }

也就是说：只要除法表达式的分子或分母含有符号变量，它就被标记为硬算术。硬算术会让求解路径变慢甚至超时，最终导致Incomplete（见 README 的已知限制表格中 “Hard arithmetic” 一节）。

本补丁的策略不是直接去求解bvudiv，而是在送入求解器之前，用局部重写消除有界场景下的除法，或者把除法比较等价转换为更简单的乘法/比较形式。这样既提升了求解完备性（更少Incomplete），也减少了求解器负担。

3. 核心机制一：除法比较的等价重写（UDiv 消元）

补丁的核心实现位于 opt.rs 中的ConstraintContext及相关辅助函数。

3.1 识别“UDiv vs 阈值”比较

udiv_comparison_operands（opt.rs#L1327-L1348）只接受Ult/Ule两种无符号比较操作符，并要求：

一侧是UDiv表达式（分子任意、分母必须是常量且非零）；
另一侧不含UDiv（即纯阈值表达式，可以是符号变量或常量）。

它返回(分子, 常量分母, 阈值, 商是否在左侧)四元组。

3.2 重写规则：把除法比较变为乘法比较

normalize_udiv_comparison（opt.rs#L1350-L1381）实现了两条经典的不等式等价规则（注意：对Ule/Ult的处理要区分商在左还是在右）：

原形式	重写后	说明
`n / d < k`（商在左，`Ult`）	`n < k * d`	阈值不变
`n / d <= k`（商在左，`Ule`）	`n < (k+1) * d`	阈值+1后转为严格小于
`k <= n / d`（商在右，`Ule`）	`k * d <= n`	阈值不变
`k < n / d`（商在右，`Ult`）	`(k+1) * d <= n`	阈值+1后转为小于等于

源码中的阈值递增逻辑由increment_threshold控制：

let increment_threshold = matches!((op, quotient_on_left), (SymCmpOp::Ule, true) | (SymCmpOp::Ult, false)); let threshold = if increment_threshold { // Prove the successor cannot wrap before constructing the word addition. self.interval(threshold)?.max.checked_add(U256::ONE)?; let one = SymExpr::one(cx); SymExpr::binop(cx, SymBinOp::Add, threshold.clone(), one) } else { threshold.clone() };

关键细节：对阈值执行+1之前，必须先通过区间分析（self.interval(threshold)）证明threshold + 1不会发生 256 位回绕（wrap）。checked_add返回None即代表可能回绕，此时放弃重写（返回None），保持原约束不变——这保证了重写始终在模 2^256 语义下精确成立。

3.3 无溢出前提：乘法比较的合法性

重写后的形式是n < k*d或k*d <= n。在 256 位字上，乘法可能溢出，因此重写必须附加无溢出前提：

if !self.mul_cannot_overflow_256(&threshold, denominator) { return None; } let scaled_threshold = SymExpr::binop(cx, SymBinOp::Mul, threshold, denominator.clone());

mul_cannot_overflow_256基于ConstraintContext从路径约束中推导的区间（interval）信息判断threshold * denominator是否必然落在 2^256 之内。若无法证明无溢出，则保守放弃重写，把原约束原样交给求解器或硬算术回退路径。这正是 changelog 中 “bounded comparisons”（有界比较）一词的来源：只有当阈值区间有界、乘法不溢出时，重写才是完备的。

3.4 一致性：上下文敏感，缓存不误用

重写必须依赖当前路径的约束上下文（例如阈值上界约束），而不能脱离上下文做“无条件重写”，否则可能在不满足前提的路径上错误消元。源码用单元测试专门锁定了这一点：

cached_normalization_keeps_udiv_rewrites_contextual（opt.rs#L2265-L2291）构造了：

quotient = numerator / 1e18
comparison = quotient <= threshold
bounded = threshold <= uint128_max（阈值上界约束）

在“comparison + bounded 同时存在”时，归一化后的约束集不再包含任何UDiv节点（normalized.iter().all(|constraint| !constraint.contains_udiv())），说明重写成功消元；而单独归一化comparison时，由于缺少上界上下文，约束保持原样。这一测试精确验证了“上下文敏感的重写 + 缓存不误用”的正确性。

4. 核心机制二：单调性事实推理（Monotonic Product Facts）

除法比较重写只是本次补丁的一部分。在 monotonic_product.rs 中，求解器还会从路径约束中提取“序关系事实”（order facts），用以在不调用 SMT 求解器的情况下判定矛盾或消解约束。

4.1 序关系事实的收集

collect_order_facts（monotonic_product.rs#L89-L150）从And合取、Ult/Ugt/Ule/Uge/Eq及Not取反中提取三类事实：

less_than：严格小于关系对；
less_or_equal：弱小于关系对；
positive：被证明非零（正）的表达式，例如从0 < x、x > 0或x != 0推导。

4.2 关键推理：同分母商的大小比较

本次补丁与除法直接相关的一条推理位于expr_less_or_equal（monotonic_product.rs#L181-L206）：

match (left.kind(), right.kind()) { ( SymExprKind::BinOp(SymBinOp::UDiv, left_num, left_den), SymExprKind::BinOp(SymBinOp::UDiv, right_num, right_den), ) if left_den == right_den => expr_less_or_equal(left_num, right_num, facts, bounds), ... }

即：若两个商的分母（常量缩放系数）相同，则“商 a <= 商 b”当且仅当“分子 a <= 分子 b”，可递归地用已有的分子序事实判定。这条规则在 README 已知限制的 “Hard arithmetic” 一节中也有对应描述：Foundry “proves unsigned monotonic product and same-divisor quotient comparisons when path bounds show that every product fits in 256 bits”。这里的 “same-divisor quotient comparisons” 正是该分支实现的。

4.3 单调乘积推理

同一文件中还实现了经典的无符号单调性规则：

若0 < a、0 < b、a < c、b < d，且a*b、c*d均不溢出，则a*b < c*d；
若a <= c、b <= d且乘积不溢出，则a*b <= c*d。

其实现函数为product_less_than_known_ordered/product_less_or_equal_known_ordered（monotonic_product.rs#L278-L293、#L222-L232），并通过product_less_than_known/product_less_or_equal_known对乘数做四种排列组合尝试。

这一层推理的意义在于：很多“乘法后除以常量”的表达式，在重写为纯乘法形式后，可以直接由单调性事实判定，完全无需求解器介入，从而把求解工作量降到最低，也提升了整体完备性。

5. 除法消除在整体求解管线中的位置

要理解本补丁的价值，需要把上述重写放进符号执行器的完整求解管线。结合 README 的 How It Works 与源码结构，求解流程大致为：

符号执行器沿路径累积约束；
约束进入ConstraintContext（opt.rs），进行上下文相关的布尔/字级归一化：
- normalize_udiv_comparison：对n/dvs 阈值的比较做除法消元（本补丁核心）；
- normalize_udiv_eq_zero/normalize_udiv_cmp等其他归一化规则处理除法等于零、商与常量比较等形态；
- 同时应用mul_div_identity（x*d/d == x）、masked_word_eq_self（x & mask == x）、ceil-div 形态化简（(x*d + d - 1)/d == x）等规则（见 opt.rs#L866-L942）；
在 monotonic_product.rs 中利用序事实做无求解器的局部矛盾判定 / 隐含约束消除（product_monotonic_unsat_normalized、remove_implied_monotonic_constraints）；
若约束仍含硬算术（如bvudiv、不可消元的乘法），进入 hard_arith_fallback.rs 的启发式回退：对少量变量（HARD_ARITH_FALLBACK_MAX_VARS限制）在精心挑选的候选值（0、1、2、3、U256::MAX及路径常量、2 的幂等）上做有界搜索构造模型；
仍无法解决时，才把（已尽可能归一化、弱化的）约束交给外部 SMT 求解器（z3、cvc5、yices、bitwuzla 等）。

可见，本补丁作用于第 2～3 步，目标是把“除法比较”在进入第 4～5 步之前就消解掉，从而显著提高这类常见模式的求解完备性——这正是 changelog 中 “Improved symbolic completeness” 的含义。

6. 实际意义与适用边界

6.1 对符号化测试的收益

在编写check*/prove*符号化测试（参考 README Quick Start）时，凡是涉及“缩放/比例/费率”的断言，例如：

function check_fee(uint256 amount) external pure { uint256 fee = amount * 100 / 10000; // amount / 100 assertLe(fee, amount); // 商与自身比较 } function check_scaled(uint256 value) external pure { uint256 scaled = value * 1e18 / 1e18; // 恒等缩放 assertEq(scaled, value); }

这类约束此前可能落入硬算术回退甚至Incomplete，本次补丁后可在有界前提（阈值区间已知、乘积不溢出）下被局部推理完备处理，输出PASS或可重放的具体反例。

6.2 边界与限制（必须注意）

重写只对常量分母、非零分母生效；符号分母或零分母不在normalize_udiv_comparison的处理范围（见 opt.rs#L1336）。
必须能证明乘法不溢出，否则放弃重写。
阈值 +1 前必须证明不回绕（checked_add失败即放弃）。
重写是上下文敏感的：缺少阈值上界等前提约束时，即使形态匹配也不会消元（opt.rs#L2265-L2291 的测试即验证此点）。
超出这些有界前提的模式仍可能落入Incomplete（原因可能是超时、unknown、硬算术回退耗尽等），此时应参照 README Troubleshooting 调整symbolic.max_paths、symbolic.max_solver_queries、symbolic.timeout等界限，或简化属性。

7. 验证与复现

7.1 运行相关测试

该补丁的推理逻辑（除法消元、单调性事实、上下文缓存）都有对应单元测试。可在仓库根目录执行：

cargo test -p foundry-evm-symbolic

重点关注的测试包括 opt.rs 中的cached_normalization_keeps_udiv_rewrites_contextual以及 monotonic_product.rs 中的product_monotonic_unsat相关用例。

7.2 端到端符号化测试（需 z3）

若想验证补丁在真实 Forge 流程中的表现，按 README 开发检查的方式运行：

cargo check -p forge cargo test -p forge --test cli test_cmd::symbolic -- --nocapture

更慢但覆盖面更广的符合性/界限套件（需 Z3）为：

SYMBOLIC_CONFORMANCE=1 cargo test -p forge --test cli symbolic_conformance -- --nocapture SYMBOLIC_LIMITS=1 cargo test -p forge --test cli symbolic_limits -- --nocapture

其中symbolic_limits专门检查路径宽度、执行深度、calldata 预算、硬算术与不变量序列深度等资源边界，与本补丁讨论的“有界比较”直接相关。

7.3 动手编写一个可观察的符号化测试

创建如下 Solidity 测试（例如放入项目的test/目录）：

// SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.20; import "forge-std/Test.sol"; contract ScaleSymbolicTest is Test { /// forge-config: default.symbolic.timeout = 60 function check_scale_bound(uint256 value) external pure { uint256 scaled = value * 1e18 / 1e18; // value / 1 assertEq(scaled, value); } function check_fee_property(uint256 amount) external pure { uint256 fee = amount * 100 / 10000; // amount / 100 assertLe(fee, amount); } }

运行：

forge test --symbolic --match-test "check_scale_bound|check_fee_property"

需要本机装有可用的求解器（默认命令为z3；macOS 可brew install z3，Ubuntu 可sudo apt-get install z3）。观察输出：若属性成立，得到PASS；若求解器发现反例，Forge 会先在普通执行器上具体重放、确认后才报告FAIL及反例（README Result Semantics）。

8. 小结

.changelog/symbolic-udiv-comparisons.md记录的是一次小而精的引擎级补丁：通过 opt.rs 中的normalize_udiv_comparison把“有界无符号常量除法比较”重写为等价且无溢出的乘法比较，再配合 monotonic_product.rs 的“同分母商比较”与单调乘积事实推理，在送入外部 SMT 求解器之前就地消解大部分除法硬算术。它没有改变符号执行的公开接口，但提升了常见比例/缩放/费率类属性的求解完备性，并保持了“上下文敏感、前提不满足即放弃、反例必须具体重放”的可靠性原则。

对于符号化测试使用者而言，这意味着：只要除法分母是常量、比较对象有界、相关乘法不溢出，这类属性更有可能得到确定的PASS或可重放反例，而不是笼统的Incomplete。这也是 Foundry 符号执行器持续向“像普通 Forge 测试一样可用的证明工具”演进的一小步。

企业官网建设流程全解析