Skip to main content

UniqueFrame

ostd::mm::frame::unique

Struct UniqueFrame 

Source 
pub struct UniqueFrame<M: AnyFrameMeta + ?Sized + 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).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@->0)
        &&& final(regions).frame_obligations
            == old(regions).frame_obligations.insert(frame_to_index(paddr))

    },
res is Err ==> final(regions).frame_obligations == old(regions).frame_obligations,
final(regions).inv(),

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(),
owner.global_inv(*old(regions)),
old(regions)
    .slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))]
    .inner_perms
    .in_list
    .value() == 0,
old(regions).inv(),
ensures
res.wf(new_owner@),
new_owner@.meta_perm_of(*final(regions)).value().metadata == metadata,
final(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>>,
Tracked(regions): Tracked<&'a MetaRegionOwners>,
requires
owner.inv(),
self.wf(*owner),
owner.global_inv(*regions),
ensures
owner.meta_perm_of(*regions).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<'a>(&'a mut self) -> res : &'a mut M

with
Tracked(owner): Tracked<&'a UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&'a mut MetaRegionOwners>,
requires
owner.inv(),
old(self).wf(*owner),
owner.global_inv(*old(regions)),
ensures
*final(self) == *old(self),
final(regions).slots.dom() == old(regions).slots.dom(),
final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),

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 const exec fn size(&self) -> usize

returns
PAGE_SIZE,

Gets the size of this page in bytes.

Source

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

returns
1u8,

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§

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

Source

pub exec fn start_paddr(&self) -> Paddr

with
Tracked(owner): Tracked<&UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
owner.inv(),
self.wf(*owner),
regions.inv(),
returns
meta_to_frame(self.ptr.addr()),

Gets the physical address of the start of the frame.

Source

pub exec fn reset_as_unused(self)

with
Tracked(owner): Tracked<UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
self.wf_with_region(owner, *old(regions)),
ensures
final(regions).inv(),

Resets the frame to unused without up-calling the allocator.

This is solely useful for the allocator implementation/testing and is highly experimental. Usage of this function is discouraged.

Usage of this function other than the allocator would actually leak the frame since the allocator would not be aware of the frame.

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.frame_obligations.count(frame_to_index(meta_to_frame(self.ptr.addr())))
        > 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 == old_regions.slot_owners
    &&& regions.frame_obligations
        == old_regions
            .frame_obligations
            .remove(frame_to_index(meta_to_frame(self.ptr.addr())))

}
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(),
returns
slot_perm.value(),
Source§

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

Source

pub exec fn try_from_shared(frame: Frame<M>) -> res : Result<Self, Frame<M>>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
frame.inv(),
old(regions).inv(),
ensures
final(regions).slots == old(regions).slots,
final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),

Tries to convert a shared frame into a unique one by CAS’ing ref_count from 1 to REF_COUNT_UNIQUE. Inherent sibling of TryFrom<Frame<M>> for UniqueFrame<M>.

Source§

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

Source

pub open spec fn wf_with_region( self, owner: UniqueFrameOwner<M>, s: MetaRegionOwners, ) -> bool

{
    let idx = owner.slot_index;
    let so = s.slot_owners[idx];
    &&& self.wf(owner)
    &&& owner.inv()
    &&& s.inv()
    &&& so.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
    &&& so.inner_perms.in_list.value() == 0
    &&& so.paths_in_pt.is_empty()

}

Cross-object validity of a live UNIQUE handle against the region map — the UniqueFrame analog of Frame::wf_with_region (which covers the SHARED state). Bundles the structural wf / owner.inv / regions.inv facts with the UNIQUE-state slot facts so a consumer (e.g. UniqueFrame::drop) can state a single invariant instead of re-listing each conjunct.

The slot’s slot_owners.contains_key(idx), slot_vaddr == meta_addr(idx), storage.is_init(), and vtable_ptr.is_init() are derived, not required: regions.inv() (with owner.inv()’s idx < max_meta_slots) delivers the first two and slot_owners[idx].inv(); the latter’s UNIQUE branch (under rc == REF_COUNT_UNIQUE) gives the storage/vtable init. The genuinely-extra conjuncts are the UNIQUE state itself plus in_list == 0 and paths_in_pt.is_empty() (a sole owner is neither on the free list nor mapped into any page table).

Trait Implementations§

Source§

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

Source§

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

Source§

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

Source§

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

{
    &&& self.ptr.addr() == meta_addr(owner.slot_index)

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

type Key = usize

Slot index — identifies which slot the obligation belongs to. UniqueFrame shares the frame_obligations multiset with Frame: at any moment a slot is in either Frame-SHARED mode (ref_count in [1, MAX]) or UniqueFrame-UNIQUE mode (ref_count == UNIQUE), never both, so the multiset semantics are unambiguous.

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
        .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, obl_key: Self::Key, ) -> bool

{
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].inner_perms
        == s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].inner_perms
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].slot_vaddr
        == s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].slot_vaddr
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].usage
        == s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].usage
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].paths_in_pt
        == s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].paths_in_pt
    &&& 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.frame_obligations =~= s0.frame_obligations.insert(obl_key)
    &&& s1.inv()

}
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

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

}
Source§

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

{
    &&& 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.frame_obligations =~= s0.frame_obligations.remove(obl_key)
    &&& s1.inv()

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

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

Source§

type State = MetaRegionOwners

Source§

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

Source§

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.

Source§

type Error = Frame<M>

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

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

Source§

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

Auto Trait Implementations§

§

impl<M> Freeze for UniqueFrame<M>

§

impl<M> !RefUnwindSafe for UniqueFrame<M>

§

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

§

impl<M> UnsafeUnpin for UniqueFrame<M>

§

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>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A