nros_params/
server.rs

1//! Parameter server implementation
2//!
3//! Provides a static storage parameter server for embedded systems.
4//! Parameters are stored in a fixed-size array with compile-time capacity.
5
6use crate::types::{
7    MAX_PARAM_NAME_LEN, Parameter, ParameterDescriptor, ParameterType, ParameterValue,
8    SetParameterResult,
9};
10use heapless::String;
11
12// MAX_PARAMETERS is generated by build.rs and included via types.rs.
13use crate::types::MAX_PARAMETERS;
14
15/// Entry in the parameter storage
16#[derive(Debug, Clone)]
17struct ParameterEntry {
18    /// The parameter (name + value)
19    param: Parameter,
20    /// Optional descriptor with constraints
21    descriptor: Option<ParameterDescriptor>,
22}
23
24/// Parameter server with static storage
25///
26/// Stores parameters in a fixed-size array. The capacity is determined
27/// at compile time via the `MAX_PARAMETERS` constant.
28///
29/// # Example
30///
31/// ```
32/// use nros_params::{ParameterServer, ParameterValue};
33///
34/// let mut server = ParameterServer::new();
35///
36/// // Declare a parameter with initial value
37/// server.declare("max_speed", ParameterValue::Double(1.0));
38///
39/// // Get parameter value
40/// if let Some(value) = server.get("max_speed") {
41///     println!("max_speed = {:?}", value.as_double());
42/// }
43///
44/// // Set parameter value
45/// server.set("max_speed", ParameterValue::Double(2.0));
46/// ```
47pub struct ParameterServer {
48    /// Parameter storage
49    entries: [Option<ParameterEntry>; MAX_PARAMETERS],
50    /// Number of parameters currently stored
51    count: usize,
52    /// Phase 172.H — set whenever a value changes via [`set`](Self::set) /
53    /// [`unset`](Self::unset), so the persistence layer flushes only after a
54    /// real change. Declaring defaults does not dirty the server.
55    dirty: bool,
56}
57
58impl Default for ParameterServer {
59    fn default() -> Self {
60        Self::new()
61    }
62}
63
64impl ParameterServer {
65    /// Create a new empty parameter server
66    #[allow(clippy::large_stack_arrays)] // Intentional: static allocation for embedded use
67    pub const fn new() -> Self {
68        // Initialize with None values
69        Self {
70            entries: [const { None }; MAX_PARAMETERS],
71            count: 0,
72            dirty: false,
73        }
74    }
75
76    /// Phase 172.H — take the dirty flag, clearing it. Returns `true` if a
77    /// value changed (via [`set`](Self::set) / [`unset`](Self::unset)) since
78    /// the last call, signalling the persistence layer to flush.
79    pub fn take_dirty(&mut self) -> bool {
80        core::mem::take(&mut self.dirty)
81    }
82
83    /// Get the number of parameters stored
84    pub fn len(&self) -> usize {
85        self.count
86    }
87
88    /// Check if the server has no parameters
89    pub fn is_empty(&self) -> bool {
90        self.count == 0
91    }
92
93    /// Check if the server is at capacity
94    pub fn is_full(&self) -> bool {
95        self.count >= MAX_PARAMETERS
96    }
97
98    /// Find the index of a parameter by name
99    fn find_index(&self, name: &str) -> Option<usize> {
100        self.entries.iter().position(|entry| {
101            entry
102                .as_ref()
103                .map(|e| e.param.name.as_str() == name)
104                .unwrap_or(false)
105        })
106    }
107
108    /// Find an empty slot
109    fn find_empty_slot(&self) -> Option<usize> {
110        self.entries.iter().position(|entry| entry.is_none())
111    }
112
113    /// Declare a new parameter with a value
114    ///
115    /// If the parameter already exists, this does nothing and returns false.
116    /// Returns true if the parameter was declared successfully.
117    pub fn declare(&mut self, name: &str, value: ParameterValue) -> bool {
118        self.declare_with_descriptor(name, value, None)
119    }
120
121    /// Declare a new parameter with value and descriptor
122    ///
123    /// The descriptor provides metadata like description, constraints, and read-only flag.
124    pub fn declare_with_descriptor(
125        &mut self,
126        name: &str,
127        value: ParameterValue,
128        descriptor: Option<ParameterDescriptor>,
129    ) -> bool {
130        // Check if already exists
131        if self.find_index(name).is_some() {
132            return false;
133        }
134
135        // Find an empty slot
136        let slot = match self.find_empty_slot() {
137            Some(idx) => idx,
138            None => return false,
139        };
140
141        // Create the parameter
142        let param = match Parameter::new(name, value) {
143            Some(p) => p,
144            None => return false,
145        };
146
147        self.entries[slot] = Some(ParameterEntry { param, descriptor });
148        self.count += 1;
149        true
150    }
151
152    /// Get a parameter value by name
153    pub fn get(&self, name: &str) -> Option<&ParameterValue> {
154        self.find_index(name)
155            .and_then(|idx| self.entries[idx].as_ref())
156            .map(|entry| &entry.param.value)
157    }
158
159    /// Get a parameter by name
160    pub fn get_parameter(&self, name: &str) -> Option<&Parameter> {
161        self.find_index(name)
162            .and_then(|idx| self.entries[idx].as_ref())
163            .map(|entry| &entry.param)
164    }
165
166    /// Get a parameter descriptor by name
167    pub fn get_descriptor(&self, name: &str) -> Option<&ParameterDescriptor> {
168        self.find_index(name)
169            .and_then(|idx| self.entries[idx].as_ref())
170            .and_then(|entry| entry.descriptor.as_ref())
171    }
172
173    /// Set a parameter value
174    ///
175    /// Returns the result of the set operation.
176    pub fn set(&mut self, name: &str, value: ParameterValue) -> SetParameterResult {
177        let idx = match self.find_index(name) {
178            Some(idx) => idx,
179            None => return SetParameterResult::NotFound,
180        };
181
182        let entry = match self.entries[idx].as_mut() {
183            Some(e) => e,
184            None => return SetParameterResult::NotFound,
185        };
186
187        // Check if read-only
188        if let Some(ref desc) = entry.descriptor {
189            if desc.read_only {
190                return SetParameterResult::ReadOnly;
191            }
192
193            // Check type compatibility
194            if !desc.dynamic_typing && desc.param_type != value.param_type() {
195                return SetParameterResult::TypeMismatch;
196            }
197
198            // Check range constraints
199            if !desc.validate_range(&value) {
200                return SetParameterResult::OutOfRange;
201            }
202        }
203
204        entry.param.value = value;
205        self.dirty = true;
206        SetParameterResult::Success
207    }
208
209    /// Unset an optional parameter (set to NotSet)
210    ///
211    /// This bypasses the type check to allow optional parameters to be unset.
212    /// Returns an error if the parameter is read-only.
213    pub fn unset(&mut self, name: &str) -> SetParameterResult {
214        let idx = match self.find_index(name) {
215            Some(idx) => idx,
216            None => return SetParameterResult::NotFound,
217        };
218
219        let entry = match self.entries[idx].as_mut() {
220            Some(e) => e,
221            None => return SetParameterResult::NotFound,
222        };
223
224        // Check if read-only
225        if let Some(ref desc) = entry.descriptor
226            && desc.read_only
227        {
228            return SetParameterResult::ReadOnly;
229        }
230
231        entry.param.value = ParameterValue::NotSet;
232        self.dirty = true;
233        SetParameterResult::Success
234    }
235
236    /// Set or declare a parameter
237    ///
238    /// If the parameter exists, sets its value. Otherwise, declares it.
239    pub fn set_or_declare(&mut self, name: &str, value: ParameterValue) -> SetParameterResult {
240        if self.find_index(name).is_some() {
241            self.set(name, value)
242        } else if self.declare(name, value) {
243            SetParameterResult::Success
244        } else {
245            SetParameterResult::StorageFull
246        }
247    }
248
249    /// Check if a parameter exists
250    pub fn has(&self, name: &str) -> bool {
251        self.find_index(name).is_some()
252    }
253
254    /// Remove a parameter
255    ///
256    /// Returns true if the parameter was removed.
257    pub fn remove(&mut self, name: &str) -> bool {
258        if let Some(idx) = self.find_index(name) {
259            self.entries[idx] = None;
260            self.count -= 1;
261            true
262        } else {
263            false
264        }
265    }
266
267    /// Get the type of a parameter
268    pub fn get_type(&self, name: &str) -> Option<ParameterType> {
269        self.get(name).map(|v| v.param_type())
270    }
271
272    /// Iterate over all parameters
273    pub fn iter(&self) -> impl Iterator<Item = &Parameter> {
274        self.entries
275            .iter()
276            .filter_map(|entry| entry.as_ref().map(|e| &e.param))
277    }
278
279    /// List all parameter names
280    pub fn list_names(&self) -> impl Iterator<Item = &str> {
281        self.iter().map(|p| p.name.as_str())
282    }
283
284    /// List parameter names with a given prefix
285    pub fn list_with_prefix<'a>(&'a self, prefix: &'a str) -> impl Iterator<Item = &'a str> {
286        self.list_names()
287            .filter(move |name| name.starts_with(prefix))
288    }
289
290    /// Get a bool parameter value
291    pub fn get_bool(&self, name: &str) -> Option<bool> {
292        self.get(name).and_then(|v| v.as_bool())
293    }
294
295    /// Get an integer parameter value
296    pub fn get_integer(&self, name: &str) -> Option<i64> {
297        self.get(name).and_then(|v| v.as_integer())
298    }
299
300    /// Get a double parameter value
301    pub fn get_double(&self, name: &str) -> Option<f64> {
302        self.get(name).and_then(|v| v.as_double())
303    }
304
305    /// Get a string parameter value
306    pub fn get_string(&self, name: &str) -> Option<&str> {
307        self.get(name).and_then(|v| v.as_string())
308    }
309
310    /// Set a bool parameter value
311    pub fn set_bool(&mut self, name: &str, value: bool) -> SetParameterResult {
312        self.set(name, ParameterValue::Bool(value))
313    }
314
315    /// Set an integer parameter value
316    pub fn set_integer(&mut self, name: &str, value: i64) -> SetParameterResult {
317        self.set(name, ParameterValue::Integer(value))
318    }
319
320    /// Set a double parameter value
321    pub fn set_double(&mut self, name: &str, value: f64) -> SetParameterResult {
322        self.set(name, ParameterValue::Double(value))
323    }
324
325    /// Set a string parameter value
326    pub fn set_string(&mut self, name: &str, value: &str) -> SetParameterResult {
327        match ParameterValue::from_string(value) {
328            Some(v) => self.set(name, v),
329            None => SetParameterResult::StorageFull, // String too long
330        }
331    }
332
333    /// Declare a parameter with a descriptor and optional initial value.
334    ///
335    /// This is a more comprehensive declaration method used by the typed parameter API.
336    ///
337    /// # Arguments
338    /// - `descriptor`: The metadata for the parameter.
339    /// - `initial_value`: An optional initial value for the parameter. If `None`,
340    ///   the parameter will be initialized to `ParameterValue::NotSet`.
341    pub fn declare_parameter(
342        &mut self,
343        descriptor: ParameterDescriptor,
344        initial_value: Option<&ParameterValue>,
345    ) -> Result<(), SetParameterResult> {
346        let name = descriptor.name.as_str();
347
348        // Check if already exists
349        if self.find_index(name).is_some() {
350            return Err(SetParameterResult::TypeMismatch); // Indicates already declared
351        }
352
353        // Find an empty slot
354        let slot = match self.find_empty_slot() {
355            Some(idx) => idx,
356            None => return Err(SetParameterResult::StorageFull),
357        };
358
359        let param_value = initial_value.cloned().unwrap_or_default();
360
361        let param = Parameter::new(name, param_value).ok_or(SetParameterResult::StorageFull)?; // name too long
362
363        self.entries[slot] = Some(ParameterEntry {
364            param,
365            descriptor: Some(descriptor),
366        });
367        self.count += 1;
368        Ok(())
369    }
370
371    /// Get the current value of a parameter.
372    ///
373    /// Returns `Some(ParameterValue)` if the parameter exists, `None` otherwise.
374    /// The `ParameterValue` is cloned to avoid lifetime issues with `&mut self`.
375    pub fn get_parameter_value(&self, name: &str) -> Option<ParameterValue> {
376        self.get(name).cloned()
377    }
378
379    /// Set the value of a parameter.
380    ///
381    /// Returns `SetParameterResult::Success` on success, or an error if the parameter
382    /// is read-only, type mismatches, or is out of range.
383    pub fn set_parameter_value(&mut self, name: &str, value: ParameterValue) -> SetParameterResult {
384        self.set(name, value)
385    }
386}
387
388/// Builder for declaring parameters with a fluent API
389pub struct LegacyParameterBuilder<'a> {
390    server: &'a mut ParameterServer,
391    name: String<MAX_PARAM_NAME_LEN>,
392    value: ParameterValue,
393    descriptor: Option<ParameterDescriptor>,
394}
395
396impl<'a> LegacyParameterBuilder<'a> {
397    /// Create a new parameter builder
398    pub fn new(server: &'a mut ParameterServer, name: &str, value: ParameterValue) -> Option<Self> {
399        let mut n = String::new();
400        n.push_str(name).ok()?;
401        Some(Self {
402            server,
403            name: n,
404            value,
405            descriptor: None,
406        })
407    }
408
409    /// Set the parameter description
410    pub fn description(mut self, desc: &str) -> Self {
411        let param_type = self.value.param_type();
412        if self.descriptor.is_none() {
413            self.descriptor = ParameterDescriptor::new(self.name.as_str(), param_type);
414        }
415        if let Some(ref mut d) = self.descriptor {
416            d.description.clear();
417            let _ = d.description.push_str(desc);
418        }
419        self
420    }
421
422    /// Set the parameter as read-only
423    pub fn read_only(mut self) -> Self {
424        let param_type = self.value.param_type();
425        if self.descriptor.is_none() {
426            self.descriptor = ParameterDescriptor::new(self.name.as_str(), param_type);
427        }
428        if let Some(ref mut d) = self.descriptor {
429            d.read_only = true;
430        }
431        self
432    }
433
434    /// Set integer range constraints
435    pub fn integer_range(mut self, min: i64, max: i64, step: i64) -> Self {
436        let param_type = self.value.param_type();
437        if self.descriptor.is_none() {
438            self.descriptor = ParameterDescriptor::new(self.name.as_str(), param_type);
439        }
440        if let Some(ref mut d) = self.descriptor {
441            d.range = crate::types::ParameterRange::Integer(crate::types::IntegerRange::new(
442                min, max, step,
443            ));
444        }
445        self
446    }
447
448    /// Set float range constraints
449    pub fn float_range(mut self, min: f64, max: f64, step: f64) -> Self {
450        let param_type = self.value.param_type();
451        if self.descriptor.is_none() {
452            self.descriptor = ParameterDescriptor::new(self.name.as_str(), param_type);
453        }
454        if let Some(ref mut d) = self.descriptor {
455            d.range = crate::types::ParameterRange::FloatingPoint(
456                crate::types::FloatingPointRange::new(min, max, step),
457            );
458        }
459        self
460    }
461
462    /// Declare the parameter
463    pub fn declare(self) -> bool {
464        self.server
465            .declare_with_descriptor(self.name.as_str(), self.value, self.descriptor)
466    }
467}
468
469#[cfg(test)]
470mod tests {
471    use super::*;
472
473    #[test]
474    fn test_new_server() {
475        let server = ParameterServer::new();
476        assert_eq!(server.len(), 0);
477        assert!(server.is_empty());
478    }
479
480    #[test]
481    #[allow(clippy::approx_constant)]
482    fn test_declare_and_get() {
483        let mut server = ParameterServer::new();
484
485        assert!(server.declare("my_bool", ParameterValue::Bool(true)));
486        assert!(server.declare("my_int", ParameterValue::Integer(42)));
487        assert!(server.declare("my_double", ParameterValue::Double(3.14)));
488
489        assert_eq!(server.len(), 3);
490        assert!(!server.is_empty());
491
492        assert_eq!(server.get_bool("my_bool"), Some(true));
493        assert_eq!(server.get_integer("my_int"), Some(42));
494        assert_eq!(server.get_double("my_double"), Some(3.14));
495    }
496
497    #[test]
498    fn test_dirty_tracks_value_changes_not_declarations() {
499        // Phase 172.H — declaring defaults must not dirty the server, but a
500        // value change (set/unset) must, and take_dirty clears the flag.
501        let mut server = ParameterServer::new();
502        assert!(server.declare("count", ParameterValue::Integer(0)));
503        assert!(!server.take_dirty(), "declare must not dirty");
504
505        assert_eq!(server.set_integer("count", 10), SetParameterResult::Success);
506        assert!(server.take_dirty(), "set must dirty");
507        assert!(!server.take_dirty(), "take_dirty clears");
508
509        // A failed set (unknown name) must not dirty.
510        assert_eq!(
511            server.set("missing", ParameterValue::Integer(1)),
512            SetParameterResult::NotFound
513        );
514        assert!(!server.take_dirty(), "failed set must not dirty");
515
516        assert_eq!(server.unset("count"), SetParameterResult::Success);
517        assert!(server.take_dirty(), "unset must dirty");
518    }
519
520    #[test]
521    fn test_set_parameter() {
522        let mut server = ParameterServer::new();
523        server.declare("count", ParameterValue::Integer(0));
524
525        assert_eq!(server.set_integer("count", 10), SetParameterResult::Success);
526        assert_eq!(server.get_integer("count"), Some(10));
527    }
528
529    #[test]
530    fn test_set_nonexistent() {
531        let mut server = ParameterServer::new();
532        assert_eq!(
533            server.set("nonexistent", ParameterValue::Integer(1)),
534            SetParameterResult::NotFound
535        );
536    }
537
538    #[test]
539    fn test_read_only_parameter() {
540        let mut server = ParameterServer::new();
541
542        let desc = ParameterDescriptor::new("version", ParameterType::String)
543            .unwrap()
544            .with_read_only(true);
545
546        server.declare_with_descriptor(
547            "version",
548            ParameterValue::from_string("1.0.0").unwrap(),
549            Some(desc),
550        );
551
552        assert_eq!(
553            server.set_string("version", "2.0.0"),
554            SetParameterResult::ReadOnly
555        );
556        assert_eq!(server.get_string("version"), Some("1.0.0"));
557    }
558
559    #[test]
560    fn test_range_constraints() {
561        let mut server = ParameterServer::new();
562
563        let desc = ParameterDescriptor::new("speed", ParameterType::Double)
564            .unwrap()
565            .with_float_range(0.0, 10.0, 0.0);
566
567        server.declare_with_descriptor("speed", ParameterValue::Double(5.0), Some(desc));
568
569        // Valid value
570        assert_eq!(server.set_double("speed", 8.0), SetParameterResult::Success);
571
572        // Out of range
573        assert_eq!(
574            server.set_double("speed", 15.0),
575            SetParameterResult::OutOfRange
576        );
577        assert_eq!(server.get_double("speed"), Some(8.0)); // Unchanged
578    }
579
580    #[test]
581    fn test_remove_parameter() {
582        let mut server = ParameterServer::new();
583        server.declare("temp", ParameterValue::Double(25.0));
584
585        assert!(server.has("temp"));
586        assert!(server.remove("temp"));
587        assert!(!server.has("temp"));
588        assert!(!server.remove("temp")); // Already removed
589    }
590
591    #[test]
592    fn test_list_parameters() {
593        let mut server = ParameterServer::new();
594        server.declare("robot.speed", ParameterValue::Double(1.0));
595        server.declare("robot.name", ParameterValue::from_string("bot1").unwrap());
596        server.declare("sensor.range", ParameterValue::Double(10.0));
597
598        let robot_params: heapless::Vec<&str, 8> = server.list_with_prefix("robot.").collect();
599        assert_eq!(robot_params.len(), 2);
600    }
601
602    #[test]
603    fn test_set_or_declare() {
604        let mut server = ParameterServer::new();
605
606        // First call declares
607        assert_eq!(
608            server.set_or_declare("new_param", ParameterValue::Integer(1)),
609            SetParameterResult::Success
610        );
611        assert_eq!(server.get_integer("new_param"), Some(1));
612
613        // Second call sets
614        assert_eq!(
615            server.set_or_declare("new_param", ParameterValue::Integer(2)),
616            SetParameterResult::Success
617        );
618        assert_eq!(server.get_integer("new_param"), Some(2));
619    }
620
621    #[test]
622    fn test_duplicate_declare() {
623        let mut server = ParameterServer::new();
624        assert!(server.declare("param", ParameterValue::Integer(1)));
625        assert!(!server.declare("param", ParameterValue::Integer(2))); // Already exists
626        assert_eq!(server.get_integer("param"), Some(1)); // Unchanged
627    }
628}
629
630// =============================================================================
631// Ghost model validation
632// =============================================================================
633
634#[cfg(test)]
635mod ghost_checks {
636    use super::*;
637    use nros_ghost_types::ParamServerGhost;
638
639    /// Structural check: construct ParamServerGhost from ParameterServer private fields.
640    /// If a field is renamed or retyped, this fails to compile.
641    fn ghost_from_server(s: &ParameterServer) -> ParamServerGhost {
642        ParamServerGhost {
643            count: s.count,
644            max: MAX_PARAMETERS,
645        }
646    }
647
648    #[test]
649    fn ghost_new_count() {
650        let server = ParameterServer::new();
651        let ghost = ghost_from_server(&server);
652        assert_eq!(ghost.count, 0);
653        assert_eq!(ghost.max, 32);
654    }
655
656    #[test]
657    fn ghost_declare_increments() {
658        let mut server = ParameterServer::new();
659        let before = ghost_from_server(&server).count;
660        assert!(server.declare("test", ParameterValue::Integer(1)));
661        let after = ghost_from_server(&server).count;
662        assert_eq!(after, before + 1);
663    }
664
665    #[test]
666    fn ghost_remove_decrements() {
667        let mut server = ParameterServer::new();
668        server.declare("test", ParameterValue::Integer(1));
669        let before = ghost_from_server(&server).count;
670        assert!(server.remove("test"));
671        let after = ghost_from_server(&server).count;
672        assert_eq!(after, before - 1);
673    }
674
675    #[test]
676    fn ghost_count_bounded() {
677        let mut server = ParameterServer::new();
678        for i in 0..MAX_PARAMETERS {
679            let mut name = heapless::String::<64>::new();
680            let _ = core::fmt::write(&mut name, format_args!("p{}", i));
681            server.declare(name.as_str(), ParameterValue::Integer(i as i64));
682        }
683        let ghost = ghost_from_server(&server);
684        assert!(ghost.count <= ghost.max);
685        assert_eq!(ghost.count, MAX_PARAMETERS);
686        // Next declare should fail — count stays bounded
687        assert!(!server.declare("overflow", ParameterValue::Integer(0)));
688        let ghost2 = ghost_from_server(&server);
689        assert!(ghost2.count <= ghost2.max);
690    }
691}
692
693// =============================================================================
694// Kani bounded model checking proofs
695// =============================================================================
696
697#[cfg(kani)]
698mod verification {
699    use super::*;
700
701    #[kani::proof]
702    fn server_new_is_empty() {
703        let server = ParameterServer::new();
704        assert!(server.is_empty());
705        assert_eq!(server.len(), 0);
706        assert!(!server.is_full());
707    }
708
709    #[kani::proof]
710    fn server_declare_get_roundtrip_integer() {
711        let mut server = ParameterServer::new();
712        let val: i64 = kani::any();
713        assert!(server.declare("test", ParameterValue::Integer(val)));
714        assert_eq!(server.get_integer("test"), Some(val));
715        assert!(server.has("test"));
716        assert_eq!(server.len(), 1);
717    }
718
719    #[kani::proof]
720    fn server_declare_get_roundtrip_bool() {
721        let mut server = ParameterServer::new();
722        let val: bool = kani::any();
723        assert!(server.declare("test", ParameterValue::Bool(val)));
724        assert_eq!(server.get_bool("test"), Some(val));
725    }
726
727    #[kani::proof]
728    fn server_set_requires_declare() {
729        let mut server = ParameterServer::new();
730        let val: i64 = kani::any();
731        // Set without declare should fail
732        let result = server.set("test", ParameterValue::Integer(val));
733        assert_eq!(result, SetParameterResult::NotFound);
734    }
735
736    #[kani::proof]
737    fn server_duplicate_declare_fails() {
738        let mut server = ParameterServer::new();
739        assert!(server.declare("test", ParameterValue::Integer(1)));
740        assert!(!server.declare("test", ParameterValue::Integer(2)));
741        // Original value preserved
742        assert_eq!(server.get_integer("test"), Some(1));
743    }
744
745    #[kani::proof]
746    fn server_remove_clears() {
747        let mut server = ParameterServer::new();
748        assert!(server.declare("test", ParameterValue::Integer(42)));
749        assert!(server.has("test"));
750        assert!(server.remove("test"));
751        assert!(!server.has("test"));
752        assert_eq!(server.len(), 0);
753    }
754
755    #[kani::proof]
756    fn server_get_nonexistent_returns_none() {
757        let server = ParameterServer::new();
758        assert!(server.get("nonexistent").is_none());
759        assert!(server.get_bool("nonexistent").is_none());
760        assert!(server.get_integer("nonexistent").is_none());
761        assert!(server.get_double("nonexistent").is_none());
762        assert!(server.get_string("nonexistent").is_none());
763    }
764}
nros_params/server.rs

nros_params/
server.rs
