ostd/mm/page_table/node/
child.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module specifies the type of the children of a page table node.
3use vstd::prelude::*;
4
5use crate::mm::frame::Frame;
6use crate::mm::frame::meta::has_safe_slot;
7use crate::mm::frame::meta::mapping::{frame_to_index, frame_to_meta, meta_addr, meta_to_frame};
8use crate::mm::page_table::*;
9use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
10use crate::specs::arch::paging_consts::PagingConsts;
11use crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED;
12use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
13
14use vstd_extra::cast_ptr::*;
15use vstd_extra::drop_tracking::*;
16use vstd_extra::ownership::*;
17
18use crate::specs::*;
19
20use crate::{
21    mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_prop::PageProperty},
22    //    sync::RcuDrop,
23};
24
25use super::*;
26
27verus! {
28
29/// A page table entry that owns the child of a page table node if present.
30pub enum Child<C: PageTableConfig> {
31    /// A child page table node.
32    pub PageTable(PageTableNode<C>),
33    /// Physical address of a mapped physical frame.
34    ///
35    /// It is associated with the virtual page property and the level of the
36    /// mapping node, which decides the size of the frame.
37    pub Frame(Paddr, PagingLevel, PageProperty),
38    pub None,
39}
40
41impl<C: PageTableConfig> Child<C> {
42    /// Returns whether the child is not present.
43    #[vstd::contrib::auto_spec]
44    pub(in crate::mm) fn is_none(&self) -> (b: bool) {
45        matches!(self, Child::None)
46    }
47
48    /// Converts the child to a raw PTE value.
49    /// # Verified Properties
50    /// ## Preconditions
51    /// - **Safety Invariants**: all [safety invariants](Child::invariants) must hold on the child.
52    /// - **Safety**: the entry's must be marked as a child, which implies that it has a `raw_count` of 0.
53    /// ## Postconditions
54    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) are preserved.
55    /// - **Safety**: the entry's raw count is incremented by 1.
56    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
57    /// - **Correctness**: the `PTE` is equivalent to the original `Child`.
58    /// ## Safety
59    /// The `PTE` safety invariants ensure that the raw pointer to the entry is tracked correctly
60    /// so that we can guarantee the safety condition on `from_pte`.
61    #[verus_spec(
62        with Tracked(owner): Tracked<&mut EntryOwner<C>>,
63            Tracked(regions): Tracked<&mut MetaRegionOwners>
64    )]
65    pub fn into_pte(self) -> (res: C::E)
66        requires
67            self.invariants(*old(owner), *old(regions)),
68            old(owner).in_scope,
69            self matches Child::PageTable(node) ==> old(regions).frame_obligations.count(
70                frame_to_index(meta_to_frame(node.ptr.addr())),
71            ) > 0,
72        ensures
73            final(owner).pte_invariants(res, *final(regions)),
74            *final(regions) == old(owner).into_pte_regions_spec(*old(regions)),
75            *final(owner) == old(owner).into_pte_owner_spec(),
76            old(owner).node is Some ==> res == C::E::new_pt_spec(
77                meta_to_frame(old(owner).node.unwrap().meta_addr_self()),
78            ),
79    {
80        proof {
81            C::E::new_properties();
82        }
83
84        match self {
85            Child::PageTable(node) => {
86                let ghost node_owner = owner.node.unwrap();
87                let ghost node_index = frame_to_index(meta_to_frame(node.ptr.addr()));
88
89                let tracked node_slot_perm = regions.slots.tracked_borrow(node_index);
90                #[verus_spec(with Tracked(node_slot_perm))]
91                let paddr = node.start_paddr();
92
93                let ghost fo0 = regions.frame_obligations;
94
95                let _ = ManuallyDrop::new(node, Tracked(regions));
96
97                proof {
98                    // `MD::new` removed one entry at `node_index`, matching
99                    // `into_pte_regions_spec`'s `.remove(index)`.
100                    assert(regions.frame_obligations =~= fo0.remove(node_index));
101                    let spec_regions = owner.into_pte_regions_spec(*old(regions));
102                    assert(regions.slot_owners =~= spec_regions.slot_owners);
103                    owner.in_scope = false;
104                }
105
106                C::E::new_pt(paddr)
107            },
108            Child::Frame(paddr, level, prop) => {
109                proof {
110                    owner.in_scope = false;
111                }
112                C::E::new_page(paddr, level, prop)
113            },
114            Child::None => {
115                proof {
116                    owner.in_scope = false;
117                }
118                C::E::new_absent()
119            },
120        }
121    }
122
123    /// Converts a `PTE` to a `Child`.
124    ///
125    /// # Verified Properties
126    /// ## Preconditions
127    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
128    /// - **Safety**: `level` must match the original level of the child.
129    /// ## Postconditions
130    /// - **Safety Invariants**: the [safety invariants](Child::invariants) are preserved.
131    /// - **Safety**: the `EntryOwner` is aware that it is tracking an entry in `Child` form.
132    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
133    /// - **Correctness**: the `Child` is equivalent to the original `PTE`.
134    /// ## Safety
135    /// The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::into_pte`]
136    /// (or another function that calls `ManuallyDrop::new`, which is sufficient for safety).
137    #[verus_spec(
138        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
139            Tracked(entry_own): Tracked<&mut EntryOwner<C>>,
140    )]
141    pub unsafe fn from_pte(pte: C::E, level: PagingLevel) -> (res: Self)
142        requires
143            old(entry_own).pte_invariants(pte, *old(regions)),
144            level == old(entry_own).parent_level,
145        ensures
146            res.invariants(*final(entry_own), *final(regions)),
147            res == Child::<C>::from_pte_spec(pte, level, *final(regions)),
148            *final(entry_own) == old(entry_own).from_pte_owner_spec(),
149            *final(regions) == final(entry_own).from_pte_regions_spec(*old(regions)),
150    {
151        if !pte.is_present() {
152            proof {
153                entry_own.in_scope = true;
154            }
155            return Child::None;
156        }
157        let paddr = pte.paddr();
158
159        if !pte.is_last(level) {
160            proof {
161                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
162
163                regions.inv_implies_correct_addr(paddr);
164            }
165
166            proof_decl! {
167                let tracked from_raw_obl: vstd_extra::drop_tracking::DropObligation<usize>;
168            }
169
170            let node = unsafe {
171                proof_with!(
172                    Tracked(regions) => Tracked(from_raw_obl)
173                );
174                PageTableNode::from_raw(paddr)
175            };
176
177            proof {
178                // `from_raw_obl` is the freshly minted obligation token
179                // for this slot. It is silently dropped here; the
180                // corresponding `frame_obligations` entry persists and
181                // is consumed by `on_drop`'s teardown path (which mints
182                // its own token via the paired axiom when it calls
183                // `frame.drop`). Net effect over `from_pte` is +1 on
184                // the ledger, balancing the prior `-1` from
185                // `into_pte`'s `MD::new` consume.
186                entry_own.in_scope = true;
187
188                assert(regions.slot_owners =~= entry_own.from_pte_regions_spec(
189                    *old(regions),
190                ).slot_owners);
191                assert(regions.slots =~= entry_own.from_pte_regions_spec(*old(regions)).slots);
192            }
193
194            return Child::PageTable(node);
195        }
196        proof {
197            entry_own.in_scope = true;
198        }
199        Child::Frame(paddr, level, pte.prop())
200    }
201}
202
203/// A reference to the child of a page table node.
204/// # Verification Design
205/// If the child is itself a page table node, it is represented by a [`PageTableNodeRef`],
206/// because a reference to it must be treated as a potentially shared reference of the appropriate lifetime.
207/// By contrast, a mapped frame can be referenced by just carrying its values, and an absent one is just a simple tag.
208pub enum ChildRef<'a, C: PageTableConfig> {
209    /// A child page table node.
210    PageTable(PageTableNodeRef<'a, C>),
211    /// Physical address of a mapped physical frame.
212    ///
213    /// It is associated with the virtual page property and the level of the
214    /// mapping node, which decides the size of the frame.
215    Frame(Paddr, PagingLevel, PageProperty),
216    None,
217}
218
219impl<C: PageTableConfig> ChildRef<'_, C> {
220    /// Converts a PTE to a reference to a child.
221    ///
222    /// # Verified Properties
223    /// ## Preconditions
224    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
225    /// - **Safety**: `level` must match the original level of the child.
226    /// ## Postconditions
227    /// - **Safety Invariants**: the [safety invariants](ChildRef::invariants) are preserved.
228    /// - **Correctness**: the `ChildRef` is equivalent to the original `PTE`.
229    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
230    /// ## Safety
231    /// - The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::from_pte`]
232    /// - The soundness of using the resulting `ChildRef` as a reference follows from `FrameRef` safety.
233    #[verus_spec(
234        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
235            Tracked(entry_owner): Tracked<&EntryOwner<C>>
236    )]
237    pub unsafe fn from_pte(pte: &C::E, level: PagingLevel) -> (res: Self)
238        requires
239            entry_owner.pte_invariants(*pte, *old(regions)),
240            level == entry_owner.parent_level,
241        ensures
242            res.invariants(*entry_owner, *final(regions)),
243            final(regions).slot_owners =~= old(regions).slot_owners,
244            forall|k: usize|
245                old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(
246                    k,
247                ),
248            forall|k: usize|
249                old(regions).slots.contains_key(k) ==> old(regions).slots[k]
250                    == #[trigger] final(regions).slots[k],
251    {
252        if !pte.is_present() {
253            return ChildRef::None;
254        }
255        let paddr = pte.paddr();
256
257        if !pte.is_last(level) {
258            proof {
259                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
260
261                regions.inv_implies_correct_addr(paddr);
262                assert(entry_owner.metaregion_sound(*regions));
263                assert(entry_owner.meta_slot_paddr().unwrap() == paddr);
264            }
265
266            let node = unsafe {
267                #[verus_spec(with Tracked(regions))]
268                PageTableNodeRef::borrow_paddr(paddr)
269            };
270
271            proof {
272                // borrow_paddr postcondition gives raw_count == 1 and field-by-field preservation.
273                // Since raw_count was already 1 (entry is in PTE, in_scope == false),
274                // slot_owners[idx] == old(slot_owners[idx]) follows field by field.
275                assert(regions.slot_owners =~= old(regions).slot_owners);
276                // slots: borrow_paddr inserts at borrow_idx. Prove existing keys preserved.
277                // The node's slot was NOT in old.slots: by active_entry_not_in_free_pool,
278                // a node entry's index can't equal any free-pool index.
279                let borrow_idx = frame_to_index(paddr);
280                assert(entry_owner.is_node());
281                let ghost entry_snap = *entry_owner;
282                assert(!old(regions).slots.contains_key(borrow_idx)) by {
283                    if old(regions).slots.contains_key(borrow_idx) {
284                        EntryOwner::<C>::active_entry_not_in_free_pool(
285                            entry_snap,
286                            *old(regions),
287                            borrow_idx,
288                        );
289                        // gives borrow_idx != borrow_idx — contradiction
290                    }
291                };
292                // Since borrow_idx was not in old.slots, insert preserves all old keys.
293                assert forall|k: usize| old(regions).slots.contains_key(k) implies old(
294                    regions,
295                ).slots[k] == #[trigger] regions.slots[k] by {
296                    assert(k != borrow_idx);
297                    // regions.slots == old.slots.insert(borrow_idx, _), and k != borrow_idx
298                };
299            }
300
301            return ChildRef::PageTable(node);
302        }
303        ChildRef::Frame(paddr, level, pte.prop())
304    }
305}
306
307} // verus!
ostd/mm/page_table/node/child.rs

ostd/mm/page_table/node/
child.rs
