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

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

Creates an untracked physical mapping without counted metadata ownership. The mapped address may belong to ordinary RAM or MMIO. 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 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 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])
        &&& self.frame_is_tracked()
            ==> {
                &&& regions.slot_owners[idx].usage !is PageTable
                &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
                &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)

            }
        &&& 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.is_node() || (self.is_frame() && self.frame_is_tracked()))
        && (other.is_node() || (other.is_frame() && other.frame_is_tracked()))
        ==> {
            self.meta_slot_paddr() is Some
                ==> (other.meta_slot_paddr() is Some
                    ==> self.meta_slot_paddr()->0 != other.meta_slot_paddr()->0)
        }
}

Physical-slot exclusion for owning entries; raw mappings impose no exclusion.

pub proof fn lemma_untracked_frame_metaregion_sound(self, regions: MetaRegionOwners)

requires

self.inv(),

self.is_frame(),

!self.frame_is_tracked(),

regions.inv(),

ensures

self.metaregion_sound(regions),

An untracked mapping needs no counted ownership of its physical slot.

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 lemma_metaregion_sound_frame_paths_changed( self, r0: MetaRegionOwners, r1: MetaRegionOwners, )

requires

self.inv(),

self.metaregion_sound(r0),

r0.inv(),

r1.inv(),

r0.slots == r1.slots,

forall |i: int| {
    r0.slot_owners.contains_key(i)
        ==> {
            &&& r1.slot_owners[i].same_permissions(r0.slot_owners[i])
            &&& r1.slot_owners[i].usage == r0.slot_owners[i].usage
            &&& r1.slot_owners[i].slot_vaddr == r0.slot_owners[i].slot_vaddr
            &&& r0.slot_owners[i].paths_in_pt.subset_of(r1.slot_owners[i].paths_in_pt)
            &&& r0.slot_owners[i].usage is PageTable
                ==> r1.slot_owners[i].paths_in_pt == r0.slot_owners[i].paths_in_pt

        }
},

ensures

self.metaregion_sound(r1),

Updating frame paths preserves metadata access and node ownership paths.

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 lemma_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.is_node() || (self.is_frame() && self.frame_is_tracked())
    ==> (self.meta_slot_paddr() is Some
        ==> frame_to_index(self.meta_slot_paddr()->0) != changed_idx),

self.meta_slot_paddr() is Some
    && frame_to_index(self.meta_slot_paddr()->0) == changed_idx ==> r1.inv(),

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.

Trait Implementations

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

open spec fn inv(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.path.inv()

}

Structural invariant of an entry owner.

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)