Adaptations for the upcoming change to the new iterator interface.

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-06-1803"
+vstd = "0.0.0-2026-05-10-0145"
 pmcopy = { path = "../pmcopy" }
 
 [target.'cfg(target_family = "unix")'.dependencies]

capybaraKV/capybarakv/src/kv2/keys/crud_v.rs

@@ -17,6 +17,8 @@ use super::super::spec_t::*;
 use vstd::slice::slice_to_vec;
 #[cfg(verus_keep_ghost)]
 use vstd::std_specs::hash::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::iter::IteratorSpec;
 
 verus! {
 
@@ -708,21 +710,19 @@ where
     {
         broadcast use vstd::std_specs::hash::group_hash_axioms;
 
-        let keys = self.m.keys();
         let mut result = Vec::<K>::new();
-        assert(result@ =~= keys@.1.take(0));
-
-        for k in iter: keys
+        let ghost keys = self.m.keys();
+        for k in iter: self.m.keys()
             invariant
-                result@ == iter@,
+                result@ == iter.seq().take(iter.index@).unref(),
         {
-            assert(iter.keys.take(iter.pos).push(*k) =~= iter.keys.take(iter.pos + 1));
             result.push(*k);
         }
 
         assert(result@.to_set() =~= self@.tentative.unwrap().key_info.dom()) by {
-            assert(keys@.1.to_set() == self.m@.dom());
-            assert(keys@.1.take(keys@.1.len() as int) =~= keys@.1);
+             assert(keys.remaining().take(keys.remaining().len() as int) == keys.remaining());
+//            assert(keys.remaining().to_set() == self.m@.dom());
+//            assert(keys@.1.take(keys@.1.len() as int) =~= keys@.1);
             assert(self.m@.dom() =~= self@.tentative.unwrap().key_info.dom());
         }
 

capybaraKV/capybarakv/src/kv2/shardkv_v.rs

@@ -270,6 +270,13 @@ where
 
         for idx in 0..nshards
             invariant
+                nshards >= 1,
+                forall |shard| 0 <= shard < nshards ==> #[trigger] shard_res_old.contains_key(shard),
+                forall |shard| #[trigger] shard_res_old.contains_key(shard) ==> {
+                    &&& shard_res_old[shard]@.ps == ps
+                    &&& shard_res_old[shard]@.pm_constants == pm_constants
+                    &&& shard_res_old[shard]@.kv == RecoveredKvStore::<K, I, L>::init(ps).kv
+                },
                 pred.shard_ids.len() == idx,
                 pred.combined_id == shardstates.combined.id(),
                 pred.combined_id == combined_res.id(),

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-06-1803"
+vstd = "0.0.0-2026-05-10-0145"
 pmsafe = { path = "../pmsafe" }
 [target.'cfg(target_os = "windows")'.dependencies]
 winapi = { version = "0.3.9", features = ["errhandlingapi", "fileapi", "handleapi", "memoryapi", "winbase", "winerror", "winnt"] }

multilog/multilog/src/multilog/multilogimpl_v.rs

@@ -1121,9 +1121,10 @@ verus! {
             // area, if flushed, would be consistent with `self.infos` and
             // `self.state`.
 
-            for current_log in iter: 0..self.num_logs
+            let num_logs = self.num_logs;
+            for current_log in iter: 0..num_logs
                 invariant
-                    iter.end == self.num_logs, // we need to remember this since `self` is changed in the loop body
+                    iter.snapshot@.end == self.num_logs, // we need to remember this since `self` is changed in the loop body
                     wrpm_regions.inv(),
 
                     memory_matches_deserialized_cdb(wrpm_regions@, self.cdb),

multilog/multilog/src/multilog/setup_v.rs

@@ -77,7 +77,7 @@ verus! {
         let mut result = Vec::<u64>::new();
         for which_region in iter: 0..region_sizes.len()
             invariant
-                iter.end == region_sizes.len(),
+                iter.snapshot@.end == region_sizes.len(),
                 forall |i: int| 0 <= i < region_sizes.len() ==> region_sizes[i] >= ABSOLUTE_POS_OF_LOG_AREA + MIN_LOG_AREA_SIZE,
                 result.len() == which_region,
                 forall |i: int| 0 <= i < which_region ==>

multilog/multilog/src/pmem/pmemutil_v.rs

@@ -154,9 +154,10 @@ verus! {
             forall |i: int| 0 <= i < pm_regions@.len() ==> result@[i] == #[trigger] pm_regions@[i].len()
     {
         let mut result: Vec<u64> = Vec::<u64>::new();
-        for which_region in iter: 0..pm_regions.get_num_regions()
+        let num_regions = pm_regions.get_num_regions();
+        for which_region in iter: 0..num_regions
             invariant
-                iter.end == pm_regions@.len(),
+                iter.snapshot@.end == num_regions == pm_regions@.len(),
                 pm_regions.inv(),
                 result@.len() == which_region,
                 forall |i: int| 0 <= i < which_region ==> result@[i] == #[trigger] pm_regions@[i].len(),

pmemlog/Cargo.toml

@@ -6,7 +6,7 @@ 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-06-1803"
+vstd = "0.0.0-2026-05-10-0145"
 crc64fast = "1.0.0"
 
 [lints.rust]