Read the docs here.

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. Three concrete things this crate gives you that the standard tools don't:

1. 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)].

2. 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.

Quick start

use connections::prelude::*;
use connections::core::B2;
use connections::core::i016::I016BE02;

let bytes = B2([0x01, 0x02]);
assert_eq!(I016BE02.ceil(258_i16), bytes);
assert_eq!(I016BE02.floor(258_i16), bytes);
assert_eq!(I016BE02.upper(bytes), 258_i16);
assert_eq!(I016BE02.lower(bytes), 258_i16);

See EXAMPLES.md for a sequence of ten worked examples in various domains.

What are connections?

A Galois connection between preorders A and B is a pair of monotone maps f: A → B and g: B → A such that f(x) ≤ y ⇔ x ≤ g(y). We say f is the left or lower adjoint, and g is the right or upper adjoint of the connection.

Here is a simple connection between two 3-element sets:

(image courtesy of 7 Sketches in Compositionality).

Each row is a (a, b) pair; arrows show the action of f (A → B, bottom legend) and g (B → A, top legend). Lone arrows mark single-direction maps (f(1) = 1, g(2) = 2); the ↔ marks a matched pair where both adjoints agree (f(3) = 3, g(3) = 3); the adjacent ↰ ↳ glyphs depict the lens f(2) ↔ g(1) — two non-crossing curves between rows 2 and 1, the geometric signature of adjointness.

How to use connections

Galois connections compose: (f₁ ⊣ g₁) ∘ (f₂ ⊣ g₂) is again an adjunction, and compose! builds that composite statically, law-checked as a whole. The moment you apply a destructor (e.g. upper , lower, ceil, floor, etc) you've left the Conn algebra and produced a concrete value that can no longer be composed. So early destructuring throws away the static guarantees that the full chain would have otherwise enjoyed. Therefore you will get the most bang for your buck if you follow two heuristics.

Lift through the Conn. A Conn is a little black box: the higher- arity helpers (e.g. ceil*, floor*, round*, truncate*, etc) take your arguments, do something with them in the Conn's other (usually higher-fidelity) domain, and return the result back in your original domain. ceil2(t, h, b1, b2) is f(h(g(b1), g(b2))): embed b1/b2 into the wider domain via g, run the closure h there, round back via f. Use this for domain arithmetic that would overflow or lose precision in your own type - do it in the wider domain and round back. Never hand-roll saturating math.

Compose at the site. Export Conns at the library level and use the ConnL/ConnR/ConnK API instead of get/set functions. When client code needs a multi-hop conversion, build the exact Conn with the compose macros (compose, compose_l, compose_r, compose_k) statically at the call site. Do not thread intermediates by hand. If the client code takes a runtime parameter then it's best to keep the helper as a normal named function whose body visibly composes with the lawful Conns it depends on.

The discipline of pushing runtime parameters and conversion policy choices close to the static Conn call site means that the policy and the static cast are both visible in the same body. The results is code that is visibly correct, easy to test, and extensible to future use cases.

Library

L & R kind connections

The basic type in this library is:

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
    // plus a phantom kind tag K ∈ {L, R}
}

A Conn<A, B, K> is exactly a Galois connection — a pair of monotone functions (f, g) whose adjoint role depends on the kind tag. An L-kind Conn satisfies f(a) ≤ b ⟺ a ≤ g(b); an R-kind Conn satisfies g(b) ≤ a ⟺ b ≤ f(a).

The kind K = {L, R} determines the API. L/ConnL exposes .ceil() and .upper(), while R/ConnR exposes .floor() and .lower().

• Direction names — ceil (rounds up) and floor (rounds down) — match downstream intuition. "Give me a ceiling cast" doesn't require the caller to know which side of an adjunction they're on. However calling .floor() on an L-kind connection, or ceil on an R-kind connection results in a compiler error.
• Position names — upper (the upper adjoint of the L-pair) and lower (the lower adjoint of the R-pair) — match the math: a generic T: ConnK bound exposes both because a triple has both adjunctions, regardless of which way each one rounds in any concrete instance.
• Consts vs markers - Regular connections are pub consts of type Conn<A, B, L> or Conn<A, B, R>. Two-sided ConnK connections ship as pub structs — zero-sized marker types implementing both ConnL and ConnR. The const-vs-struct shape tells you which kind a name refers to at a glance.

API

• L-side methods on Conn<_, _, L> (and on any ConnL implementor via default-method dispatch): ceil, upper, plus ceil1/2, upper1/2 lifters.
• R-side methods on Conn<_, _, R> (and on any ConnR implementor): floor, lower, plus floor1/2, lower1/2 lifters.
• Two-sided helpers (re-exported at the crate root): interval, round/round1/round2, truncate/truncate1/truncate2, median. All bind on T: ConnK (super-trait of ConnL + ConnR over the same (A, B)), so they're callable only on triple markers — not on one-sided Conns.

Kind discipline is structural: calling .floor(...) on an L-kind Conn is a compile error (the method only exists on Conn<_, _, R>), and likewise .ceil(...) on R. Two-sided helpers similarly reject one-sided operands at compile time because a one-sided Conn doesn't implement ConnK.

Modules

Constant-name prefixes are letter-disambiguated: Q for Q-format wrappers (sign and host bit-width come from the module path), I/U for std primitives (digits = bit-width), N for NonZero<*>, F for IEEE floats. Cross-module name collisions are allowed and resolved by qualified import (e.g. fixed::i008::Q008Q000 and fixed::i064::Q008Q000 co-exist).

ConnK connections

When the same inner function can serve as both upper and lower and satisfies an additional order-reflecting property (see Sandwich inequality), the library combines the two resulting connections into a zero-sized marker struct that gains a third group of 'ambidextrous' helpers via a super-trait that ties the L and R sides together:

• ConnL — capability trait with associated types type A: Copy; type B: Copy; and a conn_l() projection to the L-view Conn<A, B, L>. Default methods expose .ceil() and .upper().
• ConnR — symmetric capability trait whose conn_r() projects to the R-view Conn<A, B, R>. Default methods expose .floor() and .lower().
• ConnK — super-trait ConnL + ConnR over the same (A, B) pair; the two-sided helpers (round, truncate, …) bind on ConnK and reach through both views.

The trait names match the value-type spellings on purpose: a blanket impl ConnL for Conn<A, B, L> (and the R-side analogue) makes every one-sided value also satisfy the trait, so a generic T: ConnL bound accepts triple markers and raw Conn<A, B, L> values uniformly, and inner is defined as a free function in module scope, referenced from the marker's trait impls; no struct in the crate stores three function pointers.

Adjoint triples

You construct a ConnK marker out of three functions: ceil, inner, and floor using one of the crate's provided macros. Note that both ceil/inner and inner/floor must satisfy the connection inequalities given above. In addition ceil/floor must satisfy the following 'sandwich' inequality: for every a, floor(a) ≤ ceil(a)

Triples ceil/inner/floor that satisfy all three properties are known as adjoint triples — the ceil ⊣ inner ⊣ floor shape outlined in Example 3.

The sandwich inequality is equivalent to the earlier requirement that inner be order-reflecting. The prop::conn::law_battery! full subset enforces both floor_le_ceil as well as order_reflecting:

Proof of equivalence is outlined in the following section.

Sandwich inequality

Both directions of the equivalence follow from applications of the adjunction laws. Both proofs use only L-Galois f ⊣ g, R-Galois g ⊣ h, monotonicity, and transitivity — no extra assumptions.

Sufficiency (inner order-reflecting ⟹ floor(a) ≤ ceil(a)). Take any a ∈ A. The two closure laws give

inner(floor(a)) ≤ a ≤ inner(ceil(a))

so by transitivity inner(floor(a)) ≤ inner(ceil(a)). Since inner is order-reflecting, this lifts to floor(a) ≤ ceil(a). ∎

Necessity (floor(a) ≤ ceil(a) everywhere ⟹ inner order-reflecting). Take x, y ∈ B with inner(x) ≤ inner(y). Chain:

x ≤ floor(inner(x))     -- kernel of inner ⊣ floor, with b = x
  ≤ ceil(inner(x))      -- assumption at a = inner(x)
  ≤ y                   -- L-Galois ceil(a) ≤ b ⟺ a ≤ inner(b),
                           with a = inner(x), b = y; the RHS
                           inner(x) ≤ inner(y) is given

So x ≤ y. ∎

(Categorically: in an adjoint triple f ⊣ g ⊣ h over posets, g fully faithful ⟺ the counit of g ⊣ h is iso ⟺ the unit of f ⊣ g is iso ⟺ h ≤ f. The two displays above are that equivalence written for posets, where "fully faithful" reduces to "order-reflecting" and "iso" to "equality".)

Counterexample — necessity is sharp. Let A = {a} (one element) and B = {b₁ < b₂ < b₃}, with inner: B → A the constant map (inner(b) = a for every b — monotone but maximally non-injective). Watch what the per-side Galois laws force:

• L-Galois ceil(a) ≤ b ⟺ a ≤ inner(b). The RHS reduces to a ≤ a, which is always true, so ceil(a) ≤ b for every b ∈ B. The smallest such b is b₁, so ceil(a) = b₁.
• R-Galois inner(b) ≤ a ⟺ b ≤ floor(a). The LHS reduces to a ≤ a, always true, so b ≤ floor(a) for every b, giving floor(a) = b₃.

Both per-side adjunctions hold, every monotonicity check passes — and yet floor(a) = b₃ > b₁ = ceil(a). The "triple" type-checks and the per-side laws are satisfied, but the rounding sandwich is inverted.

The two-sided helpers inherit the inversion. round(a) compares inner(floor(a)) = a with inner(ceil(a)) = a to pick the closer endpoint, finds them equal, and falls through to truncate, which returns whichever side the source-zero rule selects — a value with no in-band signal that anything is wrong. A connection that fails the sandwich inequality isn't an academic foul; the two-sided helpers actively misbehave on it.

Installation

cargo add connections

Optional cargo features:

The connections::prop::conn and connections::prop::lattice predicate modules are always public — they're pure bool-returning functions over this crate's own types and don't depend on proptest. The testing feature only adds prop::arb, the strategy module that does pull proptest in as a regular dependency.

Testing

cargo test --workspace

Every connection runs its proptest law suite on every commit (the pre-commit hook in .claude/settings.json enforces this). Float generators are biased toward NaN, ±∞, ±0, denormals, and ULP-boundary values. Fixed-point generators are biased toward 0, ±PREC, and ±i64::MAX/PREC so saturation boundaries are exercised on every run.

Runtime dependencies are feature-gated. The fixed crate backs the optional binary fixed-point ladder, time backs the optional civil-calendar / clock surface, and hifitime backs the optional high-precision time surface. Proptest is a dev-dependency, exposed publicly behind the testing feature for downstream test suites.

Every connection ships with proptest coverage of the following laws — the predicates live in prop::conn and are re-runnable by downstream crates against their own connections:

A tenth law, conn_floor_le_ceil (floor(a) ≤ ceil(a)), is asserted only on ConnK connections whose inner is an injective embedding. See above.

For float-bearing types, the ≤ is an N5 lattice. In particular, NaN is reflexive, NaN sits between ±∞, and finite values are strictly ordered. N5 carries these semantics.

SMT verification (Kani)

Beyond the proptest law suite — which samples — the generated fixed-width integer / Q-format / NonZero / iso connection families listed in src/kani.rs have Kani harnesses for their Galois-law predicates over the full bit-width domain. The pointer-width usize / isize families (core::usize / core::isize) are the exception: CBMC models a single concrete pointer width per run, so those Conns are covered by the proptest battery on the host target rather than a width-agnostic SMT proof. The proof tree lives at src/kani/ and is gated behind #[cfg(kani)] so it compiles only under cargo kani — release builds, cargo test, and downstream consumers see no proof code. No new runtime dependency: Kani injects its own crate at proof time.

The float-specific SMT result is deliberately narrower: the IEEE bit space is too large for full-Galois proofs to be tractable, so the f64 → f32 ULP-walk in src/core/f064.rs (ceil_f64_f32 / floor_f64_f32) is proven to converge in ≤ 2 iterations for every finite non-NaN f64, not just the proptest sample. Three tiered harnesses (float_walk::t0_* for the full domain, t1_* for |x| ≤ 1e6, t2_* for the [1, 2) binade) each verify the bound under progressively tighter input restrictions. These harnesses do not prove full float Galois laws over NaN/±∞, and they do not cover the float→integer or float→fixed macro helper bodies; those branches are covered by the proptest law batteries and explicit helper/unit tests.

Run with:

cargo install --locked kani-verifier
cargo kani setup
cargo kani                                   # full proof tree
cargo kani --harness 'float_walk::t0_'       # the headline
cargo kani --harness 'int_narrow::'          # one family

Per-harness wall times are in the milliseconds-to-seconds range; the full tree runs in well under two minutes.