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

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

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