nros_core/

action.rs

//! ROS 2 Action types
//!
//! Actions provide asynchronous goal-based communication with feedback.
//! An action client sends a goal to an action server, which executes the goal
//! and provides feedback during execution and a result upon completion.
//!
//! ## Action Communication Pattern
//!
//! Actions use 5 underlying communication channels:
//! - `send_goal` service: Submit a new goal
//! - `cancel_goal` service: Request cancellation
//! - `get_result` service: Retrieve final result
//! - `feedback` topic: Progress updates during execution
//! - `status` topic: Goal state transitions
//!
//! ## Example
//!
//! ```text
//! use nros_core::{RosAction, GoalStatusCode};
//!
//! // Define an action type
//! struct Fibonacci;
//!
//! impl RosAction for Fibonacci {
//!     type Goal = FibonacciGoal;
//!     type Result = FibonacciResult;
//!     type Feedback = FibonacciFeedback;
//!
//!     const ACTION_NAME: &'static str = "example_interfaces::action::dds_::Fibonacci_";
//!     const ACTION_HASH: &'static str = "...";
//! }
//! ```

use crate::types::RosMessage;
use core::fmt;
use nros_serdes::{CdrReader, CdrWriter, DeserError, Deserialize, SerError, Serialize};

/// Trait for ROS 2 action types
///
/// This trait defines the associated types and metadata for a ROS 2 action.
/// Actions consist of three user-facing message types plus five action-protocol
/// envelope types used on the wire (Phase 212.K.7.1.d/b):
///
/// User-facing:
/// - `Goal`: Sent by client to initiate the action
/// - `Result`: Returned by server when action completes
/// - `Feedback`: Sent by server during execution to report progress
///
/// Wire envelopes (auto-emitted by `nros generate rust`):
/// - `SendGoalRequest` / `SendGoalResponse`: `<Action>_SendGoal` service shape
/// - `GetResultRequest` / `GetResultResponse`: `<Action>_GetResult` service shape
/// - `FeedbackMessage`: `<Action>_FeedbackMessage` topic shape
pub trait RosAction: Sized {
    /// Goal message sent by client to initiate the action
    type Goal: RosMessage;

    /// Result message returned by server upon completion
    type Result: RosMessage + Default;

    /// Feedback message sent by server during execution
    type Feedback: RosMessage;

    /// `<Action>_SendGoal_Request` service envelope (wire-level send-goal request)
    type SendGoalRequest: RosMessage;

    /// `<Action>_SendGoal_Response` service envelope (wire-level send-goal reply)
    type SendGoalResponse: RosMessage;

    /// `<Action>_GetResult_Request` service envelope (wire-level get-result request)
    type GetResultRequest: RosMessage;

    /// `<Action>_GetResult_Response` service envelope (wire-level get-result reply)
    type GetResultResponse: RosMessage;

    /// `<Action>_FeedbackMessage` topic envelope (wire-level feedback message)
    type FeedbackMessage: RosMessage;

    /// Action type name (e.g., "example_interfaces::action::dds_::Fibonacci_")
    const ACTION_NAME: &'static str;

    /// Type hash for discovery (RIHS format)
    const ACTION_HASH: &'static str;

    /// RIHS hash of the `<Action>_SendGoal` SERVICE — the value a stock
    /// `rmw_zenoh_cpp` client puts in the send_goal service keyexpr, distinct
    /// from [`ACTION_HASH`](Self::ACTION_HASH). A nano-ros action server must
    /// advertise it (not the action hash) or a ROS 2 client's `send_goal` query
    /// keyexpr won't match the server's queryable (issue #0292). Generated
    /// `impl RosAction` sets the real per-action value on Iron+; the default
    /// keeps the historical (action-hash) behavior for hand-written impls and
    /// Humble (where the placeholder hash makes all channels equal anyway).
    const SEND_GOAL_SERVICE_HASH: &'static str = Self::ACTION_HASH;

    /// RIHS hash of the `<Action>_GetResult` SERVICE (issue #0292; see
    /// [`SEND_GOAL_SERVICE_HASH`](Self::SEND_GOAL_SERVICE_HASH)).
    const GET_RESULT_SERVICE_HASH: &'static str = Self::ACTION_HASH;

    /// RIHS hash of the standard `action_msgs/srv/CancelGoal` SERVICE, which
    /// every action's `cancel_goal` endpoint is keyed on (issue 1913). The same
    /// value for every action, but `nros-core` cannot name `action_msgs`, so the
    /// generated impl carries it. Default as for
    /// [`SEND_GOAL_SERVICE_HASH`](Self::SEND_GOAL_SERVICE_HASH).
    const CANCEL_GOAL_SERVICE_HASH: &'static str = Self::ACTION_HASH;

    /// RIHS hash of the standard `action_msgs/msg/GoalStatusArray`, which every
    /// action's `status` topic is keyed on (issue 1913).
    const STATUS_MESSAGE_HASH: &'static str = Self::ACTION_HASH;

    /// Register the fixed ROS 2 action-protocol message types this action needs
    /// at runtime beyond its own 8 envelopes — the `action_msgs` types the
    /// cancel/status plumbing serializes (`CancelGoal_{Request,Response}`,
    /// `GoalStatusArray`). The 8 `RosAction`-associated envelopes are registered
    /// generically by the executor (`register_type::<A::Goal>()` …); these three
    /// are NOT associated types (they live in `action_msgs`, which `nros-core`
    /// cannot name), so the generated `impl RosAction` overrides this to register
    /// them with the active RMW backend.
    ///
    /// Default: no-op (`Ok(())`) — keeps every existing `impl RosAction` valid
    /// (RFC-0044 / phase-244 E3, non-breaking). Returns `Err(())` on a backend
    /// registration failure; the caller maps it onto its own error type
    /// (`nros-core` cannot name `nros-node::NodeError`).
    // Unit error is deliberate — `nros-core` sits below `nros-node` and cannot
    // name `NodeError`; the caller re-maps `Err(())` onto its own type.
    #[allow(clippy::result_unit_err)]
    fn register_protocol_types() -> Result<(), ()> {
        Ok(())
    }
}

/// Goal status states -- rclrs's `GoalStatusCode` (phase-515 R8).
///
/// These states match `action_msgs/msg/GoalStatus` from ROS 2. It was
/// `GoalStatus`, which is a deprecated alias for one release; rclrs gives that
/// name to the `{code, goal_id, stamp}` record, which here is
/// [`GoalStatusStamped`].
/// A goal progresses through these states during its lifecycle.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
#[repr(i8)]
pub enum GoalStatusCode {
    /// Status has not been set
    #[default]
    Unknown = 0,
    /// Goal has been accepted and is awaiting execution
    Accepted = 1,
    /// Goal is currently being executed
    Executing = 2,
    /// Goal is in the process of being canceled
    Canceling = 3,
    /// Goal completed successfully
    Succeeded = 4,
    /// Goal was canceled before completion
    Canceled = 5,
    /// Goal was aborted due to an error
    Aborted = 6,
}

impl GoalStatusCode {
    /// Check if the goal is in a terminal state (completed, canceled, or aborted)
    pub fn is_terminal(&self) -> bool {
        matches!(
            self,
            GoalStatusCode::Succeeded | GoalStatusCode::Canceled | GoalStatusCode::Aborted
        )
    }

    /// Check if the goal is still active (accepted, executing, or canceling)
    pub fn is_active(&self) -> bool {
        matches!(
            self,
            GoalStatusCode::Accepted | GoalStatusCode::Executing | GoalStatusCode::Canceling
        )
    }

    /// Convert from i8 value
    pub fn from_i8(value: i8) -> Option<Self> {
        match value {
            0 => Some(GoalStatusCode::Unknown),
            1 => Some(GoalStatusCode::Accepted),
            2 => Some(GoalStatusCode::Executing),
            3 => Some(GoalStatusCode::Canceling),
            4 => Some(GoalStatusCode::Succeeded),
            5 => Some(GoalStatusCode::Canceled),
            6 => Some(GoalStatusCode::Aborted),
            _ => None,
        }
    }
}

impl fmt::Display for GoalStatusCode {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            GoalStatusCode::Unknown => write!(f, "UNKNOWN"),
            GoalStatusCode::Accepted => write!(f, "ACCEPTED"),
            GoalStatusCode::Executing => write!(f, "EXECUTING"),
            GoalStatusCode::Canceling => write!(f, "CANCELING"),
            GoalStatusCode::Succeeded => write!(f, "SUCCEEDED"),
            GoalStatusCode::Canceled => write!(f, "CANCELED"),
            GoalStatusCode::Aborted => write!(f, "ABORTED"),
        }
    }
}

impl Serialize for GoalStatusCode {
    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
        writer.write_i8(*self as i8)
    }
}

impl Deserialize for GoalStatusCode {
    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
        let value = reader.read_i8()?;
        GoalStatusCode::from_i8(value).ok_or(DeserError::InvalidData)
    }
}

/// Unique identifier for a goal -- rclrs's `GoalUuid` (phase-515 R8).
///
/// This is a 128-bit UUID matching `unique_identifier_msgs/msg/UUID`. It was
/// `GoalId`, which is a deprecated alias for one release.
#[derive(Clone, Copy, PartialEq, Eq, Hash)]
pub struct GoalUuid {
    /// UUID bytes in standard format
    pub uuid: [u8; 16],
}

impl GoalUuid {
    /// Length of the goal UUID in bytes (ROS 2 `unique_identifier_msgs/UUID`).
    pub const UUID_LEN: usize = 16;

    /// Length of any CDR length-prefix preceding the goal UUID bytes — **zero**.
    ///
    /// ROS 2 carries the goal id as `unique_identifier_msgs/UUID`, a fixed
    /// `uint8[16]` array; CDR fixed arrays have **no** length prefix, so the goal
    /// UUID sits directly after the CDR header. Pre-233.6 the action framing
    /// wrote a `u32(16)` sequence prefix here (this const was `4`), which
    /// self-matched nano-ros peers but added 4 bytes a real `rcl_action` peer
    /// rejects. Kept as a named `0` (rather than deleted) so the C/C++/Cyclone
    /// framing calcs that read `CDR_HEADER_LEN + SEQ_PREFIX_LEN + UUID_LEN` stay
    /// correct after the migration.
    pub const SEQ_PREFIX_LEN: usize = 0;

    /// Create a new GoalUuid from UUID bytes
    pub const fn new(uuid: [u8; 16]) -> Self {
        Self { uuid }
    }

    /// Create a zero/null GoalUuid
    pub const fn zero() -> Self {
        Self { uuid: [0; 16] }
    }

    /// Check if this is a zero/null GoalUuid
    pub fn is_zero(&self) -> bool {
        self.uuid == [0; 16]
    }

    /// Create a GoalUuid from a simple counter (for testing/embedded use)
    ///
    /// This creates a deterministic UUID-like identifier from a counter value.
    /// Not a true UUID, but useful for embedded systems without random number generators.
    pub fn from_counter(counter: u64) -> Self {
        let mut uuid = [0u8; 16];
        // Put counter in last 8 bytes (big-endian)
        uuid[8..16].copy_from_slice(&counter.to_be_bytes());
        // Set version 4 (random) variant bits for compatibility
        uuid[6] = (uuid[6] & 0x0f) | 0x40; // Version 4
        uuid[8] = (uuid[8] & 0x3f) | 0x80; // Variant 1
        Self { uuid }
    }
}

impl Default for GoalUuid {
    fn default() -> Self {
        Self::zero()
    }
}

impl Serialize for GoalUuid {
    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
        for byte in &self.uuid {
            writer.write_u8(*byte)?;
        }
        Ok(())
    }
}

impl Deserialize for GoalUuid {
    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
        let mut uuid = [0u8; 16];
        for byte in &mut uuid {
            *byte = reader.read_u8()?;
        }
        Ok(Self { uuid })
    }
}

impl fmt::Debug for GoalUuid {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        // Format as UUID string: xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
        write!(
            f,
            "GoalUuid({:02x}{:02x}{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}{:02x}{:02x}{:02x}{:02x})",
            self.uuid[0],
            self.uuid[1],
            self.uuid[2],
            self.uuid[3],
            self.uuid[4],
            self.uuid[5],
            self.uuid[6],
            self.uuid[7],
            self.uuid[8],
            self.uuid[9],
            self.uuid[10],
            self.uuid[11],
            self.uuid[12],
            self.uuid[13],
            self.uuid[14],
            self.uuid[15]
        )
    }
}

impl fmt::Display for GoalUuid {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(
            f,
            "{:02x}{:02x}{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}-{:02x}{:02x}{:02x}{:02x}{:02x}{:02x}",
            self.uuid[0],
            self.uuid[1],
            self.uuid[2],
            self.uuid[3],
            self.uuid[4],
            self.uuid[5],
            self.uuid[6],
            self.uuid[7],
            self.uuid[8],
            self.uuid[9],
            self.uuid[10],
            self.uuid[11],
            self.uuid[12],
            self.uuid[13],
            self.uuid[14],
            self.uuid[15]
        )
    }
}

/// Information about a goal
///
/// This matches `action_msgs/msg/GoalInfo` from ROS 2.
/// Contains the goal ID and timestamp when the goal was accepted.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
pub struct GoalInfo {
    /// Unique identifier for the goal
    pub goal_id: GoalUuid,
    /// Timestamp when the goal was accepted (nanoseconds since epoch)
    pub stamp_sec: i32,
    /// Nanosecond part of timestamp
    pub stamp_nanosec: u32,
}

impl GoalInfo {
    /// Create a new GoalInfo with the given ID and timestamp
    pub const fn new(goal_id: GoalUuid, stamp_sec: i32, stamp_nanosec: u32) -> Self {
        Self {
            goal_id,
            stamp_sec,
            stamp_nanosec,
        }
    }

    /// Create a GoalInfo with zero timestamp
    pub const fn with_id(goal_id: GoalUuid) -> Self {
        Self {
            goal_id,
            stamp_sec: 0,
            stamp_nanosec: 0,
        }
    }
}

impl Serialize for GoalInfo {
    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
        self.goal_id.serialize(writer)?;
        writer.write_i32(self.stamp_sec)?;
        writer.write_u32(self.stamp_nanosec)?;
        Ok(())
    }
}

impl Deserialize for GoalInfo {
    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
        Ok(Self {
            goal_id: GoalUuid::deserialize(reader)?,
            stamp_sec: reader.read_i32()?,
            stamp_nanosec: reader.read_u32()?,
        })
    }
}

/// Goal status with associated goal info
///
/// This matches `action_msgs/msg/GoalStatus` from ROS 2.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
pub struct GoalStatusStamped {
    /// Goal information (ID and timestamp)
    pub goal_info: GoalInfo,
    /// Current status of the goal
    pub status: GoalStatusCode,
}

impl GoalStatusStamped {
    /// Create a new GoalStatusStamped
    pub const fn new(goal_info: GoalInfo, status: GoalStatusCode) -> Self {
        Self { goal_info, status }
    }
}

impl Serialize for GoalStatusStamped {
    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
        self.goal_info.serialize(writer)?;
        writer.write_i8(self.status as i8)?;
        Ok(())
    }
}

impl Deserialize for GoalStatusStamped {
    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
        let goal_info = GoalInfo::deserialize(reader)?;
        let status_val = reader.read_i8()?;
        let status = GoalStatusCode::from_i8(status_val).unwrap_or(GoalStatusCode::Unknown);
        Ok(Self { goal_info, status })
    }
}

/// `action_msgs/srv/CancelGoal` RPC return codes.
///
/// This is the *whole-request* outcome the server writes into the
/// `CancelGoal` reply — "did the cancel RPC succeed", not "is this one goal
/// being cancelled". These codes are the wire contract, so the discriminants
/// are fixed by `action_msgs`.
///
/// Issue 0796 — this type used to be called `CancelResponse`, which is the
/// name C ([`rclc_cancel_response_t`]) and C++ ([`nros::CancelResponse`]) both
/// use for the PER-GOAL accept/reject decision. Two concepts under one name is
/// how [`CancelResponse`] ended up being the type a per-goal cancel callback
/// returned: `CancelResponse::Ok` meant "cancel this goal", which reads as an
/// RPC status and is not one. C already named them apart
/// (`rclc_cancel_response_t` vs `rclc_cancel_return_code_t`); the Rust names
/// now follow it.
///
/// [`rclc_cancel_response_t`]: https://docs.rs/nros-c
/// [`nros::CancelResponse`]: CancelResponse
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
#[repr(i8)]
pub enum CancelResponseCode {
    /// No error, goal(s) will be canceled
    #[default]
    Ok = 0,
    /// Goal was rejected (not cancelable or doesn't exist)
    Rejected = 1,
    /// Unknown goal ID
    UnknownGoal = 2,
    /// Goal is already in a terminal state
    GoalTerminated = 3,
}

impl CancelResponseCode {
    /// Convert from i8 value
    pub fn from_i8(value: i8) -> Option<Self> {
        match value {
            0 => Some(CancelResponseCode::Ok),
            1 => Some(CancelResponseCode::Rejected),
            2 => Some(CancelResponseCode::UnknownGoal),
            3 => Some(CancelResponseCode::GoalTerminated),
            _ => None,
        }
    }
}

impl Serialize for CancelResponseCode {
    fn serialize(&self, writer: &mut CdrWriter) -> Result<(), SerError> {
        writer.write_i8(*self as i8)
    }
}

impl Deserialize for CancelResponseCode {
    fn deserialize(reader: &mut CdrReader) -> Result<Self, DeserError> {
        let value = reader.read_i8()?;
        CancelResponseCode::from_i8(value).ok_or(DeserError::InvalidData)
    }
}

/// Per-goal cancel decision returned from a server's cancel callback.
///
/// The twin of [`GoalResponse`] for the cancel path: the user is asked about
/// ONE goal and answers accept or reject. It never travels on the wire — the
/// server turns the answer into a [`CancelResponseCode`] plus a `goals_canceling`
/// entry when it writes the `CancelGoal` reply.
///
/// Discriminants match C's `rclc_cancel_response_t` (`RCLC_CANCEL_REJECT` = 0,
/// `RCLC_CANCEL_ACCEPT` = 1) and C++'s `nros::CancelResponse`, so the three
/// surfaces agree. `Reject` is the default because a zeroed or unanswered
/// decision must not cancel a goal nobody asked to cancel.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
#[repr(i8)]
pub enum CancelResponse {
    /// Do not cancel this goal.
    #[default]
    Reject = 0,
    /// Cancel this goal — it transitions to [`GoalStatusCode::Canceling`].
    Accept = 1,
}

impl CancelResponse {
    /// Convert from i8 value
    pub fn from_i8(value: i8) -> Option<Self> {
        match value {
            0 => Some(CancelResponse::Reject),
            1 => Some(CancelResponse::Accept),
            _ => None,
        }
    }
}

/// Goal accept/reject response codes
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
#[repr(i8)]
pub enum GoalResponse {
    /// Goal was rejected
    #[default]
    Reject = 0,
    /// Goal was accepted and will be executed
    AcceptAndExecute = 1,
    /// Goal was accepted and is deferred
    AcceptAndDefer = 2,
}

impl GoalResponse {
    /// Convert from i8 value
    pub fn from_i8(value: i8) -> Option<Self> {
        match value {
            0 => Some(GoalResponse::Reject),
            1 => Some(GoalResponse::AcceptAndExecute),
            2 => Some(GoalResponse::AcceptAndDefer),
            _ => None,
        }
    }

    /// Check if the goal was accepted
    pub fn is_accepted(&self) -> bool {
        matches!(
            self,
            GoalResponse::AcceptAndExecute | GoalResponse::AcceptAndDefer
        )
    }
}

// phase-417 W4.b — `ActionServer<A>` and `ActionClient<A>`, two "type-level
// marker" structs each carrying `name()` / `action_type()` / `action_hash()`,
// were DELETED here. Measured reach before the deletion: ZERO references
// anywhere in the tree, and the names were UNREACHABLE through the `nros`
// facade, which re-exports `nros_node`'s live `ActionServer` / `ActionClient`
// under exactly those spellings. The ledger row
// `c:action_client_get_action_name` cited `nros_core::ActionServer::name` as
// Rust's half of the action-name accessor; it could not be called, so the
// claim was false (issue 1022's class). PR #806's precedent: in-tree-only
// reach, measured, so a hard delete rather than a deprecated forwarder.

/// The pre-phase-515 name of [`GoalUuid`].
#[deprecated(
    since = "0.6.0",
    note = "renamed to `GoalUuid`, rclrs's name (phase-515 R8)"
)]
pub type GoalId = GoalUuid;

/// The pre-phase-515 name of [`GoalStatusCode`].
#[deprecated(
    since = "0.6.0",
    note = "renamed to `GoalStatusCode`, rclrs's name (phase-515 R8)"
)]
pub type GoalStatus = GoalStatusCode;

/// The pre-phase-515 name of [`CancelResponseCode`].
#[deprecated(
    since = "0.6.0",
    note = "renamed to `CancelResponseCode`, rclrs's name (phase-515 R8)"
)]
pub type CancelReturnCode = CancelResponseCode;

#[cfg(test)]
mod tests {
    extern crate std;

    use super::*;
    use std::format;

    #[test]
    fn test_goal_status_is_terminal() {
        assert!(!GoalStatusCode::Unknown.is_terminal());
        assert!(!GoalStatusCode::Accepted.is_terminal());
        assert!(!GoalStatusCode::Executing.is_terminal());
        assert!(!GoalStatusCode::Canceling.is_terminal());
        assert!(GoalStatusCode::Succeeded.is_terminal());
        assert!(GoalStatusCode::Canceled.is_terminal());
        assert!(GoalStatusCode::Aborted.is_terminal());
    }

    #[test]
    fn test_goal_status_is_active() {
        assert!(!GoalStatusCode::Unknown.is_active());
        assert!(GoalStatusCode::Accepted.is_active());
        assert!(GoalStatusCode::Executing.is_active());
        assert!(GoalStatusCode::Canceling.is_active());
        assert!(!GoalStatusCode::Succeeded.is_active());
        assert!(!GoalStatusCode::Canceled.is_active());
        assert!(!GoalStatusCode::Aborted.is_active());
    }

    #[test]
    fn test_goal_status_from_i8() {
        assert_eq!(GoalStatusCode::from_i8(0), Some(GoalStatusCode::Unknown));
        assert_eq!(GoalStatusCode::from_i8(1), Some(GoalStatusCode::Accepted));
        assert_eq!(GoalStatusCode::from_i8(2), Some(GoalStatusCode::Executing));
        assert_eq!(GoalStatusCode::from_i8(3), Some(GoalStatusCode::Canceling));
        assert_eq!(GoalStatusCode::from_i8(4), Some(GoalStatusCode::Succeeded));
        assert_eq!(GoalStatusCode::from_i8(5), Some(GoalStatusCode::Canceled));
        assert_eq!(GoalStatusCode::from_i8(6), Some(GoalStatusCode::Aborted));
        assert_eq!(GoalStatusCode::from_i8(7), None);
        assert_eq!(GoalStatusCode::from_i8(-1), None);
    }

    #[test]
    fn test_goal_id_zero() {
        let id = GoalUuid::zero();
        assert!(id.is_zero());
        assert_eq!(id.uuid, [0; 16]);
    }

    #[test]
    fn test_goal_id_from_counter() {
        let id1 = GoalUuid::from_counter(1);
        let id2 = GoalUuid::from_counter(2);

        assert!(!id1.is_zero());
        assert!(!id2.is_zero());
        assert_ne!(id1, id2);

        // Same counter should produce same ID
        let id1_again = GoalUuid::from_counter(1);
        assert_eq!(id1, id1_again);
    }

    #[test]
    fn test_goal_id_display() {
        let id = GoalUuid::new([
            0x12, 0x34, 0x56, 0x78, 0x9a, 0xbc, 0xde, 0xf0, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66,
            0x77, 0x88,
        ]);
        let s = format!("{}", id);
        assert_eq!(s, "12345678-9abc-def0-1122-334455667788");
    }

    #[test]
    fn test_cancel_return_code_from_i8() {
        assert_eq!(CancelResponseCode::from_i8(0), Some(CancelResponseCode::Ok));
        assert_eq!(
            CancelResponseCode::from_i8(1),
            Some(CancelResponseCode::Rejected)
        );
        assert_eq!(
            CancelResponseCode::from_i8(2),
            Some(CancelResponseCode::UnknownGoal)
        );
        assert_eq!(
            CancelResponseCode::from_i8(3),
            Some(CancelResponseCode::GoalTerminated)
        );
        assert_eq!(CancelResponseCode::from_i8(4), None);
    }

    /// Issue 0796 — the per-goal decision and the RPC return code are two
    /// types now, and the thing that made the collision dangerous is that
    /// their discriminants OVERLAP with opposite meanings: 0 is "reject this
    /// goal" on one and "the RPC succeeded" on the other. A cast between them
    /// is therefore never a no-op, which is what this pins down.
    #[test]
    fn test_cancel_response_is_not_a_return_code() {
        assert_eq!(CancelResponse::from_i8(0), Some(CancelResponse::Reject));
        assert_eq!(CancelResponse::from_i8(1), Some(CancelResponse::Accept));
        assert_eq!(CancelResponse::from_i8(2), None);
        assert_eq!(CancelResponse::default(), CancelResponse::Reject);

        // Same byte, opposite verdicts.
        assert_eq!(CancelResponse::Reject as i8, CancelResponseCode::Ok as i8);
        assert_eq!(
            CancelResponse::Accept as i8,
            CancelResponseCode::Rejected as i8
        );
    }

    #[test]
    fn test_goal_response_is_accepted() {
        assert!(!GoalResponse::Reject.is_accepted());
        assert!(GoalResponse::AcceptAndExecute.is_accepted());
        assert!(GoalResponse::AcceptAndDefer.is_accepted());
    }

    #[test]
    fn test_goal_info_new() {
        let goal_id = GoalUuid::from_counter(42);
        let info = GoalInfo::new(goal_id, 123, 456);
        assert_eq!(info.goal_id, goal_id);
        assert_eq!(info.stamp_sec, 123);
        assert_eq!(info.stamp_nanosec, 456);
    }

    #[test]
    fn test_goal_info_with_id() {
        let goal_id = GoalUuid::from_counter(42);
        let info = GoalInfo::with_id(goal_id);
        assert_eq!(info.goal_id, goal_id);
        assert_eq!(info.stamp_sec, 0);
        assert_eq!(info.stamp_nanosec, 0);
    }

    #[test]
    fn test_goal_status_stamped() {
        let goal_id = GoalUuid::from_counter(1);
        let info = GoalInfo::with_id(goal_id);
        let stamped = GoalStatusStamped::new(info, GoalStatusCode::Executing);
        assert_eq!(stamped.goal_info.goal_id, goal_id);
        assert_eq!(stamped.status, GoalStatusCode::Executing);
    }

    #[test]
    fn test_goal_id_serialization() {
        use nros_serdes::{CdrReader, CdrWriter};

        let original = GoalUuid::new([
            0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, 0x0e,
            0x0f, 0x10,
        ]);

        // Serialize
        let mut buf = [0u8; 32];
        let mut writer = CdrWriter::new(&mut buf);
        original.serialize(&mut writer).unwrap();
        let len = writer.position();
        assert_eq!(len, 16); // UUID is 16 bytes

        // Deserialize
        let mut reader = CdrReader::new(&buf[..len]);
        let deserialized = GoalUuid::deserialize(&mut reader).unwrap();

        assert_eq!(original, deserialized);
    }

    #[test]
    fn test_goal_status_serialization() {
        use nros_serdes::{CdrReader, CdrWriter};

        for status in [
            GoalStatusCode::Unknown,
            GoalStatusCode::Accepted,
            GoalStatusCode::Executing,
            GoalStatusCode::Canceling,
            GoalStatusCode::Succeeded,
            GoalStatusCode::Canceled,
            GoalStatusCode::Aborted,
        ] {
            let mut buf = [0u8; 8];
            let len = {
                let mut writer = CdrWriter::new(&mut buf);
                status.serialize(&mut writer).unwrap();
                writer.position()
            };

            let mut reader = CdrReader::new(&buf[..len]);
            let deserialized = GoalStatusCode::deserialize(&mut reader).unwrap();

            assert_eq!(status, deserialized);
        }
    }

    #[test]
    fn test_goal_info_serialization() {
        use nros_serdes::{CdrReader, CdrWriter};

        let goal_id = GoalUuid::from_counter(42);
        let original = GoalInfo::new(goal_id, 1234567890, 123456789);

        // Serialize
        let mut buf = [0u8; 64];
        let mut writer = CdrWriter::new(&mut buf);
        original.serialize(&mut writer).unwrap();
        let len = writer.position();
        // UUID (16) + i32 (4) + u32 (4) = 24 bytes
        assert_eq!(len, 24);

        // Deserialize
        let mut reader = CdrReader::new(&buf[..len]);
        let deserialized = GoalInfo::deserialize(&mut reader).unwrap();

        assert_eq!(original.goal_id, deserialized.goal_id);
        assert_eq!(original.stamp_sec, deserialized.stamp_sec);
        assert_eq!(original.stamp_nanosec, deserialized.stamp_nanosec);
    }

    #[test]
    fn test_goal_status_stamped_serialization() {
        use nros_serdes::{CdrReader, CdrWriter};

        let goal_id = GoalUuid::from_counter(99);
        let goal_info = GoalInfo::new(goal_id, 987654321, 111222333);
        let original = GoalStatusStamped::new(goal_info, GoalStatusCode::Succeeded);

        // Serialize
        let mut buf = [0u8; 64];
        let mut writer = CdrWriter::new(&mut buf);
        original.serialize(&mut writer).unwrap();
        let len = writer.position();
        // GoalInfo (24) + i8 (1) = 25 bytes
        assert_eq!(len, 25);

        // Deserialize
        let mut reader = CdrReader::new(&buf[..len]);
        let deserialized = GoalStatusStamped::deserialize(&mut reader).unwrap();

        assert_eq!(original.goal_info.goal_id, deserialized.goal_info.goal_id);
        assert_eq!(
            original.goal_info.stamp_sec,
            deserialized.goal_info.stamp_sec
        );
        assert_eq!(
            original.goal_info.stamp_nanosec,
            deserialized.goal_info.stamp_nanosec
        );
        assert_eq!(original.status, deserialized.status);
    }
}

// =============================================================================
// Kani bounded model checking proofs
// =============================================================================

#[cfg(kani)]
mod verification {
    use super::*;

    // ---- GoalStatusCode ----

    #[kani::proof]
    fn goal_status_from_i8_valid_range() {
        let val: i8 = kani::any();
        let status = GoalStatusCode::from_i8(val);
        if (0..=6).contains(&val) {
            assert!(status.is_some());
        } else {
            assert!(status.is_none());
        }
    }

    #[kani::proof]
    fn goal_status_terminal_active_exclusive() {
        let val: i8 = kani::any();
        kani::assume((0..=6).contains(&val));
        let status = GoalStatusCode::from_i8(val).unwrap();
        // Terminal and active must be mutually exclusive
        assert!(!(status.is_terminal() && status.is_active()));
        // Unknown(0) is neither terminal nor active
        if val == 0 {
            assert!(!status.is_terminal());
            assert!(!status.is_active());
        }
        // Active: 1, 2, 3
        if (1..=3).contains(&val) {
            assert!(status.is_active());
            assert!(!status.is_terminal());
        }
        // Terminal: 4, 5, 6
        if (4..=6).contains(&val) {
            assert!(status.is_terminal());
            assert!(!status.is_active());
        }
    }

    #[kani::proof]
    #[kani::unwind(5)]
    fn goal_status_serialize_roundtrip() {
        let val: i8 = kani::any();
        kani::assume((0..=6).contains(&val));
        let status = GoalStatusCode::from_i8(val).unwrap();

        let mut buf = [0u8; 8];
        let len = {
            let mut writer = CdrWriter::new(&mut buf);
            status.serialize(&mut writer).unwrap();
            writer.position()
        };

        let mut reader = CdrReader::new(&buf[..len]);
        let deserialized = GoalStatusCode::deserialize(&mut reader).unwrap();
        assert_eq!(status, deserialized);
    }

    // ---- GoalResponse ----

    #[kani::proof]
    fn goal_response_from_i8_valid_range() {
        let val: i8 = kani::any();
        let resp = GoalResponse::from_i8(val);
        if (0..=2).contains(&val) {
            assert!(resp.is_some());
        } else {
            assert!(resp.is_none());
        }
    }

    #[kani::proof]
    fn goal_response_is_accepted_consistent() {
        let val: i8 = kani::any();
        kani::assume((0..=2).contains(&val));
        let resp = GoalResponse::from_i8(val).unwrap();
        // Reject(0) → not accepted; AcceptAndExecute(1), AcceptAndDefer(2) → accepted
        assert_eq!(resp.is_accepted(), val >= 1);
    }

    // ---- CancelResponseCode ----

    #[kani::proof]
    fn cancel_return_code_from_i8_valid_range() {
        let val: i8 = kani::any();
        let resp = CancelResponseCode::from_i8(val);
        if (0..=3).contains(&val) {
            assert!(resp.is_some());
        } else {
            assert!(resp.is_none());
        }
    }

    // ---- CancelResponse ----

    #[kani::proof]
    fn cancel_response_from_i8_valid_range() {
        let val: i8 = kani::any();
        let resp = CancelResponse::from_i8(val);
        if (0..=1).contains(&val) {
            assert!(resp.is_some());
        } else {
            assert!(resp.is_none());
        }
    }

    // ---- GoalUuid ----

    #[kani::proof]
    fn goal_id_zero_is_zero() {
        let id = GoalUuid::zero();
        assert!(id.is_zero());
    }

    #[kani::proof]
    fn goal_id_from_counter_deterministic() {
        let counter: u64 = kani::any();
        // Constrain for CBMC tractability (exercises same byte/bit logic)
        kani::assume(counter <= 1_000_000);
        let id1 = GoalUuid::from_counter(counter);
        let id2 = GoalUuid::from_counter(counter);
        assert_eq!(id1, id2);
    }

    #[kani::proof]
    fn goal_id_from_counter_not_zero() {
        let counter: u64 = kani::any();
        kani::assume(counter > 0 && counter <= 1_000_000);
        let id = GoalUuid::from_counter(counter);
        assert!(!id.is_zero());
    }

    #[kani::proof]
    #[kani::unwind(20)]
    fn goal_id_serialize_roundtrip() {
        let mut uuid = [0u8; 16];
        // Use a few arbitrary bytes (bounded for tractability)
        uuid[0] = kani::any();
        uuid[7] = kani::any();
        uuid[15] = kani::any();
        let id = GoalUuid::new(uuid);

        let mut buf = [0u8; 32];
        let len = {
            let mut writer = CdrWriter::new(&mut buf);
            id.serialize(&mut writer).unwrap();
            writer.position()
        };

        let mut reader = CdrReader::new(&buf[..len]);
        let deserialized = GoalUuid::deserialize(&mut reader).unwrap();
        assert_eq!(id, deserialized);
    }
}