Implement extend for StringMap (#257)

Signed-off-by: Xudong Sun <[email protected]>

src/pervasive_ext/string_map.rs

@@ -59,6 +59,14 @@ impl StringMap {
         }
     }
 
+    #[verifier(external_body)]
+    pub fn extend(&mut self, m2: StringMap)
+        ensures
+            self@ == old(self)@.union_prefer_right(m2@),
+    {
+        self.inner.extend(m2.into_rust_map())
+    }
+
     #[verifier(external)]
     pub fn from_rust_map(inner: std::collections::BTreeMap<std::string::String, std::string::String>) -> StringMap
     {

src/unit_tests/kubernetes_api_objects/mod.rs

@@ -0,0 +1,3 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+pub mod object_meta;

src/unit_tests/object_meta.rs → src/unit_tests/kubernetes_api_objects/object_meta.rs

@@ -11,7 +11,6 @@ verus! {
 #[test]
 #[verifier(external)]
 pub fn test_set_name() {
-    println!("Testing set_name()...");
     let mut object_meta = ObjectMeta::default();
     object_meta.set_name(new_strlit("name").to_string());
     assert_eq!("name".to_string(), object_meta.into_kube().name.unwrap());

src/unit_tests/mod.rs

@@ -1,4 +1,4 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-pub mod object_meta;
-
+pub mod kubernetes_api_objects;
+pub mod vstd_ext;

src/unit_tests/vstd_ext/mod.rs

@@ -0,0 +1,3 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+pub mod string_map;

src/unit_tests/vstd_ext/string_map.rs

@@ -0,0 +1,28 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::pervasive_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+
+#[test]
+#[verifier(external)]
+pub fn test_extend() {
+    let mut m = StringMap::empty();
+    m.insert(new_strlit("key1").to_string(), new_strlit("val1").to_string());
+    m.insert(new_strlit("key2").to_string(), new_strlit("val2").to_string());
+
+    let mut m2 = StringMap::empty();
+    m.insert(new_strlit("key1").to_string(), new_strlit("new_val1").to_string());
+    m.insert(new_strlit("key3").to_string(), new_strlit("val3").to_string());
+
+    m.extend(m2);
+
+    let rust_map = m.into_rust_map();
+    assert_eq!(rust_map.get(&"key1".to_string()), Some(&"new_val1".to_string()));
+    assert_eq!(rust_map.get(&"key2".to_string()), Some(&"val2".to_string()));
+    assert_eq!(rust_map.get(&"key3".to_string()), Some(&"val3".to_string()));
+}
+
+}