From e9722303690cf6142444dc1a349fa66475da3af3 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Thu, 16 Oct 2025 14:30:27 -0700 Subject: [PATCH 1/2] Fix usability issue with unused subregions library --- capybaraKV/capybarakv/src/pmem/subregion_v.rs | 20 +++++++++---------- multilog/multilog/src/multilog/util_v.rs | 1 - multilog/multilog/src/pmem/subregion_v.rs | 8 ++++---- 3 files changed, 14 insertions(+), 15 deletions(-) diff --git a/capybaraKV/capybarakv/src/pmem/subregion_v.rs b/capybaraKV/capybarakv/src/pmem/subregion_v.rs index 77df0e168..77c4f7529 100644 --- a/capybaraKV/capybarakv/src/pmem/subregion_v.rs +++ b/capybaraKV/capybarakv/src/pmem/subregion_v.rs @@ -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) => { @@ -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 { @@ -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 @@ -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 @@ -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 { @@ -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(), @@ -1343,7 +1343,7 @@ impl WritablePersistentMemorySubregion ) ->(result: Result, PmemError>) requires self.inv(pm), - relative_addr + num_bytes <= self.len(), + relative_addr + num_bytes <= self.end(), ensures match result { Ok(bytes) => { @@ -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(), ::bytes_parseable( self.view(pm).read_state.subrange(relative_addr as int, relative_addr + S::spec_size_of()) ), @@ -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 @@ -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 diff --git a/multilog/multilog/src/multilog/util_v.rs b/multilog/multilog/src/multilog/util_v.rs index 606577dae..d6b36925e 100644 --- a/multilog/multilog/src/multilog/util_v.rs +++ b/multilog/multilog/src/multilog/util_v.rs @@ -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! { diff --git a/multilog/multilog/src/pmem/subregion_v.rs b/multilog/multilog/src/pmem/subregion_v.rs index cf9a475f0..4b16c6eda 100644 --- a/multilog/multilog/src/pmem/subregion_v.rs +++ b/multilog/multilog/src/pmem/subregion_v.rs @@ -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.start() + self.len(), self.view(old(wrpm)).no_outstanding_writes_in_range( absolute_addr - self.start(), absolute_addr + bytes@.len() - self.start() @@ -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.start() + self.len(), self.view(old(wrpm)).no_outstanding_writes_in_range( absolute_addr - self.start(), absolute_addr + S::spec_size_of() - self.start() @@ -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.start() + self.len(), self.view(old(pm)).no_outstanding_writes_in_range( absolute_addr - self.start(), absolute_addr + bytes@.len() - self.start() @@ -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.start() + self.len(), self.view(old(pm)).no_outstanding_writes_in_range( absolute_addr - self.start(), absolute_addr + S::spec_size_of() - self.start() From 6ef162863a92bd0c80237a38d94ae6526e0b3e23 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Thu, 16 Oct 2025 14:36:25 -0700 Subject: [PATCH 2/2] Simplify spec for end position --- multilog/multilog/src/pmem/subregion_v.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/multilog/multilog/src/pmem/subregion_v.rs b/multilog/multilog/src/pmem/subregion_v.rs index 4b16c6eda..e23f394f3 100644 --- a/multilog/multilog/src/pmem/subregion_v.rs +++ b/multilog/multilog/src/pmem/subregion_v.rs @@ -586,7 +586,7 @@ impl WriteRestrictedPersistentMemorySubregion requires self.inv(old(wrpm), perm), self.start() <= absolute_addr, - absolute_addr + bytes@.len() <= self.start() + 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() @@ -670,7 +670,7 @@ impl WriteRestrictedPersistentMemorySubregion requires self.inv(old(wrpm), perm), self.start() <= absolute_addr, - absolute_addr + S::spec_size_of() <= self.start() + 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() @@ -1310,7 +1310,7 @@ impl WritablePersistentMemorySubregion requires self.inv(old(pm)), self.start() <= absolute_addr, - absolute_addr + bytes@.len() <= self.start() + 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() @@ -1377,7 +1377,7 @@ impl WritablePersistentMemorySubregion requires self.inv(old(pm)), self.start() <= absolute_addr, - absolute_addr + S::spec_size_of() <= self.start() + 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()