cmk/connections 源代码： https://github.com/cmk/connections crates.io (https://crates.io/crates/connections) docs.rs (https://docs.rs/connections) 文档 (https://cmk.github.io/connections/) MSRV (https://github.com/cmk/connections) CI (https://github.com/cmk/connections/actions/workflows/ci.yml) 在此处阅读文档 (https://cmk.github.io/connections/) 或访问 docs.rs (https://docs.rs/connections)。

概述

将 Galois 连接作为 Rust 中的一等公民值使用。利用它们在数值类型之间进行合法的转换，并组合转换阶梯，使其往返行为由简单不等式决定，而非听天由命。每个从 Conn 派生的操作（舍入、饱和、中位数等）都携带一个经过属性测试的不变量。生成的定宽整数、Q 格式、NonZero 和 iso 系列还包含 Kani 工具链，用于完整的位宽 SMT 证明；浮点数的 SMT 覆盖范围较窄，在 测试 → SMT 验证 中会特别说明。

MSRV：Rust 1.88。 MSRV 的升级将被视为次版本变更——锁定 connections = "0.1"，MSRV 升级将表现为 0.2 版本发布，而非在补丁更新中静默破坏。

本 crate 是 Haskell 库 connections (https://github.com/cmk/connections-haskell) 的 Rust 原生移植。

为什么使用这个 crate

Galois 连接是偏序类型之间进行静态、合规转换的合适形状（例如 f64 → f32、Duration → seconds、f32 → u32 → IpAddr 等），其中链中的每个环节在编译时即可指定。标准转换操作符 as、From 和 Into 一次只提供一个方向——而 as 在舍入、饱和和有损转换方面尤其沉默。本 crate 提供的两个具体优势是标准工具所不具备的：

1. 清晰的语义。 对于许多 x: f64 来说，(x as f32) as f64 != x。使用 Conn 时，本 crate 中每个连接的以下不等式对中至少有一对经过了属性测试：

   • 左-Galois：ceil(a) ≤ b iff a ≤ upper(b)
   • 右-Galois：lower(b) ≤ a iff b ≤ floor(a) 一个 Conn 是 Copy、const 可构造、无堆分配，并且本 crate 是 #![forbid(unsafe_code)] 的。

2. 安全可组合。 compose! 宏在编译时将一对对 Conn 的链折叠成一个全新的 Conn。组合后的 Conn 自动遵循与其组成连接相同的属性。

快速入门

use connections::conn::ConnR;
use connections::core::u032::U032I032;

// Rust 的 `as` 保留低位；此 Conn 显式进行饱和处理。
assert_eq!(u32::MAX as i32, -1);
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);

// 根据右-Galois 定律，反向臂与 `floor` 配对。
assert_eq!(U032I032.lower(-1), 0_u32);

参见 EXAMPLES.md (https://github.com/cmk/connections/blob/main/EXAMPLES.md) 了解十个在不同领域中的完整示例。

什么是连接？

一个在预序集 A 和 B 之间的 Galois 连接 (https://en.wikipedia.org/wiki/Galois_connection) 是一对单调映射 f: A → B 和 g: B → A，满足 f(x) ≤ y ⇔ x ≤ g(y)。我们称 f 为连接的左伴随或下伴随，g 为连接的右伴随或上伴随。

下面是一个两个三元素集合之间的简单连接： （图片致谢《7 Sketches in Compositionality》(https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf)）。每一行是一个 (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 行之间的两条不相交曲线，这是伴随性的几何特征。

如何使用连接

Galois 连接可组合：(f1 ⊣ g1) ∘ (f2 ⊣ g2) 仍然是一个伴随对，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 舍入回来。用于那些在你自己的类型中会溢出或丢失精度的领域算术——在更宽的领域中执行并舍回。永远不要手动实现饱和算术。

在调用处组合。 在库级别导出 Conn，使用 ConnL/ConnR/ConnK API 而非 get/set 函数。当客户端代码需要多跳转换时，使用组合宏（compose、compose_l、compose_r、compose_k）在调用处静态构建确切的 Conn。不要手动串联中间结果。如果客户端代码接受运行时参数，那么最好将辅助函数保留为一个普通的命名函数，其函数体显式地组合它所依赖的合法 Conn。将运行时参数和转换策略选择推近静态 Conn 调用处的纪律意味着策略和静态转换都在同一个函数体中可见。这样代码既直观正确，又易于测试，并且可扩展到未来用例。

库

L 和 R 类连接

本库中的基本类型是：

pub struct Conn<A, B, K> {
    f: fn(A) -> B,   // L 类: ceil; R 类: floor
    g: fn(B) -> A,   // L 类: upper; R 类: lower
    // 加上一个幻影类型标签 K ∈ {L, R}
}

一个 Conn 恰好就是一个 Galois 连接——一对单调函数 (f, g)，其伴随角色取决于类型标签。L 类 Conn 满足 f(a) ≤ b ⟺ a ≤ g(b)；R 类 Conn 满足 g(b) ≤ a ⟺ b ≤ f(a)。类型 K = {L, R} 决定了 API。L/ConnL 暴露 .ceil() 和 .upper()，而 R/ConnR 暴露 .floor() 和 .lower()。

• 方向名称 —— ceil（向上取整）和 floor（向下取整）—— 符合下游直觉。“给我一个向上取整的转换”不需要调用者知道自己处于伴随的哪一侧。然而，在 L 类连接上调用 .floor() 或在 R 类连接上调用 ceil 会导致编译错误。
• 位置名称 —— upper（L 对的上伴随）和 lower（R 对的下伴随）—— 符合数学含义：泛型的 T: ConnK 绑定会暴露两者，因为三元组同时具有两个伴随关系，无论具体实例中每个方向如何取整。
• 常量 vs 标记 —— 常规连接是 pub const 的类型 Conn<A, B, L> 或 Conn<A, B, R>。双面 ConnK 连接以 pub struct 形式提供——零大小的标记类型，同时实现 ConnL 和 ConnR。常量 vs 结构体的形式一眼就能告诉你名称所指的种类。

API

• L 端方法，定义在 Conn<_, _, L> 上（以及通过默认方法分派到任何 ConnL 实现者）：ceil、upper，以及 ceil1/2、upper1/2 提升器。
• R 端方法，定义在 Conn<_, _, R> 上（以及通过默认方法分派到任何 ConnR 实现者）：floor、lower，以及 floor1/2、lower1/2 提升器。
• 双面辅助函数（在 crate 根处重新导出）：interval、round/round1/round2、truncate/truncate1/truncate2、median。所有这些都绑定在 T: ConnK 上（ConnL + ConnR 的父 trait，作用于相同的 (A, B)），因此只能在三元组标记上调用——不能用于单面 Conn。类别的纪律是结构化的：在 L 类 Conn 上调用 .floor(...) 是编译错误（该方法只存在于 Conn<_, _, R> 上），类似地，在 R 类上调用 .ceil(...) 也是编译错误。双面辅助函数同样会在编译时拒绝单面操作数，因为单面 Conn 不实现 ConnK。

模块

常量名称前缀通过字母区分：Q 表示 Q 格式包装器（符号和主机位宽来自模块路径），I/U 表示标准整数原语（数字 = 位宽），N 表示 NonZero<*>，F 表示 IEEE 浮点数。允许跨模块名称冲突，通过限定导入解决（例如 fixed::i008::Q008Q000 和 fixed::i064::Q008Q000 可共存）。

ConnK 连接

当同一个 inner 函数既可以作为 upper 又可以作为 lower，并且满足一个额外的序反射性质（参见 夹层不等式）时，库会将两个结果连接合并成一个零大小的标记结构体，该结构体通过一个将 L 和 R 两侧联系起来的父 trait，获得第三组“两用”辅助函数：

• ConnL —— 能力 trait，包含关联类型 type A: Copy; type B: Copy; 和一个 conn_l() 投影到 L 视图 Conn。默认方法暴露 .ceil() 和 .upper()。
• ConnR —— 对称的能力 trait，其 conn_r() 投影到 R 视图 Conn。默认方法暴露 .floor() 和 .lower()。
• ConnK —— 父 trait ConnL + ConnR，作用于相同的 (A, B) 对；双面辅助函数（round、truncate、…）绑定在 ConnK 上，并访问两个视图。

trait 名称有意与值类型拼写匹配：一个 blanket impl ConnL for Conn<A, B, L>（以及 R 端类似实现）使得每个单面值也满足 trait，因此泛型 T: ConnL 绑定可以统一接受三元组标记和原始 Conn 值，而 inner 被定义为模块作用域中的自由函数，从标记的 trait 实现中引用；crate 中没有结构体存储三个函数指针。

伴随三元组

你使用 crate 提供的某一个宏，通过三个函数 ceil、inner 和 floor 构建一个 ConnK 标记。注意，ceil/inner 和 inner/floor 都必须满足上面给出的连接不等式。此外，ceil/floor 必须满足下面的“夹层”不等式：对于每个 a，floor(a) ≤ ceil(a)

满足所有三个性质的三元组 ceil/inner/floor 被称为伴随三元组 (https://ncatlab.org/nlab/show/adjoint+triple) —— 即示例 3 (https://github.com/cmk/connections/blob/main/EXAMPLES.md#example-3) 中概述的 ceil ⊣ inner ⊣ floor 形状。夹层不等式等价于之前要求的 inner 是序反射的 (https://en.wikipedia.org/wiki/Order_theory#Functions_between_orders)。prop::conn::law_battery! 的 full 子集同时强制执行 floor_le_ceil 和 order_reflecting：

等价性的证明在以下章节中概述。

夹层不等式

等价性的两个方向都来自伴随律的应用。两个证明仅使用 L-Galois f ⊣ g、R-Galois g ⊣ h、单调性和传递性——没有额外假设。

充分性（inner 序反射 ⟹ floor(a) ≤ ceil(a)）。取任意 a ∈ A。两个闭包律给出：

inner(floor(a)) ≤ a ≤ inner(ceil(a))

因此由传递性得 inner(floor(a)) ≤ inner(ceil(a))。由于 inner 是序反射的，这提升为 floor(a) ≤ ceil(a)。∎

必要性（处处 floor(a) ≤ ceil(a) ⟹ inner 序反射）。取 x, y ∈ B，满足 inner(x) ≤ inner(y)。链式推导：

x ≤ floor(inner(x))          -- inner ⊣ floor 的核，b = x
  ≤ ceil(inner(x))           -- 假设，a = inner(x)
  ≤ y                        -- L-Galois ceil(a) ≤ b ⟺ a ≤ inner(b)，其中 a = inner(x), b = y；RHS inner(x) ≤ inner(y) 已知

所以 x ≤ y。∎

（范畴论角度：在偏序集上的伴随三元组 f ⊣ g ⊣ h 中，g 完全忠实 ⟺ g ⊣ h 的余单位是同构 ⟺ f ⊣ g 的单位是同构 ⟺ h ≤ f。上面两个展示就是将该等价关系写成了偏序集的形式，其中“完全忠实”简化为“序反射”，“同构”简化为“相等”。）

反例 —— 必要性是严格的。令 A = {a}（一个元素），B = {b1 < b2 < b3}，inner: B → A 是常数映射（对于每个 b，inner(b) = a —— 单调但极其非单射）。看看每侧 Galois 律强制了什么：

• L-Galois ceil(a) ≤ b ⟺ a ≤ inner(b)。RHS 简化为 a ≤ a，永远为真，所以对于每个 b ∈ B 都有 ceil(a) ≤ b。最小的这样的 b 是 b1，因此 ceil(a) = b1。
• R-Galois inner(b) ≤ a ⟺ b ≤ floor(a)。LHS 简化为 a ≤ a，永远为真，所以对于每个 b 都有 b ≤ floor(a)，得到 floor(a) = b3。

两侧的伴随关系都成立，所有单调性检查通过——然而 floor(a) = b3 > b1 = ceil(a)。“三元组”类型检查通过，每侧律满足，但舍入夹层是颠倒的。双面辅助函数继承了颠倒性。round(a) 比较 inner(floor(a)) = a 和 inner(ceil(a)) = a 以选择更近的端点，发现它们相等，然后回退到 truncate，后者根据源零规则返回任一侧的值——这个值没有任何带内信号表明出了问题。

一个不满足夹层不等式的连接并非学术上的失误；双面辅助函数会在其上表现异常。

安装

cargo add connections

可选的 cargo 特性：