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/symbolicFoundry 原生符号执行器是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_operandsopt.rs#L1327-L1348只接受Ult/Ule两种无符号比较操作符并要求一侧是UDiv表达式分子任意、分母必须是常量且非零另一侧不含UDiv即纯阈值表达式可以是符号变量或常量。它返回(分子, 常量分母, 阈值, 商是否在左侧)四元组。3.2 重写规则把除法比较变为乘法比较normalize_udiv_comparisonopt.rs#L1350-L1381实现了两条经典的不等式等价规则注意对Ule/Ult的处理要区分商在左还是在右原形式重写后说明n / d k商在左Ultn k * d阈值不变n / d k商在左Ulen (k1) * d阈值1后转为严格小于k n / d商在右Ulek * d n阈值不变k n / d商在右Ult(k1) * 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_contextualopt.rs#L2265-L2291构造了quotient numerator / 1e18comparison quotient thresholdbounded 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_factsmonotonic_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_equalmonotonic_product.rs#L181-L206match (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_orderedmonotonic_product.rs#L278-L293、#L222-L232并通过product_less_than_known/product_less_or_equal_known对乘数做四种排列组合尝试。这一层推理的意义在于很多“乘法后除以常量”的表达式在重写为纯乘法形式后可以直接由单调性事实判定完全无需求解器介入从而把求解工作量降到最低也提升了整体完备性。5. 除法消除在整体求解管线中的位置要理解本补丁的价值需要把上述重写放进符号执行器的完整求解管线。结合 README 的 How It Works 与源码结构求解流程大致为符号执行器沿路径累积约束约束进入ConstraintContextopt.rs进行上下文相关的布尔/字级归一化normalize_udiv_comparison对n/dvs 阈值的比较做除法消元本补丁核心normalize_udiv_eq_zero/normalize_udiv_cmp等其他归一化规则处理除法等于零、商与常量比较等形态同时应用mul_div_identityx*d/d x、masked_word_eq_selfx 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 等。可见本补丁作用于第 23 步目标是把“除法比较”在进入第 45 步之前就消解掉从而显著提高这类常见模式的求解完备性——这正是 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_CONFORMANCE1 cargo test -p forge --test cli symbolic_conformance -- --nocapture SYMBOLIC_LIMITS1 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需要本机装有可用的求解器默认命令为z3macOS 可brew install z3Ubuntu 可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 测试一样可用的证明工具”演进的一小步。延伸阅读仓库内路径crates/evm/symbolic/README.md符号执行器完整文档Quick Start、配置、已知限制、排障。crates/evm/symbolic/src/runtime/solver/opt.rs除法比较重写与上下文归一化主实现。crates/evm/symbolic/src/runtime/solver/monotonic_product.rs序关系事实与单调乘积推理。crates/evm/symbolic/src/runtime/solver/hard_arith_fallback.rs硬算术启发式回退搜索。crates/evm/symbolic/assets/symbolic-result.schema.json符号化测试结果 JSON schema。【免费下载链接】foundryFoundry is a blazing fast, portable and modular toolkit for Ethereum application development written in Rust.项目地址: https://gitcode.com/GitHub_Trending/fo/foundry创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考