Aptos Leaner 验证器测试组织与 Check 账本61 个验收夹具的通过率、失败分类与驱动约定【免费下载链接】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/lean子项目的验收测试组织文档展开系统解读 LeanerMove 智能合约的 Lean 形式化验证器当前 denotation 路线的 Check 验收套件账本61 个夹具中哪些精确通过、哪些失败、为何失败以及 Check 驱动的运行方式、基线与更新约定。读完本文你将掌握LEANER_E2E_SUITEcheck lake test的完整使用流程、UB1基线再生成机制、#leaner_require_native等注解的语义并能通过逐文件状态表定位验证器尚未覆盖的语言构造。一、背景denotation 路线与 Check 账本的角色test-organization.md 是denotation 路线denotation route的验收账本ledger记录 leaner-e2e-tests/LeanerE2ETests/Check/ 下全部接受性夹具的状态哪些精确通过pass exactly、哪些未通过、未通过的具体原因是什么。文档更新于2026-09-08是 denotation 路线的检查点快照路线设计见 denotation.mdV5一个 denotation、一个一致性证明。原始 v0 用例的时间线与映射关系归档在 test-organization-history.md不在本账本内重复。denotation 路线的核心思想是为 LeanerIR 定义一套语义模型denotation并证明编译compileFunction与求值的一致性compileFunction_agrees最终把每个verify目标发布为 Lean 内核可检查的定理。该路线当前已实现但挂起——一致性定理按用户决策被assumed作为公理直到其归纳证明完成。这一背景决定了账本中大量失败的根因凡是 denotation 尚未承载的构造验证器就报不承载而非给出错误的诊断差异。二、总体结果35 of 61 精确通过26 失败账本给出的总账是61 个 Check 文件中35 个精确通过pass exactly26 个失败。每一次失败都是 denotation 尚未承载的构造或者仍断言已退役路线名称的夹具没有任何一次是诊断diagnostics不匹配。判定标准非常严格一个文件只有在其全部输出与相邻的.exp基线完全一致在驱动的上限内即每个目标180k 验证心跳 verification heartbeats时才算通过一个文件只要有一个目标失败就整体失败无论它证明了其他多少目标没有.exp文件即意味着预期输出为空一个干净的验证文件就是没有基线文件的。三、五道 Gate 的当前状态账本把 CI/本地构建与测试门禁分为以下五道并逐项记录状态Gate结果说明leaner-ir构建PASSLeanerLang与Denote模块。DenotePerformance门禁PASS循环目标在基线 6% 以内没有任何目标突破其预算。leaner-irlake testFAIL215 个根中 38 个35 个LeanerLang.Tests.Native*根与Performance断言的是已退役路线的产物其移除属 D4Frontend需要向量replaceCompositionPerformance是资源组合残余。每个LeanerIR.Tests.*根均通过。leaner-move、leaner-rust构建PASSleaner-e2e-testslake buildFAIL无关原因mono-move-lean-linkRust crate 编译失败E0061账本按文件用lake env lean在驱动上限下采集。值得注意的两点DenotePerformance门禁是性能回归保护denotation.md 中记录该测试会输出每个目标的心跳数与证明对象规模直线代码约 1.7–6M 心跳、循环约 20M、带匹配契约的三变体match约 35M而 e2e Check 驱动把每个验证目标限制在180k 心跳——两套上限的用途不同门禁衡量证明规模Check 驱动保证验收可在合理时间窗内完成。leaner-e2e-tests的构建失败与验证器本身无关是mono-move-lean-link适配器 crate 的 E0061 编译错误因此账本改用单文件方式采集不阻塞验收记录。四、按规模排序的失败类别26 个失败按缺失能力归为七类类别文件数缺失内容向量Vectors11向量类型、元素借用与向量原语未被承载。泛型Generics4泛型局部变量、调用、构造函数与字段未被承载。资源不变量与顺序资源效应5GlobalInv、CrossInv、LooseFrame、ResourceComposition与Language/Loopsdrain留下残余义务residual obligation。递归与未指定被调函数2被调函数先于调用者被验证递归与用作摘要的纯辅助函数未被承载。返回引用与游离引用2绑定或调用参数之外的裸可变借用以及返回引用。已退役路线断言2Verification/Typed与Verification/EnumRefs断言已退役路线的产物。Rust profile1Rust profile 的原语尚无 denotation。这七类与 denotation.md 的 Not carried 清单完全对应|、^、有符号按位运算、向量类型未被承载行的来源、泛型调用/构造函数/字段、递归被调函数先于调用者验证drain、recursive_choose即此例等。换言之账本的每一行失败都可以直接映射到 denotation 路线的下一步实现清单这正是该账本作为路线图驱动的价值所在。五、逐文件状态完整验收账本每个名字对应Check/下的一个.lean文件。PASS 意味着整个夹具与其基线匹配无verify目标的 PASS 仅覆盖执行或诊断文档中已注明。以下三个表格完整继承原文档是 Check 套件的权威体检表。5.1 Language19 个文件13 通过6 失败文件状态遗留问题Language/AbilitiesPASS无验证目标。Language/AddressesPASSLanguage/ArithmeticPASSLanguage/AttributesPASS无验证目标。Language/ControlFormsFAILindex_arithmetic含有向量局部变量。Language/EmptyModulePASS无验证目标。Language/EnumPatternsPASS嵌套枚举以七个目标的代价验证通过。Language/EnumPayloadsFAIL向量局部变量与向量被调函数参数。Language/EnumRefsPASS仅执行无verify。Language/EnumsPASSLanguage/GenericsFAIL每个目标都有泛型局部变量。Language/IntegersPASSLanguage/LiteralsFAILclassify_bytes含有向量局部变量。Language/LoopsFAILdrain在活跃全局借用上循环残余义务。Language/PositionalStructsPASSLanguage/SignedPASSLanguage/TuplesPASSLanguage/VectorOperationsPASSLanguage/VectorsFAIL向量结果、局部变量与length原语。5.2 Verification30 个文件13 通过17 失败文件状态遗留问题Verification/AbortsPASS包含预期的错误契约拒绝。Verification/AccountPASSVerification/BorrowCertificatesPASS证书断言无verify。Verification/CalleesFAIL未指定的纯被调函数plus_one、pure_predicate与递归drain。Verification/CallsFAILrecursive_choose是递归的。Verification/CompositionPASSVerification/CorePrimitivesFAILvector_get、vector_set。Verification/CorpusPASSVerification/CrossInvFAIL跨资源不变量留下残余义务。Verification/EnumRefsFAIL夹具用已退役路线的匿名构造器构建枚举孪生。Verification/GenericsFAIL泛型局部变量与调用。Verification/GenericScalarCallsFAIL泛型调用。Verification/GenericStorageFAIL泛型字段没有承载泛型调用。Verification/GlobalBorrowsFAILbump_first、bump_left借用向量元素其余通过。Verification/GlobalInvFAIL资源不变量准备阶段在whnf处超时。Verification/IncrementPASSVerification/InvariantsPASSVerification/LoansFAILextend、independent_element、splice有向量局部变量。Verification/LoopInvariantsFAILclear在循环中修改向量count_to、sum_ones通过。Verification/LoopsPASSVerification/LooseFrameFAIL资源效应目标留下残余义务。Verification/NormalizedPASSVerification/PropheciesPASSVerification/ReadPASSVerification/ReferencesFAILreborrow在绑定或调用参数之外借用返回引用。Verification/ResourceCompositionFAIL顺序资源写入留下残余义务。Verification/RustFAILRust profile 的add没有 denotation。Verification/SpecLogicalArithmeticPASSVerification/StoragePASSVerification/TypedFAIL断言已退役路线的typedDenotation/Arguments名称。5.3 Negative 与支撑12 个文件9 通过3 失败关键规则正确的拒绝correct rejection并不能让一个文件通过——如果它的正向对照positive control失败的话。即负向夹具必须同时证明该拒的拒、该过的过。文件状态遗留问题Negative/BorrowGlobalsPASSNegative/BorrowsPASSNegative/IntrinsicUnsupportedPASSNegative/LoopInvariantsPASS基线在入口与迭代处命名了未建立的不变量。Negative/LoweringFAIL正向对照receiver_get、two_reads、receiver_insert有向量局部变量。Negative/ReturnedMutRefsFAIL由参数派生的返回引用留下残余义务。Negative/SpecificationsPASSNegative/SurfacePASSNegative/VerificationPASSNegative/WrongIncrementPASSPreparationRetryPASSVectorBoundsFAIL每个目标都有向量局部变量。5.4 缺失的 v0 夹具尚未移植账本同时登记了尚未从 v0 移植的夹具与剩余工作量v0 文件剩余工作Verification/OrderedMap.lean九个 proof-carrying 目标及其依赖。Verification/Quicksort.lean三个 proof-carrying 目标及其依赖。Verification/ReturnedMutRefs.lean66 个目标的语料库手工References夹具不能替代它。Verification/SpecFunctions.lean十二个目标。Verification/Summaries.lean三个目标。Negative/SpecFunctions.lean诊断用例。Language/BorrowChecker.lean借用检查器用例。六、Check 套件工作原理驱动、基线与运行方式6.1 驱动模型根据 leaner-e2e-tests/README.md 与账本约定Check 套件的工作方式为一个 Check 文件就是LeanerLang 源码模块 契约 verify命令 真正的数学所在的证明脚本驱动自动发现Check/**/*.lean下的每一个.lean文件任意深度在各自的 Lean 进程中、在驱动上限每目标 180k 心跳下elaborate驱动把lean打印的全部输出逐字与相邻的name.exp基线比较无.exp文件即表示预期输出为空约定与 compiler-v2 的基线惯例一致干净检查无期望文件打印任何内容的检查恰好以该输出为期望UB1会写入或删除文件正负测试是同一类文件全部位于Check/下前端路径Move/Rust 翻译保留在自己的目录。6.2 运行与更新命令从leaner-e2e-tests目录运行LEANER_E2E_SUITEcheck lake test # 以 check 套件运行验收 UB1 lake test # 重新生成基线UB1 等价于 UPBL / UPDATE_BASELINELEANER_E2E_SUITE环境变量选择套件move、rust、check、monovm或monodiff。UB1重新生成基线后每个重新生成的 diff 都必须人工审查——基线是意图行为的记录不能被当作自动批准的通行证。6.3 基线与晋升规则原文档的硬性约定账本末尾的 Conventions 是 Check 套件的宪法必须逐条遵守基线记录的是预期行为负向用例的期望诊断必须点名所测构造或子句一个不支持的正向证明永远不会被记录为预期失败防止把能力缺失伪装成验收通过。文件只能由驱动在未变更的上限下晋升通过中的 pilot 不晋升任何文件不得为了把一个移植计为完成而抬高上限。成功验证的verify会自动通过native audit部分移植用#leaner_require_native完成移植的夹具用#leaner_require_native_all。断言风格的 IR、Move、Rust 测试留在各自所属的包中已废弃的包仅作参考材料不再运行。源码验证不是所生成字节码的编译器正确性定理——账本不承诺编译后字节码的等价性。每批工作结束后就地更新日期、计数、受影响的行与 Gate 表提交commit单独记录一次 commit 不改变任何状态。七、Check 夹具解剖以真实文件为样本以下从仓库中选取四个代表性夹具说明通过/失败在源码层面到底是什么形态。7.1 最简干净用例Increment.leanVerification/Increment.lean 是契约被实现证明的最简形态整个文件即为账本中Verification/Increment | PASS的源码leaner module 0x42::increment where public fun increment(value : u64) - u64 : value 1 spec increment where ensures result value 1 aborts_if value 1 18446744073709551615 verify increment注意其头注释the check is clean and has no expectation file——目录清单中Increment.lean确实没有对应的.exp这正是干净检查无期望文件约定的直接体现。7.2 综合夹具ControlForms.lean 的完整解剖Language/ControlForms.lean 是账本中标记FAILindex_arithmetic有向量局部变量的文件但它展示了 Check 夹具的完整构成路由选择set_option leaner.route native指定 native 路线LeanerLang 模块leaner module 0x42::control_forms where ...内含struct、fun、spec ... where、verify声明顶层验证指令#leaner_verify 0x42::control_forms::branch_effect与#leaner_require_native ...组合出现——前者把目标发布为验证任务后者要求 native audit 通过require语义即此目标必须真正被原生证明不许用sorry带过证明卫生检查文件末尾用run_cmd遍历所有函数名确认verified定理存在于环境中并调用collectAxioms断言其中不含sorryAx不允许 admission规范不动点检查LeanerLang.Print.render输出再formatSource后必须与自身相等保证源码是规范形式的不动点canonical fixed point防止打印器漂移执行断言assertRuns携带大量输入/输出对例如branch_effect在u64::MAX上执行应得到.threw .abort #[.integer 18446744073709551616]——算术失败保留 VM 计算出的真实载荷这是与 v0 固定零载荷行为的关键差异checked_assert_eq/checked_assert_ne验证断言码 19/20 的中止行为。该文件正是账本中index_arithmetic失败的出处其fun index_arithmetic(base : u64) - u64 : do let values : vectoru64[10, 20, 30] ...含向量局部变量与values[base 1]元素借用而向量未被 denotation 承载因此它只能以#leaner_require_native做部分覆盖。7.3 负向夹具拒绝必须点名来源子句Negative/Verification.lean 与其基线 Negative/Verification.exp 展示了正确拒绝的形态。夹具中的wrong_increment与wrong_action契约刻意写错其.exp基线精确记录了诊断LeanerE2ETests/Check/Negative/Verification.lean:12:4: error: the specification clause ensures result value is not established LeanerE2ETests/Check/Negative/Verification.lean:19:9: error: leaner verification failed关键点诊断发生在源契约子句处12:4 是ensures子句本身并且文件末尾的run_cmd显式断言环境中不存在wrong_increment.verified这样的定理——错误契约绝不能导出证明定理。同理可参考 Negative/LoopInvariants.exp它在入口与迭代处分别给出a loop invariant at entry is not established与a loop invariant at an iteration is not established——这正是账本中该文件 PASS 并注明基线命名了入口处与迭代处未建立的不变量的依据。7.4 资源不变量GlobalInv.leanVerification/GlobalInv.lean 是账本中FAIL准备阶段在whnf处超时的文件但它完整演示了 LeanerLang 的资源验证面spec module where声明模块级全局不变量包括[update]标记的不变量old ≤ new 的单调性存储内建move_toCounter、move_fromCounter、existsCounter、mut Counter[addr].value全局可变借用头部使用set_option leaner.verifyHeartbeats 50000——注意这是单文件提高上限的做法而账本约定不得为计数移植而抬高驱动上限两者界限分明驱动上限 180k 是验收基准文件内选项只影响单个夹具的 elaborate 预算而该文件恰恰是在准备阶段whnf归一化不变量耗尽了预算。7.5 执行断言的支撑层CheckSupport.leanCheckSupport.lean 是执行断言的公共支撑RunCase/StateRunCase结构体定义输入输出对后者还固定最终全局/借用状态assertRuns/assertRunsState通过LeanerIR.Interpreter.Interpreter.run以256 燃料解释执行并把结果与期望值比对。头注释强调这些是执行检查与单独生成的契约证明相互独立——这正是账本中无验证目标但 PASS纯执行覆盖类夹具的运行底座。八、从账本看 denotation 路线的下一步账本的 26 个失败与 7 个缺失 v0 夹具本质上是一张按优先级排序的实现路线图**向量11 个文件**是最大缺口向量类型、元素借用、length/get/set原语、循环内向量变更LoopInvariants/clear、Loops/drain全部依赖它泛型4 个文件泛型局部变量、调用、构造函数与字段GenericStorage的泛型字段紧随其后**资源不变量与顺序资源效应5 个文件**涉及 denotation 的 wpweakest precondition规则对全局状态的表达能力GlobalInv的whnf超时说明不变量归一化的性能也需优化**递归与未指定被调函数2 个文件**要求把被调函数先于调用者验证的策略扩展为支持递归与纯函数摘要引用边界2 个文件绑定/调用参数之外的裸借用与返回引用的承载清理项3 个文件Verification/Typed、Verification/EnumRefs中已退役路线的断言产物其移除属 D4以及 Rust profile 原语的 denotation。对照 denotation.md 的 Carried 清单标量与受检算术、比较、布尔运算、无符号、受检移位与转换、常量、if/let/块、abort/assert、提前return、赋值、break/continue、带invariant的循环、单态直接调用、元组、结构体、枚举、局部变量共享借用、NTy.ref可变引用、基于运行时键控全局图的存储原语可以清晰看到账本每一行失败都落在 Not carried 与 Carried 的交界线上。因此本文所述的账本不仅是一份测试报告更是 Leaner 验证器后续开发的验收门与进度条——任何新承载的构造都以Check 账本中的 FAIL 行翻转为 PASS作为唯一可信的完成证据。对读者而言若要复现或扩展这套验收在leaner-e2e-tests目录执行LEANER_E2E_SUITEcheck lake test即可逐文件验证本账本新增一个.lean夹具无需注册驱动自动发现用UB1可再生成基线但必须人工审查 diff——这套自动发现 逐字基线 人工审查晋升的组织方式本身就是一个值得借鉴的验证器验收工程范式。【免费下载链接】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），仅供参考