ostd/mm/page_table/node/
entry.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module provides accessors to the page table entries in a node.
3use vstd::prelude::*;
4
5use vstd::simple_pptr::{self, PPtr, PointsTo};
6
7use vstd_extra::cast_ptr;
8use vstd_extra::drop_tracking::ManuallyDrop;
9use vstd_extra::ghost_tree::*;
10use vstd_extra::ownership::*;
11
12use crate::mm::frame::meta::mapping::{frame_to_index, frame_to_meta, meta_to_frame};
13use crate::mm::frame::{Frame, FrameRef};
14use crate::mm::page_table::*;
15use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
16use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
17use crate::specs::arch::paging_consts::PagingConsts;
18use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, REF_COUNT_UNUSED};
19use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
20use crate::specs::mm::page_table::{PageTableOwner, INC_LEVELS};
21use crate::specs::task::InAtomicMode;
22
23use core::marker::PhantomData;
24use core::ops::Deref;
25
26use crate::{
27    mm::{nr_subpage_per_huge, page_prop::PageProperty},
28    //    sync::RcuDrop,
29    //    task::atomic_mode::InAtomicMode,
30};
31
32use super::*;
33
34verus! {
35
36/// A reference to a page table node.
37pub type PageTableNodeRef<'a, C> = FrameRef<'a, PageTablePageMeta<C>>;
38
39/// A guard that holds the lock of a page table node.
40pub struct PageTableGuard<'rcu, C: PageTableConfig> {
41    pub inner: PageTableNodeRef<'rcu, C>,
42}
43
44impl<'rcu, C: PageTableConfig> Deref for PageTableGuard<'rcu, C> {
45    type Target = PageTableNodeRef<'rcu, C>;
46
47    #[verus_spec(ensures returns self.inner)]
48    fn deref(&self) -> &Self::Target {
49        &self.inner
50    }
51}
52
53pub struct Entry<'rcu, C: PageTableConfig> {
54    /// The page table entry.
55    ///
56    /// We store the page table entry here to optimize the number of reads from
57    /// the node. We cannot hold a `&mut E` reference to the entry because that
58    /// other CPUs may modify the memory location for accessed/dirty bits. Such
59    /// accesses will violate the aliasing rules of Rust and cause undefined
60    /// behaviors.
61    ///
62    /// # Verification Design
63    /// The concrete value of a PTE is specific to the architecture and the page table configuration,
64    /// represented by the type `C::E`. We represent its value as an abstract [`EntryOwner`], which is
65    /// connected to the concrete value by `match_pte`. The `EntryOwner` is well-formed with respect to
66    /// `Entry` if it is related to the concrete value by `match_pte`.
67    ///
68    /// An `Entry` can be thought of as a mutable handle to the concrete value of the PTE.
69    /// The `node` field points (with a level of indirection) to the node that contains the entry,
70    /// `index` provides the offset, and the `pte` is current value. Only one `Entry` can exist for
71    /// a given node at any given time.
72    pub pte: C::E,
73    /// The index of the entry in the node.
74    pub idx: usize,
75    /// The node that contains the entry. In the original Rust this is a `&mut PageTableGuard`; the PPtr
76    /// type is handling the mutable reference because Verus does not yet support storing such a reference
77    /// in a struct.
78    pub node: PPtr<PageTableGuard<'rcu, C>>,
79}
80
81impl<'rcu, C: PageTableConfig> Entry<'rcu, C> {
82    pub open spec fn new_spec(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self {
83        Self { pte, idx, node }
84    }
85
86    #[verifier::when_used_as_spec(new_spec)]
87    pub fn new(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self {
88        Self { pte, idx, node }
89    }
90}
91
92#[verus_verify]
93impl<'a, 'rcu, C: PageTableConfig> Entry<'rcu, C> {
94    /// Returns if the entry does not map to anything.
95    #[verus_spec(r =>
96        with Tracked(owner): Tracked<&EntryOwner<C>>,
97        requires
98            self.wf(*owner),
99            owner.inv(),
100        returns owner.is_absent(),
101    )]
102    pub(in crate::mm) fn is_none(&self) -> bool {
103        !self.pte.is_present()
104    }
105
106    /// Returns if the entry maps to a page table node.
107    #[verus_spec(
108        with Tracked(owner): Tracked<EntryOwner<C>>,
109            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
110            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
111    )]
112    pub(in crate::mm) fn is_node(&self) -> bool
113        requires
114            owner.inv(),
115            self.wf(owner),
116            guard_perm.addr() == self.node.addr(),
117            parent_owner.relate_guard_perm(*guard_perm),
118            parent_owner.inv(),
119            parent_owner.level == owner.parent_level,
120        returns
121            owner.is_node(),
122    {
123        let guard = self.node.borrow(Tracked(guard_perm));
124
125        self.pte.is_present() && !self.pte.is_last(
126            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
127            guard.level(),
128        )
129    }
130
131    /// Gets a reference to the child.
132    #[verus_spec(
133        with Tracked(owner): Tracked<&EntryOwner<C>>,
134            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
135            Tracked(regions): Tracked<&mut MetaRegionOwners>,
136            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
137    )]
138    pub(in crate::mm) fn to_ref(&self) -> (res: ChildRef<'rcu, C>)
139        requires
140            self.invariants(*owner, *old(regions)),
141            self.node_matching(*owner, *parent_owner, *guard_perm),
142            !owner.in_scope,
143        ensures
144            res.invariants(*owner, *final(regions)),
145            final(regions).slot_owners =~= old(regions).slot_owners,
146            forall |k: usize| old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(k),
147            forall |k: usize| old(regions).slots.contains_key(k) ==> old(regions).slots[k] == #[trigger] final(regions).slots[k],
148            final(regions).inv(),
149    {
150        let guard = self.node.borrow(Tracked(guard_perm));
151
152        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
153        let level = guard.level();
154
155        // SAFETY:
156        //  - The PTE outlives the reference (since we have `&self`).
157        //  - The level matches the current node.
158        #[verus_spec(with Tracked(regions), Tracked(owner))]
159        let res = ChildRef::from_pte(&self.pte, level);
160
161        res
162    }
163
164    /// Operates on the mapping properties of the entry.
165    ///
166    /// It only modifies the properties if the entry is present.
167    ///
168    /// # Verified Properties
169    /// ## Preconditions
170    /// - **Safety Invariants**: The entry must satisfy the relevant safety invariants.
171    /// - **Safety**: The caller must provide a valid guard permission matching `guard_perm`, and it must be guarding the
172    /// correct parent node.
173    /// - **Safety**: The entry must be a frame.
174    /// ## Postconditions
175    /// - **Safety Invariants**: The entry continues to satisfy the relevant safety invariants.
176    /// - **Safety**: The guard permission is preserved.
177    /// - **Correctness**: The entry's permissions are updated by `op`
178    /// ## Safety
179    /// - The entry is updated in place, only changing its properties, so the metadata is unchanged.
180    /// That's why we don't take a `MetaRegionOwners` argument. It means that all invariants will be preserved.
181    #[verus_spec(
182        with Tracked(owner) : Tracked<&mut EntryOwner<C>>,
183            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
184            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>,
185    )]
186    pub(in crate::mm) fn protect(&mut self, op: impl FnOnce(PageProperty) -> PageProperty)
187        requires
188            old(owner).inv(),
189            old(self).wf(*old(owner)),
190            old(self).node_matching(*old(owner), *old(parent_owner), *old(guard_perm)),
191            op.requires((old(self).pte.prop(),)),
192            old(owner).is_frame(),
193        ensures
194            final(owner).inv(),
195            final(self).wf(*final(owner)),
196            final(self).node_matching(*final(owner), *final(parent_owner), *final(guard_perm)),
197            final(self).parent_perms_preserved(*old(parent_owner), *final(parent_owner), *old(guard_perm), *final(guard_perm)),
198            final(owner).is_frame(),
199            final(owner).frame.unwrap().mapped_pa == old(owner).frame.unwrap().mapped_pa,
200            final(owner).path == old(owner).path,
201            final(owner).parent_level == old(owner).parent_level,
202            final(owner).in_scope == old(owner).in_scope,
203            final(self).idx == old(self).idx,
204            old(self).pte.is_present() ==> op.ensures((old(owner).frame.unwrap().prop,), final(owner).frame.unwrap().prop),
205    {
206        let ghost pte0 = self.pte;
207
208        if !self.pte.is_present() {
209            return ;
210        }
211        let prop = self.pte.prop();
212        let new_prop = op(prop);
213
214        /*if prop == new_prop {
215            return;
216        }*/
217
218        proof {
219            self.pte.set_prop_properties(new_prop);
220        }
221        self.pte.set_prop(new_prop);
222
223        let mut guard = self.node.take(Tracked(guard_perm));
224
225        // SAFETY:
226        //  1. The index is within the bounds.
227        //  2. We replace the PTE with a new one, which differs only in
228        //     `PageProperty`, so the level still matches the current
229        //     page table node.
230        #[verus_spec(with Tracked(parent_owner))]
231        guard.write_pte(self.idx, self.pte);
232
233        proof {
234            let tracked mut frame_owner = owner.frame.tracked_take();
235            frame_owner.prop = new_prop;
236            owner.frame = Some(frame_owner);
237        }
238        assert(owner.match_pte(self.pte, owner.parent_level));
239
240        self.node.put(Tracked(guard_perm), guard);
241    }
242
243    /// Replaces the entry with a new child.
244    ///
245    /// The old child is returned.
246    ///
247    /// # Verified Properties
248    /// ## Preconditions
249    /// - **Safety Invariants**: Both old and new owners must satisfy the respective safety invariants for an [Entry](Entry::invariants)
250    /// and a [Child](Child::invariants).
251    /// - **Safety**: The caller must provide valid owners for all objects, and for the parent node where the entry
252    /// is being replaced. The parent node must have a valid guard permission.
253    /// - **Correctness**: The new child must be compatible with the old, for instance by having the same level.
254    /// ## Postconditions
255    /// - **Safety Invariants**: The old and new owners will satisfy the safety invariants for an [Entry](Entry::invariants)
256    /// and a [Child](Child::invariants), but they have changed positions.
257    /// - **Safety**: Safety properties that hold across the page table's tree structure are preserved
258    /// everywhere except for the entry being replaced.
259    /// - **Correctness**: The entry will match the argument, and the returned child will match the entry that was replaced.
260    /// ## Safety
261    /// - The invariants ensure that the entry is appropriately aligned and its index is within bounds.
262    /// - The transformation from child to entry ensures that the tree now owns the updated entry.
263    #[verus_spec(
264        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
265            Tracked(owner): Tracked<&mut EntryOwner<C>>,
266            Tracked(new_owner): Tracked<&mut EntryOwner<C>>,
267            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
268            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>,
269    )]
270    pub(in crate::mm) fn replace(&mut self, new_child: Child<C>) -> (res: Child<C>)
271        requires
272            old(self).invariants(*old(owner), *old(regions)),
273            new_child.invariants(*old(new_owner), *old(regions)),
274            old(self).node_matching(*old(owner), *old(parent_owner), *old(guard_perm)),
275            old(self).new_owner_compatible(new_child, *old(owner), *old(new_owner), *old(regions)),
276            !old(owner).in_scope,
277        ensures
278            final(self).invariants(*final(new_owner), *final(regions)),
279            res.invariants(*final(owner), *final(regions)),
280            final(self).node_matching(*final(new_owner), *final(parent_owner), *final(guard_perm)),
281            final(self).idx == old(self).idx,
282            *final(owner) == old(owner).from_pte_owner_spec(),
283            *final(new_owner) == old(new_owner).into_pte_owner_spec(),
284            Self::metaregion_sound_neq_preserved(*old(owner), *final(new_owner), *old(regions), *final(regions)),
285            !final(new_owner).is_node() ==>
286                Self::metaregion_sound_neq_old_preserved(*old(owner), *old(regions), *final(regions)),
287            (!old(owner).is_node() && !final(new_owner).is_node()) ==>
288                Self::metaregion_sound_preserved(*old(regions), *final(regions)),
289            final(new_owner).is_node() && !final(new_owner).is_absent() ==>
290                PageTableOwner::<C>::path_tracked_pred(*final(regions))(*final(new_owner), final(new_owner).path),
291            final(self).parent_perms_preserved(*old(parent_owner), *final(parent_owner), *final(guard_perm), *old(guard_perm)),
292            // paths_in_pt changes when new owner is a node; preserved otherwise.
293            forall|idx: usize| #![trigger final(regions).slot_owners[idx].paths_in_pt]
294                (!final(new_owner).is_node() || final(new_owner).is_absent()
295                    || idx != frame_to_index(final(new_owner).meta_slot_paddr().unwrap()))
296                    ==> final(regions).slot_owners[idx].paths_in_pt == old(regions).slot_owners[idx].paths_in_pt,
297            // slots: monotonic (from_pte may add; into_pte doesn't remove for non-nodes).
298            forall|k: usize| old(regions).slots.contains_key(k)
299                ==> #[trigger] final(regions).slots.contains_key(k),
300            // When both old and new are not nodes: from_pte/into_pte are identity.
301            (!old(owner).is_node() && !final(new_owner).is_node()) ==> {
302                &&& final(regions).slots == old(regions).slots
303                &&& forall|i: usize| #![trigger final(regions).slot_owners[i]]
304                    final(regions).slot_owners[i] == old(regions).slot_owners[i]
305            },
306            // When old child is absent and new child is not a node: slots values unchanged.
307            (old(owner).is_absent() && !final(new_owner).is_node()) ==>
308                forall|k: usize| old(regions).slots.contains_key(k)
309                    ==> old(regions).slots[k] == #[trigger] final(regions).slots[k],
310            Self::replace_nonpanic_condition(*old(parent_owner), *old(new_owner)),
311    {
312        let ghost new_idx = frame_to_index(new_owner.meta_slot_paddr().unwrap());
313        let ghost old_idx = frame_to_index(owner.meta_slot_paddr().unwrap());
314
315        let mut guard = self.node.take(Tracked(guard_perm));
316
317        match &new_child {
318            Child::PageTable(node) => {
319                #[cfg(feature = "allow_panic")]
320                assert!(node.level() == guard.level() - 1);
321            }
322            Child::Frame(_, level, _) => {
323                #[cfg(feature = "allow_panic")]
324                assert!(*level == guard.level());
325            }
326            Child::None => {}
327        }
328
329        // SAFETY:
330        //  - The PTE is not referenced by other `ChildRef`s (since we have `&mut self`).
331        //  - The level matches the current node.
332        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
333        let level = guard.level();
334
335        #[verus_spec(with Tracked(regions), Tracked(owner))]
336        let old_child = Child::from_pte(self.pte, level);
337
338        let ghost regions_after_from = *regions;
339
340        assert(new_owner.is_node() ==> regions.slots.contains_key(frame_to_index(new_owner.meta_slot_paddr().unwrap())));
341
342        if old_child.is_none() && !new_child.is_none() {
343            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
344            let nr_children = guard.nr_children_mut();
345            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
346            proof {
347                parent_owner.nr_children_absent_slot_bound(self.idx);
348            }
349            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
350        } else if !old_child.is_none() && new_child.is_none() {
351            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
352            let nr_children = guard.nr_children_mut();
353            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
354            proof {
355                parent_owner.nr_children_present_slot_bound(self.idx);
356            }
357            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp - 1);
358        }
359        proof {
360            assert(owner.metaregion_sound(*regions));
361        }
362
363        #[verus_spec(with Tracked(new_owner), Tracked(regions))]
364        let new_pte = new_child.into_pte();
365
366        let ghost regions_after_into = *regions;
367
368        proof {
369            assert(owner.metaregion_sound(*regions));
370        }
371
372        // SAFETY:
373        //  1. The index is within the bounds.
374        //  2. The new PTE is a valid child whose level matches the current page table node.
375        //  3. The ownership of the child is passed to the page table node.
376        #[verus_spec(with Tracked(parent_owner))]
377        guard.write_pte(self.idx, new_pte);
378
379        self.node.put(Tracked(guard_perm), guard);
380
381        self.pte = new_pte;
382
383        proof {
384            // Install new entry's path into its slot's paths_in_pt.
385            // Nodes: singleton overwrite (tree enforces unique node path).
386            // Frames: their path is installed by the caller BEFORE calling replace,
387            //   so that `new_child.invariants` — which now requires
388            //   `paths_in_pt.contains(new.path)` for the frame arm — is satisfied on
389            //   entry. See the huge-page split and `replace_cur_entry` caller sites.
390            if new_owner.is_node() {
391                let paddr = new_owner.meta_slot_paddr().unwrap();
392                regions.inv_implies_correct_addr(paddr);
393
394                let tracked mut new_meta_slot = regions.slot_owners.tracked_remove(new_idx);
395                new_meta_slot.paths_in_pt = set![new_owner.path];
396                regions.slot_owners.tracked_insert(new_idx, new_meta_slot);
397            }
398            owner.in_scope = true;
399        }
400
401        assert(Self::metaregion_sound_neq_preserved(*old(owner), *new_owner, *old(regions), *regions));
402
403        proof {
404            // When both old and new are not nodes:
405            // from_pte/into_pte are identity, no slot_owners change. Regions unchanged.
406            if !old(owner).is_node() && !new_owner.is_node() {
407                // slot_owners and slots are identical → metaregion_sound trivially preserved.
408            }
409        }
410
411        proof {
412            if new_owner.is_node() || new_owner.is_frame() {
413                let paddr = new_owner.meta_slot_paddr().unwrap();
414                regions.inv_implies_correct_addr(paddr);
415            }
416            // Sub-page validity for new_owner (if a huge frame): preserved because
417            // replace only modifies slots/paths_in_pt at new_owner's own slot, not
418            // at sub-page slots (which have different indices for j > 0).
419            if new_owner.is_frame() && new_owner.parent_level > 1 {
420                assert(new_owner.frame_sub_pages_valid(*regions));
421            }
422            if owner.is_frame() && owner.parent_level > 1 {
423                assert(owner.frame_sub_pages_valid(*regions));
424            }
425        }
426
427        old_child
428    }
429
430    /// Allocates a new child page table node and replaces the entry with it.
431    ///
432    /// If the old entry is not none, the operation will fail and return `None`.
433    /// Otherwise, the lock guard of the new child page table node is returned.
434    /// # Verified Properties
435    /// ## Preconditions
436    /// - **Safety Invariants**: The old node's root must satisfy the safety invariants for an [Entry](Entry::invariants)
437    /// and the caller must provide its parent node owner.
438    /// ## Postconditions
439    /// - **Safety Invariants**: If a new node is allocated, it will satisfy the safety invariants.
440    /// - **Safety**: If a new node is allocated, all other nodes have their invariants preserved.
441    /// - **Correctness**: A new node is allocated if and only if the old node is absent.
442    /// - **Correctness**: If the old node is present, the function retuns `None` and the state is unchanged.
443    /// ## Safety
444    /// - The invariants ensure that the entry is appropriately aligned and its index is within bounds.
445    /// - The invariants of the entire page table are preserved in both cases.
446    #[verus_spec(res =>
447        with Tracked(owner): Tracked<&mut OwnerSubtree<C>>,
448            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
449            Tracked(regions): Tracked<&mut MetaRegionOwners>,
450            Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
451            Tracked(parent_guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
452            -> guard_perm: Tracked<Option<GuardPerm<'rcu, C>>>
453        requires
454            old(self).invariants(old(owner).value, *old(regions)),
455            old(owner).inv(),
456            old(self).node_matching(old(owner).value, *old(parent_owner), *old(parent_guard_perm)),
457            old(owner).level < INC_LEVELS - 1,
458        ensures
459            final(self).invariants(final(owner).value, *final(regions)),
460            final(self).parent_perms_preserved(*old(parent_owner), *final(parent_owner), *old(parent_guard_perm), *final(parent_guard_perm)),
461            final(self).idx == old(self).idx,
462            old(owner).value.is_absent() && old(parent_owner).level > 1 ==> {
463                // node_matching preserved: parent_owner still matches the child after allocation.
464                &&& final(self).node_matching(final(owner).value, *final(parent_owner), *final(parent_guard_perm))
465                // OwnerSubtree inv (recursive tree invariant, not just value.inv()).
466                &&& final(owner).inv()
467                // After into_pte, the entry has in_scope == false.
468                &&& !final(owner).value.in_scope
469            },
470            old(owner).value.is_absent() && old(parent_owner).level > 1 ==> {
471                &&& res is Some
472                &&& final(owner).value.is_node()
473                &&& guard_perm@ is Some
474                &&& guard_perm@.unwrap().addr() == res.unwrap().addr()
475                &&& final(owner).level == old(owner).level
476                &&& final(owner).value.parent_level == old(owner).value.parent_level
477                &&& final(owner).value.node.unwrap().relate_guard_perm(guard_perm@.unwrap())
478                &&& final(guards).lock_held(final(owner).value.node.unwrap().meta_perm.addr())
479                &&& final(owner).value.path == old(owner).value.path
480                &&& final(owner).value.metaregion_sound(*final(regions))
481                &&& OwnerSubtree::implies(
482                    CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
483                    CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value.node.unwrap().meta_perm.addr()))
484                &&& Self::metaregion_sound_neq_preserved(old(owner).value, final(owner).value, *old(regions), *final(regions))
485                &&& Self::path_tracked_pred_preserved(*old(regions), *final(regions))
486                &&& old(regions).slots.contains_key(frame_to_index(final(owner).value.meta_slot_paddr().unwrap()))
487                &&& final(owner).tree_predicate_map(final(owner).value.path,
488                    CursorOwner::<'rcu, C>::node_unlocked_except(*final(guards), final(owner).value.node.unwrap().meta_perm.addr()))
489                &&& final(owner).tree_predicate_map(final(owner).value.path, PageTableOwner::<C>::metaregion_sound_pred(*final(regions)))
490                &&& final(owner).tree_predicate_map(final(owner).value.path, PageTableOwner::<C>::path_tracked_pred(*final(regions)))
491                &&& PageTableOwner(*final(owner)).view_rec(final(owner).value.path) =~= set![]
492                // All children of the newly allocated node are absent (empty PT node).
493                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
494                    #[trigger] final(owner).children[i] is Some && final(owner).children[i].unwrap().value.is_absent()
495                // slot_owners unchanged for all indices except the new PT node's index.
496                &&& forall|i: usize| i != frame_to_index(final(owner).value.meta_slot_paddr().unwrap()) ==>
497                    (#[trigger] final(regions).slot_owners[i]) == old(regions).slot_owners[i]
498                // slots keys: the new PT node was removed then re-inserted, so all old keys preserved.
499                &&& forall|i: usize| old(regions).slots.contains_key(i)
500                    ==> (#[trigger] final(regions).slots.contains_key(i))
501                // The new PT node's ref_count is not UNUSED (was set to 1 by get_from_unused).
502                &&& final(regions).slot_owners[frame_to_index(final(owner).value.meta_slot_paddr().unwrap())]
503                    .inner_perms.ref_count.value() != REF_COUNT_UNUSED
504                // The allocated slot had ref_count == UNUSED before allocation (from get_from_unused).
505                &&& old(regions).slot_owners[frame_to_index(final(owner).value.meta_slot_paddr().unwrap())]
506                    .inner_perms.ref_count.value() == REF_COUNT_UNUSED
507            },
508            !old(owner).value.is_absent() ==> {
509                &&& res is None
510                &&& *final(owner) == *old(owner)
511            },
512            forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
513            forall |i: usize| old(guards).unlocked(i) && i != final(owner).value.node.unwrap().meta_perm.addr() ==> final(guards).unlocked(i),
514    )]
515    pub(in crate::mm) fn alloc_if_none<A: InAtomicMode>(&mut self, guard: &'rcu A)
516    -> (res: Option<PPtr<PageTableGuard<'rcu, C>>>) {
517        let entry_is_present = self.pte.is_present();
518
519        let mut parent_guard = self.node.take(Tracked(parent_guard_perm));
520
521        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
522        let level = parent_guard.level();
523
524        if entry_is_present || level <= 1 {
525            self.node.put(Tracked(parent_guard_perm), parent_guard);
526
527            proof_with!{|= Tracked(None)}
528            None
529        } else {
530            let tracked old_path = owner.value.get_path();
531
532            proof_decl! {
533                let tracked mut new_node_owner: Tracked<OwnerSubtree<C>>;
534            }
535
536            #[verus_spec(with Tracked(parent_owner), Tracked(regions), Tracked(guards), Ghost(self.idx) => Tracked(new_node_owner))]
537            let new_page = PageTableNode::<C>::alloc(level - 1);
538
539            proof {
540                let pte = C::E::new_pt_spec(meta_to_frame(new_node_owner.value.node.unwrap().meta_perm.addr()));
541                old(parent_owner).set_children_perm_axiom(self.idx, pte);
542                C::E::new_properties();
543                assert(!pte.is_last_spec(level as PagingLevel));
544            }
545
546            #[verus_spec(with Tracked(&new_node_owner.value.node.tracked_borrow().meta_perm.points_to))]
547            let paddr = new_page.start_paddr();
548
549            assert(new_node_owner.value.metaregion_sound(*regions));
550
551            #[verus_spec(with Tracked(&mut new_node_owner.value), Tracked(regions))]
552            let new_pte = Child::PageTable(new_page).into_pte();
553            self.pte = new_pte;
554
555            proof {
556                assert(new_node_owner.value.pte_invariants(self.pte, *regions));
557                assert(new_node_owner.value.match_pte(self.pte, new_node_owner.value.parent_level));
558                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
559                assert(new_node_owner.value.metaregion_sound(*regions));
560                assert(new_node_owner.value.meta_slot_paddr().unwrap() == paddr);
561            }
562
563            #[verus_spec(with Tracked(regions), Tracked(&new_node_owner.value.node.tracked_borrow().meta_perm))]
564            let pt_ref = PageTableNodeRef::borrow_paddr(paddr);
565
566            proof_decl! {
567                let tracked mut guard_perm: Tracked<GuardPerm<'rcu, C>>;
568            }
569
570            // Lock before writing the PTE, so no one else can operate on it.
571            #[verus_spec(with Tracked(&new_node_owner.value.node.tracked_borrow()), Tracked(guards) => Tracked(guard_perm))]
572            let pt_lock_guard = pt_ref.lock(guard);
573
574            proof {
575                parent_owner.nr_children_absent_slot_bound(self.idx);
576            }
577
578            // SAFETY:
579            //  1. The index is within the bounds.
580            //  2. The new PTE is a child in `C` and at the correct paging level.
581            //  3. The ownership of the child is passed to the page table node.
582            #[verus_spec(with Tracked(parent_owner))]
583            parent_guard.write_pte(self.idx, self.pte);
584
585            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
586            let nr_children = parent_guard.nr_children_mut();
587            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
588            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
589
590            self.node.put(Tracked(parent_guard_perm), parent_guard);
591
592            proof {
593                owner.value = new_node_owner.value;
594                owner.value.parent_level = level as PagingLevel;
595                owner.value.path = old_path;
596                owner.children = new_node_owner.children;
597                // From allocated_empty_node_owner: all children are absent.
598                assert(forall|i: int| 0 <= i < NR_ENTRIES ==>
599                    (#[trigger] owner.children[i]) is Some && owner.children[i].unwrap().value.is_absent());
600
601                let new_paddr = owner.value.meta_slot_paddr().unwrap();
602                assert(old(regions).slots.contains_key(frame_to_index(new_paddr)));
603                regions.inv_implies_correct_addr(new_paddr);
604                let new_idx = frame_to_index(new_paddr);
605                let tracked mut new_meta_slot = regions.slot_owners.tracked_remove(new_idx);
606                new_meta_slot.paths_in_pt = set![owner.value.path];
607                regions.slot_owners.tracked_insert(new_idx, new_meta_slot);
608            }
609
610            proof_with!{|= Tracked(Some(guard_perm))}
611            Some(pt_lock_guard)
612        }
613    }
614
615    /// Splits the entry to smaller pages if it maps to a huge page.
616    ///
617    /// If the entry does map to a huge page, it is split into smaller pages
618    /// mapped by a child page table node. The new child page table node
619    /// is returned.
620    ///
621    /// If the entry does not map to a untracked huge page, the method returns
622    /// `None`.
623    /// # Verified Properties
624    /// ## Preconditions
625    /// - **Safety Invariants**: The old node's root must satisfy the safety invariants for an [Entry](Entry::invariants)
626    /// and the caller must provide its parent node owner.
627    /// ## Postconditions
628    /// - **Safety Invariants**: The node allocated in place of the split page satisfies the safety invariants.
629    /// - **Safety**: All other nodes have their invariants preserved.
630    #[verus_spec(res =>
631        with Tracked(owner) : Tracked<&mut OwnerSubtree<C>>,
632            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
633            Tracked(regions): Tracked<&mut MetaRegionOwners>,
634            Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
635            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
636        requires
637            old(regions).inv(),
638            old(owner).inv(),
639            old(self).wf(old(owner).value),
640            old(self).node.addr() == old(guard_perm).addr(),
641            old(guard_perm).is_init(),
642            old(parent_owner).relate_guard_perm(*old(guard_perm)),
643            old(parent_owner).inv(),
644            old(parent_owner).level == old(owner).value.parent_level,
645            old(parent_owner).level < NR_LEVELS,
646            // For huge-page split: all 4KB sub-pages (j > 0) must be valid.
647            // The j = 0 sub-page coincides with the huge frame's own slot, which is
648            // already accounted for by the frame's own metaregion_sound.
649            // Fine-grained form (over 4KB pages) enables the recursive split case.
650            old(owner).value.is_frame() && old(parent_owner).level > 1 ==>
651                forall |j: usize| #![trigger frame_to_index(
652                    (old(owner).value.frame.unwrap().mapped_pa
653                        + j * PAGE_SIZE) as usize)]
654                    0 < j < page_size(old(parent_owner).level) / PAGE_SIZE ==> {
655                    let sub_idx = frame_to_index(
656                        (old(owner).value.frame.unwrap().mapped_pa
657                            + j * PAGE_SIZE) as usize);
658                    &&& old(regions).slots.contains_key(sub_idx)
659                    &&& old(regions).slot_owners[sub_idx].inner_perms.ref_count.value()
660                        != REF_COUNT_UNUSED
661                },
662        ensures
663            old(owner).value.is_frame() && old(parent_owner).level > 1 ==> {
664                &&& res is Some
665                &&& final(owner).value.is_node()
666                &&& final(owner).level == old(owner).level
667                &&& final(parent_owner).relate_guard_perm(*final(guard_perm))
668                &&& final(guards).guards.contains_key(res.unwrap().addr())
669                &&& final(guards).guards[res.unwrap().addr()] is Some
670                &&& final(guards).guards[res.unwrap().addr()].unwrap().pptr() == res.unwrap()
671                &&& final(owner).value.node.unwrap().relate_guard_perm(final(guards).guards[res.unwrap().addr()].unwrap())
672                &&& final(owner).value.node.unwrap().meta_perm.addr() == res.unwrap().addr()
673                // All children of the new node subtree are frames with the same prop (from the split loop).
674                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
675                    (#[trigger] final(owner).children[j]).unwrap().value.is_frame()
676                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
677                    (#[trigger] final(owner).children[j]).unwrap().value.frame.unwrap().prop
678                        == old(owner).value.frame.unwrap().prop
679                &&& final(owner).value.path == old(owner).value.path
680                &&& final(owner).value.metaregion_sound(*final(regions))
681                &&& OwnerSubtree::implies(
682                    CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
683                    CursorOwner::<'rcu, C>::node_unlocked(*final(guards)))
684                &&& OwnerSubtree::implies(
685                    PageTableOwner::<C>::metaregion_sound_pred(*old(regions)),
686                    PageTableOwner::<C>::metaregion_sound_pred(*final(regions)))
687                &&& final(owner).tree_predicate_map(final(owner).value.path,
688                    CursorOwner::<'rcu, C>::node_unlocked(*final(guards)))
689                &&& final(owner).tree_predicate_map(final(owner).value.path,
690                    PageTableOwner::<C>::metaregion_sound_pred(*final(regions)))
691            },
692            !old(owner).value.is_frame() || old(parent_owner).level <= 1 ==> {
693                &&& res is None
694                &&& *final(owner) == *old(owner)
695            },
696            final(owner).inv(),
697            final(owner).value.parent_level == old(owner).value.parent_level,
698            final(self).idx == old(self).idx,
699            old(owner).value.is_frame() && old(parent_owner).level > 1 ==> !final(owner).value.in_scope,
700            old(owner).value.is_frame() && old(parent_owner).level > 1 ==>
701                final(self).node_matching(final(owner).value, *final(parent_owner), *final(guard_perm)),
702            final(regions).inv(),
703            final(parent_owner).inv(),
704            final(parent_owner).level == old(parent_owner).level,
705            final(guard_perm).pptr() == old(guard_perm).pptr(),
706            final(guard_perm).value().inner.inner@.ptr.addr() == old(guard_perm).value().inner.inner@.ptr.addr(),
707            forall |i: usize| old(guards).lock_held(i) ==> final(guards).lock_held(i),
708            forall |i: usize| old(guards).unlocked(i) ==> final(guards).unlocked(i),
709            // slot_owners unchanged for all indices except the new PT node's index.
710            old(owner).value.is_frame() && old(parent_owner).level > 1 ==> {
711                &&& forall|i: usize| i != frame_to_index(meta_to_frame(final(owner).value.node.unwrap().meta_perm.addr())) ==>
712                    (#[trigger] final(regions).slot_owners[i]) == old(regions).slot_owners[i]
713                // slots keys preserved (alloc removes then borrow re-inserts).
714                &&& forall|i: usize| old(regions).slots.contains_key(i)
715                    ==> (#[trigger] final(regions).slots.contains_key(i))
716                // The new PT node's ref_count is not UNUSED.
717                &&& final(regions).slot_owners[frame_to_index(meta_to_frame(final(owner).value.node.unwrap().meta_perm.addr()))]
718                    .inner_perms.ref_count.value() != REF_COUNT_UNUSED
719                // The allocated slot had ref_count == UNUSED before allocation.
720                &&& old(regions).slot_owners[frame_to_index(meta_to_frame(final(owner).value.node.unwrap().meta_perm.addr()))]
721                    .inner_perms.ref_count.value() == REF_COUNT_UNUSED
722            },
723    )]
724    pub(in crate::mm) fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A)
725        -> (res: Option<PPtr<PageTableGuard<'rcu, C>>>) {
726        let mut node_guard = self.node.take(Tracked(guard_perm));
727
728        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
729        let level = node_guard.level();
730
731        if !(self.pte.is_last(level) && level > 1) {
732            self.node.put(Tracked(guard_perm), node_guard);
733
734            return None;
735        }
736        let pa = self.pte.paddr();
737        let prop = self.pte.prop();
738
739        proof {
740            EntryOwner::last_pte_implies_frame_match(owner.value, self.pte, level);
741        }
742
743        proof_decl!{
744            let tracked mut new_owner: OwnerSubtree<C>;
745        }
746
747        #[verus_spec(with Tracked(parent_owner), Tracked(regions), Tracked(guards), Ghost(self.idx) => Tracked(new_owner))]
748        let new_page = PageTableNode::<C>::alloc(level);
749
750        #[verus_spec(with Tracked(&new_owner.value.node.tracked_borrow().meta_perm.points_to))]
751        let paddr = new_page.start_paddr();
752
753        proof {
754            broadcast use crate::mm::frame::meta::mapping::group_page_meta;
755            assert(new_owner.value.metaregion_sound(*regions));
756            assert(new_owner.value.meta_slot_paddr().unwrap() == paddr);
757        }
758
759        #[verus_spec(with Tracked(regions), Tracked(&new_owner.value.node.tracked_borrow().meta_perm))]
760        let pt_ref = PageTableNodeRef::borrow_paddr(paddr);
761
762        proof_decl! {
763            let tracked mut new_guard_perm: Tracked<GuardPerm<'rcu, C>>;
764        }
765
766        // Lock before writing the PTE, so no one else can operate on it.
767        #[verus_spec(with Tracked(&new_owner.value.node.tracked_borrow()), Tracked(guards) => Tracked(new_guard_perm))]
768        let pt_lock_guard = pt_ref.lock(guard);
769
770        let ghost children_perm = new_owner.value.node.unwrap().children_perm;
771        let ghost new_owner_path = new_owner.value.path;
772        let ghost new_owner_meta_addr = new_owner.value.node.unwrap().meta_perm.addr();
773
774        for i in 0..nr_subpage_per_huge::<C>()
775            invariant
776                1 < level < NR_LEVELS,
777                owner.inv(),
778                owner.value.is_frame(),
779                owner.value.parent_level == level,
780                owner.value.frame.unwrap().mapped_pa == pa,
781                owner.value.frame.unwrap().prop == prop,
782                pa == old(owner).value.frame.unwrap().mapped_pa,
783                level == old(parent_owner).level,
784                pa % page_size(level) == 0,
785                pa + page_size(level) <= MAX_PADDR,
786                regions.inv(),
787                parent_owner.inv(),
788                new_owner.value.is_node(),
789                new_owner.inv(),
790                new_owner.value.path == new_owner_path,
791                new_owner.value.node.unwrap().meta_perm.addr() == new_owner_meta_addr,
792                new_owner.value.node.unwrap().relate_guard_perm(new_guard_perm),
793                new_owner.value.node.unwrap().level == (level - 1) as PagingLevel,
794                pt_lock_guard.addr() == new_guard_perm.addr(),
795                forall|j: int|
796                    #![auto]
797                    0 <= j < NR_ENTRIES ==> {
798                        &&& new_owner.children[j] is Some
799                        &&& new_owner.children[j].unwrap().value.match_pte(new_owner.value.node.unwrap().children_perm.value()[j], new_owner.value.node.unwrap().level)
800                        &&& new_owner.children[j].unwrap().value.parent_level == new_owner.value.node.unwrap().level
801                        &&& new_owner.children[j].unwrap().value.inv()
802                        &&& new_owner.children[j].unwrap().value.path == new_owner_path.push_tail(j as usize)
803                    },
804                forall|j: int| #![auto] i <= j < NR_ENTRIES ==> {
805                    &&& new_owner.children[j].unwrap().value.is_absent()
806                    &&& !new_owner.children[j].unwrap().value.in_scope
807                    &&& new_owner.value.node.unwrap().children_perm.value()[j] == C::E::new_absent_spec()
808                },
809                // Children [0, i) have been replaced with frames.
810                forall|j: int| #![auto] 0 <= j < i ==> {
811                    new_owner.children[j].unwrap().value.is_frame()
812                },
813                // Sub-page slots (4KB-grained, j > 0): slots.contains_key, rc != UNUSED, and rc > 0
814                // are all preserved. The j = 0 case is handled separately (the huge frame's own slot).
815                forall |j: usize| #![trigger frame_to_index(
816                    (pa + j * PAGE_SIZE) as usize)]
817                    0 < j < page_size(level) / PAGE_SIZE ==> {
818                    let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
819                    &&& regions.slots.contains_key(sub_idx)
820                    &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
821                    &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
822                },
823                // j = 0: the huge frame's own slot. These come from the huge
824                // frame's `metaregion_sound` at function entry and are
825                // preserved by the split loop (which only inserts into
826                // paths_in_pt, never touches slots/ref_count).
827                regions.slots.contains_key(frame_to_index(pa)),
828                regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
829                    != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED,
830                regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value() > 0,
831                new_page.ptr.addr() == new_owner_meta_addr,
832        {
833            proof {
834                C::axiom_nr_subpage_per_huge_eq_nr_entries();
835            }
836            assert(i < NR_ENTRIES);
837
838            proof {
839                // Prove required facts while we still have new_owner.value.node available.
840                let ghost the_node = new_owner.value.node.unwrap();
841                assert(0 <= i < NR_ENTRIES);
842                assert(new_owner.children[i as int].unwrap().value.match_pte(
843                    the_node.children_perm.value()[i as int],
844                    new_owner.children[i as int].unwrap().value.parent_level,
845                ));
846                assert(the_node.relate_guard_perm(new_guard_perm));
847                assert(new_guard_perm.addr() == pt_lock_guard.addr());
848                assert(new_owner.children[i as int].unwrap().value.parent_level == the_node.level);
849                assert(!new_owner.children[i as int].unwrap().value.in_scope);
850
851                OwnerSubtree::child_some_properties(new_owner, i as usize);
852            }
853
854            let tracked mut new_owner_node = new_owner.value.node.tracked_take();
855
856            proof {
857                let ghost old_children_perm = new_owner_node.children_perm;
858            }
859
860            proof {
861                EntryOwner::huge_frame_split_child_at(owner.value, *regions, i as usize);
862            }
863
864            let small_pa = pa + i * page_size(level - 1);
865
866            assert(small_pa % PAGE_SIZE == 0);
867
868            let tracked child_owner = EntryOwner::new_frame(
869                small_pa,
870                new_owner.value.path.push_tail(i as usize),
871                (level - 1) as PagingLevel,
872                prop,
873            );
874
875            #[verus_spec(with Tracked(&new_owner_node), Tracked(&new_owner.children.tracked_borrow(i as int).tracked_borrow().value), Tracked(&new_guard_perm))]
876            let mut entry = PageTableGuard::entry(pt_lock_guard, i);
877
878            proof {
879                assert(entry.idx == i as usize);
880                let ghost child_before_remove = new_owner.child(i as usize).unwrap();
881                assert(child_before_remove.inv());
882            }
883            let tracked mut new_owner_child = new_owner.children.tracked_remove(i as int).tracked_unwrap();
884
885            proof {
886                assert(new_owner_child.value.match_pte(
887                    new_owner_node.children_perm.value()[i as int],
888                    new_owner_child.value.parent_level,
889                ));
890
891                let idx = frame_to_index(small_pa);
892                assert(idx == frame_to_index(
893                    (pa + i * page_size((level - 1) as PagingLevel)) as usize));
894                if i != 0 {
895                    let ghost big_j = crate::specs::mm::page_table::cursor::
896                        page_size_lemmas::lemma_split_sub_page_big_j(pa, level, i);
897                    assert(small_pa == (pa + big_j * PAGE_SIZE) as usize);
898                }
899
900                assert(entry.node_matching(new_owner_child.value, new_owner_node, new_guard_perm)) by {
901                    let pte = new_owner_node.children_perm.value()[i as int];
902                    assert(pte == C::E::new_absent_spec());
903                    crate::specs::arch::PageTableEntry::absent_pte_paddr_ok();
904                    EntryOwner::absent_match_pte(
905                        new_owner_child.value,
906                        pte,
907                        new_owner_child.value.parent_level,
908                    );
909                };
910
911                if level - 1 > 1 {
912                    let nr_subpages = page_size((level - 1) as PagingLevel) / PAGE_SIZE;
913                    crate::specs::mm::page_table::cursor::page_size_lemmas::
914                        lemma_page_size_div_mul_eq((level - 1) as PagingLevel);
915                    crate::specs::mm::page_table::cursor::page_size_lemmas::
916                        lemma_page_size_div_mul_eq(level);
917                    crate::specs::mm::page_table::cursor::page_size_lemmas::
918                        lemma_nr_entries_times_sub_page_size(level);
919                    assert forall |j_prime: usize|
920                        #![trigger frame_to_index((small_pa + j_prime * PAGE_SIZE) as usize)]
921                        0 < j_prime < nr_subpages implies {
922                        let sub_idx = frame_to_index((small_pa + j_prime * PAGE_SIZE) as usize);
923                        &&& regions.slots.contains_key(sub_idx)
924                        &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
925                        &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
926                    } by {
927                        let sub_pages_per_subframe = page_size((level - 1) as PagingLevel) / PAGE_SIZE;
928                        let big_j_int: int = i as int * sub_pages_per_subframe as int + j_prime as int;
929                        vstd::arithmetic::mul::lemma_mul_nonnegative(
930                            i as int, sub_pages_per_subframe as int);
931                        vstd::arithmetic::mul::lemma_mul_inequality(
932                            (i + 1) as int, NR_ENTRIES as int, sub_pages_per_subframe as int);
933                        vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way(
934                            sub_pages_per_subframe as int, i as int, 1int);
935                        vstd::arithmetic::mul::lemma_mul_is_associative(
936                            NR_ENTRIES as int, sub_pages_per_subframe as int, PAGE_SIZE as int);
937                        vstd::arithmetic::div_mod::lemma_div_by_multiple(
938                            NR_ENTRIES as int * sub_pages_per_subframe as int, PAGE_SIZE as int);
939                        let big_j: usize = big_j_int as usize;
940                        vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way(
941                            PAGE_SIZE as int,
942                            i as int * sub_pages_per_subframe as int,
943                            j_prime as int);
944                        vstd::arithmetic::mul::lemma_mul_is_associative(
945                            i as int, sub_pages_per_subframe as int, PAGE_SIZE as int);
946                        assert((small_pa + j_prime * PAGE_SIZE) as usize == (pa + big_j * PAGE_SIZE) as usize);
947                    }
948                    assert(child_owner.frame_sub_pages_valid(*regions));
949                }
950
951                let small_idx = frame_to_index(small_pa);
952                regions.inv_implies_correct_addr(small_pa);
953                let tracked mut small_slot = regions.slot_owners.tracked_remove(small_idx);
954                small_slot.paths_in_pt = small_slot.paths_in_pt.insert(child_owner.path);
955                regions.slot_owners.tracked_insert(small_idx, small_slot);
956
957                if (level - 1) > 1 {
958                    assert(child_owner.frame_sub_pages_valid(*regions));
959                }
960
961                assert(Child::<C>::Frame(small_pa, (level - 1) as PagingLevel, prop)
962                    .invariants(child_owner, *regions));
963            }
964
965            #[verus_spec(with Tracked(regions),
966                Tracked(&mut new_owner_child.value),
967                Tracked(&mut child_owner),
968                Tracked(&mut new_owner_node),
969                Tracked(&mut new_guard_perm))]
970            let old = entry.replace(Child::Frame(small_pa, level - 1, prop));
971
972            proof {
973                new_owner.value.node = Some(new_owner_node);
974                new_owner_child.value.in_scope = false;
975                child_owner.in_scope = false;
976                OwnerSubtree::set_value_property(new_owner_child, child_owner);
977                new_owner_child.value = child_owner;
978                new_owner.children.tracked_insert(i as int, Some(new_owner_child));
979
980                TreePath::push_tail_property_len(new_owner_path, i as usize);
981                OwnerSubtree::insert_preserves_inv(new_owner, i as usize, new_owner_child);
982            }
983        }
984
985        self.pte = (#[verus_spec(with Tracked(&mut new_owner.value), Tracked(regions))]
986        Child::PageTable(new_page).into_pte());
987
988        proof {
989            new_owner.level = owner.level;
990            *owner = new_owner;
991        }
992
993        let tracked mut node_owner = owner.value.node.tracked_take();
994
995        // SAFETY:
996        //  1. The index is within the bounds.
997        //  2. The new PTE is a child in `C` and at the correct paging level.
998        //  3. The ownership of the child is passed to the page table node.
999        #[verus_spec(with Tracked(&mut node_owner))]
1000        node_guard.write_pte(self.idx, self.pte);
1001
1002        proof {
1003            owner.value.node = Some(node_owner);
1004        }
1005
1006        self.node.put(Tracked(guard_perm), node_guard);
1007
1008        Some(pt_lock_guard)
1009    }
1010
1011    /// Create a new entry at the node with guard.
1012    ///
1013    /// # Verified Properties
1014    /// ## Preconditions
1015    /// - **Safety**: The caller must provide the owner of the entry and the parent node, and the entry
1016    /// must match the parent node's PTE at the given index.
1017    /// - **Safety**: The caller must provide a valid guard permission matching `guard`, and it must be guarding the
1018    /// correct parent.
1019    /// ## Postconditions
1020    /// - **Correctness**: The resulting entry matches the owner.
1021    /// ## Safety
1022    /// - The precondition ensures that the index is within the bounds of the node.
1023    /// - This function does not modify the actual entry or any other relevant structure, so it is safe to call.
1024    /// Because we also require the guard to be correct, it will be safe to use the resulting `Entry` as a handle to the
1025    /// underlying `PTE`.
1026    #[verus_spec(
1027        with Tracked(owner): Tracked<&EntryOwner<C>>,
1028            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
1029            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
1030    )]
1031    pub(in crate::mm) fn new_at(guard: PPtr<PageTableGuard<'rcu, C>>, idx: usize) -> (res: Self)
1032        requires
1033            owner.inv(),
1034            !owner.in_scope,
1035            parent_owner.inv(),
1036            guard_perm.addr() == guard.addr(),
1037            parent_owner.relate_guard_perm(*guard_perm),
1038            idx < NR_ENTRIES,
1039            owner.match_pte(parent_owner.children_perm.value()[idx as int], owner.parent_level),
1040        ensures
1041            res.wf(*owner),
1042            res.node.addr() == guard_perm.addr(),
1043            res.idx == idx,
1044    {
1045        // SAFETY: The index is within the bound.
1046        let guard_val = guard.borrow(Tracked(guard_perm));
1047        #[verus_spec(with Tracked(parent_owner))]
1048        let pte = guard_val.read_pte(idx);
1049        Self { pte, idx, node: guard }
1050    }
1051}
1052
1053} // verus!
ostd/mm/page_table/node/entry.rs

ostd/mm/page_table/node/
entry.rs
