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

1use vstd::prelude::*;
2
3use vstd_extra::ownership::*;
4
5use crate::mm::frame::*;
6use crate::mm::page_prop::PageProperty;
7use crate::mm::page_table::*;
8use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
9use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
10use crate::specs::arch::paging_consts::PagingConsts;
11use crate::specs::mm::frame::meta_owners::MetaSlotOwner;
12use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
13
14verus! {
15
16impl<C: PageTableConfig> OwnerOf for Child<C> {
17    type Owner = EntryOwner<C>;
18
19    open spec fn wf(self, owner: Self::Owner) -> bool {
20        match self {
21            Self::PageTable(node) => {
22                &&& owner.is_node()
23                &&& node.ptr.addr() == owner.node.unwrap().meta_perm.addr()
24                &&& node.index() == frame_to_index(meta_to_frame(node.ptr.addr()))
25            },
26            Self::Frame(paddr, level, prop) => {
27                &&& owner.is_frame()
28                &&& owner.frame.unwrap().mapped_pa == paddr
29                &&& owner.frame.unwrap().prop == prop
30                &&& level == owner.parent_level
31            },
32            Self::None => owner.is_absent(),
33        }
34    }
35}
36
37
38impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
39    type Owner = EntryOwner<C>;
40
41    open spec fn wf(self, owner: Self::Owner) -> bool {
42        match self {
43            Self::PageTable(node) => {
44                &&& owner.is_node()
45                &&& node.inner.0.ptr.addr() == owner.node.unwrap().meta_perm.addr()
46            },
47            Self::Frame(paddr, level, prop) => {
48                &&& owner.is_frame()
49                &&& owner.frame.unwrap().mapped_pa == paddr
50                &&& owner.frame.unwrap().prop == prop
51            },
52            Self::None => owner.is_absent(),
53        }
54    }
55}
56
57impl<C: PageTableConfig> Child<C> {
58
59    pub open spec fn get_node(self) -> Option<PageTableNode<C>> {
60        match self {
61            Self::PageTable(node) => Some(node),
62            _ => None,
63        }
64    }
65
66    pub open spec fn get_frame_tuple(self) -> Option<(Paddr, PagingLevel, PageProperty)> {
67        match self {
68            Self::Frame(paddr, level, prop) => Some((paddr, level, prop)),
69            _ => None,
70        }
71    }
72
73    pub open spec fn into_pte_frame_spec(self, tuple: (Paddr, PagingLevel, PageProperty)) -> C::E {
74        let (paddr, level, prop) = tuple;
75        C::E::new_page_spec(paddr, level, prop)
76    }
77
78
79    pub open spec fn into_pte_none_spec(self) -> C::E {
80        C::E::new_absent_spec()
81    }
82
83
84    pub open spec fn from_pte_spec(pte: C::E, level: PagingLevel, regions: MetaRegionOwners) -> Self {
85        if !pte.is_present() {
86            Self::None
87        } else if pte.is_last(level) {
88            Self::Frame(pte.paddr(), level, pte.prop())
89        } else {
90            Self::PageTable(PageTableNode::from_raw_spec(pte.paddr()))
91        }
92    }
93
94    pub open spec fn from_pte_frame_spec(pte: C::E, level: PagingLevel) -> Self {
95        Self::Frame(pte.paddr(), level, pte.prop())
96    }
97
98
99    pub open spec fn from_pte_pt_spec(paddr: Paddr, regions: MetaRegionOwners) -> Self {
100        Self::PageTable(PageTableNode::from_raw_spec(paddr))
101    }
102
103    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
104        &&& owner.inv()
105        &&& regions.inv()
106        &&& self.wf(owner)
107        &&& owner.relate_region(regions)
108        &&& owner.in_scope
109    }
110}
111
112impl<C: PageTableConfig> ChildRef<'_, C> {
113    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
114        &&& owner.inv()
115        &&& regions.inv()
116        &&& self.wf(owner)
117        &&& owner.relate_region(regions)
118        &&& !owner.in_scope
119    }
120}
121
122impl<C: PageTableConfig> EntryOwner<C> {
123
124    pub open spec fn from_pte_regions_spec(self, regions: MetaRegionOwners) -> MetaRegionOwners {
125        if self.is_node() {
126            let index = frame_to_index(self.meta_slot_paddr().unwrap());
127            let old_slot = regions.slot_owners[index];
128            let new_slot = MetaSlotOwner {
129                raw_count: 0usize,
130                ..old_slot
131            };
132            MetaRegionOwners {
133                slots: regions.slots.insert(index, self.node.unwrap().meta_perm.points_to),
134                slot_owners: regions.slot_owners.insert(index, new_slot),
135            }
136        } else {
137            regions
138        }
139    }
140
141    pub open spec fn into_pte_regions_spec(self, regions: MetaRegionOwners) -> MetaRegionOwners {
142        if self.is_node() {
143            let index = frame_to_index(self.meta_slot_paddr().unwrap());
144            let old_slot = regions.slot_owners[index];
145            let new_slot = MetaSlotOwner {
146                raw_count: (old_slot.raw_count + 1) as usize,
147                ..old_slot
148            };
149            MetaRegionOwners {
150                slots: regions.slots,
151                slot_owners: regions.slot_owners.insert(index, new_slot),
152                ..regions
153            }
154        } else {
155            regions
156        }
157    }
158
159    pub open spec fn into_pte_owner_spec(self) -> EntryOwner<C> {
160        EntryOwner {
161            in_scope: false,
162            ..self
163        }
164    }
165
166    pub open spec fn from_pte_owner_spec(self) -> EntryOwner<C> {
167        EntryOwner {
168            in_scope: true,
169            ..self
170        }
171    }
172
173    /// This is equivalent to the other `invariants` relations, combining the `inv` predicates for each
174    /// object and the well-formedness relations between them.
175    pub open spec fn pte_invariants(self, pte: C::E, regions: MetaRegionOwners) -> bool {
176        &&& self.inv()
177        &&& regions.inv()
178        &&& self.match_pte(pte, self.parent_level)
179        &&& self.relate_region(regions)
180        &&& !self.in_scope
181    }
182
183}
184
185} // verus!
ostd/specs/mm/page_table/node/child.rs

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