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

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

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