[Specs] ordered_map and big_ordered_map specs for get and get_and_map

aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.move

@@ -2668,4 +2668,54 @@ module aptos_std::big_ordered_map {
         aborts_if !spec_contains_key(map, 1);
      }
 
+    #[verify_only]
+    fun test_verify_get() {
+        let keys: vector<u64> = vector[1, 2, 3];
+        let values: vector<u64> = vector[4, 5, 6];
+        let map = new_from(keys, values);
+        let res1 = map.get(&1);
+        let res2 = map.get(&4);
+        spec {
+            assert keys[0] == 1;
+            assert keys[1] == 2;
+            assert keys[2] == 3;
+            assert res1 == option::spec_some(4 as u64);
+            assert res2 == option::spec_none();
+            assert spec_len(map) == 3;
+        };
+        map.remove(&1);
+        map.remove(&2);
+        map.remove(&3);
+        map.destroy_empty();
+    }
+
+    spec test_verify_get {
+        pragma verify = true;
+        aborts_if false;
+     }
+
+    #[verify_only]
+    fun test_verify_get_and_map() {
+        let keys: vector<u64> = vector[1, 2, 3];
+        let values: vector<u64> = vector[4, 5, 6];
+        let map = new_from(keys, values);
+        let res1 = map.get_and_map(&1, |x : &u64| *x + 1);
+        let res2 = map.get_and_map(&4, |x : &u64| *x + 1);
+        spec {
+            assert keys[0] == 1;
+            assert false;
+            assert res1 == option::spec_some(2 as u64);
+            assert res2 == option::spec_none();
+            assert spec_len(map) == 3;
+        };
+        map.remove(&1);
+        map.remove(&2);
+        map.remove(&3);
+        map.destroy_empty();
+    }
+
+    spec test_verify_get_and_map {
+        pragma verify = true;
+     }
+
 }

aptos-move/framework/aptos-framework/sources/datastructures/big_ordered_map.spec.move

@@ -220,6 +220,20 @@ spec aptos_std::big_ordered_map {
             std::cmp::compare(option::spec_borrow(result), k) == std::cmp::Ordering::Less);
     }
 
+    spec get {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if [abstract] false;
+        ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(spec_get(self, key));
+        ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none();
+    }
+
+    spec get_and_map {
+        pragma opaque;
+        pragma verify = false;
+        ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(f(spec_get(self, key)));
+        ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none();
+    }
 
     spec internal_find {
         pragma opaque;
@@ -246,6 +260,11 @@ spec aptos_std::big_ordered_map {
         pragma verify = false;
     }
 
+    spec iter_modify {
+        pragma opaque;
+        pragma verify = false;
+    }
+
     spec compute_length {
         pragma verify = false;
         pragma opaque;

aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.move

@@ -1506,4 +1506,34 @@ module aptos_std::ordered_map {
         aborts_if !spec_contains_key(map, 1);
      }
 
+    #[verify_only]
+    fun test_verify_get() {
+        let keys: vector<u64> = vector[1, 2, 3];
+        let values: vector<u64> = vector[4, 5, 6];
+        let map = new_from(keys, values);
+        let res1 = map.get(&1);
+        let res2 = map.get(&4);
+        spec {
+            assert keys[0] == 1;
+            assert res1 == option::spec_some(4 as u64);
+            assert res2 == option::spec_none();
+            assert spec_len(map) == 3;
+        };
+    }
+
+    #[verify_only]
+    fun test_verify_get_and_map() {
+        let keys: vector<u64> = vector[1, 2, 3];
+        let values: vector<u64> = vector[4, 5, 6];
+        let map = new_from(keys, values);
+        let res1 = map.get_and_map(&1, |x : &u64| *x + 1);
+        let res2 = map.get_and_map(&4, |x : &u64| *x + 1);
+        spec {
+            assert keys[0] == 1;
+            assert res1 == option::spec_some(5 as u64);
+            assert res2 == option::spec_none();
+            assert spec_len(map) == 3;
+        };
+    }
+
 }

aptos-move/framework/aptos-framework/sources/datastructures/ordered_map.spec.move

@@ -51,6 +51,21 @@ spec aptos_std::ordered_map {
         pragma intrinsic;
     }
 
+    spec get {
+        pragma opaque;
+        pragma verify = false;
+        aborts_if [abstract] false;
+        ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(spec_get(self, key));
+        ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none();
+    }
+
+    spec get_and_map {
+        pragma opaque;
+        pragma verify = false;
+        ensures [abstract] spec_contains_key(self, key) ==> result == option::spec_some(f(spec_get(self, key)));
+        ensures [abstract] !spec_contains_key(self, key) ==> result == option::spec_none();
+    }
+
     spec remove {
         pragma opaque;
         pragma verify = false;