Skip to content

Make compatible with latest Verus #42

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hayley-leblanc merged 1 commit into from
Feb 6, 2026
Merged

Make compatible with latest Verus #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion capybaraKV/capybarakv/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ default = [ "pmem" ]
[dependencies]
crc64fast = "1.0.0"
rand = "0.8.5"
vstd = "0.0.0-2025-11-30-0053"
vstd = "0.0.0-2026-01-25-0057"
pmcopy = { path = "../pmcopy" }

[target.'cfg(target_family = "unix")'.dependencies]
Expand Down
16 changes: 8 additions & 8 deletions capybaraKV/capybarakv/src/journal/commit_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ where
forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
ensures
self.inv(),
self == (Self{
*self == (Self{
powerpm: self.powerpm,
..*old(self)
}),
Expand Down Expand Up @@ -207,7 +207,7 @@ where
forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
ensures
self.inv(),
self == (Self{
*self == (Self{
powerpm: self.powerpm,
..*old(self)
}),
Expand Down Expand Up @@ -256,7 +256,7 @@ where
self.sm.app_area_start as int, self.sm.app_area_end as int),
seqs_match_in_range(original_read_state, self.powerpm@.read_state,
self.sm.app_area_start as int, self.sm.app_area_end as int),
self == (Self{ powerpm: self.powerpm, ..*old(self) }),
*self == (Self{ powerpm: self.powerpm, ..*old(self) }),
crc_digest.bytes_in_digest() ==
self.powerpm@.read_state.subrange(self.sm.journal_entries_start as int, current_pos as int),
perm_factory.id() == self@.powerpm_id,
Expand Down Expand Up @@ -290,7 +290,7 @@ where
self.inv(),
self.powerpm.constants() == old(self).powerpm.constants(),
self.powerpm.id() == old(self).powerpm.id(),
self == (Self{
*self == (Self{
powerpm: self.powerpm,
..*old(self)
}),
Expand Down Expand Up @@ -366,7 +366,7 @@ where
self.inv(),
self.powerpm.constants() == old(self).powerpm.constants(),
self.powerpm.id() == old(self).powerpm.id(),
self == (Self{
*self == (Self{
status: Ghost(JournalStatus::Committed),
powerpm: self.powerpm,
..*old(self)
Expand Down Expand Up @@ -471,7 +471,7 @@ where
forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
ensures
self.inv(),
self == (Self{
*self == (Self{
powerpm: self.powerpm,
..*old(self)
}),
Expand Down Expand Up @@ -563,7 +563,7 @@ where
forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
ensures
self.inv(),
self == (Self{
*self == (Self{
powerpm: self.powerpm,
..*old(self)
}),
Expand Down Expand Up @@ -614,7 +614,7 @@ where
seqs_match_in_range(original_commit_state, desired_commit_state,
self.sm.app_area_start as int, self.sm.app_area_end as int),
recovers_to(original_commit_state, old(self).vm@, old(self).sm, old(self).constants),
self == (Self{ powerpm: self.powerpm, ..*old(self) }),
*self == (Self{ powerpm: self.powerpm, ..*old(self) }),
self.powerpm.constants() == old(self).powerpm.constants(),
self.powerpm.id() == old(self).powerpm.id(),
perm_factory.id() == self@.powerpm_id,
Expand Down
2 changes: 1 addition & 1 deletion capybaraKV/capybarakv/src/journal/write_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,7 @@ where
},
Err(JournalError::NotEnoughSpace) => {
&&& space_needed > old(self)@.remaining_capacity
&&& self == old(self)
&&& *self == *old(self)
},
Err(_) => false,
}
Expand Down
4 changes: 2 additions & 2 deletions capybaraKV/capybarakv/src/kv2/elements_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,8 +153,8 @@ where
Ok(list_addr) => {
let old_list = if former_rm.list_addr == 0 { Seq::<L>::empty() }
else { old(self).lists@.tentative.unwrap().m[former_rm.list_addr] };
&&& self == Self{ status: Ghost(KvStoreStatus::ComponentsDontCorrespond),
journal: self.journal, lists: self.lists, ..*old(self) }
&&& *self == Self{ status: Ghost(KvStoreStatus::ComponentsDontCorrespond),
journal: self.journal, lists: self.lists, ..*old(self) }
&&& self.inv()
&&& list_addr != 0
&&& list_addr == former_rm.list_addr || !old(self).lists@.tentative.unwrap().m.contains_key(list_addr)
Expand Down
4 changes: 2 additions & 2 deletions capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ where
Ok(row_addr) => {
&&& 0 < self.free_list@.len()
&&& row_addr == self.free_list@.last()
&&& self == (Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) })
&&& *self == (Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) })
&&& recover_cdb(journal@.commit_state, row_addr + self.sm.row_cdb_start) == Some(true)
&&& seqs_match_except_in_range(old(journal)@.commit_state, journal@.commit_state,
row_addr as int, row_addr + self.sm.table.row_size)
Expand Down Expand Up @@ -524,7 +524,7 @@ where
journal@.powerpm_id == old(journal)@.powerpm_id,
match result {
Ok(()) => {
&&& self == Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) }
&&& *self == Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) }
&&& self.inv(journal@)
&&& self.internal_view().consistent_with_journaled_addrs(journal@.journaled_addrs, self.sm)
&&& journal@.matches_except_in_range(old(journal)@, row_addr + self.sm.row_metadata_start,
Expand Down
10 changes: 5 additions & 5 deletions capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ where
&&& !(old(self).m@[list_addr] is Durable)
}),
ensures
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
self.internal_view() == (ListTableInternalView{ m: self.internal_view().m, ..old(self).internal_view() }),
forall|i: int| 0 <= i < self.modifications.len() ==>
(#[trigger] old(self).modifications[i] matches Some(list_addr) ==> !self.m@.contains_key(list_addr)),
Expand All @@ -113,7 +113,7 @@ where

for which_modification in 0..num_modifications
invariant
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
num_modifications == self.modifications.len(),
forall|i: int| 0 <= i < old(self).modifications.len() ==>
(#[trigger] old(self).modifications[i] matches Some(list_addr) ==> {
Expand Down Expand Up @@ -154,7 +154,7 @@ where
},
forall|list_addr: u64| #[trigger] old(self).m@.contains_key(list_addr) ==> old(self).m@[list_addr] is Durable,
ensures
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
forall|i: int| #![trigger self.deletes[i]] 0 <= i < self.deletes.len() ==> {
let summary = self.deletes[i];
&&& self.m@.contains_key(summary.head)
Expand Down Expand Up @@ -188,7 +188,7 @@ where

for which_delete in 0..num_deletes
invariant
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
num_deletes == self.deletes.len(),
forall|list_addr: u64| #[trigger] self.deletes_inverse@.contains_key(list_addr) ==> {
let which_delete = self.deletes_inverse@[list_addr];
Expand Down Expand Up @@ -244,7 +244,7 @@ where
requires
old(self).valid(jv),
ensures
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
self.internal_view().m == old(self).internal_view().abort().m,
{
self.update_m_to_reflect_abort_of_modifications();
Expand Down
4 changes: 2 additions & 2 deletions capybaraKV/capybarakv/src/kv2/lists/append_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -423,7 +423,7 @@ where
Ghost(prev_jv): Ghost<JournalView>,
) -> (result: Result<u64, KvError>)
requires
old(self) == (Self{
*old(self) == (Self{
free_list: old(self).free_list,
m: old(self).m,
..prev_self
Expand Down Expand Up @@ -580,7 +580,7 @@ where
Ghost(prev_jv): Ghost<JournalView>,
) -> (result: Result<u64, KvError>)
requires
old(self) == (Self{
*old(self) == (Self{
free_list: old(self).free_list,
m: old(self).m,
..prev_self
Expand Down
6 changes: 3 additions & 3 deletions capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ where
(#[trigger] old(self).modifications[which_modification] matches Some(list_addr) ==>
old(self).m@.contains_key(list_addr)),
ensures
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
forall|i: int| 0 <= i < self.modifications.len() ==>
(#[trigger] old(self).modifications[i] matches Some(list_addr) ==> {
&&& self.m@.contains_key(list_addr)
Expand All @@ -115,7 +115,7 @@ where
let num_modifications = self.modifications.len();
for which_modification in 0..num_modifications
invariant
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
num_modifications == self.modifications.len(),
forall|i: int| 0 <= i < old(self).modifications.len() ==>
(#[trigger] old(self).modifications[i] matches Some(list_addr) ==>
Expand Down Expand Up @@ -153,7 +153,7 @@ where
requires
old(self).valid(jv),
ensures
self == (Self{ m: self.m, ..*old(self) }),
*self == (Self{ m: self.m, ..*old(self) }),
self.internal_view().m == old(self).internal_view().commit().m,
{
self.update_m_to_reflect_commit_of_modifications();
Expand Down
8 changes: 4 additions & 4 deletions capybaraKV/capybarakv/src/kv2/lists/update_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -519,7 +519,7 @@ where
requires
prev_self.valid(journal@),
journal.valid(),
old(self) == (Self{
*old(self) == (Self{
m: old(self).m,
..prev_self
}),
Expand All @@ -530,8 +530,8 @@ where
old(self).m@ == prev_self.m@.remove(list_addr),
ensures
journal.valid(),
self == (Self{ m: self.m, deletes: self.deletes, deletes_inverse: self.deletes_inverse,
modifications: self.modifications, ..*old(self) }),
*self == (Self{ m: self.m, deletes: self.deletes, deletes_inverse: self.deletes_inverse,
modifications: self.modifications, ..*old(self) }),
({
let (success, new_entry) = result;
if success {
Expand All @@ -551,7 +551,7 @@ where
}
else {
&&& !journal@.pm_constants.impervious_to_corruption()
&&& self == old(self)
&&& *self == *old(self)
&&& new_entry == entry
}
}),
Expand Down
2 changes: 1 addition & 1 deletion multilog/multilog/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ default = [ "pmem" ]
[dependencies]
crc64fast = "1.0.0"
rand = "0.8.5"
vstd = "0.0.0-2025-11-30-0053"
vstd = "0.0.0-2026-01-25-0057"
pmsafe = { path = "../pmsafe" }

[target.'cfg(target_os = "windows")'.dependencies]
Expand Down
2 changes: 1 addition & 1 deletion pmemlog/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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-2025-11-30-0053"
vstd = "0.0.0-2026-01-25-0057"
crc64fast = "1.0.0"

[lints.rust]
Expand Down
2 changes: 1 addition & 1 deletion unverified/metadata_kv/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,5 @@ edition = "2021"

[dependencies]
rand = "0.8"
vstd = "0.0.0-2025-11-30-0053"
vstd = "0.0.0-2026-01-25-0057"
proptest = "1.4"
Loading