Read 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)].
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.
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
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).
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 result 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:
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
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:
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
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 proptest feature only adds prop::arb, the strategy module that
does pull proptest in as a regular dependency.
Testing
Every connection runs its proptest law suite in CI and in the
repository's pre-push gate. 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 proptest 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:
Per-harness wall times are in the milliseconds-to-seconds range; the
full tree runs in well under two minutes.