Hi HN — I just published 0.1.0 of `connections`, a Rust port of an older Haskell library I wrote.
It's intended to address a common issue with casting: each cast's individual behavior is specified, but the syntax doesn’t describe what a cast and its reverse do together. Once several conversions are chained, their rounding, saturation, and range choices become difficult to reason about compositionally.
The core type packages a pair of monotone functions intended to satisfy a Galois law. A left connection, for example, has `ceil: A -> B` and `upper: B -> A`, with:
ceil(a) <= b iff a <= upper(b)
There is a right-handed `lower`/`floor` form as well. When one embedding has both adjoints, the crate exposes `round`, `truncate`, interval, and related operations.
A small example of the boundary behavior:
use connections::conn::ConnR;
use connections::core::u032::U032I032;
assert_eq!(u32::MAX as i32, -1);
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);
assert_eq!(U032I032.lower(-1), 0_u32);
Here `as` preserves the low bits and wraps to -1, while this connection saturates. The claim isn’t that saturation is universally better; it is that the choice is explicit and paired with its reverse under:
lower(b) <= a iff b <= floor(a)
The main payoff is composition. Provided the components satisfy their laws, Galois connections compose, so the compile-time composition macros preserve the relationship without inventing a new rounding policy at each hop.
0.1.0 includes families for Rust integers, IEEE floats, NonZero values, chars, sortable byte encodings, and IP/socket addresses, with optional Q-format, civil-time, hifitime, and hybrid-clock families. The default core has no third-party runtime dependencies; `Conn` is Copy, const-constructible, heap-free, and the crate forbids unsafe code.
Every included connection has a proptest law suite. Generated integer, Q-format, NonZero, and isomorphism families also have Kani harnesses over their full bit-width domains. The float claims are deliberately narrower and documented separately; floats use an N5 wrapper so NaN participates in an explicit reflexive preorder rather than being quietly excluded.
This isn’t intended to replace `TryFrom`: validation, runtime-parameterized conversions, and caller-selected policies generally belong in ordinary named functions.
In our code we use non byte numbers(deranged and arbitrary int crates), symmetric signed, ordered floats, new num type pattern, our const and categorical num traits(num-traits crate sucks), static assertions, prop tests, easy cast crate(sound as). We have custom decimals.
And newtypes of u64 * u64 = u128.
This isn’t intended to replace arbitrary validation or runtime-parameterized conversions. That said, here is some lease gating code I used a connection for recently:
// Unix i64 timestamp
pub struct LeaseSecond(i64);
pub struct LeaseWindow {
pub valid_from: LeaseSecond,
pub valid_until_exclusive: Option<LeaseSecond>,
}
pub fn window(&self) -> LeaseWindow {
// Input is guarded at several points:
// - A pre-epoch acquired_at_secs is a hostile input, not a time:
// I064U064.ceil cuts the input off at zero on the way into start,
// and the upper adjoint in to_second saturates at i64::MAX on
// the way back, so upper ∘ ceil is exactly the clamp of a raw
// time_t onto the lease-second range.
// - ttl_secs is checked for finite expiry by a sentinel guard
// - start + ttl_secs is computed in u128 to prevent wraparound
let start = I064U064.ceil(self.acquired_at_secs.get());
let to_second = |secs: u64| LeaseSecond::new(I064U064.upper(secs));
LeaseWindow {
valid_from: to_second(start),
valid_until_exclusive: self.finite_expiry(start).map(to_second),
}
}
/// Exclusive u64 expiry second or None when ttl_secs is the
/// u64::MAX "no finite expiration" sentinel.
fn finite_expiry(&self, start: u64) -> Option<u64> {
let ttl_secs = (self.ttl_secs != u64::MAX).then_some(self.ttl_secs)?;
// Lift the add through U128U064 so the sum is exact in u128.
Some(U128U064.ceil2(|lhs, rhs| lhs + rhs, start, ttl_secs))
}
The library has a number of feature-flagged crates for domain-specific types. Toggling the macros flag will also expose its internal codegen macros (e.g. uint_int_sat) so you can create your own connections fairly easily. Predicates and proptest strategies are exported from src/prop.rs. I haven't tried lean, but there is a kani test suite focused mostly on the floating point connections.
Hi HN — I just published 0.1.0 of `connections`, a Rust port of an older Haskell library I wrote.
It's intended to address a common issue with casting: each cast's individual behavior is specified, but the syntax doesn’t describe what a cast and its reverse do together. Once several conversions are chained, their rounding, saturation, and range choices become difficult to reason about compositionally.
The core type packages a pair of monotone functions intended to satisfy a Galois law. A left connection, for example, has `ceil: A -> B` and `upper: B -> A`, with:
There is a right-handed `lower`/`floor` form as well. When one embedding has both adjoints, the crate exposes `round`, `truncate`, interval, and related operations.A small example of the boundary behavior:
Here `as` preserves the low bits and wraps to -1, while this connection saturates. The claim isn’t that saturation is universally better; it is that the choice is explicit and paired with its reverse under: The main payoff is composition. Provided the components satisfy their laws, Galois connections compose, so the compile-time composition macros preserve the relationship without inventing a new rounding policy at each hop.0.1.0 includes families for Rust integers, IEEE floats, NonZero values, chars, sortable byte encodings, and IP/socket addresses, with optional Q-format, civil-time, hifitime, and hybrid-clock families. The default core has no third-party runtime dependencies; `Conn` is Copy, const-constructible, heap-free, and the crate forbids unsafe code.
Every included connection has a proptest law suite. Generated integer, Q-format, NonZero, and isomorphism families also have Kani harnesses over their full bit-width domains. The float claims are deliberately narrower and documented separately; floats use an N5 wrapper so NaN participates in an explicit reflexive preorder rather than being quietly excluded.
This isn’t intended to replace `TryFrom`: validation, runtime-parameterized conversions, and caller-selected policies generally belong in ordinary named functions.
Install:
Docs: https://cmk.github.io/connections/ Examples: https://github.com/cmk/connections/blob/main/EXAMPLES.md Crate: https://crates.io/crates/connectionsI'd appreciate any feedback you can give me. Cheers!
Not sure I clear on usage.
In our code we use non byte numbers(deranged and arbitrary int crates), symmetric signed, ordered floats, new num type pattern, our const and categorical num traits(num-traits crate sucks), static assertions, prop tests, easy cast crate(sound as). We have custom decimals. And newtypes of u64 * u64 = u128.
Looking into lean4 provers integrated into rust).
Can your crate compose somewhat with above?
This isn’t intended to replace arbitrary validation or runtime-parameterized conversions. That said, here is some lease gating code I used a connection for recently:
The library has a number of feature-flagged crates for domain-specific types. Toggling the macros flag will also expose its internal codegen macros (e.g. uint_int_sat) so you can create your own connections fairly easily. Predicates and proptest strategies are exported from src/prop.rs. I haven't tried lean, but there is a kani test suite focused mostly on the floating point connections.