ostd/specs/mm/page_table/
owners.rs

1use vstd::prelude::*;
2
3use core::ops::Range;
4
5use vstd::arithmetic::power2::pow2;
6use vstd::seq::*;
7use vstd::seq_lib::*;
8use vstd::set_lib::*;
9use vstd_extra::array_ptr;
10use vstd_extra::cast_ptr::Repr;
11use vstd_extra::extern_const::*;
12use vstd_extra::ghost_tree::*;
13use vstd_extra::ownership::*;
14use vstd_extra::prelude::TreeNodeValue;
15use vstd_extra::undroppable::*;
16
17use crate::mm::{
18    page_table::{EntryOwner, FrameView},
19    MAX_NR_LEVELS, Paddr, Vaddr,
20};
21
22use crate::specs::arch::*;
23use crate::specs::mm::page_table::*;
24use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
25use crate::mm::page_table::PageTableGuard;
26
27use core::ops::Deref;
28
29verus! {
30
31#[verifier::inline]
32pub open spec fn vaddr_shift_bits<const L: usize>(idx: int) -> nat
33    recommends
34        0 < L,
35        idx < L,
36{
37    (12 + 9 * (L - 1 - idx)) as nat
38}
39
40#[verifier::inline]
41pub open spec fn vaddr_shift<const L: usize>(idx: int) -> usize
42    recommends
43        0 < L,
44        idx < L,
45{
46    pow2(vaddr_shift_bits::<L>(idx)) as usize
47}
48
49#[verifier::inline]
50pub open spec fn vaddr_make<const L: usize>(idx: int, offset: usize) -> usize
51    recommends
52        0 < L,
53        idx < L,
54        0 <= offset < 512,
55{
56    (vaddr_shift::<L>(idx) * offset) as usize
57}
58
59pub open spec fn rec_vaddr(
60    path: TreePath<CONST_NR_ENTRIES>,
61    idx: int,
62) -> usize/*        recommends
63        0 < NR_LEVELS(),
64        path.len() <= NR_LEVELS(),
65        0 <= idx <= path.len(),*/
66
67    decreases path.len() - idx,
68    when 0 <= idx <= path.len()
69{
70    if idx == path.len() {
71        0
72    } else {
73        let offset: usize = path.index(idx);
74        (vaddr_make::<CONST_NR_LEVELS>(idx, offset) + rec_vaddr(path, idx + 1)) as usize
75    }
76}
77
78pub open spec fn vaddr(path: TreePath<CONST_NR_ENTRIES>) -> usize {
79    rec_vaddr(path, 0)
80}
81
82/*
83impl<'rcu, C: PageTableConfig> EntryState<'rcu, C> {
84    open spec fn get_entry(self) -> Option<EntryOwner<'rcu, C>> {
85        match self {
86            Self::Present(owner) => Some(owner),
87            _ => None,
88        }
89    }
90}
91*/
92
93impl<C: PageTableConfig, const L: usize> TreeNodeValue<L> for EntryOwner<C> {
94    open spec fn default(lv: nat) -> Self {
95        Self {
96            path: TreePath::new(Seq::empty()),
97            parent_level: (INC_LEVELS() - lv + 1) as PagingLevel,
98            node: None,
99            frame: None,
100            locked: None,
101            absent: true,
102        }
103    }
104
105    proof fn default_preserves_inv() {
106    }
107
108    open spec fn la_inv(self, lv: nat) -> bool {
109        self.is_node() ==> lv < L - 1
110    }
111
112    proof fn default_preserves_la_inv() {
113    }
114
115    open spec fn rel_children(self, child: Option<Self>) -> bool {
116        if self.is_node() {
117            &&& child is Some
118            &&& child.unwrap().parent_level == self.node.unwrap().level
119        } else {
120            &&& child is None
121        }
122    }
123
124    proof fn default_preserves_rel_children(self, lv: nat) {
125        admit()
126    }
127}
128
129extern_const!(
130pub INC_LEVELS [INC_LEVELS_SPEC, CONST_INC_LEVELS]: usize = CONST_NR_LEVELS + 1
131);
132
133/// `OwnerSubtree` is a tree `Node` (from `vstd_extra::ghost_tree`) containing `EntryOwner`s.
134/// It lives in a tree of maximum depth 5. Page table nodes can be at levels 0-3, and their entries are their children at the next
135/// level down. This means that level 4, the lowest level, can only contain frame entries as it consists of the entries of level 1 page tables.
136///
137/// Level correspondences: tree level 0 ==> path length 0 ==> level 4 page table
138///                        tree level 1 ==> path length 1 ==> level 3 page table (the level 4 page table does not map frames directly)
139///                        tree level 2 ==> path length 2 ==> level 2 page table or frame mapped by level 3 table
140///                        tree level 3 ==> path length 3 ==> level 1 page table or frame mapped by level 2 table
141///                        tree level 4 ==> path length 4 ==> frame mapped by level 1 table
142pub type OwnerSubtree<C> = Node<EntryOwner<C>, CONST_NR_ENTRIES, CONST_INC_LEVELS>;
143
144pub struct PageTableOwner<C: PageTableConfig>(pub OwnerSubtree<C>);
145
146impl<C: PageTableConfig> PageTableOwner<C> {
147
148    /*
149    pub proof fn never_drop_preserves_unlocked<'rcu>(
150        subtree: OwnerSubtree<C>,
151        path: TreePath<CONST_NR_ENTRIES>,
152        guard: PageTableGuard<'rcu, C>,
153        guards0: Guards<'rcu, C>,
154        guards1: Guards<'rcu, C>
155    )
156        requires
157            subtree.inv(),
158            Self::unlocked(subtree, path, guards0),
159            <PageTableGuard<'rcu, C> as Undroppable>::constructor_requires(guard,guards0),
160            <PageTableGuard<'rcu, C> as Undroppable>::constructor_ensures(guard, guards0, guards1),
161        ensures
162            Self::unlocked(subtree, path, guards1),
163        decreases INC_LEVELS() - subtree.level
164    {
165        admit();
166    }
167    */
168
169    pub open spec fn view_rec(self, path: TreePath<CONST_NR_ENTRIES>) -> Set<Mapping>
170        decreases INC_LEVELS() - path.len() when self.0.inv() && path.len() <= INC_LEVELS() - 1
171    {
172        if self.0.value.is_frame() {
173            let vaddr = vaddr(path);
174            let pt_level = INC_LEVELS() - path.len();
175            let page_size = page_size(pt_level as PagingLevel);
176    
177            set![Mapping {
178                va_range: Range { start: vaddr, end: (vaddr + page_size) as Vaddr },
179                pa_range: Range {
180                    start: self.0.value.frame.unwrap().mapped_pa,
181                    end: (self.0.value.frame.unwrap().mapped_pa + page_size) as Paddr,
182                },
183                page_size: page_size,
184                property: self.0.value.frame.unwrap().prop,
185            }]
186        } else if self.0.value.is_node() && path.len() < INC_LEVELS() - 1 {
187            Set::new(
188                |m: Mapping| exists|i:int| #![auto] 0 <= i < self.0.children.len() &&
189                    self.0.children[i] is Some &&
190                    PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
191            )
192        } else {
193            set![]
194        }
195    }
196
197    pub proof fn view_rec_contains(self, path: TreePath<CONST_NR_ENTRIES>, m: Mapping)
198        requires
199            self.0.inv(),
200            path.len() < INC_LEVELS() - 1,
201            path.len() == self.0.level,
202            self.view_rec(path).contains(m),
203            self.0.value.is_node()
204        ensures
205            exists|i:int| #![auto] 0 <= i < self.0.children.len() &&
206            self.0.children[i] is Some &&
207            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
208    { }
209
210    pub proof fn view_rec_contains_choose(self, path: TreePath<CONST_NR_ENTRIES>, m: Mapping) -> (i: int)
211        requires
212            self.0.inv(),
213            path.len() < INC_LEVELS() - 1,
214            path.len() == self.0.level,
215            self.view_rec(path).contains(m),
216            self.0.value.is_node(),
217        ensures
218            0 <= i < self.0.children.len() &&
219            self.0.children[i] is Some &&
220            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
221    {
222        choose|i:int| #![auto] 0 <= i < self.0.children.len() &&
223            self.0.children[i] is Some &&
224            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
225    }
226
227    pub proof fn view_rec_vaddr_range(self, path: TreePath<CONST_NR_ENTRIES>, m: Mapping)
228        requires
229            self.0.inv(),
230            path.len() <= INC_LEVELS() - 1,
231            path.len() == self.0.level,
232            self.view_rec(path).contains(m),
233        ensures
234            vaddr(path) <= m.va_range.start < m.va_range.end <= vaddr(path) + page_size(path.len() as PagingLevel),
235    {
236        admit();
237    }
238
239    pub proof fn view_rec_disjoint_vaddrs(self, path: TreePath<CONST_NR_ENTRIES>, m1: Mapping, m2: Mapping)
240        requires
241            self.0.inv(),
242            path.len() <= INC_LEVELS() - 1,
243            path.len() == self.0.level,
244            self.view_rec(path).contains(m1),
245            self.view_rec(path).contains(m2),
246            m1 != m2,
247        ensures
248            m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start
249        decreases INC_LEVELS() - path.len()
250    {
251        broadcast use group_set_properties;
252
253        if self.0.value.is_frame() {
254            assert(self.view_rec(path).is_singleton());
255        } else if self.0.value.is_node() {
256            self.view_rec_contains(path, m1);
257            self.view_rec_contains(path, m2);
258
259            let i1 = self.view_rec_contains_choose(path, m1);
260            let i2 = self.view_rec_contains_choose(path, m2);
261
262            if i1 == i2 {
263                PageTableOwner(self.0.children[i1].unwrap()).view_rec_disjoint_vaddrs(path.push_tail(i1 as usize), m1, m2);
264            } else if i1 < i2 {
265                let page_size = page_size((path.len() + 1) as PagingLevel);
266                // TODO: connect TreePath to AbstractVaddr
267                assert(vaddr(path.push_tail(i1 as usize)) + page_size <= vaddr(path.push_tail(i2 as usize))) by { admit(); };
268                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(path.push_tail(i1 as usize), m1);
269                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(path.push_tail(i2 as usize), m2);
270            } else {
271                let page_size = page_size((path.len() + 1) as PagingLevel);
272                assert(vaddr(path.push_tail(i2 as usize)) + page_size <= vaddr(path.push_tail(i1 as usize))) by { admit(); };
273                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(path.push_tail(i2 as usize), m2);
274                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(path.push_tail(i1 as usize), m1);
275            }
276        }
277    }
278
279    pub open spec fn relate_region_rec(self, path: TreePath<CONST_NR_ENTRIES>, regions: MetaRegionOwners) -> bool
280        decreases INC_LEVELS() - self.0.level when self.0.inv()
281    {
282        if self.0.value.is_node() {
283            &&& self.0.value.node.unwrap().path == path
284            &&& self.0.value.node.unwrap().relate_region(regions)
285            &&& forall|i: int| #![auto] 0 <= i < self.0.children.len() && self.0.children[i] is Some ==>
286                PageTableOwner(self.0.children[i].unwrap()).relate_region_rec(path.push_tail(i as usize), regions)
287        } else {
288            true
289        }
290    }
291
292    pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool
293        decreases INC_LEVELS() - self.0.level when self.0.inv()
294    {
295        self.relate_region_rec(TreePath::new(Seq::empty()), regions)
296    }
297}
298
299impl<C: PageTableConfig> Inv for PageTableOwner<C> {
300    open spec fn inv(self) -> bool {
301        &&& self.0.inv()
302    }
303}
304
305impl<C: PageTableConfig> View for PageTableOwner<C> {
306    type V = PageTableView;
307
308    open spec fn view(&self) -> <Self as View>::V {
309        let mappings = self.view_rec(TreePath::new(Seq::empty()));
310        PageTableView {
311            mappings
312        }
313    }
314}
315
316impl<'a, C: PageTableConfig> CursorContinuation<'a, C> {
317    pub open spec fn into_subtree(self) -> OwnerSubtree<C>
318    {
319        Node {
320            value: self.entry_own,
321            children: self.children,
322            level: self.tree_level,
323        }
324    }
325
326    pub proof fn into_subtree_inv(self)
327        requires
328            self.inv(),
329            self.all_some(),
330        ensures
331            self.into_subtree().inv(),
332    {
333        assert forall|i: int| #![auto] 0 <= i < self.children.len() && self.children[i] is Some implies
334            self.children[i].unwrap().value.parent_level == self.entry_own.node.unwrap().level by {
335            }
336    }
337}
338
339impl<'a, C: PageTableConfig> CursorOwner<'a, C> {
340    pub open spec fn into_pt_owner_rec(self) -> PageTableOwner<C>
341        decreases NR_LEVELS() - self.level when self.inv()
342    {
343        if self.level == NR_LEVELS() {
344            PageTableOwner(self.continuations[self.level-1].into_subtree())
345        } else {
346            self.pop_level_owner_spec().0.into_pt_owner_rec()
347        }
348    }
349}
350
351} // verus!
ostd/specs/mm/page_table/owners.rs

ostd/specs/mm/page_table/
owners.rs
