ostd/specs/mm/page_table/
view.rs

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

ostd/specs/mm/page_table/
view.rs
