Struct Metadata AsLink &nbsp; Copy item path

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

pub exec fn cast_to_metadata( ptr: ReprPtr<MetaSlot, Self>, ) -> res : ReprPtr<MetaSlot, Metadata<Link<M>>>

ensures

res.addr() == ptr.addr(),

res.ptr == ptr.ptr,

pub exec fn cast_from_metadata( ptr: ReprPtr<MetaSlot, Metadata<Link<M>>>, ) -> res : ReprPtr<MetaSlot, Self>

ensures

res.addr() == ptr.addr(),

res.ptr == ptr.ptr,

pub proof fn cast_points_to_metadata(tracked perm: PointsTo<MetaSlot, MetadataAsLink<M>>, ) -> tracked result : PointsTo<MetaSlot, Metadata<Link<M>>>

ensures

result.addr() == perm.addr(),

result.is_init() == perm.is_init(),

result.points_to.pptr() == perm.points_to.pptr(),

pub proof fn cast_points_to_as_link(tracked perm: PointsTo<MetaSlot, Metadata<Link<M>>>, ) -> tracked result : PointsTo<MetaSlot, MetadataAsLink<M>>

ensures

result.addr() == perm.addr(),

result.is_init() == perm.is_init(),

result.points_to.pptr() == perm.points_to.pptr(),

Trait Implementations§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> From<Metadata<Link<M>>> for MetadataAsLink<M>

exec fn from(m: Metadata<Link<M>>) -> Self

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> From<MetadataAsLink<M>> for Metadata<Link<M>>

exec fn from(m: MetadataAsLink<M>) -> Self

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> FromSpecImpl<Metadata<Link<M>>> for MetadataAsLink<M>

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(m: Metadata<Link<M>>) -> MetadataAsLink<M>

{
    MetadataAsLink {
        metadata: m.metadata.meta,
        next: match m.metadata.next {
            Some(repr_ptr) => Some(repr_ptr.ptr),
            None => None,
        },
        prev: match m.metadata.prev {
            Some(repr_ptr) => Some(repr_ptr.ptr),
            None => None,
        },
        ref_count: m.ref_count,
        vtable_ptr: m.vtable_ptr,
        in_list: m.in_list,
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> FromSpecImpl<MetadataAsLink<M>> for Metadata<Link<M>>

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(m: MetadataAsLink<M>) -> Metadata<Link<M>>

{
    Metadata {
        metadata: Link {
            next: match m.next {
                Some(pptr) => {
                    Some(ReprPtr {
                        addr: pptr.addr(),
                        ptr: pptr,
                        _T: PhantomData,
                    })
                }
                None => None,
            },
            prev: match m.prev {
                Some(pptr) => {
                    Some(ReprPtr {
                        addr: pptr.addr(),
                        ptr: pptr,
                        _T: PhantomData,
                    })
                }
                None => None,
            },
            meta: m.metadata,
        },
        ref_count: m.ref_count,
        vtable_ptr: m.vtable_ptr,
        in_list: m.in_list,
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlot> for MetadataAsLink<M>

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

{
    &&& <Metadata<Link<M>> as Repr<MetaSlot>>::wf(r, perm)
    &&& ({
        let md = <Metadata<Link<M>> as Repr<MetaSlot>>::from_repr_spec(r, perm);
        &&& (md.metadata.next matches Some(next) ==> next.addr == next.ptr.addr())
        &&& (md.metadata.prev matches Some(prev) ==> prev.addr == prev.ptr.addr())

    })

}

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

{
    <Metadata<
        Link<M>,
    > as Repr<
        MetaSlot,
    >>::to_repr_spec(
        <Metadata<Link<M>> as FromSpec<MetadataAsLink<M>>>::from_spec(self),
        perm,
    )
}

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

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

{
    <MetadataAsLink<
        M,
    > as FromSpec<
        Metadata<Link<M>>,
    >>::from_spec(<Metadata<Link<M>> as Repr<MetaSlot>>::from_repr_spec(r, perm))
}

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

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

type Perm = MetadataInnerPerms

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

Auto Trait Implementations§

impl<M> Freeze for MetadataAsLink<M>
where M: Freeze,

impl<M> !RefUnwindSafe for MetadataAsLink<M>

impl<M> Send for MetadataAsLink<M>
where M: Send,

impl<M> Sync for MetadataAsLink<M>
where M: Sync,

impl<M> Unpin for MetadataAsLink<M>
where M: Unpin,

impl<M> UnwindSafe for MetadataAsLink<M>
where M: UnwindSafe,

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