Skip to main content

nros_core/
action.rs

1//! ROS 2 Action types
2//!
3//! Actions provide asynchronous goal-based communication with feedback.
4//! An action client sends a goal to an action server, which executes the goal
5//! and provides feedback during execution and a result upon completion.
6//!
7//! ## Action Communication Pattern
8//!
9//! Actions use 5 underlying communication channels:
10//! - `send_goal` service: Submit a new goal
11//! - `cancel_goal` service: Request cancellation
12//! - `get_result` service: Retrieve final result
13//! - `feedback` topic: Progress updates during execution
14//! - `status` topic: Goal state transitions
15//!
16//! ## Example
17//!
18//! ```text
19//! use nros_core::{RosAction, GoalStatus};
20//!
21//! // Define an action type
22//! struct Fibonacci;
23//!
24//! impl RosAction for Fibonacci {
25//!     type Goal = FibonacciGoal;
26//!     type Result = FibonacciResult;
27//!     type Feedback = FibonacciFeedback;
28//!
29//!     const ACTION_NAME: &'static str = "example_interfaces::action::dds_::Fibonacci_";
30//!     const ACTION_HASH: &'static str = "...";
31//! }
32//! ```
33
34use crate::types::RosMessage;
35use core::fmt;
36use nros_serdes::{CdrReader, CdrWriter, DeserError, Deserialize, SerError, Serialize};
37
38/// Trait for ROS 2 action types
39///
40/// This trait defines the associated types and metadata for a ROS 2 action.
41/// Actions consist of three user-facing message types plus five action-protocol
42/// envelope types used on the wire (Phase 212.K.7.1.d/b):
43///
44/// User-facing:
45/// - `Goal`: Sent by client to initiate the action
46/// - `Result`: Returned by server when action completes
47/// - `Feedback`: Sent by server during execution to report progress
48///
49/// Wire envelopes (auto-emitted by `nros generate rust`):
50/// - `SendGoalRequest` / `SendGoalResponse`: `<Action>_SendGoal` service shape
51/// - `GetResultRequest` / `GetResultResponse`: `<Action>_GetResult` service shape
52/// - `FeedbackMessage`: `<Action>_FeedbackMessage` topic shape
53pub trait RosAction: Sized {
54    /// Goal message sent by client to initiate the action
55    type Goal: RosMessage;
56
57    /// Result message returned by server upon completion
58    type Result: RosMessage + Default;
59
60    /// Feedback message sent by server during execution
61    type Feedback: RosMessage;
62
63    /// `<Action>_SendGoal_Request` service envelope (wire-level send-goal request)
64    type SendGoalRequest: RosMessage;
65
66    /// `<Action>_SendGoal_Response` service envelope (wire-level send-goal reply)
67    type SendGoalResponse: RosMessage;
68
69    /// `<Action>_GetResult_Request` service envelope (wire-level get-result request)
70    type GetResultRequest: RosMessage;
71
72    /// `<Action>_GetResult_Response` service envelope (wire-level get-result reply)
73    type GetResultResponse: RosMessage;
74
75    /// `<Action>_FeedbackMessage` topic envelope (wire-level feedback message)
76    type FeedbackMessage: RosMessage;
77
78    /// Action type name (e.g., "example_interfaces::action::dds_::Fibonacci_")
79    const ACTION_NAME: &'static str;
80
81    /// Type hash for discovery (RIHS format)
82    const ACTION_HASH: &'static str;
83
84    /// RIHS hash of the `<Action>_SendGoal` SERVICE — the value a stock
85    /// `rmw_zenoh_cpp` client puts in the send_goal service keyexpr, distinct
86    /// from [`ACTION_HASH`](Self::ACTION_HASH). A nano-ros action server must
87    /// advertise it (not the action hash) or a ROS 2 client's `send_goal` query
88    /// keyexpr won't match the server's queryable (issue #0292). Generated
89    /// `impl RosAction` sets the real per-action value on Iron+; the default
90    /// keeps the historical (action-hash) behavior for hand-written impls and
91    /// Humble (where the placeholder hash makes all channels equal anyway).
92    const SEND_GOAL_SERVICE_HASH: &'static str = Self::ACTION_HASH;
93
94    /// RIHS hash of the `<Action>_GetResult` SERVICE (issue #0292; see
95    /// [`SEND_GOAL_SERVICE_HASH`](Self::SEND_GOAL_SERVICE_HASH)).
96    const GET_RESULT_SERVICE_HASH: &'static str = Self::ACTION_HASH;
97
98    /// Register the fixed ROS 2 action-protocol message types this action needs
99    /// at runtime beyond its own 8 envelopes — the `action_msgs` types the
100    /// cancel/status plumbing serializes (`CancelGoal_{Request,Response}`,
101    /// `GoalStatusArray`). The 8 `RosAction`-associated envelopes are registered
102    /// generically by the executor (`register_type::<A::Goal>()` …); these three
103    /// are NOT associated types (they live in `action_msgs`, which `nros-core`
104    /// cannot name), so the generated `impl RosAction` overrides this to register
105    /// them with the active RMW backend.
106    ///
107    /// Default: no-op (`Ok(())`) — keeps every existing `impl RosAction` valid
108    /// (RFC-0044 / phase-244 E3, non-breaking). Returns `Err(())` on a backend
109    /// registration failure; the caller maps it onto its own error type
110    /// (`nros-core` cannot name `nros-node::NodeError`).
111    // Unit error is deliberate — `nros-core` sits below `nros-node` and cannot
112    // name `NodeError`; the caller re-maps `Err(())` onto its own type.
113    #[allow(clippy::result_unit_err)]
114    fn register_protocol_types() -> Result<(), ()> {
115        Ok(())
116    }
117}
118
119/// Goal status states
120///
121/// These states match `action_msgs/msg/GoalStatus` from ROS 2.
122/// A goal progresses through these states during its lifecycle.
123#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
124#[repr(i8)]
125pub enum GoalStatus {
126    /// Status has not been set
127    #[default]
128    Unknown = 0,
129    /// Goal has been accepted and is awaiting execution
130    Accepted = 1,
131    /// Goal is currently being executed
132    Executing = 2,
133    /// Goal is in the process of being canceled
134    Canceling = 3,
135    /// Goal completed successfully
136    Succeeded = 4,
137    /// Goal was canceled before completion
138    Canceled = 5,
139    /// Goal was aborted due to an error
140    Aborted = 6,
141}
142
143impl GoalStatus {
144    /// Check if the goal is in a terminal state (completed, canceled, or aborted)
145    pub fn is_terminal(&self) -> bool {
146        matches!(
147            self,
148            GoalStatus::Succeeded | GoalStatus::Canceled | GoalStatus::Aborted
149        )
150    }
151
152    /// Check if the goal is still active (accepted, executing, or canceling)
153    pub fn is_active(&self) -> bool {
154        matches!(
155            self,
156            GoalStatus::Accepted | GoalStatus::Executing | GoalStatus::Canceling
157        )
158    }
159
160    /// Convert from i8 value
161    pub fn from_i8(value: i8) -> Option<Self> {
162        match value {
163            0 => Some(GoalStatus::Unknown),
164            1 => Some(GoalStatus::Accepted),
165            2 => Some(GoalStatus::Executing),
166            3 => Some(GoalStatus::Canceling),
167            4 => Some(GoalStatus::Succeeded),
168            5 => Some(GoalStatus::Canceled),
169            6 => Some(GoalStatus::Aborted),
170            _ => None,
171        }
172    }
173}
174
175impl fmt::Display for GoalStatus {
176    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
177        match self {
178            GoalStatus::Unknown => write!(f, "UNKNOWN"),
179            GoalStatus::Accepted => write!(f, "ACCEPTED"),
180            GoalStatus::Executing => write!(f, "EXECUTING"),
181            GoalStatus::Canceling => write!(f, "CANCELING"),
182            GoalStatus::Succeeded => write!(f, "SUCCEEDED"),
183            GoalStatus::Canceled => write!(f, "CANCELED"),
184            GoalStatus::Aborted => write!(f, "ABORTED"),
185        }
186    }
187}
188
189impl Serialize for GoalStatus {
190    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
191        writer.write_i8(*self as i8)
192    }
193}
194
195impl Deserialize for GoalStatus {
196    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
197        let value = reader.read_i8()?;
198        GoalStatus::from_i8(value).ok_or(DeserError::InvalidData)
199    }
200}
201
202/// Unique identifier for a goal
203///
204/// This is a 128-bit UUID matching `unique_identifier_msgs/msg/UUID`.
205#[derive(Clone, Copy, PartialEq, Eq, Hash)]
206pub struct GoalId {
207    /// UUID bytes in standard format
208    pub uuid: [u8; 16],
209}
210
211impl GoalId {
212    /// Length of the goal UUID in bytes (ROS 2 `unique_identifier_msgs/UUID`).
213    pub const UUID_LEN: usize = 16;
214
215    /// Length of any CDR length-prefix preceding the goal UUID bytes — **zero**.
216    ///
217    /// ROS 2 carries the goal id as `unique_identifier_msgs/UUID`, a fixed
218    /// `uint8[16]` array; CDR fixed arrays have **no** length prefix, so the goal
219    /// UUID sits directly after the CDR header. Pre-233.6 the action framing
220    /// wrote a `u32(16)` sequence prefix here (this const was `4`), which
221    /// self-matched nano-ros peers but added 4 bytes a real `rcl_action` peer
222    /// rejects. Kept as a named `0` (rather than deleted) so the C/C++/Cyclone
223    /// framing calcs that read `CDR_HEADER_LEN + SEQ_PREFIX_LEN + UUID_LEN` stay
224    /// correct after the migration.
225    pub const SEQ_PREFIX_LEN: usize = 0;
226
227    /// Create a new GoalId from UUID bytes
228    pub const fn new(uuid: [u8; 16]) -> Self {
229        Self { uuid }
230    }
231
232    /// Create a zero/null GoalId
233    pub const fn zero() -> Self {
234        Self { uuid: [0; 16] }
235    }
236
237    /// Check if this is a zero/null GoalId
238    pub fn is_zero(&self) -> bool {
239        self.uuid == [0; 16]
240    }
241
242    /// Create a GoalId from a simple counter (for testing/embedded use)
243    ///
244    /// This creates a deterministic UUID-like identifier from a counter value.
245    /// Not a true UUID, but useful for embedded systems without random number generators.
246    pub fn from_counter(counter: u64) -> Self {
247        let mut uuid = [0u8; 16];
248        // Put counter in last 8 bytes (big-endian)
249        uuid[8..16].copy_from_slice(&counter.to_be_bytes());
250        // Set version 4 (random) variant bits for compatibility
251        uuid[6] = (uuid[6] & 0x0f) | 0x40; // Version 4
252        uuid[8] = (uuid[8] & 0x3f) | 0x80; // Variant 1
253        Self { uuid }
254    }
255}
256
257impl Default for GoalId {
258    fn default() -> Self {
259        Self::zero()
260    }
261}
262
263impl Serialize for GoalId {
264    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
265        for byte in &self.uuid {
266            writer.write_u8(*byte)?;
267        }
268        Ok(())
269    }
270}
271
272impl Deserialize for GoalId {
273    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
274        let mut uuid = [0u8; 16];
275        for byte in &mut uuid {
276            *byte = reader.read_u8()?;
277        }
278        Ok(Self { uuid })
279    }
280}
281
282impl fmt::Debug for GoalId {
283    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
284        // Format as UUID string: xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
285        write!(
286            f,
287            "GoalId({:02x}{:02x}{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}{:02x}{:02x}{:02x}{:02x})",
288            self.uuid[0],
289            self.uuid[1],
290            self.uuid[2],
291            self.uuid[3],
292            self.uuid[4],
293            self.uuid[5],
294            self.uuid[6],
295            self.uuid[7],
296            self.uuid[8],
297            self.uuid[9],
298            self.uuid[10],
299            self.uuid[11],
300            self.uuid[12],
301            self.uuid[13],
302            self.uuid[14],
303            self.uuid[15]
304        )
305    }
306}
307
308impl fmt::Display for GoalId {
309    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
310        write!(
311            f,
312            "{:02x}{:02x}{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}{:02x}{:02x}{:02x}{:02x}",
313            self.uuid[0],
314            self.uuid[1],
315            self.uuid[2],
316            self.uuid[3],
317            self.uuid[4],
318            self.uuid[5],
319            self.uuid[6],
320            self.uuid[7],
321            self.uuid[8],
322            self.uuid[9],
323            self.uuid[10],
324            self.uuid[11],
325            self.uuid[12],
326            self.uuid[13],
327            self.uuid[14],
328            self.uuid[15]
329        )
330    }
331}
332
333/// Information about a goal
334///
335/// This matches `action_msgs/msg/GoalInfo` from ROS 2.
336/// Contains the goal ID and timestamp when the goal was accepted.
337#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
338pub struct GoalInfo {
339    /// Unique identifier for the goal
340    pub goal_id: GoalId,
341    /// Timestamp when the goal was accepted (nanoseconds since epoch)
342    pub stamp_sec: i32,
343    /// Nanosecond part of timestamp
344    pub stamp_nanosec: u32,
345}
346
347impl GoalInfo {
348    /// Create a new GoalInfo with the given ID and timestamp
349    pub const fn new(goal_id: GoalId, stamp_sec: i32, stamp_nanosec: u32) -> Self {
350        Self {
351            goal_id,
352            stamp_sec,
353            stamp_nanosec,
354        }
355    }
356
357    /// Create a GoalInfo with zero timestamp
358    pub const fn with_id(goal_id: GoalId) -> Self {
359        Self {
360            goal_id,
361            stamp_sec: 0,
362            stamp_nanosec: 0,
363        }
364    }
365}
366
367impl Serialize for GoalInfo {
368    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
369        self.goal_id.serialize(writer)?;
370        writer.write_i32(self.stamp_sec)?;
371        writer.write_u32(self.stamp_nanosec)?;
372        Ok(())
373    }
374}
375
376impl Deserialize for GoalInfo {
377    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
378        Ok(Self {
379            goal_id: GoalId::deserialize(reader)?,
380            stamp_sec: reader.read_i32()?,
381            stamp_nanosec: reader.read_u32()?,
382        })
383    }
384}
385
386/// Goal status with associated goal info
387///
388/// This matches `action_msgs/msg/GoalStatus` from ROS 2.
389#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
390pub struct GoalStatusStamped {
391    /// Goal information (ID and timestamp)
392    pub goal_info: GoalInfo,
393    /// Current status of the goal
394    pub status: GoalStatus,
395}
396
397impl GoalStatusStamped {
398    /// Create a new GoalStatusStamped
399    pub const fn new(goal_info: GoalInfo, status: GoalStatus) -> Self {
400        Self { goal_info, status }
401    }
402}
403
404impl Serialize for GoalStatusStamped {
405    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
406        self.goal_info.serialize(writer)?;
407        writer.write_i8(self.status as i8)?;
408        Ok(())
409    }
410}
411
412impl Deserialize for GoalStatusStamped {
413    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
414        let goal_info = GoalInfo::deserialize(reader)?;
415        let status_val = reader.read_i8()?;
416        let status = GoalStatus::from_i8(status_val).unwrap_or(GoalStatus::Unknown);
417        Ok(Self { goal_info, status })
418    }
419}
420
421/// `action_msgs/srv/CancelGoal` RPC return codes.
422///
423/// This is the *whole-request* outcome the server writes into the
424/// `CancelGoal` reply — "did the cancel RPC succeed", not "is this one goal
425/// being cancelled". These codes are the wire contract, so the discriminants
426/// are fixed by `action_msgs`.
427///
428/// Issue 0796 — this type used to be called `CancelResponse`, which is the
429/// name C ([`nros_cancel_response_t`]) and C++ ([`nros::CancelResponse`]) both
430/// use for the PER-GOAL accept/reject decision. Two concepts under one name is
431/// how [`CancelResponse`] ended up being the type a per-goal cancel callback
432/// returned: `CancelResponse::Ok` meant "cancel this goal", which reads as an
433/// RPC status and is not one. C already named them apart
434/// (`nros_cancel_response_t` vs `nros_cancel_return_code_t`); the Rust names
435/// now follow it.
436///
437/// [`nros_cancel_response_t`]: https://docs.rs/nros-c
438/// [`nros::CancelResponse`]: CancelResponse
439#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
440#[repr(i8)]
441pub enum CancelReturnCode {
442    /// No error, goal(s) will be canceled
443    #[default]
444    Ok = 0,
445    /// Goal was rejected (not cancelable or doesn't exist)
446    Rejected = 1,
447    /// Unknown goal ID
448    UnknownGoal = 2,
449    /// Goal is already in a terminal state
450    GoalTerminated = 3,
451}
452
453impl CancelReturnCode {
454    /// Convert from i8 value
455    pub fn from_i8(value: i8) -> Option<Self> {
456        match value {
457            0 => Some(CancelReturnCode::Ok),
458            1 => Some(CancelReturnCode::Rejected),
459            2 => Some(CancelReturnCode::UnknownGoal),
460            3 => Some(CancelReturnCode::GoalTerminated),
461            _ => None,
462        }
463    }
464}
465
466impl Serialize for CancelReturnCode {
467    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
468        writer.write_i8(*self as i8)
469    }
470}
471
472impl Deserialize for CancelReturnCode {
473    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
474        let value = reader.read_i8()?;
475        CancelReturnCode::from_i8(value).ok_or(DeserError::InvalidData)
476    }
477}
478
479/// Per-goal cancel decision returned from a server's cancel callback.
480///
481/// The twin of [`GoalResponse`] for the cancel path: the user is asked about
482/// ONE goal and answers accept or reject. It never travels on the wire — the
483/// server turns the answer into a [`CancelReturnCode`] plus a `goals_canceling`
484/// entry when it writes the `CancelGoal` reply.
485///
486/// Discriminants match C's `nros_cancel_response_t` (`NROS_CANCEL_REJECT` = 0,
487/// `NROS_CANCEL_ACCEPT` = 1) and C++'s `nros::CancelResponse`, so the three
488/// surfaces agree. `Reject` is the default because a zeroed or unanswered
489/// decision must not cancel a goal nobody asked to cancel.
490#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
491#[repr(i8)]
492pub enum CancelResponse {
493    /// Do not cancel this goal.
494    #[default]
495    Reject = 0,
496    /// Cancel this goal — it transitions to [`GoalStatus::Canceling`].
497    Accept = 1,
498}
499
500impl CancelResponse {
501    /// Convert from i8 value
502    pub fn from_i8(value: i8) -> Option<Self> {
503        match value {
504            0 => Some(CancelResponse::Reject),
505            1 => Some(CancelResponse::Accept),
506            _ => None,
507        }
508    }
509}
510
511/// Goal accept/reject response codes
512#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
513#[repr(i8)]
514pub enum GoalResponse {
515    /// Goal was rejected
516    #[default]
517    Reject = 0,
518    /// Goal was accepted and will be executed
519    AcceptAndExecute = 1,
520    /// Goal was accepted and is deferred
521    AcceptAndDefer = 2,
522}
523
524impl GoalResponse {
525    /// Convert from i8 value
526    pub fn from_i8(value: i8) -> Option<Self> {
527        match value {
528            0 => Some(GoalResponse::Reject),
529            1 => Some(GoalResponse::AcceptAndExecute),
530            2 => Some(GoalResponse::AcceptAndDefer),
531            _ => None,
532        }
533    }
534
535    /// Check if the goal was accepted
536    pub fn is_accepted(&self) -> bool {
537        matches!(
538            self,
539            GoalResponse::AcceptAndExecute | GoalResponse::AcceptAndDefer
540        )
541    }
542}
543
544/// Action server handle (type-level marker)
545///
546/// This is a lightweight handle for tracking an action server.
547/// The actual implementation is in `nros-node`.
548pub struct ActionServer<A: RosAction> {
549    /// Action name (e.g., "/fibonacci")
550    pub name: &'static str,
551    /// Marker for action type
552    _marker: core::marker::PhantomData<A>,
553}
554
555impl<A: RosAction> ActionServer<A> {
556    /// Create a new action server handle
557    pub fn new(name: &'static str) -> Self {
558        Self {
559            name,
560            _marker: core::marker::PhantomData,
561        }
562    }
563
564    /// Get the action name
565    pub fn name(&self) -> &str {
566        self.name
567    }
568
569    /// Get the action type name
570    pub fn action_type(&self) -> &'static str {
571        A::ACTION_NAME
572    }
573
574    /// Get the action type hash
575    pub fn action_hash(&self) -> &'static str {
576        A::ACTION_HASH
577    }
578}
579
580/// Action client handle (type-level marker)
581///
582/// This is a lightweight handle for tracking an action client.
583/// The actual implementation is in `nros-node`.
584pub struct ActionClient<A: RosAction> {
585    /// Action name (e.g., "/fibonacci")
586    pub name: &'static str,
587    /// Marker for action type
588    _marker: core::marker::PhantomData<A>,
589}
590
591impl<A: RosAction> ActionClient<A> {
592    /// Create a new action client handle
593    pub fn new(name: &'static str) -> Self {
594        Self {
595            name,
596            _marker: core::marker::PhantomData,
597        }
598    }
599
600    /// Get the action name
601    pub fn name(&self) -> &str {
602        self.name
603    }
604
605    /// Get the action type name
606    pub fn action_type(&self) -> &'static str {
607        A::ACTION_NAME
608    }
609
610    /// Get the action type hash
611    pub fn action_hash(&self) -> &'static str {
612        A::ACTION_HASH
613    }
614}
615
616#[cfg(test)]
617mod tests {
618    extern crate std;
619
620    use super::*;
621    use std::format;
622
623    #[test]
624    fn test_goal_status_is_terminal() {
625        assert!(!GoalStatus::Unknown.is_terminal());
626        assert!(!GoalStatus::Accepted.is_terminal());
627        assert!(!GoalStatus::Executing.is_terminal());
628        assert!(!GoalStatus::Canceling.is_terminal());
629        assert!(GoalStatus::Succeeded.is_terminal());
630        assert!(GoalStatus::Canceled.is_terminal());
631        assert!(GoalStatus::Aborted.is_terminal());
632    }
633
634    #[test]
635    fn test_goal_status_is_active() {
636        assert!(!GoalStatus::Unknown.is_active());
637        assert!(GoalStatus::Accepted.is_active());
638        assert!(GoalStatus::Executing.is_active());
639        assert!(GoalStatus::Canceling.is_active());
640        assert!(!GoalStatus::Succeeded.is_active());
641        assert!(!GoalStatus::Canceled.is_active());
642        assert!(!GoalStatus::Aborted.is_active());
643    }
644
645    #[test]
646    fn test_goal_status_from_i8() {
647        assert_eq!(GoalStatus::from_i8(0), Some(GoalStatus::Unknown));
648        assert_eq!(GoalStatus::from_i8(1), Some(GoalStatus::Accepted));
649        assert_eq!(GoalStatus::from_i8(2), Some(GoalStatus::Executing));
650        assert_eq!(GoalStatus::from_i8(3), Some(GoalStatus::Canceling));
651        assert_eq!(GoalStatus::from_i8(4), Some(GoalStatus::Succeeded));
652        assert_eq!(GoalStatus::from_i8(5), Some(GoalStatus::Canceled));
653        assert_eq!(GoalStatus::from_i8(6), Some(GoalStatus::Aborted));
654        assert_eq!(GoalStatus::from_i8(7), None);
655        assert_eq!(GoalStatus::from_i8(-1), None);
656    }
657
658    #[test]
659    fn test_goal_id_zero() {
660        let id = GoalId::zero();
661        assert!(id.is_zero());
662        assert_eq!(id.uuid, [0; 16]);
663    }
664
665    #[test]
666    fn test_goal_id_from_counter() {
667        let id1 = GoalId::from_counter(1);
668        let id2 = GoalId::from_counter(2);
669
670        assert!(!id1.is_zero());
671        assert!(!id2.is_zero());
672        assert_ne!(id1, id2);
673
674        // Same counter should produce same ID
675        let id1_again = GoalId::from_counter(1);
676        assert_eq!(id1, id1_again);
677    }
678
679    #[test]
680    fn test_goal_id_display() {
681        let id = GoalId::new([
682            0x12, 0x34, 0x56, 0x78, 0x9a, 0xbc, 0xde, 0xf0, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66,
683            0x77, 0x88,
684        ]);
685        let s = format!("{}", id);
686        assert_eq!(s, "12345678-9abc-def0-1122-334455667788");
687    }
688
689    #[test]
690    fn test_cancel_return_code_from_i8() {
691        assert_eq!(CancelReturnCode::from_i8(0), Some(CancelReturnCode::Ok));
692        assert_eq!(
693            CancelReturnCode::from_i8(1),
694            Some(CancelReturnCode::Rejected)
695        );
696        assert_eq!(
697            CancelReturnCode::from_i8(2),
698            Some(CancelReturnCode::UnknownGoal)
699        );
700        assert_eq!(
701            CancelReturnCode::from_i8(3),
702            Some(CancelReturnCode::GoalTerminated)
703        );
704        assert_eq!(CancelReturnCode::from_i8(4), None);
705    }
706
707    /// Issue 0796 — the per-goal decision and the RPC return code are two
708    /// types now, and the thing that made the collision dangerous is that
709    /// their discriminants OVERLAP with opposite meanings: 0 is "reject this
710    /// goal" on one and "the RPC succeeded" on the other. A cast between them
711    /// is therefore never a no-op, which is what this pins down.
712    #[test]
713    fn test_cancel_response_is_not_a_return_code() {
714        assert_eq!(CancelResponse::from_i8(0), Some(CancelResponse::Reject));
715        assert_eq!(CancelResponse::from_i8(1), Some(CancelResponse::Accept));
716        assert_eq!(CancelResponse::from_i8(2), None);
717        assert_eq!(CancelResponse::default(), CancelResponse::Reject);
718
719        // Same byte, opposite verdicts.
720        assert_eq!(CancelResponse::Reject as i8, CancelReturnCode::Ok as i8);
721        assert_eq!(
722            CancelResponse::Accept as i8,
723            CancelReturnCode::Rejected as i8
724        );
725    }
726
727    #[test]
728    fn test_goal_response_is_accepted() {
729        assert!(!GoalResponse::Reject.is_accepted());
730        assert!(GoalResponse::AcceptAndExecute.is_accepted());
731        assert!(GoalResponse::AcceptAndDefer.is_accepted());
732    }
733
734    #[test]
735    fn test_goal_info_new() {
736        let goal_id = GoalId::from_counter(42);
737        let info = GoalInfo::new(goal_id, 123, 456);
738        assert_eq!(info.goal_id, goal_id);
739        assert_eq!(info.stamp_sec, 123);
740        assert_eq!(info.stamp_nanosec, 456);
741    }
742
743    #[test]
744    fn test_goal_info_with_id() {
745        let goal_id = GoalId::from_counter(42);
746        let info = GoalInfo::with_id(goal_id);
747        assert_eq!(info.goal_id, goal_id);
748        assert_eq!(info.stamp_sec, 0);
749        assert_eq!(info.stamp_nanosec, 0);
750    }
751
752    #[test]
753    fn test_goal_status_stamped() {
754        let goal_id = GoalId::from_counter(1);
755        let info = GoalInfo::with_id(goal_id);
756        let stamped = GoalStatusStamped::new(info, GoalStatus::Executing);
757        assert_eq!(stamped.goal_info.goal_id, goal_id);
758        assert_eq!(stamped.status, GoalStatus::Executing);
759    }
760
761    #[test]
762    fn test_goal_id_serialization() {
763        use nros_serdes::{CdrReader, CdrWriter};
764
765        let original = GoalId::new([
766            0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, 0x0e,
767            0x0f, 0x10,
768        ]);
769
770        // Serialize
771        let mut buf = [0u8; 32];
772        let mut writer = CdrWriter::new(&mut buf);
773        original.serialize(&mut writer).unwrap();
774        let len = writer.position();
775        assert_eq!(len, 16); // UUID is 16 bytes
776
777        // Deserialize
778        let mut reader = CdrReader::new(&buf[..len]);
779        let deserialized = GoalId::deserialize(&mut reader).unwrap();
780
781        assert_eq!(original, deserialized);
782    }
783
784    #[test]
785    fn test_goal_status_serialization() {
786        use nros_serdes::{CdrReader, CdrWriter};
787
788        for status in [
789            GoalStatus::Unknown,
790            GoalStatus::Accepted,
791            GoalStatus::Executing,
792            GoalStatus::Canceling,
793            GoalStatus::Succeeded,
794            GoalStatus::Canceled,
795            GoalStatus::Aborted,
796        ] {
797            let mut buf = [0u8; 8];
798            let len = {
799                let mut writer = CdrWriter::new(&mut buf);
800                status.serialize(&mut writer).unwrap();
801                writer.position()
802            };
803
804            let mut reader = CdrReader::new(&buf[..len]);
805            let deserialized = GoalStatus::deserialize(&mut reader).unwrap();
806
807            assert_eq!(status, deserialized);
808        }
809    }
810
811    #[test]
812    fn test_goal_info_serialization() {
813        use nros_serdes::{CdrReader, CdrWriter};
814
815        let goal_id = GoalId::from_counter(42);
816        let original = GoalInfo::new(goal_id, 1234567890, 123456789);
817
818        // Serialize
819        let mut buf = [0u8; 64];
820        let mut writer = CdrWriter::new(&mut buf);
821        original.serialize(&mut writer).unwrap();
822        let len = writer.position();
823        // UUID (16) + i32 (4) + u32 (4) = 24 bytes
824        assert_eq!(len, 24);
825
826        // Deserialize
827        let mut reader = CdrReader::new(&buf[..len]);
828        let deserialized = GoalInfo::deserialize(&mut reader).unwrap();
829
830        assert_eq!(original.goal_id, deserialized.goal_id);
831        assert_eq!(original.stamp_sec, deserialized.stamp_sec);
832        assert_eq!(original.stamp_nanosec, deserialized.stamp_nanosec);
833    }
834
835    #[test]
836    fn test_goal_status_stamped_serialization() {
837        use nros_serdes::{CdrReader, CdrWriter};
838
839        let goal_id = GoalId::from_counter(99);
840        let goal_info = GoalInfo::new(goal_id, 987654321, 111222333);
841        let original = GoalStatusStamped::new(goal_info, GoalStatus::Succeeded);
842
843        // Serialize
844        let mut buf = [0u8; 64];
845        let mut writer = CdrWriter::new(&mut buf);
846        original.serialize(&mut writer).unwrap();
847        let len = writer.position();
848        // GoalInfo (24) + i8 (1) = 25 bytes
849        assert_eq!(len, 25);
850
851        // Deserialize
852        let mut reader = CdrReader::new(&buf[..len]);
853        let deserialized = GoalStatusStamped::deserialize(&mut reader).unwrap();
854
855        assert_eq!(original.goal_info.goal_id, deserialized.goal_info.goal_id);
856        assert_eq!(
857            original.goal_info.stamp_sec,
858            deserialized.goal_info.stamp_sec
859        );
860        assert_eq!(
861            original.goal_info.stamp_nanosec,
862            deserialized.goal_info.stamp_nanosec
863        );
864        assert_eq!(original.status, deserialized.status);
865    }
866}
867
868// =============================================================================
869// Kani bounded model checking proofs
870// =============================================================================
871
872#[cfg(kani)]
873mod verification {
874    use super::*;
875
876    // ---- GoalStatus ----
877
878    #[kani::proof]
879    fn goal_status_from_i8_valid_range() {
880        let val: i8 = kani::any();
881        let status = GoalStatus::from_i8(val);
882        if (0..=6).contains(&val) {
883            assert!(status.is_some());
884        } else {
885            assert!(status.is_none());
886        }
887    }
888
889    #[kani::proof]
890    fn goal_status_terminal_active_exclusive() {
891        let val: i8 = kani::any();
892        kani::assume((0..=6).contains(&val));
893        let status = GoalStatus::from_i8(val).unwrap();
894        // Terminal and active must be mutually exclusive
895        assert!(!(status.is_terminal() && status.is_active()));
896        // Unknown(0) is neither terminal nor active
897        if val == 0 {
898            assert!(!status.is_terminal());
899            assert!(!status.is_active());
900        }
901        // Active: 1, 2, 3
902        if (1..=3).contains(&val) {
903            assert!(status.is_active());
904            assert!(!status.is_terminal());
905        }
906        // Terminal: 4, 5, 6
907        if (4..=6).contains(&val) {
908            assert!(status.is_terminal());
909            assert!(!status.is_active());
910        }
911    }
912
913    #[kani::proof]
914    #[kani::unwind(5)]
915    fn goal_status_serialize_roundtrip() {
916        let val: i8 = kani::any();
917        kani::assume((0..=6).contains(&val));
918        let status = GoalStatus::from_i8(val).unwrap();
919
920        let mut buf = [0u8; 8];
921        let len = {
922            let mut writer = CdrWriter::new(&mut buf);
923            status.serialize(&mut writer).unwrap();
924            writer.position()
925        };
926
927        let mut reader = CdrReader::new(&buf[..len]);
928        let deserialized = GoalStatus::deserialize(&mut reader).unwrap();
929        assert_eq!(status, deserialized);
930    }
931
932    // ---- GoalResponse ----
933
934    #[kani::proof]
935    fn goal_response_from_i8_valid_range() {
936        let val: i8 = kani::any();
937        let resp = GoalResponse::from_i8(val);
938        if (0..=2).contains(&val) {
939            assert!(resp.is_some());
940        } else {
941            assert!(resp.is_none());
942        }
943    }
944
945    #[kani::proof]
946    fn goal_response_is_accepted_consistent() {
947        let val: i8 = kani::any();
948        kani::assume((0..=2).contains(&val));
949        let resp = GoalResponse::from_i8(val).unwrap();
950        // Reject(0) → not accepted; AcceptAndExecute(1), AcceptAndDefer(2) → accepted
951        assert_eq!(resp.is_accepted(), val >= 1);
952    }
953
954    // ---- CancelReturnCode ----
955
956    #[kani::proof]
957    fn cancel_return_code_from_i8_valid_range() {
958        let val: i8 = kani::any();
959        let resp = CancelReturnCode::from_i8(val);
960        if (0..=3).contains(&val) {
961            assert!(resp.is_some());
962        } else {
963            assert!(resp.is_none());
964        }
965    }
966
967    // ---- CancelResponse ----
968
969    #[kani::proof]
970    fn cancel_response_from_i8_valid_range() {
971        let val: i8 = kani::any();
972        let resp = CancelResponse::from_i8(val);
973        if (0..=1).contains(&val) {
974            assert!(resp.is_some());
975        } else {
976            assert!(resp.is_none());
977        }
978    }
979
980    // ---- GoalId ----
981
982    #[kani::proof]
983    fn goal_id_zero_is_zero() {
984        let id = GoalId::zero();
985        assert!(id.is_zero());
986    }
987
988    #[kani::proof]
989    fn goal_id_from_counter_deterministic() {
990        let counter: u64 = kani::any();
991        // Constrain for CBMC tractability (exercises same byte/bit logic)
992        kani::assume(counter <= 1_000_000);
993        let id1 = GoalId::from_counter(counter);
994        let id2 = GoalId::from_counter(counter);
995        assert_eq!(id1, id2);
996    }
997
998    #[kani::proof]
999    fn goal_id_from_counter_not_zero() {
1000        let counter: u64 = kani::any();
1001        kani::assume(counter > 0 && counter <= 1_000_000);
1002        let id = GoalId::from_counter(counter);
1003        assert!(!id.is_zero());
1004    }
1005
1006    #[kani::proof]
1007    #[kani::unwind(20)]
1008    fn goal_id_serialize_roundtrip() {
1009        let mut uuid = [0u8; 16];
1010        // Use a few arbitrary bytes (bounded for tractability)
1011        uuid[0] = kani::any();
1012        uuid[7] = kani::any();
1013        uuid[15] = kani::any();
1014        let id = GoalId::new(uuid);
1015
1016        let mut buf = [0u8; 32];
1017        let len = {
1018            let mut writer = CdrWriter::new(&mut buf);
1019            id.serialize(&mut writer).unwrap();
1020            writer.position()
1021        };
1022
1023        let mut reader = CdrReader::new(&buf[..len]);
1024        let deserialized = GoalId::deserialize(&mut reader).unwrap();
1025        assert_eq!(id, deserialized);
1026    }
1027}