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

Struct MetaSlotOwner

pub struct MetaSlotOwner {
    pub inner_perms: MetadataInnerPerms,
    pub self_addr: usize,
    pub usage: PageUsage,
    pub raw_count: usize,
    pub path_if_in_pt: Option<TreePath<NR_ENTRIES>>,
}

Fields§

§inner_perms: MetadataInnerPerms§self_addr: usize§usage: PageUsage§raw_count: usize§path_if_in_pt: Option<TreePath<NR_ENTRIES>>

Implementations§

Source §

impl MetaSlotOwner

Source

pub proof fn take_inner_perms(tracked &mut self) -> tracked res : MetadataInnerPerms

ensures

res == old(self).inner_perms,

self.self_addr == old(self).self_addr,

self.usage == old(self).usage,

self.raw_count == old(self).raw_count,

self.path_if_in_pt == old(self).path_if_in_pt,

Source

pub proof fn sync_inner(tracked &mut self, inner_perms: &MetadataInnerPerms)

ensures

*self
    == (Self {
        inner_perms: *inner_perms,
        ..*old(self)
    }),

Trait Implementations§

Source §

impl Inv for MetaSlotOwner

Source §

open spec fn inv(self) -> bool

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

        }
    &&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
        ==> {
            &&& self.inner_perms.vtable_ptr.is_init()
            &&& self.inner_perms.storage.is_init()
            &&& self.inner_perms.in_list.value() == 0

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

        }
    &&& REF_COUNT_MAX <= self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE
        ==> { false }
    &&& self.inner_perms.ref_count.value() == 0
        ==> {
            &&& self.inner_perms.vtable_ptr.is_uninit()
            &&& self.inner_perms.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.inner_perms.storage.mem_contents();
    let ref_count = self.inner_perms.ref_count.value();
    let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
    let in_list = self.inner_perms.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,
    }
}