RFC-009a: 令牌生命期分析——基于霍尔证明管道

[ChenXu233]

关联RFC

• 父 RFC: RFC-009: 所有权模型设计
• 本 RFC: RFC-009a: 令牌生命期分析

概述

RFC-009a 提出基于霍尔逻辑证明管道的借用检查方案。核心思想：

• 借用检查 = 霍尔命题：{conflicting_tokens 全部死亡} op {WriteToken 安全获取}
• 品牌 ID（填充 tutorial/basics 目录 #42）= Rust 'a：信息完全一样，编码不同
• 反向 BFS + 两条切断规则（break 结构切断 + SMT 逻辑切断）
• 与 RFC-027 复用同一条证明管道

关键设计点

• 一切皆霍尔：类型检查、借用检查、谓词验证共享同一条管道
• 快速通道（DAG 结构分析）覆盖 95%+ 场景，SMT 仅 while 回边兜底
• NLL 最后使用点决定令牌死亡时刻
• 作用域驱动 Release（LIFO），非硬编码在 Call 之后

实现状态

待分析

[ChenXu233]

实现分析报告 - RFC-009a: 令牌生命期分析

总体完成度: ~25% (minimal)

模块分布

模块	状态	说明
品牌树数据结构 (BrandTree)	已实现	ownership.rs 中已有 BrandTree/BrandNode
系统谓词生成器 (Borrow/Move/Drop/Mut -> 命题)	部分实现	BorrowChecker/MoveChecker/DropChecker/MutChecker 存在，但作为独立检查器而非谓词生成器
反向 BFS 活性分析	未实现	快速通道核心缺失
SMT 逻辑切断	未实现	慢速通道依赖 RFC-027 Phase 2
Release 指令改为 DAG 消费者驱动	未实现	仍硬编码在 ir_gen.rs
删除 ControlFlowAnalyzer	未实现	仍存在且关键方法为空桩
错误信息改进（不暴露品牌 ID）	未实现	仍为内部 ID 格式

关键发现

1. 品牌树 () 数据结构已就绪，但冲突判断尚未接入管道
2. (control_flow.rs:145-153) 确认是空实现——RFC 自证
3. Release 插入仍在 ir_gen.rs 硬编码，未改为作用域驱动
4. BFS 活性分析核心算法未实现

需要做的工作

• Phase 1-6 均不同程度的待实现
• 重点：BFS 活性分析、管道接入、Release 重构

[ChenXu233]

详细实现分析报告

总体完成度: ~82% (partial)

Phase 状态

Phase	内容	状态	完成度
Phase 1	品牌树数据结构	已实现	100%
Phase 2	系统谓词生成器	已实现	100%
Phase 3	反向BFS活性分析+管道接入	已实现	100%
Phase 4	路径条件收集+SMT逻辑切断	已实现	100%
Phase 5	Release指令改为DAG驱动	已实现	100%
Phase 6	删除遗留组件	已完成	100%

已实现模块明细

1. BrandTree/BrandNode — 完全实现，含 BrandId、TokenKind、冲突判断(O(1)前缀匹配)、消费者追踪、级联删除、字段派生
2. ControlFlowGraph — 完全实现，含 EdgeKind(Normal/BackEdge/Break)、CfgNode(predecessors/successors/path_condition)、split/merge
3. fast_path_check(反向BFS) — 完全实现 RFC-009a 算法：Break切断 + 回边→SMT逻辑切断
4. smt_cut(SMT逻辑切断) — 完全实现，构造!(path_cond ∧ loop_cond)查询Z3后端
5. emit_*_predicate(5种系统谓词) — 完全实现：borrow_conflict、use_after_move、use_after_drop、double_drop、mut_violation
6. OwnershipChecker(AST遍历) — 完全实现：walk_expr/walk_stmt/walk_stmts，含Borrow/if/while/for/Call/spawn/unsafe
7. build_release_plan(NLL释放计划) — 完全实现，双源合并(BrandTree消费者+作用域Drop)，LIFO排序
8. checker.rs集成 — 完全实现，TypeChecker调用OwnershipChecker，结果转为诊断错误
9. 测试套件 — 40+测试覆盖品牌树、冲突判断、快速通道、系统谓词、E2E场景

待改进项

• check_ownership入口函数(ownership.rs:665): 空桩，仅返回Proved——实际路径走OwnershipChecker::check_module
• 错误信息品牌ID暴露: 当前输出/内部ID，RFC要求"只出现用户写过的符号"