ostd::mm::frame

Struct Frame

#[repr(transparent)]
pub struct Frame<M: ?Sized> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
}

Expand description

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.

§Verification Design

Fields§

§ptr: PPtr<MetaSlot>§_marker: PhantomData<M>

Implementations§

Source §

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

Source

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

with

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

requires

unique.wf(owner),

owner.inv(),

old(regions).inv(),

ensures

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

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

Converts a unique frame into a shared one by setting ref_count = 1. Inherent sibling of From<UniqueFrame<M>> for Frame<M>: freed from the trait-signature straitjacket, this version can thread the tracked MetaRegionOwners via verus_spec.

Source §

impl<M: ?Sized> Frame<M>

Source

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

{
    let idx = self.index();
    let slot_own = s.slot_owners[idx];
    &&& self.inv()
    &&& s.inv()
    &&& s.slots.contains_key(idx)
    &&& s.slots[idx].pptr() == self.ptr
    &&& s.slot_owners.contains_key(idx)
    &&& slot_own.inner_perms.ref_count.value() != REF_COUNT_UNUSED
    &&& slot_own.inner_perms.ref_count.value() != REF_COUNT_UNIQUE
    &&& slot_own.inner_perms.ref_count.value() > 0
    &&& slot_own.inner_perms.ref_count.value() <= REF_COUNT_MAX

}

Cross-object well-formedness predicate: this Frame handle and the supplied MetaRegionOwners state are mutually consistent. Packages the static “Frame ⟷ state” conjuncts (slot/pointer identity, slot in-use range) so that consumer specs ([drop_requires], [clone_requires]) read uniformly.

Name: wf_state (not just wf) to avoid clashing with the OwnerOf::wf(self, Self::Owner) impl that [PageTableNode<C> = Frame<PageTablePageMeta<C>>] inherits — the two predicates take different argument types and serve different purposes (per-handle vs. per-owner well-formedness).

The rc range (> 0 ∧ ≠ UNUSED ∧ ≠ UNIQUE ∧ ≤ MAX) captures the fact that holding a Frame<M> is itself evidence that the slot is in the SHARED state — no UNUSED, no UNIQUE (which is reserved for UniqueFrame). Combined with MetaSlotOwner::inv’s SHARED branch (post Item 1), wf_state implies storage.is_init, in_list == 0, and vtable_ptr.is_init at the slot, so consumers don’t have to repeat those.

Not preserved by drop for self: dropping self releases the reference; for other handles to the same slot, wf_state is preserved by drop’s >1 branch (post rc ∈ [1, MAX-1]) and vacuous in the ==1 branch (no other handles to break).

Source §

impl<'a, M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M>

Source

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

with

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

requires

old(regions).inv(),

ensures

final(regions).inv(),

r matches Ok(res) ==> res.ptr.addr() == frame_to_meta(paddr),

r is Ok ==> MetaSlot::get_from_unused_spec(paddr, false, *old(regions), *final(regions)),

r is Ok ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),

!has_safe_slot(paddr) ==> r is Err,

r is Ok
    ==> MetaSlot::live_frame_obligations_ok_spec(paddr, *old(regions), *final(regions)),

r is Err ==> MetaSlot::live_frame_obligations_err_spec(*old(regions), *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.

Source

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

with

Tracked(perm): Tracked<&'a PointsTo<MetaSlot, Metadata<M>>>,

requires

self.ptr.addr() == perm.addr(),

self.ptr == perm.points_to.pptr(),

perm.is_init(),

perm.wf(&perm.inner_perms),

returns

perm.value().metadata,

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.

Source §

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

Source

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

with

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

requires

old(regions).inv(),

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

ensures

final(regions).inv(),

res is Ok
    ==> final(regions).ref_count(frame_to_index(paddr))
        == old(regions).ref_count(frame_to_index(paddr)) + 1,

res matches Ok(res) ==> res.ptr == old(regions).slots[frame_to_index(paddr)].pptr(),

!has_safe_slot(paddr) ==> res is Err,

old(regions).slot_owners_agree_except(*final(regions), frame_to_index(paddr)),

res is Ok
    ==> MetaSlot::live_frame_obligations_ok_spec(paddr, *old(regions), *final(regions)),

res is Err ==> MetaSlot::live_frame_obligations_err_spec(*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.

Source §

impl<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>> Frame<M>

Source

pub exec fn start_paddr(&self) -> Paddr

with

Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,

requires

perm.addr() == self.ptr.addr(),

perm.is_init(),

FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end,

perm.addr() % META_SLOT_SIZE == 0,

returns

meta_to_frame(self.ptr.addr()),

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.

Source

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

with

Tracked(regions): Tracked<&MetaRegionOwners>,

requires

self.inv(),

other.inv(),

regions.inv(),

ensures

res == (meta_to_frame(self.ptr.addr()) == meta_to_frame(other.ptr.addr())),

Compares two frames by their start physical address.

§Verified Properties

§Preconditions

Safety Invariant: the frames and metadata regions must satisfy the global invariants.

§Postconditions

Correctness: the function returns true if the frames have the same physical addresses and false otherwise.

§Safety

Everything is immutable, so the safety invariant is preserved implicitly.

§Verification Design

This is an inherent impl equivalent to PartialEq::eq for Frame<M>: freed from the trait signature so that this version can thread the tracked MetaRegionOwners via verus_spec.

Source

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

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.

Source

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

Gets the size of this page in bytes.

Source

pub exec fn reference_count(&self) -> u64

with

Tracked(slot_own): Tracked<&mut MetaSlotOwner>,
Tracked(perm): Tracked<&PointsTo<MetaSlot, Metadata<M>>>,

requires

perm.addr() == self.ptr.addr(),

perm.points_to.pptr() == self.ptr,

perm.is_init(),

perm.wf(&perm.inner_perms),

perm.inner_perms.ref_count.id() == perm.points_to.value().ref_count.id(),

returns

perm.value().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.

§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.

§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.

Source

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

with

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

requires

self.inv_with_regions(*old(regions)),

ensures

final(regions).inv(),

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

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

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

final(regions).frame_obligations =~= old(regions).frame_obligations,

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.

Source

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

with

Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,

requires

slot_perm.pptr() == self.ptr,

slot_perm.is_init(),

returns

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

Source §

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

Source

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.

Source §

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

Source

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<'rcu>>,
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.unwrap().meta_addr_self(),

guards.unlocked(owner@.value.node.unwrap().meta_addr_self()),

MetaSlot::get_from_unused_spec(
    meta_to_frame(owner@.value.node.unwrap().meta_addr_self()),
    false,
    *old(regions),
    *final(regions),
),

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

final(regions).frame_obligations
    =~= old(regions)
        .frame_obligations
        .insert(
            frame_to_index(meta_to_frame(owner@.value.node.unwrap().meta_addr_self())),
        ),

old(regions)
    .slots
    .contains_key(
        frame_to_index(meta_to_frame(owner@.value.node.unwrap().meta_addr_self())),
    ),

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

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

forall |i: usize| {
    #[trigger] old(regions).slot_owners[i].inner_perms.ref_count.value()
        != REF_COUNT_UNUSED
        ==> i
            != frame_to_index(meta_to_frame(owner@.value.node.unwrap().meta_addr_self()))
},

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

*final(parent_owner)
    == old(parent_owner)
        .set_children_perm(
            idx,
            C::E::new_pt_spec(meta_to_frame(owner@.value.node.unwrap().meta_addr_self())),
        ),

final(regions).slots.contains_key(owner@.value.node.unwrap().slot_index),

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

Allocates a new empty page table node.

Source §

impl<'a, M: ?Sized> Frame<M>

Source

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

{
    &&& regions.slot_owners.contains_key(frame_to_index(paddr))
    &&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
    &&& has_safe_slot(paddr)
    &&& regions.inv()
    &&& regions.slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
        != REF_COUNT_UNUSED

}

Safety: The frame exists, is addressable, and its slot is alive (not torn down: ref_count != REF_COUNT_UNUSED). Under the borrow-protocol redesign this liveness gate replaces the prior raw_count <= 1 check — a slot that has not been torn down is safe to re-materialize as a Frame value. (>= 1 is not the right gate, since the UNUSED sentinel u64::MAX also satisfies it; and the PT-node ownership model only exposes != UNUSED.)

Source

pub open spec fn from_raw_ensures( old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, paddr: Paddr, r: Self, ) -> bool

{
    &&& new_regions.inv()
    &&& new_regions.slots.contains_key(frame_to_index(paddr))
    &&& new_regions.slot_owners[frame_to_index(paddr)]
        =~= old_regions.slot_owners[frame_to_index(paddr)]
    &&& new_regions.slot_owners[frame_to_index(paddr)].self_addr == r.ptr.addr()
    &&& forall |i: usize| {
        i != frame_to_index(paddr)
            ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
    }
    &&& forall |i: usize| {
        i != frame_to_index(paddr)
            ==> new_regions.slots.contains_key(i) == old_regions.slots.contains_key(i)
    }
    &&& r.ptr.addr() == frame_to_meta(paddr)
    &&& r.paddr() == paddr
    &&& r.inv()
    &&& new_regions.frame_obligations
        =~= old_regions.frame_obligations.insert(frame_to_index(paddr))

}

Source

pub open spec fn into_raw_pre_frame_inv(self) -> bool

{ self.inv() }

Safety Invariant: The frame’s structural invariant must hold.

Source

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

{ regions.slot_owners[self.index()].inner_perms.ref_count.value() != REF_COUNT_UNUSED }

Bookkeeping: The frame must be in use (not unused).

Source

pub open spec fn into_raw_post_noninterference( self, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, ) -> bool

{
    &&& forall |i: usize| {
        i != self.index() && old_regions.slots.contains_key(i)
            ==> new_regions.slots.contains_key(i)
                && new_regions.slots[i] == old_regions.slots[i]
    }
    &&& forall |i: usize| {
        i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
    }
    &&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()

}

Safety: Frames other than this one are not affected by the call.

Source §

impl<M: ?Sized> Frame<M>

Source

pub open spec fn paddr(self) -> usize

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

Source

pub open spec fn index(self) -> usize

{ frame_to_index(self.paddr()) }

Source §

impl<M: ?Sized> Frame<M>

Source

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

{
    let idx = self.index();
    let slot_own = s.slot_owners[idx];
    &&& self.inv()
    &&& s.inv()
    &&& s.slots.contains_key(idx)
    &&& s.slots[idx].pptr() == self.ptr
    &&& s.slot_owners.contains_key(idx)
    &&& slot_own.inner_perms.ref_count.value() != REF_COUNT_UNUSED
    &&& slot_own.inner_perms.ref_count.value() != REF_COUNT_UNIQUE
    &&& slot_own.inner_perms.ref_count.value() > 0
    &&& slot_own.inner_perms.ref_count.value() <= REF_COUNT_MAX

}

Cross-object well-formedness predicate: this Frame handle and the supplied MetaRegionOwners state are mutually consistent. Packages the static “Frame ⟷ state” conjuncts (slot/pointer identity, slot in-use range) so that consumer specs ([drop_requires], [clone_requires]) read uniformly.

Name: inv_with_regions (not just wf) to avoid clashing with the OwnerOf::wf(self, Self::Owner) impl that [PageTableNode<C> = Frame<PageTablePageMeta<C>>] inherits — the two predicates take different argument types and serve different purposes (per-handle vs. per-owner well-formedness).

The rc range (> 0 ∧ ≠ UNUSED ∧ ≠ UNIQUE ∧ ≤ MAX) captures the fact that holding a Frame<M> is itself evidence that the slot is in the SHARED state — no UNUSED, no UNIQUE (which is reserved for UniqueFrame). Combined with [MetaSlotOwner::inv]’s SHARED branch (post Item 1), inv_with_regions implies storage.is_init, in_list == 0, and vtable_ptr.is_init at the slot, so consumers don’t have to repeat those.

Not preserved by drop for self: dropping self releases the reference; for other handles to the same slot, inv_with_regions is preserved by drop’s >1 branch (post rc ∈ [1, MAX-1]) and vacuous in the ==1 branch (no other handles to break).

Source §

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

Source

pub open spec fn from_raw_spec(paddr: Paddr) -> Self

{
    Frame::<M> {
        ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
        _marker: PhantomData,
    }
}

Converts a single Frame into a one-page Segment by forgetting the frame and recording its paddr range. Symmetric to vostd’s From<Frame<M>> for Segment<M>.

Source §

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

Source §

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

Source §

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

Source §

open spec fn inv(self) -> bool

{
    &&& self.ptr.addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= self.ptr.addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE

}

Source §

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

Source §

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

{
    let idx = frame_to_index(meta_to_frame(self.ptr.addr()));
    &&& self.inv()
    &&& perm.inv()
    &&& perm.slots.contains_key(idx)
    &&& perm.slot_owners.contains_key(idx)
    &&& perm.slot_owners[idx].inner_perms.ref_count.value() > 0
    &&& perm.slot_owners[idx].inner_perms.ref_count.value() != meta::REF_COUNT_UNUSED
    &&& perm.slot_owners[idx].inner_perms.ref_count.value() >= meta::REF_COUNT_MAX
        ==> may_panic()
    &&& has_safe_slot(meta_to_frame(self.ptr.addr()))

}

Source §

open spec fn clone_ensures( self, old_perm: MetaRegionOwners, new_perm: MetaRegionOwners, res: Self, ) -> bool

{
    let idx = frame_to_index(meta_to_frame(self.ptr.addr()));
    &&& new_perm.inv()
    &&& new_perm.slot_owners[idx].inner_perms.ref_count.value()
        == old_perm.slot_owners[idx].inner_perms.ref_count.value() + 1
    &&& new_perm.slot_owners[idx].inner_perms.ref_count.id()
        == old_perm.slot_owners[idx].inner_perms.ref_count.id()
    &&& new_perm.slot_owners[idx].inner_perms.storage
        == old_perm.slot_owners[idx].inner_perms.storage
    &&& new_perm.slot_owners[idx].inner_perms.vtable_ptr
        == old_perm.slot_owners[idx].inner_perms.vtable_ptr
    &&& new_perm.slot_owners[idx].inner_perms.in_list
        == old_perm.slot_owners[idx].inner_perms.in_list
    &&& new_perm.slot_owners[idx].paths_in_pt == old_perm.slot_owners[idx].paths_in_pt
    &&& new_perm.slot_owners[idx].self_addr == old_perm.slot_owners[idx].self_addr
    &&& new_perm.slot_owners[idx].usage == old_perm.slot_owners[idx].usage
    &&& new_perm.slots =~= old_perm.slots
    &&& forall |i: usize| {
        i != idx ==> (#[trigger] new_perm.slot_owners[i] == old_perm.slot_owners[i])
    }
    &&& new_perm.slot_owners.dom() =~= old_perm.slot_owners.dom()
    &&& new_perm.frame_obligations =~= old_perm.frame_obligations.insert(idx)

}

Source §

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

Source §

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

We need to keep track of when frames are forgotten with ManuallyDrop. We maintain a counter for each frame of how many times it has been forgotten (raw_count). Calling ManuallyDrop::new increments the counter. It is technically safe to forget a frame multiple times, and this will happen with read-only FrameRefs. All such references need to be dropped by the time from_raw is called. So, ManuallyDrop::drop decrements the counter when the reference is dropped, and from_raw may only be called when the counter is 1.

Source §

type Key = usize

Slot index. Lets the obligation token identify which slot it belongs to — Drop::drop’s precondition then refuses a token from one slot being used to drop a Frame at another slot. (Full per-instance ledger enforcement is a follow-up; for now consume_obligation is a no-op so the token’s identity is documentary rather than gated against a multiset.)

Source §

open spec fn key(self) -> Self::Key

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

Source §

open spec fn constructor_requires(self, s: Self::State) -> bool

{
    &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.inv()

}

Source §

open spec fn constructor_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

{
    let slot_own = s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))];
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))] == slot_own
    &&& forall |i: usize| {
        i != frame_to_index(meta_to_frame(self.ptr.addr()))
            ==> s1.slot_owners[i] == s0.slot_owners[i]
    }
    &&& s1.slots =~= s0.slots
    &&& s1.slot_owners.dom() =~= s0.slot_owners.dom()
    &&& s1.frame_obligations =~= s0.frame_obligations.insert(obl_key)

}

Source §

proof fn constructor_spec(self, tracked s: &mut Self::State) -> tracked obl : DropObligation<Self::Key>

Source §

open spec fn drop_requires(self, s: Self::State) -> bool

{
    let idx = frame_to_index(meta_to_frame(self.ptr.addr()));
    let slot_own = s.slot_owners[idx];
    &&& self.inv_with_regions(s)
    &&& slot_own.inner_perms.ref_count.value() == 1
        ==> {
            &&& slot_own.paths_in_pt.is_empty()

        }

}

Source §

open spec fn drop_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

{
    let idx = frame_to_index(meta_to_frame(self.ptr.addr()));
    let so0 = s0.slot_owners[idx];
    let so1 = s1.slot_owners[idx];
    &&& s1.inv()
    &&& forall |i: usize| i != idx ==> s1.slot_owners[i] == s0.slot_owners[i]
    &&& s1.slots =~= s0.slots
    &&& s1.slot_owners.dom() =~= s0.slot_owners.dom()
    &&& so1.self_addr == so0.self_addr
    &&& so1.usage == so0.usage
    &&& so1.paths_in_pt == so0.paths_in_pt
    &&& so0.inner_perms.ref_count.value() == 1
        ==> so1.inner_perms.ref_count.value() == REF_COUNT_UNUSED
    &&& so0.inner_perms.ref_count.value() > 1
        ==> so1.inner_perms.ref_count.value()
            == (so0.inner_perms.ref_count.value() - 1) as u64
    &&& s1.frame_obligations =~= s0.frame_obligations.remove(obl_key)

}

Source §

open spec fn consume_requires(self, s: Self::State, obl_key: Self::Key) -> bool

{ s.frame_obligations.count(obl_key) > 0 }

ManuallyDrop::new / Drop::drop require the ledger to contain at least one entry at this slot — preventing a forged token from being used to “consume” a non-existent obligation.

Source §

open spec fn consume_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

{
    &&& s1.frame_obligations =~= s0.frame_obligations.remove(obl_key)
    &&& s1.slots =~= s0.slots
    &&& s1.slot_owners =~= s0.slot_owners

}

Source §

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

fn try_into(self) -> Result<U, >::Error>

Performs the conversion.

§

Struct Frame Copy item path

§Verification Design

Fields§

Implementations§

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

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

impl<M: ?Sized> Frame<M>

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

impl<'a, M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M>

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

§Verified Properties

§Preconditions

§Postconditions

§Safety

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

§Verified Properties

§Preconditions

§Postconditions

§Safety

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

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

§Verified Properties

§Preconditions

§Postconditions

§Safety

impl<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>> Frame<M>

pub exec fn start_paddr(&self) -> Paddr

§Verified Properties

§Preconditions

§Postconditions

§Safety

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

§Verified Properties

§Preconditions

§Postconditions

§Safety

§Verification Design

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

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

pub exec fn reference_count(&self) -> u64

§Verified Properties

§Preconditions

§Postconditions

§Safety

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

§Verified Properties

§Preconditions

§Postconditions

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

§Verified Properties

§Preconditions

§Postconditions

§Safety

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

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

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

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

impl<'a, M: ?Sized> Frame<M>

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

pub open spec fn from_raw_ensures( old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, paddr: Paddr, r: Self, ) -> bool

pub open spec fn into_raw_pre_frame_inv(self) -> bool

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

pub open spec fn into_raw_post_noninterference( self, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, ) -> bool

impl<M: ?Sized> Frame<M>

pub open spec fn paddr(self) -> usize

pub open spec fn index(self) -> usize

impl<M: ?Sized> Frame<M>

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

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

pub open spec fn from_raw_spec(paddr: Paddr) -> Self

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

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

Trait Implementations§

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

exec fn drop( self, verus_tmp_regions: Tracked<&mut MetaRegionOwners>, verus_tmp_obl: Tracked<DropObligation<usize>>, )

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

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

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

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

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

Struct Frame

impl<M> Freeze for Frame<M>
where M: ?Sized,

impl<M> Send for Frame<M>
where M: Send + ?Sized,

impl<M> Sync for Frame<M>
where M: Sync + ?Sized,

impl<M> Unpin for Frame<M>
where M: Unpin + ?Sized,

impl<M> UnsafeUnpin for Frame<M>
where M: ?Sized,

impl<M> UnwindSafe for Frame<M>
where M: UnwindSafe + ?Sized,

impl<T> Any for T
where T: 'static + ?Sized,

impl<T> Borrow<T> for T
where T: ?Sized,

impl<T> BorrowMut<T> for T
where T: ?Sized,

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

impl<T, U> Into<U> for T
where U: From<T>,

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

impl<T, U> TryFrom<U> for T
where U: Into<T>,

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,