区块链【免费下载链接】lndLightning Network Daemon ⚡️项目地址https://gitcode.com/gh_mirrors/ln/lnd点击查看免费下载本文以 lnd 仓库中 docs/alloy-models/linear-fee-function 目录下的 Alloy 轻量级形式化模型为主线完整讲解如何用 Alloy 对 lnd 默认的线性手续费提升函数LinearFeeFunction进行建模并通过一条核心断言复现真实代码中存在的 off-by-one 缺陷对应 issue #8741再验证修复方案的有效性。读完本文你将掌握线性手续费函数的字段与数学语义、Alloy 时间逻辑建模的基本套路以及如何用反例驱动的方式定位并修复边界条件错误。背景LinearFeeFunction 在 lnd 中的角色lnd 的扫帚sweeper子系统中FeeFunction接口负责为待广播/待替换RBF的交易计算手续费率其实现位于 sweep/fee_function.go。接口定义了两个核心方法sweep/fee_function.go#L38-L67FeeRate()返回当前计算出的手续费率Increment()/IncreaseFeeRate(confTarget)每次新块到来时推进一个步长并返回费率是否真的提升了若两次费率相同则无需 RBF。LinearFeeFunction是该接口的默认线性实现其数学语义在注释中写得很清楚sweep/fee_function.go#L69-L76feeRate startingFeeRate position * delta - width: deadlineBlockHeight - startingBlockHeight - delta: (endingFeeRate - startingFeeRate) / width - position: currentBlockHeight - startingBlockHeight即在起始费率与最大费率endingFeeRate之间线性插值费率永远不会超过endingFeeRate。其中width是起始块高到 deadline 块高之间的块数position是从起始块算起已经经过的块数delta是每个块增加的费率。实际使用场景在 sweep/fee_bumper.go 的TxPublisher中交易首次发布时由 initializeFeeFunction 用最大允许费率、当前确认目标conf target和费率估计器初始化手续费函数此后每个新块到达时handleFeeBumpTx 会调用IncreaseFeeRate(confTarget)判断是否需要 RBF。sweep/README.md给出了一个直观的例子若以bitcoind作为费率估计器一个 deadline 为 1000 块、预算 200,000 sats、交易体积 500 vbytes 的输入手续费函数会被初始化为起始费率 10 sat/vB、结束费率 400 sat/vB、每块增量约 390 sat/kvBsweep/README.md#L139-L148。正是因为在 deadline 之前就应把费率加到最大、避免错过确认窗口这一语义极其依赖边界条件lnd 团队选择用 Alloy 对它做一次形式化检验并由此发现了真实代码中的一个 off-by-one 缺陷。为什么用 Alloy 来建模手续费函数按 docs/alloy-models/README.md 的说明这个目录存放的是用 Alloy 语言书写的轻量级形式化模型。与完整形式化方法不同Alloy 是一个有界模型检查器它不对所有实例做穷尽证明而是接受一组有界的参数与迭代步数然后在这个范围内寻找给定断言的反例counterexample。如果找不到反例只能说模型可能有效。Alloy 特别适合此类建模的原因有二语言表达力强且可读Alloy 语言贴近集合论与一阶逻辑可以用声明式的方式描述状态、事件与约束支持时间逻辑temporal logicAlloy 6 内置了always、eventually等时序算子可以表达状态机/交互式时间线这类问题而这正是手续费随区块高度推进的天然建模方式。模型文件位于 docs/alloy-models/linear-fee-function/linear-fee.als全文约 310 行下面对其结构做逐层拆解。模型全景linear-fee.als 的结构状态单个 LinearFeeFunction 实例模型用一个one sig LinearFeeFunction声明系统中只存在一个手续费函数实例linear-fee.als#L4-L52并定义了六个随时间变化的字段与 Go 结构体的字段一一对应字段含义Go 对应startingFeeRate起始手续费率startingFeeRateendingFeeRatedeadline 到达后的最大费率endingFeeRatecurrentFeeRate当前正在使用的费率currentFeeRatewidth起始块高到 deadline 的块数widthposition当前经过的块数进度positiondeltaFeeRate每块费率步长msat/kwdeltaFeeRate该签名内还附带若干隐式事实用于保证轨迹良构well-formedposition 0 position width进度不能为负、不能越过 deadline各费率字段必须为正数deltaFeeRate 1模型刻意把步长简化为 1因为 Alloy 对大整数算术支持有限这里的关注点是边界语义而非精确费率。初始化与迁移init / increment / fee_bump / stutterActiveFeeFunctions签名维护已激活函数集合配合feeFuncInitZeroValues与feeFuncSetStartsEmpty两个事实保证未激活的函数position必须为 0且轨迹最开始时集合为空linear-fee.als#L54-L76。init[f, maxFeeRate, startFeeRate, confTarget]谓词负责初始化当confTarget 0时直接跳到最大费率否则设置各字段并把f加入激活集合。注意f.width confTarget——模型中的width直接等于确认目标linear-fee.als#L79-L113。increment→increase_fee_rate实现费率的推进每经过一个块position加 1并用fee_rate_at_position[f, newPosition]计算新费率同时约束position width不得越界linear-fee.als#L115-L144。fee_rate_at_position是核心函数也是缺陷所在的位置linear-fee.als#L146-L160后面单独展开。fee_bump谓词带守卫只有已激活的函数才能推进stutter谓词则允许轨迹空转用于让时间线在非迁移状态下继续推进linear-fee.als#L162-L182。事件与轨迹约束为了让生成的轨迹更易读模型使用事件具体化event reification惯用法定义enum Event { Stutter, Init, FeeBump }并用派生关系把各事件与对应的状态迁移谓词绑定linear-fee.als#L184-L212。随后用三个fact约束轨迹形态traces每个时间步至少发生一个事件init_traces轨迹中最终至少有一次Initfee_bump_happens轨迹中最终至少有一次FeeBump。linear-fee.als#L214-L230辅助谓词与已带断言模型还定义了若干可复用的谓词与断言bump_to_completion持续 bump 直到position width正好到 deadlinebump_to_final_block持续 bump 直到position width.sub[1]deadline 前一块req_num_blocks_to_conf[n]/req_starting_fee_rate[n]把函数约束到指定确认目标/起始费率三个辅助断言init_correctness、init_always_happens、init_then_fee_bump分别验证初始化语义与轨迹性质文件末尾的默认run命令生成一条确认目标恒为 4、且 bump 到完成的轨迹。linear-fee.als#L266-L311核心断言 max_fee_rate_before_deadline 的语义整个模型的主断言是max_fee_rate_before_deadlinelinear-fee.als#L290-L304// max_fee_rate_before_deadline is the main assertion in this model. This // captures a model violation for our fee function, but only if the line in // fee_rate_at_position is uncommented. // // In this assertion, we declare that if we have a fee function that has a conf // target of 4 (we want a few fee bumps), and we bump to the final block, then // at that point our current fee rate is the ending fee rate. In the original // code, assertion isnt upheld, due to an off by one error. assert max_fee_rate_before_deadline { always req_num_blocks_to_conf[4] bump_to_final_block eventually ( all f: LinearFeeFunction | f.position f.width.sub[1] f.currentFeeRate f.endingFeeRate ) }逐层翻译这段时序逻辑always req_num_blocks_to_conf[4]所有时间步上函数的确认目标恒为 4即有多次 bump 机会 bump_to_final_block并且不断 bump直到position到达width - 1 eventually (f.position f.width.sub[1] f.currentFeeRate f.endingFeeRate)那么最终在position等于width - 1deadline 前一块时当前费率必须已经等于endingFeeRate。这个断言捕捉的正是产品语义我们希望在 deadline 到达之前就把预算花满从而给交易留出尽量多的确认窗口。 若手续费函数要等position width正好到 deadline才封顶就晚了整整一个块——这正是 issue #8741 描述的 off-by-one 缺陷。在 Alloy Analyzer 中复现 off-by-one 缺陷模型附带的 walk-through 展示了如何把缺陷放回模型并用反例证实它。整个过程分两步第 1 步对主断言执行check。在模型中强制检查max_fee_rate_before_deadlinecheck max_fee_rate_before_deadline第 2 步取消注释有问题的分支把 off-by-one 错误重新引入fee_rate_at_positionp f.width f.endingFeeRate // -- NOTE: Uncomment this to re-introduce the original bug.在 Alloy Analyzer 中点击Execute求解器会立即给出反例Counterexample found. Assertion is invalid.提示断言不成立。也就是说存在一条轨迹——确认目标为 4、不断 bump——到达 deadline 前一块时currentFeeRate仍未达到endingFeeRate。这正是原始 Go 代码的行为。点击Show可以打开可视化视图时间线中展示LinearFeeFunction状态节点与Init、FeeBump、Stutter等事件节点以及position、width、currentFeeRate、startingFeeRate、endingFeeRate、deltaFeeRate各字段随时间步04的变化。可以看到即使position已经位于 deadlinewidth前一块currentFeeRate还是没有到达endingFeeRate——与 issue #8741 的描述完全一致。修复模型并验证修复方式同样直白把fee_rate_at_position的封顶条件从width改为width - 1即width.sub[1]p f.width.sub[1] f.endingFeeRate再次对同一断言执行checkAlloy 输出变为No counterexample found. Assertion may be valid.——在既有界范围内再也找不到违反断言的轨迹说明deadline 前一块费率已封顶这一性质在该修复下成立。这也再次体现了轻量级形式化方法的价值它不要求证明模型在所有实例下都正确而是通过高效寻找反例把边界错误转化为可观察、可重现、可验证的形式化结论。从模型回到 Go 源码width 减一的由来Alloy 模型与 Go 实现之间的-1关系值得点透。在模型里width被定义为确认目标本身f.width confTarget因此提前一块封顶写作p width.sub[1]而在真实 Go 代码中这个-1被直接算进了width字段// width is the number of blocks between the starting block height // and the deadline block height minus one. // // NOTE: We do minus one from the conf target here because we want to // max out the budget before the deadline height is reached. width uint32NewLinearFeeFunction在初始化时执行width confTarget - 1sweep/fee_function.go#L136-L140同时把confTarget 1的极端情况直接短路为立即使用最大费率sweep/fee_function.go#L125-L134。于是修复后的封顶判断在 Go 中写作func (l *LinearFeeFunction) feeRateAtPosition(p uint32) chainfee.SatPerKWeight { if p l.width { return l.endingFeeRate } ... }sweep/fee_function.go#L267-L284因为width已经预先减一这里p l.width在语义上就等价于 Alloy 修复后的p width.sub[1]——即从 deadline 前一块开始直接封顶到endingFeeRate。反过来若 Go 代码当初采用width不减一、封顶条件为p width的写法对应 Alloy 中被注释掉的错误分支就会得到同样的 off-by-one 缺陷。这也解释了为什么模型注释把错误分支标为取消注释以重新引入原始 bug。单元测试 sweep/fee_function_test.go 对这一语义有直接验证TestLinearFeeFunctionFeeRateAtPosition构造width 3、起始费率 1000、结束费率 3000、deltaFeeRate 1_000_000的函数断言position 2即width - 1时返回 3000position 3时仍为 3000sweep/fee_function_test.go#L214-L269TestLinearFeeFunctionIncrement用确认目标 9width 8逐块推进验证第 8 块时费率已达最大再推进会返回ErrMaxPositionsweep/fee_function_test.go#L271-L321TestLinearFeeFunctionIncreaseFeeRate验证IncreaseFeeRate(1)会一步跳到结束费率而IncreaseFeeRate(0)触发ErrMaxPositionsweep/fee_function_test.go#L323-L393。此外构造阶段还有两个值得注意的细节deltaFeeRate以 msat/kw 为单位放大精度(end - start) * 1000 / width见 sweep/fee_function.go#L157-L176而当 delta 为 0 且width ! 1时预算过小导致起始费率等于结束费率会返回ErrZeroFeeRateDelta——对应的TestLinearFeeFunctionNewZeroFeeRateDelta也覆盖了这一分支。小结这条从 Alloy 模型到 Go 代码的对照链条展示了形式化方法在真实工程中的落地方式先用可读的声明式语言把deadline 前一块费率必须封顶这条业务语义固化为断言再由模型检查器在有限界内找出反例从而在正式测试之前就锁定 off-by-one 边界错误修复后再用同一断言验证结论。该模型的完整源码在 docs/alloy-models/linear-fee-function/linear-fee.als对应的 Go 实现、单元测试与使用场景分别在 sweep/fee_function.go、sweep/fee_function_test.go 和 sweep/fee_bumper.go读者可以在本地 Alloy Analyzer 中打开模型文件按文中步骤亲自复现反例与修复验证。赞分享区块链【免费下载链接】lndLightning Network Daemon ⚡️项目地址https://gitcode.com/gh_mirrors/ln/lnd点击查看免费下载相关推荐用 Alloy 形式化建模 lnd 的线性费率函数复现并修复 fee bumping 的 off-by-one 缺陷用 Alloy 形式化建模 lnd 的线性费率函数复现并修复 fee bumping 的 off by one 缺陷 本篇技术指南围绕 lndLightni区块链Composio 回归测试指南从复现缺陷到提交可验证的修复Composio 回归测试指南从复现缺陷到提交可验证的修复 导读 本文面向 Composio SDK 的贡献者与维护者系统讲解在仓库中开展回归测试Regr人工智能AI Agent工具调用MCP 服务MCP ClientsEMQX 修复 MQTT 5.0 Maximum Packet Size 边界判定出站数据包 off-by-one 问题解析EMQX 修复 MQTT 5.0 Maximum Packet Size 边界判定出站数据包 off by one 问题解析 导读 本篇文章围绕 EMQX 开后端物联网消息队列通信创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考