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

1use vstd::{arithmetic::div_mod::lemma_mod_add_multiples_vanish, prelude::*};
2use vstd_extra::{
3    arithmetic::{lemma_nat_align_down_sound, nat_align_down},
4    ghost_tree::*,
5    ownership::*,
6};
7
8use crate::specs::{
9    arch::{NR_ENTRIES, NR_LEVELS},
10    mm::{
11        Guards, Mapping, MetaRegionOwners,
12        frame::mapping::meta_to_index,
13        page_table::{
14            cursor::{owners::*, page_size_lemmas::lemma_page_size_ge_base},
15            lemma_next_slot_pte_index, lemma_page_size_next, lemma_pte_index_bound,
16            node::EntryOwner,
17            owners::{INC_LEVELS, OwnerSubtree, PageTableOwner},
18            pte_index_spec,
19        },
20    },
21};
22
23use crate::arch::mm::PagingConsts;
24use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_size, page_table::*};
25use core::ops::Range;
26
27verus! {
28
29broadcast use group_ghost_tree_lemmas;
30
31/// Upgrade `node_unlocked_except` to `node_unlocked` on a subtree where the excepted
32/// entry cannot appear. The precondition `path == subtree.value.path` ties structural
33/// positions to entry paths. `excepted_path` must differ from all descendant paths,
34/// which is guaranteed when `excepted_path != path` and `excepted_path` is not an
35/// extension of `path` (all descendants have paths extending `path`).
36pub proof fn subtree_unlock_upgrade<'rcu, C: PageTableConfig>(
37    subtree: OwnerSubtree<C>,
38    path: TreePath<NR_ENTRIES>,
39    guards: Guards,
40    regions: MetaRegionOwners,
41    excepted_addr: usize,
42    excepted_path: TreePath<NR_ENTRIES>,
43)
44    requires
45        subtree.inv(),
46        PageTableOwner::<C>(subtree).pt_inv(),
47        subtree.subtree_satisfies(path, PageTableOwner::<C>::metaregion_sound_pred(regions)),
48        subtree.subtree_satisfies(
49            path,
50            CursorOwner::<'rcu, C>::node_unlocked_except(guards, excepted_addr),
51        ),
52        regions.slot_owners[meta_to_index(excepted_addr)].paths_in_pt == set![excepted_path],
53        // Structural path == value path
54        path == subtree.value().path,
55        path.inv(),
56        // excepted_path does not match this subtree root
57        path != excepted_path,
58        // excepted_path is not a descendant (all descendants extend path, so if
59        // excepted_path.len() <= path.len() it can't be a descendant; otherwise
60        // it must diverge at some index below path.len())
61        excepted_path.len() <= path.len() || (exists|k: int|
62            0 <= k < path.len() && #[trigger] excepted_path[k] != path[k]),
63    ensures
64        subtree.subtree_satisfies(path, CursorOwner::<'rcu, C>::node_unlocked(guards)),
65    decreases INC_LEVELS - subtree.level(),
66{
67    reveal(PageTableOwner::pt_inv_at_depth);
68    let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
69    let g = CursorOwner::<'rcu, C>::node_unlocked_except(guards, excepted_addr);
70    let h = CursorOwner::<'rcu, C>::node_unlocked(guards);
71
72    if subtree.value().is_node() {
73        if subtree.value().node().slot_vaddr() == excepted_addr {
74            // addr == excepted_addr contradicts path != excepted_path
75            // via metaregion_sound's singleton paths_in_pt.
76            let idx = meta_to_index(excepted_addr);
77
78            assert(set![subtree.value().path].contains(excepted_path));
79            assert(false);
80        }
81    }
82    if subtree.level() < INC_LEVELS - 1 && subtree.value().is_node() {
83        assert forall|i: int|
84            #![trigger subtree.children()[i]]
85            0 <= i < subtree.children().len() && subtree.has_child(i) implies subtree.child(
86            i,
87        ).subtree_satisfies(path.push_tail(i), h) by {
88            let child = subtree.child(i);
89
90            let child_path = path.push_tail(i);
91
92            subtree_unlock_upgrade(
93                child,
94                child_path,
95                guards,
96                regions,
97                excepted_addr,
98                excepted_path,
99            );
100        };
101    } else if subtree.level() < INC_LEVELS - 1 && !subtree.value().is_node() {
102        // Non-node: pt_inv gives children[i] is None, so subtree_satisfies
103        // has no children to recurse into.
104    }
105}
106
107impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
108    /// The number of steps it will take to walk through every node of a full
109    /// page table at level `level`
110    pub open spec fn max_steps_subtree(level: usize) -> nat
111        decreases level,
112    {
113        if level <= 1 {
114            NR_ENTRIES as nat
115        } else {
116            (NR_ENTRIES as nat) * (Self::max_steps_subtree((level - 1) as usize) + 1)
117        }
118    }
119
120    /// Per-level "above-current" contribution: count `NR_ENTRIES - cont.idx - 1`
121    /// at every level (the entry at `cont.idx` is being descended into; its
122    /// work is captured at lower levels in the recursion). `max_steps()`
123    /// adds back one `subtree(self.level)` to count the current level's
124    /// in-progress entry.
125    ///
126    /// The base case is `level > NR_LEVELS` (not `== NR_LEVELS`) so that
127    /// `level == NR_LEVELS` itself contributes a non-zero term. This avoids
128    /// degenerate behavior at the root: without it, `max_steps` collapses
129    /// to 0 at the root and `push_level` from the root cannot decrease
130    /// (and the popped_too_high `q` at NR_LEVELS would dominate `self`).
131    pub open spec fn max_steps_partial(self, level: usize) -> nat
132        decreases NR_LEVELS + 1 - level,
133        when level <= NR_LEVELS + 1
134    {
135        if level > NR_LEVELS {
136            0
137        } else {
138            let cont = self.continuations[level - 1];
139            let count: nat = (NR_ENTRIES - cont.idx - 1) as nat;
140            let steps = Self::max_steps_subtree(level) * count;
141            let remaining_steps = self.max_steps_partial((level + 1) as usize);
142            steps + remaining_steps
143        }
144    }
145
146    pub open spec fn max_steps(self) -> nat {
147        (self.max_steps_partial(self.level as usize) + Self::max_steps_subtree(
148            self.level as usize,
149        )) as nat
150    }
151
152    /// Two owners with the same idx values from `start` upward have the same max_steps_partial.
153    pub proof fn max_steps_partial_eq(self, other: Self, start: usize)
154        requires
155            1 <= start <= NR_LEVELS + 1,
156            forall|k: int|
157                start - 1 <= k < NR_LEVELS ==> #[trigger] self.continuations[k].idx
158                    == other.continuations[k].idx,
159        ensures
160            self.max_steps_partial(start) == other.max_steps_partial(start),
161        decreases NR_LEVELS + 1 - start,
162    {
163        if start <= NR_LEVELS {
164            self.max_steps_partial_eq(other, (start + 1) as usize);
165        }
166    }
167
168    pub proof fn max_steps_partial_inv(self, other: Self, level: usize)
169        requires
170            self.inv(),
171            other.inv(),
172            self.level == other.level,
173            self.level <= level <= NR_LEVELS + 1,
174            forall|i: int|
175                #![trigger self.continuations[i].idx]
176                #![trigger other.continuations[i].idx]
177                self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].idx
178                    == other.continuations[i].idx,
179        ensures
180            self.max_steps_partial(level) == other.max_steps_partial(level),
181        decreases NR_LEVELS + 1 - level,
182    {
183        if level <= NR_LEVELS {
184            self.max_steps_partial_inv(other, (level + 1) as usize);
185        }
186    }
187
188    pub open spec fn push_level_owner(self, guard: PageTableGuard<'rcu, C>) -> Self {
189        let cont = self.continuations[self.level - 1];
190        let (child, cont) = cont.make_cont(
191            pte_index_spec::<C>(self.cur_va(), (self.level - 1) as PagingLevel),
192            guard,
193        );
194        let new_continuations = self.continuations.insert(self.level - 1, cont).insert(
195            self.level - 2,
196            child,
197        );
198
199        let new_level = (self.level - 1) as u8;
200        Self { continuations: new_continuations, level: new_level, popped_too_high: false, ..self }
201    }
202
203    pub proof fn push_level_owner_decreases_steps(self, guard: PageTableGuard<'rcu, C>)
204        requires
205            self.inv(),
206            self.level > 1,
207        ensures
208            self.push_level_owner(guard).max_steps() < self.max_steps(),
209    {
210        C::lemma_paging_consts_properties();
211        lemma_pte_index_bound::<C>(self.cur_va(), (self.level - 1) as PagingLevel);
212        let new_self = self.push_level_owner(guard);
213        let l = self.level as usize;
214        let lm1 = (self.level - 1) as usize;
215        // Continuations agree at indices [l-1, NR_LEVELS): only [l-2] changed.
216        new_self.max_steps_partial_eq(self, l);
217        // va.index[l-2] < NR_ENTRIES (from va.inv()).
218        assert(pte_index_spec::<C>(self.va, (self.level - 2 + 1) as PagingLevel) < NR_ENTRIES);
219        let new_child = new_self.continuations[lm1 - 1];
220
221        // subtree(l) == NR * (subtree(lm1) + 1) (from def of max_steps_subtree, l > 1).
222        // subtree(lm1) * (NR - new_child.idx) <= subtree(lm1) * NR < subtree(l).
223        vstd::arithmetic::mul::lemma_mul_inequality(
224            (NR_ENTRIES - new_child.idx) as int,
225            NR_ENTRIES as int,
226            Self::max_steps_subtree(lm1) as int,
227        );
228        vstd::arithmetic::mul::lemma_mul_is_distributive_add(
229            Self::max_steps_subtree(lm1) as int,
230            NR_ENTRIES - new_child.idx - 1,
231            1,
232        );
233        vstd::arithmetic::mul::lemma_mul_is_commutative(
234            (NR_ENTRIES - new_child.idx) as int,
235            Self::max_steps_subtree(lm1) as int,
236        );
237
238    }
239
240    pub proof fn push_level_owner_preserves_mappings(self, guard: PageTableGuard<'rcu, C>)
241        requires
242            self.inv(),
243            self.level > 1,
244            self.cur_entry_owner().is_node(),
245        ensures
246            self.push_level_owner(guard)@.mappings == self@.mappings,
247    {
248        C::lemma_paging_consts_properties();
249        lemma_pte_index_bound::<C>(self.cur_va(), (self.level - 1) as PagingLevel);
250        broadcast use {
251            CursorContinuation::group_lemmas,
252            CursorOwner::group_lemmas,
253            PageTableOwner::group_lemmas,
254        };
255
256        let new_owner = self.push_level_owner(guard);
257        let old_cont = self.continuations[self.level - 1];
258        let (_, modified_cont) = old_cont.make_cont(
259            pte_index_spec::<C>(self.cur_va(), (self.level - 1) as PagingLevel),
260            guard,
261        );
262
263        old_cont.view_mappings_take_child();
264
265        let taken = old_cont.take_child().1;
266
267        assert(modified_cont.children == taken.children) by {};
268
269        assert forall|m: Mapping|
270            self.view_mappings().contains(m) implies new_owner.view_mappings().contains(m) by {
271            let i = choose|i: int|
272                self.level - 1 <= i < NR_LEVELS && (
273                #[trigger] self.continuations[i]).view_mappings().contains(m);
274            if i == self.level - 1 {
275                if old_cont.view_mappings_take_child_spec().contains(m) {
276                    assert(new_owner.continuations[self.level - 2].view_mappings().contains(m));
277                } else {
278                    assert(new_owner.continuations[self.level - 1].view_mappings().contains(m));
279                }
280            } else {
281                assert(new_owner.continuations[i] == self.continuations[i]);
282            }
283        };
284
285    }
286
287    pub proof fn push_level_owner_preserves_inv(self, guard: PageTableGuard<'rcu, C>)
288        requires
289            self.inv(),
290            self.level > 1,
291            !self.popped_too_high,
292            self.level <= self.guard_level,
293            self.in_locked_range(),
294            // The current entry is a node (we're descending into it)
295            self.cur_entry_owner().is_node(),
296            // The child node's guard relates to the new guard
297            self.cur_entry_owner().node().relate_guard(guard),
298            // Guard distinctness: the new guard points to a different node than all existing continuations
299            forall|i: int|
300                #![trigger self.continuations[i]]
301                self.level - 1 <= i < NR_LEVELS
302                    ==> self.continuations[i].guard.inner.inner@.ptr.addr()
303                    != guard.inner.inner@.ptr.addr(),
304        ensures
305            self.push_level_owner(guard).inv(),
306    {
307        C::lemma_paging_consts_properties();
308        lemma_pte_index_bound::<C>(self.cur_va(), (self.level - 1) as PagingLevel);
309        // locking-work: when self.level == self.guard_level, self.inv() does
310        // not supply va.index[guard_level-1] == prefix.index[guard_level-1]
311        // (the conjunct at owners.rs:481-482 requires strict level < guard_level).
312        // After push_level, the new level < guard_level triggers that conjunct.
313        // Derive it from in_locked_range() for all cases.
314        self.lemma_in_locked_range_guard_index_eq_prefix();
315
316        let new_owner = self.push_level_owner(guard);
317
318        let old_cont = self.continuations[self.level - 1];
319
320        let child_node = old_cont.children[old_cont.idx as int].unwrap();
321        let (child, _) = old_cont.make_cont(
322            pte_index_spec::<C>(self.cur_va(), (self.level - 1) as PagingLevel),
323            guard,
324        );
325
326        assert(pte_index_spec::<C>(self.va, (self.level - 2 + 1) as PagingLevel) < NR_ENTRIES);
327
328        assert(child.inv_children_rel()) by {
329            assert forall|j: int|
330                0 <= j < NR_ENTRIES && #[trigger] child.children[j] is Some implies {
331                &&& child.children[j].unwrap().value().parent_level == child.level()
332                &&& child.children[j].unwrap().level() == child.tree_level + 1
333                &&& child.children[j].unwrap().value().path.len()
334                    == child.entry_own.node().tree_level + 1
335                &&& child.children[j].unwrap().value().match_pte(
336                    child.entry_own.node().children_perm.value()[j],
337                    child.entry_own.node().level(),
338                )
339                &&& <EntryOwner<C> as TreeNodeValue<NR_LEVELS>>::rel_children(
340                    child.entry_own,
341                    j,
342                    Some(child.children[j].unwrap().value()),
343                )
344                &&& child.children[j].unwrap().value().path == child.path().push_tail(j)
345            } by {
346                let gc = child.children[j].unwrap();
347                PageTableOwner(child_node).pt_inv_unroll(j);
348
349            };
350        };
351        assert(child.pt_inv_children()) by {
352            assert forall|j: int|
353                0 <= j < child.children.len()
354                    && #[trigger] child.children[j] is Some implies PageTableOwner(
355                child.children[j].unwrap(),
356            ).pt_inv() by {
357                PageTableOwner(child_node).pt_inv_unroll(j);
358
359            };
360        };
361
362        assert(new_owner.continuations[new_owner.level - 1].all_some()) by {
363            assert forall|j: int| 0 <= j < NR_ENTRIES implies child.children[j] is Some by {
364                PageTableOwner(child_node).pt_inv_unroll(j);
365
366            };
367        };
368
369    }
370
371    #[verifier::rlimit(120)]
372    pub proof fn push_level_owner_preserves_invs(
373        self,
374        guard: PageTableGuard<'rcu, C>,
375        regions: MetaRegionOwners,
376        guards: Guards,
377    )
378        requires
379            self.inv(),
380            self.level > 1,
381            !self.popped_too_high,
382            self.level <= self.guard_level,
383            self.in_locked_range(),
384            self.only_current_locked(guards),
385            self.nodes_locked(guards),
386            self.metaregion_sound(regions),
387            // The current entry is a node (we're descending into it)
388            self.cur_entry_owner().is_node(),
389            // The child node's guard relates to the new guard
390            self.cur_entry_owner().node().relate_guard(guard),
391            // The new guard must be locked in guards
392            guards.lock_held(guard.inner.inner@.ptr.addr()),
393        ensures
394            self.push_level_owner(guard).inv(),
395            self.push_level_owner(guard).children_not_locked(guards),
396            self.push_level_owner(guard).nodes_locked(guards),
397            self.push_level_owner(guard).metaregion_sound(regions),
398    {
399        C::lemma_paging_consts_properties();
400        lemma_pte_index_bound::<C>(self.cur_va(), (self.level - 1) as PagingLevel);
401        reveal(CursorContinuation::map_children);
402        let new_owner = self.push_level_owner(guard);
403        let old_cont = self.continuations[self.level - 1];
404
405        let (child_cont, modified_cont) = old_cont.make_cont(
406            pte_index_spec::<C>(self.cur_va(), (self.level - 1) as PagingLevel),
407            guard,
408        );
409
410        let cur_entry = self.cur_entry_owner();
411        let cur_entry_addr = cur_entry.node().slot_vaddr();
412        let cur_entry_path = old_cont.path().push_tail(old_cont.idx as int);
413
414        assert forall|i: int|
415            #![trigger self.continuations[i]]
416            self.level - 1 <= i
417                < NR_LEVELS implies self.continuations[i].guard.inner.inner@.ptr.addr()
418            != guard.inner.inner@.ptr.addr() by {
419            reveal(CursorOwner::path_metaregion_sound);
420            let cont_i = self.continuations[i];
421
422            if cont_i.guard.inner.inner@.ptr.addr() == guard.inner.inner@.ptr.addr() {
423                let addr = cont_i.entry_own.node().slot_vaddr();
424                assert(addr == cur_entry.node().slot_vaddr());
425                let idx = meta_to_index(addr);
426                assert(regions.slot_owners[idx].paths_in_pt == set![cont_i.path()]);
427                assert(regions.slot_owners[idx].paths_in_pt == set![cur_entry_path]);
428                assert(set![cont_i.path()].contains(cur_entry_path));
429
430                assert(cur_entry_path.len() == old_cont.tree_level + 1) by {
431                    old_cont.lemma_inv_children_rel_unroll(old_cont.idx as int);
432                };
433                assert(false);
434            }
435        };
436
437        self.push_level_owner_preserves_inv(guard);
438
439        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
440        let g_except = CursorOwner::<'rcu, C>::node_unlocked_except(guards, cur_entry_addr);
441        let h = CursorOwner::<'rcu, C>::node_unlocked(guards);
442
443        assert forall|i: int|
444            #![trigger new_owner.continuations[i]]
445            new_owner.level - 1 <= i < NR_LEVELS implies new_owner.continuations[i].map_children(
446            h,
447        ) by {
448            if i == self.level - 2 {
449                assert forall|j: int|
450                    #![trigger child_cont.children[j]]
451                    0 <= j < child_cont.children.len()
452                        && child_cont.children[j] is Some implies child_cont.children[j].unwrap().subtree_satisfies(
453                child_cont.path().push_tail(j), h) by {
454                    let gc = child_cont.children[j].unwrap();
455                    let gc_path = child_cont.path().push_tail(j);
456
457                    let child_subtree = old_cont.children[old_cont.idx as int].unwrap();
458                    child_subtree.lemma_subtree_satisfies_unroll_once(cur_entry_path, f, j);
459                    child_subtree.lemma_subtree_satisfies_unroll_once(cur_entry_path, g_except, j);
460
461                    subtree_unlock_upgrade(
462                        gc,
463                        gc_path,
464                        guards,
465                        regions,
466                        cur_entry_addr,
467                        cur_entry_path,
468                    );
469                };
470            } else if i == self.level - 1 {
471                assert forall|j: int|
472                    #![trigger modified_cont.children[j]]
473                    0 <= j < modified_cont.children.len()
474                        && modified_cont.children[j] is Some implies modified_cont.children[j].unwrap().subtree_satisfies(
475                modified_cont.path().push_tail(j), h) by {
476                    let sibling = old_cont.children[j].unwrap();
477                    let sibling_path = old_cont.path().push_tail(j);
478
479                    subtree_unlock_upgrade(
480                        sibling,
481                        sibling_path,
482                        guards,
483                        regions,
484                        cur_entry_addr,
485                        cur_entry_path,
486                    );
487                };
488            } else {
489                let cont_i = self.continuations[i];
490
491                assert(cur_entry_path[cont_i.tree_level as int] == cont_i.idx);
492
493                assert forall|j: int|
494                    #![trigger cont_i.children[j]]
495                    0 <= j < cont_i.children.len()
496                        && cont_i.children[j] is Some implies cont_i.children[j].unwrap().subtree_satisfies(
497                cont_i.path().push_tail(j), h) by {
498                    let child_sub = cont_i.children[j].unwrap();
499                    let child_path = cont_i.path().push_tail(j);
500
501                    subtree_unlock_upgrade(
502                        child_sub,
503                        child_path,
504                        guards,
505                        regions,
506                        cur_entry_addr,
507                        cur_entry_path,
508                    );
509                };
510            }
511        };
512
513        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
514        let child_subtree = child_cont.as_subtree();
515
516        assert(child_cont.map_children(f)) by {
517            assert forall|j: int|
518                0 <= j < child_cont.children.len()
519                    && #[trigger] child_cont.children[j] is Some implies child_cont.children[j].unwrap().subtree_satisfies(
520            child_cont.path().push_tail(j), f) by {
521                child_subtree.lemma_subtree_satisfies_unroll_once(child_cont.path(), f, j);
522
523            };
524        };
525        reveal(CursorOwner::path_metaregion_sound);
526    }
527
528    pub proof fn tracked_push_level_owner(tracked &mut self, guard: PageTableGuard<'rcu, C>)
529        requires
530            old(self).inv(),
531            old(self).level > 1,
532        ensures
533            *final(self) == old(self).push_level_owner(guard),
534    {
535        C::lemma_paging_consts_properties();
536        lemma_pte_index_bound::<C>(self.cur_va(), (self.level - 1) as PagingLevel);
537        assert(pte_index_spec::<C>(self.va, (self.level - 2 + 1) as PagingLevel) < NR_ENTRIES);
538
539        let ghost self0 = *self;
540        let tracked mut cont = self.continuations.tracked_remove(self.level - 1);
541        let tracked child = cont.tracked_make_cont(
542            pte_index_spec::<C>(self.cur_va(), (self.level - 1) as PagingLevel),
543            guard,
544        );
545
546        self.continuations.tracked_insert(self.level - 1, cont);
547        self.continuations.tracked_insert(self.level - 2, child);
548
549        assert(self.continuations == self0.continuations.insert(self.level - 1, cont).insert(
550            self.level - 2,
551            child,
552        ));
553
554        self.popped_too_high = false;
555
556        self.level = (self.level - 1) as u8;
557    }
558
559    pub open spec fn pop_level_owner(self) -> (Self, PageTableGuard<'rcu, C>) {
560        let child = self.continuations[self.level - 1];
561        let cont = self.continuations[self.level as int];
562        let (new_cont, guard) = cont.restore(child);
563        let new_continuations = self.continuations.insert(self.level as int, new_cont).remove(
564            self.level - 1,
565        );
566        let new_level = (self.level + 1) as u8;
567        let popped_too_high = if new_level >= self.guard_level {
568            true
569        } else {
570            false
571        };
572        (
573            Self {
574                continuations: new_continuations,
575                level: new_level,
576                popped_too_high: popped_too_high,
577                ..self
578            },
579            guard,
580        )
581    }
582
583    #[verifier::rlimit(200)]
584    pub proof fn pop_level_owner_preserves_invs(self, guards: Guards, regions: MetaRegionOwners)
585        requires
586            self.inv(),
587            self.level < NR_LEVELS,
588            self.children_not_locked(guards),
589            self.nodes_locked(guards),
590            self.metaregion_sound(regions),
591        ensures
592            self.pop_level_owner().0.inv(),
593            self.pop_level_owner().0.only_current_locked(guards),
594            self.pop_level_owner().0.nodes_locked(guards),
595            self.pop_level_owner().0.metaregion_sound(regions),
596    {
597        reveal(PageTableOwner::pt_inv_at_depth);
598        let child = self.continuations[self.level - 1];
599        let child_addr = child.entry_own.node().slot_vaddr();
600
601        self.map_children_implies(
602            CursorOwner::<'rcu, C>::node_unlocked(guards),
603            CursorOwner::<'rcu, C>::node_unlocked_except(guards, child_addr),
604        );
605        reveal(CursorContinuation::map_children);
606        reveal(CursorOwner::path_metaregion_sound);
607    }
608
609    pub open spec fn move_forward_owner_spec(self) -> Self
610        decreases NR_LEVELS - self.level,
611        when self.level <= NR_LEVELS
612    {
613        if self.index() + 1 < NR_ENTRIES {
614            // Standard advance. At the very last in-range top-level slot, this
615            // produces a "one-past-end" cursor with idx == TOP_LEVEL_INDEX_RANGE.end,
616            // which the cursor inv allows (relaxed `<= top_end`). Such a cursor is
617            // `above_locked_range`.
618            self.inc_index().zero_below_level()
619        } else if self.level < NR_LEVELS {
620            self.pop_level_owner().0.move_forward_owner_spec()
621        } else {
622            // self.level == NR_LEVELS && self.index() + 1 == NR_ENTRIES.
623            // Preserve lower address bits and the former address-word wrapping semantics.
624            Self {
625                va: (self.va + page_size::<C>(C::NR_LEVELS())) as Vaddr,
626                popped_too_high: false,
627                ..self
628            }
629        }
630    }
631
632    pub proof fn move_forward_increases_va(self)
633        requires
634            self.inv(),
635            self.level <= NR_LEVELS,
636            self.in_locked_range(),
637            !self.popped_too_high,
638        ensures
639            self.move_forward_owner_spec().va > self.va,
640    {
641        self.lemma_in_locked_range_guard_index_eq_prefix();
642        self.move_forward_va_is_align_up();
643        self.lemma_va_plus_page_size_no_overflow(self.level);
644        lemma_page_size_ge_base::<PagingConsts>(self.level);
645        lemma_nat_align_down_sound(self.va as nat, page_size::<PagingConsts>(self.level) as nat);
646    }
647
648    pub proof fn move_forward_not_popped_too_high(self)
649        requires
650            self.inv(),
651            self.level <= NR_LEVELS,
652            self.in_locked_range(),
653        ensures
654            !self.move_forward_owner_spec().popped_too_high,
655        decreases NR_LEVELS - self.level,
656    {
657        reveal(PageTableOwner::pt_inv_at_depth);
658        if self.index() + 1 >= NR_ENTRIES && self.level < NR_LEVELS {
659            self.pop_level_owner().0.move_forward_not_popped_too_high();
660        }
661    }
662
663    /// Variant of `move_forward_owner_decreases_steps` for the popped_too_high
664    /// case. Same postcondition, but precondition allows `popped_too_high`.
665    /// Used by the main lemma's case 2b to handle the chain of pops that
666    /// `move_forward_owner_spec` does internally when popped_too_high.
667    pub proof fn move_forward_owner_popped_too_high_decreases(self)
668        requires
669            self.inv(),
670            self.level <= NR_LEVELS,
671            self.in_locked_range(),
672            self.popped_too_high,
673            self.continuations[NR_LEVELS - 1].idx + 1 < NR_ENTRIES,
674        ensures
675            self.move_forward_owner_spec().max_steps() + Self::max_steps_subtree(
676                self.level as usize,
677            ) <= self.max_steps(),
678        decreases NR_LEVELS - self.level,
679    {
680        reveal(PageTableOwner::pt_inv_at_depth);
681        let l = self.level as usize;
682        let st_l = Self::max_steps_subtree(l) as int;
683
684        if self.index() + 1 < NR_ENTRIES {
685            // Case A: advance via inc_index().zero_below_level().
686            // (Mirror of subcase A in the main lemma's case 2b.)
687            let inc = self.inc_index();
688
689            let new_state = inc.zero_below_level();
690
691            new_state.max_steps_partial_eq(self, (self.level + 1) as usize);
692            let self_idx = self.continuations[self.level - 1].idx as int;
693            vstd::arithmetic::mul::lemma_mul_is_distributive_add(
694                st_l,
695                NR_ENTRIES - self_idx - 2,
696                1,
697            );
698
699        } else if self.level < NR_LEVELS {
700            // Case B1: pop again (popped2.popped_too_high also true) and recurse.
701            let popped2 = self.pop_level_owner().0;
702            let lp1 = (self.level + 1) as usize;
703            popped2.max_steps_partial_eq(self, lp1);
704
705            assert(Self::max_steps_subtree(l) * 0nat == 0) by (nonlinear_arith);
706
707            // popped2.popped_too_high holds: popped2.level == self.level + 1
708            // > self.guard_level (since self.popped_too_high gives
709            // self.level >= self.guard_level), so popped2 satisfies the
710            // popped_too_high arm of pop_level_owner.
711
712            // Recurse on popped2.
713            popped2.move_forward_owner_popped_too_high_decreases();
714
715        } else {
716            // Case C: self.level == NR_LEVELS && self.index() + 1 == NR_ENTRIES.
717            // Excluded by the lemma's precondition.
718            assert(false);
719        }
720    }
721
722    pub proof fn move_forward_owner_decreases_steps(self)
723        requires
724            self.inv(),
725            self.level <= NR_LEVELS,
726            self.in_locked_range(),
727            !self.popped_too_high,
728            // See `move_forward_owner_popped_too_high_decreases` for the
729            // rationale: rules out the unreachable third-branch corner.
730            self.continuations[NR_LEVELS - 1].idx + 1 < NR_ENTRIES,
731        ensures
732    // "Decrease by ≥ subtree(self.level)" form: needed by `push_level`
733    // and by the pop+recursion case to compensate for pop_level's
734    // `+(subtree(L+1) - subtree(L))` increase.
735
736            self.move_forward_owner_spec().max_steps() + Self::max_steps_subtree(
737                self.level as usize,
738            ) <= self.max_steps(),
739            self.move_forward_owner_spec().max_steps() < self.max_steps(),
740        decreases NR_LEVELS - self.level,
741    {
742        reveal(PageTableOwner::pt_inv_at_depth);
743        let l = self.level as usize;
744        let st_l = Self::max_steps_subtree(l) as int;
745
746        if self.index() + 1 < NR_ENTRIES {
747            // Case 1: increment idx at the current level.
748            //   new_state.max_steps_partial(L) = old.max_steps_partial(L) - subtree(L)
749            //   max_steps adds +subtree(L) on both sides → diff = -subtree(L).
750            let inc = self.inc_index();
751
752            let new_state = inc.zero_below_level();
753
754            new_state.max_steps_partial_eq(self, (self.level + 1) as usize);
755            let self_idx = self.continuations[self.level - 1].idx as int;
756            let tail = self.max_steps_partial((self.level + 1) as usize) as int;
757            // st_l * (NR - idx - 1) == st_l * (NR - idx - 2) + st_l * 1.
758            vstd::arithmetic::mul::lemma_mul_is_distributive_add(
759                st_l,
760                NR_ENTRIES - self_idx - 2,
761                1,
762            );
763            // Tie new_state to move_forward_owner_spec and stitch the arithmetic:
764            //   new_state.max_steps_partial(l) = (NR - self_idx - 2) * st_l + tail
765            //   new_state.max_steps()          = new_state.max_steps_partial(l) + st_l
766            //   self.max_steps()               = (NR - self_idx - 1) * st_l + tail + st_l
767            // Hence new_state.max_steps() + st_l == self.max_steps() (equality, so ≤).
768
769        } else if self.level < NR_LEVELS {
770            let popped = self.pop_level_owner().0;
771            let lp1 = (self.level + 1) as usize;
772            popped.max_steps_partial_eq(self, lp1);
773
774            assert(Self::max_steps_subtree(l) * 0nat == 0) by (nonlinear_arith);
775
776            if !popped.popped_too_high {
777                popped.move_forward_owner_decreases_steps();
778
779            } else {
780                // popped.popped_too_high — delegate to the popped_too_high
781                // variant, which handles all subcases (advance, recursive pop,
782                // and the NR_LEVELS leaf) in one call.
783                popped.move_forward_owner_popped_too_high_decreases();
784            }
785        } else {
786            assert(false);
787        }
788    }
789
790    /// Advancing the cursor reaches the next slot boundary, including carries to a parent.
791    #[verifier::spinoff_prover]
792    pub proof fn move_forward_va_is_align_up(self)
793        requires
794            self.inv(),
795            self.level <= NR_LEVELS,
796            self.in_locked_range(),
797            !self.popped_too_high,
798            self.level == self.guard_level ==> self.index() + 1 < NR_ENTRIES,
799        ensures
800            self.move_forward_owner_spec().va == self@.align_up_spec(
801                page_size::<PagingConsts>(self.level),
802            ),
803        decreases NR_LEVELS - self.level,
804    {
805        C::lemma_paging_consts_properties();
806        reveal(PageTableOwner::pt_inv_at_depth);
807        if self.index() + 1 < NR_ENTRIES {
808            self.inc_and_zero_increases_va();
809            return;
810        }
811        assert(self.level < NR_LEVELS);
812        let popped = self.pop_level_owner().0;
813        assert(self.move_forward_owner_spec().va == popped.move_forward_owner_spec().va);
814        if !popped.popped_too_high {
815            popped.move_forward_va_is_align_up();
816            popped.lemma_va_plus_page_size_no_overflow(popped.level);
817        } else {
818            popped.inc_and_zero_increases_va();
819            popped.lemma_inc_index_va();
820        }
821
822        self.lemma_cur_pte_index();
823        self.lemma_va_plus_page_size_no_overflow(self.level);
824        lemma_page_size_next::<C>(self.level);
825        lemma_page_size_ge_base::<PagingConsts>(self.level);
826        lemma_nat_align_down_sound(self.va as nat, page_size::<PagingConsts>(self.level) as nat);
827        let next = self@.align_up_spec(page_size::<PagingConsts>(self.level));
828        lemma_mod_add_multiples_vanish(
829            nat_align_down(self.va as nat, page_size::<PagingConsts>(self.level) as nat) as int,
830            page_size::<PagingConsts>(self.level) as int,
831        );
832        lemma_next_slot_pte_index::<C>(self.va, next, self.level);
833        assert(pte_index_spec::<C>(next, self.level) == 0);
834        lemma_next_slot_pte_index::<C>(popped.va, next, popped.level);
835        assert(self@.align_up_spec(page_size::<PagingConsts>(self.level)) == popped@.align_up_spec(
836            page_size::<PagingConsts>(popped.level),
837        ));
838    }
839
840    /// After popping a level, the total view_mappings is preserved.
841    /// The restored parent at index self.level absorbs the child's mappings,
842    /// and both are within the view_mappings range [self.level, NR_LEVELS).
843    pub proof fn pop_level_owner_preserves_mappings(self)
844        requires
845            self.inv(),
846            self.level < NR_LEVELS,
847            self.in_locked_range(),
848        ensures
849            self.pop_level_owner().0@.mappings == self@.mappings,
850    {
851        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
852
853        let child = self.continuations[self.level - 1];
854        let parent = self.continuations[self.level as int];
855        let (restored_parent, _) = parent.restore(child);
856        let popped = self.pop_level_owner().0;
857        let child_subtree = child.as_subtree();
858
859        let r = restored_parent;
860        let p = parent.put_child(child_subtree);
861        assert forall|j: int| 0 <= j < r.children.len() implies r.children[j]
862            == p.children[j] by {};
863
864        assert(restored_parent.view_mappings() == parent.put_child(child_subtree).view_mappings())
865            by {};
866
867        parent.view_mappings_put_child(child_subtree);
868        child.as_page_table_owner_preserves_view_mappings();
869
870        assert(popped.view_mappings() == self.view_mappings()) by {
871            assert forall|m: Mapping|
872                self.view_mappings().contains(m) implies popped.view_mappings().contains(m) by {
873                let i = choose|i: int|
874                    self.level - 1 <= i < NR_LEVELS && (
875                    #[trigger] self.continuations[i]).view_mappings().contains(m);
876                if i == self.level - 1 {
877                    assert(popped.continuations[self.level as int].view_mappings().contains(m));
878                } else if i == self.level {
879                    assert(popped.continuations[self.level as int].view_mappings().contains(m));
880                } else {
881                    assert(popped.continuations[i] == self.continuations[i]);
882                }
883            };
884
885        };
886    }
887
888    pub proof fn move_forward_owner_preserves_mappings(self)
889        requires
890            self.inv(),
891            self.in_locked_range(),
892        ensures
893            self.move_forward_owner_spec()@.mappings == self@.mappings,
894        decreases NR_LEVELS - self.level,
895    {
896        reveal(PageTableOwner::pt_inv_at_depth);
897        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
898
899        if self.index() + 1 < NR_ENTRIES {
900            let inc = self.inc_index();
901            let result = inc.zero_below_level();
902
903            let old_cont = self.continuations[self.level - 1];
904            let new_cont = old_cont.inc_index();
905
906            assert(result.view_mappings() == self.view_mappings()) by {
907                assert forall|m: Mapping|
908                    self.view_mappings().contains(m) implies result.view_mappings().contains(m) by {
909                    let i = choose|i: int|
910                        self.level - 1 <= i < NR_LEVELS && (
911                        #[trigger] self.continuations[i]).view_mappings().contains(m);
912                    if i == self.level - 1 {
913                        assert(result.continuations[i].view_mappings().contains(m));
914                    } else {
915                        assert(result.continuations[i] == self.continuations[i]);
916                    }
917                };
918
919            };
920
921        } else if self.level < NR_LEVELS {
922            let popped = self.pop_level_owner().0;
923
924            self.pop_level_owner_preserves_mappings();
925            popped.move_forward_owner_preserves_mappings();
926        }
927    }
928}
929
930} // verus!
ostd/specs/mm/page_table/cursor/cursor_steps.rs

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