Verus：基于 Rust 验证代码正确性，指南助你掌握验证概念与技术！

键盘快捷键按 ← 或 → 可在各章节间导航按 S 或 / 能在本书中搜索按 ? 可显示此帮助信息按 Esc 则可隐藏此帮助信息。模式选项包括自动明亮模式Rust 模式煤炭模式海军蓝模式Ayu 模式Verus 教程与参考手册Verus 概述Verus 是用于验证用 Rust 编写的代码正确性的工具。其主要目标是基于现有验证框架如 Dafny、Boogie、F*、VCC、Prusti、Creusot、Aeneas、Cogent、Rocq 和 Isabelle/HOL的理念验证底层系统代码的完整功能正确性。验证是静态的Verus 不会添加运行时检查而是使用计算机辅助定理证明来静态验证可执行的 Rust 代码在所有可能的执行情况下都能满足用户提供的某些规范。更详细地说Verus 的目标如下提供一种纯数学语言来表达规范类似于 Dafny、Creusot、F*、Coq、Isabelle/HOL。提供一种基于经典逻辑类似于 Dafny的数学语言来表达证明类似于 Dafny、F*、Coq、Isabelle/HOL。提供一种基于 Rust类似于 Prusti、Creusot 和 Aeneas的底层命令式语言来表达可执行代码类似于 VCC。基于以下原则生成小型、简单的验证条件以便像 Z3 这样的 SMT 求解器能够高效求解使数学规范语言与 SMT 求解器的数学语言相近类似于 Boogie。使用轻量级线性类型检查而非 SMT 求解来推理内存和别名问题类似于 Cogent、Creusot、Aeneas 和 线性 Dafny。我们认为 Rust 是实现这些目标的理想语言。Rust 将底层数据操作包括手动内存管理与先进的高级安全类型系统相结合。该类型系统包含了高级验证语言中常见的特性如代数数据类型支持模式匹配、类型类和一等函数。这使得以自然的方式表达规范和证明变得容易。更重要的是Rust 的类型系统对线性类型和借用提供了复杂的支持这处理了大部分关于内存和别名的推理。因此剩余的推理可以忽略大多数内存和别名问题将 Rust 代码视为纯函数式语言编写的代码从而使验证更加容易。目前我们不打算支持所有 Rust 特性和库相反我们将专注于支持用户所需的高价值特性和库。验证验证器本身。验证 Rust/LLVM 编译器。本指南本指南假设你已经对 Rust 编程的基础知识有一定了解。如果你还不了解我们建议你花几个小时浏览 学习 Rust 页面。熟悉 Rust 对使用 Verus 很有帮助因为 Verus 基于 Rust 的语法和类型系统来表达规范、证明和可执行代码。实际上并没有单独的规范和证明语言规范和证明都是用 Rust 语法编写并使用 Rust 的类型检查器进行类型检查。因此如果你已经掌握了 Rust那么开始使用 Verus 会更容易。然而验证 Rust 代码的正确性需要一些超出编写普通可执行 Rust 代码的概念和技术。例如Verus 通过宏扩展了 Rust 的语法引入了用于编写规范和证明的新概念如 forall、exists、requires 和 ensures还引入了新的类型如数学整数类型 int 和 nat。证明一个 Rust 函数满足其后置条件ensures 子句或一个函数调用满足其前置条件requires 子句可能具有挑战性。因此本指南的教程将带你逐步了解各种概念和技术从相对简单的概念关于整数的基本证明开始过渡到中等难度的挑战关于数据结构的归纳证明然后再到更高级的主题如使用 forall 和 exists 对数组进行证明以及对并发代码进行证明。所有这些证明都借助了自动定理证明器具体来说是 Z3一个可满足性模理论求解器简称 “SMT 求解器”。SMT 求解器通常能够在无需程序员额外帮助的情况下证明简单的属性如布尔值或整数算术的基本属性。然而更复杂的证明通常需要程序员和 SMT 求解器共同努力。因此本指南还将帮助你了解 SMT 求解的优势和局限性并提供如何填补 SMT 求解器无法自动处理的证明部分的建议。例如SMT 求解器通常无法自动进行归纳证明但你可以通过编写一个递归的 Rust 函数其 ensures 子句表达归纳假设来编写归纳证明。