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

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

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