connections 0.1.0 – 基于 Galois‑connection 的 Rust 数值转换

connections 0.1.0 – 基于 Galois‑connection 的 Rust 数值转换

TL;DR – 这个 crate 做了什么以及为什么重要

connections 0.1.0 提供了一个 Conn 类型，用来封装满足 Galois 法则的一对单调函数。使用 Conn，你可以获得 明确的往返语义（例如饱和、四舍五入）以及 编译期可组合 的多步转换，配合属性测试的不变式和可选的 SMT 证明。

Galois 连接作为一等 Rust 值

在偏序 A 与 B 之间的 Galois 连接是一对单调映射 f : A → B 与 g : B → A，满足

f(a) ≤ b  ⇔  a ≤ g(b)

connections 在结构体中对这对函数进行编码

pub struct Conn<A, B, K: Kind = L> {
    f: fn(A) -> B,   // L‑kind: ceil; R‑kind: floor
    g: fn(B) -> A,   // L‑kind: upper; R‑kind: lower
    _kind: PhantomData<K>,
}
  • L‑kind（ConnL） 暴露 .ceil() 与 .upper()。
  • R‑kind（ConnR） 暴露 .floor() 与 .lower()。
  • ConnK 是一个零大小标记，实现了两侧功能，支持 round、truncate、interval 等双向辅助函数。

该 crate 禁止使用 unsafe 代码，使每个 Conn 都是 Copy 且可在 const 环境下构造，最低支持的 Rust 版本为 Rust 1.88。

为什么标准转换不足

  • 内置的 as 转换只能单向工作，并且会悄悄选择一种四舍五入/饱和策略。例如，u32::MAX as i32 会包装成 -1。
  • From/Into 同样只提供单向转换，且不暴露逆向操作。
  • 因此，当多个转换链式调用时，整体的往返行为难以推理。

connections 通过显式化 伴随函数对 并进行 属性测试 来解决此问题：

  • 明确的语义 – 每个 Conn 保证左侧 Galois 不等式 ceil(a) ≤ b ⇔ a ≤ upper(b) 或 右侧 Galois 不等式 lower(b) ≤ a ⇔ b ≤ floor(a)。
  • 安全的组合 – compose! 宏在编译期将一系列 Conn 折叠为单个 Conn，自动保持 Galois 法则。

快速示例

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

// Rust 的 `as` 只保留低位并会包装：
assert_eq!(u32::MAX as i32, -1);

// 同样的转换通过 Conn 明确饱和：
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);

// 逆向伴随函数是 `lower`：
assert_eq!(U032I032.lower(-1), 0_u32);

该示例展示了 Conn 如何让饱和策略可见，并与数学上的对偶操作配对。

组合 API

宏 compose!（以及其变体 compose_l、compose_r、compose_k）可以从一系列两两连接中构建复合 Conn。生成的 Conn 按构造时即满足 与其组件相同的 Galois 不等式；无需运行时检查。

最佳实践 – 从库中导出 Conn 值，让调用者在调用点使用宏进行组合。这样可以把转换策略与静态转换绑定在一起，代码更易审计和测试。

库覆盖范围

connections 提供了大量现成的连接，每个都由满足所需不等式的单调函数生成：

域 模块 示例连接
IEEE‑754 浮点数 float F064F032（f64 → f32）
定点 Q‑格式 fixed（feature） Q008Q000 等
标准整数 core 扩宽/收窄对，如 U032I032
NonZero 包装器 core NonZeroU32 ↔ u32
字节序 core U008BE01、U008LE01
IP 地址转换 addr U032IPV4、U128IPV6
char 码点 core::char U032CHAR
std::time::Duration 系列 time（feature） SDURU064、F064SDUR
高精度时间（hifitime） hifi（feature） HDURNANO、ETAINANO
混合逻辑时钟 uhlc（feature） NDURU064、HLIDLX16

所有核心连接都是 无堆、Copy 且 const。可选特性（fixed、time、hifi、uhlc、f16、try_trait）在不引入运行时依赖的情况下提供额外的族。

形式化验证

  • Proptest 法则套件 – 每个连接都会运行一套完整的属性测试，覆盖 Galois 法则、闭包、核、单调性和幂等性。浮点数生成器会偏向 NaN、无穷大、次正规数以及 ULP 边界。
  • Kani SMT 证明 – 对整数、Q‑格式、NonZero 与 iso 系列，crate 提供 Kani harness，能够在 完整 位宽域上证明 Galois 谓词。浮点数证明仅限于 f64 → f32 的收窄路径，展示所有有限输入在 ≤ 2 次迭代内收敛。
  • 证明代码通过 #[cfg(kani)] 条件编译，不影响普通构建。

三明治不等式与伴随三元组

当同一个内部函数既可以充当 upper 又可以充当 lower 时，crate 会从三个函数 ceil、inner、floor 构造一个 ConnK 标记。为了让双向辅助函数行为正确，必须对所有 a 满足 三明治不等式 floor(a) ≤ ceil(a)。文档证明了该不等式等价于 inner 为 保序反射 的要求。

文中给出一个反例：虽然每侧的 Galois 法则成立，但三明治不等式失效，导致 round/truncate 行为异常。这说明 crate 为什么要对 ConnK 连接强制该不等式。

安装与使用

cargo add connections
  • MSRV – Rust 1.88（edition 2024）。
  • 许可证 – MIT。
  • 通过 Cargo 特性启用可选族，例如 cargo add connections --features fixed,time。

社区反馈

作者在 HN 的评论中强调，connections 不是 TryFrom 的直接替代品。运行时参数化的转换和自定义策略仍应放在普通函数中；connections 在转换策略是 静态 并且需要安全组合时表现最佳。

结论

connections 为 Rust 带来了基于数学的、编译期可组合的数值转换。通过把 Galois 连接视为一等值，它使四舍五入、饱和以及往返保证变得明确、可证明并可在广泛的数值和时间域中复用。

Sources