Skip to main content

EntryOwner

ostd::specs::mm::page_table::node::entry_owners

Struct EntryOwner 

Source 
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§

Source§

impl<C: PageTableConfig> EntryOwner<C>

Source

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

{
    if self.is_node() {
        let index = frame_to_index(self.meta_slot_paddr()->0);
        MetaRegionOwners {
            frame_obligations: regions.frame_obligations.insert(index),
            ..regions
        }
    } else {
        regions
    }
}
Source

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

{
    if self.is_node() {
        let index = frame_to_index(self.meta_slot_paddr()->0);
        MetaRegionOwners {
            frame_obligations: regions.frame_obligations.remove(index),
            ..regions
        }
    } else {
        regions
    }
}
Source

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

{ self }
Source

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

{ self }
Source

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.

Source§

impl<C: PageTableConfig> EntryOwner<C>

Source

pub open spec fn is_node(self) -> bool

{ self.kind is Node }
Source

pub open spec fn is_frame(self) -> bool

{ self.kind is Frame }
Source

pub open spec fn is_absent(self) -> bool

{ self.kind is Absent }
Source

pub open spec fn is_borrowed(self) -> bool

{ self.kind is Borrowed }
Source

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

{ self.kind->Node_0 }
Source

pub open spec fn frame(self) -> FrameEntryState

{ self.kind->Frame_0 }
Source

pub open spec fn frame_is_tracked(self) -> bool

recommends
self.is_frame(),
{
    C::tracked(
        C::item_from_raw_spec(
            self.frame().mapped_pa,
            self.parent_level,
            self.frame().prop,
        ),
    )
}
Source

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

{ self.kind->Borrowed_0 }
Source

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

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

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

{
    EntryOwner {
        kind: EntryOwnerKind::Frame(FrameEntryState {
            mapped_pa: paddr,
            prop,
        }),
        path,
        parent_level,
    }
}
Source

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

pub open spec fn new_borrowed( path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, mappings: Set<Mapping>, ) -> Self

{
    EntryOwner {
        kind: EntryOwnerKind::Borrowed(mappings),
        path,
        parent_level,
    }
}

Constructor spec for a translation-only / borrowed entry. See EntryOwner’s borrowed field for semantics.

Source

pub proof fn tracked_new_borrowed( path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, mappings: Set<Mapping>, ) -> tracked Self

returns
Self::new_borrowed(path, parent_level, mappings),
Source

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

returns
Self::new_absent(path, parent_level),
Source

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

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

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

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

requires
self.kind is Node,
ensures
*res == self.node(),
Source

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

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(FrameEntryState {
            prop,
            ..old(self).frame()
        }),
        ..*old(self)
    }),
Source

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

returns
Self::new_frame(paddr, path, parent_level, prop),
Source

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.

Source

pub proof fn tracked_new_node(tracked node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> tracked Self

returns
Self::new_node(node, path),
Source

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(parent_level) == 0,
paddr + page_size(parent_level) <= MAX_PADDR,
C::raw_item_well_formed(paddr, parent_level, prop),
C::E::new_page_req(paddr, parent_level, prop),
!C::tracked(C::item_from_raw_spec(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.

Source

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().meta_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()

        }

}
Source

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.

Source

pub proof fn absent_match_pte(owner: Self, pte: C::E, parent_level: PagingLevel)

requires
owner.is_absent(),
pte == C::E::new_absent_spec(),
valid_frame_paddr(pte.paddr()),
ensures
owner.match_pte(pte, parent_level),

When owner is absent and pte is the absent PTE with valid paddr, match_pte holds.

Source

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

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((self.parent_level - 1) as PagingLevel)
    < MAX_PADDR,
((self.frame().mapped_pa + idx * page_size((self.parent_level - 1) as PagingLevel))
    as Paddr) % page_size((self.parent_level - 1) as PagingLevel) == 0,
((self.frame().mapped_pa + idx * page_size((self.parent_level - 1) as PagingLevel))
    as Paddr) + page_size((self.parent_level - 1) as PagingLevel) <= MAX_PADDR,
((self.frame().mapped_pa + idx * page_size((self.parent_level - 1) as PagingLevel))
    as Paddr) % PAGE_SIZE == 0,
Source

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).

Source

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(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)
                        &&& regions.slot_owners[sub_idx].usage !is MMIO
                            ==> {
                                &&& regions
                                    .slot_owners[sub_idx]
                                    .inner_perms
                                    .ref_count
                                    .value() != REF_COUNT_UNUSED
                                &&& regions
                                    .slot_owners[sub_idx]
                                    .inner_perms
                                    .ref_count
                                    .value() > 0
                                &&& regions
                                    .slot_owners[sub_idx]
                                    .inner_perms
                                    .ref_count
                                    .value() <= 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.

Source

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.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
        &&& 0 < regions.slot_owners[idx].inner_perms.ref_count.value() <= REF_COUNT_MAX
        &&& regions.slot_owners[idx].slot_vaddr == self.node().meta_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
            ==> {
                &&& regions.slot_owners[idx].inner_perms.ref_count.value()
                    != REF_COUNT_UNUSED
                &&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
                &&& regions.slot_owners[idx].inner_perms.ref_count.value()
                    <= REF_COUNT_MAX

            }
        &&& regions.slot_owners[idx].paths_in_pt.contains(self.path)
        &&& self.frame_sub_pages_valid(regions)

    } else {
        true
    }
}
Source

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.slot_owners[free_idx].inner_perms.ref_count.value() == 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.

Source

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

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

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)
}
Source

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.

Source

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(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.slot_owners[sub_idx].inner_perms.ref_count.value()
                                != REF_COUNT_UNUSED
                            && r1.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
                            && r1.slot_owners[sub_idx].inner_perms.ref_count.value()
                                <= 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.

Source

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

requires
self.inv(),
r0.inv(),
self.metaregion_sound(r0),
r0.slots == r1.slots,
r0.slot_owners.dom() =~= r1.slot_owners.dom(),
forall |i: int| i != changed_idx ==> r0.slot_owners[i] == r1.slot_owners[i],
r1.slot_owners[changed_idx].inner_perms == r0.slot_owners[changed_idx].inner_perms,
r1.slot_owners[changed_idx].slot_vaddr == r0.slot_owners[changed_idx].slot_vaddr,
r1.slot_owners[changed_idx].usage == r0.slot_owners[changed_idx].usage,
self.is_node() && self.meta_slot_paddr() is Some
    && frame_to_index(self.meta_slot_paddr()->0) == changed_idx
    ==> r1.slot_owners[changed_idx].paths_in_pt == set![self.path],
self.is_frame() && self.meta_slot_paddr() is Some
    && frame_to_index(self.meta_slot_paddr()->0) == changed_idx
    ==> r1.slot_owners[changed_idx].paths_in_pt.contains(self.path),
self.is_frame() && self.parent_level > 1
    ==> {
        let pa = self.frame().mapped_pa;
        let sub_level = (self.parent_level - 1) as PagingLevel;
        forall |j: int| {
            0 < j < NR_ENTRIES
                ==> {
                    let sub_idx = #[trigger]
                    frame_to_index((pa + j * page_size(sub_level)) as usize);
                    sub_idx != changed_idx
                        || r1.slot_owners[changed_idx].paths_in_pt.is_empty()
                }
        }
    },
ensures
self.metaregion_sound(r1),

metaregion_sound is preserved when only paths_in_pt changes at a slot, slots is unchanged, and the new paths_in_pt is correct for any node at that index.

Source

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

requires
self.meta_slot_paddr() is Some,
self.meta_slot_paddr() == other.meta_slot_paddr(),
regions.slot_owners[frame_to_index(self.meta_slot_paddr()->0)].paths_in_pt
    == set![self.path],
regions.slot_owners[frame_to_index(self.meta_slot_paddr()->0)].paths_in_pt
    == set![other.path],
ensures
self.path == other.path,

Two entries with the same physical address whose paths_in_pt matches their respective paths must have the same path.

Source

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

requires
self.inv(),
r0.inv(),
self.metaregion_sound(r0),
self.meta_slot_paddr() is Some,
r0.slots == r1.slots,
({
    let idx = frame_to_index(self.meta_slot_paddr()->0);
    &&& r1.slot_owners[idx].inner_perms.ref_count.id()
        == r0.slot_owners[idx].inner_perms.ref_count.id()
    &&& r1.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
    &&& r1.slot_owners[idx].inner_perms.ref_count.value() > 0
    &&& r1.slot_owners[idx].inner_perms.ref_count.value() <= REF_COUNT_MAX
    &&& r1.slot_owners[idx].inner_perms.storage
        == r0.slot_owners[idx].inner_perms.storage
    &&& r1.slot_owners[idx].inner_perms.vtable_ptr
        == r0.slot_owners[idx].inner_perms.vtable_ptr
    &&& r1.slot_owners[idx].inner_perms.in_list
        == r0.slot_owners[idx].inner_perms.in_list
    &&& r1.slot_owners[idx].slot_vaddr == r0.slot_owners[idx].slot_vaddr
    &&& r1.slot_owners[idx].paths_in_pt == r0.slot_owners[idx].paths_in_pt
    &&& r1.slot_owners[idx].usage == r0.slot_owners[idx].usage

}),
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.metaregion_sound(r1),

metaregion_sound is preserved when only ref_count.value() changes at this entry’s slot and slots is unchanged.

Source

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

requires
self.is_node(),
other.is_node(),
self.meta_slot_paddr() is Some
    ==> regions.slot_owners[frame_to_index(self.meta_slot_paddr()->0)].paths_in_pt
        == set![self.path],
other.meta_slot_paddr() is Some
    ==> regions.slot_owners[frame_to_index(other.meta_slot_paddr()->0)].paths_in_pt
        == set![other.path],
self.path != other.path,
ensures
self.node().meta_vaddr() != other.node().meta_vaddr(),

Two nodes whose paths_in_pt matches their paths have different addresses if they have different paths.

Source

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

requires
self.is_node(),
other.is_node(),
self.metaregion_sound(regions),
other.metaregion_sound(regions),
self.path.len() != other.path.len(),
ensures
self.meta_slot_paddr_neq(other),

Two node entries with metaregion_sound under the same regions cannot share a meta slot paddr if their paths have different lengths.

For nodes, metaregion_sound requires paths_in_pt == set![path] (singleton). Equal slot indices would force equal singleton sets, hence equal paths — contradicting the length difference.

Source§

impl<C: PageTableConfig> EntryOwner<C>

Source

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(self.parent_level) == 0
            &&& self.frame().mapped_pa + page_size(self.parent_level) <= MAX_PADDR
            &&& C::raw_item_well_formed(
                self.frame().mapped_pa,
                self.parent_level,
                self.frame().prop,
            )
            &&& 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§

Source§

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

Source§

open spec fn inv(self) -> bool

{ self.inv_base() }
Source§

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

Source§

proof fn view_preserves_inv(self)

Source§

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

Source§

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

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

proof fn lemma_default_preserves_inv()

Source§

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

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

proof fn lemma_default_preserves_la_inv()

Source§

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

{ true }
Source§

proof fn lemma_default_preserves_rel_children(self, lv: nat)

Source§

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

Source§

open spec fn view(&self) -> <Self as View>::V

{
    if self.is_frame() {
        let frame = self.frame();
        EntryView::Leaf {
            leaf: LeafPageTableEntryView {
                map_va: vaddr(self.path) as int,
                map_to_pa: frame.mapped_pa as int,
                level: self.path.len() as u8,
                prop: frame.prop,
                phantom: PhantomData,
            },
        }
    } else if self.is_node() {
        let node = self.node();
        EntryView::Intermediate {
            node: IntermediatePageTableEntryView {
                map_va: vaddr(self.path) as int,
                map_to_pa: meta_to_frame(node.meta_vaddr()) as int,
                level: self.path.len() as u8,
                phantom: PhantomData,
            },
        }
    } else {
        EntryView::Absent
    }
}
Source§

type V = EntryView<C>

Auto Trait Implementations§

§

impl<C> Freeze for EntryOwner<C>

§

impl<C> RefUnwindSafe for EntryOwner<C>
where <C as PageTableConfig>::E: RefUnwindSafe,

§

impl<C> Send for EntryOwner<C>

§

impl<C> Sync for EntryOwner<C>

§

impl<C> Unpin for EntryOwner<C>
where <C as PageTableConfig>::E: Unpin,

§

impl<C> UnsafeUnpin for EntryOwner<C>

§

impl<C> UnwindSafe for EntryOwner<C>
where <C as PageTableConfig>::E: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

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<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::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>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::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<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A