diff --git a/capybaraKV/capybarakv/Cargo.toml b/capybaraKV/capybarakv/Cargo.toml
index d379cfd6..759c6181 100644
--- a/capybaraKV/capybarakv/Cargo.toml
+++ b/capybaraKV/capybarakv/Cargo.toml
@@ -20,7 +20,7 @@ default = [ "pmem" ]
 crc64fast = "1.0.0"
 # Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features
 rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] }
-vstd = "0.0.0-2026-05-24-0157"
+vstd = { git = "https://github.com/verus-lang/verus.git" }
 pmcopy = { path = "../pmcopy" }
 
 [target.'cfg(target_family = "unix")'.dependencies]
@@ -34,6 +34,7 @@ winapi = { version = "0.3.9", features = ["errhandlingapi", "fileapi", "handleap
 
 [lints.rust]
 unexpected_cfgs = { level = "allow", check-cfg = ["cfg(verus_keep_ghost)"] }
+unused_features = "allow"
 
 [package.metadata.verus]
 verify = true
diff --git a/capybaraKV/capybarakv/src/common/table_v.rs b/capybaraKV/capybarakv/src/common/table_v.rs
index ccf800c9..9c3b6083 100644
--- a/capybaraKV/capybarakv/src/common/table_v.rs
+++ b/capybaraKV/capybarakv/src/common/table_v.rs
@@ -163,14 +163,13 @@ impl TableMetadata
             self.valid(),
         ensures
             ({
-                let valid_row_addrs = Set::<u64>::new(|row_addr: u64| self.validate_row_addr(row_addr));
-                &&& valid_row_addrs.len() == self.num_rows
-                &&& valid_row_addrs.finite()
+                let valid_row_addrs = Set::<u64>::from_finite_type(|row_addr: u64| self.validate_row_addr(row_addr));
+                valid_row_addrs.len() == self.num_rows
             }),
     {
         // The proof is in three parts.
 
-        let valid_row_addrs = Set::<u64>::new(|row_addr: u64| self.validate_row_addr(row_addr));
+        let valid_row_addrs = Set::<u64>::from_finite_type(|row_addr: u64| self.validate_row_addr(row_addr));
         let rows: Seq<u64> = Seq::new(self.num_rows as nat, |row_index: int| self.spec_row_index_to_addr(row_index));
 
         // First, we prove that the sequence containing all row addresses in order has no duplicates.
diff --git a/capybaraKV/capybarakv/src/common/util_v.rs b/capybaraKV/capybarakv/src/common/util_v.rs
index edfd668c..f924667a 100644
--- a/capybaraKV/capybarakv/src/common/util_v.rs
+++ b/capybaraKV/capybarakv/src/common/util_v.rs
@@ -83,12 +83,12 @@ pub proof fn lemma_injective_map_inverse<K, V>(map: Map<K, V>)
     ensures 
         forall |k: K| map.contains_key(k) ==> {
             let v = map[k];
-            map.invert()[v] == k
+            map.invert().contains_pair(v, k)
         }
 {
     assert forall |k: K| map.contains_key(k) implies {
         let v = map[k];
-        map.invert()[v] == k
+        map.invert().contains_pair(v, k)
     } by {
         let v = map[k];
         if map.invert()[v] != k {
@@ -119,10 +119,9 @@ pub proof fn lemma_seq_len_when_no_dup_and_all_values_in_range(s: Seq<int>, min:
     s.unique_seq_to_set();
     // because s_set only has values between min and max, it's a subset 
     // of the set containing all values between min and max
-    assert(s_set.subset_of(set_int_range(min, max)));
-    lemma_int_range(min, max);
-    lemma_len_subset(s_set, set_int_range(min, max));
-    assert(s.len() <= set_int_range(min, max).len());
+    assert(s_set.subset_of(Set::<int>::range(min, max)));
+    lemma_len_subset(s_set, Set::<int>::range(min, max));
+    assert(s.len() <= Set::<int>::range(min, max).len());
 }
 
 // This executable function clones a vector of objects of type `T`
@@ -162,8 +161,6 @@ pub exec fn extend_vec_u8_from_slice(v: &mut Vec<u8>, s: &[u8])
 // Proves that, given that `s` is finite, it contains `v` if and only if
 // `s.to_seq()` contains `v`.
 pub proof fn lemma_set_to_seq_contains_iff_set_contains<A>(s: Set<A>, v: A)
-    requires
-        s.finite(),
     ensures
         s.contains(v) <==> s.to_seq().contains(v),
     decreases
@@ -194,8 +191,6 @@ pub proof fn lemma_set_to_seq_contains_iff_set_contains<A>(s: Set<A>, v: A)
 // Proves that, given that `s` is finite, `s.to_seq()` has the same length as `s`
 // and has no duplicates.
 pub proof fn lemma_set_to_seq_has_same_length_with_no_duplicates<A>(s: Set<A>)
-    requires
-        s.finite(),
     ensures
         s.to_seq().len() == s.len(),
         s.to_seq().no_duplicates(),
@@ -225,11 +220,9 @@ pub proof fn lemma_bijection_makes_sets_have_equal_size<A, B>(
     g: spec_fn(B) -> A,
 )
     requires
-        s1.finite(),
         forall|x: A| #[trigger] s1.contains(x) ==> s2.contains(f(x)) && x == g(f(x)),
         forall|y: B| #[trigger] s2.contains(y) ==> s1.contains(g(y)) && y == f(g(y)),
     ensures
-        s2.finite(),
         s2.len() == s1.len(),
 {
     // Convert set `s1` to a sequence and prove key properties of the
diff --git a/capybaraKV/capybarakv/src/journal/entry_v.rs b/capybaraKV/capybarakv/src/journal/entry_v.rs
index 0fbca152..634b0392 100644
--- a/capybaraKV/capybarakv/src/journal/entry_v.rs
+++ b/capybaraKV/capybarakv/src/journal/entry_v.rs
@@ -26,7 +26,7 @@ impl JournalEntry
 
     pub(super) open spec fn addrs(self) -> Set<int>
     {
-        Set::<int>::new(|i| self.start <= i < self.end())
+        Set::<int>::range(self.start, self.end())
     }
 
     pub(super) open spec fn fits(self, sm: JournalStaticMetadata) -> bool
diff --git a/capybaraKV/capybarakv/src/journal/write_v.rs b/capybaraKV/capybarakv/src/journal/write_v.rs
index 1dec5554..89ea4b43 100644
--- a/capybaraKV/capybarakv/src/journal/write_v.rs
+++ b/capybaraKV/capybarakv/src/journal/write_v.rs
@@ -147,7 +147,7 @@ where
                         &&& final(self)@ == (JournalView{
                                commit_state: update_bytes(old(self)@.commit_state, addr as int, bytes_to_write@),
                                journaled_addrs: old(self)@.journaled_addrs +
-                                                Set::<int>::new(|i: int| addr <= i < addr + bytes_to_write.len()),
+                                                Set::<int>::range(addr as int, addr + bytes_to_write.len()),
                                remaining_capacity: old(self)@.remaining_capacity - space_needed,
                                ..old(self)@
                            })
@@ -182,7 +182,7 @@ where
         
         self.journal_length = self.journal_length + overhead + bytes_to_write.len() as u64;
         self.journaled_addrs = Ghost(self.journaled_addrs@ +
-                                     Set::<int>::new(|i: int| addr <= i < addr + bytes_to_write.len()));
+                                     Set::<int>::range(addr as int, addr + bytes_to_write.len()));
         let concrete_entry = ConcreteJournalEntry::new(addr, bytes_to_write);
         self.entries.push(concrete_entry);
 
diff --git a/capybaraKV/capybarakv/src/kv2/concurrentspec_t.rs b/capybaraKV/capybarakv/src/kv2/concurrentspec_t.rs
index caabafcc..183e7a6e 100644
--- a/capybaraKV/capybarakv/src/kv2/concurrentspec_t.rs
+++ b/capybaraKV/capybarakv/src/kv2/concurrentspec_t.rs
@@ -70,7 +70,7 @@ pub trait ReadLinearizer<K, I, L, Op: ReadOnlyOperation<K, I, L>> : Sized
 {
     type Completion;
 
-    spec fn namespaces(self) -> Set<int>;
+    spec fn namespaces(self) -> ISet<int>;
 
     spec fn pre(self, id: Loc, op: Op) -> bool;
 
@@ -140,7 +140,7 @@ pub trait MutatingLinearizer<K, I, L, Op: MutatingOperation<K, I, L>> : Sized
 {
     type Completion;
 
-    spec fn namespaces(self) -> Set<int>;
+    spec fn namespaces(self) -> ISet<int>;
 
     spec fn pre(self, id: Loc, op: Op) -> bool;
 
diff --git a/capybaraKV/capybarakv/src/kv2/inv_v.rs b/capybaraKV/capybarakv/src/kv2/inv_v.rs
index 682c2dc0..361fae5a 100644
--- a/capybaraKV/capybarakv/src/kv2/inv_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/inv_v.rs
@@ -79,13 +79,6 @@ where
         }
     }
 
-    pub(super) open spec fn inv_components_finite(self) -> bool
-    {
-        &&& self.keys@.durable.key_info.dom().finite()
-        &&& self.items@.durable.m.dom().finite()
-        &&& self.lists@.durable.m.dom().finite()
-    }
-
     pub(super) open spec fn inv_used_slots_correspond(self) -> bool
     {
         self.status@ is Quiescent ==> {
@@ -110,7 +103,6 @@ where
         &&& self.inv_tentative_components_exist()
         &&& self.inv_components_valid()
         &&& self.inv_components_correspond()
-        &&& self.inv_components_finite()
         &&& self.inv_used_slots_correspond()
         &&& self.inv_perm_factory_allows_recovery_idempotent_changes()
         &&& decode_policies(self.sm@.encoded_policies) == Some(self.lists@.logical_range_gaps_policy)
diff --git a/capybaraKV/capybarakv/src/kv2/items/abort_v.rs b/capybaraKV/capybarakv/src/kv2/items/abort_v.rs
index a48e08e6..2bd82aea 100644
--- a/capybaraKV/capybarakv/src/kv2/items/abort_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/items/abort_v.rs
@@ -37,12 +37,11 @@ where
         ensures
             final(self).valid(jv_after_abort),
             final(self)@ == (ItemTableView{ tentative: Some(old(self)@.durable), used_slots: final(self)@.used_slots, ..old(self)@ }),
-            final(self)@.durable.m.dom().finite(),
             final(self)@.used_slots == final(self)@.durable.m.dom().len(),
     {
         let ghost new_row_info =
             Map::<u64, ItemRowDisposition<I>>::new(
-                |row_addr: u64| self.row_info@.contains_key(row_addr),
+                self.row_info@.dom(),
                 |row_addr: u64| match self.row_info@[row_addr] {
                     ItemRowDisposition::<I>::InPendingAllocationList{ pos, item } =>
                         ItemRowDisposition::<I>::InFreeList{ pos: self.free_list@.len() + pos },
diff --git a/capybaraKV/capybarakv/src/kv2/items/commit_v.rs b/capybaraKV/capybarakv/src/kv2/items/commit_v.rs
index 7b596eb3..411fccd2 100644
--- a/capybaraKV/capybarakv/src/kv2/items/commit_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/items/commit_v.rs
@@ -37,12 +37,11 @@ where
         ensures
             final(self).valid(jv_after_commit),
             final(self)@ == (ItemTableView{ durable: old(self)@.tentative.unwrap(), used_slots: final(self)@.used_slots, ..old(self)@ }),
-            final(self)@.durable.m.dom().finite(),
             final(self)@.used_slots == final(self)@.durable.m.dom().len(),
     {
         let ghost new_row_info =
             Map::<u64, ItemRowDisposition<I>>::new(
-                |row_addr: u64| self.row_info@.contains_key(row_addr),
+                self.row_info@.dom(),
                 |row_addr: u64| match self.row_info@[row_addr] {
                     ItemRowDisposition::<I>::InPendingAllocationList{ pos, item } =>
                         ItemRowDisposition::<I>::NowhereFree{ item },
diff --git a/capybaraKV/capybarakv/src/kv2/items/inv_v.rs b/capybaraKV/capybarakv/src/kv2/items/inv_v.rs
index e598bd75..119f6b6f 100644
--- a/capybaraKV/capybarakv/src/kv2/items/inv_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/items/inv_v.rs
@@ -160,11 +160,11 @@ impl<I> ItemTableInternalView<I>
     {
         ItemTableSnapshot::<I>{
             m: Map::<u64, I>::new(
+                self.row_info.dom().filter(
                 |row_addr: u64| {
-                    &&& self.row_info.contains_key(row_addr)
                     &&& self.row_info[row_addr] is NowhereFree ||
                        self.row_info[row_addr] is InPendingDeallocationList
-                },
+                }),
                 |row_addr: u64| match self.row_info[row_addr] {
                     ItemRowDisposition::NowhereFree{ item } => item,
                     ItemRowDisposition::InPendingDeallocationList{ pos, item } => item,
@@ -178,11 +178,11 @@ impl<I> ItemTableInternalView<I>
     {
         ItemTableSnapshot::<I>{
             m: Map::<u64, I>::new(
+                self.row_info.dom().filter(
                 |row_addr: u64| {
-                    &&& self.row_info.contains_key(row_addr)
                     &&& self.row_info[row_addr] is NowhereFree ||
                        self.row_info[row_addr] is InPendingAllocationList
-                },
+                }),
                 |row_addr: u64| match self.row_info[row_addr] {
                     ItemRowDisposition::NowhereFree{ item } => item,
                     ItemRowDisposition::InPendingAllocationList{ pos, item } => item,
@@ -199,7 +199,6 @@ impl<I> ItemTableInternalView<I>
             self.pending_allocations == Seq::<u64>::empty(),
             self.pending_deallocations == Seq::<u64>::empty(),
         ensures
-            self.as_durable_snapshot().m.dom().finite(),
             self.as_durable_snapshot().m.dom().len() == sm.table.num_rows - self.free_list.len(),
     {
         assert forall|pos: int| 0 <= pos < self.free_list.len() implies
@@ -208,24 +207,20 @@ impl<I> ItemTableInternalView<I>
             assert(self.row_info.contains_key(self.free_list[pos]));
         }
 
-        let free_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr] is InFreeList
-        );
-        let item_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr] is NowhereFree
-        );
-        let valid_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr)
-        );
+        let free_row_addrs =
+            self.row_info.dom().filter(|row_addr: u64| self.row_info[row_addr] is InFreeList);
+        let item_row_addrs =
+            self.row_info.dom().filter(|row_addr: u64| self.row_info[row_addr] is NowhereFree);
+        let valid_row_addrs = self.row_info.dom();
 
-        assert(valid_row_addrs.finite() && valid_row_addrs.len() == sm.table.num_rows) by {
-            assert(valid_row_addrs =~= Set::<u64>::new(|row_addr: u64| sm.table.validate_row_addr(row_addr)));
+        assert(valid_row_addrs.len() == sm.table.num_rows) by {
+            assert(valid_row_addrs =~= Set::<u64>::from_finite_type(|row_addr: u64| sm.table.validate_row_addr(row_addr)));
             sm.table.lemma_valid_row_set_len();
         }
-        assert(free_row_addrs.finite()) by {
+        assert(free_row_addrs.len() <= valid_row_addrs.len()) by {
             vstd::set_lib::lemma_len_subset(free_row_addrs, valid_row_addrs);
         }
-        assert(item_row_addrs.finite()) by {
+        assert(item_row_addrs.len() <= valid_row_addrs.len()) by {
             vstd::set_lib::lemma_len_subset(item_row_addrs, valid_row_addrs);
         }
 
diff --git a/capybaraKV/capybarakv/src/kv2/items/recover_v.rs b/capybaraKV/capybarakv/src/kv2/items/recover_v.rs
index 7e69b888..16e8d1c2 100644
--- a/capybaraKV/capybarakv/src/kv2/items/recover_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/items/recover_v.rs
@@ -59,7 +59,7 @@ pub(super) open spec fn recover_items<I>(
         items_recoverable::<I>(s, addrs, sm),
 {
     Map::<u64, I>::new(
-        |addr: u64| addrs.contains(addr),
+        addrs,
         |addr: u64| recover_item::<I>(s, addr, sm),
     )
 }
diff --git a/capybaraKV/capybarakv/src/kv2/items/start_v.rs b/capybaraKV/capybarakv/src/kv2/items/start_v.rs
index d7af7367..509da1bc 100644
--- a/capybaraKV/capybarakv/src/kv2/items/start_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/items/start_v.rs
@@ -41,7 +41,6 @@ where
                     let recovered_state = Self::recover(journal@.read_state, item_addrs@, *sm).unwrap();
                     &&& items.valid(journal@)
                     &&& items@.sm == *sm
-                    &&& recovered_state.m.dom().finite()
                     &&& items@.used_slots == recovered_state.m.dom().len()
                     &&& items@.durable == recovered_state
                     &&& items@.tentative == Some(recovered_state)
diff --git a/capybaraKV/capybarakv/src/kv2/keys/abort_v.rs b/capybaraKV/capybarakv/src/kv2/keys/abort_v.rs
index 08f22bff..3faaf5cd 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/abort_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/abort_v.rs
@@ -105,7 +105,6 @@ where
         ensures
             final(self).valid(jv_after_abort),
             final(self)@ == (KeyTableView{ tentative: Some(old(self)@.durable), used_slots: final(self)@.used_slots, ..old(self)@ }),
-            final(self)@.durable.key_info.dom().finite(),
             final(self)@.used_slots == final(self)@.durable.key_info.dom().len(),
     {
         self.status = Ghost(KeyTableStatus::Inconsistent);
diff --git a/capybaraKV/capybarakv/src/kv2/keys/commit_v.rs b/capybaraKV/capybarakv/src/kv2/keys/commit_v.rs
index bd5feccd..2abf97fa 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/commit_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/commit_v.rs
@@ -32,7 +32,6 @@ where
         ensures
             final(self).valid(jv_after_commit),
             final(self)@ == (KeyTableView{ durable: old(self)@.tentative.unwrap(), used_slots: final(self)@.used_slots, ..old(self)@ }),
-            final(self)@.durable.key_info.dom().finite(),
             final(self)@.used_slots == final(self)@.durable.key_info.dom().len(),
     {
         // Delete all the undo records, and move everything in the pending deallocations
diff --git a/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs b/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
index cd9d5eef..50851f7d 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
@@ -160,8 +160,8 @@ where
                     &&& seqs_match_except_in_range(old(journal)@.commit_state, final(journal)@.commit_state,
                                                  row_addr as int, row_addr + final(self).sm.table.row_size)
                     &&& final(journal)@.journaled_addrs == old(journal)@.journaled_addrs +
-                        Set::<int>::new(|i: int| row_addr + final(self).sm.row_cdb_start <= i
-                                      < row_addr + final(self).sm.row_cdb_start + u64::spec_size_of())
+                        Set::<int>::range(row_addr + final(self).sm.row_cdb_start,
+                                      row_addr + final(self).sm.row_cdb_start + u64::spec_size_of())
                     &&& final(journal)@.remaining_capacity >= old(journal)@.remaining_capacity -
                            spec_journal_entry_overhead() - u64::spec_size_of()
                 },
diff --git a/capybaraKV/capybarakv/src/kv2/keys/inv_v.rs b/capybaraKV/capybarakv/src/kv2/keys/inv_v.rs
index a74ed113..2257b377 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/inv_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/inv_v.rs
@@ -200,22 +200,22 @@ impl<K> KeyMemoryMapping<K>
     {
         KeyRecoveryMapping::<K>{
             row_info: Map::<u64, Option<(K, KeyTableRowMetadata)>>::new(
-                |row_addr: u64| self.row_info.contains_key(row_addr),
+                self.row_info.dom(),
                 |row_addr: u64| match self.row_info[row_addr] {
                     KeyRowDisposition::InHashTable{ k, rm } => Some((k, rm)),
                     _ => None,
                 },
             ),
             key_info: Map::<K, u64>::new(
-                |k: K| self.key_info.contains_key(k),
+                self.key_info.dom(),
                 |k: K| self.key_info[k] as u64,
             ),
             item_info: Map::<u64, u64>::new(
-                |item_addr: u64| self.item_info.contains_key(item_addr),
+                self.item_info.dom(),
                 |item_addr: u64| self.item_info[item_addr] as u64,
             ),
             list_info: Map::<u64, u64>::new(
-                |list_addr: u64| self.list_info.contains_key(list_addr),
+                self.list_info.dom(),
                 |list_addr: u64| self.list_info[list_addr] as u64,
             ),
         }
@@ -225,15 +225,15 @@ impl<K> KeyMemoryMapping<K>
     {
         KeyTableSnapshot::<K>{
             key_info: Map::<K, KeyTableRowMetadata>::new(
-                |k: K| self.key_info.contains_key(k),
+                self.key_info.dom(),
                 |k: K| self.row_info[self.key_info[k]]->rm,
             ),
             item_info: Map::<u64, K>::new(
-                |item_addr: u64| self.item_info.contains_key(item_addr),
+                self.item_info.dom(),
                 |item_addr: u64| self.row_info[self.item_info[item_addr]]->k
             ),
             list_info: Map::<u64, K>::new(
-                |list_addr: u64| self.list_info.contains_key(list_addr),
+                self.list_info.dom(),
                 |list_addr: u64| self.row_info[self.list_info[list_addr]]->k
             ),
         }
@@ -453,7 +453,6 @@ impl<K> KeyMemoryMapping<K>
             self.consistent_with_free_list_and_pending_deallocations(free_list, Seq::<u64>::empty()),
         ensures
             self.as_recovery_mapping().key_info.dom() == self.key_info.dom(),
-            self.key_info.dom().finite(), 
             self.key_info.dom().len() == sm.table.num_rows - free_list.len(),
     {
         assert forall|pos: int| 0 <= pos < free_list.len() implies self.row_info.contains_key(#[trigger] free_list[pos]) by {
@@ -461,24 +460,20 @@ impl<K> KeyMemoryMapping<K>
             assert(self.row_info.contains_key(free_list[pos]));
         }
 
-        let free_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr] is InFreeList
-        );
-        let key_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr] is InHashTable
-        );
-        let valid_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr)
-        );
+        let free_row_addrs =
+            self.row_info.dom().filter(|row_addr: u64| self.row_info[row_addr] is InFreeList);
+        let key_row_addrs =
+            self.row_info.dom().filter(|row_addr: u64| self.row_info[row_addr] is InHashTable);
+        let valid_row_addrs = self.row_info.dom();
 
-        assert(valid_row_addrs.finite() && valid_row_addrs.len() == sm.table.num_rows) by {
-            assert(valid_row_addrs =~= Set::<u64>::new(|row_addr: u64| sm.table.validate_row_addr(row_addr)));
+        assert(valid_row_addrs.len() == sm.table.num_rows) by {
+            assert(valid_row_addrs =~= Set::<u64>::from_finite_type(|row_addr: u64| sm.table.validate_row_addr(row_addr)));
             sm.table.lemma_valid_row_set_len();
         }
-        assert(free_row_addrs.finite()) by {
+        assert(free_row_addrs.len() <= valid_row_addrs.len()) by {
             vstd::set_lib::lemma_len_subset(free_row_addrs, valid_row_addrs);
         }
-        assert(key_row_addrs.finite()) by {
+        assert(key_row_addrs.len() <= valid_row_addrs.len()) by {
             vstd::set_lib::lemma_len_subset(key_row_addrs, valid_row_addrs);
         }
 
@@ -493,7 +488,7 @@ impl<K> KeyMemoryMapping<K>
             free_list.unique_seq_to_set();
         }
 
-        assert(self.key_info.dom().finite() && self.key_info.dom().len() == key_row_addrs.len()) by {
+        assert(self.key_info.dom().len() == key_row_addrs.len()) by {
             lemma_bijection_makes_sets_have_equal_size::<u64, K>(
                 key_row_addrs, self.key_info.dom(),
                 |row_addr: u64| self.row_info[row_addr]->InHashTable_k,
diff --git a/capybaraKV/capybarakv/src/kv2/keys/recover_v.rs b/capybaraKV/capybarakv/src/kv2/keys/recover_v.rs
index 7e85b3b3..b8db98ac 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/recover_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/recover_v.rs
@@ -42,7 +42,7 @@ impl<K> KeyRecoveryMapping<K>
     pub(super) open spec fn new_empty(tm: TableMetadata) -> Self
     {
         let row_info = Map::<u64, Option<(K, KeyTableRowMetadata)>>::new(
-            |addr: u64| tm.validate_row_addr(addr),
+            Set::<u64>::from_finite_type(|addr: u64| tm.validate_row_addr(addr)),
             |addr: u64| None,
         );
         Self{
@@ -126,15 +126,15 @@ impl<K> KeyRecoveryMapping<K>
     {
         KeyTableSnapshot::<K>{
             key_info: Map::<K, KeyTableRowMetadata>::new(
-                |k: K| self.key_info.contains_key(k),
+                self.key_info.dom(),
                 |k: K| self.row_info[self.key_info[k]].unwrap().1,
             ),
             item_info: Map::<u64, K>::new(
-                |item_addr: u64| self.item_info.contains_key(item_addr),
+                self.item_info.dom(),
                 |item_addr: u64| self.row_info[self.item_info[item_addr]].unwrap().0,
             ),
             list_info: Map::<u64, K>::new(
-                |list_addr: u64| self.list_info.contains_key(list_addr),
+                self.list_info.dom(),
                 |list_addr: u64| self.row_info[self.list_info[list_addr]].unwrap().0,
             ),
         }
diff --git a/capybaraKV/capybarakv/src/kv2/keys/spec_v.rs b/capybaraKV/capybarakv/src/kv2/keys/spec_v.rs
index 0968965d..153e6e37 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/spec_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/spec_v.rs
@@ -139,7 +139,6 @@ impl<K> KeyTableSnapshot<K>
     pub proof fn lemma_valid_implies_num_keys_equals_num_items(self)
         requires
             self.valid(),
-            self.key_info.dom().finite(),
         ensures
             self.item_info.dom().len() == self.key_info.dom().len(),
     {
diff --git a/capybaraKV/capybarakv/src/kv2/keys/start_v.rs b/capybaraKV/capybarakv/src/kv2/keys/start_v.rs
index ec1bb336..bf53f243 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/start_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/start_v.rs
@@ -51,7 +51,6 @@ where
                     &&& keys@.sm == *sm
                     &&& keys@.durable == recovered_state
                     &&& keys@.tentative == Some(recovered_state)
-                    &&& recovered_state.key_info.dom().finite()
                     &&& keys@.used_slots == recovered_state.key_info.dom().len()
                     &&& item_addrs@ == recovered_state.item_addrs()
                     &&& list_addrs@.to_set() == recovered_state.list_addrs()
diff --git a/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs b/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
index 1a7ca495..d64e0cb6 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
@@ -22,13 +22,9 @@ impl<L> ListTableInternalView<L>
     pub(super) open spec fn abort_m(self) -> Map<u64, ListTableEntryView<L>>
     {
         Map::<u64, ListTableEntryView<L>>::new(
-            |list_addr: u64| {
-                ||| self.deletes_inverse.contains_key(list_addr)
-                ||| {
-                       &&& self.m.contains_key(list_addr)
-                       &&& self.m[list_addr] is Durable
-                   }
-            },
+            self.deletes_inverse.dom().union(
+                self.m.dom().filter(|list_addr: u64| self.m[list_addr] is Durable)
+            ),
             |list_addr: u64| {
                 if self.deletes_inverse.contains_key(list_addr) {
                     ListTableEntryView::Durable{ summary: self.deletes[self.deletes_inverse[list_addr] as int] }
@@ -43,7 +39,7 @@ impl<L> ListTableInternalView<L>
     pub(super) open spec fn abort_row_info(self) -> Map<u64, ListRowDisposition>
     {
         Map::<u64, ListRowDisposition>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr),
+            self.row_info.dom(),
             |row_addr: u64| match self.row_info[row_addr] {
                 ListRowDisposition::InPendingAllocationList{ pos } =>
                     ListRowDisposition::InFreeList{ pos: self.free_list.len() + pos },
@@ -281,8 +277,7 @@ where
             final(self)@ == (ListTableView{ tentative: Some(old(self)@.durable), used_slots: final(self)@.used_slots, ..old(self)@ }),
             ({
                 let m = final(self)@.durable.m;
-                &&& m.dom().finite()
-                &&& final(self)@.used_slots ==
+                final(self)@.used_slots ==
                        m.dom().to_seq().fold_left(0, |total: int, row_addr: u64| total + m[row_addr].len())
             }),
     {
diff --git a/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs b/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
index 832dedce..bf8acca9 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
@@ -22,7 +22,7 @@ impl<L> ListTableInternalView<L>
     pub(super) open spec fn commit_m(self) -> Map<u64, ListTableEntryView<L>>
     {
         Map::<u64, ListTableEntryView<L>>::new(
-            |list_addr: u64| self.m.contains_key(list_addr),
+            self.m.dom(),
             |list_addr: u64| self.m[list_addr].commit(),
         )
     }
@@ -30,7 +30,7 @@ impl<L> ListTableInternalView<L>
     pub(super) open spec fn commit_row_info(self) -> Map<u64, ListRowDisposition>
     {
         Map::<u64, ListRowDisposition>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr),
+            self.row_info.dom(),
             |row_addr: u64| match self.row_info[row_addr] {
                 ListRowDisposition::InPendingAllocationList{ pos } =>
                     ListRowDisposition::NowhereFree,
@@ -176,8 +176,7 @@ where
             final(self)@ == (ListTableView{ durable: old(self)@.tentative.unwrap(), used_slots: final(self)@.used_slots, ..old(self)@ }),
             ({
                 let m = final(self)@.durable.m;
-                &&& m.dom().finite()
-                &&& final(self)@.used_slots ==
+                final(self)@.used_slots ==
                        m.dom().to_seq().fold_left(0, |total: int, row_addr: u64| total + m[row_addr].len())
             }),
     {
diff --git a/capybaraKV/capybarakv/src/kv2/lists/delete_v.rs b/capybaraKV/capybarakv/src/kv2/lists/delete_v.rs
index 1fb9078f..124378b1 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/delete_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/delete_v.rs
@@ -26,7 +26,9 @@ impl<L> ListRecoveryMapping<L>
             self.list_info.contains_key(list_addr),
     {
         let new_row_info = Map::<u64, ListRowRecoveryInfo<L>>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr].head != list_addr,
+            self.row_info.dom().filter(
+                |row_addr: u64| self.row_info[row_addr].head != list_addr
+            ),
             |row_addr: u64| self.row_info[row_addr],
         );
         Self{
@@ -60,7 +62,7 @@ impl<L> ListTableInternalView<L>
             self.m.contains_key(list_addr),
     {
         let new_row_info = Map::<u64, ListRowDisposition>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr),
+            self.row_info.dom(),
             |row_addr: u64|
                 if {
                     &&& self.tentative_mapping.row_info.contains_key(row_addr)
diff --git a/capybaraKV/capybarakv/src/kv2/lists/slots_v.rs b/capybaraKV/capybarakv/src/kv2/lists/slots_v.rs
index d5001c46..6bfbe7a3 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/slots_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/slots_v.rs
@@ -7,6 +7,7 @@ use super::impl_v::*;
 use super::inv_v::*;
 use super::super::spec_t::*;
 use vstd::set_lib::*;
+use vstd::contrib::set_build;
 
 verus! {
 
@@ -26,19 +27,17 @@ impl<L> ListTableInternalView<L>
             self.durable_mapping.internally_consistent(sm),
             self.pending_allocations == Seq::<u64>::empty(),
             self.pending_deallocations == Seq::<u64>::empty(),
-            self.durable_mapping.as_snapshot().m.dom().finite(),
             0 <= pos <= self.durable_mapping.as_snapshot().m.dom().to_seq().len(),
         ensures
             ({
                 let m = self.durable_mapping.as_snapshot().m;
                 let s = m.dom().to_seq();
                 let prefix = s.take(pos);
-                let tups = Set::<(u64, int)>::new(|tup: (u64, int)| {
-                    let (head, i) = tup;
-                    &&& prefix.contains(head)
-                    &&& 0 <= i < m[head].len()
-                });
-                &&& tups.finite()
+                let tups = set_build!{ (head, i): (u64, int) |
+                    head: u64,
+                    i: int in 0..m[head].len() as int,
+                    prefix.contains(head),
+                };
                 &&& prefix.fold_left(0, |total: int, head: u64| total + m[head].len()) == tups.len()
             }),
         decreases
@@ -47,28 +46,28 @@ impl<L> ListTableInternalView<L>
         let m = self.durable_mapping.as_snapshot().m;
         let s = m.dom().to_seq();
         let prefix = s.take(pos);
-        let tups = Set::<(u64, int)>::new(|tup: (u64, int)| {
-            let (head, i) = tup;
-            &&& prefix.contains(head)
-            &&& 0 <= i < m[head].len()
-        });
+        let tups = set_build!{ (head, i): (u64, int) |
+            head: u64,
+            i: int in 0..m[head].len() as int,
+            prefix.contains(head),
+        };
         let f = |total: int, head: u64| total + m[head].len();
         lemma_set_to_seq_has_same_length_with_no_duplicates(m.dom());
         if pos > 0 {
-            let tups_prev = Set::<(u64, int)>::new(|tup: (u64, int)| {
-                let (head, i) = tup;
-                &&& s.take(pos - 1).contains(head)
-                &&& 0 <= i < m[head].len()
-            });
-            let tups_cur = Set::<(u64, int)>::new(|tup: (u64, int)| {
-                let (head, i) = tup;
-                &&& head == s[pos - 1]
-                &&& 0 <= i < m[head].len()
-            });
-            assert(tups_cur.finite() && tups_cur.len() == m[s[pos - 1]].len()) by {
-                lemma_int_range(0, m[s[pos - 1]].len() as int);
+            let tups_prev = set_build!{ (head, i): (u64, int) |
+                head: u64,
+                i: int in 0..m[head].len() as int,
+                s.take(pos - 1).contains(head),
+            };
+            let tups_cur = set_build!{ (head, i): (u64, int) |
+                head: u64,
+                i: int in 0..m[head].len() as int,
+                head == s[pos - 1],
+            };
+
+            assert(tups_cur.len() == m[s[pos - 1]].len()) by {
                 lemma_bijection_makes_sets_have_equal_size(
-                    set_int_range(0, m[s[pos - 1]].len() as int),
+                    Set::<int>::range(0, m[s[pos - 1]].len() as int),
                     tups_cur,
                     |i: int| (s[pos - 1], i),
                     |tup: (u64, int)| tup.1
@@ -111,8 +110,7 @@ impl<L> ListTableInternalView<L>
         ensures
             ({
                 let m = self.durable_mapping.as_snapshot().m;
-                &&& m.dom().finite()
-                &&& m.dom().to_seq().fold_left(0, |total: int, head: u64| total + m[head].len())
+                m.dom().to_seq().fold_left(0, |total: int, head: u64| total + m[head].len())
                        == sm.table.num_rows - self.free_list.len()
             }),
     {
@@ -125,36 +123,21 @@ impl<L> ListTableInternalView<L>
             assert(self.row_info.contains_key(self.free_list[pos]));
         }
 
-        let free_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr] is InFreeList
-        );
-        let list_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr) && self.row_info[row_addr] is NowhereFree
-        );
-        let valid_row_addrs = Set::<u64>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr)
-        );
-        let list_head_addrs = Set::<u64>::new(
-            |row_addr: u64| self.durable_mapping.row_info.contains_key(row_addr) &&
-                            self.durable_mapping.row_info[row_addr].pos == 0
-        );
+        let free_row_addrs =
+            self.row_info.dom().filter(|row_addr: u64| self.row_info[row_addr] is InFreeList);
+        let list_row_addrs =
+            self.row_info.dom().filter(|row_addr: u64| self.row_info[row_addr] is NowhereFree);
+        let valid_row_addrs = self.row_info.dom();
+        let list_head_addrs = self.durable_mapping.row_info.dom().filter(
+            |row_addr: u64| self.durable_mapping.row_info[row_addr].pos == 0);
 
         assert(m.dom() == self.durable_mapping.list_elements.dom());
         let list_heads = m.dom().to_seq();
 
-        assert(valid_row_addrs.finite() && valid_row_addrs.len() == sm.table.num_rows) by {
-            assert(valid_row_addrs =~= Set::<u64>::new(|row_addr: u64| sm.table.validate_row_addr(row_addr)));
+        assert(valid_row_addrs.len() == sm.table.num_rows) by {
+            assert(valid_row_addrs =~= Set::<u64>::from_finite_type(|row_addr: u64| sm.table.validate_row_addr(row_addr)));
             sm.table.lemma_valid_row_set_len();
         }
-        assert(free_row_addrs.finite()) by {
-            vstd::set_lib::lemma_len_subset(free_row_addrs, valid_row_addrs);
-        }
-        assert(list_row_addrs.finite()) by {
-            vstd::set_lib::lemma_len_subset(list_row_addrs, valid_row_addrs);
-        }
-        assert(list_head_addrs.finite()) by {
-            vstd::set_lib::lemma_len_subset(list_head_addrs, valid_row_addrs);
-        }
         assert(list_head_addrs =~= m.dom());
 
         assert(valid_row_addrs.len() == free_row_addrs.len() + list_row_addrs.len()) by {
@@ -168,12 +151,12 @@ impl<L> ListTableInternalView<L>
             self.free_list.unique_seq_to_set();
         }
 
-        let tups = Set::<(u64, int)>::new(|tup: (u64, int)| {
-            let (head, i) = tup;
-            &&& list_heads.contains(head)
-            &&& 0 <= i < m[head].len()
-        });
-        assert(tups.finite() && list_heads.fold_left(0, addr_to_len) == tups.len()) by {
+        let tups = set_build!{ (head, i): (u64, int) |
+            head: u64,
+            i: int in 0..m[head].len() as int,
+            list_heads.contains(head),
+        };
+        assert(list_heads.fold_left(0, addr_to_len) == tups.len()) by {
             self.lemma_corresponds_implies_sum_lengths_equals_num_pos_tuples(sm, list_heads.len() as int);
             assert(list_heads.take(list_heads.len() as int) =~= list_heads);
         }
diff --git a/capybaraKV/capybarakv/src/kv2/lists/start_v.rs b/capybaraKV/capybarakv/src/kv2/lists/start_v.rs
index 9f1c9726..d18287fe 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/start_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/start_v.rs
@@ -351,7 +351,6 @@ where
                     &&& lists.valid(journal@)
                     &&& lists@.sm == *sm
                     &&& lists@.logical_range_gaps_policy == logical_range_gaps_policy
-                    &&& m.dom().finite()
                     &&& lists@.used_slots ==
                            m.dom().to_seq().fold_left(0, |total: int, row_addr: u64| total + m[row_addr].len())
                     &&& lists@.durable == recovered_state
diff --git a/capybaraKV/capybarakv/src/kv2/lists/trim_v.rs b/capybaraKV/capybarakv/src/kv2/lists/trim_v.rs
index b968dd2f..0c1145a0 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/trim_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/trim_v.rs
@@ -30,10 +30,9 @@ impl<L> ListRecoveryMapping<L>
         let new_addrs = self.list_info[list_addr].skip(trim_length);
         let new_elements = self.list_elements[list_addr].skip(trim_length);
         let new_row_info = Map::<u64, ListRowRecoveryInfo<L>>::new(
-            |row_addr: u64| {
-                &&& self.row_info.contains_key(row_addr)
-                &&& self.row_info[row_addr].head == list_addr ==> self.row_info[row_addr].pos >= trim_length
-            },
+            self.row_info.dom().filter(
+                |row_addr: u64| self.row_info[row_addr].head == list_addr ==> self.row_info[row_addr].pos >= trim_length
+            ),
             |row_addr: u64|
             {
                 let info = self.row_info[row_addr];
@@ -194,7 +193,7 @@ impl<L> ListTableInternalView<L>
     {
         let new_head = self.tentative_mapping.list_info[list_addr][trim_length];
         let new_row_info = Map::<u64, ListRowDisposition>::new(
-            |row_addr: u64| self.row_info.contains_key(row_addr),
+            self.row_info.dom(),
             |row_addr: u64|
                 if {
                     &&& self.tentative_mapping.row_info.contains_key(row_addr)
diff --git a/capybaraKV/capybarakv/src/kv2/lists/update_v.rs b/capybaraKV/capybarakv/src/kv2/lists/update_v.rs
index 0d033852..abfe109c 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/update_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/update_v.rs
@@ -140,13 +140,7 @@ impl<L> ListTableInternalView<L>
         let prev_addr = if idx == 0 { 0 } else { old_addrs[idx - 1] };
 
         let new_row_info = Map::<u64, ListRowRecoveryInfo<L>>::new(
-            |row_addr: u64| {
-                ||| row_addr == new_row_addr
-                ||| {
-                       &&& self.tentative_mapping.row_info.contains_key(row_addr)
-                       &&& row_addr != old_row_addr
-                }
-            },
+            self.tentative_mapping.row_info.dom().filter(|row_addr: u64| row_addr != old_row_addr).insert(new_row_addr),
             |row_addr: u64|
             {
                 if row_addr == new_row_addr {
@@ -733,8 +727,8 @@ where
                 }
                 &&& final(journal)@.journaled_addrs ==
                     old(journal)@.journaled_addrs +
-                    Set::<int>::new(|i: int| prev_row_addr + self.sm.row_next_start <= i
-                                  < prev_row_addr + self.sm.row_next_start + u64::spec_size_of() + u64::spec_size_of())
+                    Set::<int>::range(prev_row_addr + self.sm.row_next_start,
+                                  prev_row_addr + self.sm.row_next_start + u64::spec_size_of() + u64::spec_size_of())
             } else {
                 &&& forall|other_row_addr: u64| {
                     &&& self.sm.table.validate_row_addr(other_row_addr)
@@ -922,8 +916,8 @@ where
                 }
                 &&& new_jv.journaled_addrs ==
                     old_jv.journaled_addrs +
-                    Set::<int>::new(|i: int| prev_row_addr + sm.row_next_start <= i
-                                  < prev_row_addr + sm.row_next_start + u64::spec_size_of() + u64::spec_size_of())
+                    Set::<int>::range(prev_row_addr + sm.row_next_start,
+                                  prev_row_addr + sm.row_next_start + u64::spec_size_of() + u64::spec_size_of())
             } else {
                 &&& forall|other_row_addr: u64| {
                     &&& sm.table.validate_row_addr(other_row_addr)
diff --git a/capybaraKV/capybarakv/src/kv2/recover_v.rs b/capybaraKV/capybarakv/src/kv2/recover_v.rs
index 32766da9..0b2ddd33 100644
--- a/capybaraKV/capybarakv/src/kv2/recover_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/recover_v.rs
@@ -184,7 +184,7 @@ pub(super) open spec fn recover_kv_from_keys_items_and_lists<K, I, L>(
                 kv: AtomicKvStore::<K, I, L>{
                     logical_range_gaps_policy: ps.logical_range_gaps_policy,
                     m: Map::<K, (I, Seq<L>)>::new(
-                        |k: K| keys.dom().contains(k),
+                        keys.dom(),
                         |k: K| (items[keys[k].item_addr],
                                 if keys[k].list_addr == 0 { Seq::<L>::empty() } else { lists[keys[k].list_addr] }),
                     ),
@@ -303,7 +303,7 @@ pub(super) open spec fn combine_component_snapshots<K, I, L>(
     AtomicKvStore::<K, I, L>{
         logical_range_gaps_policy,
         m: Map::<K, (I, Seq<L>)>::new(
-            |k: K| keys.key_info.dom().contains(k),
+            keys.key_info.dom(),
             |k: K| (items.m[keys.key_info[k].item_addr],
                     if keys.key_info[k].list_addr == 0 { Seq::<L>::empty() }
                     else { lists.m[keys.key_info[k].list_addr] }),
diff --git a/capybaraKV/capybarakv/src/kv2/rwkv_v.rs b/capybaraKV/capybarakv/src/kv2/rwkv_v.rs
index 2b2a89d2..a12aed1d 100644
--- a/capybaraKV/capybarakv/src/kv2/rwkv_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/rwkv_v.rs
@@ -95,6 +95,7 @@ proof fn linearize_nop<PM, K, I, L, Op, CB>(
     let tracked mut completion;
     open_atomic_invariant_in_proof!(credit => &inv => inner => {
         inner.rwlock_auth.agree(ckv_res);
+        assert(cb.namespaces().subset_of(cb.namespaces().insert(inv.namespace())));
         completion = cb.apply(op, ckv_res@, exec_result, &mut inner.caller_auth);
     });
     completion
diff --git a/capybaraKV/capybarakv/src/kv2/shardkv_t.rs b/capybaraKV/capybarakv/src/kv2/shardkv_t.rs
index d22fd49e..6cb65c20 100644
--- a/capybaraKV/capybarakv/src/kv2/shardkv_t.rs
+++ b/capybaraKV/capybarakv/src/kv2/shardkv_t.rs
@@ -45,7 +45,7 @@ where
     I: PmCopy + Sized + std::fmt::Debug,
     L: PmCopy + LogicalRange + std::fmt::Debug + Copy,
 {
-    spec fn namespaces(self) -> Set<int>;
+    spec fn namespaces(self) -> ISet<int>;
     spec fn id(self) -> Loc;
 
     exec fn setup(
@@ -92,7 +92,7 @@ where
             shard_namespace != inv.namespace(),
         ensures
             result.id() == inv.constant().combined_id,
-            result.namespaces() == set![inv.namespace(), shard_namespace];
+            result.namespaces() == iset![inv.namespace(), shard_namespace];
 
     exec fn read_item<CB>(
         &self,
@@ -303,7 +303,7 @@ pub exec fn setup<PM, K, I, L>(
         match result {
             Ok((kv, res)) => {
                 &&& kv.id() == res@.id()
-                &&& kv.namespaces() == set![namespace, shard_namespace]
+                &&& kv.namespaces() == iset![namespace, shard_namespace]
                 &&& res@@ == ConcurrentKvStoreView::<K, I, L>{
                         ps: *ps,
                         pm_constants: pm_constants,
@@ -399,7 +399,7 @@ pub exec fn recover<PM, K, I, L>(
         match result {
             Ok(kv) => {
                 &&& kv.id() == id
-                &&& kv.namespaces() == set![namespace, shard_namespace]
+                &&& kv.namespaces() == iset![namespace, shard_namespace]
             },
             Err(KvError::CRCMismatch) => !pm_constants.impervious_to_corruption(),
             Err(KvError::WrongKvStoreId{ requested_id, actual_id }) => {
diff --git a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs
index a4e555ab..e29dad75 100644
--- a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs
@@ -230,8 +230,8 @@ where
     I: PmCopy + Sized + std::fmt::Debug,
     L: PmCopy + LogicalRange + std::fmt::Debug + Copy,
 {
-    closed spec fn namespaces(self) -> Set<int> {
-        set![self.inv@.namespace(), self.shard_namespace@]
+    closed spec fn namespaces(self) -> ISet<int> {
+        iset![self.inv@.namespace(), self.shard_namespace@]
     }
 
     closed spec fn id(self) -> Loc {
@@ -562,7 +562,7 @@ impl<K, I, L, Op, Lin> ReadLinearizer<K, I, L, Op> for ShardedReadLinearizer<K,
 {
     type Completion = Lin::Completion;
 
-    closed spec fn namespaces(self) -> Set<int> {
+    closed spec fn namespaces(self) -> ISet<int> {
         self.lin.namespaces().insert(self.inv.namespace())
     }
 
@@ -623,7 +623,7 @@ impl<K, I, L, Op, Lin> MutatingLinearizer<K, I, L, Op> for ShardedMutatingLinear
 {
     type Completion = Lin::Completion;
 
-    closed spec fn namespaces(self) -> Set<int> {
+    closed spec fn namespaces(self) -> ISet<int> {
         self.lin.namespaces().insert(self.inv.namespace())
     }
 
diff --git a/capybaraKV/capybarakv/src/kv2/slots_v.rs b/capybaraKV/capybarakv/src/kv2/slots_v.rs
index 737df1d7..03ebdb61 100644
--- a/capybaraKV/capybarakv/src/kv2/slots_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/slots_v.rs
@@ -21,7 +21,6 @@ where
 {
     pub(super) proof fn lemma_filtering_keys_doesnt_affect_fold(self, pos: int)
         requires
-            self@.durable.m.dom().finite(),
             0 <= pos <= self@.durable.m.dom().to_seq().len(),
         ensures
             ({
@@ -73,7 +72,6 @@ where
 
     pub(super) proof fn lemma_used_list_slots_correspond(self)
         requires
-            self.inv_components_finite(),
             self.inv_components_correspond(),
             self.keys@.durable.valid(),
         ensures
@@ -186,7 +184,6 @@ where
 
     pub(super) proof fn lemma_used_slots_correspond(self)
         requires
-            self.inv_components_finite(),
             self.inv_components_correspond(),
             self.inv_components_valid(),
         ensures
diff --git a/capybaraKV/capybarakv/src/pmem/pmemutil_v.rs b/capybaraKV/capybarakv/src/pmem/pmemutil_v.rs
index 83746415..06bf9fa5 100644
--- a/capybaraKV/capybarakv/src/pmem/pmemutil_v.rs
+++ b/capybaraKV/capybarakv/src/pmem/pmemutil_v.rs
@@ -586,7 +586,7 @@ verus! {
             recover_fn(new_durable_state) == recover_fn(durable_state)
     {
         assert(new_durable_state.len() == durable_state.len());
-        assert forall|i: int| 0 <= i < durable_state.len() && !addrs.contains(i)
+        assert forall|i: int| #![trigger addrs.contains(i)] 0 <= i < durable_state.len() && !addrs.contains(i)
             implies new_durable_state[i] == durable_state[i] by {
             lemma_auto_can_result_from_partial_write_effect();
         }
diff --git a/capybaraKV/capybarakv/src/testkv_v.rs b/capybaraKV/capybarakv/src/testkv_v.rs
index 25cf3ba8..fa42d196 100644
--- a/capybaraKV/capybarakv/src/testkv_v.rs
+++ b/capybaraKV/capybarakv/src/testkv_v.rs
@@ -701,9 +701,9 @@ impl ReadLinearizer<TestKey, TestItem, TestListElement, ReadItemOp<TestKey>>
 {
     type Completion = Self;
 
-    open spec fn namespaces(self) -> Set<int>
+    open spec fn namespaces(self) -> ISet<int>
     {
-        Set::empty()
+        ISet::empty()
     }
 
     open spec fn pre(self, id: Loc, op: ReadItemOp<TestKey>) -> bool
@@ -753,9 +753,9 @@ where
 {
     type Completion = Self;
 
-    closed spec fn namespaces(self) -> Set<int>
+    closed spec fn namespaces(self) -> ISet<int>
     {
-        Set::empty()
+        ISet::empty()
     }
 
     closed spec fn pre(self, id: Loc, op: Op) -> bool
diff --git a/capybaraKV/pmcopy/rust-toolchain.toml b/capybaraKV/pmcopy/rust-toolchain.toml
index f25b5b14..14c86262 100644
--- a/capybaraKV/pmcopy/rust-toolchain.toml
+++ b/capybaraKV/pmcopy/rust-toolchain.toml
@@ -1,2 +1,2 @@
-[toolchain]
-channel = "1.95.0"
+[toolchain]
+channel = "1.96.0"
diff --git a/multilog/multilog/Cargo.toml b/multilog/multilog/Cargo.toml
index 66d2eb27..e6f52e9a 100644
--- a/multilog/multilog/Cargo.toml
+++ b/multilog/multilog/Cargo.toml
@@ -20,7 +20,7 @@ default = [ "pmem" ]
 crc64fast = "1.0.0"
 # Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features
 rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] }
-vstd = "0.0.0-2026-05-24-0157"
+vstd = { git = "https://github.com/verus-lang/verus.git" }
 pmsafe = { path = "../pmsafe" }
 [target.'cfg(target_os = "windows")'.dependencies]
 winapi = { version = "0.3.9", features = ["errhandlingapi", "fileapi", "handleapi", "memoryapi", "winbase", "winerror", "winnt"] }
@@ -34,6 +34,7 @@ memmap = "0.7.0"
 
 [lints.rust]
 unexpected_cfgs = { level = "allow", check-cfg = ["cfg(verus_keep_ghost)"] }
+unused_features = "allow"
 
 [package.metadata.verus]
 verify = true
diff --git a/multilog/pmsafe/rust-toolchain.toml b/multilog/pmsafe/rust-toolchain.toml
index f25b5b14..14c86262 100644
--- a/multilog/pmsafe/rust-toolchain.toml
+++ b/multilog/pmsafe/rust-toolchain.toml
@@ -1,2 +1,2 @@
-[toolchain]
-channel = "1.95.0"
+[toolchain]
+channel = "1.96.0"
diff --git a/pmemlog/Cargo.toml b/pmemlog/Cargo.toml
index 0a73a63f..cae39bf3 100644
--- a/pmemlog/Cargo.toml
+++ b/pmemlog/Cargo.toml
@@ -6,11 +6,12 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-vstd = "0.0.0-2026-05-24-0157"
+vstd = { git = "https://github.com/verus-lang/verus.git" }
 crc64fast = "1.0.0"
 
 [lints.rust]
 unexpected_cfgs = { level = "allow", check-cfg = ["cfg(verus_keep_ghost)"] }
+unused_features = "allow"
 
 [package.metadata.verus]
 verify = true
diff --git a/pmemlog/rust-toolchain.toml b/pmemlog/rust-toolchain.toml
index f25b5b14..14c86262 100644
--- a/pmemlog/rust-toolchain.toml
+++ b/pmemlog/rust-toolchain.toml
@@ -1,2 +1,2 @@
-[toolchain]
-channel = "1.95.0"
+[toolchain]
+channel = "1.96.0"
diff --git a/unverified/metadata_kv/Cargo.lock b/unverified/metadata_kv/Cargo.lock
index b213f1ab..fb9f9b39 100644
--- a/unverified/metadata_kv/Cargo.lock
+++ b/unverified/metadata_kv/Cargo.lock
@@ -514,14 +514,12 @@ checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
 [[package]]
 name = "verus_builtin"
 version = "0.0.0-2026-05-17-0151"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
+source = "git+https://github.com/verus-lang/verus.git#bdaaf5793bf445b3242adeb0d55423c7eab9fe10"
 
 [[package]]
 name = "verus_builtin_macros"
-version = "0.0.0-2026-05-24-0157"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9b5028291963009f075fd4fbfa883d176ad108afbeef54e950bc74cef4e1f9e"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#bdaaf5793bf445b3242adeb0d55423c7eab9fe10"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -533,9 +531,8 @@ dependencies = [
 
 [[package]]
 name = "verus_prettyplease"
-version = "0.0.0-2026-05-24-0157"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ed6977d81af3e0f2454f24833f2e82f50a0650254190584399d5476587083e51"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#bdaaf5793bf445b3242adeb0d55423c7eab9fe10"
 dependencies = [
  "proc-macro2",
  "verus_syn",
@@ -543,9 +540,8 @@ dependencies = [
 
 [[package]]
 name = "verus_state_machines_macros"
-version = "0.0.0-2026-05-24-0157"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "23036d788cacd25c4279130ef422124912bc199f351ef5f695d81009622a5458"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#bdaaf5793bf445b3242adeb0d55423c7eab9fe10"
 dependencies = [
  "indexmap 1.9.3",
  "proc-macro2",
@@ -555,9 +551,8 @@ dependencies = [
 
 [[package]]
 name = "verus_syn"
-version = "0.0.0-2026-05-24-0157"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0adef4208f95cd6cd0f27404afd9ffbbe3e09677b619a52d3f505ca43fa8f0a2"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#bdaaf5793bf445b3242adeb0d55423c7eab9fe10"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -566,9 +561,8 @@ dependencies = [
 
 [[package]]
 name = "vstd"
-version = "0.0.0-2026-05-24-0157"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "eef08139d238dfe8c1081513849f76136280c5699af0f88ad18dd95b3f72cfe0"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#bdaaf5793bf445b3242adeb0d55423c7eab9fe10"
 dependencies = [
  "verus_builtin",
  "verus_builtin_macros",
diff --git a/unverified/metadata_kv/Cargo.toml b/unverified/metadata_kv/Cargo.toml
index 5c0910ba..739d663f 100644
--- a/unverified/metadata_kv/Cargo.toml
+++ b/unverified/metadata_kv/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 # Avoid default features since @lopopolo reports that rand is unsound with both the log and thread_rng features
 rand = { version = "0.10.1", default-features = false, features = [ "thread_rng" ] }
-vstd = "0.0.0-2026-05-24-0157"
+vstd = { git = "https://github.com/verus-lang/verus.git" }
 proptest = "1.4"