ostd/specs/mm/page_table/node/
page_table_node_specs.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> Child<C> {
17    #[rustc_allow_incoherent_impl]
18    pub open spec fn into_pte_pt_spec(self, slot_own: MetaSlotOwner) -> C::E {
19        C::E::new_pt_spec(meta_to_frame(slot_own.self_addr))
20    }
21
22    #[rustc_allow_incoherent_impl]
23    pub open spec fn into_pte_frame_spec(self, tuple: (Paddr, PagingLevel, PageProperty)) -> C::E {
24        let (paddr, level, prop) = tuple;
25        C::E::new_page_spec(paddr, level, prop)
26    }
27
28    #[rustc_allow_incoherent_impl]
29    pub open spec fn into_pte_none_spec(self) -> C::E {
30        C::E::new_absent_spec()
31    }
32
33    #[rustc_allow_incoherent_impl]
34    pub open spec fn from_pte_frame_spec(pte: C::E, level: PagingLevel) -> Self {
35        Self::Frame(pte.paddr(), level, pte.prop())
36    }
37
38    #[rustc_allow_incoherent_impl]
39    pub open spec fn from_pte_pt_spec(paddr: Paddr, regions: MetaRegionOwners) -> Self {
40        Self::PageTable(PageTableNode::from_raw_spec(paddr))
41    }
42}
43
44} // verus!
ostd/specs/mm/page_table/node/page_table_node_specs.rs

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