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::*, simple_pptr::PPtr};
4use vstd_extra::{cast_ptr::*, ownership::*};
5
6use crate::specs::{
7 arch::*,
8 mm::frame::{
9 mapping::{group_page_meta, meta_to_index},
10 meta_region_owners::MetaRegionOwners,
11 },
12 *,
13};
14
15use super::*;
16use crate::arch::mm::PagingConsts;
17use crate::mm::frame::Frame;
18use crate::mm::frame::meta::REF_COUNT_UNUSED;
19use crate::mm::frame::meta::mapping::{frame_to_meta, meta_to_frame};
20use crate::mm::page_table::*;
21use crate::{
22 mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_prop::PageProperty},
23 // sync::RcuDrop,
24};
25use core::marker::PhantomData;
26use core::mem::ManuallyDrop;
27
28verus! {
29
30/// A page table entry that owns the child of a page table node if present.
31pub enum Child<C: PageTableConfig> {
32 /// A child page table node.
33 pub PageTable(PageTableNode<C>),
34 /// Physical address of a mapped physical frame.
35 ///
36 /// It is associated with the virtual page property and the level of the
37 /// mapping node, which decides the size of the frame.
38 pub Frame(Paddr, PagingLevel, PageProperty),
39 pub None,
40}
41
42#[verus_verify]
43impl<C: PageTableConfig> Child<C> {
44 /// Returns whether the child is not present.
45 #[vstd::contrib::auto_spec]
46 pub(in crate::mm) fn is_none(&self) -> (b: bool) {
47 matches!(self, Child::None)
48 }
49
50 /// Converts the child to a raw PTE value.
51 /// # Verified Properties
52 /// ## Preconditions
53 /// - **Safety Invariants**: all [safety invariants](Child::invariants) must hold on the child.
54 /// - **Safety**: the entry's must be marked as a child, which implies that it has a `raw_count` of 0.
55 /// ## Postconditions
56 /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) are preserved.
57 /// - **Safety**: the entry's raw count is incremented by 1.
58 /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
59 /// - **Correctness**: the `PTE` is equivalent to the original `Child`.
60 /// ## Safety
61 /// The `PTE` safety invariants ensure that the raw pointer to the entry is tracked correctly
62 /// so that we can guarantee the safety condition on `from_pte`.
63 #[verus_spec(res =>
64 with Tracked(owner): Tracked<&mut EntryOwner<C>>,
65 requires
66 old(owner).inv_base(),
67 self.wf(*old(owner)),
68 self matches Child::Frame(paddr, level, prop) ==> C::E::new_page_req(paddr, level, prop),
69 ensures
70 final(owner).inv(),
71 final(owner).match_pte(res, final(owner).parent_level),
72 *final(owner) == old(owner).into_pte_owner_spec(),
73 old(owner).is_node() ==> res == C::E::new_pt_spec(
74 meta_to_frame(old(owner).node().slot_vaddr()),
75 ),
76 )]
77 pub fn into_pte(self) -> C::E {
78 proof {
79 C::E::lemma_page_table_entry_properties();
80 }
81
82 match self {
83 Child::PageTable(node) => {
84 let paddr = node.start_paddr();
85 let _ = ManuallyDrop::new(node);
86 C::E::new_pt(paddr)
87 },
88 Child::Frame(paddr, level, prop) => { C::E::new_page(paddr, level, prop) },
89 Child::None => { C::E::new_absent() },
90 }
91 }
92
93 /// Converts a `PTE` to a `Child`.
94 ///
95 /// # Verified Properties
96 /// ## Preconditions
97 /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
98 /// - **Safety**: `level` must match the original level of the child.
99 /// ## Postconditions
100 /// - **Safety Invariants**: the [safety invariants](Child::invariants) are preserved.
101 /// - **Safety**: the `EntryOwner` is aware that it is tracking an entry in `Child` form.
102 /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
103 /// - **Correctness**: the `Child` is equivalent to the original `PTE`.
104 /// ## Safety
105 /// The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::into_pte`]
106 /// (or another function that calls `ManuallyDrop::new`, which is sufficient for safety).
107 #[verus_spec(res =>
108 with Tracked(regions): Tracked<& MetaRegionOwners>,
109 Tracked(entry_own): Tracked<&mut EntryOwner<C>>,
110 requires
111 old(entry_own).pte_invariants(pte, *regions),
112 level == old(entry_own).parent_level,
113 ensures
114 res.invariants(*final(entry_own), *regions),
115 res == Child::<C>::from_pte_spec(pte, level, *regions),
116 *final(entry_own) == old(entry_own).from_pte_owner_spec(),
117 )]
118 pub unsafe fn from_pte(pte: C::E, level: PagingLevel) -> Self {
119 if !pte.is_present() {
120 return Child::None;
121 }
122 let paddr = pte.paddr();
123
124 if !pte.is_last(level) {
125 proof {
126 broadcast use group_page_meta;
127
128 regions.lemma_contains_valid_frame_paddr(paddr);
129 }
130 let tracked slot_perm = regions.tracked_borrow_slot(paddr);
131
132 proof_with!{ tracked_slot_perm: Tracked(slot_perm), tracked_metadata_perm: Tracked(None) }
133 let node = PageTableNode::<C> {
134 ptr: PPtr::from_addr(frame_to_meta(paddr)),
135 _marker: PhantomData,
136 };
137
138 return Child::PageTable(node);
139 }
140 Child::Frame(paddr, level, pte.prop())
141 }
142}
143
144/// A reference to the child of a page table node.
145/// # Verification Design
146/// If the child is itself a page table node, it is represented by a [`PageTableNodeRef`],
147/// because a reference to it must be treated as a potentially shared reference of the appropriate lifetime.
148/// By contrast, a mapped frame can be referenced by just carrying its values, and an absent one is just a simple tag.
149pub enum ChildRef<'a, C: PageTableConfig> {
150 /// A child page table node.
151 PageTable(PageTableNodeRef<'a, C>),
152 /// Physical address of a mapped physical frame.
153 ///
154 /// It is associated with the virtual page property and the level of the
155 /// mapping node, which decides the size of the frame.
156 Frame(Paddr, PagingLevel, PageProperty),
157 None,
158}
159
160#[verus_verify]
161impl<C: PageTableConfig> ChildRef<'_, C> {
162 /// Converts a PTE to a reference to a child.
163 ///
164 /// # Verified Properties
165 /// ## Preconditions
166 /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
167 /// - **Safety**: `level` must match the original level of the child.
168 /// ## Postconditions
169 /// - **Safety Invariants**: the [safety invariants](ChildRef::invariants) are preserved.
170 /// - **Correctness**: the `ChildRef` is equivalent to the original `PTE`.
171 /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
172 /// ## Safety
173 /// - The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::from_pte`]
174 /// - The soundness of using the resulting `ChildRef` as a reference follows from `FrameRef` safety.
175 #[verus_spec(res =>
176 with Tracked(regions): Tracked<&mut MetaRegionOwners>,
177 Tracked(entry_owner): Tracked<&EntryOwner<C>>,
178 requires
179 entry_owner.pte_invariants(*pte, *old(regions)),
180 level == entry_owner.parent_level,
181 ensures
182 res.invariants(*entry_owner, *final(regions)),
183 final(regions).slot_owners == old(regions).slot_owners,
184 forall|k: int|
185 old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(
186 k,
187 ),
188 forall|k: int|
189 old(regions).slots.contains_key(k) ==> old(regions).slots[k]
190 == #[trigger] final(regions).slots[k],
191 )]
192 pub unsafe fn from_pte(pte: &C::E, level: PagingLevel) -> Self {
193 if !pte.is_present() {
194 return ChildRef::None;
195 }
196 let paddr = pte.paddr();
197
198 if !pte.is_last(level) {
199 proof {
200 broadcast use group_page_meta;
201
202 }
203
204 let tracked node_owner = entry_owner.tracked_borrow_node();
205 let tracked slot_perm = *regions.slots.tracked_borrow(node_owner.slot_index);
206 let node = unsafe {
207 #[verus_spec(with Tracked(slot_perm), Tracked(&node_owner.frame_permission))]
208 PageTableNodeRef::borrow_paddr(paddr)
209 };
210
211 return ChildRef::PageTable(node);
212 }
213 ChildRef::Frame(paddr, level, pte.prop())
214 }
215}
216
217} // verus!