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

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