Struct Link 

pub struct Link<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub next: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
    pub prev: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
    pub meta: M,
}

A link in the linked list.

Fields

next: Option<ReprPtr<MetaSlotStorage, Link<M>>>

prev: Option<ReprPtr<MetaSlotStorage, Link<M>>>

meta: M

Implementations

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

pub const exec fn new(meta: M) -> Self

Creates a new linked list metadata.

Trait Implementations

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

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

{ self.meta.on_drop_pre(reader, regions, vm_io_owner) }

exec fn on_drop( &mut self, reader: &mut VmReader<'_, Infallible>, regions: Tracked<&mut MetaRegionOwners>, vm_io_owner: Tracked<&mut VmIoOwner>, )

exec fn is_untyped(&self) -> bool

uninterp spec fn vtable_ptr(&self) -> usize

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

exec fn deref(&self) -> &Self::Target

type Target = M

The resulting type after dereferencing.

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

exec fn deref_mut(&mut self) -> &mut Self::Target

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

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

{ true }

type Owner = LinkOwner

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

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.