1use vstd::{atomic::PermissionU64, prelude::*, simple_pptr::PointsTo};
36use vstd_extra::{
37 once::OnceImpl, ownership::*, prelude::*, resource_invariant::TrivialResourceInvariant,
38};
39
40use crate::specs::{
41 arch::*,
42 mm::{
43 frame::{
44 mapping::group_page_meta,
45 meta_owners::{FracMetadataPerm, MetaSlotStorage},
46 meta_region_owners::MetaRegionOwners,
47 },
48 page_table::{nr_pte_index_bits_spec, pte_index_bit_offset_spec},
49 },
50};
51
52use core::{marker::PhantomData, ops::Range};
53
54pub(crate) mod kvirt_area;
56#[cfg(ktest)]
57mod test;
58
59use super::{
60 Paddr, PagingConstsTrait, Vaddr,
61 frame::{
62 Frame, Segment,
63 meta::{AnyFrameMeta, MetaPageMeta, MetaSlot, mapping},
64 },
65 page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags},
66 page_table::{PageTable, PageTableConfig},
67};
68use crate::mm::frame::DynFrame;
69use crate::mm::page_table::RCClone;
70use crate::{
71 arch::mm::{PageTableEntry, PagingConsts},
72 boot::memory_region::MemoryRegionType,
73 mm::{PagingLevel, largest_pages},
74 };
76
77verus! {
78
79pub const ADDR_WIDTH_SHIFT: isize = 48 - 48;
83
84#[cfg(not(target_arch = "loongarch64"))]
87pub const KERNEL_BASE_VADDR: Vaddr = 0xffff_8000_0000_0000 << ADDR_WIDTH_SHIFT;
88
89#[cfg(target_arch = "loongarch64")]
90pub const KERNEL_BASE_VADDR: Vaddr = 0x9000_0000_0000_0000 << ADDR_WIDTH_SHIFT;
91
92pub const KERNEL_END_VADDR: Vaddr = 0xffff_ffff_ffff_0000 << ADDR_WIDTH_SHIFT;
94
95#[cfg(target_arch = "x86_64")]
106const KERNEL_CODE_BASE_VADDR: usize = 0xffff_ffff_8000_0000 << ADDR_WIDTH_SHIFT;
107
108#[cfg(target_arch = "riscv64")]
109const KERNEL_CODE_BASE_VADDR: usize = 0xffff_ffff_0000_0000 << ADDR_WIDTH_SHIFT;
110
111#[cfg(target_arch = "loongarch64")]
112const KERNEL_CODE_BASE_VADDR: usize = 0x9000_0000_0000_0000 << ADDR_WIDTH_SHIFT;
113
114pub const FRAME_METADATA_CAP_VADDR: Vaddr = 0xffff_e100_0000_0000 << ADDR_WIDTH_SHIFT;
115
116pub const FRAME_METADATA_BASE_VADDR: Vaddr = 0xffff_e000_0000_0000 << ADDR_WIDTH_SHIFT;
117
118pub const FRAME_METADATA_RANGE: Range<Vaddr> = 0xffff_e000_0000_0000..0xffff_e100_0000_0000;
119
120pub const VMALLOC_BASE_VADDR: Vaddr = 0xffff_c000_0000_0000 << ADDR_WIDTH_SHIFT;
121
122pub const VMALLOC_VADDR_RANGE: Range<Vaddr> = VMALLOC_BASE_VADDR..FRAME_METADATA_BASE_VADDR;
123
124pub const LINEAR_MAPPING_BASE_VADDR: Vaddr = 0xffff_8000_0000_0000 << ADDR_WIDTH_SHIFT;
127
128pub const LINEAR_MAPPING_VADDR_RANGE: Range<Vaddr> = LINEAR_MAPPING_BASE_VADDR..VMALLOC_BASE_VADDR;
129
130#[verus_verify(dual_spec, open)]
140#[verus_spec(
141 requires
142 pa + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
143 returns
144 paddr_to_vaddr(pa),
145)]
146pub fn paddr_to_vaddr(pa: Paddr) -> usize {
147 pa + LINEAR_MAPPING_BASE_VADDR
149}
150
151#[allow(private_interfaces)]
156pub exec static KERNEL_PAGE_TABLE: OnceImpl<PageTable<KernelPtConfig>, TrivialResourceInvariant> =
157 OnceImpl::new(Ghost(TrivialResourceInvariant));
158
159#[verifier::allow(autoderive_clone_without_spec)]
160#[derive(Clone, Debug)]
161pub(crate) struct KernelPtConfig {}
162
163unsafe impl PageTableConfig for KernelPtConfig {
166 open spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize> {
167 256..512
168 }
169
170 open spec fn LEADING_BITS_spec() -> usize {
171 0xffff
172 }
173
174 proof fn lemma_page_table_config_constant_requirements() {
175 use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2};
176
177 use crate::mm::nr_subpage_per_huge;
178 Self::C::lemma_paging_consts_properties();
179 PageTableEntry::lemma_layout();
180 lemma2_to64();
181 lemma2_to64_rest();
182 vstd::layout::unsigned_int_max_values();
183 lemma_usize_pow2_ilog2(12);
184 lemma_usize_pow2_ilog2(9);
185 lemma_pow2_adds(9, 39);
186 lemma_pow2_adds(8, 39);
187
188 assert((256 * pow2(39) as int) / (pow2(47) as int) == 1);
189 lemma_pow2_adds(16, 48);
190 }
191
192 fn TOP_LEVEL_INDEX_RANGE() -> (r: Range<usize>) {
193 256..512
194 }
195
196 open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool {
197 false
198 }
199
200 fn TOP_LEVEL_CAN_UNMAP() -> (b: bool) {
201 false
202 }
203
204 open spec fn LOCKED_END_BOUND_spec() -> int {
207 FRAME_METADATA_BASE_VADDR as int
208 }
209
210 type E = PageTableEntry;
211
212 type C = PagingConsts;
213
214 type Item = MappedItem;
215
216 type Perm = (&'static vstd::simple_pptr::PointsTo<MetaSlot>, FracMetadataPerm);
217
218 open spec fn perm_well_formed_with_region(
219 pa: Paddr,
220 perm: Tracked<Option<Self::Perm>>,
221 regions: MetaRegionOwners,
222 ) -> bool {
223 perm@ is Some ==> {
224 let idx = crate::specs::mm::frame::mapping::frame_to_index(pa);
225 let frame_perm = perm@->0;
226 &&& frame_perm.0 == regions.slots[idx]
227 &&& frame_perm.1.frac() == 1
228 &&& frame_perm.1.id() == regions.slot_owners[idx].metadata_perm.id()
229 &&& MetaSlot::perms_related(*frame_perm.0, frame_perm.1.resource())
230 }
231 }
232
233 proof fn lemma_none_perm_well_formed(pa: Paddr, regions: MetaRegionOwners) {
234 }
235
236 open spec fn item_into_raw_spec(item: Self::Item) -> (
237 Paddr,
238 PagingLevel,
239 PageProperty,
240 Tracked<Option<Self::Perm>>,
241 ) {
242 match item {
243 MappedItem::Tracked(frame, prop) => (
244 crate::mm::frame::meta::mapping::meta_to_frame(frame.ptr.addr()),
245 1,
246 Self::encode_tracked_prop(prop),
247 Tracked(Some((frame.tracked_slot_perm@, frame.tracked_metadata_perm@->0))),
248 ),
249 MappedItem::Untracked(pa, level, prop) => (
250 pa,
251 level,
252 Self::decode_tracked_prop(prop),
253 Tracked(None),
254 ),
255 }
256 }
257
258 #[verifier::external_body]
259 fn item_into_raw(item: Self::Item) -> (res: (
260 Paddr,
261 PagingLevel,
262 PageProperty,
263 Tracked<Option<Self::Perm>>,
264 )) {
265 match item {
266 MappedItem::Tracked(frame, mut prop) => {
267 proof_decl! {
268 let tracked frame_permission: FracMetadataPerm;
269 }
270 debug_assert!(!prop.flags.contains(PageFlags::AVAIL1()));
271 prop.flags = prop.flags | PageFlags::AVAIL1();
272 proof_decl! {
273 let tracked slot_perm = *frame.tracked_slot_perm;
274 }
275 let level = frame.map_level();
276 let paddr = frame.into_raw();
277 proof_with!(=> Tracked(frame_permission));
278 (paddr, level, prop, Tracked(Some((slot_perm, frame_permission))))
279 },
280 MappedItem::Untracked(pa, level, mut prop) => {
281 debug_assert!(!prop.flags.contains(PageFlags::AVAIL1()));
282 prop.flags = prop.flags - PageFlags::AVAIL1();
283 (pa, level, prop, Tracked(None))
284 },
285 }
286 }
287
288 open spec fn item_from_raw_spec(
289 paddr: Paddr,
290 level: PagingLevel,
291 prop: PageProperty,
292 perm: Tracked<Option<Self::Perm>>,
293 ) -> Self::Item {
294 if prop.flags.contains(PageFlags::AVAIL1()) {
295 MappedItem::Tracked(
296 Frame::<MetaSlotStorage> {
297 ptr: vstd::simple_pptr::PPtr(mapping::frame_to_meta(paddr), PhantomData),
298 _marker: PhantomData,
299 #[cfg(verus_keep_ghost_body)]
300 tracked_slot_perm: Tracked((perm@->0).0),
301 #[cfg(verus_keep_ghost_body)]
302 tracked_metadata_perm: Tracked(Some((perm@->0).1)),
303 },
304 Self::decode_tracked_prop(prop),
305 )
306 } else {
307 MappedItem::Untracked(paddr, level, prop)
308 }
309 }
310
311 #[verifier::external_body]
312 unsafe fn item_from_raw(
313 paddr: Paddr,
314 level: PagingLevel,
315 prop: PageProperty,
316 Tracked(perm): Tracked<Option<Self::Perm>>,
317 ) -> Self::Item {
318 if prop.flags.contains(PageFlags::AVAIL1()) {
319 debug_assert_eq!(level, 1);
320 let mut item_prop = prop;
322 item_prop.flags = item_prop.flags - PageFlags::AVAIL1();
323 let tracked (slot_perm, frame_permission) = perm.tracked_unwrap();
325 proof_with!(Tracked(slot_perm), Tracked(frame_permission));
326 let frame = unsafe { Frame::<MetaSlotStorage>::from_raw(paddr) };
327 MappedItem::Tracked(frame, item_prop)
328 } else {
329 MappedItem::Untracked(paddr, level, prop)
330 }
331 }
332
333 proof fn lemma_item_into_raw_roundtrip(
334 pa: Paddr,
335 level: PagingLevel,
336 prop: PageProperty,
337 perm: Tracked<Option<Self::Perm>>,
338 ) {
339 broadcast use group_page_meta;
340
341 assert(Self::raw_item_well_formed((pa, level, prop, perm)));
342 prop.lemma_avail1_tag_encoding();
343 if prop.flags.contains(PageFlags::AVAIL1()) {
344 assert(Self::item_from_raw(pa, level, prop, perm) is Tracked);
345 assert(perm@ is Some);
346 } else {
347 assert(Self::item_from_raw(pa, level, prop, perm) is Untracked);
348 assert(perm@ is None);
349 }
350 }
351
352 proof fn lemma_item_from_raw_roundtrip(
353 item: Self::Item,
354 paddr: Paddr,
355 level: PagingLevel,
356 prop: PageProperty,
357 perm: Tracked<Option<Self::Perm>>,
358 ) {
359 broadcast use group_page_meta;
360
361 match item {
362 MappedItem::Tracked(frame, prop_actual) => {
363 assert(Self::item_well_formed(item));
364 prop_actual.lemma_avail1_tag_encoding();
365 },
366 MappedItem::Untracked(_, _, prop_actual) => {
367 assert(Self::item_well_formed(item));
368 prop_actual.lemma_avail1_tag_encoding();
369 },
370 }
371 }
372
373 open spec fn item_well_formed(item: Self::Item) -> bool {
374 match item {
375 MappedItem::Tracked(frame, prop) => {
376 &&& !prop.flags.contains(PageFlags::AVAIL1())
377 &&& frame.inv()
378 },
379 MappedItem::Untracked(_, _, prop) => !prop.flags.contains(PageFlags::AVAIL1()),
380 }
381 }
382
383 open spec fn raw_item_well_formed(
384 item: (Paddr, PagingLevel, PageProperty, Tracked<Option<Self::Perm>>),
385 ) -> bool {
386 let (pa, level, prop, perm) = item;
387 &&& (prop.flags.contains(PageFlags::AVAIL1()) <==> perm@ is Some)
388 &&& prop.flags.contains(PageFlags::AVAIL1()) ==> {
389 &&& level == 1
390 &&& (perm@->0).0.addr() == mapping::frame_to_meta(pa)
391 &&& (perm@->0).0.is_init()
392 &&& (perm@->0).1.frac() == 1
393 &&& MetaSlot::perms_related(*(perm@->0).0, (perm@->0).1.resource())
394 }
395 }
396
397 proof fn lemma_perm_well_formed_with_region_preserved(
398 pa: Paddr,
399 perm: Tracked<Option<Self::Perm>>,
400 old_regions: MetaRegionOwners,
401 new_regions: MetaRegionOwners,
402 ) {
403 }
404
405 proof fn lemma_raw_item_well_formed_preserved(
406 pa: Paddr,
407 level: PagingLevel,
408 old_prop: PageProperty,
409 new_prop: PageProperty,
410 perm: Tracked<Option<Self::Perm>>,
411 ) {
412 }
413
414 proof fn lemma_raw_item_well_formed_split(
415 pa: Paddr,
416 level: PagingLevel,
417 prop: PageProperty,
418 child_pa: Paddr,
419 child_idx: usize,
420 perm: Tracked<Option<Self::Perm>>,
421 ) {
422 assert(<PageTableEntry as crate::mm::page_table::PageTableEntryTrait>::new_page_req(
423 pa,
424 level,
425 prop,
426 ));
427 assert(<PageTableEntry as crate::mm::page_table::PageTableEntryTrait>::new_page_req(
428 child_pa,
429 (level - 1) as PagingLevel,
430 prop,
431 ));
432 }
433
434 proof fn lemma_huge_raw_item_untracked(
435 pa: Paddr,
436 level: PagingLevel,
437 prop: PageProperty,
438 perm: Tracked<Option<Self::Perm>>,
439 ) {
440 }
441
442 proof fn lemma_item_from_raw_well_formed(
443 pa: Paddr,
444 level: PagingLevel,
445 prop: PageProperty,
446 perm: Tracked<Option<Self::Perm>>,
447 ) {
448 broadcast use group_page_meta;
449
450 prop.lemma_avail1_tag_encoding();
451 }
452
453 proof fn lemma_clone_ensures_concrete(
454 item: Self::Item,
455 pa: Paddr,
456 old_regions: MetaRegionOwners,
457 new_regions: MetaRegionOwners,
458 res: Self::Item,
459 ) {
460 use crate::specs::mm::frame::mapping::{frame_to_index, meta_to_index};
461
462 match item {
463 MappedItem::Tracked(frame, _) => {
464 let frame_idx = meta_to_index(frame.ptr.addr());
465 assert(frame.index() == frame_to_index(pa));
466 assert(<MappedItem as RCClone>::clone_ensures(item, old_regions, new_regions, res));
467 },
468 MappedItem::Untracked(_, _, _) => {},
469 }
470 }
471
472 proof fn lemma_clone_requires_concrete(
473 item: Self::Item,
474 pa: Paddr,
475 level: PagingLevel,
476 prop: PageProperty,
477 regions: MetaRegionOwners,
478 ) {
479 use crate::specs::mm::frame::mapping::frame_to_index;
480
481 use crate::mm::frame::meta::mapping::{frame_to_meta, meta_to_frame};
482 use crate::mm::frame::meta::{REF_COUNT_MAX, REF_COUNT_UNUSED};
483 broadcast use group_page_meta;
484
485 let perm = Self::item_into_raw(item).3;
486 Self::lemma_item_from_raw_well_formed(pa, level, prop, perm);
487 match item {
488 MappedItem::Tracked(frame, _) => {
489 crate::specs::mm::frame::mapping::lemma_paddr_to_meta_biinjective(pa);
490 regions.lemma_contains_valid_frame_paddr(pa);
491 },
492 MappedItem::Untracked(_, _, _) => {},
493 }
494 }
495}
496
497impl KernelPtConfig {
498 pub open spec fn encode_tracked_prop(prop: PageProperty) -> PageProperty {
500 PageProperty { flags: prop.flags.union(PageFlags::AVAIL1()), ..prop }
501 }
502
503 pub open spec fn decode_tracked_prop(prop: PageProperty) -> PageProperty {
505 PageProperty { flags: prop.flags.difference(PageFlags::AVAIL1()), ..prop }
506 }
507}
508
509pub enum MappedItem {
518 Tracked(DynFrame, PageProperty),
519 Untracked(Paddr, PagingLevel, PageProperty),
520}
521
522impl RCClone for MappedItem {
523 open spec fn clone_requires(self, perm: MetaRegionOwners) -> bool {
524 match self {
525 MappedItem::Tracked(frame, _) => frame.clone_requires(perm),
526 MappedItem::Untracked(_, _, _) => perm.inv(),
527 }
528 }
529
530 open spec fn clone_ensures(
531 self,
532 old_perm: MetaRegionOwners,
533 new_perm: MetaRegionOwners,
534 res: Self,
535 ) -> bool {
536 match (self, res) {
537 (MappedItem::Tracked(frame, prop), MappedItem::Tracked(res_frame, res_prop)) => {
538 &&& prop == res_prop
539 &&& frame.clone_ensures(old_perm, new_perm, res_frame)
540 },
541 (
542 MappedItem::Untracked(pa, level, prop),
543 MappedItem::Untracked(res_pa, res_level, res_prop),
544 ) => {
545 &&& pa == res_pa
546 &&& level == res_level
547 &&& prop == res_prop
548 &&& old_perm == new_perm
549 },
550 _ => false,
551 }
552 }
553
554 #[verifier::external_body]
555 fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> (res: Self) {
556 unimplemented!();
557 }
558}
559
560}