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::meta_to_frame;
10use crate::mm::page_prop::PageProperty;
11use crate::mm::page_table::*;
12use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
13use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
14use crate::specs::arch::paging_consts::PagingConsts;
15use crate::specs::arch::*;
16use crate::specs::mm::page_table::owners::*;
17use core::marker::PhantomData;
18
19verus! {
20
21pub tracked struct FrameEntryOwner {
22    pub mapped_pa: usize,
23    pub size: usize,
24    pub prop: PageProperty,
25}
26
27pub tracked struct EntryOwner<C: PageTableConfig> {
28    pub node: Option<NodeOwner<C>>,
29    pub frame: Option<FrameEntryOwner>,
30    pub locked: Option<Ghost<Seq<FrameView<C>>>>,
31    pub absent: bool,
32    pub path: TreePath<CONST_NR_ENTRIES>,
33    pub parent_level: PagingLevel,
34}
35
36impl<C: PageTableConfig> EntryOwner<C> {
37    pub open spec fn is_node(self) -> bool {
38        self.node is Some
39    }
40
41    pub open spec fn is_frame(self) -> bool {
42        self.frame is Some
43    }
44
45    pub open spec fn is_locked(self) -> bool {
46        self.locked is Some
47    }
48
49    pub open spec fn is_absent(self) -> bool {
50        self.absent
51    }
52
53    pub open spec fn new_absent_spec(parent_level: PagingLevel) -> Self {
54        EntryOwner {
55            node: None,
56            frame: None,
57            locked: None,
58            absent: true,
59            path: TreePath::new(Seq::empty()),
60            parent_level,
61        }
62    }
63
64    pub open spec fn new_frame_spec(paddr: Paddr, parent_level: PagingLevel, prop: PageProperty) -> Self {
65        EntryOwner {
66            node: None,
67            frame: Some(FrameEntryOwner { mapped_pa: paddr, size: page_size(parent_level), prop }),
68            locked: None,
69            absent: false,
70            path: TreePath::new(Seq::empty()),
71            parent_level,
72        }
73    }
74
75    pub open spec fn new_node_spec(node: NodeOwner<C>) -> Self {
76        EntryOwner {
77            node: Some(node),
78            frame: None,
79            locked: None,
80            absent: false,
81            path: TreePath::new(Seq::empty()),
82            parent_level: (node.level + 1) as PagingLevel,
83        }
84    }
85
86    pub axiom fn new_absent(parent_level: PagingLevel) -> tracked Self
87        returns Self::new_absent_spec(parent_level);
88
89    pub axiom fn new_frame(paddr: Paddr, parent_level: PagingLevel, prop: PageProperty) -> tracked Self
90        returns Self::new_frame_spec(paddr, parent_level, prop);
91
92    pub axiom fn new_node(node: NodeOwner<C>) -> tracked Self
93        returns Self::new_node_spec(node);
94
95    pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool {
96        &&& pte.paddr() % PAGE_SIZE() == 0
97        &&& pte.paddr() < MAX_PADDR()
98        &&& !pte.is_present() ==> {
99            self.is_absent()
100        }
101        &&& pte.is_present() && !pte.is_last(parent_level) ==> {
102            &&& self.is_node()
103            &&& meta_to_frame(self.node.unwrap().meta_perm.addr()) == pte.paddr()
104        }
105        &&& pte.is_present() && pte.is_last(parent_level) ==> {
106            &&& self.is_frame()
107            &&& self.frame.unwrap().mapped_pa == pte.paddr()
108            &&& self.frame.unwrap().prop == pte.prop()
109        }
110    }
111}
112
113impl<C: PageTableConfig> Inv for EntryOwner<C> {
114    open spec fn inv(self) -> bool {
115        &&& self.node is Some ==> {
116            &&& self.frame is None
117            &&& self.locked is None
118            &&& self.node.unwrap().inv()
119            &&& !self.absent
120        }
121        &&& self.frame is Some ==> {
122            &&& self.node is None
123            &&& self.locked is None
124            &&& !self.absent
125            &&& self.frame.unwrap().mapped_pa % PAGE_SIZE() == 0
126            &&& self.frame.unwrap().mapped_pa < MAX_PADDR()
127        }
128        &&& self.locked is Some ==> {
129            &&& self.frame is None
130            &&& self.node is None
131            &&& !self.absent
132        }
133    }
134}
135
136impl<C: PageTableConfig> View for EntryOwner<C> {
137    type V = EntryView<C>;
138
139    #[verifier::external_body]
140    open spec fn view(&self) -> <Self as View>::V {
141        if let Some(frame) = self.frame {
142            EntryView::Leaf {
143                leaf: LeafPageTableEntryView {
144                    map_va: vaddr(self.path) as int,
145                    //                    frame_pa: self.base_addr as int,
146                    //                    in_frame_index: self.index as int,
147                    map_to_pa: frame.mapped_pa as int,
148                    level: (self.path.len() + 1) as u8,
149                    prop: frame.prop,
150                    phantom: PhantomData,
151                },
152            }
153        } else if let Some(node) = self.node {
154            EntryView::Intermediate {
155                node: IntermediatePageTableEntryView {
156                    map_va: vaddr(self.path) as int,
157                    //                    frame_pa: self.base_addr as int,
158                    //                    in_frame_index: self.index as int,
159                    map_to_pa: meta_to_frame(node.meta_perm.addr()) as int,
160                    level: (self.path.len() + 1) as u8,
161                    phantom: PhantomData,
162                },
163            }
164        } else if let Some(view) = self.locked {
165            EntryView::LockedSubtree { views: view@ }
166        } else {
167            EntryView::Absent
168        }
169    }
170}
171
172impl<C: PageTableConfig> InvView for EntryOwner<C> {
173    proof fn view_preserves_inv(self) {
174        admit()
175    }
176}
177
178impl<'rcu, C: PageTableConfig> OwnerOf for Entry<'rcu, C> {
179    type Owner = EntryOwner<C>;
180
181    open spec fn wf(self, owner: Self::Owner) -> bool {
182        &&& self.idx < NR_ENTRIES()
183        &&& owner.match_pte(self.pte, owner.parent_level)
184        &&& self.pte.paddr() % PAGE_SIZE() == 0
185        &&& self.pte.paddr() < MAX_PADDR()
186    }
187}
188
189} // verus!
ostd/specs/mm/page_table/node/entry_owners.rs

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