Skip to content

Fix usability issue with unused subregions library #39

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 2 commits into from
Oct 20, 2025
Merged

Fix usability issue with unused subregions library #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e972230
Fix usability issue with unused subregions library
jaylorch Oct 16, 2025
6ef1628
Simplify spec for end position
jaylorch Oct 16, 2025
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
20 changes: 10 additions & 10 deletions capybaraKV/capybarakv/src/pmem/subregion_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -580,7 +580,7 @@ impl PoWERPersistentMemorySubregion
PMRegion: PersistentMemoryRegion,
requires
self.inv(powerpm, perm),
relative_addr + num_bytes <= self.len(),
relative_addr + num_bytes <= self.end(),
ensures
match result {
Ok(bytes) => {
Expand Down Expand Up @@ -651,7 +651,7 @@ impl PoWERPersistentMemorySubregion
PMRegion: PersistentMemoryRegion,
requires
self.inv(powerpm, perm),
relative_addr + S::spec_size_of() <= self.len(),
relative_addr + S::spec_size_of() <= self.end(),
self.view(powerpm).read_state.subrange(relative_addr as int, relative_addr + S::spec_size_of()) == true_val.spec_to_bytes(),
ensures
match result {
Expand Down Expand Up @@ -752,7 +752,7 @@ impl PoWERPersistentMemorySubregion
requires
self.inv(&*old(powerpm), perm),
self.start() <= absolute_addr,
absolute_addr + bytes@.len() <= self.len(),
absolute_addr + bytes@.len() <= self.end(),
forall |i: int| absolute_addr <= i < absolute_addr + bytes@.len() ==>
#[trigger] self.is_writable_absolute_addr_fn()(i),
ensures
Expand Down Expand Up @@ -815,7 +815,7 @@ impl PoWERPersistentMemorySubregion
requires
self.inv(&*old(powerpm), perm),
self.start() <= absolute_addr,
absolute_addr + S::spec_size_of() <= self.len(),
absolute_addr + S::spec_size_of() <= self.end(),
forall |i: int| absolute_addr <= i < absolute_addr + S::spec_size_of() ==>
#[trigger] self.is_writable_absolute_addr_fn()(i),
ensures
Expand Down Expand Up @@ -946,7 +946,7 @@ impl PersistentMemorySubregion
PMRegion: PersistentMemoryRegion,
requires
self.inv(pm),
relative_addr + num_bytes <= self.len(),
relative_addr + num_bytes <= self.end(),
ensures
pm.constants().valid(),
match result {
Expand Down Expand Up @@ -1025,7 +1025,7 @@ impl PersistentMemorySubregion
PMRegion: PersistentMemoryRegion,
requires
self.inv(pm),
relative_addr + S::spec_size_of() <= self.len(),
relative_addr + S::spec_size_of() <= self.end(),
S::bytes_parseable(extract_bytes(self.view(pm).read_state, relative_addr as nat, S::spec_size_of())),
ensures
pm.constants().valid(),
Expand Down Expand Up @@ -1343,7 +1343,7 @@ impl WritablePersistentMemorySubregion
) ->(result: Result<Vec<u8>, PmemError>)
requires
self.inv(pm),
relative_addr + num_bytes <= self.len(),
relative_addr + num_bytes <= self.end(),
ensures
match result {
Ok(bytes) => {
Expand Down Expand Up @@ -1418,7 +1418,7 @@ impl WritablePersistentMemorySubregion
PMRegion: PersistentMemoryRegion,
requires
self.inv(pm),
relative_addr < relative_addr + S::spec_size_of() <= self.len(),
relative_addr < relative_addr + S::spec_size_of() <= self.end(),
<S as PmCopyHelper>::bytes_parseable(
self.view(pm).read_state.subrange(relative_addr as int, relative_addr + S::spec_size_of())
),
Expand Down Expand Up @@ -1513,7 +1513,7 @@ impl WritablePersistentMemorySubregion
requires
self.inv(&*old(pm)),
self.start() <= absolute_addr,
absolute_addr + bytes@.len() <= self.len(),
absolute_addr + bytes@.len() <= self.end(),
forall |i: int| absolute_addr <= i < absolute_addr + bytes@.len() ==>
#[trigger] self.is_writable_absolute_addr_fn()(i),
ensures
Expand Down Expand Up @@ -1573,7 +1573,7 @@ impl WritablePersistentMemorySubregion
requires
self.inv(&*old(pm)),
self.start() <= absolute_addr,
absolute_addr + S::spec_size_of() <= self.len(),
absolute_addr + S::spec_size_of() <= self.end(),
forall |i: int| absolute_addr <= i < absolute_addr + S::spec_size_of() ==>
#[trigger] self.is_writable_absolute_addr_fn()(i),
ensures
Expand Down
1 change: 0 additions & 1 deletion multilog/multilog/src/multilog/util_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
use crate::pmem::pmemspec_t::*;
use crate::pmem::pmemutil_v::*;
use crate::pmem::pmcopy_t::*;
use crate::pmem::subregion_v::*;
use vstd::prelude::*;

verus! {
Expand Down
8 changes: 4 additions & 4 deletions multilog/multilog/src/pmem/subregion_v.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -586,7 +586,7 @@ impl WriteRestrictedPersistentMemorySubregion
requires
self.inv(old(wrpm), perm),
self.start() <= absolute_addr,
absolute_addr + bytes@.len() <= self.len(),
absolute_addr + bytes@.len() <= self.end(),
self.view(old(wrpm)).no_outstanding_writes_in_range(
absolute_addr - self.start(),
absolute_addr + bytes@.len() - self.start()
Expand Down Expand Up @@ -670,7 +670,7 @@ impl WriteRestrictedPersistentMemorySubregion
requires
self.inv(old(wrpm), perm),
self.start() <= absolute_addr,
absolute_addr + S::spec_size_of() <= self.len(),
absolute_addr + S::spec_size_of() <= self.end(),
self.view(old(wrpm)).no_outstanding_writes_in_range(
absolute_addr - self.start(),
absolute_addr + S::spec_size_of() - self.start()
Expand Down Expand Up @@ -1310,7 +1310,7 @@ impl WritablePersistentMemorySubregion
requires
self.inv(old(pm)),
self.start() <= absolute_addr,
absolute_addr + bytes@.len() <= self.len(),
absolute_addr + bytes@.len() <= self.end(),
self.view(old(pm)).no_outstanding_writes_in_range(
absolute_addr - self.start(),
absolute_addr + bytes@.len() - self.start()
Expand Down Expand Up @@ -1377,7 +1377,7 @@ impl WritablePersistentMemorySubregion
requires
self.inv(old(pm)),
self.start() <= absolute_addr,
absolute_addr + S::spec_size_of() <= self.len(),
absolute_addr + S::spec_size_of() <= self.end(),
self.view(old(pm)).no_outstanding_writes_in_range(
absolute_addr - self.start(),
absolute_addr + S::spec_size_of() - self.start()
Expand Down