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
34        * MAX_NR_PAGES as int
35}
36
37pub ghost struct LeafPageTableEntryView<C: PageTableConfig> {
38    pub map_va: int,
39    //    pub frame_pa: int,
40    //    pub in_frame_index: int,
41    pub map_to_pa: int,
42    pub level: PagingLevel,
43    pub prop: PageProperty,
44    pub phantom: PhantomData<C>,
45}
46
47impl<C: PageTableConfig> Inv for LeafPageTableEntryView<C> {
48    open spec fn inv(self) -> bool {
49        //        &&& pa_is_valid_pt_address(self.frame_pa)
50        //        &&& index_is_in_range(self.in_frame_index)
51        &&& pa_is_valid_kernel_address(
52            self.map_to_pa,
53        )
54        // We assume that all level PTEs can be leaf. Thus they can map to huge pages.
55        &&& level_is_in_range(
56            self.level as int,
57        )
58        // The corresponding virtual address must be aligned to the page size.
59        &&& self.map_va % (page_size_spec(self.level) as int) == 0
60    }
61}
62
63impl<C: PageTableConfig> LeafPageTableEntryView<C> {
64    pub uninterp spec fn va_end(self) -> Vaddr;
65}
66
67pub ghost struct IntermediatePageTableEntryView<C: PageTableConfig> {
68    pub map_va: int,
69    //    pub frame_pa: int,
70    //    pub in_frame_index: int,
71    pub map_to_pa: int,
72    pub level: PagingLevel,
73    pub phantom: PhantomData<C>,
74}
75
76impl<C: PageTableConfig> Inv for IntermediatePageTableEntryView<C> {
77    open spec fn inv(self) -> bool {
78        //        &&& pa_is_valid_pt_address(self.frame_pa)
79        //        &&& index_is_in_range(self.in_frame_index)
80        &&& pa_is_valid_pt_address(self.map_to_pa)
81        &&& level_is_in_range(self.level as int)
82        // No self-loop.
83        //        &&& self.map_to_pa != self.frame_pa
84        // The corresponding virtual address must be aligned to the page size.
85        &&& self.map_va % (page_size_spec(self.level) as int) == 0
86    }
87}
88
89pub ghost struct FrameView<C: PageTableConfig> {
90    /// A map from the ancestor frame level to the PTE that the ancestor maps to its child.
91    pub ancestor_chain: Map<int, IntermediatePageTableEntryView<C>>,
92    /// The view of the page table leaf entry
93    pub leaf: LeafPageTableEntryView<C>,
94}
95
96impl<C: PageTableConfig> Inv for FrameView<C> {
97    open spec fn inv(self) -> bool {
98        true
99    }
100}
101
102impl<C: PageTableConfig> LeafPageTableEntryView<C> {
103    pub open spec fn to_frame_view(
104        self,  /*, ancestors: Map<int, IntermediatePageTableEntryView<C>>*/
105    ) -> FrameView<C> {
106        FrameView { ancestor_chain: Map::empty(), leaf: self }
107    }
108}
109
110pub ghost enum EntryView<C: PageTableConfig> {
111    Leaf { leaf: LeafPageTableEntryView<C> },
112    Intermediate { node: IntermediatePageTableEntryView<C> },
113    LockedSubtree { views: Seq<FrameView<C>> },
114    Absent,
115}
116
117impl<C: PageTableConfig> Inv for EntryView<C> {
118    open spec fn inv(self) -> bool {
119        true/*
120        match self {
121            Self::Leaf { leaf: _ } => self->leaf.inv(),
122            Self::Intermediate { node: _ } => self->node.inv(),
123            Self::LockedSubtree { views: _ } => forall|i: int| #[trigger] self->views[i].inv(),
124            Self::Absent => true,
125        }
126        */
127
128    }
129}
130
131} // verus!
ostd/specs/mm/page_table/node/entry_view.rs

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