ostd/mm/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Virtual memory (VM).
3use crate::specs::arch::PAGE_SIZE;
4use core::fmt::Debug;
5use vstd::arithmetic::div_mod::group_div_basics;
6use vstd::arithmetic::div_mod::lemma_div_non_zero;
7use vstd::arithmetic::power2::*;
8use vstd::prelude::*;
9
10/// Virtual addresses.
11pub type Vaddr = usize;
12
13/// Physical addresses.
14pub type Paddr = usize;
15
16/// The maximum value of `PagingConstsTrait::NR_LEVELS`.
17pub const MAX_NR_LEVELS: usize = 4;
18
19pub(crate) mod dma;
20pub mod frame;
21//pub mod heap;
22pub mod io;
23pub use io::{
24    Fallible, FallibleVmRead, FallibleVmWrite, Infallible, VmIo, VmIoOnce, VmReader, VmWriter,
25};
26pub mod kspace;
27pub(crate) mod page_prop;
28pub mod page_table;
29pub mod tlb;
30pub mod vm_space;
31
32#[cfg(ktest)]
33mod test;
34
35use core::ops::Range;
36
37// Import types and constants from arch
38pub use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, NR_ENTRIES, NR_LEVELS};
39
40#[doc(hidden)]
41pub use crate::specs::arch::paging_consts::PagingConsts;
42
43// Re-export paddr_to_vaddr from kspace
44#[doc(hidden)]
45pub use kspace::paddr_to_vaddr;
46
47// Re-export largest_pages from page_table
48#[doc(hidden)]
49pub use page_table::largest_pages;
50
51/// The level of a page table node or a frame.
52pub type PagingLevel = u8;
53
54verus! {
55
56/// The maximum virtual address of user space (non inclusive).
57///
58/// Typical 64-bit systems have at least 48-bit virtual address space.
59/// A typical way to reserve half of the address space for the kernel is
60/// to use the highest 48-bit virtual address space.
61///
62/// Also, the top page is not regarded as usable since it's a workaround
63/// for some x86_64 CPUs' bugs. See
64/// <https://github.com/torvalds/linux/blob/480e035fc4c714fb5536e64ab9db04fedc89e910/arch/x86/include/asm/page_64.h#L68-L78>
65/// for the rationale.
66/// Page size.
67pub const MAX_USERSPACE_VADDR: usize = 0x0000_8000_0000_0000 - PAGE_SIZE;
68
69/// The kernel address space.
70///
71/// There are the high canonical addresses defined in most 48-bit width
72/// architectures.
73pub const KERNEL_VADDR_RANGE: Range<Vaddr> = 0xffff_8000_0000_0000..0xffff_ffff_ffff_0000;
74
75pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static {
76    spec fn BASE_PAGE_SIZE_spec() -> usize;
77
78    proof fn lemma_BASE_PAGE_SIZE_properties()
79        ensures
80            0 < Self::BASE_PAGE_SIZE_spec(),
81            is_pow2(Self::BASE_PAGE_SIZE_spec() as int),
82    ;
83
84    /// The smallest page size.
85    /// This is also the page size at level 1 page tables.
86    #[verifier::when_used_as_spec(BASE_PAGE_SIZE_spec)]
87    fn BASE_PAGE_SIZE() -> (res: usize)
88        ensures
89            res == Self::BASE_PAGE_SIZE_spec(),
90            0 < res,
91            is_pow2(res as int),
92    ;
93
94    spec fn NR_LEVELS_spec() -> PagingLevel;
95
96    /// The number of levels in the page table.
97    /// The numbering of levels goes from deepest node to the root node. For example,
98    /// the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables,
99    /// Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5
100    /// Table, respectively.
101    #[verifier::when_used_as_spec(NR_LEVELS_spec)]
102    fn NR_LEVELS() -> (res: PagingLevel)
103        ensures
104            res == Self::NR_LEVELS_spec(),
105            res > 0,
106    ;
107
108    /// All configs in vostd use the same value for the per-config
109    /// `NR_LEVELS_spec()` as the architecture-level constant `NR_LEVELS`
110    /// (= 4 for x86_64). This is *implicit* in the cursor framework:
111    /// `CursorOwner::inv()` hardcodes `self.level <= NR_LEVELS` (const)
112    /// for cursors over any `C: PagingConstsTrait`, so a config whose
113    /// `NR_LEVELS_spec()` exceeded `NR_LEVELS` would be unusable. This
114    /// lemma exposes that equality as a usable fact so generic proofs
115    /// can chain `level != C::NR_LEVELS_spec()` to `level < NR_LEVELS`
116    /// (e.g. `Cursor::find_next_impl`'s PageTable-branch gate ⟹
117    /// `CursorMut::take_next`'s `replace_cur_entry` discharge).
118    proof fn lemma_NR_LEVELS_eq()
119        ensures
120            Self::NR_LEVELS_spec() as int == NR_LEVELS as int,
121    ;
122
123    spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel;
124
125    /// The highest level that a PTE can be directly used to translate a VA.
126    /// This affects the the largest page size supported by the page table.
127    #[verifier::when_used_as_spec(HIGHEST_TRANSLATION_LEVEL_spec)]
128    fn HIGHEST_TRANSLATION_LEVEL() -> (res: PagingLevel)
129        ensures
130            res == Self::HIGHEST_TRANSLATION_LEVEL_spec(),
131    ;
132
133    spec fn PTE_SIZE_spec() -> usize;
134
135    /// The size of a PTE.
136    #[verifier::when_used_as_spec(PTE_SIZE_spec)]
137    fn PTE_SIZE() -> (res: usize)
138        ensures
139            res == Self::PTE_SIZE_spec(),
140            is_pow2(res as int),
141            0 < res <= Self::BASE_PAGE_SIZE(),
142    ;
143
144    proof fn lemma_PTE_SIZE_properties()
145        ensures
146            0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE(),
147            is_pow2(Self::PTE_SIZE_spec() as int),
148    ;
149
150    spec fn ADDRESS_WIDTH_spec() -> usize;
151
152    /// The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS.
153    /// If it is shorter than that, the higher bits in the highest level are ignored.
154    #[verifier::when_used_as_spec(ADDRESS_WIDTH_spec)]
155    fn ADDRESS_WIDTH() -> (res: usize)
156        ensures
157            res == Self::ADDRESS_WIDTH_spec(),
158    ;
159
160    /// Whether virtual addresses are sign-extended.
161    ///
162    /// The sign bit of a [`Vaddr`] is the bit at index [`PagingConstsTrait::ADDRESS_WIDTH`] - 1.
163    /// If this constant is `true`, bits in [`Vaddr`] that are higher than the sign bit must be
164    /// equal to the sign bit. If an address violates this rule, both the hardware and OSTD
165    /// should reject it.
166    ///
167    /// Otherwise, if this constant is `false`, higher bits must be zero.
168    ///
169    /// Regardless of sign extension, [`Vaddr`] is always not signed upon calculation.
170    /// That means, `0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001` is `true`.
171    spec fn VA_SIGN_EXT_spec() -> bool;
172
173    #[verifier::when_used_as_spec(VA_SIGN_EXT_spec)]
174    fn VA_SIGN_EXT() -> (res: bool)
175        ensures
176            res == Self::VA_SIGN_EXT_spec(),
177    ;
178}
179
180#[verifier::inline]
181pub open spec fn nr_subpage_per_huge_spec<C: PagingConstsTrait>() -> usize {
182    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
183}
184
185/// The number of sub pages in a huge page.
186#[inline(always)]
187#[verifier::when_used_as_spec(nr_subpage_per_huge_spec)]
188pub fn nr_subpage_per_huge<C: PagingConstsTrait>() -> (res: usize)
189    ensures
190        res == nr_subpage_per_huge_spec::<C>(),
191{
192    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
193}
194
195pub proof fn lemma_nr_subpage_per_huge_bounded<C: PagingConstsTrait>()
196    ensures
197        0 < nr_subpage_per_huge::<C>() <= C::BASE_PAGE_SIZE(),
198{
199    C::lemma_PTE_SIZE_properties();
200    broadcast use group_div_basics;
201
202    assert(C::PTE_SIZE() <= C::BASE_PAGE_SIZE());
203    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() <= C::BASE_PAGE_SIZE());
204    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() > 0) by {
205        lemma_div_non_zero(C::BASE_PAGE_SIZE() as int, C::PTE_SIZE() as int);
206    };
207}
208
209/// Gets physical address trait
210pub trait HasPaddr {
211    /// Returns the physical address.
212    fn paddr(&self) -> Paddr;
213}
214
215/// Checks if the given address is page-aligned.
216pub const fn is_page_aligned(p: usize) -> bool {
217    (p & (PAGE_SIZE - 1)) == 0
218}
219
220} // verus!
ostd/mm/mod.rs

ostd/mm/
mod.rs
