ostd/specs/mm/page_table/cursor/
cursor_fn_specs.rs

1use vstd::prelude::*;
2
3use crate::mm::page_table::*;
4use crate::mm::{PagingConstsTrait, Vaddr};
5use crate::specs::arch::mm::{NR_LEVELS, PAGE_SIZE};
6use crate::specs::mm::frame::mapping::frame_to_index;
7use crate::specs::mm::frame::meta_owners::{REF_COUNT_MAX, REF_COUNT_UNUSED};
8use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
9use crate::specs::mm::page_table::cursor::owners::*;
10use crate::specs::mm::page_table::*;
11use crate::specs::task::InAtomicMode;
12
13use core::ops::Range;
14
15verus! {
16
17// ─── Cursor specs ─────────────────────────────────────────────────────────────
18
19impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
20    pub open spec fn cursor_new_success_conditions(va: &Range<Vaddr>) -> bool {
21        &&& va.start < va.end
22        &&& va.start % C::BASE_PAGE_SIZE() == 0
23        &&& va.end % C::BASE_PAGE_SIZE() == 0
24        &&& crate::mm::page_table::is_valid_range_spec::<C>(va)
25    }
26
27    pub open spec fn invariants(
28        self,
29        owner: CursorOwner<'rcu, C>,
30        regions: MetaRegionOwners,
31        guards: Guards<'rcu, C>,
32    ) -> bool {
33        &&& owner.inv()
34        &&& self.inv()
35        &&& self.wf(owner)
36        &&& regions.inv()
37        &&& owner.children_not_locked(guards)
38        &&& owner.nodes_locked(guards)
39        &&& owner.metaregion_sound(regions)
40        &&& !owner.popped_too_high
41    }
42
43    pub open spec fn query_some_condition(self, owner: CursorOwner<'rcu, C>) -> bool {
44        self.model(owner).present()
45    }
46
47    pub open spec fn query_some_ensures(
48        self,
49        owner: CursorOwner<'rcu, C>,
50        res: PagesState<C>,
51    ) -> bool {
52        &&& owner.cur_va_range().start.reflect(res.0.start)
53        &&& owner.cur_va_range().end.reflect(res.0.end)
54        &&& res.1 is Some
55        &&& {
56            let qr = owner@.query_range();
57            owner@.query_item_spec(res.1.unwrap()) == Some(qr.start as Vaddr..qr.end as Vaddr)
58        }
59    }
60
61    pub open spec fn query_none_ensures(
62        self,
63        owner: CursorOwner<'rcu, C>,
64        res: PagesState<C>,
65    ) -> bool {
66        &&& res.1 is None
67    }
68
69    pub open spec fn jump_panic_condition(self, va: Vaddr) -> bool {
70        va % PAGE_SIZE != 0
71    }
72
73    pub open spec fn find_next_panic_condition(self, len: usize) -> bool {
74        ||| len % PAGE_SIZE != 0
75        ||| self.va + len > self.barrier_va.end
76    }
77}
78
79// ─── CursorMut specs ──────────────────────────────────────────────────────────
80
81impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
82    // TODO: trace the `level >= guard_level` panic to its actual location in `pop_level`
83    // (unwrap of None path entry). Doing so requires tweaking the cursor invariant's
84    // treatment of locks so that `pop_level` can express the panic as a precondition violation.
85    pub open spec fn map_panic_conditions(self, item: C::Item) -> bool {
86        ||| self.inner.va >= self.inner.barrier_va.end
87        ||| C::item_into_raw(item).1 > C::HIGHEST_TRANSLATION_LEVEL()
88        ||| C::item_into_raw(item).1 >= self.inner.guard_level
89        ||| (!C::TOP_LEVEL_CAN_UNMAP_spec() && C::item_into_raw(item).1 >= NR_LEVELS)
90        ||| self.inner.va % page_size(C::item_into_raw(item).1) != 0
91        ||| self.inner.va + page_size(C::item_into_raw(item).1) > self.inner.barrier_va.end
92    }
93
94    // TODO: ideally this should be an `OwnerOf` impl for `C::Item`
95    pub open spec fn item_wf(self, item: C::Item, entry_owner: EntryOwner<C>) -> bool {
96        let (paddr, level, prop) = C::item_into_raw(item);
97        &&& entry_owner.inv()
98        &&& (entry_owner.is_absent() || Child::Frame(paddr, level, prop).wf(entry_owner))
99    }
100
101    pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
102        let (pa, level, prop) = C::item_into_raw(item);
103        let size = page_size(level);
104        let range = pa..(pa + size) as usize;
105        regions.paddr_range_not_mapped(range)
106    }
107
108    pub open spec fn item_slot_in_regions(item: C::Item, regions: MetaRegionOwners) -> bool {
109        let (pa, level, prop) = C::item_into_raw(item);
110        let idx = frame_to_index(pa);
111        &&& regions.slots.contains_key(idx)
112        &&& regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
113        &&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
114        // Allocator invariant for huge frames (level > 1): all 4KB sub-page slots are valid.
115        // Established by huge-frame allocator postcondition.
116        &&& level > 1 ==> {
117            forall |j: usize| #![trigger frame_to_index((pa + j * PAGE_SIZE) as usize)]
118                0 < j < page_size(level) / PAGE_SIZE ==> {
119                let sub_idx = frame_to_index((pa + j * PAGE_SIZE) as usize);
120                &&& regions.slots.contains_key(sub_idx)
121                &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
122                &&& regions.slot_owners[sub_idx].inner_perms.ref_count.value() > 0
123            }
124        }
125    }
126
127    pub open spec fn map_item_ensures(
128        self,
129        item: C::Item,
130        old_view: CursorView<C>,
131        new_view: CursorView<C>,
132    ) -> bool {
133        let (pa, level, prop) = C::item_into_raw(item);
134        new_view == old_view.map_spec(pa, page_size(level), prop)
135    }
136}
137
138} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs

ostd/specs/mm/page_table/cursor/
cursor_fn_specs.rs
