From b8cb24f77884fe1714f1f803fd325a89af8ba1c1 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 27 Apr 2026 21:49:09 -0400 Subject: [PATCH 1/4] Adaptations for the upcoming change to the new iterator interface. --- capybaraKV/capybarakv/src/kv2/keys/crud_v.rs | 16 ++++++++-------- multilog/multilog/src/multilog/multilogimpl_v.rs | 5 +++-- multilog/multilog/src/multilog/setup_v.rs | 2 +- multilog/multilog/src/pmem/pmemutil_v.rs | 5 +++-- 4 files changed, 15 insertions(+), 13 deletions(-) diff --git a/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs b/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs index 6a223f923..a6c67e11d 100644 --- a/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs +++ b/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::::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()); } diff --git a/multilog/multilog/src/multilog/multilogimpl_v.rs b/multilog/multilog/src/multilog/multilogimpl_v.rs index ba4ea610c..ff732f0b5 100644 --- a/multilog/multilog/src/multilog/multilogimpl_v.rs +++ b/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), diff --git a/multilog/multilog/src/multilog/setup_v.rs b/multilog/multilog/src/multilog/setup_v.rs index b93ee559b..ff007bee1 100644 --- a/multilog/multilog/src/multilog/setup_v.rs +++ b/multilog/multilog/src/multilog/setup_v.rs @@ -77,7 +77,7 @@ verus! { let mut result = Vec::::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 ==> diff --git a/multilog/multilog/src/pmem/pmemutil_v.rs b/multilog/multilog/src/pmem/pmemutil_v.rs index a6e7cb4b9..08678d7ff 100644 --- a/multilog/multilog/src/pmem/pmemutil_v.rs +++ b/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 = Vec::::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(), From 18c03c2efb512353efbe6f96d8a7026ff0419dc4 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Sun, 10 May 2026 17:37:52 -0400 Subject: [PATCH 2/4] Update vstd versions --- capybaraKV/capybarakv/Cargo.toml | 2 +- multilog/multilog/Cargo.toml | 2 +- pmemlog/Cargo.toml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/capybaraKV/capybarakv/Cargo.toml b/capybaraKV/capybarakv/Cargo.toml index cfe7e6c6d..ce5de9ce0 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-04-20-1748" +vstd = "0.0.0-2026-05-10-0145" pmcopy = { path = "../pmcopy" } [target.'cfg(target_family = "unix")'.dependencies] diff --git a/multilog/multilog/Cargo.toml b/multilog/multilog/Cargo.toml index e9ec63429..aac07d5b4 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-04-20-1748" +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"] } diff --git a/pmemlog/Cargo.toml b/pmemlog/Cargo.toml index 912a9ccba..34aa7e9e6 100644 --- a/pmemlog/Cargo.toml +++ b/pmemlog/Cargo.toml @@ -6,11 +6,11 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -vstd = "0.0.0-2026-04-20-1748" +vstd = "0.0.0-2026-05-10-0145" crc64fast = "1.0.0" [lints.rust] unexpected_cfgs = { level = "allow", check-cfg = ["cfg(verus_keep_ghost)"] } [package.metadata.verus] -verify = true \ No newline at end of file +verify = true From 9cf8adae1455fbdb133111b3f53ace7e63f4ab98 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 11 May 2026 16:23:28 -0400 Subject: [PATCH 3/4] Ad hoc fix to stabilize a proof. --- capybaraKV/capybarakv/src/kv2/shardkv_v.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs index 3f932c7ca..45db90ff8 100644 --- a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs +++ b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs @@ -238,6 +238,7 @@ where self.inv@.constant().combined_id } + #[verifier::spinoff_prover] exec fn setup( nshards: usize, Tracked(shard_res): Tracked>>>, From 9e080a846d2023c825709f49ceb142a514b59c66 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 11 May 2026 20:13:17 -0400 Subject: [PATCH 4/4] Add some additional loop invariants that @jaylorch suggested, and remove the spinoff_prover --- capybaraKV/capybarakv/src/kv2/shardkv_v.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs index 45db90ff8..a4e555abf 100644 --- a/capybaraKV/capybarakv/src/kv2/shardkv_v.rs +++ b/capybaraKV/capybarakv/src/kv2/shardkv_v.rs @@ -238,7 +238,6 @@ where self.inv@.constant().combined_id } - #[verifier::spinoff_prover] exec fn setup( nshards: usize, Tracked(shard_res): Tracked>>>, @@ -271,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::::init(ps).kv + }, pred.shard_ids.len() == idx, pred.combined_id == shardstates.combined.id(), pred.combined_id == combined_res.id(),