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

1use vstd::prelude::*;
2
3use vstd::cell;
4use vstd::simple_pptr::PointsTo;
5use vstd_extra::array_ptr;
6use vstd_extra::ghost_tree::*;
7use vstd_extra::ownership::*;
8
9use crate::mm::frame::meta::mapping::{frame_to_index, meta_to_frame};
10use crate::mm::frame::meta::REF_COUNT_UNUSED;
11use crate::mm::page_prop::PageProperty;
12use crate::mm::page_table::*;
13use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
14use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
15use crate::specs::arch::paging_consts::PagingConsts;
16use crate::specs::arch::*;
17use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
18use crate::specs::mm::page_table::node::entry_view::*;
19use crate::specs::mm::page_table::*;
20use core::marker::PhantomData;
21
22verus! {
23
24pub tracked struct FrameEntryOwner {
25    pub mapped_pa: usize,
26    pub size: usize,
27    pub prop: PageProperty,
28}
29
30pub tracked struct EntryOwner<C: PageTableConfig> {
31    pub node: Option<NodeOwner<C>>,
32    pub frame: Option<FrameEntryOwner>,
33    pub locked: Option<Ghost<Seq<FrameView<C>>>>,
34    pub absent: bool,
35    pub in_scope: bool,
36    pub path: TreePath<NR_ENTRIES>,
37    pub parent_level: PagingLevel,
38}
39
40impl<C: PageTableConfig> EntryOwner<C> {
41    pub open spec fn is_node(self) -> bool {
42        self.node is Some
43    }
44
45    pub open spec fn is_frame(self) -> bool {
46        self.frame is Some
47    }
48
49    pub open spec fn is_locked(self) -> bool {
50        self.locked is Some
51    }
52
53    pub open spec fn is_absent(self) -> bool {
54        self.absent
55    }
56
57    pub open spec fn new_absent_spec(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> Self {
58        EntryOwner {
59            node: None,
60            frame: None,
61            locked: None,
62            absent: true,
63            in_scope: true,
64            path,
65            parent_level,
66        }
67    }
68
69    pub open spec fn new_frame_spec(paddr: Paddr, path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, prop: PageProperty) -> Self {
70        EntryOwner {
71            node: None,
72            frame: Some(FrameEntryOwner { mapped_pa: paddr, size: page_size(parent_level), prop }),
73            locked: None,
74            absent: false,
75            in_scope: true,
76            path,
77            parent_level,
78        }
79    }
80
81    pub open spec fn new_node_spec(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> Self {
82        EntryOwner {
83            node: Some(node),
84            frame: None,
85            locked: None,
86            absent: false,
87            in_scope: true,
88            path,
89            parent_level: (node.level + 1) as PagingLevel,
90        }
91    }
92
93    pub axiom fn new_absent(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> tracked Self
94        returns Self::new_absent_spec(path, parent_level);
95
96    pub axiom fn new_frame(paddr: Paddr, path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, prop: PageProperty) -> tracked Self
97        returns Self::new_frame_spec(paddr, path, parent_level, prop);
98
99    pub axiom fn new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> tracked Self
100        returns Self::new_node_spec(node, path);
101
102    pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
103        &&& pte.paddr() % PAGE_SIZE == 0
104        &&& pte.paddr() < MAX_PADDR
105        &&& !pte.is_present() ==> {
106            self.is_absent()
107        }
108        &&& pte.is_present() && !pte.is_last(parent_level) ==> {
109            &&& self.is_node()
110            &&& meta_to_frame(self.node.unwrap().meta_perm.addr()) == pte.paddr()
111        }
112        &&& pte.is_present() && pte.is_last(parent_level) ==> {
113            &&& self.is_frame()
114            &&& self.frame.unwrap().mapped_pa == pte.paddr()
115            &&& self.frame.unwrap().prop == pte.prop()
116        }
117    }
118
119    /// When owner is absent and pte is the absent PTE with valid paddr, match_pte holds.
120    pub proof fn absent_match_pte(owner: Self, pte: C::E, parent_level: PagingLevel)
121        requires
122            owner.is_absent(),
123            pte == C::E::new_absent_spec(),
124            pte.paddr() % PAGE_SIZE == 0,
125            pte.paddr() < MAX_PADDR,
126        ensures
127            owner.match_pte(pte, parent_level),
128    {
129        C::E::new_properties();
130        assert(!pte.is_present());
131        if pte.is_present() && !pte.is_last(parent_level) {
132            assert(pte.is_present());
133            assert(!pte.is_present());
134        }
135        if pte.is_present() && pte.is_last(parent_level) {
136            assert(pte.is_present());
137            assert(!pte.is_present());
138        }
139    }
140
141    pub open spec fn expected_raw_count(self) -> usize {
142        if self.in_scope {
143            0
144        } else {
145            1
146        }
147    }
148
149    pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool {
150        if self.is_node() {
151            let idx = frame_to_index(self.meta_slot_paddr().unwrap());
152            &&& regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
153            &&& regions.slot_owners[idx].raw_count == self.expected_raw_count()
154            &&& regions.slot_owners[idx].self_addr == self.node.unwrap().meta_perm.addr()
155            &&& self.node.unwrap().meta_perm.points_to.value().wf(regions.slot_owners[idx])
156            &&& regions.slot_owners[idx].path_if_in_pt is Some ==>
157                regions.slot_owners[idx].path_if_in_pt.unwrap() == self.path
158        } else if self.is_frame() {
159            regions.slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())].path_if_in_pt is Some ==>
160            regions.slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())].path_if_in_pt.unwrap() == self.path
161        } else {
162            true
163        }
164    }
165
166    pub axiom fn get_path(self) -> tracked TreePath<NR_ENTRIES>
167        returns self.path;
168
169    pub open spec fn meta_slot_paddr(self) -> Option<Paddr> {
170        if self.is_node() {
171            Some(meta_to_frame(self.node.unwrap().meta_perm.addr()))
172        } else if self.is_frame() {
173            Some(self.frame.unwrap().mapped_pa)
174        } else {
175            None
176        }
177    }
178
179    pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool {
180        self.meta_slot_paddr() is Some ==>
181        other.meta_slot_paddr() is Some ==>
182        self.meta_slot_paddr().unwrap() != other.meta_slot_paddr().unwrap()
183    }
184
185    /// Two nodes satisfying relate_region with the same regions have different addresses
186    /// if and only if they have different paths.
187    pub proof fn nodes_different_paths_different_addrs(
188        self,
189        other: Self,
190        regions: MetaRegionOwners,
191    )
192        requires
193            self.is_node(),
194            other.is_node(),
195            self.relate_region(regions),
196            self.meta_slot_paddr() is Some ==> regions.slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())].path_if_in_pt is Some,
197            other.meta_slot_paddr() is Some ==> regions.slot_owners[frame_to_index(other.meta_slot_paddr().unwrap())].path_if_in_pt is Some,
198            other.relate_region(regions),
199            self.path != other.path,
200        ensures
201            self.node.unwrap().meta_perm.addr() != other.node.unwrap().meta_perm.addr(),
202    {
203        let self_addr = self.node.unwrap().meta_perm.addr();
204        let other_addr = other.node.unwrap().meta_perm.addr();
205        let self_idx = frame_to_index(meta_to_frame(self_addr));
206        let other_idx = frame_to_index(meta_to_frame(other_addr));
207
208        if self_addr == other_addr {
209            assert(regions.slot_owners[self_idx].path_if_in_pt == Some(self.path));
210            assert(regions.slot_owners[other_idx].path_if_in_pt == Some(other.path));
211//            assert(Some(self.path) == Some(other.path));
212            assert(self.path == other.path);
213            assert(false); // Contradiction
214        }
215    }
216}
217
218impl<C: PageTableConfig> Inv for EntryOwner<C> {
219    open spec fn inv(self) -> bool {
220        &&& self.node is Some ==> {
221            &&& self.frame is None
222            &&& self.locked is None
223            &&& self.node.unwrap().inv()
224            &&& !self.absent
225        }
226        &&& self.frame is Some ==> {
227            &&& self.node is None
228            &&& self.locked is None
229            &&& !self.absent
230            &&& self.frame.unwrap().mapped_pa % PAGE_SIZE == 0
231            &&& self.frame.unwrap().mapped_pa < MAX_PADDR
232            &&& self.frame.unwrap().size == page_size(self.parent_level)
233        }
234        &&& self.locked is Some ==> {
235            &&& self.frame is None
236            &&& self.node is None
237            &&& !self.absent
238        }
239        &&& self.path.inv()
240    }
241}
242
243impl<C: PageTableConfig> View for EntryOwner<C> {
244    type V = EntryView<C>;
245
246    #[verifier::external_body]
247    open spec fn view(&self) -> <Self as View>::V {
248        if let Some(frame) = self.frame {
249            EntryView::Leaf {
250                leaf: LeafPageTableEntryView {
251                    map_va: vaddr(self.path) as int,
252                    //                    frame_pa: self.base_addr as int,
253                    //                    in_frame_index: self.index as int,
254                    map_to_pa: frame.mapped_pa as int,
255                    level: self.path.len() as u8,
256                    prop: frame.prop,
257                    phantom: PhantomData,
258                },
259            }
260        } else if let Some(node) = self.node {
261            EntryView::Intermediate {
262                node: IntermediatePageTableEntryView {
263                    map_va: vaddr(self.path) as int,
264                    //                    frame_pa: self.base_addr as int,
265                    //                    in_frame_index: self.index as int,
266                    map_to_pa: meta_to_frame(node.meta_perm.addr()) as int,
267                    level: self.path.len() as u8,
268                    phantom: PhantomData,
269                },
270            }
271        } else if let Some(view) = self.locked {
272            EntryView::LockedSubtree { views: view@ }
273        } else {
274            EntryView::Absent
275        }
276    }
277}
278
279impl<C: PageTableConfig> InvView for EntryOwner<C> {
280    proof fn view_preserves_inv(self) {
281        admit()
282    }
283}
284
285impl<'rcu, C: PageTableConfig> OwnerOf for Entry<'rcu, C> {
286    type Owner = EntryOwner<C>;
287
288    open spec fn wf(self, owner: Self::Owner) -> bool {
289        &&& self.idx < NR_ENTRIES
290        &&& owner.match_pte(self.pte, owner.parent_level)
291        &&& self.pte.paddr() % PAGE_SIZE == 0
292        &&& self.pte.paddr() < MAX_PADDR
293    }
294}
295
296} // verus!
ostd/specs/mm/page_table/node/entry_owners.rs

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