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

1use vstd::prelude::*;
2
3use core::marker::PhantomData;
4
5use crate::arch::mm::PagingConsts;
6use crate::mm::page_prop::PageProperty;
7use crate::mm::page_table::*;
8use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_size};
9use crate::specs::arch::*;
10use crate::specs::arch::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
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
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(self.level) as int) == 0
59    }
60}
61
62impl<C: PageTableConfig> LeafPageTableEntryView<C> {
63    pub open spec fn va_end(self) -> Vaddr {
64        (self.map_va + page_size(self.level)) as Vaddr
65    }
66}
67
68pub ghost struct IntermediatePageTableEntryView<C: PageTableConfig> {
69    pub map_va: int,
70    //    pub frame_pa: int,
71    //    pub in_frame_index: int,
72    pub map_to_pa: int,
73    pub level: PagingLevel,
74    pub phantom: PhantomData<C>,
75}
76
77impl<C: PageTableConfig> Inv for IntermediatePageTableEntryView<C> {
78    open spec fn inv(self) -> bool {
79        //        &&& pa_is_valid_pt_address(self.frame_pa)
80        //        &&& index_is_in_range(self.in_frame_index)
81        &&& pa_is_valid_pt_address(self.map_to_pa)
82        &&& level_is_in_range(self.level as int)
83        // No self-loop.
84        //        &&& self.map_to_pa != self.frame_pa
85        // The corresponding virtual address must be aligned to the page size.
86        &&& self.map_va % (page_size(self.level) as int) == 0
87    }
88}
89
90pub ghost struct FrameView<C: PageTableConfig> {
91    /// A map from the ancestor frame level to the PTE that the ancestor maps to its child.
92    pub ancestor_chain: Map<int, IntermediatePageTableEntryView<C>>,
93    /// The view of the page table leaf entry
94    pub leaf: LeafPageTableEntryView<C>,
95}
96
97impl<C: PageTableConfig> Inv for FrameView<C> {
98    open spec fn inv(self) -> bool {
99        true
100    }
101}
102
103impl<C: PageTableConfig> LeafPageTableEntryView<C> {
104    pub open spec fn to_frame_view(
105        self,  /*, ancestors: Map<int, IntermediatePageTableEntryView<C>>*/
106    ) -> FrameView<C> {
107        FrameView { ancestor_chain: Map::empty(), leaf: self }
108    }
109}
110
111pub ghost enum EntryView<C: PageTableConfig> {
112    Leaf { leaf: LeafPageTableEntryView<C> },
113    Intermediate { node: IntermediatePageTableEntryView<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::Absent => true,
124        }
125        */
126
127    }
128}
129
130} // verus!
ostd/specs/mm/page_table/node/entry_view.rs

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