ostd/specs/mm/page_table/
view.rs

1use vstd::{arithmetic::power2::pow2, prelude::*};
2use vstd_extra::ownership::*;
3
4use crate::specs::arch::MAX_PADDR;
5
6use super::*;
7use crate::mm::{Paddr, Vaddr, page_prop::PageProperty};
8use core::{marker::PhantomData, ops::Range};
9
10verus! {
11
12/// A `Mapping` maps a virtual address range to a physical address range.
13/// Its size, `page_size`, is fixed and must be one of 4096, 2097152, 1073741824.
14/// The `va_range` and `pa_range` must be of size `page_size` and aligned on a
15/// page boundary.
16/// The `property` is a bitfield of flags that describe the properties of the mapping.
17///
18/// `va_range` is `Range<int>` rather than `Range<Vaddr>` because the
19/// canonical upper-half kernel range can reach `usize::MAX + 1` for its
20/// exclusive end (`2^64`), which cannot be represented in `usize`. The
21/// `Mapping::inv` predicate bounds `va_range.end` by `pow2(64)` so all
22/// concretely realized mappings stay within the addressable space; this
23/// is a no-op constraint for user mappings and the essential cap for
24/// kernel mappings.
25pub ghost struct Mapping {
26    pub va_range: Range<int>,
27    pub pa_range: Range<Paddr>,
28    pub page_size: usize,
29    pub property: PageProperty,
30}
31
32/// A view of the page table is simply the set of mappings that it contains.
33/// Its [invariant](PageTableView::inv) is a crucial property for memory correctness.
34pub ghost struct PageTableView {
35    pub mappings: Set<Mapping>,
36}
37
38impl Mapping {
39    pub open spec fn disjoint_vaddrs(m1: Mapping, m2: Mapping) -> bool {
40        m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start
41    }
42
43    pub open spec fn disjoint_paddrs(m1: Mapping, m2: Mapping) -> bool {
44        m1.pa_range.end <= m2.pa_range.start || m2.pa_range.end <= m1.pa_range.start
45    }
46
47    pub open spec fn inv(self) -> bool {
48        &&& set![4096, 2097152, 1073741824].contains(self.page_size)
49        &&& self.pa_range.start % self.page_size == 0
50        &&& self.pa_range.start + self.page_size == self.pa_range.end
51        &&& self.pa_range.end <= MAX_PADDR
52        &&& self.va_range.start % self.page_size as int == 0
53        &&& self.va_range.start + self.page_size as int == self.va_range.end
54        &&& 0
55            <= self.va_range.start
56        // VA range fits in the 64-bit addressable space. `va_range.end` may
57        // equal `pow2(64)` for a kernel mapping at the top of the canonical
58        // high half; `va_range.start` is strictly less than `pow2(64)`
59        // because `start + page_size == end <= pow2(64)` and `page_size > 0`.
60        &&& self.va_range.end <= pow2(64)
61    }
62}
63
64/// Every mapping in the set satisfies its intrinsic invariant.
65pub open spec fn mappings_well_formed(mappings: Set<Mapping>) -> bool {
66    forall|m: Mapping| #[trigger] mappings.contains(m) ==> m.inv()
67}
68
69/// Distinct mappings in the set have disjoint virtual address ranges.
70pub open spec fn mappings_disjoint_vaddrs(mappings: Set<Mapping>) -> bool {
71    forall|m: Mapping, n: Mapping|
72        #![trigger mappings.contains(m), mappings.contains(n)]
73        mappings.contains(m) && mappings.contains(n) && m != n ==> Mapping::disjoint_vaddrs(m, n)
74}
75
76/// Distinct mappings in the set have disjoint physical address ranges.
77pub open spec fn mappings_disjoint_paddrs(mappings: Set<Mapping>) -> bool {
78    forall|m: Mapping, n: Mapping|
79        #![trigger mappings.contains(m), mappings.contains(n)]
80        mappings.contains(m) && mappings.contains(n) && m != n ==> Mapping::disjoint_paddrs(m, n)
81}
82
83/// A valid view contains well-formed mappings with disjoint VA and PA ranges.
84impl PageTableView {
85    pub open spec fn inv(self) -> bool {
86        &&& mappings_well_formed(self.mappings)
87        &&& mappings_disjoint_vaddrs(self.mappings)
88        &&& mappings_disjoint_paddrs(self.mappings)
89    }
90}
91
92} // verus!
ostd/specs/mm/page_table/view.rs

ostd/specs/mm/page_table/
view.rs
