connections 0.1.0 – 基於 Galois 連接的 Rust 數值轉換

connections 0.1.0 – 基於 Galois 連接的 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‑format fixed（功能） Q008Q000 等
標準整數 core 擴大/縮小配對，如 U032I032
NonZero 包裝 core NonZeroU32 ↔ u32
位元序 core U008BE01、U008LE01
IP 位址轉換 addr U032IPV4、U128IPV6
char 代碼點 core::char U032CHAR
std::time::Duration 系列 time（功能） SDURU064、F064SDUR
高精度時間（hifitime） hifi（功能） HDURNANO、ETAINANO
混合邏輯時鐘 uhlc（功能） NDURU064、HLIDLX16

所有核心連接皆 無堆分配、Copy 且 const。可選功能（fixed、time、hifi、uhlc、f16、try_trait）會加入額外族群，卻不會拉入執行時相依。

形式驗證

  • Proptest 法則套件 – 每個連接都會執行完整的屬性測試，涵蓋 Galois 法則、閉包、核、單調性與冪等性。浮點產生器會偏向 NaN、無限大、次正規數與 ULP 邊界。
  • Kani SMT 證明 – 對整數、Q‑format、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