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::frame::meta::mapping::{max_meta_slots, meta_addr};
9use crate::mm::kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR};
10use crate::mm::paddr_to_vaddr;
11use crate::mm::page_table::PageTableGuard;
12use crate::mm::page_table::*;
13use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
14use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
15use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
16use crate::specs::arch::paging_consts::PagingConsts;
17use crate::specs::mm::frame::mapping::{META_SLOT_SIZE, frame_to_index, meta_to_frame};
18use crate::specs::mm::frame::meta_owners::*;
19use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
20use crate::specs::mm::page_table::owners::INC_LEVELS;
21
22use vstd_extra::array_ptr;
23use vstd_extra::cast_ptr::Repr;
24use vstd_extra::ghost_tree::TreePath;
25use vstd_extra::ownership::*;
26
27verus! {
28
29pub tracked struct PageMetaOwner {
30    pub nr_children: pcell_maybe_uninit::PointsTo<u16>,
31    pub stray: pcell_maybe_uninit::PointsTo<bool>,
32}
33
34impl Inv for PageMetaOwner {
35    open spec fn inv(self) -> bool {
36        &&& self.nr_children.is_init()
37        &&& 0 <= self.nr_children.value() <= NR_ENTRIES
38        &&& self.stray.is_init()
39    }
40}
41
42pub ghost struct PageMetaModel {
43    pub nr_children: u16,
44    pub stray: bool,
45}
46
47impl Inv for PageMetaModel {
48    open spec fn inv(self) -> bool {
49        true
50    }
51}
52
53impl View for PageMetaOwner {
54    type V = PageMetaModel;
55
56    open spec fn view(&self) -> <Self as View>::V {
57        PageMetaModel { nr_children: self.nr_children.value(), stray: self.stray.value() }
58    }
59}
60
61impl InvView for PageMetaOwner {
62    proof fn view_preserves_inv(self) {
63    }
64}
65
66impl<C: PageTableConfig> OwnerOf for PageTablePageMeta<C> {
67    type Owner = PageMetaOwner;
68
69    open spec fn wf(self, owner: Self::Owner) -> bool {
70        &&& self.nr_children.id() == owner.nr_children.id()
71        &&& self.stray.id() == owner.stray.id()
72        &&& 0 <= owner.nr_children.value() <= NR_ENTRIES
73    }
74}
75
76pub tracked struct NodeOwner<C: PageTableConfig> {
77    pub meta_own: PageMetaOwner,
78    pub children_perm: array_ptr::PointsTo<C::E, NR_ENTRIES>,
79    pub level: PagingLevel,
80    pub tree_level: int,
81    /// Borrow-model handle for the node's metadata slot: identifies the slot
82    /// in `MetaRegionOwners` where the perm is parked. Consumers source the
83    /// perm via `regions.borrow_typed_perm(slot_index)`.
84    pub slot_index: usize,
85}
86
87impl<C: PageTableConfig> Inv for NodeOwner<C> {
88    open spec fn inv(self) -> bool {
89        &&& self.meta_own.inv()
90        &&& 0 <= self.meta_own.nr_children.value() <= NR_ENTRIES
91        &&& 1 <= self.level <= NR_LEVELS
92        &&& self.children_perm.is_init_all()
93        &&& self.children_perm.addr() == paddr_to_vaddr(meta_to_frame(meta_addr(self.slot_index)))
94        &&& self.tree_level == INC_LEVELS - self.level - 1
95        &&& self.slot_index < max_meta_slots() as usize
96        &&& FRAME_METADATA_RANGE.start <= meta_addr(self.slot_index) < FRAME_METADATA_RANGE.end
97        &&& meta_addr(self.slot_index) % META_SLOT_SIZE == 0
98        &&& meta_to_frame(meta_addr(self.slot_index)) < VMALLOC_BASE_VADDR
99            - LINEAR_MAPPING_BASE_VADDR
100        &&& meta_to_frame(meta_addr(self.slot_index)) < MAX_PADDR
101        &&& meta_to_frame(meta_addr(self.slot_index)) == self.children_perm.addr()
102        &&& self.slot_index == frame_to_index(meta_to_frame(meta_addr(self.slot_index)))
103    }
104}
105
106impl<C: PageTableConfig> NodeOwner<C> {
107    /// The meta address of this node's slot, computed from `slot_index`.
108    /// Always equals `self.meta_perm.addr()` under `inv()`.
109    pub open spec fn meta_addr_self(self) -> Vaddr {
110        meta_addr(self.slot_index)
111    }
112
113    /// Reconstructs a metadata cast_ptr from `regions` at `self.slot_index`.
114    /// The borrow-model home of the node's metadata perm.
115    pub open spec fn meta_perm_of(
116        self,
117        regions: MetaRegionOwners,
118    ) -> vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<PageTablePageMeta<C>>> {
119        vstd_extra::cast_ptr::PointsTo::new_spec(
120            regions.slots[self.slot_index],
121            regions.slot_owners[self.slot_index].inner_perms,
122        )
123    }
124
125    /// Regions-tied invariants that used to live in `NodeOwner::inv()` via
126    /// the now-removed `meta_perm` field. Establishes the bridge between
127    /// the NodeOwner and the slot perm parked in regions.
128    pub open spec fn metaregion_sound_node(self, regions: MetaRegionOwners) -> bool {
129        let idx = self.slot_index;
130        &&& regions.slots.contains_key(idx)
131        &&& self.meta_perm_of(regions).is_init()
132        &&& self.meta_perm_of(regions).wf(&self.meta_perm_of(regions).inner_perms)
133        &&& self.meta_perm_of(regions).value().metadata.wf(self.meta_own)
134        &&& self.level == self.meta_perm_of(regions).value().metadata.level
135        &&& self.meta_own.nr_children.id() == self.meta_perm_of(
136            regions,
137        ).value().metadata.nr_children.id()
138    }
139}
140
141impl<C: PageTableConfig> NodeOwner<C> {
142    // TODO: this is a bizzare structure; `set_children_perm` needs to actually be
143    // defined to satisfy the axiom, which can then be deleted.
144    pub uninterp spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
145
146    #[verifier::external_body]
147    pub axiom fn set_children_perm_axiom(self, idx: usize, pte: C::E)
148        requires
149            self.inv(),
150            idx < NR_ENTRIES,
151        ensures
152            self.set_children_perm(idx, pte).inv(),
153            self.set_children_perm(idx, pte).meta_own == self.meta_own,
154            self.set_children_perm(idx, pte).slot_index == self.slot_index,
155            self.set_children_perm(idx, pte).level == self.level,
156            self.set_children_perm(idx, pte).tree_level == self.tree_level,
157            self.set_children_perm(idx, pte).children_perm.addr() == self.children_perm.addr(),
158            self.set_children_perm(idx, pte).children_perm.value()
159                == self.children_perm.value().update(idx as int, pte),
160    ;
161
162    /// If any slot in `children_perm` holds a non-present PTE, then
163    /// `nr_children < NR_ENTRIES`.
164    ///
165    /// Axiomatizes the intended meaning of `nr_children`: it counts the
166    /// number of *present* PTEs in the node. When at least one slot is
167    /// absent, the count must be strictly less than the maximum. This
168    /// sidesteps a full `nr_children == count(present PTEs)` invariant
169    /// (which would thread through every PTE mutation); the axiom instead
170    /// exposes the single boundary fact that `Entry::replace` needs when
171    /// incrementing the counter.
172    pub axiom fn nr_children_absent_slot_bound(self, idx: usize)
173        requires
174            self.inv(),
175            idx < NR_ENTRIES,
176            !self.children_perm.value()[idx as int].is_present(),
177        ensures
178            self.meta_own.nr_children.value() < NR_ENTRIES,
179    ;
180
181    /// If any slot in `children_perm` holds a present PTE, then
182    /// `nr_children > 0`. Dual of [`Self::nr_children_absent_slot_bound`];
183    /// used by `Entry::replace` when decrementing the counter.
184    pub axiom fn nr_children_present_slot_bound(self, idx: usize)
185        requires
186            self.inv(),
187            idx < NR_ENTRIES,
188            self.children_perm.value()[idx as int].is_present(),
189        ensures
190            self.meta_own.nr_children.value() > 0,
191    ;
192}
193
194impl<'rcu, C: PageTableConfig> NodeOwner<C> {
195    pub open spec fn relate_guard(self, guard: PageTableGuard<'rcu, C>) -> bool {
196        &&& guard.inner.inner@.ptr.addr() == self.meta_addr_self()
197        &&& guard.inner.inner@.wf(self)
198    }
199}
200
201pub ghost struct NodeModel<C: PageTableConfig> {
202    pub level: PagingLevel,
203    pub _phantom: core::marker::PhantomData<C>,
204}
205
206impl<C: PageTableConfig> Inv for NodeModel<C> {
207    open spec fn inv(self) -> bool {
208        true
209    }
210}
211
212impl<C: PageTableConfig> View for NodeOwner<C> {
213    type V = NodeModel<C>;
214
215    open spec fn view(&self) -> <Self as View>::V {
216        NodeModel { level: self.level, _phantom: core::marker::PhantomData }
217    }
218}
219
220impl<C: PageTableConfig> InvView for NodeOwner<C> {
221    proof fn view_preserves_inv(self) {
222    }
223}
224
225impl<C: PageTableConfig> OwnerOf for PageTableNode<C> {
226    type Owner = NodeOwner<C>;
227
228    open spec fn wf(self, owner: Self::Owner) -> bool {
229        &&& self.ptr.addr() == owner.meta_addr_self()
230    }
231}
232
233impl<C: PageTableConfig> PageTableNode<C> {
234    pub open spec fn invariants(self, owner: NodeOwner<C>) -> bool {
235        &&& owner.inv()
236        &&& self.wf(
237            owner,
238        )
239        //        &&& owner.meta_perm.wf(&owner.meta_perm.inner_perms)
240        //        &&& owner.meta_perm.addr() == self.ptr.addr()
241        //        &&& owner.meta_perm.addr() == self.ptr.addr()
242
243    }
244}
245
246} // verus!
ostd/specs/mm/page_table/node/owners.rs

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