Enum Meta Slot Storage &nbsp; Copy item path

Empty([u8; 39])

FrameLink(StoredLink)

PTNode(StoredPageTablePageMeta)

Implementations§

impl MetaSlotStorage

pub open spec fn get_link_spec(self) -> Option<StoredLink>

{
    match self {
        MetaSlotStorage::FrameLink(link) => Some(link),
        _ => None,
    }
}

pub exec fn get_link(self) -> res : Option<StoredLink>

ensures

res == self.get_link_spec(),

pub open spec fn get_node_spec(self) -> Option<StoredPageTablePageMeta>

{
    match self {
        MetaSlotStorage::PTNode(node) => Some(node),
        _ => None,
    }
}

pub exec fn get_node(self) -> res : Option<StoredPageTablePageMeta>

ensures

res == self.get_node_spec(),

Trait Implementations§

impl AnyFrameMeta for MetaSlotStorage

MetaSlotStorage is an inductive tagged union of all of the frame meta types that we work with in this development. So, it should itself implement AnyFrameMeta, and it can then be used to stand in for dyn AnyFrameMeta.

uninterp fn vtable_ptr(&self) -> usize

fn on_drop(&mut self)

fn is_untyped(&self) -> bool

proof fn to_repr_wf(self)

Auto Trait Implementations§

impl !Freeze for MetaSlotStorage

impl !RefUnwindSafe for MetaSlotStorage

impl Send for MetaSlotStorage

impl Sync for MetaSlotStorage

impl Unpin for MetaSlotStorage

impl UnwindSafe for MetaSlotStorage

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