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

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

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