comprehensive-rust 安全证明推论：为什么纯 Safe Rust 实现的函数必然 Sound

comprehensive-rust 安全证明推论：为什么纯 Safe Rust 实现的函数必然 Sound

【免费下载链接】comprehensive-rustThis is the Rust course used by the Android team at Google. It provides you the material to quickly teach Rust.项目地址: https://gitcode.com/GitHub_Trending/co/comprehensive-rust

导读

本文基于 Google Android 团队 Rust 课程（comprehensive-rust）"unsafe 深潜"章节中的《Soundness Proof (Part 2)》（corollary.md）展开。核心主题是回答一个问题：纯 Safe Rust 写出来的函数，为什么天生就是 sound（健全）的？文章中我们将先梳理 sound / unsound 的正式定义与"证明责任"归属，再逐条拆解该推论的证明步骤，并结合仓库中三类典型 sound 代码形态（纯 Safe、封装 unsafe、带文档化安全前置条件的 unsafe 函数）的源码示例，帮助读者在编写与审查 Rust 代码时准确判断一段代码是否健全、unsafe的证明负担到底落在谁身上。

一、从定义出发：什么是 sound（健全）的函数

在进入推论之前，需要先明确课程给出的正式定义。位于 soundness.md 中的定义如下：

sound 的函数：只要它的安全前置条件（safety preconditions）被满足，就不可能触发未定义行为（UB）的函数。

这个定义有两个关键短语，缺一不可：

1. "安全前置条件被满足"：sound 不是无条件的。一个 sound 的 unsafe 函数允许声明前置条件（例如"传入的指针必须非空、必须指向合法内存"），只要调用方满足这些条件，函数行为就保证良好（不会出现 UB）。
2. "不可能触发 UB"：soundness 与"内存安全问题"深度绑定。rust-is-sound.md 明确指出，soundness 是 Rust 的根基性原则，可以通俗地理解为"不可能引发内存安全问题"。

课程提醒一个容易被忽略的事实（见 soundness.md 的授课要点）：编译器不会替你检查安全前置条件。负责满足前置条件的是"实现调用方的那位程序员"，这是将 unsafe 函数设计得 sound 时必须牢记的责任边界。

二、反面对照：unsound（不健全）意味着什么

unsoundness.md 给出了对照定义：

unsound 的函数：即使你满足了文档中声明的所有安全前置条件，它依然可能触发 UB。

也就是说，unsound 与"调用方是否遵守规则"无关——问题出在函数内部实现本身。unsoundness.md 中毫不含糊地写道：Unsound code is BAD，即便你完全按文档规则调用，unsound 代码仍可能触发 UB。

这一节还给出一条重要的工程准则：仓库中不允许存在任何 unsound 代码，而"找出 unsound 代码"是代码评审（code review）的首要目标。这与 corollary.md 的推论形成闭环：因为纯 Safe Rust 的函数不存在 unsound 的可能，所以审查者的注意力应当集中在包含unsafe的部分，尤其是那些把证明负担转移给调用方的 unsafe 函数。

三、核心推论：纯 Safe Rust 实现的所有函数都是 sound 的

corollary.md 在 sound 定义的基础上立刻导出一个推论（Corollary）：

所有用纯 Safe Rust 实现的函数都是 sound 的。

其证明（Proof）只有三步，逻辑非常简洁：

1. Safe Rust 代码没有安全前置条件。Safe Rust 由编译器保证内存安全，不需要调用方额外承诺任何前提（没有裸指针、没有可变静态、没有 union 访问等需要人工把关的约束）。
2. 因此，调用纯 Safe Rust 函数的调用方，总是平凡地（trivially）满足这个"空的前置条件集合"。空集的条件当然永远成立，调用方无需做任何额外论证。
3. Safe Rust 代码不可能触发 UB。这是 Safe Rust 语言层面的根本保证。

由 1–3 得证：QED。

把证明"翻译"成非正式语言（课程给出的授课提示）：所有 Safe Rust 代码都是"好代码"——程序员不需要为它操心任何安全前置条件，它总是按规则行事，永远不会触发 UB。

值得强调的是"平凡满足空前置条件"这一句：这正是 sound 定义与 Safe Rust 交汇的地方。sound 要求"前置条件满足 ⇒ 无 UB"，而 Safe Rust 的前置条件集合为空，于是"无 UB"对任何输入都成立，sound 自动成立。

四、推论的另一面：证明责任（burden of proof）落在谁身上

推论的成立，本质是把"证明义务"从程序员身上转移走了。课程在 3-shapes-of-sound-rust.md 中总结了 sound 代码只可能有三种形态，以及各自的证明责任归属：

可见，corollary.md 的推论对应表格第一行：纯 Safe 函数把证明责任完全交给了编译器，程序员不需要做任何证明工作。而一旦引入unsafe，证明责任就会转移到作者或调用方身上——这正是后续章节（copying-memory 系列）要逐一剖析的内容。

五、三种形态的代码佐证：从纯 Safe 到文档化前置条件

仓库中 copying-memory 目录用同一个copy（拷贝字节切片）函数演示了三种演进版本，恰好对应上表三种形态，也直观印证了推论。

5.1 纯 Safe Rust 版本（推论直接适用）

safe.md 展示了第一种形态：

pub fn copy(dest: &mut [u8], source: &[u8]) { for (dest, src) in dest.iter_mut().zip(source) { *dest = *src; } }

该实现只用 Safe Rust 的迭代器完成拷贝。课程指出：无论传入什么参数，这个copy都不可能触发内存安全问题——因为 Rust 的类型系统与借用检查器已经替你排除了以下所有隐患：

• 不存在别名（aliasing）问题（借用检查器保证&mut互斥）；
• 悬垂指针不可能出现；
• 对齐必然正确；
• 不会意外读取未初始化的内存；
• 不需要手动处理空指针或越界检查。

用推论的表述来说：这个函数"没有安全前置条件"，所以它是 sound 的。课程同时补充了一个澄清：sound 不等于"一定符合调用方的期望"——如果dest空间不足，copy只会拷贝一部分数据（这是 zip 截断到较短长度的行为），但这属于逻辑语义问题，而非 UB，sound 只承诺"无 UB"。

5.2 封装 unsafe 的 Safe 函数（作者承担证明责任）

encapsulated-unsafe.md 演示了第二种形态：函数签名仍是 safe 的，但内部通过get_unchecked/get_unchecked_mut手动访问内存，绕开了迭代器：

pub fn copy(dest: &mut [u8], source: &[u8]) { let len = dest.len().min(source.len()); let mut i = 0; while i < len { // SAFETY: `i` must be in-bounds as it was produced by source.len() let new = unsafe { source.get_unchecked(i) }; // SAFETY: `i` must be in-bounds as it was produced by dest.len() let old = unsafe { dest.get_unchecked_mut(i) }; *old = *new; i += 1; } }

课程要点：

• 从调用方视角看，这个函数依然是 safe 的（签名没有 unsafe），调用方无需了解内部细节；
• 从 soundness 角度看，只要不可能存在任何输入触发内存安全问题，含 unsafe 块的 Safe 函数就是 sound 的；
• 这里的证明责任在函数作者：作者必须用内联的// SAFETY:注释说明为什么每个 unsafe 块在当前上下文是安全的（本例如i由len约束必然在界内），并保证循环逻辑不会引入越界访问。

5.3 文档化安全前置条件的 unsafe 函数（调用方承担证明责任）

documented-safety-preconditions.md 演示第三种形态：函数被声明为unsafe fn，并用# Safety文档段声明前置条件：

/// # Safety /// /// This function can easily trigger undefined behavior. Ensure that: /// /// - `source` pointer is non-null and non-dangling /// - `source` data ends with a null byte within its memory allocation /// - `source` data is not freed (its lifetime invariants are preserved) /// - `source` data contains fewer than `isize::MAX` bytes pub unsafe fn copy(dest: &mut [u8], source: *const u8) { // ...内部通过 unsafe 解引用与 from_raw_parts 构造切片... }

这一形态的关键约束（对应 corollary 推论的反面）：soundness 不再自动成立。unsafe 函数要 sound，必须同时满足两个条件：

1. 安全前置条件被文档化（# Safety段写得足够清楚）；
2. 函数内部每个 unsafe 块都配有// SAFETY:注释，说明在哪些前置条件下该操作合法。

课程还指出 main 中调用方的两种常见错误，用来强调"调用方承担证明责任"：

• a（[114, 117, 115, 116]）并不满足copy的"数据以 null 字节结尾"这一前置条件——直接调用会产生 UB；
• 在unsafe块中调用copy时，需要写// SAFETY:注释，逐一说明本次调用满足了哪些前置条件。

这正是"3 Shapes"表格第三行的工程含义：一旦进入 unsafe 函数，编译器不再兜底，证明责任移交调用方；审查者应据此核查调用点的 SAFETY 注释是否完整、准确。

六、总结：如何运用这个推论

回顾整条逻辑链（soundness-proof.md 统领 soundness.md → unsoundness.md → corollary.md 三个小节）：

1. sound 的定义：前置条件满足时绝不触发 UB（soundness.md）；
2. unsound 的定义：即便满足文档化前置条件仍可能触发 UB（unsoundness.md）；
3. 推论（本文核心）：纯 Safe Rust 函数没有前置条件、不可能触发 UB，因此必然 sound（corollary.md）。

落到日常实践，这个推论给开发者三条可操作准则：

• 能用纯 Safe Rust 实现，就用纯 Safe Rust 实现——它把证明责任交给编译器，是成本最低、最可靠的 sound 代码形态；
• 当需要unsafe时，优先"封装"而非"暴露"——把 unsafe 块封装在 safe 函数内部并配齐// SAFETY:注释，由作者承担证明责任，调用方保持安全体验；
• 必须暴露 unsafe 函数时，前置条件文档要精确、调用点注释要完整——unsafe 函数的 soundness 依赖于# Safety文档与调用点// SAFETY:注释的配合，这也是代码评审中查找 unsound 代码的着力点。

本文涉及的课程小节均位于 src/unsafe-deep-dive/rules-of-the-game 目录下，其中 3-shapes-of-sound-rust.md 提供三种 sound 形态总览，copying-memory 目录提供可运行的完整代码示例，建议对照阅读以获得完整图景。

【免费下载链接】comprehensive-rustThis is the Rust course used by the Android team at Google. It provides you the material to quickly teach Rust.项目地址: https://gitcode.com/GitHub_Trending/co/comprehensive-rust