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

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

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