【Rust日报】2026-11-06 用 Lean 证明没有未定义行为
内容提要
本期 Rust 社区动态：lean-miri 将 Miri 移植到 Lean 4，用于证明 Rust 程序无未定义行为，已证明空函数和缓冲区复制两例，但检查耗时超 2 小时、证明超 70 万行，且存在信任边界；有文章列举不用 String::new 创建 String 的多种写法；compile_fail 测试发现泛型 Display 实现破坏了 Secret<T> 不实现 Display 的设计；另有文章对比 Rust 与 C++ 的指针来源，说明 ptr::addr 不暴露来源、with_addr 保留来源。
延伸解读
形式化验证的代价与边界
lean-miri 虽能证明程序无未定义行为，但当前代价极高：duplicate_prefix 的证明检查超过 2 小时，证明本身超 70 万行，导出的程序数据约 500MiB。此外，exporter、编译器及解释器与 Rust 的对应关系均属信任边界，移植并非 100% 忠实。这说明该工具目前更适合验证小型关键片段，而非日常开发。
compile_fail 测试的警示
Secret<T> 案例表明，泛型 Display 实现会悄然拓宽 API，使原本禁止的格式化操作变得可编译。普通单元测试无法发现这类设计约束的破坏，而 compile_fail doctest 能捕获。不过该测试也有局限：片段可能因无关原因编译失败。作者建议搭配正例，并考虑更精确的 UI 测试，以降低误报和漏报。
指针来源的实际影响
文章通过 C++ 与 Rust 的对比说明，来源信息影响编译器优化。Rust 的 ptr::addr 不暴露来源，因此编译器仍会重新加载变量；而 with_addr 可保留来源、仅替换地址，适合带标志位的指针。但 tagged 指针若未对齐则不能解引用，否则是未定义行为。旧式整数转指针写法虽能运行，却会触发 Miri 警告，并可能漏掉指针错误。
Q&A
lean-miri 是什么？它如何证明 Rust 程序没有未定义行为？
lean-miri 是将 Rust 的 Miri 解释器移植到 Lean 4 的项目，用于在 Miri 的执行模型下证明 Rust 程序没有未定义行为。它把 Miri 的操作语义放入 Lean 4，从而可以写成定理：对满足前提的输入，解释器的结果不是未定义行为。程序通过 Rust 写的 exporter 将 MIR 和元数据编成 JSON，再由 Lean 写的解释器读取。
lean-miri 目前有哪些限制和挑战？
lean-miri 的解释器尚未做性能优化，duplicate_prefix 的证明检查耗时超过 2 小时，导出的程序数据约 500MiB，第二个例子的证明超过 70 万行 Lean。当前是向前执行的步进解释器，没有最弱前置条件等程序逻辑，中间引理需手写。为跑通验证，实验关闭了垃圾回收和数据竞争检测。此外，exporter 处于信任边界，移植并非 100% 忠实。
在 Rust 中，除了 String::new，还有哪些创建 String 的方法？
文章列举了多种写法，例如：字符数组 into_iter().collect()；String::from_utf8(vec![102, 101, 114, 114, 105, 115])；通过 Debug 格式化单元变体；CString::new("ferris").unwrap().into_string().unwrap()；include_str!("file.rs").to_owned()；线程名读取；子进程 stdout 转换；f64::from_bits 构造字节；String::from_raw_parts；type_name 解析；panic_any 配合 catch_unwind；以及格式化填充等。
compile_fail 测试如何帮助发现泛型 Display 实现破坏 Secret<T> 的设计？
作者为 Secret<T> 编写了 compile_fail doctest，要求用 Display 格式化 Secret 时编译失败。后来有人添加了泛型 Display 实现，普通单元测试通过，但该 doctest 失败，因为代码现在能编译。这暴露了新的 trait 实现拓宽了 API，破坏了原本不实现 Display 的设计意图。
Rust 和 C++ 在指针来源（provenance）处理上有何不同？
指针来源记录指针属于哪次分配以及可访问的内存。C++ 中，将指针转为整数会暴露来源，编译器必须假设整数可重建指针，从而放弃优化；而 Rust 的 ptr::addr 读出地址但不暴露来源，因此编译器仍可优化。Rust 提供 with_addr 保留来源只换地址，而旧写法 p as usize 再转回指针会暴露来源，Miri 会警告。
在 Rust 中如何安全地使用带标志位的指针而不丢失来源？
可以使用 with_addr 方法保留来源、只替换地址，例如 let tagged: *const u32 = p.with_addr(p.addr() | 1)。注意 tagged 不能解引用，因为地址未对齐，解引用是未定义行为。清掉最低位后再用 with_addr 恢复。避免使用 p as usize 再转回指针，因为这会暴露来源并可能触发 Miri 警告。
