GoKawiilRead the docs here or on docs.rs.
Overview
Galois connections as first-class Rust values. Use them to cast lawfully between numeric types, and compose ladders of conversions whose round-trip behavior is determined by simple inequalities rather than left to chance. Every operation derived from a Conn (rounding, saturation, median, ...) carries a property-tested invariant. The generated fixed-width integer, Q-format, NonZero, and iso families also have Kani harnesses for full bit-width SMT proofs; float SMT coverage is narrower and called out under Testing → SMT verification.
MSRV: Rust 1.88. Bumps to the MSRV will be treated as minor-version changes — pin connections = "0.1" and an MSRV upgrade will surface as a 0.2 release rather than a silent break on a patch update.
This crate is a Rust-native port of the Haskell library connections .
Why this crate
Galois connections are the right shape for static, lawful conversions between partially ordered types (e.g. f64 → f32 , Duration → seconds , f32 → u32 → IpAddr , etc) where each link in the chain is specifiable at compile time.
The standard cast operators as , From , and Into give you exactly one direction at a time — and as in particular is silent on rounding, saturation, and lossy conversion. Two concrete things this crate gives you that the standard tools don't:
Clear semantics. (x as f32) as f64 != x for many x: f64 . With a Conn , at least one of the following pairs of inequalities is property-tested for every connection in this crate: left-Galois: ceil(a) ≤ b iff a ≤ upper(b)
right-Galois: lower(b) ≤ a iff b ≤ floor(a) A Conn is Copy , const -constructible, heap-free, and the crate is #![forbid(unsafe_code)] . Safely composable. The compose! macro folds a chain of pairwise Conns into one fresh Conn<Src, Dst> at compile time. A composed Conn obeys the same properties as its component connections by construction.
... continue reading