ostd::mm::frame::linked_list

Struct Link

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

Expand description

A link in the linked list.

Fields§

§next: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>§prev: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>§meta: M

Implementations§

Source §

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

Source

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

Creates a new linked list metadata.

Trait Implementations§

Source §

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

{ true }

Source §

type Owner = LinkOwner

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

Source §

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

Source §

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,
    }
}

Source §

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,
            },
        },
    )
}

Source §

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

Source §

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),
            }
        }
    }
}