Struct Unique Frame &nbsp; Copy item path

impl<M: AnyFrameMeta + Repr<MetaSlot> + OwnerOf> UniqueFrame<M>

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

with

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

requires

paddr < MAX_PADDR(),

paddr % PAGE_SIZE() == 0,

old(regions).slots.contains_key(frame_to_meta(paddr)),

old(regions).inv(),

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

The caller should provide the initial metadata of the page.

pub exec fn meta(&self) -> l : &M

Gets the metadata of this page.

pub exec fn meta_mut(&mut self) -> res : ReprPtr<MetaSlot, M>

with

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

ensures

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

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

*self == *old(self),

Gets the mutable metadata of this page.

impl<M: AnyFrameMeta + Repr<MetaSlot> + OwnerOf> UniqueFrame<M>

pub exec fn start_paddr(&self) -> Paddr

with

Tracked(regions): Tracked <& MetaRegionOwners>,

Gets the physical address of the start of the frame.

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

Gets the paging 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

Gets the size of this page in bytes.

pub exec fn from_raw(paddr: Paddr) -> res : (Self, Tracked<UniqueFrameOwner<M>>)

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(meta_perm): Tracked <PointsTo <MetaSlot,M>>,
Tracked(meta_own): Tracked <M ::Owner>,

requires

paddr < MAX_PADDR(),

paddr % PAGE_SIZE() == 0,

old(regions).dropped_slots.contains_key(frame_to_index(paddr)),

ensures

res.0.ptr.addr() == frame_to_meta(paddr),

res.0.wf(res.1@),

res.1@.meta_own == meta_own,

res.1@.meta_perm == meta_perm,

regions.slots[frame_to_index(paddr)] == old(regions).dropped_slots[frame_to_index(paddr)],

!regions.dropped_slots.contains_key(frame_to_index(paddr)),

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

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

Restores a raw physical address back into a unique frame.

§Safety

The caller must ensure that the physical address is valid and points to a forgotten frame that was previously casted by Self::into_raw.

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

with

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

requires

slot_perm.pptr() == self.ptr,

slot_perm.is_init(),

impl<M: AnyFrameMeta + Repr<MetaSlot> + OwnerOf> UniqueFrame<M>

pub open spec fn from_unused_spec( paddr: Paddr, metadata: M, pre: MetaRegionModel, ) -> (Self, MetaRegionModel)

recommends

paddr % PAGE_SIZE() == 0,

paddr < MAX_PADDR(),

pre.inv(),

pre.slots[frame_to_index(paddr)].ref_count == REF_COUNT_UNUSED,

{
    let (ptr, post) = MetaSlot::get_from_unused_spec(paddr, metadata, true, pre);
    (
        UniqueFrame {
            ptr,
            _marker: PhantomData,
        },
        post,
    )
}

pub proof fn from_unused_properties(paddr: Paddr, metadata: M, pre: MetaRegionModel)

requires

paddr % 4096 == 0,

paddr < MAX_PADDR(),

pre.inv(),

pre.slots[paddr / 4096].ref_count == REF_COUNT_UNUSED,

ensures

UniqueFrame::from_unused_spec(paddr, metadata, pre).1.inv(),

Trait Implementations§

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& self.ptr.addr() == owner.meta_perm.addr()

}

type Owner = UniqueFrameOwner<M>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Auto Trait Implementations§

impl<M> Freeze for UniqueFrame<M>

impl<M> !RefUnwindSafe for UniqueFrame<M>

impl<M> Send for UniqueFrame<M>
where M: Send,

impl<M> Sync for UniqueFrame<M>
where M: Sync,

impl<M> Unpin for UniqueFrame<M>
where M: Unpin,

impl<M> UnwindSafe for UniqueFrame<M>
where M: UnwindSafe,

Blanket Implementations§

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

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

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

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

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

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

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

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

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

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

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

type Error = Infallible

The type returned in the event of a conversion error.

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

Performs the conversion.

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

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

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

type Error = >::Error

The type returned in the event of a conversion error.

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

Performs the conversion.

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

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

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

fn obeys_try_into_spec() -> bool