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

1use vstd::prelude::*;
2
3use vstd::cell;
4use vstd::simple_pptr::*;
5
6use crate::mm::frame::meta::MetaSlot;
7use crate::mm::paddr_to_vaddr;
8use crate::mm::page_table::*;
9use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
10use crate::specs::arch::kspace::{
11    FRAME_METADATA_RANGE, LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR,
12};
13use crate::specs::arch::mm::{
14    CONST_NR_ENTRIES, MAX_NR_PAGES, MAX_PADDR, NR_ENTRIES, NR_LEVELS, PAGE_SIZE,
15};
16use crate::specs::arch::paging_consts::PagingConsts;
17use crate::specs::mm::frame::mapping::{meta_to_frame, frame_to_index, META_SLOT_SIZE};
18use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
19use crate::specs::mm::page_table::GuardPerm;
20
21use vstd_extra::array_ptr;
22use vstd_extra::cast_ptr::Repr;
23use vstd_extra::ownership::*;
24use vstd_extra::ghost_tree::TreePath;
25
26verus! {
27
28pub tracked struct PageMetaOwner {
29    pub nr_children: vstd::cell::PointsTo<u16>,
30    pub stray: vstd::cell::PointsTo<bool>,
31}
32
33impl Inv for PageMetaOwner {
34    open spec fn inv(self) -> bool {
35        &&& self.nr_children.is_init()
36        &&& 0 <= self.nr_children.value() <= NR_ENTRIES()
37        &&& self.stray.is_init()
38    }
39}
40
41pub ghost struct PageMetaModel {
42    pub nr_children: u16,
43    pub stray: bool,
44}
45
46impl Inv for PageMetaModel {
47    open spec fn inv(self) -> bool {
48        true
49    }
50}
51
52impl View for PageMetaOwner {
53    type V = PageMetaModel;
54
55    open spec fn view(&self) -> <Self as View>::V {
56        PageMetaModel { nr_children: self.nr_children.value(), stray: self.stray.value() }
57    }
58}
59
60impl InvView for PageMetaOwner {
61    proof fn view_preserves_inv(self) {
62    }
63}
64
65impl<C: PageTableConfig> OwnerOf for PageTablePageMeta<C> {
66    type Owner = PageMetaOwner;
67
68    open spec fn wf(self, owner: Self::Owner) -> bool {
69        &&& self.nr_children.id() == owner.nr_children.id()
70        &&& self.stray.id() == owner.stray.id()
71        &&& 0 <= owner.nr_children.value() <= NR_ENTRIES()
72    }
73}
74
75pub tracked struct NodeOwner<C: PageTableConfig> {
76    pub meta_own: PageMetaOwner,
77    pub meta_perm: vstd_extra::cast_ptr::PointsTo<MetaSlot, PageTablePageMeta<C>>,
78    pub children_perm: array_ptr::PointsTo<C::E, CONST_NR_ENTRIES>,
79    pub level: PagingLevel,
80    pub path: TreePath<CONST_NR_ENTRIES>,
81}
82
83impl<C: PageTableConfig> Inv for NodeOwner<C> {
84    open spec fn inv(self) -> bool {
85        &&& self.meta_perm.points_to.is_init()
86        &&& <PageTablePageMeta<C> as Repr<MetaSlot>>::wf(self.meta_perm.points_to.value())
87        &&& self.meta_perm.addr() == self.meta_perm.points_to.addr()
88        &&& self.meta_own.inv()
89        &&& self.meta_perm.value().wf(self.meta_own)
90        &&& self.meta_perm.is_init()
91        &&& self.meta_perm.wf()
92        &&& FRAME_METADATA_RANGE().start <= self.meta_perm.addr() < FRAME_METADATA_RANGE().end
93        &&& self.meta_perm.addr() % META_SLOT_SIZE() == 0
94        &&& meta_to_frame(self.meta_perm.addr()) < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR()
95        &&& meta_to_frame(self.meta_perm.addr()) < MAX_PADDR()
96        &&& meta_to_frame(self.meta_perm.addr()) == self.children_perm.addr()
97        &&& self.meta_own.nr_children.id() == self.meta_perm.value().nr_children.id()
98        &&& 0 <= self.meta_own.nr_children.value() <= NR_ENTRIES()
99        &&& 1 <= self.level <= NR_LEVELS()
100        &&& self.children_perm.is_init_all()
101        &&& self.children_perm.addr() == paddr_to_vaddr(meta_to_frame(self.meta_perm.addr()))
102    }
103}
104
105impl<'rcu, C: PageTableConfig> NodeOwner<C> {
106    pub open spec fn relate_guard_perm(self, guard_perm: GuardPerm<'rcu, C>) -> bool {
107        &&& guard_perm.is_init()
108        &&& guard_perm.value().inner.inner@.ptr.addr() == self.meta_perm.addr()
109        &&& guard_perm.value().inner.inner@.ptr.addr() == self.meta_perm.points_to.addr()
110        &&& guard_perm.value().inner.inner@.wf(self)
111        &&& self.meta_perm.is_init()
112        &&& self.meta_perm.wf()
113    }
114
115    /// All nodes' metadata is forgotten for the duration of their lifetime.
116    pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool {
117        &&& !regions.slots.contains_key(frame_to_index(meta_to_frame(self.meta_perm.addr())))
118        &&& regions.slot_owners[frame_to_index(meta_to_frame(self.meta_perm.addr()))].path_if_in_pt == Some(self.path)
119    }
120}
121
122pub ghost struct NodeModel<C: PageTableConfig> {
123    pub meta: PageTablePageMeta<C>,
124}
125
126impl<C: PageTableConfig> Inv for NodeModel<C> {
127    open spec fn inv(self) -> bool {
128        true
129    }
130}
131
132impl<C: PageTableConfig> View for NodeOwner<C> {
133    type V = NodeModel<C>;
134
135    open spec fn view(&self) -> <Self as View>::V {
136        NodeModel { meta: self.meta_perm.value() }
137    }
138}
139
140impl<C: PageTableConfig> InvView for NodeOwner<C> {
141    proof fn view_preserves_inv(self) {
142    }
143}
144
145impl<C: PageTableConfig> OwnerOf for PageTableNode<C> {
146    type Owner = NodeOwner<C>;
147
148    open spec fn wf(self, owner: Self::Owner) -> bool {
149        &&& self.ptr.addr() == owner.meta_perm.addr()
150    }
151}
152
153} // verus!
ostd/specs/mm/page_table/node/owners.rs

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