在形式化验证领域，从定理证明器提取可部署代码一直是一个核心挑战。传统的提取方案往往生成难以维护的目标代码，或者与生产环境的代码库存在显著的集成障碍。BLOOMBERG 推出的 Crane 项目试图从根本上解决这一问题，它不仅是一个 Rocq 到 C++ 的提取器，更是一套完整的编译器工具链，旨在将经过形式化验证的 Rocq 组件无缝集成到生产级的 C++ 代码库中。
设计定位与目标环境
Crane 的设计出发点源于 Bloomberg 内部的技术现状：C++ 是其主导的实现语言，代码必须符合长期建立的编码标准，特别是 BDE 风格指南。在这一环境下，可读性和可维护性与原始性能同等重要。因此，Crane 的核心目标不是生成最小的目标代码，也不是与 Rocq 语法一一对应，而是生成 "工程师可以认出是自己可能写出的 C++ 代码" 的产物。这意味着开发者应该能够直接打开 Crane 生成的文件，使用与手写 C++ 相同的习惯进行推理：通过调试器单步执行、浏览检查不变量、在代码审查中审查差异。
从组织层面看，Crane 承载着 "让小型验证团队服务众多 C++ 开发者" 的愿景。少数 Rocq 专家可以构建和维护经过验证的库，而应用团队则将这些库作为 "普通"C++ 来消费。这种模式大大扩展了形式化验证的覆盖范围，避免了每个团队都需要具备深度验证能力的瓶颈。
核心设计原则
Crane 的设计遵循六项核心原则，这些原则共同塑造了其编译器工具链的技术路线。第一项原则强调可读性和惯用 C++ 优先，提取结果应使用熟悉的 C++ 构造，如智能指针、变体和 lambda 表达式，并与既有的编码规范对齐。这不是关于最小化内部表示尺寸或一一映射 Rocq 语法的问题，而是关于生成看起来 "像写得很好的 C++ 库" 的代码。
第二项原则处理功能结构与 C++ 表面的关系。Rocq 程序本质上是函数式的，Crane 保持这种结构的可见性，但用惯用的现代 C++ 呈现。代数数据类型变成类似 std::variant 的形式，模式匹配变成结构化的条件语句，高阶函数变成 lambda 和可调用对象，单子效果变成具有具体 C++ API 的库。这样做的目的是保留 Rocq 程序的 "概念形状"，使证明和实现仍然能够在人的头脑中 "对应起来"。
第三项原则将内存和线程安全作为默认选项。Crane 追求 "按构造安全" 的代码：使用智能指针和值类型而非原始的 new 和 delete，仔细控制共享和突变，并发构建在软件事务性内存（STM）风格的抽象之上，而非随意的锁机制。这种设计意图使得竞争条件和生命周期错误难以在生成的代码中表达，而不仅仅是难以测试。
值得注意的是第四项原则：务实的信任，而非完全验证的编译。Crane 故意不从 CompCert 风格的完全验证编译器管道出发。承认验证整个提取器将是一项大型的多年度工作，因此选择关注人们实际会使用的表达性代码生成，通过差分测试和静态分析来验证提取器本身。这是一种 "实用的保证加经过验证的源程序" 的策略，而非在提取器完全被证明之前延迟有用输出的产生。
提取机制与关键技术
Crane 的提取机制建立在高度可配置的类型映射系统之上。对于归纳类型，开发者可以使用 Crane Extract Inductive 命令定义 Rocq 类型如何映射到 C++ 类型。这个命令接受 Rocq 类型名称、C++ 类型表达式、构造函数映射和模式匹配语句四个参数。例如，将 Rocq 的 option 类型映射到 std::optional 的配置如下：C++ 类型表达式使用 %t0 作为类型参数占位符，构造函数分别映射为 std::make_optional 和 std::nullopt，模式匹配则编译为 C++ 的 if 语句和 has_value() 检查。
占位符系统是这一映射机制的核心。%t0、%t1 等表示归纳类型的类型参数，%a0、%a1 等表示构造函数参数，%scrut 表示被检查的模式匹配对象，%b0a0 表示绑定到第零个分支第零个参数的名称，%br0、%br1 则表示各个分支的代码。这种细粒度的控制使得开发者可以精确地指定每个 Rocq 结构如何转化为等价的 C++ 代码。
对于常量映射，Crane Extract Inlined Constant 命令允许将 Rocq 常量直接映射为字面的 C++ 表达式，而非函数调用。fst 和 snd 这样的投影函数可以简单地映射为 .first 和 .second 成员访问。这种内联能力对于生成高效的代码至关重要，因为它消除了不必要的函数调用开销。
单子接口的处理是 Crane 技术路线中的另一个关键点。通过 Crane Extract Monad 命令，开发者可以定义 Rocq 单子如何映射到 C++ 单子类型，并指定实现 bind 和 ret 的 Rocq 标识符。这使得单子记法和 do 记法能够被正确翻译，将函数式编程中的抽象概念转换为具体的 C++ API。这种机制在处理状态、IO 和软件事务性内存等效果时尤为重要。
配置化策略与可扩展性
Crane 的设计明确拒绝了硬编码映射的方案。不同项目有不同的 C++"世界观"：有些只使用 C++ 标准库，有些使用 Bloomberg 的核心库 BDE，有些可能有自己的基础库。因此，Crane 提供了宏语言用于自定义 Rocq 定义的提取方式，以及定义效果接口和单子 API 的机制。开发者可以将 Rocq 的 option 映射到 std::optional<T> 或映射到符合自己风格的 optional 类型，可以决定特定效果（如 IO、STM）如何在 C++ 中表示和排序。
标准库映射集的选择通过 Set Crane StdLib 命令控制。"std" 集合使用 C++ 标准库类型如 std::string 和 std::shared_ptr，而 "BDE" 集合则使用 Bloomberg 的 BDE 类型如 bsl::string 和 bsl::shared_ptr。这种分离确保了 Crane 能够适应不同组织的代码库风格，而不仅仅是为 Bloomberg 内部需求服务。
提取过程本身通过 Crane Extraction 命令触发。指定输出路径和 Rocq 定义名称后，Crane 会生成相应的头文件和实现文件。值得注意的是，虽然 Crane 诞生于 Bloomberg 的需求，但它被明确设计为通用工具，不锁定在 Bloomberg 生态中。Bloomberg 特定的集成（如 BDE）是可选模块，核心提取针对 "普通" 现代 C++，宏和效果机制是开放的。
工程实践中的考量
将 Crane 集成到实际工程工作流中需要考虑几个实际因素。首先，当前 Crane 处于 alpha 版本阶段，在生产环境中使用需要谨慎评估和充分的测试覆盖。验证责任仍然在 Rocq 源程序一侧，Crane 的职责是将这些经过验证的程序忠实地翻译为 C++，而不是重新验证它们。
差分测试是 Crane 保证自身正确性的主要手段。通过将 Rocq 提取到 OCaml（这是 Rocq 原生的提取目标）的结果与 Crane 生成的 C++ 代码进行对比，可以发现翻译过程中的错误。这种策略避免了完全验证提取器的高昂成本，同时仍然提供了实质性的正确性保证。静态分析工具进一步补充了这一保证，确保生成的 C++ 代码符合内存和线程安全的要求。
在集成层面，生成的 C++ 代码需要与既有的代码库兼容。虽然 Crane 努力生成符合 BDE 风格或其他编码标准的代码，但人工审查仍然是必要的。特别是在处理外部提供的原语（如通过 Crane Extract Skip 命令跳过的符号）时，需要确保这些符号在链接时能够正确解析。
Crane 的基准测试功能提供了对提取代码性能进行量化评估的能力。通过 Crane Benchmark 命令，开发者可以比较 Rocq 提取到 OCaml 与 Crane 提取到 C++ 在不同编译器优化级别下的运行性能。这种比较对于确保 C++ 输出的性能竞争力至关重要，特别是在性能敏感的应用场景中。
小结
Crane 代表了一种务实的形式化验证工程化路径。它不追求完全验证编译器管道的理想化目标，而是通过精心设计的提取机制、差分测试和静态分析的组合，在可接受的信任成本下生成高质量的 C++ 代码。对于希望在生产环境中利用形式化验证成果的团队，Crane 提供了一个值得认真考虑的工具链选择。其可配置性确保了适应不同代码库风格的能力，而对可读性的坚持则使得生成的代码能够融入既有的开发和维护流程中。
资料来源：
- Crane 官方文档，https://bloomberg.github.io/crane/