Adapt to finite sets and maps

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

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.

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

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

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);
 

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;
 

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)

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 },

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 },

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);
         }
 

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),
     )
 }

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)

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);

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

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()
                 },

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,32 +453,27 @@ 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 {
             assert(self.row_info[free_list[pos]] is InFreeList);
             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,