Galois Connections for Composable Numeric Casts in Rust

This crate is a native Rust implementation of the Haskell connections library. It provides a framework for performing lawful numeric type conversions, allowing developers to build "ladders" of casts where the round-trip behavior is governed by strict mathematical inequalities rather than unpredictable implicit behavior.

Why Use This Crate?

When converting between partially ordered types (such as f64 $\to$ f32 or Duration $\to$ seconds), standard Rust tools like as, From, and Into are often insufficient:

• They typically only provide a single direction of conversion.
• The as keyword is silent opaque regarding saturation, rounding, and precision loss.

connections solves this by using Galois connections, ensuring that every link in a conversion chain is specifiable at compile time.

Key Advantages

The Mathematical Foundation

A Galois connection between two preorders $A$ and $B$ consists of two monotone maps, $f: A \to B$ and $g: B \to A$, defined by the property:

$f(x) \le y \iff x \le g(y)$

In this relationship:

• $f$ is the left (lower) adjoint.
• $g$ is the right (upper) adjoint.

Visualizing the Connection

The following diagram illustrates the relationship between two sets where arrows represent the mapping of elements through $f$ and $g$.

(Note: In a true adjoint pair, the "lens" effect—where $f(2) \leftrightarrow g(1)$—creates a non-crossing geometric signature of adjointness.)

Technical Implementation & Verification

Every operation derived from a Conn (such as median, saturation, or rounding) is backed by a property-tested invariant. Specifically, the crate ensures:

• Left-Galois Law: $\text{ceil}(a) \le b \iff a \le \text{upper}(b)$
• Right-Galois Law: $\text{lower}(b) \le a \iff b \le \text{floor}(a)$

Verification Suite

• Property Testing: All connections are validated against the laws above.
• SMT Proofs: Using Kani, full bit-width proofs are provided for:
  • Fixed-width integers
  • Q-format numbers
  • NonZero types
  • iso families
• Float SMT: Coverage is currently narrower (see Testing $\to$ SMT verification in docs).

Quick Start

use connections::{conn::ConnR, core::u32::U032I032};

// Unlike `as`, which just keeps low bits, this Conn makes saturation explicit.
let my_conn = U032I032; 

// The reverse arm is paired with `floor` via the right-Galois law.
let val = my_conn.floor(u32::MAX, i32::MAX); 
let low = my_conn.lower(-1, 0_u32);

Usage Guidelines

To maximize the benefits of the Conn algebra, follow these heuristics:

1. Avoid Early Destructuring

A Conn is a "black box." If you call upper or floor too early, you produce a concrete value and lose the ability to compose.

Pro Tip: Use higher-arity helpers like ceil2(t, h, b1, b2). This performs the operation $f(h(g(b1), g(b2)))$, embedding values into a higher-fidelity domain via $g$, processing them with closure $h$, and rounding back via $f$. This prevents overflow in the original type.

2. Architecture Recommendations

• Library Level: Export Conn types. Use the ConnL / ConnR / ConnK APIs instead of traditional getter/setter functions.
• Call Site: Use compose!, compose_l, compose_r, or compose_k to build multi-hop conversions statically.
• Runtime Params: If a conversion depends on a runtime variable, wrap the logic in a named function that visibly composes the necessary lawful Conns.

Versioning and MSRV

The crate follows a specific policy regarding the Minimum Supported Rust Version (MSRV):

• MSRV bumps are treated as minor-version changes.
• If you pin connections = "0.1", an MSRV upgrade will trigger a 0.2 release rather than a silent breaking change in a patch update.

---

Reference Image: