Struct Meta Slot &nbsp; Copy item path

impl MetaSlot

pub exec fn addr_of(&self, Tracked(perm): Tracked<&PointsTo<MetaSlot>>) -> Paddr

requires

self == perm.value(),

This is the equivalent of &self as *const as Vaddr, but we need to axiomatize it.

pub exec fn cast_slot<T: Repr<MetaSlot>>( &self, addr: usize, verus_tmp_perm: Tracked<&PointsTo<MetaSlot>>, ) -> res : ReprPtr<MetaSlot, T>

requires

perm.value() == self,

addr == perm.addr(),

ensures

res.ptr.addr() == addr,

res.addr == addr,

pub exec fn cast_perm<T: Repr<MetaSlot>>( addr: usize, verus_tmp_perm: Tracked<PointsTo<MetaSlot>>, ) -> Tracked<PointsTo<MetaSlot, T>>

pub exec fn inc_ref_count(&self)

with

Tracked(rc_perm): Tracked <& mut PermissionU64>,

requires

old(rc_perm).is_for(self.ref_count),

old(rc_perm).value() != 0,

old(rc_perm).value() != REF_COUNT_UNUSED,

old(rc_perm).value() < REF_COUNT_MAX,

Increases the frame reference count by one.

§Safety

The caller must have already held a reference to the frame.

pub exec fn frame_paddr(&self) -> pa : Paddr

with

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

requires

perm.value() == self,

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

perm.addr() % META_SLOT_SIZE() == 0,

Gets the corresponding frame’s physical address.

pub exec fn as_meta_ptr<M: AnyFrameMeta + Repr<MetaSlot>>( &self, ) -> res : ReprPtr<MetaSlot, M>

with

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

requires

self == perm.value(),

ensures

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

res.addr == perm.addr(),

Gets the stored metadata as type M.

Calling the method should be safe, but using the returned pointer would be unsafe. Specifically, the derefernecer should ensure that:

the stored metadata is initialized (by Self::write_meta) and valid;
the initialized metadata is of type M;
the returned pointer should not be dereferenced as mutable unless having exclusive access to the metadata slot.

pub exec fn write_meta<M: AnyFrameMeta + Repr<MetaSlot>>(&self, metadata: M)

with

Tracked(slot_own): Tracked <& mut MetaSlotOwner>,

requires

old(slot_own).storage.pptr() == self.storage,

ensures

slot_own.ref_count == old(slot_own).ref_count,

slot_own.vtable_ptr.is_init(),

slot_own.vtable_ptr.value() == metadata.vtable_ptr(),

slot_own.in_list == old(slot_own).in_list,

slot_own.self_addr == old(slot_own).self_addr,

Writes the metadata to the slot without reading or dropping the previous value.

§Safety

The caller should have exclusive access to the metadata slot’s fields.

impl MetaSlot

pub open spec fn from_unused_slot_spec<M: AnyFrameMeta>( paddr: Paddr, metadata: M, as_unique_ptr: bool, ) -> MetaSlotModel

{
    let (rc, status) = if as_unique_ptr {
        (REF_COUNT_UNIQUE, MetaSlotStatus::UNIQUE)
    } else {
        (1, MetaSlotStatus::SHARED)
    };
    MetaSlotModel {
        status,
        storage: cell::MemContents::Uninit,
        ref_count: rc,
        vtable_ptr: simple_pptr::MemContents::Init(metadata.vtable_ptr()),
        in_list: 0,
        self_addr: frame_to_meta(paddr),
        usage: PageUsage::Frame,
    }
}

pub open spec fn get_from_unused_spec<M: AnyFrameMeta>( paddr: Paddr, metadata: M, as_unique_ptr: bool, pre: MetaRegionModel, ) -> (PPtr<MetaSlot>, MetaRegionModel)

recommends

paddr % 4096 == 0,

paddr < MAX_PADDR(),

pre.inv(),

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

{
    let ptr = get_slot_spec(paddr);
    let idx = frame_to_index(paddr);
    let post = MetaRegionModel {
        slots: pre
            .slots
            .insert(idx, Self::from_unused_slot_spec(paddr, metadata, as_unique_ptr)),
    };
    (ptr, post)
}

pub open spec fn update_index_tracked( idx: usize, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

recommends

pre.slots.contains_key(idx),

{
    &&& pre.slots.dom() == post.slots.dom()
    &&& pre.dropped_slots.dom() == post.dropped_slots.dom()
    &&& pre.slot_owners.dom() == post.slot_owners.dom()
    &&& forall |i: usize| {
        #[trigger] pre.slots.contains_key(i) && i != idx
            ==> pre.slots[i] == post.slots[i]
    }
    &&& forall |i: usize| {
        #[trigger] pre.dropped_slots.contains_key(i) && i != idx
            ==> pre.dropped_slots[i] == post.dropped_slots[i]
    }
    &&& forall |i: usize| {
        #[trigger] pre.slot_owners.contains_key(i) && i != idx
            ==> pre.slot_owners[i] == post.slot_owners[i]
    }

}

All other slots remain unchanged.

pub open spec fn get_from_unused_tracked<M: AnyFrameMeta>( paddr: Paddr, metadata: M, as_unique_ptr: bool, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

recommends

paddr % 4096 == 0,

paddr < MAX_PADDR(),

pre.inv(),

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

{
    let idx = paddr / 4096;
    {
        &&& Self::update_index_tracked(idx, pre, post)
        &&& Self::get_from_unused_spec(paddr, metadata, as_unique_ptr, pre.view()).1
            == post.view()

    }
}

pub open spec fn get_from_in_use_spec( paddr: Paddr, pre: MetaRegionModel, ) -> (PPtr<MetaSlot>, MetaRegionModel)

recommends

paddr % 4096 == 0,

paddr < MAX_PADDR(),

pre.inv(),

0 <= pre.slots[paddr / 4096].ref_count < REF_COUNT_MAX,

{
    let ptr = get_slot_spec(paddr);
    let idx = paddr / 4096;
    let pre_slot = pre.slots[idx];
    let post = MetaRegionModel {
        slots: pre
            .slots
            .insert(
                idx,
                MetaSlotModel {
                    ref_count: (pre_slot.ref_count + 1) as u64,
                    ..pre_slot
                },
            ),
    };
    (ptr, post)
}

pub open spec fn get_from_in_use_tracked( paddr: Paddr, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

recommends

paddr % 4096 == 0,

paddr < MAX_PADDR(),

pre.inv(),

0 <= pre.view().slots[paddr / 4096].ref_count < REF_COUNT_MAX,

{
    let idx = paddr / 4096;
    {
        &&& Self::update_index_tracked(idx, pre, post)
        &&& Self::get_from_in_use_spec(paddr, pre.view()).1 == post.view()

    }
}

pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> MetaSlotModel

recommends

pre.inv(),

pre.status == MetaSlotStatus::SHARED,

{
    MetaSlotModel {
        ref_count: (pre.ref_count + 1) as u64,
        ..pre
    }
}

Trait Implementations§

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

{
    &&& self.storage == owner.storage.pptr()
    &&& self.ref_count.id() == owner.ref_count.id()
    &&& self.vtable_ptr == owner.vtable_ptr.pptr()
    &&& self.in_list.id() == owner.in_list.id()

}

type Owner = MetaSlotOwner

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

impl<M: AnyFrameMeta> Repr<MetaSlot> for Frame<M>

open spec fn wf(m: MetaSlot) -> bool

{ true }

open spec fn to_repr_spec(self) -> MetaSlot

{ arbitrary() }

open spec fn from_repr_spec(r: MetaSlot) -> Self

{ arbitrary() }

exec fn to_repr(self) -> res : MetaSlot

ensures

res == self.to_repr_spec(),

exec fn from_repr(r: MetaSlot) -> res : Self

ensures

res == Self::from_repr_spec(r),

exec fn from_borrowed<'a>(r: &'a MetaSlot) -> res : &'a Self

ensures

*res == Self::from_repr_spec(*r),

proof fn from_to_repr(self)

ensures

Self::from_repr(self.to_repr()) == self,

proof fn to_from_repr(r: MetaSlot)

ensures

Self::from_repr(r).to_repr() == r,

proof fn to_repr_wf(self)

ensures

Self::wf(self.to_repr()),

impl<M: AnyFrameMeta + Repr<MetaSlot>> Repr<MetaSlot> for Link<M>

uninterp fn wf(r: MetaSlot) -> bool

uninterp fn to_repr_spec(self) -> MetaSlot

exec fn to_repr(self) -> MetaSlot

uninterp fn from_repr_spec(r: MetaSlot) -> Self

exec fn from_repr(r: MetaSlot) -> Self

exec fn from_borrowed<'a>(r: &'a MetaSlot) -> &'a Self

proof fn from_to_repr(self)

ensures

Self::from_repr(self.to_repr()) == self,

proof fn to_from_repr(r: MetaSlot)

ensures

Self::from_repr(r).to_repr() == r,

proof fn to_repr_wf(self)

ensures

<Self as Repr<MetaSlot>>::wf(self.to_repr()),

impl Repr<MetaSlot> for MetaSlotStorage

uninterp fn wf(slot: MetaSlot) -> bool

uninterp fn to_repr_spec(self) -> MetaSlot

exec fn to_repr(self) -> MetaSlot

uninterp fn from_repr_spec(slot: MetaSlot) -> Self

exec fn from_repr(slot: MetaSlot) -> Self

exec fn from_borrowed<'a>(slot: &'a MetaSlot) -> &'a Self

proof fn from_to_repr(self)

proof fn to_from_repr(slot: MetaSlot)

proof fn to_repr_wf(self)

impl<C: PageTableConfig> Repr<MetaSlot> for PageTablePageMeta<C>

uninterp fn wf(r: MetaSlot) -> bool

uninterp fn to_repr_spec(self) -> MetaSlot

exec fn to_repr(self) -> MetaSlot

uninterp fn from_repr_spec(r: MetaSlot) -> Self

exec fn from_repr(r: MetaSlot) -> Self

exec fn from_borrowed<'a>(r: &'a MetaSlot) -> &'a Self

proof fn from_to_repr(self)

proof fn to_from_repr(r: MetaSlot)

proof fn to_repr_wf(self)

Auto Trait Implementations§

impl !Freeze for MetaSlot

impl !RefUnwindSafe for MetaSlot

impl Send for MetaSlot

impl Sync for MetaSlot

impl Unpin for MetaSlot

impl UnwindSafe for MetaSlot

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