Skip to main content

nros_params/
types.rs

1//! Parameter types for ROS 2 compatible parameter handling
2//!
3//! This module provides types for representing ROS 2 parameters including
4//! scalar values, arrays, and parameter descriptors.
5
6use heapless::{String, Vec};
7
8#[cfg(feature = "std")]
9use std::string::ToString;
10
11pub use crate::config::*;
12
13/// ROS 2 parameter types
14///
15/// These match the parameter types defined in rcl_interfaces/msg/ParameterType
16#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
17#[repr(u8)]
18pub enum ParameterType {
19    /// Parameter value not set
20    #[default]
21    NotSet = 0,
22    /// Boolean parameter
23    Bool = 1,
24    /// 64-bit signed integer parameter
25    Integer = 2,
26    /// 64-bit floating point parameter
27    Double = 3,
28    /// String parameter
29    String = 4,
30    /// Byte array parameter
31    ByteArray = 5,
32    /// Boolean array parameter
33    BoolArray = 6,
34    /// Integer array parameter
35    IntegerArray = 7,
36    /// Double array parameter
37    DoubleArray = 8,
38    /// String array parameter
39    StringArray = 9,
40}
41
42/// Parameter value container
43///
44/// Holds a parameter value of any supported type.
45/// Note: This enum is intentionally large to support all parameter types
46/// without heap allocation in embedded systems.
47#[derive(Debug, Clone, Default)]
48#[allow(clippy::large_enum_variant)]
49pub enum ParameterValue {
50    /// Value not set
51    #[default]
52    NotSet,
53    /// Boolean value
54    Bool(bool),
55    /// 64-bit signed integer value
56    Integer(i64),
57    /// 64-bit floating point value
58    Double(f64),
59    /// String value
60    String(String<MAX_STRING_VALUE_LEN>),
61    /// Byte array value
62    ByteArray(Vec<u8, MAX_BYTE_ARRAY_LEN>),
63    /// Boolean array value
64    BoolArray(Vec<bool, MAX_ARRAY_LEN>),
65    /// Integer array value
66    IntegerArray(Vec<i64, MAX_ARRAY_LEN>),
67    /// Double array value
68    DoubleArray(Vec<f64, MAX_ARRAY_LEN>),
69    /// String array value (array of fixed-size strings)
70    StringArray(Vec<String<MAX_STRING_VALUE_LEN>, MAX_ARRAY_LEN>),
71}
72
73impl ParameterValue {
74    /// Get the parameter type for this value
75    pub fn param_type(&self) -> ParameterType {
76        match self {
77            Self::NotSet => ParameterType::NotSet,
78            Self::Bool(_) => ParameterType::Bool,
79            Self::Integer(_) => ParameterType::Integer,
80            Self::Double(_) => ParameterType::Double,
81            Self::String(_) => ParameterType::String,
82            Self::ByteArray(_) => ParameterType::ByteArray,
83            Self::BoolArray(_) => ParameterType::BoolArray,
84            Self::IntegerArray(_) => ParameterType::IntegerArray,
85            Self::DoubleArray(_) => ParameterType::DoubleArray,
86            Self::StringArray(_) => ParameterType::StringArray,
87        }
88    }
89
90    /// Check if the value is set
91    pub fn is_set(&self) -> bool {
92        !matches!(self, Self::NotSet)
93    }
94
95    /// Try to get the value as a bool
96    pub fn as_bool(&self) -> Option<bool> {
97        match self {
98            Self::Bool(v) => Some(*v),
99            _ => None,
100        }
101    }
102
103    /// Try to get the value as an integer
104    pub fn as_integer(&self) -> Option<i64> {
105        match self {
106            Self::Integer(v) => Some(*v),
107            _ => None,
108        }
109    }
110
111    /// Try to get the value as a double
112    pub fn as_double(&self) -> Option<f64> {
113        match self {
114            Self::Double(v) => Some(*v),
115            _ => None,
116        }
117    }
118
119    /// Try to get the value as a string slice
120    pub fn as_string(&self) -> Option<&str> {
121        match self {
122            Self::String(v) => Some(v.as_str()),
123            _ => None,
124        }
125    }
126
127    /// Try to get the value as a byte array slice
128    pub fn as_byte_array(&self) -> Option<&[u8]> {
129        match self {
130            Self::ByteArray(v) => Some(v.as_slice()),
131            _ => None,
132        }
133    }
134
135    /// Try to get the value as a bool array slice
136    pub fn as_bool_array(&self) -> Option<&[bool]> {
137        match self {
138            Self::BoolArray(v) => Some(v.as_slice()),
139            _ => None,
140        }
141    }
142
143    /// Try to get the value as an integer array slice
144    pub fn as_integer_array(&self) -> Option<&[i64]> {
145        match self {
146            Self::IntegerArray(v) => Some(v.as_slice()),
147            _ => None,
148        }
149    }
150
151    /// Try to get the value as a double array slice
152    pub fn as_double_array(&self) -> Option<&[f64]> {
153        match self {
154            Self::DoubleArray(v) => Some(v.as_slice()),
155            _ => None,
156        }
157    }
158
159    /// Create a bool value
160    pub fn from_bool(value: bool) -> Self {
161        Self::Bool(value)
162    }
163
164    /// Create an integer value
165    pub fn from_integer(value: i64) -> Self {
166        Self::Integer(value)
167    }
168
169    /// Create a double value
170    pub fn from_double(value: f64) -> Self {
171        Self::Double(value)
172    }
173
174    /// Create a string value from a str slice
175    pub fn from_string(value: &str) -> Option<Self> {
176        let mut s = String::new();
177        s.push_str(value).ok()?;
178        Some(Self::String(s))
179    }
180}
181
182/// Floating point range constraints for parameters
183#[derive(Debug, Clone, Copy, Default)]
184pub struct FloatingPointRange {
185    /// Minimum allowed value (inclusive)
186    pub min: f64,
187    /// Maximum allowed value (inclusive)
188    pub max: f64,
189    /// Step size for value changes (0 = any step allowed)
190    pub step: f64,
191}
192
193impl FloatingPointRange {
194    /// Create a new floating point range
195    pub const fn new(min: f64, max: f64, step: f64) -> Self {
196        Self { min, max, step }
197    }
198
199    /// Check if a value is within this range
200    pub fn contains(&self, value: f64) -> bool {
201        value >= self.min && value <= self.max
202    }
203}
204
205/// Integer range constraints for parameters
206#[derive(Debug, Clone, Copy, Default)]
207pub struct IntegerRange {
208    /// Minimum allowed value (inclusive)
209    pub min: i64,
210    /// Maximum allowed value (inclusive)
211    pub max: i64,
212    /// Step size for value changes (0 = any step allowed)
213    pub step: i64,
214}
215
216impl IntegerRange {
217    /// Create a new integer range
218    pub const fn new(min: i64, max: i64, step: i64) -> Self {
219        Self { min, max, step }
220    }
221
222    /// Check if a value is within this range
223    pub fn contains(&self, value: i64) -> bool {
224        value >= self.min && value <= self.max
225    }
226}
227
228/// Range constraints for a parameter
229#[derive(Debug, Clone, Copy, Default)]
230pub enum ParameterRange {
231    /// No range constraints
232    #[default]
233    None,
234    /// Floating point range
235    FloatingPoint(FloatingPointRange),
236    /// Integer range
237    Integer(IntegerRange),
238}
239
240/// Parameter descriptor containing metadata
241///
242/// Describes a parameter including its type, constraints, and documentation.
243#[derive(Debug, Clone)]
244pub struct ParameterDescriptor {
245    /// Parameter name
246    pub name: String<MAX_PARAM_NAME_LEN>,
247    /// Parameter type
248    pub param_type: ParameterType,
249    /// Human-readable description
250    pub description: String<MAX_STRING_VALUE_LEN>,
251    /// Whether the parameter is read-only
252    pub read_only: bool,
253    /// Whether the parameter type can change dynamically
254    pub dynamic_typing: bool,
255    /// Range constraints
256    pub range: ParameterRange,
257}
258
259impl ParameterDescriptor {
260    /// Create a new parameter descriptor
261    pub fn new(name: &str, param_type: ParameterType) -> Option<Self> {
262        let mut n = String::new();
263        n.push_str(name).ok()?;
264        Some(Self {
265            name: n,
266            param_type,
267            description: String::new(),
268            read_only: false,
269            dynamic_typing: false,
270            range: ParameterRange::None,
271        })
272    }
273
274    /// Set the description
275    pub fn with_description(mut self, desc: &str) -> Self {
276        self.description.clear();
277        let _ = self.description.push_str(desc);
278        self
279    }
280
281    /// Set read-only flag
282    pub fn with_read_only(mut self, read_only: bool) -> Self {
283        self.read_only = read_only;
284        self
285    }
286
287    /// Set dynamic typing flag
288    pub fn with_dynamic_typing(mut self, dynamic: bool) -> Self {
289        self.dynamic_typing = dynamic;
290        self
291    }
292
293    /// Set integer range constraints
294    pub fn with_integer_range(mut self, min: i64, max: i64, step: i64) -> Self {
295        self.range = ParameterRange::Integer(IntegerRange::new(min, max, step));
296        self
297    }
298
299    /// Set floating point range constraints
300    pub fn with_float_range(mut self, min: f64, max: f64, step: f64) -> Self {
301        self.range = ParameterRange::FloatingPoint(FloatingPointRange::new(min, max, step));
302        self
303    }
304
305    /// Check if a value satisfies the range constraints
306    pub fn validate_range(&self, value: &ParameterValue) -> bool {
307        match (&self.range, value) {
308            (ParameterRange::None, _) => true,
309            (ParameterRange::Integer(range), ParameterValue::Integer(v)) => range.contains(*v),
310            (ParameterRange::FloatingPoint(range), ParameterValue::Double(v)) => range.contains(*v),
311            _ => true,
312        }
313    }
314}
315
316/// A named parameter with value and optional descriptor
317#[derive(Debug, Clone)]
318pub struct Parameter {
319    /// Parameter name
320    pub name: String<MAX_PARAM_NAME_LEN>,
321    /// Parameter value
322    pub value: ParameterValue,
323}
324
325impl Parameter {
326    /// Create a new parameter with a value
327    pub fn new(name: &str, value: ParameterValue) -> Option<Self> {
328        let mut n = String::new();
329        n.push_str(name).ok()?;
330        Some(Self { name: n, value })
331    }
332
333    /// Create a new boolean parameter
334    pub fn bool(name: &str, value: bool) -> Option<Self> {
335        Self::new(name, ParameterValue::Bool(value))
336    }
337
338    /// Create a new integer parameter
339    pub fn integer(name: &str, value: i64) -> Option<Self> {
340        Self::new(name, ParameterValue::Integer(value))
341    }
342
343    /// Create a new double parameter
344    pub fn double(name: &str, value: f64) -> Option<Self> {
345        Self::new(name, ParameterValue::Double(value))
346    }
347
348    /// Create a new string parameter
349    pub fn string(name: &str, value: &str) -> Option<Self> {
350        Self::new(name, ParameterValue::from_string(value)?)
351    }
352
353    /// Get the parameter type
354    pub fn param_type(&self) -> ParameterType {
355        self.value.param_type()
356    }
357
358    /// Get the parameter name
359    pub fn name(&self) -> &str {
360        &self.name
361    }
362}
363
364/// Result of setting a parameter
365#[derive(Debug, Clone, Copy, PartialEq, Eq)]
366pub enum SetParameterResult {
367    /// Parameter was set successfully
368    Success,
369    /// Parameter is read-only
370    ReadOnly,
371    /// Parameter type mismatch (and dynamic typing disabled)
372    TypeMismatch,
373    /// Value is outside allowed range
374    OutOfRange,
375    /// Parameter not found
376    NotFound,
377    /// Storage is full
378    StorageFull,
379}
380
381impl SetParameterResult {
382    /// Check if the result indicates success
383    pub fn is_success(&self) -> bool {
384        matches!(self, Self::Success)
385    }
386}
387
388/// Trait for types that can be used as typed parameters
389///
390/// This trait provides conversions between Rust types and ParameterValue,
391/// enabling type-safe parameter access.
392pub trait ParameterVariant: Clone {
393    /// Convert this type to a ParameterValue
394    fn to_parameter_value(&self) -> ParameterValue;
395
396    /// Try to extract this type from a ParameterValue
397    fn from_parameter_value(value: &ParameterValue) -> Option<Self>;
398
399    /// Get the expected parameter type
400    fn parameter_type() -> ParameterType;
401}
402
403// Implement ParameterVariant for basic types
404
405impl ParameterVariant for bool {
406    fn to_parameter_value(&self) -> ParameterValue {
407        ParameterValue::Bool(*self)
408    }
409
410    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
411        value.as_bool()
412    }
413
414    fn parameter_type() -> ParameterType {
415        ParameterType::Bool
416    }
417}
418
419impl ParameterVariant for i64 {
420    fn to_parameter_value(&self) -> ParameterValue {
421        ParameterValue::Integer(*self)
422    }
423
424    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
425        value.as_integer()
426    }
427
428    fn parameter_type() -> ParameterType {
429        ParameterType::Integer
430    }
431}
432
433impl ParameterVariant for f64 {
434    fn to_parameter_value(&self) -> ParameterValue {
435        ParameterValue::Double(*self)
436    }
437
438    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
439        value.as_double()
440    }
441
442    fn parameter_type() -> ParameterType {
443        ParameterType::Double
444    }
445}
446
447// For strings, we implement ParameterVariant for heapless::String (no_std)
448#[cfg(not(feature = "std"))]
449impl ParameterVariant for String<MAX_STRING_VALUE_LEN> {
450    fn to_parameter_value(&self) -> ParameterValue {
451        ParameterValue::String(self.clone())
452    }
453
454    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
455        if let ParameterValue::String(s) = value {
456            Some(s.clone())
457        } else {
458            None
459        }
460    }
461
462    fn parameter_type() -> ParameterType {
463        ParameterType::String
464    }
465}
466
467// Implement ParameterVariant for std::string::String (std)
468#[cfg(feature = "std")]
469impl ParameterVariant for std::string::String {
470    fn to_parameter_value(&self) -> ParameterValue {
471        ParameterValue::from_string(self.as_str()).unwrap_or_default()
472    }
473
474    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
475        value.as_string().map(|s| s.to_string())
476    }
477
478    fn parameter_type() -> ParameterType {
479        ParameterType::String
480    }
481}
482
483// Implement ParameterVariant for std::vec::Vec<i64> (std)
484#[cfg(feature = "std")]
485impl ParameterVariant for std::vec::Vec<i64> {
486    fn to_parameter_value(&self) -> ParameterValue {
487        ParameterValue::IntegerArray(Vec::from_slice(self.as_slice()).unwrap_or_default())
488    }
489
490    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
491        value.as_integer_array().map(|v| v.to_vec())
492    }
493
494    fn parameter_type() -> ParameterType {
495        ParameterType::IntegerArray
496    }
497}
498
499// Implement ParameterVariant for std::vec::Vec<f64> (std)
500#[cfg(feature = "std")]
501impl ParameterVariant for std::vec::Vec<f64> {
502    fn to_parameter_value(&self) -> ParameterValue {
503        ParameterValue::DoubleArray(Vec::from_slice(self.as_slice()).unwrap_or_default())
504    }
505
506    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
507        value.as_double_array().map(|v| v.to_vec())
508    }
509
510    fn parameter_type() -> ParameterType {
511        ParameterType::DoubleArray
512    }
513}
514
515// Implement ParameterVariant for std::vec::Vec<bool> (std)
516#[cfg(feature = "std")]
517impl ParameterVariant for std::vec::Vec<bool> {
518    fn to_parameter_value(&self) -> ParameterValue {
519        ParameterValue::BoolArray(Vec::from_slice(self.as_slice()).unwrap_or_default())
520    }
521
522    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
523        value.as_bool_array().map(|v| v.to_vec())
524    }
525
526    fn parameter_type() -> ParameterType {
527        ParameterType::BoolArray
528    }
529}
530
531// Implement ParameterVariant for std::vec::Vec<std::string::String> (std)
532#[cfg(feature = "std")]
533impl ParameterVariant for std::vec::Vec<std::string::String> {
534    fn to_parameter_value(&self) -> ParameterValue {
535        let mut vec = Vec::new();
536        for s in self {
537            let mut h_string = String::new();
538            if h_string.push_str(s.as_str()).is_ok() {
539                let _ = vec.push(h_string);
540            }
541        }
542        ParameterValue::StringArray(vec)
543    }
544
545    fn from_parameter_value(value: &ParameterValue) -> Option<Self> {
546        if let ParameterValue::StringArray(v) = value {
547            Some(v.iter().map(|s| s.as_str().to_string()).collect())
548        } else {
549            None
550        }
551    }
552
553    fn parameter_type() -> ParameterType {
554        ParameterType::StringArray
555    }
556}
557
558#[cfg(test)]
559mod tests {
560    use super::*;
561
562    #[test]
563    #[allow(clippy::approx_constant)]
564    fn test_parameter_value_types() {
565        let bool_val = ParameterValue::Bool(true);
566        assert_eq!(bool_val.param_type(), ParameterType::Bool);
567        assert_eq!(bool_val.as_bool(), Some(true));
568
569        let int_val = ParameterValue::Integer(42);
570        assert_eq!(int_val.param_type(), ParameterType::Integer);
571        assert_eq!(int_val.as_integer(), Some(42));
572
573        let double_val = ParameterValue::Double(3.14);
574        assert_eq!(double_val.param_type(), ParameterType::Double);
575        assert_eq!(double_val.as_double(), Some(3.14));
576    }
577
578    #[test]
579    fn test_parameter_value_string() {
580        let string_val = ParameterValue::from_string("hello").unwrap();
581        assert_eq!(string_val.param_type(), ParameterType::String);
582        assert_eq!(string_val.as_string(), Some("hello"));
583    }
584
585    #[test]
586    fn test_parameter_creation() {
587        let param = Parameter::bool("my_param", true).unwrap();
588        assert_eq!(param.name(), "my_param");
589        assert_eq!(param.param_type(), ParameterType::Bool);
590        assert_eq!(param.value.as_bool(), Some(true));
591    }
592
593    #[test]
594    fn test_parameter_descriptor() {
595        let desc = ParameterDescriptor::new("speed", ParameterType::Double)
596            .unwrap()
597            .with_description("Maximum speed in m/s")
598            .with_float_range(0.0, 10.0, 0.1);
599
600        assert_eq!(desc.name.as_str(), "speed");
601        assert_eq!(desc.param_type, ParameterType::Double);
602        assert!(!desc.read_only);
603
604        // Test range validation
605        assert!(desc.validate_range(&ParameterValue::Double(5.0)));
606        assert!(!desc.validate_range(&ParameterValue::Double(15.0)));
607    }
608
609    #[test]
610    fn test_integer_range() {
611        let range = IntegerRange::new(0, 100, 1);
612        assert!(range.contains(50));
613        assert!(range.contains(0));
614        assert!(range.contains(100));
615        assert!(!range.contains(-1));
616        assert!(!range.contains(101));
617    }
618
619    #[test]
620    fn test_set_result() {
621        assert!(SetParameterResult::Success.is_success());
622        assert!(!SetParameterResult::ReadOnly.is_success());
623    }
624}
625
626// =============================================================================
627// Ghost model validation
628// =============================================================================
629
630#[cfg(test)]
631mod ghost_checks {
632    use super::*;
633    use nros_ghost_types::ParameterValueGhost;
634
635    /// Structural check: exhaustive match maps all 10 variants.
636    /// If a variant is added or removed, this fails to compile.
637    fn ghost_from_value(v: &ParameterValue) -> ParameterValueGhost {
638        match v {
639            ParameterValue::NotSet => ParameterValueGhost::NotSet,
640            ParameterValue::Bool(b) => ParameterValueGhost::Bool(*b),
641            ParameterValue::Integer(i) => ParameterValueGhost::Integer(*i),
642            ParameterValue::Double(_) => ParameterValueGhost::Double,
643            ParameterValue::String(_) => ParameterValueGhost::String,
644            ParameterValue::ByteArray(_) => ParameterValueGhost::ByteArray,
645            ParameterValue::BoolArray(_) => ParameterValueGhost::BoolArray,
646            ParameterValue::IntegerArray(_) => ParameterValueGhost::IntegerArray,
647            ParameterValue::DoubleArray(_) => ParameterValueGhost::DoubleArray,
648            ParameterValue::StringArray(_) => ParameterValueGhost::StringArray,
649        }
650    }
651
652    #[test]
653    fn ghost_variant_coverage() {
654        // Exhaustive match compiles — all 10 variants exist in both types
655        let _ = ghost_from_value(&ParameterValue::NotSet);
656        let _ = ghost_from_value(&ParameterValue::Bool(true));
657        let _ = ghost_from_value(&ParameterValue::Integer(0));
658        let _ = ghost_from_value(&ParameterValue::Double(0.0));
659        let _ = ghost_from_value(&ParameterValue::String(String::new()));
660        let _ = ghost_from_value(&ParameterValue::ByteArray(Vec::new()));
661        let _ = ghost_from_value(&ParameterValue::BoolArray(Vec::new()));
662        let _ = ghost_from_value(&ParameterValue::IntegerArray(Vec::new()));
663        let _ = ghost_from_value(&ParameterValue::DoubleArray(Vec::new()));
664        let _ = ghost_from_value(&ParameterValue::StringArray(Vec::new()));
665    }
666
667    #[test]
668    fn ghost_bool_preserves() {
669        let ghost = ghost_from_value(&ParameterValue::Bool(true));
670        assert!(matches!(ghost, ParameterValueGhost::Bool(true)));
671    }
672
673    #[test]
674    fn ghost_integer_preserves() {
675        let ghost = ghost_from_value(&ParameterValue::Integer(42));
676        assert!(matches!(ghost, ParameterValueGhost::Integer(42)));
677    }
678}
679
680// =============================================================================
681// Kani bounded model checking proofs
682// =============================================================================
683
684#[cfg(kani)]
685mod verification {
686    use super::*;
687
688    // ---- ParameterValue type conversions ----
689
690    #[kani::proof]
691    fn parameter_i64_roundtrip() {
692        let val: i64 = kani::any();
693        let pv = ParameterValue::from_integer(val);
694        assert_eq!(pv.as_integer(), Some(val));
695        assert_eq!(pv.param_type(), ParameterType::Integer);
696        assert!(pv.is_set());
697    }
698
699    #[kani::proof]
700    fn parameter_bool_roundtrip() {
701        let val: bool = kani::any();
702        let pv = ParameterValue::from_bool(val);
703        assert_eq!(pv.as_bool(), Some(val));
704        assert_eq!(pv.param_type(), ParameterType::Bool);
705        assert!(pv.is_set());
706    }
707
708    #[kani::proof]
709    fn parameter_double_roundtrip() {
710        let val: f64 = kani::any();
711        let pv = ParameterValue::from_double(val);
712        let result = pv.as_double();
713        assert!(result.is_some());
714        assert_eq!(result.unwrap().to_bits(), val.to_bits());
715        assert_eq!(pv.param_type(), ParameterType::Double);
716    }
717
718    #[kani::proof]
719    fn parameter_not_set_default() {
720        let pv = ParameterValue::default();
721        assert!(!pv.is_set());
722        assert_eq!(pv.param_type(), ParameterType::NotSet);
723        assert!(pv.as_bool().is_none());
724        assert!(pv.as_integer().is_none());
725        assert!(pv.as_double().is_none());
726        assert!(pv.as_string().is_none());
727    }
728
729    // ---- Type mismatch returns None ----
730
731    #[kani::proof]
732    fn parameter_type_mismatch_bool() {
733        let val: i64 = kani::any();
734        let pv = ParameterValue::from_integer(val);
735        assert!(pv.as_bool().is_none());
736        assert!(pv.as_double().is_none());
737        assert!(pv.as_string().is_none());
738    }
739
740    #[kani::proof]
741    fn parameter_type_mismatch_integer() {
742        let val: bool = kani::any();
743        let pv = ParameterValue::from_bool(val);
744        assert!(pv.as_integer().is_none());
745        assert!(pv.as_double().is_none());
746        assert!(pv.as_string().is_none());
747    }
748
749    // ---- IntegerRange ----
750
751    #[kani::proof]
752    fn integer_range_contains_bounds() {
753        let min: i64 = kani::any();
754        let max: i64 = kani::any();
755        // Constrain to bounded range to avoid subtraction overflow
756        kani::assume(min >= -1_000_000 && min <= 1_000_000);
757        kani::assume(max >= -1_000_000 && max <= 1_000_000);
758        kani::assume(min <= max);
759        let range = IntegerRange::new(min, max, 1);
760        // Endpoints must be contained
761        assert!(range.contains(min));
762        assert!(range.contains(max));
763    }
764
765    #[kani::proof]
766    fn integer_range_outside_bounds() {
767        let min: i64 = kani::any();
768        let max: i64 = kani::any();
769        kani::assume(min <= max);
770        kani::assume(min > i64::MIN); // So min-1 doesn't overflow
771        kani::assume(max < i64::MAX); // So max+1 doesn't overflow
772        let range = IntegerRange::new(min, max, 1);
773        assert!(!range.contains(min - 1));
774        assert!(!range.contains(max + 1));
775    }
776
777    // ---- FloatingPointRange ----
778
779    #[kani::proof]
780    fn float_range_contains_bounds() {
781        let min: f64 = kani::any();
782        let max: f64 = kani::any();
783        kani::assume(!min.is_nan() && !max.is_nan());
784        kani::assume(min <= max);
785        let range = FloatingPointRange::new(min, max, 0.0);
786        assert!(range.contains(min));
787        assert!(range.contains(max));
788    }
789
790    // ---- SetParameterResult ----
791
792    #[kani::proof]
793    fn set_result_success_only() {
794        // Only Success should return true from is_success()
795        assert!(SetParameterResult::Success.is_success());
796        assert!(!SetParameterResult::ReadOnly.is_success());
797        assert!(!SetParameterResult::TypeMismatch.is_success());
798        assert!(!SetParameterResult::OutOfRange.is_success());
799        assert!(!SetParameterResult::NotFound.is_success());
800        assert!(!SetParameterResult::StorageFull.is_success());
801    }
802}