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

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

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