lean-miri 用 Lean 证明没有未定义行为
lean-miri 是把 Rust 的 Miri 解释器移植到 Lean 4 的项目，用来在 Miri 的执行模型下证明一段 Rust 程序没有未定义行为。项目页在 https://proofs-rs.github.io/lean-miri/ ，仓库在 https://github.com/proofs-rs/lean-miri 。作者 ___yuni 2026 年 11 月 5 日发到 r/rust，采集时 150 分、26 条评论。
Miri 检查的是具体执行。lean-miri 把同一套操作语义放进 Lean 4，于是可以写成定理：对满足前提的输入，解释器的结果不是未定义行为。作者写，Miri 已经覆盖高级 trait 和裸指针，也实现了现有已知的各类未定义行为检查。移植这条现成的解释器，就不另做一套只覆盖语言子集的语义。
目前移植了解释器的大部分。已经证明没有未定义行为的例子有两个。一个是空函数 empty_function。空函数仍会初始化调用帧再返回。定理覆盖调用初始化和这次调用里每个有限执行前缀，前提是声明过的调用方和执行配置。安全的资源耗尽被允许，不保证每种资源供给都能正常返回。另一个是 duplicate_prefix：把缓冲区前 n 个字节复制到后面 n 个字节。n == 0 直接返回 true。n > buf.len() / 2 返回 false。通过检查之后，用 as_mut_ptr 取出指针，在 unsafe 里调用 std::ptr::copy_nonoverlapping。引用按 Tree Borrows 处理。站点写，对声明域里的每个 count 和每份输入，定理给出正常返回、没有解释器错误，以及任何被允许的有限前缀上都没有未定义行为。它不保证每一种 Rust 调用历史都能形成这次调用，也不额外保证返回的布尔值。
程序进入 Lean 的路径是：Rust 写的 exporter 把 MIR 和元数据编成 JSON，Lean 写的解释器读这份 JSON。元数据包括相关标准库类型的布局和大小。作者在评论里写，exporter 处于信任边界，另外有一批差分测试，这不等于移植 100% 忠实。编译器、exporter，以及解释器和 Rust 的对应关系，站点都列为信任边界。
验证 Tree Borrows 的状态转移时，作者碰到 Miri 内部断言失败，报给了 rust-lang/miri#5543。issue 标题是 [tree borrows] Internal assertion failure during wildcard access traversal。
限制也写在说明里。Lean 里的解释器还没有做性能优化。duplicate_prefix 的证明检查要超过 2 小时。导出的程序数据大约 500MiB。现在是向前执行的步进解释器，没有最弱前置条件这类程序逻辑，中间引理要手写。为了先把验证跑通，当前实验关掉了垃圾回收和数据竞争检测。第二个例子的证明超过 70 万行 Lean。作者写，移植大部分由 agent 完成，中间有不少人工介入；例子程序的验证需要更多人工指导。作者写自己的背景是计算机科学和逻辑，技术决定是自己做的。
JoJoModding 的评论有 36 分，问程序怎么进 Lean、怎么知道移植忠实、Tree Borrows 的 bug 是什么。annodomini 的评论有 29 分，问有多少是 LLM 写的，以及作者本人有没有形式化验证经验。
原文链接：https://proofs-rs.github.io/lean-miri/
不用 String::new 造出字符串
这是 Matthias Endler 写的一篇说明，列了不用 String::new 得到 String 的若干写法。页面写最后更新于 2026 年 11 月 5 日。作者从 RustLab 2026 回来后把一场没有录像的闪电演讲写成了文章。mre__ 同日发到 r/rust，采集时 94 分、14 条评论。
字符数组可以 into_iter().collect()。UTF-8 字节可以 String::from_utf8(vec![102, 101, 114, 114, 105, 115])，这六个字节是 ferris。给单元变体 ferris 派生 Debug，再 format!("{:?}", Mascot::ferris)，得到的也是这个名字。作者写，Debug 输出不是稳定的序列化格式，这里只是这个名字碰巧能用。
CString::new("ferris").unwrap().into_string().unwrap() 会先加上 NUL，转回 String 时去掉终止符并检查剩余字节是合法 UTF-8。另一条路是故意把带 NUL 的字节交给 CString::new，用 unwrap_err().into_vec() 拿回被拒绝的字节，再 pop() 掉注入的 NUL。char::from(u8) 把每个字节当成码点，不按 UTF-8 解码。收成 String 时再编码成合法 UTF-8。原字节如果是多字节 UTF-8，结果文本可以是错的，但转换本身不会失败。
include_str!("file.rs").to_owned() 在编译期嵌入文件文本。文件内容是 ferris，没有尾随换行。扩展名不影响，宏不把文件当 Rust 解析。
线程名那条：thread::Builder::new().name("ferris".to_owned())，再在子线程里读 current().name()。子进程那条：同一个可执行文件带 --child 时 print!("ferris")，父进程用 Command 取 stdout，再 String::from_utf8。
浮点那条用 f64::from_bits(0x0000_7369_7272_6566)。这组位按小端字节读是 f e r r i s 加两个 0。to_le_bytes() 后再丢掉两个填充字节。String::from_raw_parts 那条先 Box::new(*b"ferris")，Box::into_raw 交出分配，再以指针、长度 6、容量 6 组装。type_name::<ferris>() 取类型名的最后一段，再 parse::<String>()。作者写，type_name 没有稳定的命名约定。
panic 那条用 panic_any(format!("ferris"))，catch_unwind 之后 downcast::<String>()。这依赖 unwind。panic = "abort" 时进程会直接退出。
格式化填充那条用空字符串和填充说明符：format!("{0:f>1}{0:e>1}{0:r>2}{0:i>1}{0:s>1}", "")。> 右对齐，前面的字符是填充，数字是最小宽度。r>2 用同一个空参数填出两个 r。
somebodddy 的评论有 23 分，指出线程那条里 "ferris".to_owned() 已经造出了 String。作者回复同意。SuplenC 的评论有 7 分，写自己在 RustLab 现场看了这场演讲。
原文链接：https://endler.dev/2026/wrong-ways-to-create-strings/
compile_fail 抓住了多出来的 Display
这是 TroutWindlass 发在 r/rust 的一篇工作记录。作者维护一个内部 crate，给几个服务处理凭据。采集时 47 分、9 条评论。帖子时间是 2026-11-05 21:18 UTC。
crate 里有 Secret<T>。它故意不实现 Display。值可以传递，需要时显式取出。Debug 给出打码后的表示。format!("{}", secret) 不能把原始秘密写进日志。
作者先前加了一个 compile_fail doctest，要求用 Display 格式化 Secret 时编译失败。上周有人整理格式化代码，加了一个泛型 Display 实现。普通单元测试通过了。这个 doctest 失败了，因为那段代码现在能编译。编译器按新的实现接受了 API 原本要拒绝的写法。
作者写，compile_fail 不完美。片段可以因为无关原因编译失败。他们把否定测试和正例配在一起，也在看更精确的 UI 测试。作者写，加一个 trait 实现通常是把 API 变宽。这次它去掉了设计里的一条限制。
Tomato7550 的评论有 40 分，建议直接实现一个写出 [redacted] 的 Display，再断言这个行为。WormRabbit 的评论有 6 分，提到 static_assertions::assert_not_impl_any!。
原文链接：https://www.reddit.com/r/rust/comments/1xoulve/the_best_regression_test_we_added_this_year/
指针来源记录所属分配
这是一篇对照 Rust 和 C++ 指针来源（provenance）的说明。作者 Sofiabelen15 2026 年 11 月 5 日发到 r/rust，采集时 41 分、4 条评论。
来源记录的是指针属于哪一次分配、因此可以碰到哪块内存。它是编译器里的抽象，不作为字段跟地址存在一起。CHERI 是例外。文章用一段 C++ 说明这件事：opaque 只有前向声明，f 里 int x = 1，调用 opaque(p) 后 return x。Clang -O2 把它收成直接返回 1。编译器认为 p 不能等于 &x，因为 p 不是从 x 派生出来的。LLVM IR 里，%2 是 x 的分配根。根不同，经 %0 写入就不会改 %2。
把 &x 转成 uintptr_t 再传出去，地址就被暴露。编译器必须假设别人能从整数把指针造回来，于是放弃这个优化。
Rust 的 ptr::addr 读出地址数字，并声明不会把它铸回有效指针，因此不暴露来源。作者用对应实验看生成的代码，opaque(p) 之后仍有 mov eax, dword ptr [rsp + 12]，也就是重新加载 x。这一步优化目前同样被放弃。
带标志位的指针用 with_addr 保留来源、只换地址：let tagged: *const u32 = p.with_addr(p.addr() | 1)，清掉最低位再用 with_addr 恢复。p.addr() | 1 对 u32 未对齐，tagged 不能解引用，解引用是未定义行为。旧写法 p as usize 再铸回 *const u32 能跑，但 Miri 会警告 integer-to-pointer cast，并指向 ptr::with_exposed_provenance。警告写，这种语义下 Miri 可能漏掉指针错误。严格来源 API 对应 MIRIFLAGS=-Zmiri-strict-provenance。p as usize 会暴露 p 的来源；重建的指针如果还落在同一次分配上，来源可以恢复。落到另一次分配上，来源就丢了。
Shnatsel 的评论有 34 分，附上了 Ralf Jung 关于指针和来源的几篇文章。
原文链接：https://sofiabelen.github.io/projects/pointer-provenance-in-rust-vs-cpp/
From Rust中文社区 Mike
社区学习交流平台订阅：
评论区
写评论还没有评论