Make Set and Map finite, add ISet and IMap.

examples/doubly_linked.rs

@@ -324,7 +324,7 @@ mod doubly_linked_list {
                         }
                         self.ghost_state.borrow_mut().points_to_map.tracked_map_keys_in_place(
                             Map::<nat, nat>::new(
-                                |j: nat| 1 <= j && j <= old(self).view().len(),
+                                Set::range(1, old(self)@.len() + 1),
                                 |j: nat| (j - 1) as nat,
                             ),
                         );
@@ -406,7 +406,7 @@ mod doubly_linked_list {
                         };
                         self.ghost_state.borrow_mut().points_to_map.tracked_map_keys_in_place(
                             Map::<nat, nat>::new(
-                                |j: nat| 0 <= j && j < old(self).view().len() - 1,
+                                Set::range(0, (old(self)@.len() - 1) as nat),
                                 |j: nat| (j + 1) as nat,
                             ),
                         );

examples/doubly_linked_xor.rs

@@ -354,7 +354,7 @@ impl<V> DListXor<V> {
                 }
                 (self.perms.borrow_mut()).tracked_map_keys_in_place(
                     Map::<nat, nat>::new(
-                        |j: nat| 0 <= j < old(self)@.len() - 1,
+                        Set::range(0, (old(self)@.len() - 1) as nat),
                         |j: nat| (j + 1) as nat,
                     ),
                 );
@@ -423,7 +423,7 @@ impl<V> DListXor<V> {
                 }
                 self.perms.borrow_mut().tracked_map_keys_in_place(
                     Map::<nat, nat>::new(
-                        |j: nat| 1 <= j <= old(self)@.len(),
+                        Set::range(1, old(self)@.len() + 1),
                         |j: nat| (j - 1) as nat,
                     ),
                 );

examples/extensionality.rs

@@ -2,7 +2,7 @@
 
 use verus_builtin::*;
 use verus_builtin_macros::*;
-use vstd::{map::*, seq::*, seq_lib::*, set::*, set_lib::*};
+use vstd::{imap::*, imap_lib::*, iset::*, iset_lib::*, map::*, seq::*, seq_lib::*, set::*, set_lib::*};
 
 verus! {
 
@@ -84,9 +84,9 @@ proof fn assert_maps_equal_with_proof(m: Map<int, int>, q: Map<int, int>)
 }
 
 proof fn assert_maps_equal_with_proof2() {
-    let m = Map::<u64, u64>::total(|t: u64| t & 184);
-    let q = Map::<u64, u64>::new(|t: u64| t ^ t == 0, |t: u64| 184 & t);
-    assert_maps_equal!(m, q, t => {
+    let m = IMap::<u64, u64>::total(|t: u64| t & 184);
+    let q = IMap::<u64, u64>::new(|t: u64| t ^ t == 0, |t: u64| 184 & t);
+    assert_imaps_equal!(m, q, t => {
         // show that the `q` map is total:
         assert_bit_vector(t ^ t == 0);
 
@@ -106,9 +106,9 @@ proof fn test_set(s: Set<int>, t: Set<int>) {
 }
 
 proof fn assert_sets_equal_with_proof() {
-    let s = Set::<u64>::new(|i: u64| i ^ 25 < 100);
-    let t = Set::<u64>::new(|i: u64| 25 ^ i < 100);
-    assert_sets_equal!(s, t, i => {
+    let s = ISet::<u64>::new(|i: u64| i ^ 25 < 100);
+    let t = ISet::<u64>::new(|i: u64| 25 ^ i < 100);
+    assert_isets_equal!(s, t, i => {
         assert_bit_vector(i ^ 25 == 25 ^ i);
     });
     assert(s == t);

examples/guide/lib_examples.rs

@@ -13,6 +13,11 @@ proof fn test_seq1() {
 
 proof fn test_set1() {
     let s: Set<int> = set![0, 10, 20, 30, 40];
+    assert(s.contains(20));
+    assert(s.contains(30));
+    assert(!s.contains(60));
+
+    let s: ISet<int> = iset![0, 10, 20, 30, 40];
     assert(s.finite());
     assert(s.contains(20));
     assert(s.contains(30));
@@ -52,26 +57,35 @@ proof fn test_seq2() {
 }
 
 proof fn test_set2() {
-    let s: Set<int> = Set::new(|i: int| 0 <= i <= 40 && i % 10 == 0);
+    let s_finite: Set<int> = Set::range(0, 41).filter(|i: int| i % 10 == 0);
+    assert(s_finite.contains(20));
+    assert(s_finite.contains(30));
+    assert(!s_finite.contains(60));
+
+    let s: ISet<int> = ISet::new(|i: int| 0 <= i <= 40 && i % 10 == 0);
     assert(s.contains(20));
     assert(s.contains(30));
     assert(!s.contains(60));
 
-    let s_infinite: Set<int> = Set::new(|i: int| i % 10 == 0);
+    let s_infinite: ISet<int> = ISet::new(|i: int| i % 10 == 0);
     assert(s_infinite.contains(20));
     assert(s_infinite.contains(30));
     assert(!s_infinite.contains(35));
 }
 
 proof fn test_map2() {
-    let m: Map<int, int> = Map::new(|i: int| 0 <= i <= 40 && i % 10 == 0, |i: int| 10 * i);
+    let m: IMap<int, int> = IMap::new(|i: int| 0 <= i <= 40 && i % 10 == 0, |i: int| 10 * i);
     assert(m[20] == 200);
     assert(m[30] == 300);
 
-    let m_infinite: Map<int, int> = Map::new(|i: int| i % 10 == 0, |i: int| 10 * i);
+    let m_infinite: IMap<int, int> = IMap::new(|i: int| i % 10 == 0, |i: int| 10 * i);
     assert(m_infinite[20] == 200);
     assert(m_infinite[30] == 300);
     assert(m_infinite[90] == 900);
+
+    let m_finite: Map<int, int> = Map::new(Set::range(0, 41), |i: int| 10 * i);
+    assert(m_finite[20] == 200);
+    assert(m_finite[30] == 300);
 }
 // ANCHOR_END: new
 
@@ -130,8 +144,6 @@ proof fn test_eq2() {
 /*
 // ANCHOR: lemma_len_intersect_fail
 pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
-    requires
-        s1.finite(),
     ensures
         s1.intersect(s2).len() <= s1.len(),
     decreases
@@ -149,8 +161,6 @@ pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
 
 // ANCHOR: lemma_len_intersect_sketch
 pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
-    requires
-        s1.finite(),
     ensures
         s1.intersect(s2).len() <= s1.len(),
     decreases
@@ -187,8 +197,6 @@ pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
 
 // ANCHOR: lemma_len_intersect
 pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
-    requires
-        s1.finite(),
     ensures
         s1.intersect(s2).len() <= s1.len(),
     decreases
@@ -207,8 +215,6 @@ pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
 
 // ANCHOR: lemma_len_intersect_commented
 pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
-    requires
-        s1.finite(),
     ensures
         s1.intersect(s2).len() <= s1.len(),
     decreases s1.len(),

examples/state_machines/dist_rwlock.rs

@@ -3,7 +3,7 @@
 use verus_builtin::*;
 use verus_builtin_macros::*;
 use vstd::atomic_ghost::*;
-use vstd::map::*;
+use vstd::imap::*;
 use vstd::multiset::*;
 use vstd::prelude::*;
 
@@ -23,8 +23,8 @@ tokenized_state_machine!{
             #[sharding(variable)]
             pub exc_locked: bool,
 
-            #[sharding(map)]
-            pub ref_counts: Map<int, int>,
+            #[sharding(imap)]
+            pub ref_counts: IMap<int, int>,
 
             #[sharding(option)]
             pub exc_pending: Option<int>,
@@ -45,7 +45,7 @@ tokenized_state_machine!{
                 init rc_width = rc_width;
                 init storage = Option::Some(init_t);
                 init exc_locked = false;
-                init ref_counts = Map::new(
+                init ref_counts = IMap::new(
                     |i| 0 <= i < rc_width,
                     |i| 0,
                 );

examples/state_machines/flat_combine.rs

@@ -46,20 +46,20 @@ tokenized_state_machine! {
             #[sharding(constant)]
             pub num_clients: nat,
 
-            #[sharding(map)]
-            pub clients: Map<nat, Client>,
+            #[sharding(imap)]
+            pub clients: IMap<nat, Client>,
 
-            #[sharding(map)]
-            pub slots: Map<nat, bool>,
+            #[sharding(imap)]
+            pub slots: IMap<nat, bool>,
 
             #[sharding(variable)]
             pub combiner: Combiner,
 
-            #[sharding(storage_map)]
-            pub requests: Map<nat, Request>,
+            #[sharding(storage_imap)]
+            pub requests: IMap<nat, Request>,
 
-            #[sharding(storage_map)]
-            pub responses: Map<nat, Response>,
+            #[sharding(storage_imap)]
+            pub responses: IMap<nat, Response>,
         }
 
         pub open spec fn valid_idx(self, i: nat) -> bool {
@@ -169,15 +169,15 @@ tokenized_state_machine! {
         init!{
             initialize(num_clients: nat) {
                 init num_clients = num_clients;
-                init clients = Map::new(
+                init clients = IMap::new(
                     |i: nat| 0 <= i && i < num_clients,
                     |i: nat| Client::Idle);
-                init slots = Map::new(
+                init slots = IMap::new(
                     |i: nat| 0 <= i && i < num_clients,
                     |i: nat| false);
                 init combiner = Combiner::Collecting { elems: Seq::empty() };
-                init requests = Map::empty();
-                init responses = Map::empty();
+                init requests = IMap::empty();
+                init responses = IMap::empty();
             }
         }
 

examples/state_machines/interner.rs

@@ -17,14 +17,14 @@ tokenized_state_machine! {InternSystem<T> {
         #[sharding(variable)]
         pub auth: Seq<T>,
 
-        #[sharding(persistent_map)]
-        pub frag: Map<int, T>,
+        #[sharding(persistent_imap)]
+        pub frag: IMap<int, T>,
     }
 
     init!{
         empty() {
             init auth = Seq::empty();
-            init frag = Map::empty();
+            init frag = IMap::empty();
         }
     }
 

examples/state_machines/maps.rs

@@ -1,22 +1,22 @@
 // rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
-use vstd::map::*;
+use vstd::imap::*;
 use vstd::{pervasive::*, *};
 
 use verus_state_machines_macros::tokenized_state_machine;
 
 tokenized_state_machine!(
     X {
         fields {
-            #[sharding(map)]
-            pub bool_map: Map<int, bool>,
+            #[sharding(imap)]
+            pub bool_map: IMap<int, bool>,
 
         }
 
         init!{
             initialize(cond: bool) {
-                init bool_map = Map::empty().insert(5, true);
+                init bool_map = IMap::empty().insert(5, true);
             }
         }
 
@@ -52,11 +52,11 @@ tokenized_state_machine!(
             #[sharding(variable)]
             pub m: int,
 
-            #[sharding(map)]
-            pub map: Map<int, bool>,
+            #[sharding(imap)]
+            pub map: IMap<int, bool>,
 
-            #[sharding(storage_map)]
-            pub storage_map: Map<int, bool>,
+            #[sharding(storage_imap)]
+            pub storage_map: IMap<int, bool>,
         }
 
         #[invariant]
@@ -80,8 +80,8 @@ tokenized_state_machine!(
         init!{
             initialize(cond: bool) {
                 init m = 0;
-                init storage_map = Map::empty();
-                init map = Map::empty();
+                init storage_map = IMap::empty();
+                init map = IMap::empty();
             }
         }