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        &&& pa_is_valid_pt_address(self.leaf.map_to_pa)
98        &&& level_is_in_range(
99            self.leaf.level as int,
100        )
101        // The corresponding virtual address must be aligned to the upper-level page size.
102        &&& self.leaf.map_va % (page_size_spec((self.leaf.level + 1) as PagingLevel) as int)
103            == 0
104        // Ancestor properties.
105        &&& forall|ancestor_level: int| #[trigger]
106            self.ancestor_chain.contains_key(ancestor_level) ==> {
107                &&& level_is_in_range(ancestor_level)
108                &&& self.leaf.level < ancestor_level
109                &&& self.ancestor_chain[ancestor_level].inv()
110                &&& self.ancestor_chain[ancestor_level].level
111                    == ancestor_level
112                // No loops.
113                //                &&& #[trigger] self.ancestor_chain[ancestor_level].frame_pa
114                //                    != self.leaf.map_to_pa
115                // The map-to-addresses actually forms a chain.
116                &&& if ancestor_level == self.leaf.level + 1 {
117                    self.ancestor_chain[ancestor_level].map_to_pa == self.leaf.map_to_pa
118                } else {
119                    /*                    &&& self.ancestor_chain.contains_key(ancestor_level - 1)
120                        ==> #[trigger] self.ancestor_chain[ancestor_level].map_to_pa
121                        == self.ancestor_chain[ancestor_level - 1].frame_pa*/
122                    true
123                }/*                &&& if self.ancestor_chain.contains_key(ancestor_level + 1) {
124                    self.ancestor_chain[ancestor_level + 1].map_to_pa
125                        == self.ancestor_chain[ancestor_level].frame_pa
126                    } else {
127                        true
128                    }*/
129                // The ancestor is not duplicate.
130                &&& forall|other_ancestor_level: int| #[trigger]
131                    self.ancestor_chain.contains_key(other_ancestor_level) ==> {
132                        ||| other_ancestor_level == ancestor_level
133                        ||| self.ancestor_chain[other_ancestor_level]
134                            != self.ancestor_chain[ancestor_level]
135                    }
136            }
137    }
138}
139
140impl<C: PageTableConfig> LeafPageTableEntryView<C> {
141    pub open spec fn to_frame_view(
142        self,  /*, ancestors: Map<int, IntermediatePageTableEntryView<C>>*/
143    ) -> FrameView<C> {
144        FrameView { ancestor_chain: Map::empty(), leaf: self }
145    }
146}
147
148pub ghost enum EntryView<C: PageTableConfig> {
149    Leaf { leaf: LeafPageTableEntryView<C> },
150    Intermediate { node: IntermediatePageTableEntryView<C> },
151    LockedSubtree { views: Seq<FrameView<C>> },
152    Absent,
153}
154
155impl<C: PageTableConfig> Inv for EntryView<C> {
156    open spec fn inv(self) -> bool {
157        match self {
158            Self::Leaf { leaf: _ } => self->leaf.inv(),
159            Self::Intermediate { node: _ } => self->node.inv(),
160            Self::LockedSubtree { views: _ } => forall|i: int| #[trigger] self->views[i].inv(),
161            Self::Absent => true,
162        }
163    }
164}
165
166} // verus!
ostd/specs/mm/page_table/node/entry_view.rs

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