ostd::specs::mm::frame::meta_owners

Struct Metadata

pub struct Metadata<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
    pub metadata: M,
    pub ref_count: u64,
    pub vtable_ptr: MemContents<usize>,
    pub in_list: u64,
}

Fields§

§metadata: M§ref_count: u64§vtable_ptr: MemContents<usize>§in_list: u64

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M>

Source

pub uninterp spec fn metadata_from_inner_perms(perm: PointsTo<MetaSlotStorage>) -> M

The metadata value is an abstract function of the inner permissions, since extracting M from MetaSlotStorage requires M::Perm which is not stored in MetadataInnerPerms.

Source

pub uninterp spec fn inner_perms_from_metadata( m: M, base: PointsTo<MetaSlotStorage>, ) -> PointsTo<MetaSlotStorage>

Inverse of [metadata_from_inner_perms]: given an M and a base storage permission, produce a new permission with the same cell id whose metadata_from_inner_perms interpretation yields m.

Source

pub proof fn metadata_perms_inverse(m: M, base: PointsTo<MetaSlotStorage>)

ensures

Self::metadata_from_inner_perms(Self::inner_perms_from_metadata(m, base)) == m,

Self::inner_perms_from_metadata(m, base).id() == base.id(),

Self::inner_perms_from_metadata(m, base).is_init(),

Axiomatic roundtrip laws for the metadata ↔ storage-perm pair. The conversion is a transmute / reinterpret at exec level, so these laws live at the cast_ptr trust boundary.

Source

pub proof fn inner_perms_from_metadata_roundtrip(perm: PointsTo<MetaSlotStorage>)

ensures

Self::inner_perms_from_metadata(Self::metadata_from_inner_perms(perm), perm) == perm,

Source

pub proof fn switch_perm_to_inner_perms_from_metadata(tracked perm: &mut PointsTo<MetaSlotStorage>, m: M, )

requires

old(perm).is_init(),

ensures

*final(perm) == Self::inner_perms_from_metadata(m, *old(perm)),

Proof-level companion: given a storage perm that has been initialized with some (arbitrary) MetaSlotStorage value, advance it to the spec form inner_perms_from_metadata(m, *old(perm)). This is the proof-side step for writing m into the cell — it bridges the raw PCell::write of a MetaSlotStorage value to the spec encoding. Combined with Self::metadata_perms_inverse, it lets a real exec write discharge the metadata_from_inner_perms == m post.

Source

pub exec fn write_metadata_into_storage( cell: &PCell<MetaSlotStorage>, verus_tmp_perm: Tracked<&mut PointsTo<MetaSlotStorage>>, metadata: M, )

requires

cell.id() == old(perm).id(),

ensures

final(perm).id() == old(perm).id(),

final(perm).is_init(),

Self::metadata_from_inner_perms(*final(perm)) == metadata,

Exec-level write primitive: writing metadata into the storage cell yields a perm whose metadata_from_inner_perms interpretation is exactly metadata.

Trait Implementations§

Source §

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

Source §

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

Source §

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

Source §

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

Source §

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

Source §

open spec fn obeys_from_spec() -> bool

{ true }

Source §

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

Source §

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

Source §

open spec fn obeys_from_spec() -> bool

{ true }

Source §

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

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

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M>

Source §

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

{
    &&& perm.storage.id() == r.storage.id()
    &&& perm.ref_count.id() == r.ref_count.id()
    &&& perm.vtable_ptr.pptr() == r.vtable_ptr
    &&& perm.in_list.id() == r.in_list.id()

}

Source §

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

{
    let new_perm = MetadataInnerPerms {
        storage: Self::inner_perms_from_metadata(self.metadata, perm.storage),
        ref_count: perm_u64_with(perm.ref_count, self.ref_count),
        vtable_ptr: pptr_usize_with(perm.vtable_ptr, self.vtable_ptr),
        in_list: perm_u64_with(perm.in_list, self.in_list),
    };
    (meta_slot_from_perm(new_perm), new_perm)
}

Source §

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

Source §

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

{
    Metadata {
        metadata: Self::metadata_from_inner_perms(perm.storage),
        ref_count: perm.ref_count.value(),
        vtable_ptr: perm.vtable_ptr.mem_contents(),
        in_list: perm.in_list.value(),
    }
}

Source §