pub struct SegmentOwner<M: AnyFrameMeta + ?Sized> {
pub range: Range<Paddr>,
pub _marker: PhantomData<M>,
}Fields§
§range: Range<Paddr>The physical-address range of the segment that this owner corresponds to.
Design B (Arc-style): the owner no longer holds the per-frame slot
permissions. Each frame’s simple_pptr::PointsTo<MetaSlot> stays
canonical in regions.slots[idx] and is borrowed on drop/next;
the segment merely contributes one (forgotten) reference per frame.
Per-frame linear-drop: the owner carries no obligation token. The
segment’s “must drop” guarantee is enforced entirely by the per-frame
regions.frame_obligations multiset (one count per segment frame, see
SegmentOwner::relate_regions) combined with the boundary
clean_inv() check — silently dropping a SegmentOwner leaves those
counts outstanding and breaks clean_inv(). Redeem-time tokens are
fabricated on demand via DropObligation::tracked_mint, so no token
needs to travel with the owner.
_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 < seg_nframes(self.range)
==> {
let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
&&& regions.frame_obligations.count(idx) >= 1
&&& regions.slot_owners.contains_key(idx)
&&& regions.slots.contains_key(idx)
&&& 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
&&& regions.slot_owners[idx].paths_in_pt.is_empty()
&&& regions.slot_owners[idx].usage
== crate::specs::mm::frame::meta_owners::PageUsage::Frame
}
}
&&& forall |i: int, j: int| {
0 <= i < j < seg_nframes(self.range)
==> 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 < seg_nframes(self.range),({
let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
&&& regions.frame_obligations.count(idx) >= 1
&&& regions.slot_owners.contains_key(idx)
&&& regions.slots.contains_key(idx)
&&& 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
&&& regions.slot_owners[idx].paths_in_pt.is_empty()
&&& regions.slot_owners[idx].usage
== crate::specs::mm::frame::meta_owners::PageUsage::Frame
}),Manually instantiates the [relate_regions] forall at a specific index.
Use this to extract per-frame facts (slot_owner present, slot perm in
regions.slots, raw_count == 1, ref_count > 0, etc.) without fighting
trigger inference.
Sourcepub proof fn relate_regions_distinct(self, regions: MetaRegionOwners, i: int, j: int)
pub proof fn relate_regions_distinct(self, regions: MetaRegionOwners, i: int, j: int)
self.relate_regions(regions),0 <= i < j < seg_nframes(self.range),frame_to_index((self.range.start + i * PAGE_SIZE) as usize)
!= frame_to_index((self.range.start + j * PAGE_SIZE) as usize),Manually instantiates the [relate_regions] distinctness forall at a
specific index pair: distinct in-range frames map to distinct slot
indices. Reusable lever for from_unused/split/slice proofs.
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
}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.
- the bundled obligation token is keyed to this owner’s
range.