|
| 1 | +use vstd::prelude::*; |
| 2 | + |
| 3 | +use vstd_extra::ownership::*; |
| 4 | + |
| 5 | +use crate::mm::frame::*; |
| 6 | +use crate::mm::page_prop::PageProperty; |
| 7 | +use crate::mm::page_table::*; |
| 8 | +use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr}; |
| 9 | +use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE}; |
| 10 | +use crate::specs::arch::paging_consts::PagingConsts; |
| 11 | +use crate::specs::mm::frame::meta_owners::MetaSlotOwner; |
| 12 | +use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners; |
| 13 | + |
| 14 | +verus! { |
| 15 | + |
| 16 | +impl<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_perm.addr() |
| 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 | + |
| 37 | + |
| 38 | +impl<'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.0.ptr.addr() == owner.node.unwrap().meta_perm.addr() |
| 46 | + }, |
| 47 | + Self::Frame(paddr, level, prop) => { |
| 48 | + &&& owner.is_frame() |
| 49 | + &&& owner.frame.unwrap().mapped_pa == paddr |
| 50 | + &&& owner.frame.unwrap().prop == prop |
| 51 | + }, |
| 52 | + Self::None => owner.is_absent(), |
| 53 | + } |
| 54 | + } |
| 55 | +} |
| 56 | + |
| 57 | +impl<C: PageTableConfig> Child<C> { |
| 58 | + |
| 59 | + pub open spec fn get_node(self) -> Option<PageTableNode<C>> { |
| 60 | + match self { |
| 61 | + Self::PageTable(node) => Some(node), |
| 62 | + _ => None, |
| 63 | + } |
| 64 | + } |
| 65 | + |
| 66 | + pub open spec fn get_frame_tuple(self) -> Option<(Paddr, PagingLevel, PageProperty)> { |
| 67 | + match self { |
| 68 | + Self::Frame(paddr, level, prop) => Some((paddr, level, prop)), |
| 69 | + _ => None, |
| 70 | + } |
| 71 | + } |
| 72 | + |
| 73 | + pub open spec fn into_pte_frame_spec(self, tuple: (Paddr, PagingLevel, PageProperty)) -> C::E { |
| 74 | + let (paddr, level, prop) = tuple; |
| 75 | + C::E::new_page_spec(paddr, level, prop) |
| 76 | + } |
| 77 | + |
| 78 | + |
| 79 | + pub open spec fn into_pte_none_spec(self) -> C::E { |
| 80 | + C::E::new_absent_spec() |
| 81 | + } |
| 82 | + |
| 83 | + |
| 84 | + pub open spec fn from_pte_spec(pte: C::E, level: PagingLevel, regions: MetaRegionOwners) -> 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 | + |
| 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() |
| 105 | + &&& regions.inv() |
| 106 | + &&& self.wf(owner) |
| 107 | + &&& owner.relate_region(regions) |
| 108 | + &&& owner.in_scope |
| 109 | + } |
| 110 | +} |
| 111 | + |
| 112 | +impl<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.relate_region(regions) |
| 118 | + &&& !owner.in_scope |
| 119 | + } |
| 120 | +} |
| 121 | + |
| 122 | +impl<C: PageTableConfig> EntryOwner<C> { |
| 123 | + |
| 124 | + pub open spec fn from_pte_regions_spec(self, regions: MetaRegionOwners) -> MetaRegionOwners { |
| 125 | + if self.is_node() { |
| 126 | + let index = frame_to_index(self.meta_slot_paddr().unwrap()); |
| 127 | + let old_slot = regions.slot_owners[index]; |
| 128 | + let new_slot = MetaSlotOwner { |
| 129 | + raw_count: 0usize, |
| 130 | + ..old_slot |
| 131 | + }; |
| 132 | + MetaRegionOwners { |
| 133 | + slots: regions.slots.insert(index, self.node.unwrap().meta_perm.points_to), |
| 134 | + slot_owners: regions.slot_owners.insert(index, new_slot), |
| 135 | + } |
| 136 | + } else { |
| 137 | + regions |
| 138 | + } |
| 139 | + } |
| 140 | + |
| 141 | + pub open spec fn into_pte_regions_spec(self, regions: MetaRegionOwners) -> MetaRegionOwners { |
| 142 | + if self.is_node() { |
| 143 | + let index = frame_to_index(self.meta_slot_paddr().unwrap()); |
| 144 | + let old_slot = regions.slot_owners[index]; |
| 145 | + let new_slot = MetaSlotOwner { |
| 146 | + raw_count: (old_slot.raw_count + 1) as usize, |
| 147 | + ..old_slot |
| 148 | + }; |
| 149 | + MetaRegionOwners { |
| 150 | + slots: regions.slots, |
| 151 | + slot_owners: regions.slot_owners.insert(index, new_slot), |
| 152 | + ..regions |
| 153 | + } |
| 154 | + } else { |
| 155 | + regions |
| 156 | + } |
| 157 | + } |
| 158 | + |
| 159 | + pub open spec fn into_pte_owner_spec(self) -> EntryOwner<C> { |
| 160 | + EntryOwner { |
| 161 | + in_scope: false, |
| 162 | + ..self |
| 163 | + } |
| 164 | + } |
| 165 | + |
| 166 | + pub open spec fn from_pte_owner_spec(self) -> EntryOwner<C> { |
| 167 | + EntryOwner { |
| 168 | + in_scope: true, |
| 169 | + ..self |
| 170 | + } |
| 171 | + } |
| 172 | + |
| 173 | + /// This is equivalent to the other `invariants` relations, combining the `inv` predicates for each |
| 174 | + /// object and the well-formedness relations between them. |
| 175 | + pub open spec fn pte_invariants(self, pte: C::E, regions: MetaRegionOwners) -> bool { |
| 176 | + &&& self.inv() |
| 177 | + &&& regions.inv() |
| 178 | + &&& self.match_pte(pte, self.parent_level) |
| 179 | + &&& self.relate_region(regions) |
| 180 | + &&& !self.in_scope |
| 181 | + } |
| 182 | + |
| 183 | +} |
| 184 | + |
| 185 | +} // verus! |
0 commit comments