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

1use vstd::prelude::*;
2use vstd_extra::ownership::*;
3
4use crate::specs::arch::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE, *};
5
6use crate::arch::mm::PagingConsts;
7use crate::mm::{
8    Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_prop::PageProperty, page_size, page_table::*,
9};
10use core::marker::PhantomData;
11
12verus! {
13
14pub open spec fn pa_is_valid_pt_address(pa: int) -> bool {
15    &&& pa_is_valid_kernel_address(pa as int)
16    &&& pa % PAGE_SIZE as int == 0
17}
18
19pub open spec fn PHYSICAL_BASE_ADDRESS_SPEC() -> usize {
20    0
21}
22
23pub open spec fn pa_is_valid_kernel_address(pa: int) -> bool {
24    PHYSICAL_BASE_ADDRESS_SPEC() <= pa < PHYSICAL_BASE_ADDRESS_SPEC() + PAGE_SIZE * MAX_NR_PAGES
25}
26
27pub ghost struct LeafPageTableEntryView<C: PageTableConfig> {
28    pub map_va: int,
29    //    pub frame_pa: int,
30    //    pub in_frame_index: int,
31    pub map_to_pa: int,
32    pub level: PagingLevel,
33    pub prop: PageProperty,
34    pub phantom: PhantomData<C>,
35}
36
37impl<C: PageTableConfig> Inv for LeafPageTableEntryView<C> {
38    open spec fn inv(self) -> bool {
39        //        &&& pa_is_valid_pt_address(self.frame_pa)
40        &&& pa_is_valid_kernel_address(
41            self.map_to_pa,
42        )
43        // We assume that all level PTEs can be leaf. Thus they can map to huge pages.
44        &&& 1 <= self.level
45            <= NR_LEVELS
46        // The corresponding virtual address must be aligned to the page size.
47        &&& self.map_va % (page_size::<PagingConsts>(self.level) as int) == 0
48    }
49}
50
51impl<C: PageTableConfig> LeafPageTableEntryView<C> {
52    pub open spec fn va_end(self) -> Vaddr {
53        (self.map_va + page_size::<PagingConsts>(self.level)) as Vaddr
54    }
55}
56
57pub ghost struct IntermediatePageTableEntryView<C: PageTableConfig> {
58    pub map_va: int,
59    //    pub frame_pa: int,
60    //    pub in_frame_index: int,
61    pub map_to_pa: int,
62    pub level: PagingLevel,
63    pub phantom: PhantomData<C>,
64}
65
66impl<C: PageTableConfig> Inv for IntermediatePageTableEntryView<C> {
67    open spec fn inv(self) -> bool {
68        //        &&& pa_is_valid_pt_address(self.frame_pa)
69        &&& pa_is_valid_pt_address(self.map_to_pa)
70        &&& 1 <= self.level <= NR_LEVELS
71        // No self-loop.
72        //        &&& self.map_to_pa != self.frame_pa
73        // The corresponding virtual address must be aligned to the page size.
74        &&& self.map_va % (page_size::<PagingConsts>(self.level) as int) == 0
75    }
76}
77
78pub ghost struct FrameView<C: PageTableConfig> {
79    /// A map from the ancestor frame level to the PTE that the ancestor maps to its child.
80    pub ancestor_chain: Map<int, IntermediatePageTableEntryView<C>>,
81    /// The view of the page table leaf entry
82    pub leaf: LeafPageTableEntryView<C>,
83}
84
85impl<C: PageTableConfig> Inv for FrameView<C> {
86    open spec fn inv(self) -> bool {
87        true
88    }
89}
90
91impl<C: PageTableConfig> LeafPageTableEntryView<C> {
92    pub open spec fn to_frame_view(
93        self,  /*, ancestors: Map<int, IntermediatePageTableEntryView<C>>*/
94    ) -> FrameView<C> {
95        FrameView { ancestor_chain: Map::empty(), leaf: self }
96    }
97}
98
99} // verus!
ostd/specs/mm/page_table/node/entry_view.rs

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