Show HN: Galois connections for composable numeric casts in Rust
github.com
github.com
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)
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);
lower(b) <= a iff b <= floor(a)
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:
cargo add connections
I'd appreciate any feedback you can give me. Cheers!
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?
// 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))
}