[partialsolve]

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.

Install:

    cargo add connections

Docs: https://cmk.github.io/connections/ Examples: https://github.com/cmk/connections/blob/main/EXAMPLES.md Crate: https://crates.io/crates/connections

I'd appreciate any feedback you can give me. Cheers!

[dlahoda]

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?

[partialsolve]

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.