1use crate::types::RosMessage;
35use core::fmt;
36use nros_serdes::{CdrReader, CdrWriter, DeserError, Deserialize, SerError, Serialize};
37
38pub trait RosAction: Sized {
54 type Goal: RosMessage;
56
57 type Result: RosMessage + Default;
59
60 type Feedback: RosMessage;
62
63 type SendGoalRequest: RosMessage;
65
66 type SendGoalResponse: RosMessage;
68
69 type GetResultRequest: RosMessage;
71
72 type GetResultResponse: RosMessage;
74
75 type FeedbackMessage: RosMessage;
77
78 const ACTION_NAME: &'static str;
80
81 const ACTION_HASH: &'static str;
83
84 const SEND_GOAL_SERVICE_HASH: &'static str = Self::ACTION_HASH;
93
94 const GET_RESULT_SERVICE_HASH: &'static str = Self::ACTION_HASH;
97
98 #[allow(clippy::result_unit_err)]
114 fn register_protocol_types() -> Result<(), ()> {
115 Ok(())
116 }
117}
118
119#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
124#[repr(i8)]
125pub enum GoalStatus {
126 #[default]
128 Unknown = 0,
129 Accepted = 1,
131 Executing = 2,
133 Canceling = 3,
135 Succeeded = 4,
137 Canceled = 5,
139 Aborted = 6,
141}
142
143impl GoalStatus {
144 pub fn is_terminal(&self) -> bool {
146 matches!(
147 self,
148 GoalStatus::Succeeded | GoalStatus::Canceled | GoalStatus::Aborted
149 )
150 }
151
152 pub fn is_active(&self) -> bool {
154 matches!(
155 self,
156 GoalStatus::Accepted | GoalStatus::Executing | GoalStatus::Canceling
157 )
158 }
159
160 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#[derive(Clone, Copy, PartialEq, Eq, Hash)]
206pub struct GoalId {
207 pub uuid: [u8; 16],
209}
210
211impl GoalId {
212 pub const UUID_LEN: usize = 16;
214
215 pub const SEQ_PREFIX_LEN: usize = 0;
226
227 pub const fn new(uuid: [u8; 16]) -> Self {
229 Self { uuid }
230 }
231
232 pub const fn zero() -> Self {
234 Self { uuid: [0; 16] }
235 }
236
237 pub fn is_zero(&self) -> bool {
239 self.uuid == [0; 16]
240 }
241
242 pub fn from_counter(counter: u64) -> Self {
247 let mut uuid = [0u8; 16];
248 uuid[8..16].copy_from_slice(&counter.to_be_bytes());
250 uuid[6] = (uuid[6] & 0x0f) | 0x40; uuid[8] = (uuid[8] & 0x3f) | 0x80; 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 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#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
338pub struct GoalInfo {
339 pub goal_id: GoalId,
341 pub stamp_sec: i32,
343 pub stamp_nanosec: u32,
345}
346
347impl GoalInfo {
348 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 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#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
390pub struct GoalStatusStamped {
391 pub goal_info: GoalInfo,
393 pub status: GoalStatus,
395}
396
397impl GoalStatusStamped {
398 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#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
440#[repr(i8)]
441pub enum CancelReturnCode {
442 #[default]
444 Ok = 0,
445 Rejected = 1,
447 UnknownGoal = 2,
449 GoalTerminated = 3,
451}
452
453impl CancelReturnCode {
454 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#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
491#[repr(i8)]
492pub enum CancelResponse {
493 #[default]
495 Reject = 0,
496 Accept = 1,
498}
499
500impl CancelResponse {
501 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#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
513#[repr(i8)]
514pub enum GoalResponse {
515 #[default]
517 Reject = 0,
518 AcceptAndExecute = 1,
520 AcceptAndDefer = 2,
522}
523
524impl GoalResponse {
525 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 pub fn is_accepted(&self) -> bool {
537 matches!(
538 self,
539 GoalResponse::AcceptAndExecute | GoalResponse::AcceptAndDefer
540 )
541 }
542}
543
544pub struct ActionServer<A: RosAction> {
549 pub name: &'static str,
551 _marker: core::marker::PhantomData<A>,
553}
554
555impl<A: RosAction> ActionServer<A> {
556 pub fn new(name: &'static str) -> Self {
558 Self {
559 name,
560 _marker: core::marker::PhantomData,
561 }
562 }
563
564 pub fn name(&self) -> &str {
566 self.name
567 }
568
569 pub fn action_type(&self) -> &'static str {
571 A::ACTION_NAME
572 }
573
574 pub fn action_hash(&self) -> &'static str {
576 A::ACTION_HASH
577 }
578}
579
580pub struct ActionClient<A: RosAction> {
585 pub name: &'static str,
587 _marker: core::marker::PhantomData<A>,
589}
590
591impl<A: RosAction> ActionClient<A> {
592 pub fn new(name: &'static str) -> Self {
594 Self {
595 name,
596 _marker: core::marker::PhantomData,
597 }
598 }
599
600 pub fn name(&self) -> &str {
602 self.name
603 }
604
605 pub fn action_type(&self) -> &'static str {
607 A::ACTION_NAME
608 }
609
610 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 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 #[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 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 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); 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 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 assert_eq!(len, 24);
825
826 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 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 assert_eq!(len, 25);
850
851 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#[cfg(kani)]
873mod verification {
874 use super::*;
875
876 #[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 assert!(!(status.is_terminal() && status.is_active()));
896 if val == 0 {
898 assert!(!status.is_terminal());
899 assert!(!status.is_active());
900 }
901 if (1..=3).contains(&val) {
903 assert!(status.is_active());
904 assert!(!status.is_terminal());
905 }
906 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 #[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 assert_eq!(resp.is_accepted(), val >= 1);
952 }
953
954 #[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 #[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 #[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 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 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}