Creusot 0.11.0：VerifyThis 竞赛优胜者

# Creusot 0.11.0：VerifyThis 冠军 来源：https://devlog.creusot.rs/2026-04-20/ 欢迎来到 Creusot 开发日志。Creusot 是一款用于证明 Rust 程序正确性的工具。 ## 全新官网 如果你对这个项目感兴趣，请访问 Creusot 的全新官网：creusot.rs。网站介绍了 Creusot 的定位、主要功能以及相关资源链接。新增部分还包括一份与 Creusot 相关的学术出版物列表。 --- 上周，Creusot 团队前往都灵参加了 ETAPS 会议。我们重点参与了两个活动：VerifyThis 挑战赛和 RustVerify 研讨会。本次版本的发布稍作延迟，以便团队准备 RustVerify 的演讲。 ## VerifyThis 2026 VerifyThis (https://verifythis.github.io/onsite/) 是一项程序验证竞赛。它与编程比赛类似，但目标不是通过测试用例，而是使用你熟悉的验证工具来证明程序满足给定的规范。 > 解决方案将依据正确性、完整性和优雅度进行评判。 Jacques-Henri Jourdan 和 Li-yao Xia 组队（队名：*The Steelmakers*）参加了今年的 VerifyThis 挑战赛，使用的工具正是 Creusot。很高兴地宣布，我们荣获了**最佳整体团队奖**！这是一次绝佳的机会，让我们切身体验了长期使用该工具的实际情况。我们的工具链基本未引发任何问题——除了一个在 `\#[bitwise\_mode]` 中的孤立 Bug ——因此我们可以迅速专注于解题本身。 并发问题（挑战题 2）是 Ghost Permissions 特性的完美用例。该特性于今年早些时候在 Creusot 中推出（CPP 2026 (https://hal.science/hal-05396946v1)），最初则在 Verus 中提出（OOPSLA 2023 (https://arxiv.org/abs/2303.05491)）。 VerifyThis 的挑战题设计得格外艰深，参赛者允许对问题进行适配以符合工具限制或时间要求——题目描述甚至会明确提示可能的简化方案。但我们很自豪的是，Creusot 使得我们实现了零次简化：无论优劣，我们都严格按照题目原始描述进行了验证。我们的解决方案已收录于 creusot-examples 仓库 (https://github.com/creusot-rs/creusot-examples?tab=readme-ov-file#verifythis-2026) 中。 ## RustVerify 2026 RustVerify 研讨会 (https://sites.google.com/view/rustverify2026/home) 包含两场直接与 Creusot 相关的演讲： - *Verifying the Rust standard library with Creusot*：由 Li-yao Xia 等人主讲，介绍了我们在标准库 slice 函数验证方面的工作进展 (https://github.com/Lysxia/creusot-rust-std)。该工作使用了新的“证明模式（proof modes）”特性，目前仍在开发中，未包含在本版本中。 - *Supporting weak memory in Creusot and Verus*：由 Natalie Neamtu 等人主讲，介绍了针对 release-acquire 和 relaxed 原子访问的新原语。在 Creusot 侧，这些功能已在此版本中可用。关于如何在 Creusot 中进行并发推理的详细文档将是未来的工作。 ## Creusot 有哪些新变化？ 本次发布没有重大新功能；详见更新日志 (https://github.com/creusot-rs/creusot/blob/master/CHANGELOG.md#0110---2026-04-20)。不过下个月已经准备好了重磅内容，敬请期待！ ## 结果变量的显式绑定 现在可以在后置条件中为结果变量命名： ```rust #[ensures(result@ == 0)] // 默认名称为 `result`（旧语法，仍支持） #[ensures(|my_result| my_result@ == 0)] // 显式命名为 `my_result`（新语法） fn zero() -> usize { 0 } ``` 你也可以使用模式解构结果： ```rust #[ensures(|(_, b)| b@ == 42)] fn forty_two() -> (usize, usize) { (0, 42) } ``` ## 集合不应充当迭代器 这是我们关于 Rust 迭代器学到的一点经验。`Vec` 这样的集合类型通常自带三种迭代器：“所有权”迭代器（通常名为 `IntoIter`）、“共享”迭代器（`Iter`）和“可变”迭代器（`IterMut`）。每种迭代器类型都通过对应的 `IntoIterator` trait 实现与集合类型关联。 我当时的“天才”想法是：让 Creusot 中表示 `T` 序列的逻辑类型 `Seq` 自己兼任这三种迭代器的角色。我以为这样可以轻松实现 `Seq` 的 `IntoIterator` trait。但这事实证明是个坏主意。你能猜出下面这段代码的问题所在吗？ ```rust /* A bad idea in the making */ impl Iterator for Seq { type Item = T; fn next(&mut self) -> Option { /* ghost code */ } } // Blanket impl from std impl IntoIterator for I { type IntoIter = Self; fn into_iter(self) -> Self::IntoIter { self } } impl IntoIterator for &Seq { type IntoIter = Seq<&T>; fn into_iter(self) -> Self::IntoIter { /* ghost code */ } } impl IntoIterator for &mut Seq { type IntoIter = Seq<&mut T>; fn into_iter(self) -> Self::IntoIter { /* ghost code */ } } ``` 如果这是一个普通类型（比如 `Vec`），不让 `Vec` 自身充当迭代器的一个简单原因是效率极低：`next` 会移除第一个元素，然后将其余所有元素向前平移，耗时呈线性增长。而另一个“显然”的选择是将 `next` 定义为 `pop`，这会导致反向遍历。此外，对于借用迭代器（`Iter` 和 `IterMut`），你并不希望分配一整个包含引用的 `Vec`，而是希望 `next` 在不分配任何内存的情况下动态返回引用。 然而，`Seq` 是一种*逻辑类型*（logic type）：它仅存在于*幽灵代码*（ghost code）中用于辅助验证（其关键特性是 `Seq` 的长度是有限的但无固定上限，这与 `Vec` 不同，后者最多只能包含 `usize::MAX` 个元素）。由于幽灵代码在运行时实际上并不存在，因此性能问题无需考虑。 那么还有其他地方出问题了吗？简单来说，**上述代码无法编译**。Rust 编译器拒绝了 `IntoIterator for &mut Seq` 的实现，因为它与 blanket 实现重叠（https://doc.rust-lang.org/std/iter/trait.IntoIterator.html#impl-IntoIterator-for-I）： ```rust impl IntoIterator for I ``` 事实上，由于 `Seq: Iterator`，根据以下实现（https://doc.rust-lang.org/std/iter/trait.Iterator.html#impl-Iterator-for-%26mut+I），我们也自动拥有了 `&mut Seq: Iterator`： ```rust impl Iterator for &mut I ``` 此外，如果你坚持使用该 blanket 实现，最终会导致非常令人困惑的行为：如果你在 `&mut s` 上编写 `for` 循环，你本以为是在遍历可变的借用元素 `&mut T`，但实际上你却是在消费 `s` 以产出完全拥有的 `T`！ ```rust let s: Seq = ...; for x in &mut s { ... } /* Here `s` would be empty! */ ``` 既然这个错误已经被编译器捕获，而且此类代码本来就是为了形式化证明而写的，那其实也没什么大不了的……除非我在上一个版本中就已经开始为 Creusot 的另一种逻辑类型 `FMap` 做同样的操作。我当时恰好临时省略了 `IntoIterator for &mut FMap`，否则就能提前暴露这个问题。哎呀。 我一意识到这个错误就赶紧回滚了代码（https://github.com/creusot-rs/creusot/pull/1964/changes#diff-5c9d108ce643f2321e13267ebb68245b32a136bd14dc968d2d7c8612f21967deL541）。因此，`Seq`（以及其他“逻辑类型”）现在拥有独立的迭代器类型（`IntoIter`、`Iter`、`IterMut`），它们仅仅是对 `Seq`、`Seq<&T>`、`Seq<&mut T>` 的 newtype 包装。 这就是本月（费了一番功夫才得来的）教训：**集合不应充当迭代器**。