ostd/specs/mm/page_table/node/
child.rs

1use vstd::prelude::*;
2
3use vstd_extra::ownership::*;
4
5use crate::specs::mm::frame::{mapping::meta_to_index, meta_region_owners::MetaRegionOwners};
6
7use crate::arch::mm::PagingConsts;
8use crate::mm::{
9    Paddr, PagingConstsTrait, PagingLevel, Vaddr, frame::*, page_prop::PageProperty, page_table::*,
10};
11
12verus! {
13
14impl<C: PageTableConfig> OwnerOf for Child<C> {
15    type Owner = EntryOwner<C>;
16
17    open spec fn wf(self, owner: Self::Owner) -> bool {
18        match self {
19            Self::PageTable(node) => {
20                &&& owner.is_node()
21                &&& node.ptr.addr() == owner.node().meta_vaddr()
22                &&& node.index() == meta_to_index(node.ptr.addr())
23            },
24            Self::Frame(paddr, level, prop) => {
25                &&& owner.is_frame()
26                &&& owner.frame().mapped_pa == paddr
27                &&& owner.frame().prop == prop
28                &&& level == owner.parent_level
29            },
30            Self::None => owner.is_absent(),
31        }
32    }
33}
34
35impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
36    type Owner = EntryOwner<C>;
37
38    open spec fn wf(self, owner: Self::Owner) -> bool {
39        match self {
40            Self::PageTable(node) => {
41                &&& owner.is_node()
42                &&& node.inner@.ptr.addr() == owner.node().meta_vaddr()
43            },
44            Self::Frame(paddr, level, prop) => {
45                &&& owner.is_frame()
46                &&& owner.frame().mapped_pa == paddr
47                &&& owner.frame().prop == prop
48            },
49            Self::None => owner.is_absent(),
50        }
51    }
52}
53
54impl<C: PageTableConfig> Child<C> {
55    pub open spec fn get_node(self) -> Option<PageTableNode<C>> {
56        match self {
57            Self::PageTable(node) => Some(node),
58            _ => None,
59        }
60    }
61
62    pub open spec fn get_frame_tuple(self) -> Option<(Paddr, PagingLevel, PageProperty)> {
63        match self {
64            Self::Frame(paddr, level, prop) => Some((paddr, level, prop)),
65            _ => None,
66        }
67    }
68
69    pub open spec fn into_pte_frame_spec(self, tuple: (Paddr, PagingLevel, PageProperty)) -> C::E {
70        let (paddr, level, prop) = tuple;
71        C::E::new_page_spec(paddr, level, prop)
72    }
73
74    pub open spec fn into_pte_none_spec(self) -> C::E {
75        C::E::new_absent_spec()
76    }
77
78    pub open spec fn from_pte_spec(
79        pte: C::E,
80        level: PagingLevel,
81        regions: MetaRegionOwners,
82    ) -> Self {
83        if !pte.is_present() {
84            Self::None
85        } else if pte.is_last(level) {
86            Self::Frame(pte.paddr(), level, pte.prop())
87        } else {
88            Self::PageTable(PageTableNode::from_raw_spec(pte.paddr()))
89        }
90    }
91
92    pub open spec fn from_pte_frame_spec(pte: C::E, level: PagingLevel) -> Self {
93        Self::Frame(pte.paddr(), level, pte.prop())
94    }
95
96    pub open spec fn from_pte_pt_spec(paddr: Paddr, regions: MetaRegionOwners) -> Self {
97        Self::PageTable(PageTableNode::from_raw_spec(paddr))
98    }
99
100    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
101        &&& owner.inv_base()
102        &&& regions.inv()
103        &&& self.wf(owner)
104        &&& match self {
105            Self::Frame(paddr, level, prop) => C::E::new_page_req(paddr, level, prop),
106            _ => true,
107        }
108        &&& owner.metaregion_sound(regions)
109    }
110}
111
112impl<C: PageTableConfig> ChildRef<'_, C> {
113    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
114        &&& owner.inv()
115        &&& regions.inv()
116        &&& self.wf(owner)
117        &&& owner.metaregion_sound(regions)
118    }
119}
120
121impl<C: PageTableConfig> EntryOwner<C> {
122    pub open spec fn from_pte_regions_spec(self, regions: MetaRegionOwners) -> MetaRegionOwners {
123        if self.is_node() {
124            let index = frame_to_index(self.meta_slot_paddr()->0);
125            MetaRegionOwners {
126                frame_obligations: regions.frame_obligations.insert(index),
127                ..regions
128            }
129        } else {
130            regions
131        }
132    }
133
134    pub open spec fn into_pte_regions_spec(self, regions: MetaRegionOwners) -> MetaRegionOwners {
135        if self.is_node() {
136            let index = frame_to_index(self.meta_slot_paddr()->0);
137            // Canonical model: forgetting a live PT-node into a PTE CONSUMES
138            // its pending-Drop obligation (the body's `MD::new` redeems one
139            // entry at the node's slot), mirroring `Frame::into_raw`. `slots`
140            // / `slot_owners` are untouched. Balances the `+1` minted by
141            // `from_pte` (`from_pte_regions_spec`) / `PageTableNode::alloc`.
142            MetaRegionOwners {
143                frame_obligations: regions.frame_obligations.remove(index),
144                ..regions
145            }
146        } else {
147            // Forgetting a mapped frame / clearing an absent entry leaves the
148            // per-frame ledger untouched (`item_into_raw` is `external_body`).
149            regions
150        }
151    }
152
153    pub open spec fn into_pte_owner_spec(self) -> EntryOwner<C> {
154        self
155    }
156
157    pub open spec fn from_pte_owner_spec(self) -> EntryOwner<C> {
158        self
159    }
160
161    /// This is equivalent to the other `invariants` relations, combining the `inv` predicates for each
162    /// object and the well-formedness relations between them.
163    pub open spec fn pte_invariants(self, pte: C::E, regions: MetaRegionOwners) -> bool {
164        &&& self.inv()
165        &&& regions.inv()
166        &&& self.match_pte(pte, self.parent_level)
167        &&& self.metaregion_sound(regions)
168    }
169}
170
171} // verus!
ostd/specs/mm/page_table/node/child.rs

ostd/specs/mm/page_table/node/
child.rs
