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            final(owner).pte_invariants(res, *final(regions)),
71            *final(regions) == old(owner).into_pte_regions_spec(*old(regions)),
72            *final(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 {
102                    owner.in_scope = false;
103                }
104                C::E::new_page(paddr, level, prop)
105            },
106            Child::None => {
107                proof {
108                    owner.in_scope = false;
109                }
110                C::E::new_absent()
111            },
112        }
113    }
114
115    /// Converts a `PTE` to a `Child`.
116    ///
117    /// # Verified Properties
118    /// ## Preconditions
119    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
120    /// - **Safety**: `level` must match the original level of the child.
121    /// ## Postconditions
122    /// - **Safety Invariants**: the [safety invariants](Child::invariants) are preserved.
123    /// - **Safety**: the `EntryOwner` is aware that it is tracking an entry in `Child` form.
124    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
125    /// - **Correctness**: the `Child` is equivalent to the original `PTE`.
126    /// ## Safety
127    /// The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::into_pte`]
128    /// (or another function that calls `ManuallyDrop::new`, which is sufficient for safety).
129    #[verus_spec(
130        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
131            Tracked(entry_own): Tracked<&mut EntryOwner<C>>,
132    )]
133    pub fn from_pte(pte: C::E, level: PagingLevel) -> (res: Self)
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        if !pte.is_present() {
144            proof {
145                entry_own.in_scope = true;
146            }
147            return Child::None;
148        }
149        let paddr = pte.paddr();
150
151        if !pte.is_last(level) {
152            proof {
153                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
154
155                regions.inv_implies_correct_addr(paddr);
156            }
157
158            proof_decl! {
159                let tracked from_raw_debt: crate::specs::mm::frame::frame_specs::BorrowDebt;
160            }
161
162            #[verus_spec(with Tracked(regions), Tracked(&entry_own.node.tracked_borrow().meta_perm) => Tracked(from_raw_debt))]
163            let node = PageTableNode::from_raw(paddr);
164
165            proof {
166                // raw_count was 1 (node was in a PTE via into_raw), so discharge trivially.
167                from_raw_debt.discharge_bookkeeping();
168
169                entry_own.in_scope = true;
170
171                assert(regions.slot_owners =~= entry_own.from_pte_regions_spec(
172                    *old(regions),
173                ).slot_owners);
174                assert(regions.slots =~= entry_own.from_pte_regions_spec(*old(regions)).slots);
175            }
176
177            return Child::PageTable(node);
178        }
179        proof {
180            entry_own.in_scope = true;
181        }
182        Child::Frame(paddr, level, pte.prop())
183    }
184}
185
186/// A reference to the child of a page table node.
187/// # Verification Design
188/// If the child is itself a page table node, it is represented by a [`PageTableNodeRef`],
189/// because a reference to it must be treated as a potentially shared reference of the appropriate lifetime.
190/// By contrast, a mapped frame can be referenced by just carrying its values, and an absent one is just a simple tag.
191pub enum ChildRef<'a, C: PageTableConfig> {
192    /// A child page table node.
193    PageTable(PageTableNodeRef<'a, C>),
194    /// Physical address of a mapped physical frame.
195    ///
196    /// It is associated with the virtual page property and the level of the
197    /// mapping node, which decides the size of the frame.
198    Frame(Paddr, PagingLevel, PageProperty),
199    None,
200}
201
202impl<C: PageTableConfig> ChildRef<'_, C> {
203    /// Converts a PTE to a reference to a child.
204    ///
205    /// # Verified Properties
206    /// ## Preconditions
207    /// - **Safety Invariants**: the `PTE`'s [safety invariants](EntryOwner::pte_invariants) must hold.
208    /// - **Safety**: `level` must match the original level of the child.
209    /// ## Postconditions
210    /// - **Safety Invariants**: the [safety invariants](ChildRef::invariants) are preserved.
211    /// - **Correctness**: the `ChildRef` is equivalent to the original `PTE`.
212    /// - **Safety**: No frame other than the target entry's (if applicable) is impacted by the call.
213    /// ## Safety
214    /// - The `PTE` safety invariants require that the `PTE` was previously obtained using [`Self::from_pte`]
215    /// - The soundness of using the resulting `ChildRef` as a reference follows from `FrameRef` safety.
216    #[verus_spec(
217        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
218            Tracked(entry_owner): Tracked<&EntryOwner<C>>
219    )]
220    pub fn from_pte(pte: &C::E, level: PagingLevel) -> (res: Self)
221        requires
222            entry_owner.pte_invariants(*pte, *old(regions)),
223            level == entry_owner.parent_level,
224        ensures
225            res.invariants(*entry_owner, *final(regions)),
226            final(regions).slot_owners =~= old(regions).slot_owners,
227            forall |k: usize| old(regions).slots.contains_key(k) ==> #[trigger] final(regions).slots.contains_key(k),
228            forall |k: usize| old(regions).slots.contains_key(k) ==> old(regions).slots[k] == #[trigger] final(regions).slots[k],
229    {
230        if !pte.is_present() {
231            return ChildRef::None;
232        }
233        let paddr = pte.paddr();
234
235        if !pte.is_last(level) {
236            proof {
237                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
238
239                regions.inv_implies_correct_addr(paddr);
240                assert(entry_owner.metaregion_sound(*regions));
241                assert(entry_owner.meta_slot_paddr().unwrap() == paddr);
242            }
243
244            #[verus_spec(with Tracked(regions), Tracked(&entry_owner.node.tracked_borrow().meta_perm))]
245            let node = PageTableNodeRef::borrow_paddr(paddr);
246
247            proof {
248                // borrow_paddr postcondition gives raw_count == 1 and field-by-field preservation.
249                // Since raw_count was already 1 (entry is in PTE, in_scope == false),
250                // slot_owners[idx] == old(slot_owners[idx]) follows field by field.
251                assert(regions.slot_owners =~= old(regions).slot_owners);
252                // slots: borrow_paddr inserts at borrow_idx. Prove existing keys preserved.
253                // The node's slot was NOT in old.slots: by active_entry_not_in_free_pool,
254                // a node entry's index can't equal any free-pool index.
255                let borrow_idx = frame_to_index(paddr);
256                assert(entry_owner.is_node());
257                let ghost entry_snap = *entry_owner;
258                assert(!old(regions).slots.contains_key(borrow_idx)) by {
259                    if old(regions).slots.contains_key(borrow_idx) {
260                        EntryOwner::<C>::active_entry_not_in_free_pool(
261                            entry_snap,
262                            *old(regions),
263                            borrow_idx,
264                        );
265                        // gives borrow_idx != borrow_idx — contradiction
266                    }
267                };
268                // Since borrow_idx was not in old.slots, insert preserves all old keys.
269                assert forall|k: usize| old(regions).slots.contains_key(k) implies old(
270                    regions,
271                ).slots[k] == #[trigger] regions.slots[k] by {
272                    assert(k != borrow_idx);
273                    // regions.slots == old.slots.insert(borrow_idx, _), and k != borrow_idx
274                };
275            }
276
277            return ChildRef::PageTable(node);
278        }
279        ChildRef::Frame(paddr, level, pte.prop())
280    }
281}
282
283} // verus!
ostd/mm/page_table/node/child.rs

ostd/mm/page_table/node/
child.rs
