The "connections" Rust crate introduces Galois connections as first-class values for composable numeric casts. This enables lawful conversions between numeric types, forming conversion ladders with predictable round-trip behavior determined by simple inequalities, unlike standard cast operators.

Every operation derived from a Conn carries a property-tested invariant. The crate includes generated fixed-width integer, Q-format, Non Zero, and iso families with Kani harnesses for SMT proofs. It is a Rust-native port of the Haskell library "connections".

Galois connections are ideal for static, lawful conversions between partially ordered types where each link is specifiable at compile time. The standard `as`, `From`, and `Into` operators lack clear semantics regarding rounding, saturation, and lossy conversions. This crate provides clear semantics and safety through composability using the `compose!` macro, which folds chains of pairwise Conns into a single, new Conn at compile time.

The core type is `Conn<A, B, K>`, representing a pair of monotone functions (f, g) with an adjoint role determined by the `Kind` tag (`L` or `R`). This kind discipline ensures that methods like `.ceil()` and `.floor()` are only available on the appropriate Conn kinds, preventing compile-time errors. Two-sided Conn K connections are zero-sized marker types implementing both `Conn L` and `Conn R`.