Enum MetaSlotStorage 

pub enum MetaSlotStorage {
    Empty([u8; 39]),
    Untyped,
    FrameLink(StoredLink),
    PTNode(StoredPageTablePageMeta),
}

Variants

Empty([u8; 39])

Untyped

FrameLink(StoredLink)

PTNode(StoredPageTablePageMeta)

Implementations

impl MetaSlotStorage

pub fn arrow_0(self) -> StoredPageTablePageMeta

pub fn arrow_Empty_0(self) -> [u8; 39]

pub fn arrow_FrameLink_0(self) -> StoredLink

pub fn arrow_PTNode_0(self) -> StoredPageTablePageMeta

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 spec fn vtable_ptr(&self) -> usize

fn on_drop_pre( &self, reader: VmReader<'_, Infallible>, regions: MetaRegionOwners, vm_io_owner: VmIoOwner, ) -> bool

fn on_drop( &mut self, _reader: &mut VmReader<'_, Infallible>, verus_tmp__regions: Tracked<&mut MetaRegionOwners>, verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>, )

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)
            &&& link.next is Some ==> link.next->0 == perm.next_ptr->0.addr()
            &&& link.prev is Some ==> link.prev->0 == perm.prev_ptr->0.addr()

        ),
        _ => 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.ptr.addr()),
                None => None,
            },
            prev: match self.prev {
                Some(ptr) => Some(ptr.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, Tracked(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 {
                            ptr: perm.next_ptr->0,
                            _T: PhantomData,
                        })
                    }
                    None => None,
                },
                prev: match link.prev {
                    Some(addr) => {
                        Some(ReprPtr {
                            ptr: perm.prev_ptr->0,
                            _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, Tracked(perm): Tracked<&LinkInnerPerms<M>>, ) -> Self

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

exec fn from_borrowed_mut<'a>( r: &'a mut MetaSlotStorage, Tracked(perm): Tracked<&'a mut LinkInnerPerms<M>>, ) -> &'a mut 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 ReprPerm = 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, Tracked(perm): Tracked<&'a ()>, ) -> &'a Self

exec fn from_borrowed_mut<'a>( slot: &'a mut MetaSlotStorage, Tracked(perm): Tracked<&'a mut ()>, ) -> &'a mut Self

proof fn from_to_repr(self, perm: ())

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

proof fn to_repr_wf(self, perm: ())

type ReprPerm = ()

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, Tracked(perm): Tracked<&'a ()>, ) -> &'a Self

exec fn from_borrowed_mut<'a>( r: &'a mut MetaSlotStorage, Tracked(perm): Tracked<&'a mut ()>, ) -> &'a mut Self

proof fn from_to_repr(self, perm: ())

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

proof fn to_repr_wf(self, perm: ())

type ReprPerm = ()

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