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

1use vstd::prelude::*;
2
3use crate::specs::{
4    arch::PAGE_SIZE,
5    mm::{
6        frame::{mapping::frame_to_index, meta_region_owners::MetaRegionOwners},
7        page_table::{
8            cursor::owners::*, is_valid_range_spec,
9            vaddr_range_proofs::lemma_page_table_managed_index_bounds, *,
10        },
11    },
12    task::InAtomicMode,
13};
14
15use crate::arch::mm::PagingConsts;
16use crate::mm::{
17    PagingConstsTrait, PagingLevel, Vaddr,
18    frame::meta::{REF_COUNT_MAX, REF_COUNT_UNUSED},
19    page_table::*,
20};
21use core::ops::Range;
22
23verus! {
24
25impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
26    /// Request addresses lie inside the locked node and satisfy configuration bounds.
27    pub proof fn lemma_barrier_va_bounds(self, va: Vaddr)
28        requires
29            self.inv(),
30            self.barrier_va.start <= va < self.barrier_va.end,
31            va % C::BASE_PAGE_SIZE() == 0,
32        ensures
33            self.locked_range().start <= va < self.locked_range().end,
34            vaddr_leading_part_spec::<C>(va) == page_table_coverage_start_spec::<C>(),
35            C::TOP_LEVEL_INDEX_RANGE().start <= pte_index_spec::<C>(va, C::NR_LEVELS())
36                < C::TOP_LEVEL_INDEX_RANGE().end,
37    {
38        C::lemma_paging_consts_properties();
39        C::axiom_current_paging_consts_hardcoded();
40        C::lemma_page_table_config_constant_properties();
41        self.lemma_locked_range_span();
42        lemma_same_node_vaddr_leading_part_match::<C>(
43            va,
44            self.prefix,
45            self.prefix,
46            self.guard_level,
47        );
48        lemma_page_table_managed_index_bounds::<C>(va);
49    }
50}
51
52// ─── Cursor specs ─────────────────────────────────────────────────────────────
53impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
54    /// Checks the range validity, ordering, and alignment enforced by the executable constructor.
55    pub open spec fn cursor_new_input_valid(va: Range<Vaddr>) -> bool {
56        &&& va.start < va.end
57        &&& va.start % C::BASE_PAGE_SIZE() == 0
58        &&& va.end % C::BASE_PAGE_SIZE() == 0
59        &&& is_valid_range_spec::<C>(va)
60    }
61
62    /// Conditions for verified construction, including representable slot successors.
63    pub open spec fn cursor_new_success_conditions(va: Range<Vaddr>) -> bool {
64        let top = C::NR_LEVELS();
65        let end = page_table_coverage_end_spec::<C>();
66        // A request wholly in the last root slot must descend when root leaves are unsupported.
67        let reserve_level = if top > 1 && C::HIGHEST_TRANSLATION_LEVEL() < top && end - page_size::<
68            C,
69        >(top) <= va.start {
70            (top - 1) as PagingLevel
71        } else {
72            top
73        };
74        &&& Self::cursor_new_input_valid(va)
75        &&& va.end + page_size::<C>(reserve_level) <= end
76    }
77
78    pub open spec fn invariants(
79        self,
80        owner: CursorOwner<'rcu, C>,
81        regions: MetaRegionOwners,
82        guards: Guards,
83    ) -> bool {
84        &&& self.va <= self.barrier_va.end
85        &&& owner.inv()
86        &&& self.inv()
87        &&& self.wf(owner)
88        &&& regions.inv()
89        &&& owner.children_not_locked(guards)
90        &&& owner.nodes_locked(guards)
91        &&& owner.metaregion_sound(regions)
92        &&& !owner.popped_too_high
93    }
94
95    pub open spec fn query_some_condition(self, owner: CursorOwner<'rcu, C>) -> bool {
96        owner@.present()
97    }
98
99    /// Panic condition for [`Self::query`]. `query` diverges *only* via the
100    /// Arc-style refcount-saturation abort when it clones the **specific**
101    /// frame the cursor resolves to. That happens iff:
102    ///  - the cursor is in range,
103    ///  - the resolved leaf owner carries a permission, so cloning
104    ///    it bumps its slot's refcount (raw RAM/MMIO mappings never bump),
105    ///  - that slot's refcount is already at `REF_COUNT_MAX`, so the
106    ///    `inc_ref_count` in `clone_item` would overflow and abort.
107    pub open spec fn query_panic_condition(
108        self,
109        owner: CursorOwner<'rcu, C>,
110        regions: MetaRegionOwners,
111    ) -> bool {
112        &&& self.barrier_va.start <= self.va < self.barrier_va.end
113        &&& PageTableOwner(owner.cur_subtree()).query_leaf(self.va) matches Some(entry) && {
114            &&& entry.is_frame()
115            &&& entry.frame_is_tracked()
116            &&& regions.ref_count(frame_to_index(entry.frame().mapped_pa)) >= REF_COUNT_MAX
117        }
118    }
119
120    pub open spec fn query_some_ensures(
121        self,
122        owner: CursorOwner<'rcu, C>,
123        res: PagesState<C>,
124    ) -> bool {
125        &&& owner.cur_va_range() == res.0
126        &&& res.1 is Some
127        &&& {
128            let qr = owner@.query_range();
129            owner@.query_item_spec(res.1->0) == Some(qr.start as Vaddr..qr.end as Vaddr)
130        }
131    }
132
133    pub open spec fn query_none_ensures(
134        self,
135        owner: CursorOwner<'rcu, C>,
136        res: PagesState<C>,
137    ) -> bool {
138        &&& res.1 is None
139    }
140
141    /// Whether the level-`lv` node around the cursor's own VA contains `va`
142    /// — exactly the per-iteration test in `jump`'s loop
143    /// (`node_start <= va && va - node_start < node_size`, with
144    /// `node_start == nat_align_down(self.va, page_size(lv + 1))` and
145    /// `node_size == page_size(lv + 1)`).
146    pub open spec fn jump_node_holds(self, lv: PagingLevel, va: Vaddr) -> bool {
147        let nstart = nat_align_down(
148            self.va as nat,
149            page_size::<PagingConsts>((lv + 1) as PagingLevel) as nat,
150        );
151        &&& nstart <= va as nat
152        &&& (va as nat) - nstart < page_size::<PagingConsts>((lv + 1) as PagingLevel) as nat
153    }
154
155    /// Structural (reachability) panic condition for `jump`: it diverges on a
156    /// misaligned `va` (the `assert_eq!`), or when `va` is in the barrier
157    /// range but **no** node on the ascending path within the guard levels
158    /// `[level, guard_level]` contains it — exactly the case where the loop
159    /// never finds `va`, pops above the guard, and hits `pop_level`'s
160    /// `None`-slot unwrap. (An out-of-range `va` returns `Err`, no panic.)
161    /// This mirrors the loop's own search, so it neither over- nor
162    /// under-approximates: an out-of-locked-range cursor that *can* still
163    /// reach `va` via a shared ancestor node does **not** satisfy it.
164    pub open spec fn jump_panic_condition(self, va: Vaddr) -> bool {
165        ||| va % PAGE_SIZE != 0
166        ||| (self.barrier_va.start <= va < self.barrier_va.end && forall|lv: PagingLevel|
167            #![trigger self.jump_node_holds(lv, va)]
168            self.level <= lv <= self.guard_level ==> !self.jump_node_holds(lv, va))
169    }
170
171    pub open spec fn find_next_panic_condition(self, len: usize) -> bool {
172        ||| len % PAGE_SIZE != 0
173        ||| self.va + len > self.barrier_va.end
174    }
175}
176
177// ─── CursorMut specs ──────────────────────────────────────────────────────────
178impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
179    /// Runtime checks for mapping an item, matching the source's range and alignment checks.
180    pub open spec fn map_panic_conditions(self, item: C::Item) -> bool {
181        ||| self.0.va >= self.0.barrier_va.end
182        ||| C::item_into_raw(item).1 > C::HIGHEST_TRANSLATION_LEVEL()
183        ||| C::item_into_raw(item).1 > self.0.guard_level
184        ||| self.0.va % page_size::<PagingConsts>(C::item_into_raw(item).1) != 0
185        ||| self.0.va + page_size::<PagingConsts>(C::item_into_raw(item).1) > self.0.barrier_va.end
186    }
187
188    // TODO: ideally this should be an `OwnerOf` impl for `C::Item`
189    pub open spec fn item_wf(self, item: C::Item, entry_owner: EntryOwner<C>) -> bool {
190        let (paddr, level, prop, _perm) = C::item_into_raw(item);
191        &&& C::item_well_formed(
192            item,
193        )
194        // Mapping may descend within the locked subtree, but cannot replace its parent PTE.
195        &&& level <= self.0.guard_level
196        &&& entry_owner.inv()
197        &&& (entry_owner.is_absent() || Child::Frame(paddr, level, prop).wf(entry_owner))
198    }
199
200    pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
201        let (pa, level, prop, perm) = C::item_into_raw(item);
202        let size = page_size::<PagingConsts>(level);
203        let range = pa..(pa + size) as usize;
204        perm@ is Some ==> regions.paddr_range_not_mapped(range)
205    }
206
207    pub open spec fn item_slot_in_regions_except_perm(
208        item: C::Item,
209        regions: MetaRegionOwners,
210    ) -> bool {
211        let (pa, _level, _prop, perm) = C::item_into_raw(item);
212        let idx = frame_to_index(pa);
213        &&& regions.contains(idx)
214        &&& perm@ is Some ==> {
215            &&& regions.slot_owners[idx].usage !is PageTable
216            &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
217        }
218    }
219
220    pub closed spec fn item_slot_in_regions(item: C::Item, regions: MetaRegionOwners) -> bool {
221        let (pa, _level, _prop, perm) = C::item_into_raw(item);
222        &&& Self::item_slot_in_regions_except_perm(item, regions)
223        &&& C::perm_well_formed_with_region(pa, perm, regions)
224    }
225
226    pub proof fn lemma_item_slot_in_regions_facts(item: C::Item, regions: MetaRegionOwners)
227        ensures
228            Self::item_slot_in_regions(item, regions) <==> {
229                &&& Self::item_slot_in_regions_except_perm(item, regions)
230                &&& C::perm_well_formed_with_region(
231                    C::item_into_raw(item).0,
232                    C::item_into_raw(item).3,
233                    regions,
234                )
235            },
236    {
237    }
238
239    pub proof fn lemma_item_slot_in_regions_preserved(
240        item: C::Item,
241        regions0: MetaRegionOwners,
242        regions1: MetaRegionOwners,
243    )
244        requires
245            Self::item_slot_in_regions(item, regions0),
246            Self::item_slot_in_regions_except_perm(item, regions1),
247            C::item_into_raw(item).3@ is Some ==> {
248                let idx = frame_to_index(C::item_into_raw(item).0);
249                &&& regions0.slots[idx] == regions1.slots[idx]
250                &&& regions0.slot_owners[idx].metadata_perm.id()
251                    == regions1.slot_owners[idx].metadata_perm.id()
252            },
253        ensures
254            Self::item_slot_in_regions(item, regions1),
255    {
256        if C::item_into_raw(item).3@ is Some {
257            C::lemma_perm_well_formed_with_region_preserved(
258                C::item_into_raw(item).0,
259                C::item_into_raw(item).3,
260                regions0,
261                regions1,
262            );
263        } else {
264            C::lemma_none_perm_well_formed(C::item_into_raw(item).0, regions1);
265        }
266    }
267
268    pub proof fn lemma_all_item_slots_preserved(
269        regions0: MetaRegionOwners,
270        regions1: MetaRegionOwners,
271    )
272        requires
273            forall|idx: int| regions0.contains(idx) ==> #[trigger] regions1.contains(idx),
274            forall|idx: int|
275                regions0.contains(idx) && regions0.ref_count(idx) != REF_COUNT_UNUSED ==> {
276                    &&& (#[trigger] regions1.slot_owners[idx]).same_permissions(
277                        regions0.slot_owners[idx],
278                    )
279                    &&& regions1.slot_owners[idx].usage == regions0.slot_owners[idx].usage
280                    &&& regions1.slot_owners[idx].slot_vaddr == regions0.slot_owners[idx].slot_vaddr
281                    &&& regions1.slots[idx] == regions0.slots[idx]
282                },
283        ensures
284            forall|item: C::Item|
285                #![trigger Self::item_slot_in_regions(item, regions0)]
286                Self::item_slot_in_regions(item, regions0) ==> Self::item_slot_in_regions(
287                    item,
288                    regions1,
289                ),
290    {
291        assert forall|item: C::Item|
292            Self::item_slot_in_regions(
293                item,
294                regions0,
295            ) implies #[trigger] Self::item_slot_in_regions(item, regions1) by {
296            let (pa, _level, _prop, _perm) = C::item_into_raw(item);
297            if C::item_into_raw(item).3@ is Some {
298                Self::lemma_item_slot_in_regions_preserved(item, regions0, regions1);
299            } else {
300                C::lemma_none_perm_well_formed(pa, regions1);
301            }
302        };
303    }
304
305    pub open spec fn map_item_ensures(
306        self,
307        item: C::Item,
308        old_view: CursorView<C>,
309        new_view: CursorView<C>,
310    ) -> bool {
311        let (pa, level, prop, _perm) = C::item_into_raw(item);
312        new_view == old_view.map_spec(pa, page_size::<PagingConsts>(level), prop)
313    }
314}
315
316} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_specs.rs

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