pub struct SegmentOwner<M: AnyFrameMeta + ?Sized> {
pub range: Range<Paddr>,
pub perms: Seq<PointsTo<MetaSlot>>,
pub _marker: PhantomData<M>,
}Expand description
A SegmentOwner<M> holds the permission tokens for all frames in the
Segment<M> for verification purposes.
The range field tracks which physical-address range this owner corresponds
to. It is a ghost-only field used by Self::inv to express the structural
connection between perms and the segment’s frames.
Fields§
§range: Range<Paddr>The physical-address range of the segment that this owner corresponds to.
perms: Seq<PointsTo<MetaSlot>>The slot-pointer permissions for all frames in the segment.
Inner permissions for each slot live exclusively in
regions.slot_owners[idx].inner_perms; this Seq carries only the
simple_pptr::PointsTo<MetaSlot> per frame.
_marker: PhantomData<M>Implementations§
Source§impl<M: AnyFrameMeta + ?Sized> SegmentOwner<M>
impl<M: AnyFrameMeta + ?Sized> SegmentOwner<M>
Sourcepub open spec fn relate_regions(self, regions: MetaRegionOwners) -> bool
pub open spec fn relate_regions(self, regions: MetaRegionOwners) -> bool
{
&&& forall |i: int| {
0 <= i < self.perms.len() as int
==> {
let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
&&& regions.slot_owners.contains_key(idx)
&&& !regions.slots.contains_key(idx)
&&& regions.slot_owners[idx].raw_count == 1
&&& regions.slot_owners[idx].self_addr == meta_addr(idx)
&&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
&&& regions.slot_owners[idx].inner_perms.ref_count.value()
<= crate::mm::frame::meta::REF_COUNT_MAX
&&& self.perms[i].value().wf(regions.slot_owners[idx])
}
}
&&& forall |i: int, j: int| {
0 <= i < j < self.perms.len() as int
==> frame_to_index((self.range.start + i * PAGE_SIZE) as usize)
!= frame_to_index((self.range.start + j * PAGE_SIZE) as usize)
}
}The cross-object relation between a SegmentOwner and the global
MetaRegionOwners.
For every frame i in the segment, this asserts:
- the slot owner is present in
regionsand the perm matches it, - the slot’s
self_addris consistent with its index, - the slot has a live, non-
UNUSEDreference count, raw_count == 1(the segment holds one forgotten reference per frame),- the slot’s perm is not in
regions.slots(it lives inself.perms), - distinct frames in the segment map to distinct slot indices.
This is an invariant preserved by every operation that transforms a
SegmentOwner together with MetaRegionOwners — analogous to
crate::specs::mm::frame::unique::UniqueFrameOwner::global_inv but
spanning all frames in a segment.
Sourcepub proof fn relate_regions_at(self, regions: MetaRegionOwners, i: int)
pub proof fn relate_regions_at(self, regions: MetaRegionOwners, i: int)
self.relate_regions(regions),0 <= i < self.perms.len() as int,({
let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
&&& regions.slot_owners.contains_key(idx)
&&& !regions.slots.contains_key(idx)
&&& regions.slot_owners[idx].raw_count == 1
&&& regions.slot_owners[idx].self_addr == meta_addr(idx)
&&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
&&& regions.slot_owners[idx].inner_perms.ref_count.value()
<= crate::mm::frame::meta::REF_COUNT_MAX
&&& self.perms[i].value().wf(regions.slot_owners[idx])
}),Manually instantiates the [relate_regions] forall at a specific index.
Use this to extract per-frame facts (slot_owner present, raw_count == 1,
ref_count > 0, perm.value().wf, etc.) without fighting trigger inference.
Trait Implementations§
Source§impl<M: AnyFrameMeta + ?Sized> Inv for SegmentOwner<M>
impl<M: AnyFrameMeta + ?Sized> Inv for SegmentOwner<M>
Source§open spec fn inv(self) -> bool
open spec fn inv(self) -> bool
{
&&& self.range.start % PAGE_SIZE == 0
&&& self.range.end % PAGE_SIZE == 0
&&& self.range.start <= self.range.end <= MAX_PADDR
&&& self.perms.len() * PAGE_SIZE == self.range.end - self.range.start
&&& forall |i: int| {
0 <= i < self.perms.len() as int
==> {
&&& self.perms[i].addr()
== meta_addr(
frame_to_index((self.range.start + i * PAGE_SIZE) as usize),
)
&&& self.perms[i].addr() % META_SLOT_SIZE == 0
&&& self.perms[i].addr() < FRAME_METADATA_RANGE.end
&&& self.perms[i].is_init()
}
}
}The invariant of a SegmentOwner:
- the tracked
rangeis page-aligned and within bounds; - the number of permissions matches the number of frames in the range;
- each permission’s address corresponds to the meta slot of its frame
(so consecutive permissions are spaced by
META_SLOT_SIZE); - each permission is initialized and individually well-formed.