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

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

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