Add specs for HashMap entry API (verus-lang#2420)

Author: tjhance

examples/entry_api.rs

@@ -0,0 +1,52 @@
+use vstd::prelude::*;
+use vstd::std_specs::hash::*;
+use std::hash::*;
+use std::collections::hash_map::*;
+
+verus!{
+
+fn main() {
+    let mut m = HashMap::<u64, u64>::new();
+
+    // Use the entry to insert 0 => 20
+    let entry0 = m.entry(0);
+    entry0.insert_entry(20);
+
+    // Use the entry to insert 1 => 30, then change it to 40
+    let entry1 = m.entry(1);
+    let mut occupied_entry = entry1.insert_entry(30);
+    let value_ref = occupied_entry.get_mut();
+    *value_ref = 40;
+
+    assert(m@ =~= map![0 => 20, 1 => 40]);
+}
+
+/// Inserts the given key, value pair into the map if absent,
+/// does nothing otherwise
+fn insert_if_absent(m: &mut HashMap<u64, u64>, key: u64, value: u64)
+    ensures
+        !old(m)@.dom().contains(key) ==> final(m)@ =~= old(m)@.insert(key, value),
+        old(m)@.dom().contains(key) ==> final(m)@ =~= old(m)@,
+{
+    m.entry(key).or_insert(value);
+}
+
+/// If the key is absent, insert 1; else, double it
+fn try_double(m: &mut HashMap<u64, u64>, key: u64)
+    requires
+        m@.dom().contains(key) ==> m[key] * 2 <= u64::MAX,
+    ensures
+        !old(m)@.dom().contains(key) ==> final(m)@ =~= old(m)@.insert(key, 1),
+        old(m)@.dom().contains(key) ==> final(m)@ =~= old(m)@.insert(key, (old(m)@[key] * 2) as u64)
+{
+    match m.entry(key) {
+        Entry::Occupied(mut occ_entry) => {
+            *occ_entry.get_mut() *= 2;
+        }
+        Entry::Vacant(vac_entry) => {
+            vac_entry.insert(1);
+        }
+    }
+}
+
+}

examples/experimental_new_mut_ref/README.md

@@ -765,3 +765,164 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_fails(err, 3)
 }
+
+test_verify_one_file! {
+    #[test] hash_map_entry_api verus_code! {
+        use vstd::prelude::*;
+        use vstd::std_specs::hash::*;
+        use std::collections::hash_map::*;
+        use std::hash::*;
+
+        fn test1() {
+            let mut m = HashMap::<u64, u64>::new();
+
+            // Use entry API to insert to the map
+
+            let entry = m.entry(5);
+            assert(entry.key() == 5 && entry.value() === None);
+
+            let value_ref = entry.or_insert(20);
+            assert(*value_ref == 20);
+
+            *value_ref = 40;
+
+            assert(m@.dom().contains(5) && m@[5] == 40);
+
+            // Use entry API to remove from the map
+
+            let entry = m.entry(5);
+            match entry {
+                Entry::Occupied(occupied_entry) => {
+                    let (k, v) = occupied_entry.remove_entry();
+                    assert(k == 5);
+                    assert(v == 40);
+                }
+                Entry::Vacant(_) => {
+                    assert(false);
+                }
+            }
+
+            assert(!m@.dom().contains(5));
+
+            assert(false); // FAILS
+        }
+
+        fn test_occupied_entry() {
+            let mut m = HashMap::<u64, u64>::new();
+            let entry = m.entry(5);
+            let mut occ_entry = entry.insert_entry(20);
+
+            assert(occ_entry.key() == 5);
+            assert(occ_entry.value() == 20);
+
+            let x = occ_entry.get();
+            assert(*x == 20);
+
+            let x = occ_entry.get_mut();
+            assert(*x == 20);
+            *x = 30;
+
+            assert(occ_entry.key() == 5);
+            assert(occ_entry.value() == 30);
+
+            let x = occ_entry.into_mut();
+            assert(*x == 30);
+            *x = 40;
+
+            assert(m@.dom().contains(5));
+            assert(m@[5] == 40);
+
+            // Now let's remove it
+
+            let entry = m.entry(5);
+            let mut occ_entry = entry.insert_entry(60);
+
+            let (removed_key, removed_value) = occ_entry.remove_entry();
+            assert(removed_key == 5);
+            assert(removed_value == 60);
+
+            assert(m@ =~= Map::empty());
+
+            assert(false); // FAILS
+        }
+
+        fn test_occupied_entry2() {
+            let mut m = HashMap::<u64, u64>::new();
+            let entry = m.entry(5);
+            let mut occ_entry = entry.insert_entry(20);
+
+            let old_value = occ_entry.insert(17);
+            assert(old_value == 20);
+
+            assert(m@.dom().contains(5));
+            assert(m@[5] == 17);
+
+            let entry = m.entry(5);
+            let mut occ_entry = entry.insert_entry(20);
+            let mut old_value = occ_entry.remove();
+            assert(old_value == 20);
+
+            assert(m@ =~= Map::empty());
+
+            assert(false); // FAILS
+        }
+
+        fn test_vacant_entry() {
+            let mut m = HashMap::<u64, u64>::new();
+            let entry = m.entry(5);
+
+            let Entry::Vacant(vac_entry) = entry else { assert(false); return; };
+
+            let k = vac_entry.into_key();
+            assert(k == 5);
+
+            assert(m@ =~= Map::empty());
+
+            assert(false); // FAILS
+        }
+
+        fn test_vacant_entry2() {
+            let mut m = HashMap::<u64, u64>::new();
+            let entry = m.entry(5);
+
+            let Entry::Vacant(vac_entry) = entry else { assert(false); return; };
+
+            // do nothing
+
+            assert(m@ =~= Map::empty());
+
+            assert(false); // FAILS
+        }
+
+        fn test_vacant_entry3() {
+            let mut m = HashMap::<u64, u64>::new();
+            let entry = m.entry(5);
+
+            let Entry::Vacant(vac_entry) = entry else { assert(false); return; };
+
+            let r = vac_entry.insert(20);
+            assert(*r == 20);
+            *r = 30;
+
+            assert(m@.dom().contains(5) && m[5] == 30);
+
+            assert(false); // FAILS
+        }
+
+        fn test_vacant_entry4() {
+            let mut m = HashMap::<u64, u64>::new();
+            let entry = m.entry(5);
+
+            let Entry::Vacant(vac_entry) = entry else { assert(false); return; };
+
+            let mut occ_entry = vac_entry.insert_entry(20);
+            let r = occ_entry.get_mut();
+            assert(*r == 20);
+            *r = 30;
+
+            assert(m@.dom().contains(5) && m[5] == 30);
+
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 7)
+}