ostd/specs/mm/page_table/
view.rs

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

ostd/specs/mm/page_table/
view.rs
