在这里或在 docs.rs 上阅读文档。概览 伽罗华连接作为一等公民 Rust 值。使用它们在数字类型之间合法地进行转换，并组合转换梯子的回程行为由简单的不等式决定，而非任由运气。每个从 Conn 派生的操作（舍入、饱和、中位数等）都带有经过属性测试的恒量。生成的定宽整数、Q 格式、非零和等距族也具有 Kani 驱动程序，进行全面的位宽 SMT 证明；浮动 SMT 覆盖较窄，并在测试 → SMT 验证 下被特别指出。MSRV: Rust 1.88。对 MSRV 的提升将被视为次要版本更改——固定连接 = "0.1"，而 MSRV 升级将会作为 0.2 版本而非在补丁更新中静默破坏。本 crate 是 Haskell 库 connections 的 Rust 本地移植。为什么需要这个 crate 伽罗华连接是静态的、合法的部分有序类型之间转换的正确形状（例如 f64 → f32，Duration → 秒，f32 → u32 → IpAddr，等），其中链中的每个连接都可以在编译时指定。标准转换运算符如 as、From 和 Into 一次仅提供一个方向——而特别是在舍入、饱和和有损转换方面是沈默的。这个 crate 提供的两个具体事物是标准工具所没有的：清晰的语义。(x as f32) as f64 != x 对于许多 x: f64。使用 Conn 时，该 crate 中每个连接的以下不等式对都经过属性测试：左伽罗华：ceil(a) ≤ b 当且仅当 a ≤ upper(b) 右伽罗华：lower(b) ≤ a 当且仅当 b ≤ floor(a) Conn 是 Copy、const 可构造的、无需堆，并且库使用 #![forbid(unsafe_code)]。安全可组合的。compose! 宏在编译时将一系列成对的 Conns 折叠为一个新的 Conn<Src, Dst>。通过构造，组合的 Conn 遵循其组成连接相同的属性。快速入门 使用 connections::conn::ConnR；使用 connections::core::u032::U032I032；// Rust 的 `as` 保持低位；这个 Conn 显示饱和。assert_eq!(u32::MAX as i32, -1); assert_eq!(U032I032.floor(u32::MAX), i32::MAX); // 反向臂与 `floor` 通过右伽罗华法则成对。assert_eq!(U032I032.lower(-1), 0_u32); 查看 EXAMPLES.md，了解各个领域的十个示例系列。什么是连接？在预序 A 和 B 之间的伽罗华连接是一对单调映射 f: A → B 和 g: B → A，使得 f(x) ≤ y ⇔ x ≤ g(y)。我们称 f 为左或下伴随，g 为右或上伴随的连接。以下是两个 3 元素集合之间的简单连接： (图片由 7 Sketches in Compositionality 提供)。每一行是一个 (a, b) 对；箭头显示 f 的作用(A → B，底部图例)和 g 的作用(B → A，顶部图例)。孤箭标记单向映射 (f(1) = 1, g(2) = 2)；↔ 标记一对匹配对，其中两个伴随一致 (f(3) = 3, g(3) = 3)；相邻的 ↰ ↳ 字形描绘了透镜 f(2) ↔ g(1)——在 2 行和 1 行之间的两个不交曲线，伴随关系的几何特征。如何使用连接 伽罗华连接可以组合：（f₁ ⊣ g₁）∘（f₂ ⊣ g₂）再次是一个伴随，compose! 静态构建该复合，并作为一个整体进行合法检查。当你应用一个析构函数（例如 upper、lower、ceil、floor 等）时，你已经离开了 Conn 代数，并产生了一个不再可以组合的具体值。因此，过早的析构消除了本应享有的完整链的静态保证。因此，如果你遵循两个启发式，你将获得最大的收益。通过 Conn 提升。Conn 是一个小黑盒子：高阶助手（例如 ceil*、floor*、round*、truncate* 等）接受你的参数，在 Conn 的其他（通常是更高保真度）领域内做些事情，然后把结果返回到你原始的领域。ceil2(t, h, b1, b2) 是 f(h(g(b1), g(b2)))：通过 g 将 b1 / b2 嵌入到更宽的领域，运行那里闭包 h，通过 f 进行舍入。对于会溢出或在你自己的类型中失去精度的领域算术使用这一方法——在更广阔的领域中进行，并通过舍入返回。绝不要自行处理饱和数学。在站点组合。在库层面导出 Conns，并使用 ConnL / ConnR / ConnK API，而不是 get/set 函数。当客户端代码需要多次转换时，使用 compose 宏（compose、compose_l、compose_r、compose_k）在调用站点静态构建精确的 Conn。不要手动发送中间体。如果客户端代码需要运行时参数，则最好将助手保持为一个常规命名函数，其主体明显与其依赖的合法 Conns 进行组合。将运行时参数和转换策略选择推近静态 Conn 调用点的原则意味着策略和静态转换在同一主体中都是可见的。结果是可见正确、易于测试、可扩展到未来用例的代码。库 L & R 种类 conn