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

ostd/mm/page_table/node/
child.rs
