ostd::specs::mm::frame::meta_owners

Struct MetaSlotOwner

pub struct MetaSlotOwner {
    pub storage: PointsTo<MetaSlotStorage>,
    pub ref_count: PermissionU64,
    pub vtable_ptr: PointsTo<usize>,
    pub in_list: PermissionU64,
    pub self_addr: usize,
    pub usage: PageUsage,
    pub path_if_in_pt: Option<TreePath<CONST_NR_ENTRIES>>,
}

Fields§

§storage: PointsTo<MetaSlotStorage>§ref_count: PermissionU64§vtable_ptr: PointsTo<usize>§in_list: PermissionU64§self_addr: usize§usage: PageUsage§path_if_in_pt: Option<TreePath<CONST_NR_ENTRIES>>

Trait Implementations§

Source §

impl Inv for MetaSlotOwner

Source §

open spec fn inv(self) -> bool

{
    &&& self.ref_count.value() == REF_COUNT_UNUSED
        ==> {
            &&& self.vtable_ptr.is_uninit()
            &&& self.in_list.value() == 0

        }
    &&& self.ref_count.value() == REF_COUNT_UNIQUE
        ==> {
            &&& self.vtable_ptr.is_init()

        }
    &&& 0 < self.ref_count.value() < REF_COUNT_MAX
        ==> {
            &&& self.vtable_ptr.is_init()

        }
    &&& REF_COUNT_MAX <= self.ref_count.value() < REF_COUNT_UNUSED ==> { false }
    &&& self.ref_count.value() == 0
        ==> {
            &&& self.vtable_ptr.is_uninit()
            &&& self.in_list.value() == 0

        }
    &&& FRAME_METADATA_RANGE().start <= self.self_addr < FRAME_METADATA_RANGE().end
    &&& self.self_addr % META_SLOT_SIZE() == 0

}

Source §

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

{
    let storage = self.storage.mem_contents();
    let ref_count = self.ref_count.value();
    let vtable_ptr = self.vtable_ptr.mem_contents();
    let in_list = self.in_list.value();
    let self_addr = self.self_addr;
    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,
        self_addr,
        usage,
    }
}