Struct MetaSlotOwner 

pub struct MetaSlotOwner {
    pub metadata_perm: MetadataPerms,
    pub ref_count_perm: PermissionU64,
    pub in_list_perm: PermissionU64,
    pub slot_vaddr: Vaddr,
    pub usage: PageUsage,
    pub paths_in_pt: Set<TreePath<NR_ENTRIES>>,
}

Permissions that remain under the authority of MetaRegionOwners.

ref_count and in_list exist for the complete lifetime of the corresponding MetaSlot (i.e., 'static).

Fields

metadata_perm: MetadataPerms

ref_count_perm: PermissionU64

in_list_perm: PermissionU64

slot_vaddr: Vaddr

usage: PageUsage

paths_in_pt: Set<TreePath<NR_ENTRIES>>

The set of tree paths at which this slot is referenced. For PT-node slots this is a singleton. For data-frame slots this tracks every location the frame is currently mapped — allowing a single frame to be mapped at multiple addresses.

Implementations

impl MetaSlotOwner

pub open spec fn same_permissions(self, other: Self) -> bool

{
    &&& self.metadata_perm == other.metadata_perm
    &&& self.ref_count_perm == other.ref_count_perm
    &&& self.in_list_perm == other.in_list_perm

}

pub open spec fn ref_count(self) -> u64

{ self.ref_count_perm.value() }

pub open spec fn storage_perm(self) -> PointsTo<MetaSlotStorage>

{ self.metadata_perm.storage_perm }

pub open spec fn vtable_ptr_perm(self) -> PointsTo<usize>

{ self.metadata_perm.vtable_ptr_perm }

pub proof fn tracked_borrow_mut_metadata_perms(tracked &mut self) -> tracked res : &mut MetadataPerms

ensures

*res == old(self).metadata_perm,

*final(self)
    == (Self {
        metadata_perm: *final(res),
        ..*old(self)
    }),

Trait Implementations

impl Inv for MetaSlotOwner

open spec fn inv(self) -> bool

{
    &&& self.ref_count() == REF_COUNT_UNUSED
        ==> {
            &&& self.storage_perm().is_uninit()
            &&& self.vtable_ptr_perm().is_uninit()
            &&& self.in_list_perm.value() == 0
            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())

        }
    &&& self.ref_count() == REF_COUNT_UNIQUE
        ==> {
            &&& self.vtable_ptr_perm().is_init()
            &&& self.storage_perm().is_init()
            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())

        }
    &&& 0 < self.ref_count() <= REF_COUNT_MAX
        ==> {
            &&& self.vtable_ptr_perm().is_init()
            &&& self.storage_perm().is_init()
            &&& self.in_list_perm.value() == 0

        }
    &&& REF_COUNT_MAX < self.ref_count() < REF_COUNT_UNIQUE ==> { false }
    &&& self.ref_count() == 0
        ==> {
            &&& self.in_list_perm.value() == 0

        }
    &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
    &&& self.slot_vaddr % META_SLOT_SIZE == 0

}

impl InvView for MetaSlotOwner

proof fn view_preserves_inv(self)

impl View for MetaSlotOwner

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

{
    let storage = self.storage_perm().mem_contents();
    let ref_count = self.ref_count();
    let vtable_ptr = self.vtable_ptr_perm().mem_contents();
    let in_list = self.in_list_perm.value();
    let slot_vaddr = self.slot_vaddr;
    let usage = self.usage;
    let status = match ref_count {
        REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
        REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
        0 => MetaSlotStatus::UNDER_CONSTRUCTION,
        _ if ref_count <= REF_COUNT_MAX => MetaSlotStatus::SHARED,
        _ => MetaSlotStatus::OVERFLOW,
    };
    MetaSlotModel {
        status,
        storage,
        ref_count,
        vtable_ptr,
        in_list,
        slot_vaddr,
        usage,
    }
}

type V = MetaSlotModel