Fix nightly-verita, update to version 2026-09-20 (#62)

The last nightly-verita run had two rlimit timeouts. This PR makes those two function proofs more robust by breaking them down a bit. It also updates to use the latest Verus version, 2026-09-20.

This PR was generated by prompting GPT-5.6 Sol.

Author: jaylorch

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 = { version = "=0.0.0-2026-09-16-0054" }
+vstd = { version = "=0.0.0-2026-09-20-0158" }
 pmcopy = { path = "../pmcopy" }
 
 [target.'cfg(target_family = "unix")'.dependencies]

capybaraKV/capybarakv/src/journal/spec_v.rs

@@ -82,6 +82,25 @@ impl JournalView {
         &&& self.matches_in_range(other, end, self.constants.app_area_end as int)
     }
 
+    pub proof fn lemma_matches_except_in_range_can_widen(
+        self,
+        other: JournalView,
+        inner_start: int,
+        inner_end: int,
+        outer_start: int,
+        outer_end: int,
+    )
+        requires
+            self.matches_except_in_range(other, inner_start, inner_end),
+            self.constants.app_area_start <= outer_start <= inner_start,
+            inner_start <= inner_end,
+            inner_end <= outer_end <= self.constants.app_area_end,
+        ensures
+            self.matches_except_in_range(other, outer_start, outer_end),
+    {
+        broadcast use broadcast_seqs_match_in_range_can_narrow_range;
+    }
+
     pub open spec fn abort(self) -> Self
     {
         JournalView{

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

@@ -357,11 +357,6 @@ where
                 _ => false,
             },
     {
-        proof {
-            journal.lemma_valid_implications();
-            self.lemma_valid_implications(journal@);
-        }
-
         let row_addr = match self.create_step1(k, item_addr, journal) {
             Ok(r) => r,
             Err(e) => { return Err(e); },
@@ -388,12 +383,11 @@ where
 
         self.status = Ghost(KeyTableStatus::Quiescent);
 
-        proof {
+        assert(self.valid(journal@)) by {
             broadcast use broadcast_seqs_match_in_range_can_narrow_range;
             broadcast use group_validate_row_addr;
         }
 
-        assert(self.valid(journal@));
         assert(self@.tentative =~= Some(old(self)@.tentative.unwrap().create(*k, item_addr)));
         Ok(())
     }
@@ -685,14 +679,26 @@ where
             assert(self.undo_records@.last() =~= undo_record);
         }
 
-        proof {
-            broadcast use broadcast_seqs_match_in_range_can_narrow_range;
+        self.status = Ghost(KeyTableStatus::Quiescent);
+
+        assert(journal@.matches_except_in_range(old(journal)@,
+                                                self@.sm.start() as int,
+                                                self@.sm.end() as int)) by {
             broadcast use group_validate_row_addr;
+            journal@.lemma_matches_except_in_range_can_widen(
+                old(journal)@,
+                row_addr + self.sm.row_metadata_start,
+                row_addr + self.sm.row_metadata_crc_start + u64::spec_size_of(),
+                self@.sm.start() as int,
+                self@.sm.end() as int,
+            );
         }
 
-        self.status = Ghost(KeyTableStatus::Quiescent);
+        assert(self.valid(journal@)) by {
+            broadcast use broadcast_seqs_match_in_range_can_narrow_range;
+            broadcast use group_validate_row_addr;
+        }
 
-        assert(self.valid(journal@));
         assert(self@.tentative =~= Some(old(self)@.tentative.unwrap().update(*k, new_rm, former_rm)));
         Ok(())
     }

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

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 = { version = "=0.0.0-2026-09-16-0054" }
+vstd = { version = "=0.0.0-2026-09-20-0158" }
 crc64fast = "1.0.0"
 
 [lints.rust]

unverified/metadata_kv/Cargo.lock

@@ -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 = { version = "=0.0.0-2026-09-16-0054" }
+vstd = { version = "=0.0.0-2026-09-20-0158" }
 proptest = "1.4"