connections 0.1.0 – Galois‑connection based numeric casts for Rust

connections 0.1.0 – Galois‑connection based numeric casts for Rust

TL;DR – What the crate does and why it matters

connections 0.1.0 provides a Conn type that packages a pair of monotone functions satisfying a Galois law. Using Conn you get clear, round‑trip semantics for numeric casts (e.g. saturation, rounding) and compile‑time composability of multi‑step conversions, with property‑tested invariants and optional SMT proofs.

Galois connections as first‑class Rust values

A Galois connection between preorders A and B is a pair of monotone maps f : A → B and g : B → A such that

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

connections encodes this pair in the struct

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) exposes .ceil() and .upper().
  • R‑kind (ConnR) exposes .floor() and .lower().
  • ConnK is a zero‑size marker that implements both sides, enabling two‑sided helpers like round, truncate, and interval.

The crate forbids unsafe code, makes every Conn Copy and const‑constructible, and ships with a minimal MSRV of Rust 1.88.

Why standard casts are insufficient

  • The built‑in as cast gives a single direction and silently chooses a rounding/saturation policy. For example, u32::MAX as i32 wraps to -1.
  • From/Into also provide only one direction and do not expose the reverse operation.
  • Consequently, when several casts are chained, the overall round‑trip behavior is hard to reason about.

connections solves this by making the pair of adjoint functions explicit and property‑tested:

  • Clear semantics – each Conn guarantees the left‑Galois inequality ceil(a) ≤ b ⇔ a ≤ upper(b) or the right‑Galois inequality lower(b) ≤ a ⇔ b ≤ floor(a).
  • Safe composition – the compose! macro folds a chain of Conns into a single Conn at compile time, preserving the Galois law automatically.

Quick example

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

// Rust's `as` keeps low bits and wraps:
assert_eq!(u32::MAX as i32, -1);

// The same conversion via a Conn saturates explicitly:
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);

// The reverse adjoint is `lower`:
assert_eq!(U032I032.lower(-1), 0_u32);

The example demonstrates that the Conn makes the saturation policy visible and pairs it with a mathematically dual operation.

Composition API

The macro compose! (and its variants compose_l, compose_r, compose_k) builds a composite Conn from a list of pairwise connections. The resulting Conn obeys the same Galois inequalities as its components by construction; no runtime checks are needed.

Best practice – Export Conn values from libraries and let callers compose them at the call site with the macro. This keeps the conversion policy and the static cast together, making the code easy to audit and test.

Library coverage

connections ships a large family of ready‑made connections, each generated from monotone functions that satisfy the required inequalities:

Domain Module Example connections
IEEE‑754 floats float F064F032 (f64 → f32)
Fixed‑point Q‑format fixed (feature) Q008Q000 etc.
Standard integers core widening/narrowing pairs like U032I032
NonZero wrappers core NonZeroU32 ↔ u32
Byte orderings core U008BE01, U008LE01
IP address conversions addr U032IPV4, U128IPV6
char codepoints core::char U032CHAR
std::time::Duration family time (feature) SDURU064, F064SDUR
High‑precision time (hifitime) hifi (feature) HDURNANO, ETAINANO
Hybrid logical clocks uhlc (feature) NDURU064, HLIDLX16

All core connections are heap‑free, Copy, and const. Optional features (fixed, time, hifi, uhlc, f16, try_trait) add extra families without pulling runtime dependencies.

Formal verification

  • Proptest law suite – Every connection runs a comprehensive set of property tests covering the Galois laws, closure, kernel, monotonicity, and idempotence. Float generators bias toward NaN, infinities, denormals, and ULP boundaries.
  • Kani SMT proofs – For integer, Q‑format, NonZero, and iso families the crate provides Kani harnesses that prove the Galois predicates over the full bit‑width domain. Float proofs are limited to the f64 → f32 narrowing walk, showing convergence in ≤ 2 iterations for all finite inputs.
  • The proof code is gated behind #[cfg(kani)] and does not affect normal builds.

The sandwich inequality and adjoint triples

When a single inner function can serve as both upper and lower, the crate builds a ConnK marker from three functions: ceil, inner, and floor. For the two‑sided helpers to behave correctly, the sandwich inequality floor(a) ≤ ceil(a) must hold for all a. The documentation proves equivalence between this inequality and the requirement that inner be order‑reflecting.

A counterexample is given where the per‑side Galois laws hold but the sandwich inequality fails, causing round/truncate to misbehave. This illustrates why the crate enforces the inequality for ConnK connections.

Installation & usage

cargo add connections
  • MSRV – Rust 1.88 (edition 2024).
  • License – MIT.
  • Enable optional families with Cargo features, e.g. cargo add connections --features fixed,time.

Community feedback

The author’s HN comment emphasizes that connections is not a drop‑in replacement for TryFrom. Runtime‑parameterized conversions and custom policies still belong in ordinary functions; connections shines when the conversion policy is static and needs to be composed safely.

Takeaway

connections brings mathematically grounded, compile‑time composable numeric casts to Rust. By treating Galois connections as first‑class values, it makes rounding, saturation, and round‑trip guarantees explicit, provable, and reusable across a wide range of numeric and time domains.

Sources