ostd/specs/mm/page_table/node/
child.rs

1use vstd::prelude::*;
2use vstd_extra::ownership::*;
3
4use crate::specs::mm::frame::{mapping::meta_to_index, meta_region_owners::MetaRegionOwners};
5
6use crate::arch::mm::PagingConsts;
7use crate::mm::{
8    Paddr, PagingConstsTrait, PagingLevel, Vaddr, frame::*, page_prop::PageProperty, page_table::*,
9};
10
11verus! {
12
13impl<C: PageTableConfig> OwnerOf for Child<C> {
14    type Owner = EntryOwner<C>;
15
16    open spec fn wf(self, owner: Self::Owner) -> bool {
17        match self {
18            Self::PageTable(node) => {
19                &&& owner.is_node()
20                &&& node.ptr.addr() == owner.node().slot_vaddr()
21                &&& node.index() == meta_to_index(node.ptr.addr())
22                &&& node.ptr_inv()
23            },
24            Self::Frame(paddr, level, prop) => {
25                &&& owner.is_frame()
26                &&& owner.frame().mapped_pa == paddr
27                &&& owner.frame().prop == prop
28                &&& level == owner.parent_level
29            },
30            Self::None => owner.is_absent(),
31        }
32    }
33}
34
35impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
36    type Owner = EntryOwner<C>;
37
38    open spec fn wf(self, owner: Self::Owner) -> bool {
39        match self {
40            Self::PageTable(node) => {
41                &&& owner.is_node()
42                &&& node.inner@.ptr.addr() == owner.node().slot_vaddr()
43                &&& node.inner@.ptr_inv()
44                &&& node.inner@.external_meta_wf(owner.node().frame_permission.resource(), ())
45            },
46            Self::Frame(paddr, level, prop) => {
47                &&& owner.is_frame()
48                &&& owner.frame().mapped_pa == paddr
49                &&& owner.frame().prop == prop
50            },
51            Self::None => owner.is_absent(),
52        }
53    }
54}
55
56impl<C: PageTableConfig> Child<C> {
57    pub open spec fn from_pte_spec(
58        pte: C::E,
59        level: PagingLevel,
60        regions: MetaRegionOwners,
61    ) -> Self {
62        if !pte.is_present() {
63            Self::None
64        } else if pte.is_last(level) {
65            Self::Frame(pte.paddr(), level, pte.prop())
66        } else {
67            Self::PageTable(
68                PageTableNode::from_raw_spec(
69                    pte.paddr(),
70                    regions.slots[crate::specs::mm::frame::mapping::frame_to_index(pte.paddr())],
71                    None,
72                ),
73            )
74        }
75    }
76
77    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
78        &&& owner.inv_base()
79        &&& regions.inv()
80        &&& self.wf(owner)
81        &&& match self {
82            Self::Frame(paddr, level, prop) => C::E::new_page_req(paddr, level, prop),
83            _ => true,
84        }
85        &&& owner.metaregion_sound(regions)
86    }
87}
88
89impl<C: PageTableConfig> ChildRef<'_, C> {
90    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
91        &&& owner.inv()
92        &&& regions.inv()
93        &&& self.wf(owner)
94        &&& owner.metaregion_sound(regions)
95    }
96}
97
98impl<C: PageTableConfig> EntryOwner<C> {
99    pub open spec fn into_pte_owner_spec(self) -> EntryOwner<C> {
100        self
101    }
102
103    pub open spec fn from_pte_owner_spec(self) -> EntryOwner<C> {
104        self
105    }
106
107    /// This is equivalent to the other `invariants` relations, combining the `inv` predicates for each
108    /// object and the well-formedness relations between them.
109    pub open spec fn pte_invariants(self, pte: C::E, regions: MetaRegionOwners) -> bool {
110        &&& self.inv()
111        &&& regions.inv()
112        &&& self.match_pte(pte, self.parent_level)
113        &&& self.metaregion_sound(regions)
114    }
115}
116
117} // verus!
ostd/specs/mm/page_table/node/child.rs

ostd/specs/mm/page_table/node/
child.rs
