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::arch::mm::PagingConsts;
8use crate::mm::frame::meta::mapping::meta_to_frame;
9use crate::mm::frame::meta::{META_SLOT_SIZE, MetaSlot};
10use crate::mm::kspace::FRAME_METADATA_RANGE;
11use crate::mm::kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR};
12use crate::mm::paddr_to_vaddr;
13use crate::mm::page_table::PageTableGuard;
14use crate::mm::page_table::*;
15use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
16use crate::specs::arch::{MAX_PADDR, NR_ENTRIES, NR_LEVELS};
17use crate::specs::mm::frame::mapping::{frame_to_index, max_meta_slots, meta_addr};
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;
23
24use vstd_extra::ownership::*;
25
26verus! {
27
28// ─── Present-PTE counting ──────────────────────────────────────────────────────
29// The intended meaning of `nr_children`: the number of *present* PTEs in the
30// node's `children_perm` array. `metaregion_sound_node` ties `nr_children` to
31// `count_present(children_perm.value())` (a settled-node invariant), which lets
32// the `nr_children_*_slot_bound` boundary facts be proven rather than axiomatized.
33/// Number of present PTEs among the first `n` entries of `s`.
34pub open spec fn count_present_upto<E: PageTableEntryTrait>(s: Seq<E>, n: int) -> int
35    decreases n,
36{
37    if n <= 0 {
38        0
39    } else {
40        count_present_upto(s, n - 1) + if s[n - 1].is_present() {
41            1int
42        } else {
43            0int
44        }
45    }
46}
47
48/// Number of present PTEs in `s`.
49pub open spec fn count_present<E: PageTableEntryTrait>(s: Seq<E>) -> int {
50    count_present_upto(s, s.len() as int)
51}
52
53/// `count_present_upto` is between `0` and `n`.
54pub proof fn lemma_count_present_upto_bound<E: PageTableEntryTrait>(s: Seq<E>, n: int)
55    requires
56        0 <= n,
57    ensures
58        0 <= count_present_upto(s, n) <= n,
59    decreases n,
60{
61    if n > 0 {
62        lemma_count_present_upto_bound(s, n - 1);
63    }
64}
65
66/// An absent slot below `n` makes the count strictly less than `n`.
67pub proof fn lemma_count_present_upto_absent<E: PageTableEntryTrait>(s: Seq<E>, n: int, idx: int)
68    requires
69        0 <= idx < n,
70        !s[idx].is_present(),
71    ensures
72        count_present_upto(s, n) < n,
73    decreases n,
74{
75    lemma_count_present_upto_bound(s, n - 1);
76    if idx < n - 1 {
77        lemma_count_present_upto_absent(s, n - 1, idx);
78    }
79}
80
81/// A present slot below `n` makes the count at least `1`.
82pub proof fn lemma_count_present_upto_present<E: PageTableEntryTrait>(s: Seq<E>, n: int, idx: int)
83    requires
84        0 <= idx < n,
85        s[idx].is_present(),
86    ensures
87        count_present_upto(s, n) >= 1,
88    decreases n,
89{
90    lemma_count_present_upto_bound(s, n - 1);
91    if idx < n - 1 {
92        lemma_count_present_upto_present(s, n - 1, idx);
93    }
94}
95
96/// Updating slot `idx` (with `idx < n`) shifts the count by the change in that
97/// slot's present-indicator.
98pub proof fn lemma_count_present_upto_update<E: PageTableEntryTrait>(
99    s: Seq<E>,
100    n: int,
101    idx: int,
102    pte: E,
103)
104    requires
105        0 <= idx < n <= s.len(),
106    ensures
107        count_present_upto(s.update(idx, pte), n) == count_present_upto(s, n) - (
108        if s[idx].is_present() {
109            1int
110        } else {
111            0int
112        }) + (if pte.is_present() {
113            1int
114        } else {
115            0int
116        }),
117    decreases n,
118{
119    let s2 = s.update(idx, pte);
120    if n - 1 == idx {
121        // The first `idx` entries are unchanged.
122        assert(count_present_upto(s2, n - 1) == count_present_upto(s, n - 1)) by {
123            lemma_count_present_upto_unchanged(s, s2, n - 1, idx);
124        }
125    } else {
126        lemma_count_present_upto_update(s, n - 1, idx, pte);
127    }
128}
129
130/// A zero present-count up to `n` means every slot below `n` is absent.
131pub proof fn lemma_count_present_upto_zero_all_absent<E: PageTableEntryTrait>(s: Seq<E>, n: int)
132    requires
133        count_present_upto(s, n) == 0,
134        0 <= n,
135    ensures
136        forall|k: int| 0 <= k < n ==> !#[trigger] s[k].is_present(),
137    decreases n,
138{
139    if n > 0 {
140        lemma_count_present_upto_bound(s, n - 1);
141        lemma_count_present_upto_zero_all_absent(s, n - 1);
142    }
143}
144
145/// If two sequences agree on `[0, n)`, their counts up to `n` are equal.
146pub proof fn lemma_count_present_upto_unchanged<E: PageTableEntryTrait>(
147    s: Seq<E>,
148    s2: Seq<E>,
149    n: int,
150    idx: int,
151)
152    requires
153        0 <= n <= idx,
154        forall|k: int| 0 <= k < n ==> s[k] == s2[k],
155    ensures
156        count_present_upto(s2, n) == count_present_upto(s, n),
157    decreases n,
158{
159    if n > 0 {
160        lemma_count_present_upto_unchanged(s, s2, n - 1, idx);
161    }
162}
163
164pub tracked struct PageMetaOwner {
165    pub nr_children: pcell_maybe_uninit::PointsTo<u16>,
166    pub stray: pcell_maybe_uninit::PointsTo<bool>,
167}
168
169impl Inv for PageMetaOwner {
170    open spec fn inv(self) -> bool {
171        &&& self.nr_children.is_init()
172        &&& 0 <= self.nr_children.value() <= NR_ENTRIES
173        &&& self.stray.is_init()
174    }
175}
176
177pub ghost struct PageMetaModel {
178    pub nr_children: u16,
179    pub stray: bool,
180}
181
182impl Inv for PageMetaModel {
183    open spec fn inv(self) -> bool {
184        true
185    }
186}
187
188impl View for PageMetaOwner {
189    type V = PageMetaModel;
190
191    open spec fn view(&self) -> <Self as View>::V {
192        PageMetaModel { nr_children: self.nr_children.value(), stray: self.stray.value() }
193    }
194}
195
196impl InvView for PageMetaOwner {
197    proof fn view_preserves_inv(self) {
198    }
199}
200
201impl<C: PageTableConfig> OwnerOf for PageTablePageMeta<C> {
202    type Owner = PageMetaOwner;
203
204    open spec fn wf(self, owner: Self::Owner) -> bool {
205        &&& self.nr_children.id() == owner.nr_children.id()
206        &&& self.stray.id() == owner.stray.id()
207        &&& 0 <= owner.nr_children.value() <= NR_ENTRIES
208    }
209}
210
211/// # Verification Design
212/// The owner type for a page table node. It contains:
213/// - `meta_own`, a `PageMetaOwner`, which holds the permissions for node-specific
214///   metadata fields, `nr_children` and `stray`
215/// - `children_perm` is an array permission for the underlying frame in which the node
216///   is allocated, interpreted as an array of `NR_ENTRIES` page table entries
217/// - `slot_index` identifies the underlying frame's index in the metadata region
218/// - Each node is a page table with a level between 1 and 4 (on x86); `level` tracks
219///   the level of this node.
220/// - `tree_level` is the level field of the `ghost_tree::Node` that carries this object.
221///   Carried here for convenience, though it can be computed from `level`.
222pub tracked struct NodeOwner<C: PageTableConfig> {
223    pub meta_own: PageMetaOwner,
224    pub children_perm: array_ptr::PointsTo<C::E, NR_ENTRIES>,
225    pub level: PagingLevel,
226    pub tree_level: int,
227    pub slot_index: usize,
228}
229
230impl<C: PageTableConfig> Inv for NodeOwner<C> {
231    open spec fn inv(self) -> bool {
232        &&& self.meta_own.inv()
233        &&& 0 <= self.meta_own.nr_children.value() <= NR_ENTRIES
234        &&& 1 <= self.level <= NR_LEVELS
235        &&& self.children_perm.is_init_all()
236        &&& self.children_perm.addr() == paddr_to_vaddr(meta_to_frame(meta_addr(self.slot_index)))
237        &&& self.tree_level == INC_LEVELS - self.level - 1
238        &&& self.slot_index < max_meta_slots() as usize
239        &&& FRAME_METADATA_RANGE.start <= meta_addr(self.slot_index) < FRAME_METADATA_RANGE.end
240        &&& meta_addr(self.slot_index) % META_SLOT_SIZE == 0
241        &&& meta_to_frame(meta_addr(self.slot_index)) < VMALLOC_BASE_VADDR
242            - LINEAR_MAPPING_BASE_VADDR
243        &&& meta_to_frame(meta_addr(self.slot_index)) < MAX_PADDR
244        &&& meta_to_frame(meta_addr(self.slot_index)) == self.children_perm.addr()
245        &&& self.slot_index == frame_to_index(meta_to_frame(meta_addr(self.slot_index)))
246    }
247}
248
249impl<C: PageTableConfig> NodeOwner<C> {
250    /// The meta address of this node's slot, computed from `slot_index`.
251    /// Always equals `self.meta_perm.addr()` under `inv()`.
252    pub open spec fn meta_addr_self(self) -> Vaddr {
253        meta_addr(self.slot_index)
254    }
255
256    /// Reconstructs a metadata cast_ptr from `regions` at `self.slot_index`.
257    /// The borrow-model home of the node's metadata perm.
258    pub open spec fn meta_perm_of(
259        self,
260        regions: MetaRegionOwners,
261    ) -> vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<PageTablePageMeta<C>>> {
262        vstd_extra::cast_ptr::PointsTo::new_spec(
263            regions.slots[self.slot_index],
264            regions.slot_owners[self.slot_index].inner_perms,
265        )
266    }
267
268    /// Regions-tied invariants that used to live in `NodeOwner::inv()` via
269    /// the now-removed `meta_perm` field. Establishes the bridge between
270    /// the NodeOwner and the slot perm parked in regions.
271    pub open spec fn metaregion_sound_node(self, regions: MetaRegionOwners) -> bool {
272        let idx = self.slot_index;
273        &&& regions.slots.contains_key(idx)
274        &&& self.meta_perm_of(regions).is_init()
275        &&& self.meta_perm_of(regions).wf(&self.meta_perm_of(regions).inner_perms)
276        &&& self.meta_perm_of(regions).value().metadata.wf(self.meta_own)
277        &&& self.level == self.meta_perm_of(regions).value().metadata.level
278        &&& self.meta_own.nr_children.id() == self.meta_perm_of(
279            regions,
280        ).value().metadata.nr_children.id()
281        // A page-table node's slot is tracked with `PageTable` usage (set at
282        // allocation via `get_node_from_unused_spec`). This discriminates node
283        // slots from data-frame slots (`Frame`/MMIO) by `usage` alone, so a
284        // freshly-allocated node (whose slot was `UNUSED`) can't collide with an
285        // existing live node — giving `alloc_if_none`/`split` the parent≠child
286        // slot distinctness without a PointsTo-linearity axiom.
287        &&& regions.slot_owners[self.slot_index].usage
288            == PageUsage::PageTable
289        // `nr_children` counts the present PTEs in `children_perm`. A settled-node
290        // invariant (it is momentarily broken mid-`replace`/`alloc_if_none`, between
291        // the PTE write and the counter update, which is why it lives here rather
292        // than in `inv()`). Lets `nr_children_*_slot_bound` be proven, not axiomatized.
293        &&& self.count_consistent()
294    }
295
296    /// `nr_children` equals the number of present PTEs in `children_perm`.
297    /// Held by a settled node (see `metaregion_sound_node`'s use site).
298    pub open spec fn count_consistent(self) -> bool {
299        self.meta_own.nr_children.value() == count_present(self.children_perm.value())
300    }
301}
302
303impl<C: PageTableConfig> NodeOwner<C> {
304    // TODO: this is a bizzare structure; `set_children_perm` needs to actually be
305    // defined to satisfy the axiom, which can then be deleted.
306    pub uninterp spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
307
308    #[verifier::external_body]
309    pub axiom fn set_children_perm_axiom(self, idx: usize, pte: C::E)
310        requires
311            self.inv(),
312            idx < NR_ENTRIES,
313        ensures
314            self.set_children_perm(idx, pte).inv(),
315            self.set_children_perm(idx, pte).meta_own == self.meta_own,
316            self.set_children_perm(idx, pte).slot_index == self.slot_index,
317            self.set_children_perm(idx, pte).level == self.level,
318            self.set_children_perm(idx, pte).tree_level == self.tree_level,
319            self.set_children_perm(idx, pte).children_perm.addr() == self.children_perm.addr(),
320            self.set_children_perm(idx, pte).children_perm.value()
321                == self.children_perm.value().update(idx as int, pte),
322    ;
323
324    /// If a slot in `children_perm` holds a non-present PTE, then
325    /// `nr_children < NR_ENTRIES`. Proven (no longer axiomatized) from the
326    /// `count_consistent` invariant: `nr_children` counts present PTEs, and an
327    /// absent slot means not all `NR_ENTRIES` slots are present.
328    pub proof fn nr_children_absent_slot_bound(self, idx: usize)
329        requires
330            self.inv(),
331            self.count_consistent(),
332            self.children_perm.value().len() == NR_ENTRIES,
333            idx < NR_ENTRIES,
334            !self.children_perm.value()[idx as int].is_present(),
335        ensures
336            self.meta_own.nr_children.value() < NR_ENTRIES,
337    {
338        lemma_count_present_upto_absent(self.children_perm.value(), NR_ENTRIES as int, idx as int);
339    }
340
341    /// If a slot in `children_perm` holds a present PTE, then `nr_children > 0`.
342    /// Dual of [`Self::nr_children_absent_slot_bound`]; proven from
343    /// `count_consistent`.
344    pub proof fn nr_children_present_slot_bound(self, idx: usize)
345        requires
346            self.inv(),
347            self.count_consistent(),
348            self.children_perm.value().len() == NR_ENTRIES,
349            idx < NR_ENTRIES,
350            self.children_perm.value()[idx as int].is_present(),
351        ensures
352            self.meta_own.nr_children.value() > 0,
353    {
354        lemma_count_present_upto_present(self.children_perm.value(), NR_ENTRIES as int, idx as int);
355    }
356}
357
358impl<'rcu, C: PageTableConfig> NodeOwner<C> {
359    pub open spec fn relate_guard(self, guard: PageTableGuard<'rcu, C>) -> bool {
360        &&& guard.inner.inner@.ptr.addr() == self.meta_addr_self()
361        &&& guard.inner.inner@.wf(self)
362    }
363}
364
365pub ghost struct NodeModel<C: PageTableConfig> {
366    pub level: PagingLevel,
367    pub _phantom: core::marker::PhantomData<C>,
368}
369
370impl<C: PageTableConfig> Inv for NodeModel<C> {
371    open spec fn inv(self) -> bool {
372        true
373    }
374}
375
376impl<C: PageTableConfig> View for NodeOwner<C> {
377    type V = NodeModel<C>;
378
379    open spec fn view(&self) -> <Self as View>::V {
380        NodeModel { level: self.level, _phantom: core::marker::PhantomData }
381    }
382}
383
384impl<C: PageTableConfig> InvView for NodeOwner<C> {
385    proof fn view_preserves_inv(self) {
386    }
387}
388
389impl<C: PageTableConfig> OwnerOf for PageTableNode<C> {
390    type Owner = NodeOwner<C>;
391
392    open spec fn wf(self, owner: Self::Owner) -> bool {
393        &&& self.ptr.addr() == owner.meta_addr_self()
394    }
395}
396
397impl<C: PageTableConfig> PageTableNode<C> {
398    pub open spec fn invariants(self, owner: NodeOwner<C>) -> bool {
399        &&& owner.inv()
400        &&& self.wf(
401            owner,
402        )
403        //        &&& owner.meta_perm.wf(&owner.meta_perm.inner_perms)
404        //        &&& owner.meta_perm.addr() == self.ptr.addr()
405        //        &&& owner.meta_perm.addr() == self.ptr.addr()
406
407    }
408}
409
410} // verus!
ostd/specs/mm/page_table/node/owners.rs

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