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

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

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