Struct MetaRegionOwners 

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

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. This makes the MetaRegionOwners the one place that tracks every frame, whether or not it is in use. Likewise, every slot has an permission stored in slots.

Safety

The frame_obligations table tracks how many active (in-scope) frames exist for each slot. Each one corresponds to an active drop obligation that must be consumed when its owner leaves scope, either by dropping it with an explicit call to drop or forgetting it with ManuallyDrop. Forgetting a slot with into_raw or ManuallyDrop::new will leak the frame. Forgetting it multiple times without restoring it will likely result in a memory leak, but not double-free. Double-free happens when from_raw is called on a frame that is not forgotten, or that has been dropped with ManuallyDrop::drop instead of into_raw. All functions in the verified code that call from_raw have a precondition that the frame’s index is not a key in slots.

Fields

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

slot_owners: Map<int, MetaSlotOwner>

frame_obligations: Multiset<int>

Outstanding per-instance obligations for both Frame<M> and Segment<M>, as a multiset of slot indices. ManuallyDrop::new(frame, ..) adds one entry at frame.key() (mint paired with the raw_count++ bump); Frame::drop (via consume_obligation) and ManuallyDrop::new redeem one. A Segment<M> records one entry per frame it holds (see crate::specs::mm::frame::segment::tracked_mint_seg_obligations). Multiset semantics — multiple outstanding obligations at the same slot are counted individually.

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 slot_owners_agree_except(self, other: MetaRegionOwners, idx: int) -> bool

{ forall |i: int| i != idx ==> other.slot_owners[i] == self.slot_owners[i] }

other agrees with self on every slot owner except the one at index idx: a single-slot operation leaves all other slots’ owners untouched.

pub open spec fn paddr_range_in_region(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.contains(frame_to_index(paddr))
    }
}

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 open spec fn paddr_range_not_in_region(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.contains(frame_to_index(paddr))
    }
}

pub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)

requires

self.paddr_range_not_mapped(range),

range.start <= paddr,

paddr < range.end,

paddr % PAGE_SIZE == 0,

ensures

self.slot_owner(paddr).paths_in_pt.is_empty(),

Instantiates paddr_range_not_mapped at a specific paddr in the range.

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 ret : &'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 ret : &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)
    == (Self {
        slot_owners: old(self).slot_owners.insert(frame_to_index(paddr), *final(ret)),
        ..*old(self)
    }),

Mutably borrows the MetaSlotOwner, indexed by frame paddr.

pub open spec fn clean_inv(self) -> bool

{
    &&& self.inv()
    &&& self.frame_obligations.len() == 0

}

“Clean” boundary invariant: standard invariant plus an empty per-frame obligation multiset (every minted token has been redeemed via Drop::drop or ManuallyDrop::new; and every Segment has been dropped, draining its per-frame entries).

Functions that should leave no outstanding Frame/Segment obligations (e.g., top-of-call-stack entry points, or any helper that opens fresh resources locally) should require this in their postcondition instead of the plain inv().

pub open spec fn mint_frame_obligation(self, slot_idx: int) -> Self

{
    Self {
        frame_obligations: self.frame_obligations.insert(slot_idx),
        ..self
    }
}

pub open spec fn redeem_frame_obligation(self, slot_idx: int) -> Self

recommends

self.frame_obligations.count(slot_idx) > 0,

{
    Self {
        frame_obligations: self.frame_obligations.remove(slot_idx),
        ..self
    }
}

pub proof fn tracked_mint_frame_obligation( tracked &mut self, slot_idx: int, ) -> tracked obl : DropObligation<int>

ensures

obl.value() == slot_idx,

*final(self) == old(self).mint_frame_obligation(slot_idx),

Pairs the production of a per-Frame DropObligation with a +1 on the frame_obligations[slot_idx] count. Called by Frame’s constructor_spec (i.e. ManuallyDrop::new(frame, ..)).

pub proof fn tracked_redeem_frame_obligation(tracked &mut self, tracked obl: DropObligation<int>)

requires

old(self).frame_obligations.count(obl.value()) > 0,

ensures

*final(self) == old(self).redeem_frame_obligation(obl.value()),

Redeems a per-Frame obligation, decrementing frame_obligations at obl.value(). Called by Frame’s consume_obligation (i.e. by Drop::drop or ManuallyDrop::new).

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()

                }
        }
    }

}

impl InvView for MetaRegionOwners

proof fn view_preserves_inv(self)

impl View for MetaRegionOwners

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

{
    let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s@);
    MetaRegionModel { slots }
}

type V = MetaRegionModel