Enum Meta Slot Storage &nbsp; Copy item path

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

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlotStorage> for Link<M>

open spec fn wf(r: MetaSlotStorage, perm: LinkInnerPerms<M>) -> bool

{
    match r {
        MetaSlotStorage::FrameLink(link) => (
            &&& M::wf(link.slot, perm.storage)
            &&& (link.next is Some) == (perm.next_ptr is Some)
            &&& (link.prev is Some) == (perm.prev_ptr is Some)

        ),
        _ => false,
    }
}

open spec fn to_repr_spec( self, perm: LinkInnerPerms<M>, ) -> (MetaSlotStorage, LinkInnerPerms<M>)

{
    let (slot, storage) = self.meta.to_repr_spec(perm.storage);
    (
        MetaSlotStorage::FrameLink(StoredLink {
            next: match self.next {
                Some(ptr) => Some(ptr.addr),
                None => None,
            },
            prev: match self.prev {
                Some(ptr) => Some(ptr.addr),
                None => None,
            },
            slot,
        }),
        LinkInnerPerms {
            storage,
            next_ptr: match self.next {
                Some(ptr) => Some(ptr.ptr),
                None => None,
            },
            prev_ptr: match self.prev {
                Some(ptr) => Some(ptr.ptr),
                None => None,
            },
        },
    )
}

exec fn to_repr( self, verus_tmp_perm: Tracked<&mut LinkInnerPerms<M>>, ) -> MetaSlotStorage

open spec fn from_repr_spec(r: MetaSlotStorage, perm: LinkInnerPerms<M>) -> Self

{
    match r {
        MetaSlotStorage::FrameLink(link) => {
            Link {
                next: match link.next {
                    Some(addr) => {
                        Some(ReprPtr {
                            addr,
                            ptr: perm.next_ptr.unwrap(),
                            _T: PhantomData,
                        })
                    }
                    None => None,
                },
                prev: match link.prev {
                    Some(addr) => {
                        Some(ReprPtr {
                            addr,
                            ptr: perm.prev_ptr.unwrap(),
                            _T: PhantomData,
                        })
                    }
                    None => None,
                },
                meta: M::from_repr_spec(link.slot, perm.storage),
            }
        }
        _ => {
            Link {
                next: None,
                prev: None,
                meta: M::from_repr_spec(MetaSlotSmall, perm.storage),
            }
        }
    }
}

exec fn from_repr( r: MetaSlotStorage, verus_tmp_perm: Tracked<&LinkInnerPerms<M>>, ) -> Self

exec fn from_borrowed<'a>( r: &'a MetaSlotStorage, verus_tmp_perm: Tracked<&'a LinkInnerPerms<M>>, ) -> &'a Self

proof fn from_to_repr(self, perm: LinkInnerPerms<M>)

proof fn to_from_repr(r: MetaSlotStorage, perm: LinkInnerPerms<M>)

proof fn to_repr_wf(self, perm: LinkInnerPerms<M>)

type Perm = LinkInnerPerms<M>

If the underlying representation contains cells, the translation may require permission objects that access them.

impl Repr<MetaSlotStorage> for MetaSlotStorage

open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool

{ true }

open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ())

{ (self, ()) }

exec fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage

open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self

{ slot }

exec fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self

exec fn from_borrowed<'a>( slot: &'a MetaSlotStorage, verus_tmp_perm: Tracked<&'a ()>, ) -> &'a Self

proof fn from_to_repr(self, perm: ())

proof fn to_from_repr(slot: MetaSlotStorage, perm: ())

proof fn to_repr_wf(self, perm: ())

type Perm = ()

If the underlying representation contains cells, the translation may require permission objects that access them.

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

open spec fn wf(r: MetaSlotStorage, perm: ()) -> bool

{ matches!(r, MetaSlotStorage::PTNode(_)) }

open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ())

{ (MetaSlotStorage::PTNode(self.into_spec()), ()) }

exec fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage

open spec fn from_repr_spec(r: MetaSlotStorage, perm: ()) -> Self

{
    match r {
        MetaSlotStorage::PTNode(node) => node.into_spec::<C>(),
        _ => arbitrary(),
    }
}

exec fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self

exec fn from_borrowed<'a>( r: &'a MetaSlotStorage, verus_tmp_perm: Tracked<&'a ()>, ) -> &'a Self

proof fn from_to_repr(self, perm: ())

proof fn to_from_repr(r: MetaSlotStorage, perm: ())

proof fn to_repr_wf(self, perm: ())

type Perm = ()

If the underlying representation contains cells, the translation may require permission objects that access them.

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