Struct Frame 

pub struct Frame<M: ?Sized> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
    pub tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>,
    pub tracked_metadata_perm: Tracked<Option<FracMetadataPerm>>,
}

A smart pointer to a frame.

A frame is a contiguous range of bytes in physical memory. The Frame type is a smart pointer to a frame that is reference-counted.

Frames are associated with metadata. The type of the metadata M is determines the kind of the frame. If M implements AnyUFrameMeta, the frame is a untyped frame. Otherwise, it is a typed frame.

Fields

ptr: PPtr<MetaSlot>

_marker: PhantomData<M>

tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>

The permission to access the MetaSlot fields.

tracked_metadata_perm: Tracked<Option<FracMetadataPerm>>

One fractional permission for the currently installed metadata.

Implementations

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M>

pub exec fn from_unique(unique: UniqueFrame<M>) -> res : Self

with

Tracked(owner): Tracked<UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,

requires

unique.inv(),

owner.inv(),

old(regions).inv(),

unique.wf_with_region(owner, *old(regions)),

old(regions).slot_owners[owner.slot_index].in_list_perm.value() == 0,

ensures

res.inv(),

final(regions).inv(),

res.wf_with_region(*final(regions)),

final(regions).slots == old(regions).slots,

final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M>

pub exec fn from_unused(paddr: Paddr, metadata: M) -> r : Result<Self, GetFrameError>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(repr_perm): Tracked<&mut M::ReprPerm>,

requires

old(regions).inv(),

ensures

final(regions).inv(),

r matches Ok(
    res,
) ==> {
    &&& MetaSlot::get_from_unused_region_spec(
        paddr,
        false,
        *old(regions),
        *final(regions),
    )
    &&& res.inv()
    &&& res.start_paddr_spec() == paddr
    &&& res.wf_with_region(*final(regions))

},

r is Err ==> *final(regions) == *old(regions),

Gets a Frame with a specific usage from a raw, unused page.

The caller should provide the initial metadata of the page.

If the provided frame is not truly unused at the moment, it will return an error. If wanting to acquire a frame that is already in use, use Frame::from_in_use instead.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.

Postconditions

• Safety Invariant: Metaslot region invariants hold after the call.
• Correctness: If successful, the function returns a pointer to the metadata slot and a permission to the slot.
• Correctness: If successful, the slot is initialized with the given metadata.
• Correctness: If paddr does not have a corresponding metadata slot, the function returns an error.
• Drop Bookkeeping: If successful, the function returns a live frame, which is tracked correctly as needing to be dropped.

Safety

• This function returns an error if paddr does not correspond to a valid slot or the slot is in use.

pub exec fn meta<'a>(&'a self) -> ret : &'a M

with

Tracked(metadata_perm): Tracked<Option<&'a MetadataPerm>>,
Tracked(repr_perm): Tracked<&'a M::ReprPerm>,

requires

self.ptr_inv(),

{
    self.inv() && metadata_perm is None
        && typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), *repr_perm)
        || metadata_perm is Some && self.external_meta_wf(*metadata_perm->0, *repr_perm)
},

ensures

{
    let metadata_perm = if metadata_perm is Some {
        *metadata_perm->0
    } else {
        self.metadata_perm()
    };
    ret == typed_meta_value::<M>(metadata_perm, *repr_perm)
},

Gets the metadata of this page.

Verified Properties

Preconditions

• The caller must have a valid permission for the frame.

Postconditions

• The function returns the borrowed metadata of the frame.

Safety

• By requiring the caller to provide a typed permission, we ensure that the metadata is of type M. While a non-verified caller cannot be trusted to obey this interface, all functions that return a Frame<M> also return an appropriate permission.

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Frame<M>

pub exec fn from_in_use(paddr: Paddr) -> res : Result<Self, GetFrameError>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,

requires

old(regions).inv(),

valid_frame_paddr(paddr)
    ==> (old(regions).ref_count(frame_to_index(paddr)) >= REF_COUNT_MAX ==> may_panic()),

ensures

final(regions).inv(),

res matches Ok(
    res,
) ==> {
    &&& old(regions).inc_frame_reference_region_spec(paddr, *final(regions))
    &&& res.inv()
    &&& res.start_paddr_spec() == paddr
    &&& res.wf_with_region(*final(regions))

},

res is Err ==> *old(regions) == *final(regions),

Gets a dynamically typed Frame from a raw, in-use page.

If the provided frame is not in use at the moment, it will return an error.

The returned frame will have an extra reference count to the frame.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.
• Termination: The function may panic if paddr is a valid slot and its reference count is saturated.

Postconditions

• Safety Invariant: Metaslot region invariants hold after the call.
• Correctness: If successful, the function returns the frame at paddr.
• Correctness: If successful, the frame has an extra reference count.
• Correctness: If paddr does not have a valid metadata slot, the function returns an error.
• Safety: Frames other than the one at paddr are not affected by the call.

Safety

• If paddr is a valid frame address, it is safe to take a reference to the frame.
• If paddr is not a valid frame address, the function will return an error.

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M>

pub exec fn start_paddr(&self) -> Paddr

requires

self.ptr_inv(),

returns

self.start_paddr_spec(),

Gets the physical address of the start of the frame.

Verified Properties

Preconditions

• Bookkeeping: takes the permission for the frame’s metadata slot.

Postconditions

• Correctness: returns the physical address of the frame.

Safety

The caller cannot obtain a frame that doesn’t have a valid permission, and this function does not mutate any state, so it is always sound to call.

pub const exec fn map_level(&self) -> PagingLevel

returns

1u8,

Gets the map level of this page.

This is the level of the page table entry that maps the frame, which determines the size of the frame.

Currently, the level is always 1, which means the frame is a regular page frame.

pub const exec fn size(&self) -> usize

returns

PAGE_SIZE,

Gets the size of this page in bytes.

pub exec fn reference_count(&self) -> u64

with

Tracked(slot_own): Tracked<&MetaSlotOwner>,

requires

self.ptr_inv(),

self.tracked_slot_perm@.value().wf(*slot_own),

returns

slot_own.ref_count(),

Gets the reference count of the frame.

It returns the number of all references to the frame, including all the existing frame handles (Frame, Frame<dyn AnyFrameMeta>), and all the mappings in the page table that points to the frame.

Safety

The function is safe to call, but using it requires extra care. The reference count can be changed by other threads at any time including potentially between calling this method and acting on the result.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.
• Bookkeeping: The caller must have a valid and well-typed permission for the frame.

Postconditions

• Correctness: The function returns the reference count of the frame.

pub exec fn borrow<'a>(&self) -> res : FrameRef<'a, M>

requires

self.inv(),

ensures

res.inner@.ptr.addr() == self.ptr.addr(),

Borrows a reference from the given frame.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.

Postconditions

• Safety Invariant: Metaslot region invariants hold after the call.
• Correctness: The function returns a reference to the frame.
• Correctness: The system context is unchanged.

impl<M: ?Sized> Frame<M>

pub exec fn slot<'a>(&'a self) -> &'a MetaSlot

requires

self.ptr_inv(),

returns

self.tracked_slot_perm@.value(),

Gets the metadata slot of the frame.

Verified Properties

Preconditions

• Safety: The caller must have a valid permission for the frame.

Postconditions

• Correctness: The function returns a reference to the metadata slot of the frame.

Safety

• There is no way to mutably borrow the metadata slot, so taking an immutable reference is safe. (The fields of the slot can be mutably borrowed, but not the slot itself.)

impl<M: ?Sized> Frame<M>

pub exec fn drop(self, Tracked(regions): Tracked<&mut MetaRegionOwners>)

requires

self.drop_requires(*old(regions)),

ensures

self.drop_ensures(*old(regions), *final(regions)),

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + 'static> Frame<M>

pub exec fn into_dyn(self) -> Frame<dyn AnyFrameMeta>

Erases the static metadata type, yielding a Frame<dyn AnyFrameMeta>.

Inherent method rather than From/Into to avoid trait-inference ambiguity at call sites that previously relied on the blanket From<T> for T (e.g. frame.into() for Frame<UFrame>).

Axiomatized (external_body) because the body is transmute, which Verus has no built-in spec for.

impl<C: PageTableConfig> Frame<PageTablePageMeta<C>>

pub exec fn alloc<'rcu>(level: PagingLevel) -> res : Self

with

Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&Guards>,
Ghost(idx): Ghost<usize>,
->
owner: Tracked<OwnerSubtree<C>>,

requires

1 <= level < NR_LEVELS,

idx < NR_ENTRIES,

old(regions).inv(),

old(parent_owner).inv(),

ensures

final(regions).inv(),

final(parent_owner).inv(),

allocated_empty_node_owner(owner@, level),

allocated_empty_node_grandchildren_none(owner@),

res.ptr.addr() == owner@.value().node().slot_vaddr(),

res.inv(),

res.wf_with_region(*final(regions)),

guards.unlocked(owner@.value().node().slot_vaddr()),

MetaSlot::get_node_from_unused_spec(
    meta_to_frame(owner@.value().node().slot_vaddr()),
    *old(regions),
    *final(regions),
),

MetaSlot::slot_perm_reparked_spec(
    meta_to_frame(owner@.value().node().slot_vaddr()),
    *old(regions),
    *final(regions),
),

old(regions).contains(meta_to_index(owner@.value().node().slot_vaddr())),

!crate::specs::mm::frame::meta_owners::is_mmio_paddr(
    meta_to_frame(owner@.value().node().slot_vaddr()),
),

owner@.value().metaregion_sound(*final(regions)),

forall |i: int| {
    #[trigger] old(regions).ref_count(i) != REF_COUNT_UNUSED
        ==> i != meta_to_index(owner@.value().node().slot_vaddr())
},

owner@
    .value()
    .match_pte(
        C::E::new_pt_spec(meta_to_frame(owner@.value().node().slot_vaddr())),
        level as PagingLevel,
    ),

final(parent_owner).meta_own == old(parent_owner).meta_own,

final(parent_owner).frame_permission == old(parent_owner).frame_permission,

final(parent_owner).slot_index == old(parent_owner).slot_index,

final(parent_owner).level() == old(parent_owner).level(),

final(parent_owner).tree_level == old(parent_owner).tree_level,

final(parent_owner).children_perm.addr() == old(parent_owner).children_perm.addr(),

final(parent_owner).children_perm.value()
    == old(parent_owner)
        .children_perm
        .value()
        .update(
            idx as int,
            C::E::new_pt_spec(meta_to_frame(owner@.value().node().slot_vaddr())),
        ),

final(regions).contains(owner@.value().node().slot_index),

owner@.value().node().metaregion_sound_node(*final(regions)),

Allocates a new empty page table node.

impl<M: ?Sized> Frame<M>

pub open spec fn frac_metadata_perm(self) -> FracMetadataPerm

{ self.tracked_metadata_perm@->0 }

Accessor for the fractional metadata permission tracked by this Frame handle.

pub open spec fn metadata_perm(self) -> MetadataPerm

{ self.frac_metadata_perm().resource() }

Accessor for the full metadata permission tracked by the fractional permission.

pub open spec fn slot_perm(self) -> PointsTo<MetaSlot>

{ *self.tracked_slot_perm@ }

Accessor for the MetaSlot permission tracked by this Frame handle.

pub open spec fn ref_count_id(self) -> int

{ self.slot_perm().value().ref_count.id() }

Accessor for the id of the ref_count field.

pub open spec fn storage_id(self) -> CellId

{ self.slot_perm().value().storage.id() }

Accessor for the id of the storage field.

pub open spec fn ptr_inv(self) -> bool

{
    &&& valid_slot_vaddr(self.ptr.addr())
    &&& self.slot_perm().pptr() == self.ptr
    &&& self.slot_perm().is_init()

}

Address-related invariant shared by owning frames and non-owning ManuallyDrop<Frame> values embedded in FrameRef.

pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool

{
    &&& regions.slot_owner(paddr).slot_vaddr == frame_to_meta(paddr)
    &&& valid_frame_paddr(paddr)
    &&& regions.inv()
    &&& 0 < regions.slot_owner(paddr).ref_count() <= REF_COUNT_MAX

}

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M>

pub open spec fn external_meta_wf( self, metadata_perm: MetadataPerm, repr_perm: M::ReprPerm, ) -> bool

{
    &&& self.ptr_inv()
    &&& self.tracked_metadata_perm@ is None
    &&& typed_meta_wf::<M>(self.slot_perm(), metadata_perm, repr_perm)

}

Relates an externally stored metadata permission to this frame’s slot permission.

impl<M: ?Sized> Frame<M>

pub open spec fn index(self) -> int

{ frame_to_index(self.start_paddr_spec()) }

pub open spec fn start_paddr_spec(self) -> Paddr

{ meta_to_frame(self.ptr.addr()) }

pub open spec fn drop_requires(self, region: MetaRegionOwners) -> bool

{
    let idx = self.index();
    let slot_own = region.slot_owners[idx];
    &&& self.inv()
    &&& region.inv()
    &&& self.wf_with_region(region)
    &&& 0 < slot_own.ref_count() <= REF_COUNT_MAX
    &&& slot_own.ref_count() == 1
        ==> {
            &&& slot_own.paths_in_pt.is_empty()

        }

}

pub open spec fn drop_ensures(self, old: MetaRegionOwners, new: MetaRegionOwners) -> bool

{
    let paddr = self.start_paddr_spec();
    let old_owner = old.slot_owner(paddr);
    let new_owner = new.slot_owner(paddr);
    &&& new.inv()
    &&& new =~= old.insert_slot_owner(paddr, new_owner)
    &&& new_owner.slot_vaddr == old_owner.slot_vaddr
    &&& new_owner.usage == old_owner.usage
    &&& new_owner.paths_in_pt == old_owner.paths_in_pt
    &&& new_owner.metadata_perm.id() == old_owner.metadata_perm.id()
    &&& old_owner.ref_count() == 1 ==> { new_owner.ref_count() == REF_COUNT_UNUSED }
    &&& old_owner.ref_count() > 1
        ==> new_owner.ref_count() == (old_owner.ref_count() - 1) as u64

}

impl<M: ?Sized> Frame<M>

pub open spec fn wf_with_region(self, s: MetaRegionOwners) -> bool

{
    let idx = self.index();
    let slot_own = s.slot_owners[idx];
    &&& s.contains(idx)
    &&& self.tracked_slot_perm@ == s.slots[idx]
    &&& self.frac_metadata_perm().id() == slot_own.metadata_perm.id()

}

Relates this Frame handle to its metadata in the metadata region.

impl<M: ?Sized> Frame<M>

pub open spec fn from_raw_spec( paddr: Paddr, slot_perm: &'static PointsTo<MetaSlot>, metadata_perm: Option<FracMetadataPerm>, ) -> Self

{
    Frame::<M> {
        ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
        _marker: PhantomData,
        #[cfg(verus_keep_ghost_body)]
        tracked_slot_perm: Tracked(slot_perm),
        #[cfg(verus_keep_ghost_body)]
        tracked_metadata_perm: Tracked(metadata_perm),
    }
}

impl<C: PageTableConfig> Frame<PageTablePageMeta<C>>

pub open spec fn invariants(self, owner: NodeOwner<C>) -> bool

{
    &&& owner.inv()
    &&& self.wf(owner)

}

Trait Implementations

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Eq for Frame<M>

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> From<Frame<M>> for Segment<M>

exec fn from(frame: Frame<M>) -> Self

impl<M: AnyUFrameMeta> From<Frame<M>> for UFrame

exec fn from(frame: Frame<M>) -> Self

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> From<UniqueFrame<M>> for Frame<M>

exec fn from(unique: UniqueFrame<M>) -> Self

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> FromSpecImpl<Frame<M>> for Segment<M>

open spec fn obeys_from_spec() -> bool

{ true }

closed spec fn from_spec(frame: Frame<M>) -> Self

impl<M: ?Sized> Inv for Frame<M>

open spec fn inv(self) -> bool

{
    &&& self.ptr_inv()
    &&& self.tracked_metadata_perm@ is Some
    &&& self.frac_metadata_perm().frac() == 1
    &&& MetaSlot::perms_related(self.slot_perm(), self.metadata_perm())

}

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> PartialEq for Frame<M>

exec fn eq(&self, other: &Self) -> bool

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> PartialEqSpecImpl for Frame<M>

open spec fn obeys_eq_spec() -> bool

{ true }

open spec fn eq_spec(&self, other: &Self) -> bool

{ self.start_paddr_spec() == other.start_paddr_spec() }

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> RCClone for Frame<M>

open spec fn clone_requires(self, regions: MetaRegionOwners) -> bool

{
    let paddr = self.start_paddr_spec();
    let ref_count = regions.slot_owner(paddr).ref_count();
    &&& self.inv()
    &&& regions.inv()
    &&& self.wf_with_region(regions)
    &&& ref_count > 0
    &&& ref_count != REF_COUNT_UNUSED
    &&& ref_count >= REF_COUNT_MAX ==> may_panic()

}

open spec fn clone_ensures( self, pre: MetaRegionOwners, post: MetaRegionOwners, res: Self, ) -> bool

{
    let idx = self.index();
    &&& pre.inc_frame_reference_region_spec(self.start_paddr_spec(), post)
    &&& post.inv()
    &&& res.tracked_metadata_perm@ is Some
    &&& res.tracked_metadata_perm@->0.frac() == 1
    &&& res.tracked_metadata_perm@->0.id() == post.slot_owners[idx].metadata_perm.id()
    &&& res.tracked_slot_perm@ == post.slots[idx]
    &&& res.ptr == self.ptr

}

exec fn clone(&self, Tracked(regions): Tracked<&mut MetaRegionOwners>) -> Self

impl<M: AnyFrameMeta + ?Sized> Send for Frame<M>

impl<M: AnyFrameMeta + ?Sized> Sync for Frame<M>

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TryFrom<Frame<M>> for UniqueFrame<M>

exec fn try_from(frame: Frame<M>) -> Result<Self, Self::Error>

Tries to get a unique frame from a shared frame.

If the reference count is not 1, the frame is returned back.

type Error = Frame<M>

The type returned in the event of a conversion error.