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
16/// A `Mapping` maps a virtual address range to a physical address range.
17/// Its size, `page_size`, is fixed and must be one of 4096, 2097152, 1073741824.
18/// The `va_range` and `pa_range` must of size `page_size` and aligned on a page boundary.
19/// The `property` is a bitfield of flags that describe the properties of the mapping.
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
27/// A view of the page table is simply the set of mappings that it contains.
28/// Its [invariant](PageTableView::inv) is a crucial property for memory correctness.
29pub ghost struct PageTableView {
30    pub mappings: Set<Mapping>
31}
32
33impl Mapping {
34    pub open spec fn disjoint_vaddrs(m1: Mapping, m2: Mapping) -> bool {
35        m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start
36    }
37
38    pub open spec fn disjoint_paddrs(m1: Mapping, m2: Mapping) -> bool {
39        m1.pa_range.end <= m2.pa_range.start || m2.pa_range.end <= m1.pa_range.start
40    }
41
42    pub open spec fn inv(self) -> bool {
43        &&& set![4096, 2097152, 1073741824].contains(self.page_size)
44        &&& self.pa_range.start % self.page_size == 0
45        &&& self.pa_range.end % self.page_size == 0
46        &&& self.pa_range.start + self.page_size == self.pa_range.end
47        &&& self.pa_range.start <= self.pa_range.end < MAX_PADDR
48        &&& self.va_range.start % self.page_size == 0
49        &&& self.va_range.end % self.page_size == 0
50        &&& self.va_range.start + self.page_size == self.va_range.end
51        &&& 0 < self.va_range.start <= self.va_range.end < MAX_USERSPACE_VADDR
52    }
53}
54
55/// In addition to requiring that individual mappings be well-formed, a valid `PageTableView` must
56/// not have any overlapping mappings, in the physical or virtual address space.
57/// The virtual ranges not overlapping is a consequence of the structure of the page table.
58/// The physical ranges not overlapping must be maintained by the page table implementation.
59impl PageTableView {
60    pub open spec fn inv(self) -> bool {
61        &&& forall|m: Mapping| #![auto] self.mappings has m ==> m.inv()
62        &&& forall|m: Mapping, n:Mapping| #![auto]
63            self.mappings has m ==>
64            self.mappings has n ==>
65            m != n ==> {
66                &&& m.va_range.end <= n.va_range.start || n.va_range.end <= m.va_range.start
67                &&& m.pa_range.end <= n.pa_range.start || n.pa_range.end <= m.pa_range.start
68            }
69    }
70}
71
72} // verus!
ostd/specs/mm/page_table/view.rs

ostd/specs/mm/page_table/
view.rs
