Creusot 0.14.0：为 Rust 提供可证明的契约

📋 概述

Rust 形式化验证工具 Creusot 发布 0.14.0。文章介绍三项变化：一是自 0.13.0 起把 PartialOrd 的规范从全序放宽到偏序，改用基于布尔比较函数的经典表述（lt_log 需满足非自反与传递），全序则作为额外定律写出，有趣的是已有证明全都没受影响；二是开始为 snapshot!（嵌入 Rust 程序中的逻辑表达式）生成验证条件，这让「引理函数」可以写成逻辑函数并在 snapshot 中调用，避免了真实函数调用与借用检查器带来的样板代码，因为 snapshot 在编译时会被完全擦除；三是接入 rust-analyzer，让 Pearlite 规范里也能跳转到定义，做法是让 rust-analyzer 像 Creusot 一样展开规范宏，而它不做借用检查这一点恰好帮了忙。