nros_core/
time.rs

1//! ROS time types.
2//!
3//! Provides [`Time`] (seconds + nanoseconds) and [`Duration`] with
4//! arithmetic, conversions, and CDR serialization. All types are `no_std`
5//! compatible and use integer arithmetic only (no `f64::floor`/`f64::abs`).
6
7use core::ops::{Add, Sub};
8use nros_serdes::{CdrReader, CdrWriter, DeserError, Deserialize, SerError, Serialize};
9
10/// Nanoseconds per second
11const NANOS_PER_SEC: i64 = 1_000_000_000;
12
13/// Split a float seconds value into (sec, nanosec) without using `f64::floor()`/`f64::abs()`
14/// which require `std`. Uses integer truncation with correction for negative values.
15fn split_secs_f64(secs: f64) -> (i32, u32) {
16    let truncated = secs as i32;
17    // `as i32` truncates toward zero; floor rounds toward negative infinity.
18    // Correct for negative values with a fractional part.
19    let sec = if (truncated as f64) > secs {
20        truncated - 1
21    } else {
22        truncated
23    };
24    let frac = secs - sec as f64;
25    // frac should be in [0, 1), but guard against float imprecision
26    let frac = if frac < 0.0 { -frac } else { frac };
27    let nanosec = (frac * NANOS_PER_SEC as f64) as u32;
28    (sec, nanosec)
29}
30
31/// ROS Time representation
32///
33/// Matches `builtin_interfaces/msg/Time`:
34/// - `sec`: Seconds since epoch (signed for pre-epoch times)
35/// - `nanosec`: Nanoseconds within the second (0-999999999)
36#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, PartialOrd, Ord)]
37pub struct Time {
38    /// Seconds component
39    pub sec: i32,
40    /// Nanoseconds component (0-999999999)
41    pub nanosec: u32,
42}
43
44impl Time {
45    /// Create a new Time
46    pub const fn new(sec: i32, nanosec: u32) -> Self {
47        Self { sec, nanosec }
48    }
49
50    /// Create a Time representing zero
51    pub const fn zero() -> Self {
52        Self { sec: 0, nanosec: 0 }
53    }
54
55    /// Check if this time is zero
56    pub const fn is_zero(&self) -> bool {
57        self.sec == 0 && self.nanosec == 0
58    }
59
60    /// Create a Time from nanoseconds since epoch
61    pub const fn from_nanos(nanos: i64) -> Self {
62        let sec = (nanos / NANOS_PER_SEC) as i32;
63        let nanosec = (nanos % NANOS_PER_SEC) as u32;
64        Self { sec, nanosec }
65    }
66
67    /// Convert to total nanoseconds since epoch
68    pub const fn to_nanos(&self) -> i64 {
69        (self.sec as i64) * NANOS_PER_SEC + (self.nanosec as i64)
70    }
71
72    /// Create a Time from a Duration (treating duration as time since epoch)
73    pub const fn from_duration(d: Duration) -> Self {
74        Self {
75            sec: d.sec,
76            nanosec: d.nanosec,
77        }
78    }
79
80    /// Convert to Duration (treating time as duration since epoch)
81    pub const fn as_duration(&self) -> Duration {
82        Duration {
83            sec: self.sec,
84            nanosec: self.nanosec,
85        }
86    }
87
88    /// Create a Time from seconds (float)
89    pub fn from_secs_f64(secs: f64) -> Self {
90        let (sec, nanosec) = split_secs_f64(secs);
91        Self { sec, nanosec }
92    }
93
94    /// Convert to seconds (float)
95    pub fn to_secs_f64(&self) -> f64 {
96        self.sec as f64 + (self.nanosec as f64 / NANOS_PER_SEC as f64)
97    }
98}
99
100impl Add<Duration> for Time {
101    type Output = Time;
102
103    fn add(self, rhs: Duration) -> Self::Output {
104        let total_nanos = self.to_nanos() + rhs.to_nanos();
105        Time::from_nanos(total_nanos)
106    }
107}
108
109impl Sub<Duration> for Time {
110    type Output = Time;
111
112    fn sub(self, rhs: Duration) -> Self::Output {
113        let total_nanos = self.to_nanos() - rhs.to_nanos();
114        Time::from_nanos(total_nanos)
115    }
116}
117
118impl Sub<Time> for Time {
119    type Output = Duration;
120
121    fn sub(self, rhs: Time) -> Self::Output {
122        let diff_nanos = self.to_nanos() - rhs.to_nanos();
123        Duration::from_nanos(diff_nanos)
124    }
125}
126
127impl Serialize for Time {
128    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
129        writer.write_i32(self.sec)?;
130        writer.write_u32(self.nanosec)?;
131        Ok(())
132    }
133}
134
135impl Deserialize for Time {
136    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
137        Ok(Self {
138            sec: reader.read_i32()?,
139            nanosec: reader.read_u32()?,
140        })
141    }
142}
143
144/// ROS Duration representation
145///
146/// Matches `builtin_interfaces/msg/Duration`:
147/// - `sec`: Seconds (signed for negative durations)
148/// - `nanosec`: Nanoseconds (0-999999999)
149#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, PartialOrd, Ord)]
150pub struct Duration {
151    /// Seconds component
152    pub sec: i32,
153    /// Nanoseconds component (0-999999999)
154    pub nanosec: u32,
155}
156
157impl Duration {
158    /// Create a new Duration
159    pub const fn new(sec: i32, nanosec: u32) -> Self {
160        Self { sec, nanosec }
161    }
162
163    /// Create a Duration representing zero
164    pub const fn zero() -> Self {
165        Self { sec: 0, nanosec: 0 }
166    }
167
168    /// Check if this duration is zero
169    pub const fn is_zero(&self) -> bool {
170        self.sec == 0 && self.nanosec == 0
171    }
172
173    /// Create a Duration from seconds
174    pub const fn from_secs(secs: i32) -> Self {
175        Self {
176            sec: secs,
177            nanosec: 0,
178        }
179    }
180
181    /// Create a Duration from milliseconds
182    pub const fn from_millis(millis: i64) -> Self {
183        let sec = (millis / 1000) as i32;
184        let nanosec = ((millis % 1000) * 1_000_000) as u32;
185        Self { sec, nanosec }
186    }
187
188    /// Create a Duration from nanoseconds
189    pub const fn from_nanos(nanos: i64) -> Self {
190        let sec = (nanos / NANOS_PER_SEC) as i32;
191        let nanosec = (nanos % NANOS_PER_SEC).unsigned_abs() as u32;
192        Self { sec, nanosec }
193    }
194
195    /// Convert to total nanoseconds
196    pub const fn to_nanos(&self) -> i64 {
197        (self.sec as i64) * NANOS_PER_SEC + (self.nanosec as i64)
198    }
199
200    /// Create a Duration from seconds (float)
201    pub fn from_secs_f64(secs: f64) -> Self {
202        let (sec, nanosec) = split_secs_f64(secs);
203        Self { sec, nanosec }
204    }
205
206    /// Convert to seconds (float)
207    pub fn to_secs_f64(&self) -> f64 {
208        self.sec as f64 + (self.nanosec as f64 / NANOS_PER_SEC as f64)
209    }
210}
211
212impl Add for Duration {
213    type Output = Duration;
214
215    fn add(self, rhs: Duration) -> Self::Output {
216        let total_nanos = self.to_nanos() + rhs.to_nanos();
217        Duration::from_nanos(total_nanos)
218    }
219}
220
221impl Sub for Duration {
222    type Output = Duration;
223
224    fn sub(self, rhs: Duration) -> Self::Output {
225        let diff_nanos = self.to_nanos() - rhs.to_nanos();
226        Duration::from_nanos(diff_nanos)
227    }
228}
229
230impl Serialize for Duration {
231    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
232        writer.write_i32(self.sec)?;
233        writer.write_u32(self.nanosec)?;
234        Ok(())
235    }
236}
237
238impl Deserialize for Duration {
239    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
240        Ok(Self {
241            sec: reader.read_i32()?,
242            nanosec: reader.read_u32()?,
243        })
244    }
245}
246
247#[cfg(test)]
248mod tests {
249    use super::*;
250
251    #[test]
252    fn test_time_roundtrip() {
253        let mut buf = [0u8; 16];
254        let time = Time::new(1234567890, 123456789);
255
256        let mut writer = CdrWriter::new(&mut buf);
257        time.serialize(&mut writer).unwrap();
258
259        let mut reader = CdrReader::new(&buf);
260        let result = Time::deserialize(&mut reader).unwrap();
261        assert_eq!(result, time);
262    }
263
264    #[test]
265    fn test_duration_roundtrip() {
266        let mut buf = [0u8; 16];
267        let duration = Duration::new(-10, 500000000);
268
269        let mut writer = CdrWriter::new(&mut buf);
270        duration.serialize(&mut writer).unwrap();
271
272        let mut reader = CdrReader::new(&buf);
273        let result = Duration::deserialize(&mut reader).unwrap();
274        assert_eq!(result, duration);
275    }
276
277    #[test]
278    fn test_time_from_nanos() {
279        let time = Time::from_nanos(1_500_000_000);
280        assert_eq!(time.sec, 1);
281        assert_eq!(time.nanosec, 500_000_000);
282    }
283
284    #[test]
285    fn test_time_to_nanos() {
286        let time = Time::new(2, 500_000_000);
287        assert_eq!(time.to_nanos(), 2_500_000_000);
288    }
289
290    #[test]
291    fn test_time_add_duration() {
292        let time = Time::new(10, 500_000_000);
293        let duration = Duration::new(5, 700_000_000);
294        let result = time + duration;
295        assert_eq!(result.sec, 16);
296        assert_eq!(result.nanosec, 200_000_000);
297    }
298
299    #[test]
300    fn test_time_sub_duration() {
301        let time = Time::new(10, 500_000_000);
302        let duration = Duration::new(3, 200_000_000);
303        let result = time - duration;
304        assert_eq!(result.sec, 7);
305        assert_eq!(result.nanosec, 300_000_000);
306    }
307
308    #[test]
309    fn test_time_sub_time() {
310        let t1 = Time::new(10, 500_000_000);
311        let t2 = Time::new(7, 200_000_000);
312        let result = t1 - t2;
313        assert_eq!(result.sec, 3);
314        assert_eq!(result.nanosec, 300_000_000);
315    }
316
317    #[test]
318    fn test_time_from_duration() {
319        let duration = Duration::new(5, 123456789);
320        let time = Time::from_duration(duration);
321        assert_eq!(time.sec, 5);
322        assert_eq!(time.nanosec, 123456789);
323    }
324
325    #[test]
326    fn test_time_as_duration() {
327        let time = Time::new(5, 123456789);
328        let duration = time.as_duration();
329        assert_eq!(duration.sec, 5);
330        assert_eq!(duration.nanosec, 123456789);
331    }
332
333    #[test]
334    fn test_time_ordering() {
335        let t1 = Time::new(10, 0);
336        let t2 = Time::new(10, 500_000_000);
337        let t3 = Time::new(11, 0);
338        assert!(t1 < t2);
339        assert!(t2 < t3);
340    }
341
342    #[test]
343    fn test_duration_from_nanos() {
344        let duration = Duration::from_nanos(2_500_000_000);
345        assert_eq!(duration.sec, 2);
346        assert_eq!(duration.nanosec, 500_000_000);
347    }
348
349    #[test]
350    fn test_duration_to_nanos() {
351        let duration = Duration::new(3, 250_000_000);
352        assert_eq!(duration.to_nanos(), 3_250_000_000);
353    }
354
355    #[test]
356    fn test_duration_add() {
357        let d1 = Duration::new(2, 500_000_000);
358        let d2 = Duration::new(1, 700_000_000);
359        let result = d1 + d2;
360        assert_eq!(result.sec, 4);
361        assert_eq!(result.nanosec, 200_000_000);
362    }
363
364    #[test]
365    fn test_duration_sub() {
366        let d1 = Duration::new(5, 500_000_000);
367        let d2 = Duration::new(2, 200_000_000);
368        let result = d1 - d2;
369        assert_eq!(result.sec, 3);
370        assert_eq!(result.nanosec, 300_000_000);
371    }
372
373    #[test]
374    fn test_duration_ordering() {
375        let d1 = Duration::new(1, 0);
376        let d2 = Duration::new(1, 500_000_000);
377        let d3 = Duration::new(2, 0);
378        assert!(d1 < d2);
379        assert!(d2 < d3);
380    }
381
382    #[test]
383    fn test_time_secs_f64() {
384        let time = Time::from_secs_f64(1.5);
385        assert_eq!(time.sec, 1);
386        assert_eq!(time.nanosec, 500_000_000);
387
388        let secs = time.to_secs_f64();
389        assert!((secs - 1.5).abs() < 0.000001);
390    }
391
392    #[test]
393    fn test_duration_secs_f64() {
394        let duration = Duration::from_secs_f64(2.25);
395        assert_eq!(duration.sec, 2);
396        assert_eq!(duration.nanosec, 250_000_000);
397
398        let secs = duration.to_secs_f64();
399        assert!((secs - 2.25).abs() < 0.000001);
400    }
401}
402
403// =============================================================================
404// Kani bounded model checking proofs
405// =============================================================================
406
407#[cfg(kani)]
408mod verification {
409    use super::*;
410
411    // ---- Duration ----
412
413    #[kani::proof]
414    fn duration_from_nanos_no_panic() {
415        let nanos: i64 = kani::any();
416        // Constrain to tractable range for CBMC (i64 div/mod is expensive)
417        kani::assume(nanos >= -10_000_000_000 && nanos <= 10_000_000_000);
418        let dur = Duration::from_nanos(nanos);
419        // nanosec must always be in valid range
420        assert!(dur.nanosec < NANOS_PER_SEC as u32);
421    }
422
423    #[kani::proof]
424    fn duration_roundtrip_nanos() {
425        let nanos: i64 = kani::any();
426        // Constrain to tractable range for CBMC (i64 div/mod is expensive)
427        // Still covers multi-second values to exercise the div/mod logic
428        kani::assume(nanos >= 0 && nanos <= 10_000_000_000);
429        let dur = Duration::from_nanos(nanos);
430        assert_eq!(dur.to_nanos(), nanos);
431    }
432
433    #[kani::proof]
434    fn duration_zero_is_zero() {
435        let dur = Duration::zero();
436        assert!(dur.is_zero());
437        assert_eq!(dur.to_nanos(), 0);
438    }
439
440    #[kani::proof]
441    fn duration_from_secs() {
442        let secs: i32 = kani::any();
443        let dur = Duration::from_secs(secs);
444        assert_eq!(dur.sec, secs);
445        assert_eq!(dur.nanosec, 0);
446    }
447
448    #[kani::proof]
449    #[kani::unwind(5)]
450    fn duration_serialize_roundtrip() {
451        let sec: i32 = kani::any();
452        let nanosec: u32 = kani::any();
453        kani::assume(nanosec < NANOS_PER_SEC as u32);
454        let dur = Duration::new(sec, nanosec);
455
456        let mut buf = [0u8; 16];
457        let len = {
458            let mut writer = CdrWriter::new(&mut buf);
459            dur.serialize(&mut writer).unwrap();
460            writer.position()
461        };
462
463        let mut reader = CdrReader::new(&buf[..len]);
464        let deserialized = Duration::deserialize(&mut reader).unwrap();
465        assert_eq!(dur, deserialized);
466    }
467
468    // ---- Time ----
469
470    #[kani::proof]
471    fn time_from_nanos_no_panic() {
472        let nanos: i64 = kani::any();
473        // Constrain to tractable range for CBMC (i64 div/mod is expensive)
474        // NOTE: Negative nanos cause nanosec wrapping (known bug — Time::from_nanos
475        // lacks .unsigned_abs() unlike Duration::from_nanos). Constrain to >= 0.
476        kani::assume(nanos >= 0 && nanos <= 10_000_000_000);
477        let time = Time::from_nanos(nanos);
478        // nanosec must always be in valid range
479        assert!(time.nanosec < NANOS_PER_SEC as u32);
480    }
481
482    #[kani::proof]
483    fn time_roundtrip_nanos() {
484        let nanos: i64 = kani::any();
485        // Constrain to tractable range for CBMC (i64 div/mod is expensive)
486        kani::assume(nanos >= 0 && nanos <= 10_000_000_000);
487        let time = Time::from_nanos(nanos);
488        assert_eq!(time.to_nanos(), nanos);
489    }
490
491    #[kani::proof]
492    fn time_zero_is_zero() {
493        let time = Time::zero();
494        assert!(time.is_zero());
495        assert_eq!(time.to_nanos(), 0);
496    }
497
498    #[kani::proof]
499    fn time_duration_conversion() {
500        let sec: i32 = kani::any();
501        let nanosec: u32 = kani::any();
502        kani::assume(nanosec < NANOS_PER_SEC as u32);
503        let time = Time::new(sec, nanosec);
504        let dur = time.as_duration();
505        assert_eq!(dur.sec, time.sec);
506        assert_eq!(dur.nanosec, time.nanosec);
507        let back = Time::from_duration(dur);
508        assert_eq!(back, time);
509    }
510
511    #[kani::proof]
512    #[kani::unwind(5)]
513    fn time_serialize_roundtrip() {
514        let sec: i32 = kani::any();
515        let nanosec: u32 = kani::any();
516        kani::assume(nanosec < NANOS_PER_SEC as u32);
517        let time = Time::new(sec, nanosec);
518
519        let mut buf = [0u8; 16];
520        let len = {
521            let mut writer = CdrWriter::new(&mut buf);
522            time.serialize(&mut writer).unwrap();
523            writer.position()
524        };
525
526        let mut reader = CdrReader::new(&buf[..len]);
527        let deserialized = Time::deserialize(&mut reader).unwrap();
528        assert_eq!(time, deserialized);
529    }
530}
nros_core/time.rs

nros_core/
time.rs
