🐓🐫 rocq-of-ocaml

针对 OCaml 程序的正式验证

将 OCaml 程序翻译为 外观相似的 Rocq 代码，Rocq 是一种表达能力极强的形式化语言，用于表达并正式验证 各种类型的属性（不变量保持、断言失败缺失、向后兼容性、……）。我们使用 rocq-of-ocaml 来正式验证加密货币 Tezos 的“协议”（核心部分），该部分由 100,000 行 OCaml 代码组成。我们覆盖了大部分代码：在 coq-tezos-of-ocaml 项目中，80% 的文件至少包含一个经过正式验证的属性。这是 大规模 的正式验证。

请通过访问 https://koalendar.com/e/meet-with-formal-land 随时安排一次简短的会议以获取更多信息。我们提供正式验证服务和建议，并随时乐意进行简短交流。

📚 文档位于 https://formal.land/docs/tools/rocq-of-ocaml/introduction

🎯 目标

rocq-of-ocaml 为 OCaml 程序 🦄 提供正式验证。证明得越多，你越快乐。

通过将 OCaml 代码转换为类似的 Rocq 程序，我们可以利用 Rocq 现有的能力证明任意复杂的性质。rocq-of-ocaml 的最佳适用点是纯函数式和单子式程序。单子之外的副作用，如引用，以及面向对象编程等高级特性，可能永远不会得到支持。通过坚持使用 OCaml 的支持子集，你可以将数百万行代码导入 Rocq 并进行大规模证明。通过在每次代码更改后运行 rocq-of-ocaml，你可以确保你的证明仍然有效。生成的 Rocq 代码旨在保持稳定，不包含生成的变量名。我们建议像组织测试一样组织你的证明文件，每个代码文件对应一个证明文件。

rocq-of-ocaml 的指导思想是 TypeScript。我们不是将类型引入无类型语言，而是将证明引入有类型语言。方法是相同的：找到正确的最佳适用点，在需要时使用启发式方法，通过错误消息引导用户。我们在加密货币 Tezos 中使用 rocq-of-ocaml，希望借助形式化证明实现近乎零缺陷。Tezos 目前是最先进的加密货币之一，具有智能合约、权益证明、加密交易和协议升级。它旨在与 Ethereum 竞争。对于加密货币而言，形式化验证至关重要，因为没有中央权威来禁止漏洞利用和资金窃取。

rocq-of-ocaml 仍有一些未解决的问题，例如 GADTs 的无公理编译（一个正在进行的项目）。如果你愿意参与某个特定项目，可以通过 contact@formal.land 联系我们。

happiness and proofs

示例

从文件 main.ml 🐫 开始：

type 'a tree =
  | Leaf of 'a
  | Node of 'a tree * 'a tree

let rec sum tree =
  match tree with
  | Leaf n -> n
  | Node (tree1, tree2) -> sum tree1 + sum tree2

运行：

rocq-of-ocaml main.ml

获得文件 Main.v 🦄：

Require Import RocqOfOCaml.RocqOfOCaml.
Require Import RocqOfOCaml.Settings.

Inductive tree (a : Set) : Set :=
| Leaf : a -> tree a
| Node : tree a -> tree a -> tree a.

Arguments Leaf {_}.
Arguments Node {_}.

Fixpoint sum (tree : tree int) : int :=
  match tree with
  | Leaf n => n
  | Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
  end.

现在你可以使用 Rocq 对 sum 函数进行归纳法证明。要了解如何编写证明，你可以直接查看 Rocq 文档。学习编写证明就像学习一种新的编程范式。这需要时间，但可能是值得的！以下是一个证明示例：

(** Definition of a tree with only positive integers *)
Inductive positive : tree int -> Prop :=
| Positive_leaf : forall n, n > 0 -> positive (Leaf n)
| Positive_node : forall tree1 tree2,
  positive tree1 -> positive tree2 -> positive (Node tree1 tree2).

From Stdlib Require Import micromega.Lia.

Lemma positive_plus n m : n > 0 -> m > 0 -> n + m > 0.
  lia.
Qed.

(** Proof that if a tree is positive, then its sum is positive too *)
Fixpoint positive_sum (tree : tree int) (H : positive tree)
  : sum tree > 0.
  destruct tree; simpl; inversion H; trivial.
  apply positive_plus; now apply positive_sum.
Qed.

安装

使用 OCaml 包管理器 opam，运行：

opam install rocq-of-ocaml

用法

基本命令是：

rocq-of-ocaml file.ml

你可以开始使用 tests/ 中的测试文件进行实验，或者查看我们的在线示例。rocq-of-ocaml 使用 Merlin 编译 .ml 或 .mli 文件以理解项目的依赖关系。首先需要有一个 已编译的项目，并且 Merlin 配置正常工作。如果你使用 dune 作为构建系统，则会自动满足此条件。

文档

你可以在项目网站上阅读文档，地址为 https://formal.land/docs/tools/rocq-of-ocaml/introduction。

支持

OCaml 核心（函数、let 绑定、模式匹配等） ✔️
类型定义（记录、归纳类型、同义词、相互类型） ✔️
单子程序 ✔️
作为命名空间的模块 ✔️
作为多态记录的模块（签名、函子、一等模块） ✔️
多文件项目（得益于 Merlin） ✔️
.ml 和 .mli 文件 ✔️
存在类型（我们使用非谓词集合以避免宇宙爆炸） ✔️
部分支持 GADT 🌊
部分支持多态变体 🌊
部分支持可扩展类型 🌊
忽略单子之外的副作用 ❌
不支持面向对象编程 ❌

即使在出现错误的情况下，我们也会尝试生成一些 Rocq 代码以及错误消息。生成的 Rocq 代码应该是可读的，且大小与 OCaml 源代码相似。生成的代码在第一次尝试后不一定能编译。这可能是由各种错误引起的，例如名称冲突。请通过相应地更新 OCaml 源代码来修复这些错误，不要犹豫。如果您需要更多帮助，请通过在此仓库中打开 issue 与我们联系。

贡献

如果您想为该项目做出贡献，您可以提交 pull request。

使用 opam 构建

要安装当前开发版本：

opam pin add https://github.com/formal-land/rocq-of-ocaml.git#master

手动构建

阅读项目根目录下的 rocq-of-ocaml.opam 文件，以了解需要安装的依赖项并获取构建项目的命令列表。

许可证

MIT（开源软件）