Struct MetaRegionOwners 

pub struct MetaRegionOwners {
    pub slots: Map<int, &'static PointsTo<MetaSlot>>,
    pub slot_owners: Map<int, MetaSlotOwner>,
}

Represents the ownership of the meta-frame memory region.

Verification Design

Slot owners and permissions

Every metadata slot has its owner (MetaSlotOwner) tracked by the slot_owners map at all times. Likewise, every slot has an permission stored in slots.

Fields

slots: Map<int, &'static PointsTo<MetaSlot>>

slot_owners: Map<int, MetaSlotOwner>

Implementations

impl MetaRegionOwners

pub open spec fn contains(self, index: int) -> bool

{
    &&& self.slot_owners.contains_key(index)
    &&& self.slots.contains_key(index)

}

Returns whether the slot permission and its corresponding owner are both present.

pub open spec fn insert_slot_owner(self, paddr: Paddr, owner: MetaSlotOwner) -> Self

{
    let index = frame_to_index(paddr);
    Self {
        slot_owners: self.slot_owners.insert(index, owner),
        ..self
    }
}

pub open spec fn ref_count(self, i: int) -> res : u64

recommends

0 <= i < max_meta_slots(),

{ self.slot_owners[i].ref_count() }

pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool

recommends

range.start < range.end < MAX_PADDR,

{
    forall |paddr: Paddr| {
        (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
            ==> self.slot_owner(paddr).paths_in_pt.is_empty()
    }
}

pub proof fn lemma_contains_valid_frame_paddr(self, paddr: usize)

requires

valid_frame_paddr(paddr),

self.inv(),

ensures

self.contains(frame_to_index(paddr)),

pub open spec fn slot_owner(self, paddr: Paddr) -> MetaSlotOwner

{ self.slot_owners[frame_to_index(paddr)] }

Rertuns the MetaSlotOwner, indexed by frame paddr.

pub proof fn tracked_borrow_slot(tracked &self, paddr: Paddr) -> tracked &'static PointsTo<MetaSlot>

requires

valid_frame_paddr(paddr),

self.inv(),

returns

self.slots[frame_to_index(paddr)],

Borrows the metadata slot permission, indexed by frame paddr.

pub proof fn tracked_borrow_slot_owner(tracked &self, paddr: Paddr) -> tracked &MetaSlotOwner

requires

valid_frame_paddr(paddr),

self.inv(),

returns

self.slot_owner(paddr),

Borrows the MetaSlotOwner, indexed by frame paddr.

pub proof fn tracked_borrow_mut_slot_owner( tracked &mut self, paddr: Paddr, ) -> tracked ret : &mut MetaSlotOwner

requires

valid_frame_paddr(paddr),

self.inv(),

ensures

*ret == old(self).slot_owner(paddr),

*final(self) == old(self).insert_slot_owner(paddr, *final(ret)),

Mutably borrows the MetaSlotOwner, indexed by frame paddr.

pub open spec fn inc_frame_reference_region_spec(self, paddr: Paddr, post: Self) -> bool

{
    let idx = frame_to_index(paddr);
    let pre_owner = self.slot_owners[idx];
    let post_owner = post.slot_owners[idx];
    {
        &&& post.ref_count(idx) == self.ref_count(idx) + 1
        &&& post_owner.ref_count_perm.id() == pre_owner.ref_count_perm.id()
        &&& post_owner.metadata_perm.id() == pre_owner.metadata_perm.id()
        &&& post_owner.metadata_perm.frac() + 1 == pre_owner.metadata_perm.frac()
        &&& post_owner.metadata_perm@ == pre_owner.metadata_perm@
        &&& post_owner.in_list_perm == pre_owner.in_list_perm
        &&& post_owner.slot_vaddr == pre_owner.slot_vaddr
        &&& post_owner.usage == pre_owner.usage
        &&& post_owner.paths_in_pt == pre_owner.paths_in_pt
        &&& post =~= self.insert_slot_owner(paddr, post_owner)

    }
}

The metadata region transition of claiming a currently shared slot.

Trait Implementations

impl Inv for MetaRegionOwners

open spec fn inv(self) -> bool

{
    &&& {
        forall |i: int| {
            0 <= i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
        }
    }
    &&& {
        forall |i: int| {
            #[trigger] self.slot_owners.contains_key(i) ==> self.slots.contains_key(i)
        }
    }
    &&& {
        forall |i: int| {
            #[trigger] self.slots.contains_key(i) ==> 0 <= i < max_meta_slots()
        }
    }
    &&& {
        forall |i: int| {
            #[trigger] self.slots.contains_key(i)
                ==> {
                    &&& self.slot_owners[i].inv()
                    &&& self.slots[i].is_init()
                    &&& self.slots[i].addr() == index_to_meta(i)
                    &&& self.slots[i].value().wf(self.slot_owners[i])
                    &&& self.slot_owners[i].slot_vaddr == self.slots[i].addr()

                }
        }
    }

}