UniqueFrame

ostd::mm::frame::unique

Struct UniqueFrame 

Source 
pub struct UniqueFrame<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
}

Fields§

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

Implementations§

Source§

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

Source

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

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
->
owner: Tracked<Option<UniqueFrameOwner<M>>>,
requires
old(regions).slots.contains_key(frame_to_index(paddr)),
old(regions).slot_owners.contains_key(frame_to_index(paddr)),
old(regions).slot_owners[frame_to_index(paddr)].usage is Unused,
old(regions).inv(),
ensures
!has_safe_slot(paddr) ==> res is Err,
res is Ok ==> res.unwrap().wf(owner@.unwrap()),

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

The caller should provide the initial metadata of the page.

§Verified Properties
§Preconditions

The page must be unused and the metadata region must be well-formed.

§Postconditions

If the page is valid, the function returns a unique frame.

§Safety

If paddr is misaligned or out of bounds, the function will return an error. If it returns a frame, it also returns an owner for that frame, indicating that the caller now has exclusive ownership of it. See [Safe Encapsulation] for more details.

Source

pub open spec fn transmute_spec<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>( self, transmuted: UniqueFrame<M1>, ) -> bool

{
    &&& transmuted.ptr.addr() == self.ptr.addr()
    &&& transmuted._marker == PhantomData::<M1>

}
Source

pub exec fn transmute<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>( self, ) -> res : UniqueFrame<M1>

ensures
Self::transmute_spec(self, res),
Source

pub exec fn repurpose<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>( self, metadata: M1, ) -> res : UniqueFrame<M1>

with
Tracked(owner): Tracked<UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
->
new_owner: Tracked<UniqueFrameOwner<M1>>,
requires
self.wf(owner),
owner.inv(),
old(regions).slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr()))),
old(regions)
    .slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))]
    .inner_perms
    .ref_count
    .value() == REF_COUNT_UNIQUE,
old(regions).inv(),
ensures
res.wf(new_owner@),
new_owner@.meta_perm.value().metadata == metadata,
regions.inv(),

Repurposes the frame with a new metadata.

§Verified Properties
§Preconditions
  • The caller must provide a valid owner for the frame, and the metadata region invariants must hold.
  • The meta slot’s reference count must be REF_COUNT_UNIQUE.
§Postconditions

The function returns a new owner for the frame with the new metadata, and the metadata region invariants are preserved.

§Safety

The existence of a valid owner guarantees that the memory is initialized with metadata of type M, and represents that the caller has exclusive ownership of the frame.

Source

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

with
Tracked(owner): Tracked<&'a UniqueFrameOwner<M>>,
requires
owner.inv(),
self.wf(*owner),
ensures
owner.meta_perm.mem_contents().value().metadata == l,

Gets the metadata of this page. Note that this function body differs from the original, because as_meta_ptr returns a ReprPtr<MetaSlot, Metadata<M>> instead of a *M. So in order to keep the immutable borrow, we borrow the metadata value from that pointer.

§Verified Properties
§Preconditions

The caller must provide a valid owner for the frame.

§Postconditions

The function returns the metadata of the frame.

§Safety

The existence of a valid owner guarantees that the memory is initialized with metadata of type M, and represents that the caller has exclusive ownership of the frame.

Source

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

with
Tracked(owner): Tracked<&UniqueFrameOwner<M>>,
requires
owner.inv(),
old(self).wf(*owner),
ensures
res.addr() == self.ptr.addr(),
res.ptr.addr() == self.ptr.addr(),
*self == *old(self),

Gets the mutable metadata of this page. Verified Properties

§Preconditions

The caller must provide a valid owner for the frame.

§Postconditions

The function returns the mutable metadata of the frame.

§Safety

The existence of a valid owner guarantees that the memory is initialized with metadata of type M, and represents that the caller has exclusive ownership of the frame. (See [Safe Encapsulation])

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + ?Sized> UniqueFrame<M>

Source

pub exec fn start_paddr(&self) -> Paddr

with
Tracked(owner): Tracked<&UniqueFrameOwner<M>>,
requires
owner.inv(),
self.wf(*owner),

Gets the physical address of the start of the frame.

Source

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.

Source

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

Gets the size of this page in bytes.

Source

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

{
    &&& regions.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& regions.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count
        == 0
    &&& regions.inv()

}
Source

pub open spec fn into_raw_ensures( self, old_regions: MetaRegionOwners, regions: MetaRegionOwners, r: Paddr, ) -> bool

{
    &&& r == meta_to_frame(self.ptr.addr())
    &&& regions.inv()
    &&& regions.slots =~= old_regions.slots
    &&& regions.slot_owners[frame_to_index(r)].raw_count == 1
    &&& forall |i: usize| {
        i != frame_to_index(r) ==> regions.slot_owners[i] == old_regions.slot_owners[i]
    }

}
Source

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

Trait Implementations§

Source§

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

§

fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V

Source§

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

Source§

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

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

}
Source§

type Owner = UniqueFrameOwner<M>

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

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

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.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
    &&& s
        .slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))]
        .inner_perms
        .ref_count
        .value() != REF_COUNT_UNUSED
    &&& s.inv()

}
Source§

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

{
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 1
    &&& 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.inv()

}
Source§

proof fn constructor_spec(self, tracked s: &mut Self::State)

Source§

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

{
    &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count > 0
    &&& s.inv()

}
Source§

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

{
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
    &&& 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.inv()

}
Source§

proof fn drop_spec(self, tracked s: &mut Self::State)

Source§

type State = MetaRegionOwners

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§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

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

Source§

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<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::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>

Source§

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

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::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<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>