使用 Move Prover 形式化验证 DeFi 合约Aptos 仓库 reserve 与 uniswap 示例深度解析【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core导读本篇文章基于 aptos-core 仓库中third_party/move/move-examples/experimental/defi包的 README.md深入剖析两个为 Move Prover 形式化验证量身打造的 DeFi 合约示例储备支撑货币系统reserve.move与 Uniswap v1 风格自动做市商uniswap.move。通过本文你将掌握如何用 Move 规范语言MSL表达储备充足率恒定乘积不变量无免费午餐定理等关键安全属性理解规范spec块与实现函数体如何配合、aborts_if/ensures/invariant等关键语法的实战写法以及故意注入错误实现的反例教学方法论——这是学习 Move Prover 与智能合约安全验证的最佳入门样本之一。包概览为验证而生的精简 DeFi 合约该示例包位于 third_party/move/move-examples/experimental/defi与basic-coin、coin-swap、math-puzzle、verify-sort等示例一同归属于 move-examples/experimental 目录是 Move 生态中面向规范与验证设计的实验性示例集合。包内结构非常简单清晰文件作用sources/reserve.move储备支撑货币系统含故意错误的实现sources/uniswap.moveUniswap v1 风格 AMM 池含白皮书有缺陷算法Move.toml包清单与依赖声明README.md包说明从 Move.toml 可以看到包的依赖与地址布局[package] name DeFi version 0.0.0 [addresses] std 0x1 defi 0xDEF1 [dependencies] MoveStdlib { local ../../../move-stdlib }关键点在于地址defi被固定为0xDEF1两个合约模块defi::reserve与defi::uniswap都部署在该地址下合约内通过常量ADMIN/PoolAddr直接引用defi依赖MoveStdlib以本地路径形式引入 move-stdlib其中fixed_point32模块fixed_point32.move提供了定点数运算及其配套的规范函数spec_multiply_u64、spec_create_from_rational是 reserve 示例规范编写的基石。与生产级 DeFi 合约不同这两个示例刻意做了减法没有事件、没有权限管理、没有 flash loan 等复杂逻辑只保留最核心的资金流操作。这种精简使得每条路径都能被 Prover 在可接受的时间内穷举验证也让学习者能够聚焦于写规范—写实现—验证属性这条主线。一、reserve.move储备支撑货币系统1.1 业务语义货币完全由储备支撑reserve模块sources/reserve.move实现了一个最简化的储备支撑货币系统一种货币Coin1的价值完全由另一种货币Coin2的储备支撑任何用户都可以通过存入 Coin2 铸造 Coin1或者销毁 Coin1 赎回等值的 Coin2。系统状态存储在单一资源中struct Coin1Info has key { total_value: u64, // Coin1 的总供应量 reserve_coin2: ReserveComponent, } struct ReserveComponent has store { backing_value: u64, // 储备中 Coin2 的总量 backing_ratio: FixedPoint32, // 每单位 Coin1 需要锁定的 Coin2 数量储备比率 }核心不变量写在Coin1Info的spec块里这是整个合约最重要的安全属性spec Coin1Info { // Safety property: the backing value always satisfies the backing ratio. invariant fixed_point32::spec_multiply_u64(total_value, reserve_coin2.backing_ratio) reserve_coin2.backing_value; }它表达的语义是Coin1 总供应量 × 储备比率 ≤ 储备中的 Coin2 总量即系统在任何状态下都满足全额储备要求——每一枚已发行的 Coin1 背后都有足额的 Coin2 作为支撑没有人能凭空制造无抵押的 Coin1。这里使用的是fixed_point32的规范函数spec_multiply_u64它定义在 fixed_point32.move是专门在规范中表达定点乘法语义的抽象函数确保 Prover 在验证时不会因定点运算的取整误差而产生误报。1.2 铸造与销毁的完整实现铸造函数要求调用者提供与储备比率精确匹配的 Coin2 作为抵押public fun mint_coin1(amount_to_mint: u64, backing_coin2: u64): u64 // returns the minted Coin1. acquires Coin1Info { assert!(amount_to_mint 0, 1); let coin1info borrow_global_mutCoin1Info(ADMIN); let coin2_amount_to_reserve fixed_point32::multiply_u64(amount_to_mint, * coin1info.reserve_coin2.backing_ratio) 1; assert!(backing_coin2 coin2_amount_to_reserve, 2); coin1info.reserve_coin2.backing_value coin1info.reserve_coin2.backing_value coin2_amount_to_reserve; coin1info.total_value coin1info.total_value amount_to_mint; amount_to_mint }注意实现中的 1由于定点乘法存在向下取整实现额外多保留 1 个单位的 Coin2确保储备只多不少从实现层面就主动维护了上述不变量。backing_coin2必须是精确的应储备数量否则直接abort错误码 2。对应的spec块完整声明了函数的终止条件与后置条件spec mint_coin1 { let coin1info globalCoin1Info(ADMIN); let coin2_amount_to_reserve fixed_point32::spec_multiply_u64(amount_to_mint, coin1info.reserve_coin2.backing_ratio) 1; aborts_if amount_to_mint 0; aborts_if backing_coin2 ! coin2_amount_to_reserve; aborts_if globalCoin1Info(ADMIN).total_value amount_to_mint MAX_U64; aborts_if coin1info.reserve_coin2.backing_value backing_coin2 MAX_U64; aborts_if !existsCoin1Info(ADMIN); ensures globalCoin1Info(ADMIN).total_value old(globalCoin1Info(ADMIN).total_value) amount_to_mint; ensures globalCoin1Info(ADMIN).reserve_coin2.backing_value old(globalCoin1Info(ADMIN).reserve_coin2.backing_value) backing_coin2; ensures backing_coin2 coin2_amount_to_reserve; }这些声明对应 Prover 验证中最重要的几类条件规范语句含义验证价值aborts_if列出所有可能中止abort的路径防止规范遗漏证明函数在未声明条件下不会意外失败ensures ... old(...) ...精确刻画状态变更证明账本只按预期方式变动杜绝未声明的副作用ensures ... old(...) ...中的MAX_U64上界声明溢出路径捕获u64溢出这类在 Move 中会 abort 的情况这里的old(globalCoin1Info(ADMIN))是 MSL 的标准写法在ensures中引用函数执行前的全局状态用于描述状态前后的精确关系。销毁函数是对称操作public fun burn_coin1(amount_to_burn: u64): u64 // returns the Coin2 that was reserved. acquires Coin1Info { let coin1info borrow_global_mutCoin1Info(ADMIN); let coin2_amount_to_return fixed_point32::multiply_u64(amount_to_burn, * coin1info.reserve_coin2.backing_ratio); assert!(coin1info.reserve_coin2.backing_value coin2_amount_to_return, 1); coin1info.reserve_coin2.backing_value coin1info.reserve_coin2.backing_value - coin2_amount_to_return; coin1info.total_value coin1info.total_value - amount_to_burn; coin2_amount_to_return }销毁时按比率返还 Coin2并用assert!(backing_value coin2_amount_to_return, 1)防止储备被透支。1.3 故意注入的错误实现Prover 能力展示reserve.move的亮点在于随正确实现一起给出了两个故意写错的版本mint_coin1_incorrect在计算应储备的 Coin2 时去掉了 1第 53 行fixed_point32::multiply_u64(...)不带1导致因定点取整误差而少储备了 Coin2——这就违反了Coin1Info的全额储备不变量burn_coin1_incorrect在返还 Coin2 时反而加上了 1第 76 行导致销毁时多返还储备同样破坏不变量。这两个错误实现没有附对应的spec块这是刻意为之的教学反例运行 Prover 时它们会在Coin1Info的模块级invariant检查处被自动发现违反属性并给出反例counterexample让学习者直观看到安全属性如何拦住有缺陷的实现。这正是 README 中所说的demonstrate the Move Provers capabilities——用可控的缺陷演示形式化验证的检出能力。1.4 组合验证mint 后 burn 不能多拿钱模块最后提供了一个#[verify_only]标注的验证辅助函数#[verify_only]表示该函数仅存在于规范验证模型中不进入正式发布字节码#[verify_only] fun mint_and_burn(amount_to_mint: u64, backing_coin2: u64): u64 acquires Coin1Info { let coin1 mint_coin1(amount_to_mint, backing_coin2); let coin2 burn_coin1(coin1); coin2 } spec mint_and_burn { ensures result backing_coin2; }它证明一个组合性质先铸造再销毁最终拿回的 Coin2 不会超过最初投入的 Coin2result backing_coin2——即不存在铸币套利路径。由于mint_coin1内部1的舍入策略销毁返还时可能略少于投入这正是储备只多不少在组合层面的体现。1.5 模块级假设储备比率固定模块末尾通过spec module对全局状态施加约束spec module { // We assume that the backing ratio is fixed at 1:3, and never changes. invariant existsCoin1Info(ADMIN) globalCoin1Info(ADMIN).reserve_coin2.backing_ratio fixed_point32::spec_create_from_rational(1, 5); }它声明只要Coin1Info存在其backing_ratio就恒等于1/5spec_create_from_rational(1, 5)是 fixed_point32.move 提供的规范构造函数。这既是对当前合约比率一经设定不可改变这一设计约束的形式化表达注释中写的是 1:3实际取值为 1/5以代码为准也为后续所有验证提供前提假设。二、uniswap.moveUniswap v1 风格自动做市商2.1 池结构与恒定乘积不变量uniswap模块sources/uniswap.move实现了一个双币种流动性池支持币币兑换与添加/移除流动性。池状态同样是一个单一资源struct Pool has key { coin1: u64, coin2: u64, total_share: u64 }池子最重要的安全属性是恒定乘积不变量constant product invariant兑换前后两种币的余额乘积不减non-decreasing。这一属性以相同的形式附加在多个兑换函数上例如spec coin1_to_coin2_swap_code { let old_pool globalPool(PoolAddr); let post new_pool globalPool(PoolAddr); ensures old_pool.coin1 * old_pool.coin2 new_pool.coin1 * new_pool.coin2; // safety property }这里的let post new_pool是 MSL 在 spec 块中引入执行后状态的局部绑定语法配合old_pool一起把乘积不减这一数学不变量直接写成可验证的断言。乘积不变量正是 Uniswap 协议防套利、保证流动性提供者不因单笔兑换而亏损的核心机制。2.2 三种兑换实现同一规范三种命运模块提供了三个语义上等价的兑换函数但安全性截然不同这是本示例最具教学价值的部分① 官方代码实现coin1_to_coin2_swap_code基于 Uniswap v1 代码库公式public fun coin1_to_coin2_swap_code(coin1_in: u64): u64 acquires Pool { let pool borrow_global_mutPool(PoolAddr); let coin2_out getInputPrice(coin1_in, pool.coin1, pool.coin2); pool.coin1 pool.coin1 coin1_in; pool.coin2 pool.coin2 - coin2_out; coin2_out } fun getInputPrice(input_amount: u64, input_reserve: u64, output_reserve: u64): u64 { let input_amount_with_fee input_amount * 997; let numerator input_amount_with_fee * output_reserve; let denominator (input_reserve * 1000) input_amount_with_fee; numerator / denominator }定价公式input * 997 * output_reserve / (input_reserve * 1000 input * 997)内置了0.3% 手续费997/1000这是 Uniswap 的实际取费机制。由于coin1_out总是严格小于无手续费理论值乘积不减不变量必然成立。② 简化实现coin1_to_coin2_swap_code_simple把公式内联展开为一行(997 * coin1_in * pool.coin2) / (1000 * pool.coin1 997 * coin1_in)与官方实现数学上等价同样附加了完全相同的乘积不减 spec。③ 白皮书缺陷实现coin1_to_coin2_swap_whitepaper基于 Uniswap v1 白皮书中的公式public fun coin1_to_coin2_swap_whitepaper(coin1_in: u64): u64 acquires Pool { assert! (coin1_in 0, 1); let fee coin1_in * 3 / 1000; // 0.3% let pool borrow_global_mutPool(PoolAddr); spec { assume pool.coin1 0; assume pool.coin2 0; }; let inv pool.coin1 * pool.coin2; // inv may need to be u128 let new_pool_coin1 pool.coin1 coin1_in; let new_pool_coin2 inv / (new_pool_coin1 - fee); // No div-by-zero because (new_pool_coin1 - fee) cannot be 0. let coin2_out pool.coin2 - new_pool_coin2; pool.coin1 new_pool_coin1; pool.coin2 new_pool_coin2; coin2_out }白皮书版本的缺陷在于它先单独计算手续费fee coin1_in * 3 / 1000再从分母中扣除这种取整方式引入了无界的舍入误差unbounded rounding error在极端余额组合下可能让用户兑换出比无手续费情形更多的币从而破坏old_pool.coin1 * old_pool.coin2 new_pool.coin1 * new_pool.coin2这一不变量。源码注释明确警告This version of the swapping function is not safe because it does not satisfy the safety property, having an unbounded rounding error.尽管该函数自己也写了相同的乘积不减 spec第 66-72 行但 Prover 会在该函数上报告反例指出存在使不变量失效的具体余额与输入组合——这就是用规范对照实现发现真实漏洞的完整示范。运行时assume pool.coin1 0; assume pool.coin2 0;则把验证限定在非空池场景避免除零等平凡反例干扰核心结论。2.3 添加与移除流动性add_liquidity要求调用者按当前池内币种比例成对存入返回新增的流动性份额public fun add_liquidity(coin1_in: u64, coin2_in: u64): u64 // returns liquidity share acquires Pool { let pool borrow_global_mutPool(PoolAddr); spec { assume pool.coin1 0; assume pool.coin2 0; }; let coin1_added coin1_in; let share_minted (coin1_added * pool.total_share) / pool.coin1; let coin2_added (share_minted * pool.coin2) / pool.total_share; assert!(coin2_in coin2_added, 1); pool.coin1 pool.coin1 coin1_added; pool.coin2 pool.coin2 coin2_added; pool.total_share pool.total_share share_minted; share_minted }实现通过按比例分配保证新份额不稀释原有流动性提供者的权益并要求coin2_in与按比例算出的coin2_added完全一致assert!(coin2_in coin2_added, 1)否则拒绝交易。其 spec 用三个ensures声明池子各字段只增不减spec add_liquidity { ensures old_pool.coin1 new_pool.coin1; ensures old_pool.coin2 new_pool.coin2; ensures old_pool.total_share new_pool.total_share; }remove_liquidity是对称操作按份额占比返还两种币并销毁份额public fun remove_liquidity(share: u64): (u64, u64) // returns (coin1, coin2) acquires Pool { let pool borrow_global_mutPool(PoolAddr); assert!(share pool.total_share, 1); let coin1_removed (pool.coin1 * share) / pool.total_share; let coin2_removed (pool.coin2 * share) / pool.total_share; pool.coin1 pool.coin1 - coin1_removed; pool.coin2 pool.coin2 - coin2_removed; pool.total_share pool.total_share - share; (coin1_removed, coin2_removed) }对应 spec 声明各字段只减不增保证移除流动性不会凭空产生币。2.4 无免费午餐定理No Free Money Theorem模块以#[verify_only]函数形式给出了 AMM 领域最著名的组合性质验证#[verify_only] // The No Free Money Theorem states that if you add liquidity to a pool, then remove liquidity from the pool, // you will not end up with more money than you started with. fun no_free_money_theorem(coin1_in: u64, coin2_in: u64): (u64, u64) acquires Pool { let share add_liquidity(coin1_in, coin2_in); remove_liquidity(share) } spec no_free_money_theorem { ensures result_1 coin1_in; ensures result_2 coin2_in; }无免费午餐定理声明先按比例添加流动性、再全额移除刚获得的份额最终拿回的两种币都不会超过最初投入的量result_1 coin1_in且result_2 coin2_in。由于份额计算与移除均存在向下取整这一性质并不平凡——它证明取整损耗只会让用户少拿绝不会多拿从而排除了针对 AMM 的存-取套利攻击面。三、从示例看 Move Prover 的验证方法论把两个示例放在一起可以提炼出一套可复用的 Move Prover 实战方法论3.1 三层验证结构数据不变量data invariant在struct的spec块中声明全局状态必须始终满足的性质如 reserve 的全额储备Coin1Info的 invariant。Prover 会在所有修改该状态的函数中自动检查该不变量是否被保持——这是覆盖面最广、最省力的验证层。函数契约function contract为每个函数用aborts_if/ensures声明终止条件与状态前后关系。aborts_if同时充当完备性声明——凡实现中可能 abort 的路径必须在规范中列出否则验证失败这能强迫开发者想清楚所有失败分支。组合性质composite property用#[verify_only]函数串联多个操作验证跨函数的安全性质如mint_and_burn与no_free_money_theorem。这是单函数正确推不出组合行为安全时的关键补充。3.2 规范函数与舍入误差的处理定点运算的取整误差是金融类合约验证的经典难点。fixed_point32模块提供了规范抽象实现中用fixed_point32::multiply_u64真实定点运算规范中用fixed_point32::spec_multiply_u64数学意义上的精确乘法见 fixed_point32.move。两者语义通过 spec 声明绑定ensures result spec_multiply_u64(val, multiplier); // 实现函数与规范函数的一致性这种实现用真实运算、规范用理想运算的分离让 Prover 既能验证不变量如spec_multiply_u64(...) backing_value又不会因取整误差产生误报。当舍入方向本身影响安全性时如mint_coin1的1、白皮书版本的舍入缺陷则直接在实现层面显式建模让 Prover 去证明取整策略是否破坏属性。3.3 错误教学法错例驱动reserve.move与uniswap.move共有的教学特色是正确实现与故意错误的实现并存。正确版本用于展示通过验证的写法错误版本用于展示Prover 如何精确指出哪里错了、错到什么程度。建议的学习路径先阅读正确函数及其 spec理解每条规范语句的意图对错误函数运行move prover观察反例counterexample中给出的具体输入与状态对比正确/错误实现逐行差异理解舍入、边界条件如何悄然破坏不变量尝试删除某条ensures或invariant观察 Prover 是否报出更多漏洞体会规范的完备性价值。3.4 验证运行方式该包是标准的 Move 包Move.toml声明了包名DeFi与本地MoveStdlib依赖在已构建 Move Prover 工具链的环境下可于third_party/move/move-examples/experimental/defi目录中运行move prove # 验证包内所有模块的规范 # 或针对单文件 move prove --path sources/reserve.moveProver 会逐条检查本篇文章所介绍的全部invariant、aborts_if、ensures对mint_coin1_incorrect、burn_coin1_incorrect、coin1_to_coin2_swap_whitepaper报告反例而对其余函数确认通过。本包在仓库中的定位是教学与实验位于experimental目录未被打包进 aptos-core 的正式发布流程因此其规范语句如assume的使用、MAX_U64的显式溢出声明带有明显的示例教学痕迹生产合约应依据实际资金安全模型在此基础上强化。结语defi示例包以极小的代码量完整示范了 Move Prover 在 DeFi 场景中的三种典型验证目标储备充足性reserve 的全额储备不变量、定价正确性uniswap 的恒定乘积不变量、组合安全性无免费午餐定理。更重要的是它通过成对出现的正确与错误实现直观展示了形式化验证的检出能力与局限——规范写得好漏洞就无处遁形规范有遗漏Prover 也会同步失明。对于想要学习智能合约形式化验证或希望在 Aptos/Move 上构建安全 DeFi 协议的开发者这份示例是兼具理论深度与实战参考价值的起点。【免费下载链接】aptos-coreAptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.项目地址: https://gitcode.com/GitHub_Trending/ap/aptos-core创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考