Struct UniqueFrameOwner 

pub struct UniqueFrameOwner<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
    pub meta_own: M::Owner,
    pub repr_perm: Option<M::ReprPerm>,
    pub slot_index: int,
}

Fields

meta_own: M::Owner

repr_perm: Option<M::ReprPerm>

slot_index: int

Implementations

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrameOwner<Link<M>>

pub open spec fn frame_link_inv(&self, regions: MetaRegionOwners) -> bool

{
    &&& self.meta_value(regions).prev is None
    &&& self.meta_value(regions).next is None
    &&& self.meta_own.paddr == regions.slots[self.slot_index].addr()
    &&& regions.slot_owners[self.slot_index].in_list_perm.value() == 0

}

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M>

pub open spec fn meta_wf(self, regions: MetaRegionOwners) -> bool

{
    typed_meta_wf::<
        M,
    >(
        *regions.slots[self.slot_index],
        regions.slot_owners[self.slot_index].metadata_perm,
        self.repr_perm->0,
    )
}

pub open spec fn meta_value(self, regions: MetaRegionOwners) -> M

{
    typed_meta_value::<
        M,
    >(regions.slot_owners[self.slot_index].metadata_perm, self.repr_perm->0)
}

pub open spec fn perm_inv(self, perm: PointsTo<MetaSlot>) -> bool

{
    &&& perm.is_init()
    &&& perm.addr() == index_to_meta(self.slot_index)

}

pub open spec fn global_inv(self, regions: MetaRegionOwners) -> bool

{
    &&& regions.contains(self.slot_index)
    &&& self.meta_wf(regions)
    &&& regions.slots[self.slot_index].addr() == index_to_meta(self.slot_index)
    &&& self.meta_value(regions).wf(self.meta_own)
    &&& regions.slot_owners[self.slot_index].slot_vaddr == index_to_meta(self.slot_index)
    &&& regions.slot_owners[self.slot_index].ref_count() == REF_COUNT_UNIQUE
    &&& regions.slot_owners[self.slot_index].usage is Frame
    &&& regions.frame_obligations.count(self.slot_index) > 0

}

Borrow-model global invariant: the frame’s permission is parked in regions.slots[slot_index] (NOT owned by the frame), and the concrete storage and representation permissions decode to metadata matching meta_own. A UniqueFrame is the sole live reference to its slot, so the slot sits at REF_COUNT_UNIQUE — the unique-frame analog of the segment’s 0 < ref_count <= REF_COUNT_MAX regime in Segment::relate_regions. Being live, it also owes a pending-Drop obligation in frame_obligations (minted at from_unused/from_raw, consumed by drop/into_raw).

pub open spec fn from_unused_owner( meta_own: M::Owner, repr_perm: M::ReprPerm, slot_index: int, ) -> Self

{
    Self {
        meta_own,
        repr_perm: Some(repr_perm),
        slot_index,
    }
}

pub proof fn tracked_from_unused_owner( tracked meta_own: M::Owner, tracked repr_perm: M::ReprPerm, slot_index: int, ) -> tracked res : Self

returns

Self::from_unused_owner(meta_own, repr_perm, slot_index),

pub proof fn tracked_borrow_repr_perm(tracked &self) -> tracked res : &M::ReprPerm

requires

self.repr_perm is Some,

ensures

*res == self.repr_perm->0,

pub proof fn tracked_borrow_mut_repr_perm(tracked &mut self) -> tracked res : &mut M::ReprPerm

requires

old(self).inv(),

ensures

*res == old(self).repr_perm->0,

final(self).meta_own == old(self).meta_own,

final(self).slot_index == old(self).slot_index,

final(self).repr_perm is Some,

final(self).repr_perm->0 == *final(res),

final(self).inv(),

Trait Implementations

impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M>

open spec fn inv(self) -> bool

{
    &&& 0 <= self.slot_index < MAX_NR_PAGES
    &&& self.slot_index < max_meta_slots()
    &&& self.repr_perm is Some

}

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> InvView for UniqueFrameOwner<M>

proof fn view_preserves_inv(self)

impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> View for UniqueFrameOwner<M>

open spec fn view(&self) -> Self::V

{
    UniqueFrameModel {
        meta: self.meta_own@,
    }
}

type V = UniqueFrameModel<M>