3 ms·

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

by dlahoda 3mo ago

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 3mo ago
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.

by dlahoda 3mo ago

partialsolve 3mo ago

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.