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

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

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