Struct EntryOwner 

pub struct EntryOwner<C: PageTableConfig> {
    pub kind: EntryOwnerKind<C>,
    pub path: TreePath<NR_ENTRIES>,
    pub parent_level: PagingLevel,
}

Fields

kind: EntryOwnerKind<C>

path: TreePath<NR_ENTRIES>

parent_level: PagingLevel

Implementations

impl<C: PageTableConfig> EntryOwner<C>

pub open spec fn into_pte_owner_spec(self) -> EntryOwner<C>

{ self }

pub open spec fn from_pte_owner_spec(self) -> EntryOwner<C>

{ self }

pub open spec fn pte_invariants(self, pte: C::E, regions: MetaRegionOwners) -> bool

{
    &&& self.inv()
    &&& regions.inv()
    &&& self.match_pte(pte, self.parent_level)
    &&& self.metaregion_sound(regions)

}

This is equivalent to the other invariants relations, combining the inv predicates for each object and the well-formedness relations between them.

impl<C: PageTableConfig> EntryOwner<C>

pub open spec fn is_node(self) -> bool

{ self.kind is Node }

pub open spec fn is_frame(self) -> bool

{ self.kind is Frame }

pub open spec fn is_absent(self) -> bool

{ self.kind is Absent }

pub open spec fn is_borrowed(self) -> bool

{ self.kind is Borrowed }

pub open spec fn node(self) -> NodeOwner<C>

{ self.kind->Node_0 }

pub open spec fn frame(self) -> FrameEntryOwner<C>

{ self.kind->Frame_0 }

pub open spec fn frame_permission(self) -> Option<C::Perm>

recommends

self.is_frame(),

{ self.frame().permission }

pub open spec fn frame_is_tracked(self) -> bool

recommends

self.is_frame(),

{ self.frame_permission() is Some }

pub open spec fn borrowed(self) -> Set<Mapping>

{ self.kind->Borrowed_0 }

pub open spec fn new_absent(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> Self

{
    EntryOwner {
        kind: EntryOwnerKind::Absent,
        path,
        parent_level,
    }
}

pub open spec fn new_frame( paddr: Paddr, path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, prop: PageProperty, permission: Option<C::Perm>, ) -> Self

{
    EntryOwner {
        kind: EntryOwnerKind::Frame(FrameEntryOwner {
            mapped_pa: paddr,
            prop,
            permission,
        }),
        path,
        parent_level,
    }
}

pub open spec fn new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> Self

{
    EntryOwner {
        kind: EntryOwnerKind::Node(node),
        path,
        parent_level: (node.level() + 1) as PagingLevel,
    }
}

pub proof fn tracked_new_absent( path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, ) -> tracked Self

returns

Self::new_absent(path, parent_level),

pub proof fn tracked_take_node(tracked &mut self) -> tracked res : NodeOwner<C>

requires

old(self).kind is Node,

ensures

res == old(self).node(),

*final(self)
    == (EntryOwner {
        kind: EntryOwnerKind::Absent,
        ..*old(self)
    }),

pub proof fn tracked_put_node(tracked &mut self, tracked node: NodeOwner<C>)

ensures

*final(self)
    == (EntryOwner {
        kind: EntryOwnerKind::Node(node),
        ..*old(self)
    }),

pub proof fn tracked_borrow_node(tracked &self) -> tracked res : &NodeOwner<C>

requires

self.kind is Node,

ensures

*res == self.node(),

pub proof fn tracked_borrow_mut_node(tracked &mut self) -> tracked res : &mut NodeOwner<C>

requires

old(self).kind is Node,

ensures

*res == old(self).node(),

*final(self)
    == (EntryOwner {
        kind: EntryOwnerKind::Node(*final(res)),
        ..*old(self)
    }),

pub proof fn tracked_set_frame_prop(tracked &mut self, prop: PageProperty)

requires

old(self).kind is Frame,

ensures

*final(self)
    == (EntryOwner {
        kind: EntryOwnerKind::Frame(FrameEntryOwner {
            prop,
            ..old(self).frame()
        }),
        ..*old(self)
    }),

pub proof fn tracked_take_frame_permission(tracked &mut self) -> tracked res : Option<C::Perm>

requires

old(self).is_frame(),

ensures

res == old(self).frame_permission(),

*final(self)
    == (EntryOwner {
        kind: EntryOwnerKind::Frame(FrameEntryOwner {
            permission: None,
            ..old(self).frame()
        }),
        ..*old(self)
    }),

pub proof fn tracked_put_frame_permission(tracked &mut self, tracked permission: Option<C::Perm>)

requires

old(self).is_frame(),

old(self).frame_permission() is None,

ensures

*final(self)
    == (EntryOwner {
        kind: EntryOwnerKind::Frame(FrameEntryOwner {
            permission,
            ..old(self).frame()
        }),
        ..*old(self)
    }),

pub proof fn tracked_new_frame( paddr: Paddr, path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, prop: PageProperty, tracked permission: Option<C::Perm>, ) -> tracked Self

returns

Self::new_frame(paddr, path, parent_level, prop, permission),

pub broadcast proof fn axiom_frame_is_tracked_iff_not_mmio(entry: Self)

requires

entry.is_frame(),

entry.inv_base(),

ensures

#[trigger] entry.frame_is_tracked()
    != crate::specs::mm::frame::meta_owners::is_mmio_paddr(entry.frame().mapped_pa),

The frame’s is_tracked flag is pinned to its paddr’s range membership: tracked frames map regular RAM (non-MMIO paddrs); untracked frames map MMIO. Combined with axiom_mmio_usage_iff_mmio_paddr, this lets proofs translate between the derived frame trackedness and usage == MMIO on the corresponding meta slot.

pub proof fn tracked_new_untracked_frame( paddr: Paddr, parent_level: PagingLevel, prop: PageProperty, ) -> tracked res : Self

requires

valid_frame_paddr(paddr),

1 <= parent_level < NR_LEVELS,

paddr % page_size::<PagingConsts>(parent_level) == 0,

paddr + page_size::<PagingConsts>(parent_level) <= MAX_PADDR,

C::raw_item_well_formed((paddr, parent_level, prop, Tracked(None))),

C::E::new_page_req(paddr, parent_level, prop),

ensures

res.is_frame(),

res.frame().mapped_pa == paddr,

res.frame().prop == prop,

!res.frame_is_tracked(),

res.parent_level == parent_level,

res.path.inv(),

res.inv_base(),

crate::mm::page_table::Child::<C>::Frame(paddr, parent_level, prop).wf(res),

Creates a ghost entry owner for mapping an untracked (device memory) frame. Unlike new_frame, this does not consume a slot permission from the meta region, since device memory PAs are outside the tracked frame allocator. The actual mapping correctness is guaranteed by the caller’s unsafe contract.

The requires reflect properties established by collect_largest_pages and the page-table configuration model, allowing this checked constructor to build an invariant-safe, untracked entry owner.

pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool

{
    &&& valid_frame_paddr(pte.paddr())
    &&& !pte.is_present()
        ==> {
            &&& self.is_absent()
            &&& parent_level > 1 ==> !pte.is_last(parent_level)

        }
    &&& pte.is_present() && !pte.is_last(parent_level)
        ==> {
            &&& self.is_node()
            &&& meta_to_frame(self.node().slot_vaddr()) == pte.paddr()

        }
    &&& pte.is_present() && pte.is_last(parent_level)
        ==> {
            &&& self.is_frame()
            &&& self.frame().mapped_pa == pte.paddr()
            &&& self.frame().prop == pte.prop()

        }

}

pub open spec fn borrowed_match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool

{
    &&& self.is_borrowed()
    &&& valid_frame_paddr(pte.paddr())
    &&& pte.is_present()
    &&& !pte.is_last(parent_level)

}

PTE-shape constraint for a borrowed / translation-only entry. The PTE must be a node-PTE (present and non-leaf at parent_level), since the borrowed sub-table is accessed only via the MMU walk. Unlike [match_pte], we do not pin the PTE’s target paddr to any owned NodeOwner — the sub-table is owned by a different page-table configuration and the embedding doesn’t track its address here.

pub proof fn last_pte_implies_frame_match(self, pte: C::E, parent_level: PagingLevel)

requires

self.inv(),

self.match_pte(pte, parent_level),

1 < parent_level,

pte.is_last(parent_level),

ensures

self.is_frame(),

self.frame().mapped_pa == pte.paddr(),

self.frame().prop == pte.prop(),

pub proof fn huge_frame_split_child_at(self, regions: MetaRegionOwners, idx: usize)

requires

self.inv(),

self.is_frame(),

regions.inv(),

1 < self.parent_level < NR_LEVELS,

idx < NR_ENTRIES,

ensures

self.frame().mapped_pa
    + idx * page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel) < MAX_PADDR,

((self.frame().mapped_pa
    + idx * page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel)) as Paddr)
    % page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel) == 0,

((self.frame().mapped_pa
    + idx * page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel)) as Paddr)
    + page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel) <= MAX_PADDR,

((self.frame().mapped_pa
    + idx * page_size::<PagingConsts>((self.parent_level - 1) as PagingLevel)) as Paddr)
    % PAGE_SIZE == 0,

pub proof fn frame_sub_pages_valid_preserved_at_own_slot( self, r0: MetaRegionOwners, r1: MetaRegionOwners, )

requires

self.inv(),

r0.inv(),

self.is_frame(),

self.parent_level <= NR_LEVELS,

self.frame_sub_pages_valid(r0),

r0.slots == r1.slots,

r0.slot_owners.dom() =~= r1.slot_owners.dom(),

forall |i: int| {
    i != frame_to_index(self.meta_slot_paddr()->0) && r0.slot_owners.contains_key(i)
        ==> r0.slot_owners[i] == r1.slot_owners[i]
},

ensures

self.frame_sub_pages_valid(r1),

Helper: sub-page validity is preserved when the only slot that changed is the frame’s own slot (and slots map and other slot owners are unchanged).

pub open spec fn frame_sub_pages_valid(self, regions: MetaRegionOwners) -> bool

{
    self.is_frame() && self.parent_level > 1
        ==> {
            let pa = self.frame().mapped_pa;
            let nr_pages = page_size::<PagingConsts>(self.parent_level) / PAGE_SIZE;
            forall |j: usize| {
                0 < j < nr_pages
                    ==> {
                        let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
                        &&& regions.slots.contains_key(sub_idx)
                        &&& self.frame_is_tracked()
                            ==> {
                                &&& regions.ref_count(sub_idx) != REF_COUNT_UNUSED
                                &&& regions.ref_count(sub_idx) > 0
                                &&& regions.ref_count(sub_idx) <= REF_COUNT_MAX

                            }

                    }
            }
        }
}

Sub-page slot validity for huge frames (fine-grained: all 4KB pages within).

When a frame at this entry has parent_level > 1, it is a huge page covering page_size(parent_level) bytes. Every 4KB sub-page within this range (excluding the j = 0 case which coincides with the frame’s own slot) must be allocated (in the free pool) with rc != UNUSED.

The fine-grained form (over j * PAGE_SIZE rather than j * page_size(L-1)) is what enables the recursive split case in split_if_mapped_huge: when splitting a 1GB frame into 2MB sub-frames, each 2MB sub-frame’s own sub-page validity (over its 511 4KB sub-sub-pages) follows from the 1GB frame’s fine-grained validity over the corresponding subrange of indices.

pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool

{
    if self.is_node() {
        let idx = frame_to_index(self.meta_slot_paddr()->0);
        &&& regions.ref_count(idx) != REF_COUNT_UNUSED
        &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
        &&& regions.slot_owners[idx].slot_vaddr == self.node().slot_vaddr()
        &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
        &&& regions.slot_owners[idx].paths_in_pt == set![self.path]
        &&& self.node().metaregion_sound_node(regions)

    } else if self.is_frame() {
        let idx = frame_to_index(self.meta_slot_paddr()->0);
        &&& regions.slots.contains_key(idx)
        &&& regions.slots[idx].addr() == index_to_meta(idx)
        &&& regions.slots[idx].is_init()
        &&& regions.slots[idx].value().wf(regions.slot_owners[idx])
        &&& regions.slot_owners[idx].usage !is PageTable
        &&& regions.slot_owners[idx].usage !is MMIO
            ==> {
                &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX

            }
        &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)
        &&& self.frame_sub_pages_valid(regions)
        &&& C::perm_well_formed_with_region(
            self.frame().mapped_pa,
            Tracked(self.frame_permission()),
            regions,
        )

    } else {
        true
    }
}

pub proof fn lemma_active_entry_not_in_free_pool( entry: Self, regions: MetaRegionOwners, free_idx: int, )

requires

regions.inv(),

entry.inv(),

entry.is_node(),

entry.metaregion_sound(regions),

regions.slots.contains_key(free_idx),

regions.ref_count(free_idx) == REF_COUNT_UNUSED,

ensures

frame_to_index(entry.meta_slot_paddr()->0) != free_idx,

An active page-table node cannot occupy a metadata slot whose refcount is still REF_COUNT_UNUSED.

pub open spec fn meta_slot_paddr(self) -> Option<Paddr>

{
    if self.is_node() {
        Some(meta_to_frame(self.node().slot_vaddr()))
    } else if self.is_frame() {
        Some(self.frame().mapped_pa)
    } else {
        None
    }
}

pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool

{
    self.meta_slot_paddr() is Some
        ==> (other.meta_slot_paddr() is Some
            ==> self.meta_slot_paddr()->0 != other.meta_slot_paddr()->0)
}

pub proof fn metaregion_sound_slot_owners_only( self, r0: MetaRegionOwners, r1: MetaRegionOwners, )

requires

self.inv(),

self.metaregion_sound(r0),

r0.slot_owners == r1.slot_owners,

forall |k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),

forall |k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],

ensures

self.metaregion_sound(r1),

metaregion_sound transfers when slot_owners matches and slots is a superset. For nodes: only slot_owners matters. For frames: slots.contains_key and slots[idx] must be preserved, which holds when slots is a superset with values unchanged.

pub proof fn metaregion_sound_frame_prop_changed( self, other: Self, regions: MetaRegionOwners, )

requires

regions.inv(),

self.inv(),

other.inv(),

self.is_frame(),

other.is_frame(),

self.metaregion_sound(regions),

other.frame().mapped_pa == self.frame().mapped_pa,

other.path == self.path,

other.parent_level == self.parent_level,

other.frame_permission() == self.frame_permission(),

other.frame_is_tracked() == self.frame_is_tracked(),

ensures

other.metaregion_sound(regions),

Changing only a leaf PTE’s page properties preserves its relationship to the metadata region. The counting permission, physical address and page-table path remain unchanged.

pub proof fn metaregion_sound_one_slot_changed( self, r0: MetaRegionOwners, r1: MetaRegionOwners, changed_idx: int, )

requires

self.inv(),

self.metaregion_sound(r0),

forall |i: int| i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],

r0.slot_owners.dom() =~= r1.slot_owners.dom(),

forall |k: int| r0.slots.contains_key(k) ==> #[trigger] r1.slots.contains_key(k),

forall |k: int| r0.slots.contains_key(k) ==> r0.slots[k] == #[trigger] r1.slots[k],

self.meta_slot_paddr() is Some
    ==> frame_to_index(self.meta_slot_paddr()->0) != changed_idx,

self.is_frame() && self.parent_level > 1
    ==> {
        let pa = self.frame().mapped_pa;
        let nr_pages = page_size::<PagingConsts>(self.parent_level) / PAGE_SIZE;
        forall |j: usize| {
            0 < j < nr_pages
                ==> {
                    let sub_idx = #[trigger]
                    frame_to_index((pa + j * PAGE_SIZE) as usize);
                    sub_idx != changed_idx || r1.slot_owners[sub_idx].usage is MMIO
                        || (r1.slots.contains_key(sub_idx)
                            && r1.ref_count(sub_idx) != REF_COUNT_UNUSED
                            && r1.ref_count(sub_idx) > 0
                            && r1.ref_count(sub_idx) <= REF_COUNT_MAX)
                }
        }
    },

ensures

self.metaregion_sound(r1),

If metaregion_sound(r0) holds and r1 differs from r0 only at one slot index that this entry does not reference, then metaregion_sound(r1) also holds.

impl<C: PageTableConfig> EntryOwner<C>

pub open spec fn inv_base(self) -> bool

{
    &&& self.is_node()
        ==> {
            &&& self.node().inv()
            &&& self.parent_level == self.node().level() + 1

        }
    &&& self.is_frame()
        ==> {
            &&& 1 <= self.parent_level < NR_LEVELS
            &&& valid_frame_paddr(self.frame().mapped_pa)
            &&& self.frame().mapped_pa % page_size::<PagingConsts>(self.parent_level)
                == 0
            &&& self.frame().mapped_pa + page_size::<PagingConsts>(self.parent_level)
                <= MAX_PADDR
            &&& C::raw_item_well_formed((
                self.frame().mapped_pa,
                self.parent_level,
                self.frame().prop,
                Tracked(self.frame_permission()),
            ))
            &&& C::E::new_page_req(
                self.frame().mapped_pa,
                self.parent_level,
                self.frame().prop,
            )

        }
    &&& self.is_borrowed() ==> { true }
    &&& self.path.inv()

}

Structural invariant of an entry owner. This is the whole of inv(), and is also used directly by Child::invariants.

Trait Implementations

impl<C: PageTableConfig> Inv for EntryOwner<C>

open spec fn inv(self) -> bool

{ self.inv_base() }

impl<C: PageTableConfig, const L: usize> TreeNodeValue<L> for EntryOwner<C>

open spec fn default(lv: nat) -> Self

{
    Self {
        kind: EntryOwnerKind::Absent,
        path: TreePath::new(Seq::empty()),
        parent_level: (INC_LEVELS - lv) as PagingLevel,
    }
}

proof fn lemma_default_preserves_inv()

open spec fn la_inv(self, lv: nat) -> bool

{ self.is_node() ==> lv < L - 1 }

proof fn lemma_default_preserves_la_inv()

open spec fn rel_children(self, i: int, child: Option<Self>) -> bool

{ true }

proof fn lemma_default_preserves_rel_children(self, lv: nat)