Creusot 0.14.0 release - Contracts for Rust, formally proved

本文为原文前 6,000 字符的节选翻译，完整内容请查看原文。

We are pleased to announce the release of version 0.14.0 of Creusot, our formal verification tool for Rust. In this post, we highlight a small selection of new features. See the full changelog for the rest. What’s new in Creusot? Partial orders Previously, Creusot restricted its specification of PartialOrd to total orders. Since version 0.13.0, we have relaxed it to allow partial orders. (We skipped a devlog entry for 0.13.0 so let’s talk about this here.)

我们很高兴宣布发布 Creusot 0.14.0 版本，这是我们用于 Rust 的形式化验证工具。在这篇文章中，我们将重点介绍一些新功能，其余内容请参阅完整的更新日志。Creusot 有哪些新变化？偏序关系：此前，Creusot 将 PartialOrd 的规范限制为全序关系。自 0.13.0 版本起，我们放宽了这一限制，允许使用偏序关系。（由于我们跳过了 0.13.0 的开发日志，因此在这里进行说明。）

Our previous definition of total order (OrdLogic) relied on the comparison function cmp_log (the logic counterpart to cmp), which returns an Ordering. That had the benefit of making totality an implicit consequence of the type of the function: any two elements must compare either Less, Equal, or Greater. With the switch to partial orders, a traditional formulation based on a boolean comparison function (”<”, aka. lt_log) becomes more natural. A strict partial order (PartialOrdLogic) consists of a comparison function lt_log which is irreflexive and transitive. Totality becomes another law: for all x, y, the trijunction x < y || x == y || y < x must hold.

我们之前对全序关系（OrdLogic）的定义依赖于比较函数 cmp_log（cmp 的逻辑对应项），它返回一个 Ordering。这样做的好处是使全序性成为函数类型的一个隐含结果：任意两个元素必须比较为 Less、Equal 或 Greater。随着转向偏序关系，基于布尔比较函数（“<”，即 lt_log）的传统表述变得更加自然。严格偏序关系（PartialOrdLogic）由一个非自反且传递的比较函数 lt_log 组成。全序性则成为另一条定律：对于所有 x 和 y，必须满足三歧性 x < y || x == y || y < x。

Interestingly, none of our existing proofs were affected by this change. Our automated provers just took it in stride. Logic VC gen Creusot now generates verification conditions (VCs) for snapshots, which are logic expressions embedded in Rust programs. In particular, this enhances the use of “lemma functions”, a common idiom in verification tools similar to Creusot. For example, you can encode a lemma as a logic function such as this, which logically amounts to the proposition forall hyp(x) -> concl(x).

有趣的是，我们现有的证明都没有受到此更改的影响。我们的自动化证明器轻松应对了这一变化。逻辑验证条件（VC）生成：Creusot 现在为 snapshot 生成验证条件（VC），这些 snapshot 是嵌入在 Rust 程序中的逻辑表达式。特别是，这增强了“引理函数”的使用，这是类似于 Creusot 的验证工具中的一种常见惯用法。例如，你可以将引理编码为如下逻辑函数，其逻辑上等同于命题 forall hyp(x) -> concl(x)。

Creusot now translates this call to an assertion that hyp(n) (the precondition of lemma) is true and an assumption that concl(n) (its postcondition) is true. Notably, these statements are specialized to n, the argument of lemma, so we avoid relying on provers to instantiate the universal quantifier in forall hyp(x) -> concl(x). It should be said that this new feature specifically enables logic functions to be used as lemma functions. Before, you could already do something similar with program functions. The difference is that (1) this version introduces a Rust function call, however trivial it may be, and (2) it must pass the borrow checker, which may require boilerplate to work around when all you wanted is to state some facts.

Creusot 现在将此调用转换为一个断言：hyp(n)（引理的前置条件）为真，并假设 concl(n)（其后置条件）为真。值得注意的是，这些语句专门针对引理的参数 n，因此我们避免了依赖证明器来实例化 forall hyp(x) -> concl(x) 中的全称量词。需要说明的是，此新功能专门使逻辑函数能够用作引理函数。在此之前，你已经可以使用程序函数实现类似的操作。区别在于：(1) 该版本引入了 Rust 函数调用，无论它多么简单；(2) 它必须通过借用检查器，而当你只是想陈述一些事实时，这可能需要编写样板代码来绕过检查。

In contrast, snapshots are entirely erased, so it is clear that they are there only for the sake of formal proof. Thus, these newly generated VCs for snapshots let us draw clearer boundaries between the worlds of programs and proofs. It may seem surprising that Creusot did not already do this. This comes down to the fact that programs and specifications are written in two separate languages, with their own semantics, and thus with different mechanisms and motivations for generating VCs. Without going into too much details, VCs were originally not generated for snapshot! because it isn’t necessary for soundness, but it turns out to help catch mistakes in specifications quicker (such as out-of-bounds indexing), on top of enabling new techniques such as that described above.

相比之下，snapshot 会被完全擦除，因此很明显它们的存在仅是为了形式化证明。因此，这些为 snapshot 新生成的 VC 让我们能够在程序世界和证明世界之间划定更清晰的界限。Creusot 之前没有这样做可能令人惊讶。这归结于程序和规范是用两种独立的语言编写的，它们有各自的语义，因此生成 VC 的机制和动机也不同。无需赘述细节，最初没有为 snapshot! 生成 VC 是因为它对可靠性而言并非必要，但事实证明，除了实现上述新技术外，它还有助于更快地发现规范中的错误（例如越界索引）。

rust-analyzer integration It is finally possible to use Go-to-definition in Pearlite specifications. To start, we needed to make rust-analyzer expand the code of specifications. In normal compilation, specification macros (#[requires], #[ensures], proof_assert!, snapshot!, etc.) erase themselves, discarding their contents. We just needed to pass options to rust-analyzer for it to expand those macros the same way Creusot does (see our guide for the relevant rust-analyzer settings). One worry we had was that Pearlite macros expand to not quite valid Rust code, not meant to be compiled by rustc: it passes the type checker, but not the borrow checker. Luckily for us, rust-analyzer does not do borrow checking, so it doesn’t see any problem with the expanded code.

rust-analyzer 集成：现在终于可以在 Pearlite 规范中使用“转到定义”功能了。首先，我们需要让 rust-analyzer 展开规范代码。在正常编译中，规范宏（#[requires]、#[ensures]、proof_assert!、snapshot! 等）会自行擦除并丢弃其内容。我们只需要向 rust-analyzer 传递选项，使其以与 Creusot 相同的方式展开这些宏（有关相关的 rust-analyzer 设置，请参阅我们的指南）。我们曾担心 Pearlite 宏展开后的代码并非完全有效的 Rust 代码，不打算由 rustc 编译：它能通过类型检查器，但无法通过借用检查器。幸运的是，rust-analyzer 不进行借用检查，因此它不会认为展开后的代码有问题。

With that done, Go-to-definition did start to work, but it returned numerous irrelevant results. The problem was that the tokens produced by Pearlite macros carried spans that were too coarse-grained. To explain it very roughly, when you activate Go-to-definition, rust-analyzer looks for identifiers in the final AST whose span ranges over your cursor. For example, a + b in Pearlite expands to a method call ::creusot_std::logic::ops::AddLogic::add_logic(a, b), where every generated token carries the span of the whole expression a + b. Hence, Go-to-definition from anywhere in that expression ends up looking up the definitions of all of creusot_std, logic, ops, AddLogic, and add_logic.

完成后，“转到定义”功能确实开始工作了，但它返回了许多不相关的结果。问题在于 Pearlite 宏生成的标记所携带的跨度（span）过于粗糙。粗略地解释一下，当你激活“转到定义”时，rust-analyzer 会在最终的 AST 中查找跨度覆盖你光标位置的标识符。例如，Pearlite 中的 a + b 会展开为方法调用 ::creusot_std::logic::ops::AddLogic::add_logic(a, b)，其中每个生成的标记都携带整个表达式 a + b 的跨度。因此，在该表达式的任何位置使用“转到定义”最终都会查找 creusot_std、logic、ops、AddLogic 和 add_logic 的所有定义。

The fix is to make the token add_logic have the span of +, and to make the other identifiers have a zero-width span, which seems to be enough for rust-analyzer to ignore them. Many thanks to Sarah Quiñones for figuring all this out. This fix makes navigating specifications in Creusot much more pleasant. Thanks for tuning in. If you have any questions about Creusot, you are welcome to join our Zulip channel, or to open a discussion or an issue on.

解决方法是让 add_logic 标记具有 + 的跨度，并使其他标识符具有零宽度的跨度，这对于让 rust-analyzer 忽略它们似乎已经足够了。非常感谢 Sarah Quiñones 解决了这个问题。此修复使在 Creusot 中浏览规范变得更加愉快。感谢关注。如果你对 Creusot 有任何疑问，欢迎加入我们的 Zulip 频道，或发起讨论或提交 issue。