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_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.relate_region(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        &&& owner@.query_item_spec(res.1.unwrap()) == Some(owner@.query_range())
56    }
57
58    pub open spec fn query_none_ensures(
59        self,
60        owner: CursorOwner<'rcu, C>,
61        res: PagesState<C>,
62    ) -> bool {
63        &&& res.1 is None
64    }
65
66    pub open spec fn jump_panic_condition(self, va: Vaddr) -> bool {
67        va % PAGE_SIZE != 0
68    }
69
70    pub open spec fn find_next_panic_condition(self, len: usize) -> bool {
71        ||| len % PAGE_SIZE != 0
72        ||| self.va + len > self.barrier_va.end
73    }
74}
75
76// ─── CursorMut specs ──────────────────────────────────────────────────────────
77
78impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
79    pub open spec fn map_panic_conditions(self, item: C::Item) -> bool {
80        ||| self.inner.va >= self.inner.barrier_va.end
81        ||| C::item_into_raw(item).1 > C::HIGHEST_TRANSLATION_LEVEL()
82        ||| (!C::TOP_LEVEL_CAN_UNMAP_spec() && C::item_into_raw(item).1 >= NR_LEVELS)
83        ||| self.inner.va % page_size(C::item_into_raw(item).1) != 0
84        ||| self.inner.va + page_size(C::item_into_raw(item).1) > self.inner.barrier_va.end
85    }
86
87    pub open spec fn map_cursor_requires(
88        self,
89        owner: CursorOwner<'rcu, C>,
90        guards: Guards<'rcu, C>,
91    ) -> bool {
92        &&& owner.in_locked_range()
93        &&& self.inner.level < self.inner.guard_level
94        &&& self.inner.va < self.inner.barrier_va.end
95    }
96
97    pub open spec fn map_item_requires(self, item: C::Item, entry_owner: EntryOwner<C>) -> bool {
98        let (paddr, level, prop) = C::item_into_raw(item);
99        &&& entry_owner.inv()
100        &&& self.inner.va % page_size(level) == 0
101        &&& self.inner.va + page_size(level) <= self.inner.barrier_va.end
102        &&& level < self.inner.guard_level
103        &&& (entry_owner.is_absent()
104            || Child::Frame(paddr, level, prop).wf(entry_owner))
105    }
106
107    pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
108        let (pa, level, prop) = C::item_into_raw(item);
109        let size = page_size(level);
110        let range = pa..(pa + size) as usize;
111        regions.paddr_range_not_mapped(range)
112    }
113
114    pub open spec fn item_slot_in_regions(item: C::Item, regions: MetaRegionOwners) -> bool {
115        let (pa, level, prop) = C::item_into_raw(item);
116        let idx = frame_to_index(pa);
117        &&& regions.slots.contains_key(idx)
118        &&& regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
119    }
120
121    pub open spec fn map_item_ensures(
122        self,
123        item: C::Item,
124        old_view: CursorView<C>,
125        new_view: CursorView<C>,
126    ) -> bool {
127        let (pa, level, prop) = C::item_into_raw(item);
128        new_view == old_view.map_spec(pa, page_size(level), prop)
129    }
130}
131
132} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs

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