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::meta::has_safe_slot;
6use crate::mm::frame::meta::mapping::{frame_to_index, frame_to_meta, meta_addr, meta_to_frame};
7use crate::mm::frame::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::{page_prop::PageProperty, Paddr, PagingConstsTrait, PagingLevel, Vaddr},
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        ensures
70            owner.pte_invariants(res, *regions),
71            *regions == old(owner).into_pte_regions_spec(*old(regions)),
72            *owner == old(owner).into_pte_owner_spec(),
73            old(owner).node is Some ==> res == C::E::new_pt_spec(
74                meta_to_frame(old(owner).node.unwrap().meta_perm.addr()),
75            ),
76    {
77        proof {
78            C::E::new_properties();
79        }
80
81        match self {
82            Child::PageTable(node) => {
83                let ghost node_owner = owner.node.unwrap();
84
85                #[verus_spec(with Tracked(&owner.node.tracked_borrow().meta_perm.points_to))]
86                let paddr = node.start_paddr();
87
88                let ghost node_index = frame_to_index(meta_to_frame(node.ptr.addr()));
89
90                let _ = ManuallyDrop::new(node, Tracked(regions));
91
92                proof {
93                    let node_index = frame_to_index(meta_to_frame(node.ptr.addr()));
94                    let spec_regions = owner.into_pte_regions_spec(*old(regions));
95                    assert(regions.slot_owners =~= spec_regions.slot_owners);
96                    owner.in_scope = false;
97                }
98
99                C::E::new_pt(paddr)
100            },
101            Child::Frame(paddr, level, prop) => {
102                proof {
103                    owner.in_scope = false;
104                }
105                C::E::new_page(paddr, level, prop)
106            },
107            Child::None => {
108                proof {
109                    owner.in_scope = false;
110                }
111                C::E::new_absent()
112            },
113        }
114    }
115
116    /// Converts a `PTE` to a `Child`.
117    ///
118    /// # Verified Properties
119    /// ## Preconditions
120    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
121    /// - **Safety**: `level` must match the original level of the child.
122    /// ## Postconditions
123    /// - **Safety Invariants**: the [safety invariants](Child::invariants) are preserved.
124    /// - **Safety**: the `EntryOwner` is aware that it is tracking an entry in `Child` form.
125    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
126    /// - **Correctness**: the `Child` is equivalent to the original `PTE`.
127    /// ## Safety
128    /// The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::into_pte`]
129    /// (or another function that calls `ManuallyDrop::new`, which is sufficient for safety).
130    #[verus_spec(
131        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
132            Tracked(entry_own): Tracked<&mut EntryOwner<C>>,
133    )]
134    pub fn from_pte(pte: C::E, level: PagingLevel) -> (res: Self)
135        requires
136            old(entry_own).pte_invariants(pte, *old(regions)),
137            level == old(entry_own).parent_level,
138        ensures
139            res.invariants(*entry_own, *regions),
140            res == Child::<C>::from_pte_spec(pte, level, *regions),
141            *entry_own == old(entry_own).from_pte_owner_spec(),
142            *regions == entry_own.from_pte_regions_spec(*old(regions)),
143    {
144        if !pte.is_present() {
145            proof {
146                entry_own.in_scope = true;
147            }
148            return Child::None;
149        }
150        let paddr = pte.paddr();
151
152        if !pte.is_last(level) {
153            proof {
154                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
155
156                regions.inv_implies_correct_addr(paddr);
157            }
158
159            #[verus_spec(with Tracked(regions), Tracked(&entry_own.node.tracked_borrow().meta_perm))]
160            let node = PageTableNode::from_raw(paddr);
161
162            proof {
163                entry_own.in_scope = true;
164
165                assert(regions.slot_owners =~= entry_own.from_pte_regions_spec(
166                    *old(regions),
167                ).slot_owners);
168                assert(regions.slots =~= entry_own.from_pte_regions_spec(*old(regions)).slots);
169            }
170
171            return Child::PageTable(node);
172        }
173        proof {
174            entry_own.in_scope = true;
175        }
176        Child::Frame(paddr, level, pte.prop())
177    }
178}
179
180/// A reference to the child of a page table node.
181/// # Verification Design
182/// If the child is itself a page table node, it is represented by a [`PageTableNodeRef`],
183/// because a reference to it must be treated as a potentially shared reference of the appropriate lifetime.
184/// By contrast, a mapped frame can be referenced by just carrying its values, and an absent one is just a simple tag.
185pub enum ChildRef<'a, C: PageTableConfig> {
186    /// A child page table node.
187    PageTable(PageTableNodeRef<'a, C>),
188    /// Physical address of a mapped physical frame.
189    ///
190    /// It is associated with the virtual page property and the level of the
191    /// mapping node, which decides the size of the frame.
192    Frame(Paddr, PagingLevel, PageProperty),
193    None,
194}
195
196impl<C: PageTableConfig> ChildRef<'_, C> {
197    /// Converts a PTE to a reference to a child.
198    ///
199    /// # Verified Properties
200    /// ## Preconditions
201    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
202    /// - **Safety**: `level` must match the original level of the child.
203    /// ## Postconditions
204    /// - **Safety Invariants**: the [safety invariants](ChildRef::invariants) are preserved.
205    /// - **Correctness**: the `ChildRef` is equivalent to the original `PTE`.
206    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
207    /// ## Safety
208    /// - The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::from_pte`]
209    /// - The soundness of using the resulting `ChildRef` as a reference follows from `FrameRef` safety.
210    #[verus_spec(
211        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
212            Tracked(entry_owner): Tracked<&EntryOwner<C>>
213    )]
214    pub fn from_pte(pte: &C::E, level: PagingLevel) -> (res: Self)
215        requires
216            entry_owner.pte_invariants(*pte, *old(regions)),
217            level == entry_owner.parent_level,
218        ensures
219            res.invariants(*entry_owner, *regions),
220            *regions =~= *old(regions),
221    {
222        if !pte.is_present() {
223            return ChildRef::None;
224        }
225        let paddr = pte.paddr();
226
227        if !pte.is_last(level) {
228            proof {
229                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
230
231                regions.inv_implies_correct_addr(paddr);
232            }
233
234            #[verus_spec(with Tracked(regions), Tracked(&entry_owner.node.tracked_borrow().meta_perm))]
235            let node = PageTableNodeRef::borrow_paddr(paddr);
236
237            return ChildRef::PageTable(node);
238        }
239        ChildRef::Frame(paddr, level, pte.prop())
240    }
241}
242
243} // verus!
ostd/mm/page_table/node/child.rs

ostd/mm/page_table/node/
child.rs
