connections 0.1.0 – Galois‑connection に基づく Rust 用数値キャスト

connections 0.1.0 – Galois‑connection に基づく Rust 用数値キャスト

TL;DR – クレートの機能と重要性

connections 0.1.0 は、Galois 法則を満たす単調関数のペアをパッケージ化した Conn 型を提供します。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 といった双方向ヘルパーを可能にします。

このクレートは unsafe コードを禁止し、すべての Conn を Copy かつ const で構築可能にし、最小 MSRV を 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、同型ファミリについては、全ビット幅領域 に対する Galois 述語を証明する Kani ハーネスを提供します。浮動小数点の証明は f64 → f32 の縮小パスに限定され、すべての有限入力で ≤ 2 回のイテレーションで収束することを示します。
  • 証明コードは #[cfg(kani)] でゲートされ、通常ビルドには影響しません。

サンドイッチ不等式と隣接トリプル

単一の内部関数が upper と lower の両方を務める場合、クレートは ceil, inner, floor の 3 つの関数から ConnK マーカーを構築します。双方向ヘルパーが正しく動作するためには、サンドイッチ不等式 floor(a) ≤ ceil(a) がすべての a について成り立つ必要があります。ドキュメントでは、この不等式と inner が 順序反映 であることの同値性を証明しています。

側面ごとの Galois 法則は成り立つがサンドイッチ不等式が失敗する例が示され、round/truncate が誤動作することが説明されています。これがクレートが 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