verus: update to new resource algebras

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

capybaraKV/capybarakv/src/common/util_v.rs

@@ -152,7 +152,7 @@ pub exec fn clone_pmcopy_vec<T: PmCopy>(v: &Vec<T>) -> (result: Vec<T>)
 #[inline]
 pub exec fn extend_vec_u8_from_slice(v: &mut Vec<u8>, s: &[u8])
     ensures
-        v@ == old(v)@ + s@,
+        final(v)@ == old(v)@ + s@,
 {
     v.extend_from_slice(s);
     assert(v@ =~= old(v)@ + s@);

capybaraKV/capybarakv/src/journal/entry_v.rs

@@ -200,7 +200,7 @@ impl ConcreteJournalEntries
     #[inline]
     pub exec fn push(&mut self, e: ConcreteJournalEntry)
         ensures
-            self@ == old(self)@.push(e@)
+            final(self)@ == old(self)@.push(e@)
     {
         self.entries.push(e);
         assert(self@ =~= old(self)@.push(e@));
@@ -217,7 +217,7 @@ impl ConcreteJournalEntries
     #[inline]
     pub exec fn clear(&mut self)
         ensures
-            self@ == Seq::<JournalEntry>::empty(),
+            final(self)@ == Seq::<JournalEntry>::empty(),
     {
         self.entries.clear();
         assert(self@ =~= Seq::<JournalEntry>::empty());

capybaraKV/capybarakv/src/journal/impl_v.rs

@@ -1,14 +1,15 @@
 #![allow(unused_imports)]
-use vstd::prelude::*;
-use vstd::tokens::frac::*;
-use crate::common::subrange_v::*;
-use crate::pmem::pmcopy_t::*;
-use crate::pmem::pmemspec_t::*;
-use crate::pmem::power_t::*;
 use super::entry_v::*;
 use super::inv_v::*;
 use super::recover_v::*;
 use super::spec_v::*;
+use crate::common::subrange_v::*;
+use crate::pmem::pmcopy_t::*;
+use crate::pmem::pmemspec_t::*;
+use crate::pmem::power_t::*;
+use vstd::prelude::*;
+use vstd::resource::frac::*;
+use vstd::resource::ghost_var::*;
 
 verus! {
 
@@ -142,10 +143,10 @@ where
         requires
             old(self).valid(),
         ensures
-            self.valid(),
-            self@.valid(),
-            self.recover_idempotent(),
-            self@ == old(self)@.abort(),
+            final(self).valid(),
+            final(self)@.valid(),
+            final(self).recover_idempotent(),
+            final(self)@ == old(self)@.abort(),
     {
         self.journal_length = 0;
         self.journaled_addrs = Ghost(Set::<int>::empty());
@@ -156,9 +157,9 @@ where
         requires
             old(self).valid(),
         ensures
-            self.valid(),
-            self@ == old(self)@,
-            self@.durable_state == self@.read_state,
+            final(self).valid(),
+            final(self)@ == old(self)@,
+            final(self)@.durable_state == final(self)@.read_state,
     {
         self.powerpm.flush();
     }
@@ -170,4 +171,3 @@ pub open(super) spec fn spec_journal_entry_overhead() -> nat
 }
 
 }
-

capybaraKV/capybarakv/src/journal/setup_v.rs

@@ -203,27 +203,27 @@ where
         requires
             old(pm).inv(),
         ensures
-            pm.inv(),
-            pm.constants() == old(pm).constants(),
+            final(pm).inv(),
+            final(pm).constants() == old(pm).constants(),
             match result {
                 Ok(constants) => {
-                    &&& pm@.flush_predicted()
-                    &&& Self::recover(pm@.durable_state)
-                        == Some(RecoveredJournal{ constants: *jc, state: pm@.durable_state })
+                    &&& final(pm)@.flush_predicted()
+                    &&& Self::recover(final(pm)@.durable_state)
+                        == Some(RecoveredJournal{ constants: *jc, state: final(pm)@.durable_state })
                     &&& jc.app_area_start <= jc.app_area_end
-                    &&& jc.app_area_end == pm@.len()
-                    &&& seqs_match_in_range(old(pm)@.read_state, pm@.read_state, jc.app_area_start as int,
+                    &&& jc.app_area_end == final(pm)@.len()
+                    &&& seqs_match_in_range(old(pm)@.read_state, final(pm)@.read_state, jc.app_area_start as int,
                                            jc.app_area_end as int)
                 },
                 Err(JournalError::InvalidSetupParameters) => {
-                    &&& pm@ == old(pm)@
+                    &&& final(pm)@ == old(pm)@
                     &&& {
                            ||| jc.app_area_start > jc.app_area_end
-                           ||| jc.app_area_end != pm@.len()
+                           ||| jc.app_area_end != final(pm)@.len()
                        }
                 },
                 Err(JournalError::NotEnoughSpace) => {
-                    &&& pm@ == old(pm)@
+                    &&& final(pm)@ == old(pm)@
                     &&& jc.app_area_start < Self::spec_space_needed_for_setup(jc.journal_capacity as nat)
                 },
                 Err(_) => false,

capybaraKV/capybarakv/src/journal/spec_v.rs

@@ -1,6 +1,7 @@
-use vstd::prelude::*;
-use crate::pmem::pmemspec_t::*;
 use crate::common::subrange_v::*;
+use crate::pmem::pmemspec_t::*;
+use vstd::prelude::*;
+use vstd::resource::Loc;
 
 verus! {
 
@@ -42,7 +43,7 @@ pub struct JournalView {
     pub commit_state: Seq<u8>,
     pub remaining_capacity: int,
     pub journaled_addrs: Set<int>,
-    pub powerpm_id: int,
+    pub powerpm_id: Loc,
 }
 
 impl JournalView {

capybaraKV/capybarakv/src/journal/start_v.rs

@@ -174,15 +174,15 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2)
                 ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
-            powerpm.inv(),
-            powerpm.constants() == old(powerpm).constants(),
-            powerpm.id() == old(powerpm).id(),
-            powerpm@.len() == old(powerpm)@.len(),
-            powerpm@.valid(),
-            recover_journal(powerpm@.durable_state) == recover_journal(old(powerpm)@.durable_state),
-            apply_journal_entries(powerpm@.read_state, entries.skip(num_entries_installed + 1), *sm) == Some(commit_state),
-            seqs_match_in_range(old(powerpm)@.durable_state, powerpm@.durable_state, 0, sm.app_area_start as int),
-            seqs_match_in_range(old(powerpm)@.read_state, powerpm@.read_state, 0, sm.app_area_start as int),
+            final(powerpm).inv(),
+            final(powerpm).constants() == old(powerpm).constants(),
+            final(powerpm).id() == old(powerpm).id(),
+            final(powerpm)@.len() == old(powerpm)@.len(),
+            final(powerpm)@.valid(),
+            recover_journal(final(powerpm)@.durable_state) == recover_journal(old(powerpm)@.durable_state),
+            apply_journal_entries(final(powerpm)@.read_state, entries.skip(num_entries_installed + 1), *sm) == Some(commit_state),
+            seqs_match_in_range(old(powerpm)@.durable_state, final(powerpm)@.durable_state, 0, sm.app_area_start as int),
+            seqs_match_in_range(old(powerpm)@.read_state, final(powerpm)@.read_state, 0, sm.app_area_start as int),
     {
         proof {
             lemma_addresses_in_entry_dont_affect_recovery(powerpm@.durable_state, vm, *sm,
@@ -249,19 +249,19 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2)
                 ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
-            powerpm.inv(),
-            powerpm.constants() == old(powerpm).constants(),
-            powerpm.id() == old(powerpm).id(),
-            powerpm@.len() == old(powerpm)@.len(),
-            powerpm@.flush_predicted(),
-            recover_version_metadata(powerpm@.read_state) == Some(vm),
-            recover_static_metadata(powerpm@.read_state, vm) == Some(*sm),
-            recover_committed_cdb(powerpm@.read_state, *sm) == Some(true),
-            recover_journal_length(powerpm@.read_state, *sm) == Some(entries_bytes.len() as u64),
-            recover_journal_entries_bytes(powerpm@.read_state, *sm, entries_bytes.len() as u64) == Some(entries_bytes@),
-            apply_journal_entries(powerpm@.durable_state, entries, *sm) == Some(powerpm@.read_state),
-            apply_journal_entries(old(powerpm)@.read_state, entries, *sm) == Some(powerpm@.read_state),
-            recover_journal(powerpm@.durable_state) == recover_journal(old(powerpm)@.durable_state),
+            final(powerpm).inv(),
+            final(powerpm).constants() == old(powerpm).constants(),
+            final(powerpm).id() == old(powerpm).id(),
+            final(powerpm)@.len() == old(powerpm)@.len(),
+            final(powerpm)@.flush_predicted(),
+            recover_version_metadata(final(powerpm)@.read_state) == Some(vm),
+            recover_static_metadata(final(powerpm)@.read_state, vm) == Some(*sm),
+            recover_committed_cdb(final(powerpm)@.read_state, *sm) == Some(true),
+            recover_journal_length(final(powerpm)@.read_state, *sm) == Some(entries_bytes.len() as u64),
+            recover_journal_entries_bytes(final(powerpm)@.read_state, *sm, entries_bytes.len() as u64) == Some(entries_bytes@),
+            apply_journal_entries(final(powerpm)@.durable_state, entries, *sm) == Some(final(powerpm)@.read_state),
+            apply_journal_entries(old(powerpm)@.read_state, entries, *sm) == Some(final(powerpm)@.read_state),
+            recover_journal(final(powerpm)@.durable_state) == recover_journal(old(powerpm)@.durable_state),
     {
         let mut start: usize = 0;
         let end: usize = entries_bytes.len();
@@ -386,15 +386,15 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| spec_recovery_equivalent_for_app(s1, s2)
                 ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
-            powerpm.inv(),
-            powerpm.constants() == old(powerpm).constants(),
-            powerpm.id() == old(powerpm).id(),
-            powerpm@.len() == old(powerpm)@.len(),
-            powerpm@.flush_predicted(),
-            recover_version_metadata(powerpm@.read_state) == Some(vm),
-            recover_static_metadata(powerpm@.read_state, vm) == Some(*sm),
-            recover_committed_cdb(powerpm@.read_state, *sm) == Some(false),
-            spec_recovery_equivalent_for_app(powerpm@.durable_state, old(powerpm)@.durable_state),
+            final(powerpm).inv(),
+            final(powerpm).constants() == old(powerpm).constants(),
+            final(powerpm).id() == old(powerpm).id(),
+            final(powerpm)@.len() == old(powerpm)@.len(),
+            final(powerpm)@.flush_predicted(),
+            recover_version_metadata(final(powerpm)@.read_state) == Some(vm),
+            recover_static_metadata(final(powerpm)@.read_state, vm) == Some(*sm),
+            recover_committed_cdb(final(powerpm)@.read_state, *sm) == Some(false),
+            spec_recovery_equivalent_for_app(final(powerpm)@.durable_state, old(powerpm)@.durable_state),
     {
         let new_cdb: u64 = CDB_FALSE;
         let ghost new_state = update_bytes(powerpm@.durable_state, sm.committed_cdb_start as int,

capybaraKV/capybarakv/src/journal/write_v.rs

@@ -59,7 +59,7 @@ where
         requires
             old(self).write_preconditions(addr, bytes_to_write@, perm),
         ensures
-            self.write_postconditions(*old(self), addr, bytes_to_write@),
+            final(self).write_postconditions(*old(self), addr, bytes_to_write@),
     {
         broadcast use broadcast_seqs_match_in_range_can_narrow_range;
         broadcast use broadcast_update_bytes_effect;
@@ -102,7 +102,7 @@ where
         requires
             old(self).write_preconditions(addr, bytes_to_write@, perm),
         ensures
-            self.write_postconditions(*old(self), addr, bytes_to_write@),
+            final(self).write_postconditions(*old(self), addr, bytes_to_write@),
     {
         self.write_slice::<Perm>(addr, bytes_to_write.as_slice(), Tracked(perm))
     }
@@ -120,7 +120,7 @@ where
         requires
             old(self).write_preconditions(addr, object.spec_to_bytes(), perm),
         ensures
-            self.write_postconditions(*old(self), addr, object.spec_to_bytes()),
+            final(self).write_postconditions(*old(self), addr, object.spec_to_bytes()),
     {
         broadcast use pmcopy_axioms;
         self.write_slice::<Perm>(addr, object.as_byte_slice(), Tracked(perm))
@@ -136,26 +136,26 @@ where
             old(self)@.constants.app_area_start <= addr,
             addr + bytes_to_write.len() <= old(self)@.constants.app_area_end,
         ensures
-            self.valid(),
-            self@.valid(),
-            self.recover_idempotent(),
+            final(self).valid(),
+            final(self)@.valid(),
+            final(self).recover_idempotent(),
             ({
                 let space_needed = spec_journal_entry_overhead() + bytes_to_write@.len();
                 match result {
                     Ok(_) => {
                         &&& space_needed <= old(self)@.remaining_capacity
-                        &&& self@ == (JournalView{
+                        &&& 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()),
                                remaining_capacity: old(self)@.remaining_capacity - space_needed,
                                ..old(self)@
                            })
-                        &&& self@.matches_except_in_range(old(self)@, addr as int, addr + bytes_to_write.len())
+                        &&& final(self)@.matches_except_in_range(old(self)@, addr as int, addr + bytes_to_write.len())
                     },
                     Err(JournalError::NotEnoughSpace) => {
                         &&& space_needed > old(self)@.remaining_capacity
-                        &&& *self == *old(self)
+                        &&& *final(self) == *old(self)
                     },
                     Err(_) => false,
                 }

capybaraKV/capybarakv/src/kv2/abort_v.rs

@@ -22,9 +22,9 @@ where
         requires 
             old(self).valid(),
         ensures 
-            self.valid(),
+            final(self).valid(),
             match result {
-                Ok(()) => self@ == old(self)@.abort(),
+                Ok(()) => final(self)@ == old(self)@.abort(),
                 Err(_) => false,
             }
     {
@@ -39,9 +39,9 @@ where
             old(self).inv(),
             old(self).status@ is MustAbort,
         ensures 
-            self.valid(),
-            self@ == old(self)@.abort(),
-            self.journal@.durable_state == self.journal@.read_state,
+            final(self).valid(),
+            final(self)@ == old(self)@.abort(),
+            final(self).journal@.durable_state == final(self).journal@.read_state,
     {
         let ghost jv_before_abort = self.journal@;
         self.journal.abort();

capybaraKV/capybarakv/src/kv2/commit_v.rs

@@ -1,15 +1,16 @@
 #![allow(unused_imports)]
 use vstd::prelude::*;
-use vstd::tokens::frac::*;
+use vstd::resource::frac::*;
+use vstd::resource::ghost_var::*;
 
+use super::impl_v::*;
+use super::recover_v::*;
+use super::spec_t::*;
 use crate::common::subrange_v::*;
-use crate::pmem::pmemspec_t::*;
 use crate::pmem::pmcopy_t::*;
+use crate::pmem::pmemspec_t::*;
 use crate::pmem::power_t::*;
 use std::hash::Hash;
-use super::impl_v::*;
-use super::recover_v::*;
-use super::spec_t::*;
 
 verus! {
 
@@ -22,12 +23,12 @@ where
     L: PmCopy + LogicalRange + std::fmt::Debug + Copy,
 {
     pub exec fn commit<Perm>(
-        &mut self, 
+        &mut self,
         Tracked(perm): Tracked<Perm>
     ) -> (result: Result<Tracked<Perm::Completion>, KvError>)
         where
             Perm: CheckPermission<Seq<u8>>,
-        requires 
+        requires
             old(self).valid(),
             perm.id() == old(self)@.powerpm_id,
             forall|s1: Seq<u8>, s2: Seq<u8>| ({
@@ -37,11 +38,11 @@ where
                 &&& Self::recover(s1) == Some(RecoveredKvStore::<K, I, L>{ ps: old(self)@.ps, kv: old(self)@.durable })
                 &&& Self::recover(s2) == Some(RecoveredKvStore::<K, I, L>{ ps: old(self)@.ps, kv: old(self)@.durable })
             }) ==> #[trigger] perm.permits(s1, s2),
-        ensures 
-            self.valid(),
+        ensures
+            final(self).valid(),
             match result {
                 Ok(complete) => {
-                    &&& self@ == old(self)@.commit()
+                    &&& final(self)@ == old(self)@.commit()
                     &&& perm.completed(complete@)
                 },
                 Err(_) => false,