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

ostd/mm/page_table/node/
child.rs
