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

1use vstd::cell::pcell_maybe_uninit;
2use vstd::prelude::*;
3
4use vstd::cell;
5use vstd::simple_pptr::*;
6
7use crate::mm::frame::meta::MetaSlot;
8use crate::mm::kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR};
9use crate::mm::paddr_to_vaddr;
10use crate::mm::page_table::*;
11use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
12use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
13use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
14use crate::specs::arch::paging_consts::PagingConsts;
15use crate::specs::mm::frame::mapping::{frame_to_index, meta_to_frame, META_SLOT_SIZE};
16use crate::specs::mm::frame::meta_owners::*;
17use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
18use crate::specs::mm::page_table::owners::INC_LEVELS;
19use crate::specs::mm::page_table::GuardPerm;
20
21use vstd_extra::array_ptr;
22use vstd_extra::cast_ptr::Repr;
23use vstd_extra::ghost_tree::TreePath;
24use vstd_extra::ownership::*;
25
26verus! {
27
28pub tracked struct PageMetaOwner {
29    pub nr_children: pcell_maybe_uninit::PointsTo<u16>,
30    pub stray: pcell_maybe_uninit::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: MetaPerm<PageTablePageMeta<C>>,
78    pub children_perm: array_ptr::PointsTo<C::E, NR_ENTRIES>,
79    pub level: PagingLevel,
80    pub tree_level: int,
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        &&& self.meta_perm.addr() == self.meta_perm.points_to.addr()
87        &&& self.meta_own.inv()
88        &&& self.meta_perm.value().metadata.wf(self.meta_own)
89        &&& self.meta_perm.is_init()
90        &&& self.meta_perm.wf(&self.meta_perm.inner_perms)
91        &&& FRAME_METADATA_RANGE.start <= self.meta_perm.addr() < FRAME_METADATA_RANGE.end
92        &&& self.meta_perm.addr() % META_SLOT_SIZE == 0
93        &&& meta_to_frame(self.meta_perm.addr()) < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR
94        &&& meta_to_frame(self.meta_perm.addr()) < MAX_PADDR
95        &&& meta_to_frame(self.meta_perm.addr()) == self.children_perm.addr()
96        &&& self.meta_own.nr_children.id() == self.meta_perm.value().metadata.nr_children.id()
97        &&& 0 <= self.meta_own.nr_children.value() <= NR_ENTRIES
98        &&& 1 <= self.level <= NR_LEVELS
99        &&& self.children_perm.is_init_all()
100        &&& self.children_perm.addr() == paddr_to_vaddr(meta_to_frame(self.meta_perm.addr()))
101        &&& self.level == self.meta_perm.value().metadata.level
102        &&& self.tree_level == INC_LEVELS - self.level
103    }
104}
105
106impl<C: PageTableConfig> NodeOwner<C> {
107    /// Returns a NodeOwner with children_perm updated at the given index.
108    /// Used to specify the state after storing a new PTE for an allocated child.
109    pub uninterp spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
110
111    #[verifier::external_body]
112    pub axiom fn set_children_perm_axiom(self, idx: usize, pte: C::E)
113        requires
114            self.inv(),
115            idx < NR_ENTRIES,
116        ensures
117            self.set_children_perm(idx, pte).inv(),
118            self.set_children_perm(idx, pte).meta_perm == self.meta_perm,
119            self.set_children_perm(idx, pte).meta_own == self.meta_own,
120            self.set_children_perm(idx, pte).level == self.level,
121            self.set_children_perm(idx, pte).tree_level == self.tree_level,
122            self.set_children_perm(idx, pte).children_perm.addr() == self.children_perm.addr(),
123            self.set_children_perm(idx, pte).children_perm.value()
124                == self.children_perm.value().update(idx as int, pte);
125}
126
127impl<'rcu, C: PageTableConfig> NodeOwner<C> {
128
129    pub open spec fn relate_guard_perm(self, guard_perm: GuardPerm<'rcu, C>) -> bool {
130        &&& guard_perm.is_init()
131        &&& guard_perm.value().inner.inner@.ptr.addr() == self.meta_perm.addr()
132        &&& guard_perm.value().inner.inner@.ptr.addr() == self.meta_perm.points_to.addr()
133        &&& guard_perm.value().inner.inner@.wf(self)
134        &&& self.meta_perm.is_init()
135        &&& self.meta_perm.wf(&self.meta_perm.inner_perms)
136    }
137}
138
139pub ghost struct NodeModel<C: PageTableConfig> {
140    pub meta: PageTablePageMeta<C>,
141}
142
143impl<C: PageTableConfig> Inv for NodeModel<C> {
144    open spec fn inv(self) -> bool {
145        true
146    }
147}
148
149impl<C: PageTableConfig> View for NodeOwner<C> {
150    type V = NodeModel<C>;
151
152    open spec fn view(&self) -> <Self as View>::V {
153        NodeModel { meta: self.meta_perm.value().metadata }
154    }
155}
156
157impl<C: PageTableConfig> InvView for NodeOwner<C> {
158    proof fn view_preserves_inv(self) {
159    }
160}
161
162impl<C: PageTableConfig> OwnerOf for PageTableNode<C> {
163    type Owner = NodeOwner<C>;
164
165    open spec fn wf(self, owner: Self::Owner) -> bool {
166        &&& self.ptr.addr() == owner.meta_perm.addr()
167    }
168}
169
170impl<C: PageTableConfig> PageTableNode<C> {
171    pub open spec fn invariants(self, owner: NodeOwner<C>) -> bool {
172        &&& owner.inv()
173        &&& self.wf(owner)
174//        &&& owner.meta_perm.wf(&owner.meta_perm.inner_perms)
175//        &&& owner.meta_perm.addr() == self.ptr.addr()
176//        &&& owner.meta_perm.addr() == self.ptr.addr()
177    }
178}
179
180} // verus!
ostd/specs/mm/page_table/node/owners.rs

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