Struct PageTablePageMeta 

pub struct PageTablePageMeta<C: PageTableConfig> {
    pub nr_children: PCell<u16>,
    pub stray: PCell<bool>,
    pub level: PagingLevel,
    pub lock: PAtomicU8,
    pub _phantom: PhantomData<C>,
}

The metadata of any kinds of page table pages. Make sure the the generic parameters don’t effect the memory layout.

Fields

nr_children: PCell<u16>

The number of valid PTEs. It is mutable if the lock is held.

stray: PCell<bool>

If the page table is detached from its parent.

A page table can be detached from its parent while still being accessed, since we use a RCU scheme to recycle page tables. If this flag is set, it means that the parent is recycling the page table.

level: PagingLevel

The level of the page table page. A page table page cannot be referenced by page tables of different levels.

lock: PAtomicU8

The lock for the page table page.

_phantom: PhantomData<C>

Implementations

impl<C: PageTableConfig> PageTablePageMeta<C>

pub exec fn new(level: PagingLevel) -> Self

pub open spec fn walk_pte_at_view(view: MemView, c: usize) -> C::E

{ ostd_pod::decode_pod::<C::E>(view.read_bytes(c, core::mem::size_of::<C::E>())) }

The PTE value that read_once::<C::E> would produce at cursor c against the given memory view. Linked to read_once via pod_bytes(v) == read_view.read_bytes(...) (strengthened ensures) and the checked byte-decoding model.

pub open spec fn walk_coverage_at(self, view: MemView, dom: Set<int>, c: usize) -> bool

{
    let pte = Self::walk_pte_at_view(view, c);
    pte.is_present() && !pte.is_last(self.level)
        ==> dom.contains(frame_to_index(pte.paddr()))
}

Single-cursor projection of [walk_coverage_from_view]. Extracting the forall body to a named predicate lets the body invoke [lemma_coverage_at] for one specific c instead of relying on auto-trigger matching across the loop invariant’s forall|c|.

pub proof fn lemma_coverage_at( self, reader: VmReader<'_, Infallible>, view: MemView, dom: Set<int>, c: usize, )

requires

self.walk_coverage_from_view(reader, view, dom),

reader.cursor.vaddr <= c,

c + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),

(c - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,

ensures

self.walk_coverage_at(view, dom, c),

Instantiate [walk_coverage_from_view]’s forall at one cursor.

pub proof fn lemma_uniqueness_at_pair( self, reader: VmReader<'_, Infallible>, view: MemView, c1: usize, c2: usize, )

requires

self.walk_uniqueness_from_view(reader, view),

reader.cursor.vaddr <= c1,

c1 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),

(c1 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,

reader.cursor.vaddr <= c2,

c2 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),

(c2 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,

c1 != c2,

Self::walk_pte_at_view(view, c1).is_present(),

!Self::walk_pte_at_view(view, c1).is_last(self.level),

Self::walk_pte_at_view(view, c2).is_present(),

!Self::walk_pte_at_view(view, c2).is_last(self.level),

ensures

Self::walk_pte_at_view(view, c1).paddr() != Self::walk_pte_at_view(view, c2).paddr(),

Instantiate [walk_uniqueness_from_view]’s forall at one cursor pair.

pub open spec fn walk_coverage_from_view( self, reader: VmReader<'_, Infallible>, view: MemView, dom: Set<int>, ) -> bool

{
    forall |c: usize| {
        reader.cursor.vaddr <= c
            && c + core::mem::size_of::<C::E>()
                <= reader.cursor.vaddr + reader.remain_spec()
            && (c - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0
            ==> {
                let pte = Self::walk_pte_at_view(view, c);
                pte.is_present() && !pte.is_last(self.level)
                    ==> dom.contains(frame_to_index(pte.paddr()))
            }
    }
}

Caller-side dom-membership obligation: every present non-last PTE position in the walk (over view) has its child-frame index in dom. Phrased over a frozen (view, dom) pair so the body can carry it as a loop invariant against an entry-state snapshot while vm_io_owner advances per iteration.

pub open spec fn walk_uniqueness_from_view( self, reader: VmReader<'_, Infallible>, view: MemView, ) -> bool

{
    forall |c1: usize, c2: usize| {
        reader.cursor.vaddr <= c1
            && c1 + core::mem::size_of::<C::E>()
                <= reader.cursor.vaddr + reader.remain_spec()
            && (c1 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0
            && reader.cursor.vaddr <= c2
            && c2 + core::mem::size_of::<C::E>()
                <= reader.cursor.vaddr + reader.remain_spec()
            && (c2 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0
            && c1 != c2
            ==> {
                let pte1 = Self::walk_pte_at_view(view, c1);
                let pte2 = Self::walk_pte_at_view(view, c2);
                pte1.is_present() && !pte1.is_last(self.level) && pte2.is_present()
                    && !pte2.is_last(self.level) ==> pte1.paddr() != pte2.paddr()
            }
    }
}

Caller-side uniqueness obligation: distinct cursor positions with present non-last PTEs (in view) map to distinct paddrs.

pub open spec fn child_perms_embedding( regions: MetaRegionOwners, excluded: Set<int>, ) -> bool

{
    forall |paddr: crate::mm::Paddr| {
        regions.slots.dom().contains(frame_to_index(paddr))
            && !excluded.contains(frame_to_index(paddr))
            ==> {
                let idx = frame_to_index(paddr);
                let so = regions.slot_owners[idx];
                &&& <Frame<Self>>::from_raw_requires(regions, paddr)
                &&& 0 < so.ref_count() <= REF_COUNT_MAX
                &&& so.storage_perm().is_init()
                &&& so.ref_count() == 1
                    ==> {
                        &&& so.in_list_perm.value() == 0
                        &&& so.paths_in_pt.is_empty()

                    }

            }
    }
}

Caller-side shape obligation: every paddr in child_perms.dom() has a slot perm matching the shape from_raw + VerifiedDrop::drop expect (init, alignment, refcount within bounds, last-reference shape when refcount == 1).

impl<C: PageTableConfig> PageTablePageMeta<C>

pub open spec fn into_spec(self) -> StoredPageTablePageMeta

{
    StoredPageTablePageMeta {
        nr_children: self.nr_children,
        stray: self.stray,
        level: self.level,
        lock: self.lock,
    }
}

pub exec fn into(self) -> res : StoredPageTablePageMeta

ensures

res == self.into_spec(),

Trait Implementations

impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C>

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

{
    &&& reader.inv()
    &&& reader.wf(vm_io_owner)
    &&& reader.remain_spec() >= crate::specs::arch::PAGE_SIZE
    &&& reader.cursor.vaddr % core::mem::align_of::<C::E>() == 0
    &&& vm_io_owner.inv()
    &&& vm_io_owner.read_view_initialized()
    &&& regions.inv()
    &&& Self::child_perms_embedding(regions, vstd::set::Set::empty())
    &&& self
        .walk_coverage_from_view(reader, vm_io_owner.read_view_of(), regions.slots.dom())
    &&& self.walk_uniqueness_from_view(reader, vm_io_owner.read_view_of())

}

Caller invariants the PT-node on_drop body relies on:

• Reader well-formedness + vm_io_owner matching + read view initialized + at least PAGE_SIZE bytes remaining for the PT-node walk.
• Global region table invariant.
• Embedding ([child_perms_embedding]): for every paddr in child_perms.dom(), the slot and perm match from_raw / VerifiedDrop::drop’s expected shape.
• Walk coverage ([walk_coverage_from_view]): for every present non-last PTE in the page bytes, frame_to_index(pte.paddr()) ∈ child_perms.dom().
• Walk uniqueness ([walk_uniqueness_from_view]): distinct PTE positions with present non-last PTEs have distinct paddrs.

Coverage and uniqueness retain the memory-safety premises needed by the trusted destructor body, without storing item permissions in VmIoOwner.

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

Drops the children of a page-table node.

The permission handoff for recursively destroying page-table entries is not modeled yet. Keep that trusted boundary local to this destructor; VmIoOwner only supplies the memory view used by reader.

exec fn is_untyped(&self) -> bool

uninterp spec fn vtable_ptr(&self) -> usize

impl<C: PageTableConfig> OwnerOf for PageTablePageMeta<C>

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

{
    &&& self.nr_children.id() == owner.nr_children.id()
    &&& self.stray.id() == owner.stray.id()
    &&& 0 <= owner.nr_children.value() <= NR_ENTRIES

}

type Owner = PageMetaOwner

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

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.