ostd/specs/mm/page_table/
view.rs

1use vstd::prelude::*;
2
3use vstd_extra::ownership::*;
4
5use core::marker::PhantomData;
6use core::ops::Range;
7
8use crate::mm::page_prop::PageProperty;
9use crate::mm::{Paddr, Vaddr};
10use crate::specs::arch::mm::{MAX_PADDR, MAX_USERSPACE_VADDR};
11
12use super::*;
13
14verus! {
15
16pub ghost struct PageTableView {
17    pub mappings: Set<Mapping>
18}
19
20pub tracked struct Mapping {
21    pub va_range: Range<Vaddr>,
22    pub pa_range: Range<Paddr>,
23    pub page_size: usize,
24    pub property: PageProperty,
25}
26
27impl Mapping {
28    pub open spec fn inv(self) -> bool {
29        &&& set![4096, 2097152, 1073741824].contains(self.page_size)
30        &&& self.pa_range.start % self.page_size == 0
31        &&& self.pa_range.end % self.page_size == 0
32        &&& self.pa_range.start + self.page_size == self.pa_range.end
33        &&& self.pa_range.start <= self.pa_range.end < MAX_PADDR()
34        &&& self.va_range.start % self.page_size == 0
35        &&& self.va_range.end % self.page_size == 0
36        &&& self.va_range.start + self.page_size == self.va_range.end
37        &&& 0 < self.va_range.start <= self.va_range.end < MAX_USERSPACE_VADDR()
38    }
39}
40
41impl Inv for PageTableView {
42    open spec fn inv(self) -> bool {
43        &&& forall|m: Mapping| #![auto] self.mappings.contains(m) ==> m.inv()
44        &&& forall|m: Mapping, n:Mapping| #![auto]
45            self.mappings.contains(m) ==>
46            self.mappings.contains(n) ==>
47            m != n ==>
48            m.va_range.end <= n.va_range.start || n.va_range.end <= m.va_range.start
49    }
50}
51
52} // verus!
ostd/specs/mm/page_table/view.rs

ostd/specs/mm/page_table/
view.rs
