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.end % self.page_size == 0
51        &&& self.pa_range.start + self.page_size == self.pa_range.end
52        &&& self.pa_range.start <= self.pa_range.end <= MAX_PADDR
53        &&& self.va_range.start % self.page_size as int == 0
54        &&& self.va_range.end % self.page_size as int == 0
55        &&& self.va_range.start + self.page_size as int == self.va_range.end
56        &&& 0 <= self.va_range.start
57            <= self.va_range.end
58        // VA range fits in the 64-bit addressable space. `va_range.end` may
59        // equal `pow2(64)` for a kernel mapping at the top of the canonical
60        // high half; `va_range.start` is strictly less than `pow2(64)`
61        // because `start + page_size == end <= pow2(64)` and `page_size > 0`.
62        &&& self.va_range.end <= pow2(
63            64,
64        )
65        // Per-config VA range bounds are enforced by `CursorView<C>::inv`
66        // via `vaddr_range_spec<C>`, not here — a single
67        // config-agnostic `Mapping::inv` cannot express them.
68
69    }
70}
71
72/// In addition to requiring that individual mappings be well-formed, a valid `PageTableView` must
73/// not have any overlapping mappings, in the physical or virtual address space.
74/// The virtual ranges not overlapping is a consequence of the structure of the page table.
75/// The physical ranges not overlapping must be maintained by the page table implementation.
76impl PageTableView {
77    pub open spec fn inv(self) -> bool {
78        &&& forall|m: Mapping| #![trigger self.mappings.contains(m)] self.mappings has m ==> m.inv()
79        &&& forall|m: Mapping, n: Mapping|
80            #![trigger self.mappings.contains(m), self.mappings.contains(n)]
81            self.mappings has m ==> self.mappings has n ==> m != n ==> {
82                &&& m.va_range.end <= n.va_range.start || n.va_range.end <= m.va_range.start
83                &&& m.pa_range.end <= n.pa_range.start || n.pa_range.end <= m.pa_range.start
84            }
85    }
86}
87
88} // verus!
ostd/specs/mm/page_table/view.rs

ostd/specs/mm/page_table/
view.rs
