# 从 Rocq 定理证明器提取经过数学证明的 C++ 代码 > 解析 Bloomberg 的 Crane 提取系统如何将经过形式化验证的 Rocq 程序转换为符合生产标准的 C++ 代码，涉及类型映射、函数式惯用法转换与软件事务内存等核心技术。 ## 元数据 - 路径: /posts/2026/01/24/extracting-verified-cpp-from-rocq/ - 发布时间: 2026-01-24T20:02:40+08:00 - 分类: [compilers](/categories/compilers/) - 站点: https://blog.hotdry.top ## 正文 在金融系统与高频交易领域，软件正确性的代价往往以毫秒计算。一次整数溢出可能导致灾难性的计算错误，一次竞态条件可能引发难以复现的数据损坏。传统的单元测试只能验证有限输入集上的行为，而无法排除所有可能的执行路径。Bloomberg 在其基础设施与安全研究团队中，选择使用 Rocq 定理证明器编写带有数学正确性证明的认证程序。然而，证明语言与生产语言之间的鸿沟始终存在：如何在不牺牲验证保证的前提下，将这些经过严格证明的程序投入实际生产？ 现有的 Rocq 提取方案主要面向 OCaml、Haskell 等函数式语言，或 C、Rust 等系统编程语言。OCaml 和 Haskell 的提取路径成熟，但与 Bloomberg 现有的 C++ 代码库存在互操作障碍；C 和 Rust 的提取虽然更接近底层，但缺乏对 Bloomberg 自研核心库的原生支持，且生成的代码风格与团队习惯的编码规范不符。正是在这一背景下，Bloomberg 开发了 Crane——一套专门针对其生产级 C++ 代码库定制的提取系统。Crane 的目标不仅是语法层面的转换，而是在保持函数式语义的同时，生成符合 Bloomberg 编码规范、能够无缝集成到既有 C++ 代码库中的可读、可维护、高性能代码。 ## 类型映射与数据结构的语义等价转换 Rocq 中的数据结构基于归纳类型（Inductive Types）构建，其核心是构造子（Constructors）和模式匹配（Pattern Matching）机制。以自然数类型为例，Rocq 使用 `O` 表示零、`S n` 表示后继，这种 Peano 表示法在数学上优雅，但在传统 C++ 中并无直接对应。Crane 的类型映射策略并非简单地用 `enum` 或整数替代，而是将归纳类型映射为具有编译期类型安全的类层次结构。`nat` 类型被转换为一个抽象基类及其具体实现类，构造子对应不同的派生类，模式匹配则通过虚函数分派实现动态绑定。这种映射方式虽然引入了一定的运行时多态开销，但保留了 Rocq 程序的递归结构，使得证明中的归纳论证在生成的 C++ 代码中仍然可追溯。 列表类型是另一个典型案例。Rocq 中的 `list A` 由 `nil`（空列表）和 `cons a l`（头元素与尾列表）构造，标准提取方案通常将其映射为 C++ 标准库的 `std::vector` 或 `std::list`。然而，Bloomberg 的需求更为精细：他们需要生成的代码能够使用公司内部的核心库类型，以方便与既有系统集成。Crane 提供了两层映射机制，第一层允许将 Rocq 的 `list` 映射到 `std::vector` 或 `std::list`，第二层则支持映射到 Bloomberg 自研的序列容器。更重要的是，这种映射是可配置且可组合的——开发者可以为不同的模块指定不同的映射策略，而无需修改证明本身的结构。这一设计体现了 Crane 的核心哲学：提取系统应当适应代码库，而非强迫代码库适应提取系统。 整数类型的映射揭示了形式化验证与工程实践之间的深层张力。Rocq 的 `nat` 类型在理论上可以表示任意大的自然数，而 C++ 的 `int` 是有界的。文档中明确指出，当程序可能处理超过最大整数范围的数时，开发者需要显式地将 `nat` 映射为大整数类型（如 `boost::multiprecision::cpp_int`），或在证明阶段就引入边界约束。Rocq 的提取框架本身并不自动处理这种转换，因为边界检查的引入会改变程序的渐近复杂度，而证明中可能并未考虑这些边界情况。Crane 将这一决策权交给开发者，同时提供静态分析工具以识别可能产生溢出的代码路径，在编译期给出警告或建议。 ## 函数式惯用法向 C++ 的语义-preserving 转换 Rocq 的函数定义依赖于模式匹配和高阶函数，这两者在命令式的 C++ 中需要不同的表达方式。以列表上的 `map` 函数为例，其 Rocq 定义遍历列表，对每个元素应用给定函数并收集结果。在传统 C++ 中，这一模式可以通过模板和 `std::transform` 实现，但 Rocq 的 `map` 不仅仅是一个算法——它是依赖于类型构造子的多态函数，其行为由归纳类型的结构保证。Crane 的转换策略是将 `map` 展开为递归函数，尾递归优化的部分被转换为循环，而非尾递归部分则保持递归结构。生成的 C++ 代码保留了原始证明中的递归结构，这使得代码审查者可以相对容易地验证生成的实现与原始证明的一致性。 高阶函数的处理更为复杂。Rocq 允许将函数作为参数传递和返回，这种能力在 C++ 中通过函数指针、`std::function` 或模板实现。Crane 优先使用模板，因为模板在编译期展开，避免了 `std::function` 的类型擦除开销，同时保持了完整的类型信息。当高阶函数需要跨模块边界传递时（例如从提取的模块传递到未提取的 C++ 代码），Crane 会生成相应的函数对象包装器，这些包装器负责捕获上下文并正确转发调用。这一设计确保了提取的代码可以与 Bloomberg 代码库中的既有组件无缝协作，而无需修改这些组件的接口。 证明中常见的依赖类型和等式证明在提取时需要特殊处理。Rocq 的依赖类型允许定义值级别的约束（如「这个向量的长度等于那个列表的长度」），这些约束在证明完成后通常可以被擦除，因为运行时不再需要它们。Crane 的提取策略正是基于这一观察：所有 `Prop` 类型的证明项在提取过程中被完全移除，只保留计算相关的项。然而，等式约束有时会在类型层面残留，例如当函数的返回值类型依赖于输入值的某个属性时。这些残留的类型信息被转换为 C++ 的静态断言（`static_assert`），在编译期验证不变量的成立。这种设计将证明的静态保证部分地转化为编译期的静态检查，而运行时则只保留纯粹的计算逻辑。 ## 软件事务内存：并发安全的函数式抽象 金融系统几乎总是并发的——多个处理器核同时处理市场数据流，不同模块的状态需要同步更新，锁的粒度和顺序直接影响系统的吞吐量和延迟。传统的并发编程依赖于锁（Mutex）或原子操作，但这两者都容易引入死锁、活锁或数据竞争等问题。Rocq 的并发原语允许开发者在证明阶段就验证并发程序的正确性，而 Crane 则将这些验证过的原语转换为 C++ 中的软件事务内存（Software Transactional Memory，STM）实现。 STM 的核心思想是将一段代码块视为一个事务：要么完整执行并提交所有修改，要么在发生冲突时回滚并重试。这一模型与数据库事务类似，但应用于内存操作。在 Rocq 中，开发者可以使用高级的并发原语描述并发行为，而无需关心底层的锁或原子操作细节。Crane 的转换层将这些原语映射到 C++ 的 STM 库实现，该实现使用日志记录事务中的读操作和写操作，在提交时检测冲突并决定提交或回滚。关键在于，由于 Rocq 中的并发程序已经通过了正确性证明，生成的 STM 代码只需要确保「执行的原子性」，而无需重新验证业务逻辑的正确性。 这一设计的工程价值在于分离关注点。形式化验证专家可以继续在 Rocq 中工作，使用熟悉的证明技术验证并发算法；C++ 工程师则可以继续使用熟悉的工具链和调试器，唯一的「额外负担」是理解 STM 的语义以及事务失败时的重试策略。更重要的是，STM 的使用使得生成的 C++ 代码天然具有可组合性——多个事务可以嵌套，而不会产生死锁（因为事务内部的锁获取被推迟到提交阶段统一处理）。这一特性对于模块化的大型系统尤为重要，因为它允许独立开发的不同组件安全地并发执行。 ## 代码可读性与生成代码的工程实践 形式化验证系统的一个常见批评是「验证过的代码不可读」——生成的代码往往充满临时变量、冗余的类型转换和难以理解的递归结构，难以进行人工审查和维护。Crane 在设计之初就将可读性作为核心目标之一。生成的 C++ 代码遵循 Bloomberg 的编码规范，包括命名约定、缩进风格和注释要求。变量名从 Rocq 的标识符直接映射而来，保留原始证明中的语义信息。函数和类的组织结构反映 Rocq 模块的层次结构，使得熟悉原始证明的开发者可以快速定位生成代码中的对应部分。 代码审查是 Bloomberg 开发流程中的关键环节，任何代码变更都必须经过同行评审。生成的代码同样需要接受审查，这意味着审查者需要能够理解和验证生成代码与原始证明的一致性。Crane 生成的代码不仅包含实现本身，还包含从 Rocq 证明结构到 C++ 代码结构的映射注释。这些注释引用原始证明中的关键定理和引理，帮助审查者理解某段代码为何以特定方式实现。当审查者对生成代码有疑问时，可以追溯到原始证明，找到相应的形式化论证。 测试策略也需要相应调整。传统 C++ 代码的测试侧重于行为验证，而经过 Rocq 验证的代码则需要在两个方面进行测试：第一，提取过程的正确性——确保生成的代码忠实地实现了原始证明中的计算逻辑；第二，与外部世界的接口正确性——确保生成的代码能够正确地与 C++ 环境交互，包括资源管理、异常处理和边界条件处理。Crane 提供了自动化测试生成工具，可以从 Rocq 的测试用例生成等价的 C++ 测试用例，同时生成接口层的桩代码（Stubs）和模拟对象（Mocks），以隔离测试范围并提高测试的可靠性。 ## 工程权衡与实践建议 从 HN 讨论中可以看到，社区对这一技术路线既兴奋又审慎。有评论者指出，生成的代码中存在大量 `std::shared_ptr` 包装器，这是为了保留 Rocq 的共享语义并避免悬垂指针，但这种设计可能引入额外的内存分配开销和引用计数维护开销。是否使用共享语义取决于具体的应用场景：对于性能关键的代码路径，开发者可能需要在证明阶段就选择不同的数据结构或映射策略，以生成更轻量的 C++ 实现。Crane 的设计允许这种定制化，但需要开发者在证明阶段就做出决策，而非在提取阶段优化。 另一项重要的权衡是整数类型的选择。Rocq 的 `nat` 类型在理论上无限，而 C++ 的 `int` 有界。如前所述，Crane 允许使用大整数类型，但这会带来性能损失。一种折中方案是在证明阶段引入「小于等于 `max_int`」的约束，然后在提取时使用普通的 `int`，同时在关键路径上插入断言验证这一约束始终成立。这种方法在大多数情况下能够获得接近原生 `int` 的性能，同时在极少数可能溢出的情况下提供安全网。然而，这种方法的前提是开发者能够在证明阶段就识别并约束这些边界情况，这需要 Rocq 证明技能的深入掌握。 对于考虑采用类似技术路线的团队，Bloomberg 的经验表明，成功的关键在于渐进式集成而非激进式替换。Crane 最初被用于验证系统中最关键、错误代价最高的组件，这些组件通常规模较小、逻辑复杂、难以通过传统测试覆盖。在验证这些组件并积累经验后，团队才逐步扩大验证范围。同时，提取系统的开发和改进是一个持续的过程：每次发现新的边缘情况或优化机会，都会被纳入工具链的改进中。这意味着采用类似技术的团队需要投入资源维护和改进提取工具本身，而不仅仅是使用它。 ## 未来方向与行业影响 Bloomberg 的实践代表了形式化验证领域的一个重要趋势：从纯学术研究走向工业应用。传统上，形式化验证被视为理论计算机科学的专属领域，其成果往往停留在论文和原型系统层面。然而，随着软件系统越来越复杂、错误的代价越来越高，工业界对形式化验证的需求日益增长。Crane 的成功表明，通过精心设计的提取系统，形式化验证的成果可以有效地转化为生产级代码，从而跨越「验证」与「部署」之间的鸿沟。 这一技术路线的潜在影响不仅限于金融行业。任何对软件正确性有高要求的领域——航空、医疗、核电、自动驾驶——都可以从类似的技术中受益。当然，形式化验证的门槛仍然较高，需要专门的培训和工具支持。但随着提取系统的成熟和文档的完善，这一门槛正在逐渐降低。可以预见，未来会出现更多面向特定领域或特定语言的提取系统，使形式化验证变得更加普及和实用。 Bloomberg 的 Crane 系统为行业提供了一个可参考的范式：如何将定理证明器的形式化能力与现代 C++ 的工程实践相结合，在保持正确性保证的同时实现代码的可读性、可维护性和高性能。这条路径虽然充满挑战，但其潜在回报——消除关键系统中的潜在错误——对于任何对软件质量有严格要求的组织而言都是值得追求的目标。 --- **参考资料** - Bloomberg Open Source: Crane Lowers Rocq Safely into C++ (https://bloomberg.github.io/crane/papers/crane-rocqpl26.pdf) - Rocq Prover Documentation: Program Extraction (https://rocq-prover.org/doc/master/refman/addendum/extraction.html) ## 同分类近期文章 ### [C# 15 联合类型：穷尽性模式匹配与密封层次设计](/posts/2026/04/08/csharp-15-union-types-exhaustive-pattern-matching/) - 日期: 2026-04-08T21:26:12+08:00 - 分类: [compilers](/categories/compilers/) - 摘要: 深入分析 C# 15 联合类型的语法设计、穷尽性匹配保证及其与密封类层次结构的工程权衡。 ### [LLVM JSIR 设计解析：面向 JavaScript 的高层 IR 与 SSA 构造策略](/posts/2026/04/08/jsir-javascript-high-level-ir/) - 日期: 2026-04-08T16:51:07+08:00 - 分类: [compilers](/categories/compilers/) - 摘要: 深度解析 LLVM JSIR 的设计动因、SSA 构造策略以及在 JavaScript 编译器工具链中的集成路径，为前端工具链开发者提供可落地的工程参数。 ### [JSIR：面向 JavaScript 的高级 IR 与碎片化解决之道](/posts/2026/04/08/jsir-high-level-javascript-ir/) - 日期: 2026-04-08T15:51:15+08:00 - 分类: [compilers](/categories/compilers/) - 摘要: 解析 LLVM 社区推进的 JSIR 如何通过 MLIR 实现无源码丢失的往返转换，并终结 JavaScript 工具链碎片化困境。 ### [JSIR：面向 JavaScript 的高层中间表示设计实践](/posts/2026/04/08/jsir-high-level-ir-for-javascript/) - 日期: 2026-04-08T10:49:18+08:00 - 分类: [compilers](/categories/compilers/) - 摘要: 深入解析 Google 推出的 JSIR 如何利用 MLIR 框架实现 JavaScript 源码的高保真往返，并探讨其在反编译与去混淆场景的工程实践。 ### [沙箱JIT编译执行安全：内存隔离机制与性能权衡实战](/posts/2026/04/07/sandboxed-jit-compiler-execution-safety/) - 日期: 2026-04-07T12:25:13+08:00 - 分类: [compilers](/categories/compilers/) - 摘要: 深入解析受控沙箱中JIT代码的内存安全隔离机制，提供工程化落地的参数配置清单与性能优化建议。