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

1use vstd::prelude::*;
2
3use vstd_extra::ghost_tree::*;
4use vstd_extra::ownership::*;
5
6use crate::mm::page_table::*;
7use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
8use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
9use crate::specs::arch::paging_consts::PagingConsts;
10use crate::specs::mm::page_table::cursor::owners::*;
11use crate::specs::mm::page_table::node::EntryOwner;
12use crate::specs::mm::page_table::node::GuardPerm;
13use crate::specs::mm::page_table::owners::{OwnerSubtree, PageTableOwner, INC_LEVELS};
14use crate::specs::mm::page_table::AbstractVaddr;
15use crate::specs::mm::Guards;
16use crate::specs::mm::MetaRegionOwners;
17
18use core::ops::Range;
19
20verus! {
21
22/// Paths obtained by push_tail with different indices are different
23pub proof fn push_tail_different_indices_different_paths(
24    path: TreePath<NR_ENTRIES>,
25    i: usize,
26    j: usize,
27)
28    requires
29        path.inv(),
30        0 <= i < NR_ENTRIES,
31        0 <= j < NR_ENTRIES,
32        i != j,
33    ensures
34        path.push_tail(i) != path.push_tail(j),
35{
36    path.push_tail_property(i);
37    path.push_tail_property(j);
38    assert(path.push_tail(i).index(path.len() as int) == i as usize);
39    assert(path.push_tail(j).index(path.len() as int) == j as usize);
40    if path.push_tail(i) == path.push_tail(j) {
41        assert(i == j); // Contradiction
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    // Trivial: if path1 == path2, then their lengths are equal
56    if path1 == path2 {
57        assert(path1.len() == path2.len());
58    }
59}
60
61/// A path obtained by push_tail has greater length than the original
62pub proof fn push_tail_increases_length(
63    path: TreePath<NR_ENTRIES>,
64    i: usize,
65)
66    requires
67        path.inv(),
68        0 <= i < NR_ENTRIES,
69    ensures
70        path.push_tail(i).len() > path.len(),
71{
72    path.push_tail_property(i);
73}
74
75impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
76
77    /// The number of steps it will take to walk through every node of a full
78    /// page table at level `level`
79    pub open spec fn max_steps_subtree(level: usize) -> usize
80        decreases level,
81    {
82        if level <= 1 {
83            NR_ENTRIES
84        } else {
85            // One step to push down a level, then the number for that subtree
86            (NR_ENTRIES * (Self::max_steps_subtree((level - 1) as usize) + 1)) as usize
87        }
88    }
89
90    /// The number of steps it will take to walk through the remaining entries of the page table
91    /// starting at the given level.
92    pub open spec fn max_steps_partial(self, level: usize) -> usize
93        decreases NR_LEVELS - level,
94        when level <= NR_LEVELS
95    {
96        if level == NR_LEVELS {
97            0
98        } else {
99            // How many entries remain at this level?
100            let cont = self.continuations[(level - 1) as int];
101            // Each entry takes at most `max_step_subtree` steps.
102            let steps = Self::max_steps_subtree(level) * (NR_ENTRIES - cont.idx);
103            // Then the number of steps for the remaining entries at higher levels
104            let remaining_steps = self.max_steps_partial((level + 1) as usize);
105            (steps + remaining_steps) as usize
106        }
107    }
108
109    pub open spec fn max_steps(self) -> usize {
110        self.max_steps_partial(self.level as usize)
111    }
112
113    pub proof fn max_steps_partial_inv(self, other: Self, level: usize)
114        requires
115            self.inv(),
116            other.inv(),
117            self.level == other.level,
118            self.level <= level <= NR_LEVELS,
119            forall |i: int|
120                #![trigger self.continuations[i].idx]
121                #![trigger other.continuations[i].idx]
122            self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].idx == other.continuations[i].idx,
123        ensures
124            self.max_steps_partial(level) == other.max_steps_partial(level),
125        decreases NR_LEVELS - level,
126    {
127        if level < NR_LEVELS {
128            self.max_steps_partial_inv(other, (level + 1) as usize);
129        }
130    }
131
132    pub open spec fn push_level_owner_spec(self, guard_perm: GuardPerm<'rcu, C>) -> Self
133    {
134        let cont = self.continuations[self.level - 1];
135        let (child, cont) = cont.make_cont_spec(self.va.index[self.level - 2] as usize, guard_perm);
136        let new_continuations = self.continuations.insert(self.level - 1, cont);
137        let new_continuations = new_continuations.insert(self.level - 2, child);
138
139        let new_level = (self.level - 1) as u8;
140        Self {
141            continuations: new_continuations,
142            level: new_level,
143            popped_too_high: false,
144            ..self
145        }
146    }
147
148    pub proof fn push_level_owner_decreases_steps(self, guard_perm: GuardPerm<'rcu, C>)
149        requires
150            self.inv(),
151            self.level > 0,
152        ensures
153            self.push_level_owner_spec(guard_perm).max_steps() < self.max_steps()
154    { admit() }
155
156    pub proof fn push_level_owner_preserves_va(self, guard_perm: GuardPerm<'rcu, C>)
157        requires
158            self.inv(),
159            self.level > 1,
160        ensures
161            self.push_level_owner_spec(guard_perm).va == self.va,
162            self.push_level_owner_spec(guard_perm).continuations[self.level - 2].idx == self.va.index[self.level - 2],
163    {
164        assert(self.va.index.contains_key(self.level - 2));
165    }
166
167    pub proof fn push_level_owner_preserves_mappings(self, guard_perm: GuardPerm<'rcu, C>)
168        requires
169            self.inv(),
170            self.level > 1,
171        ensures
172            self.push_level_owner_spec(guard_perm)@.mappings == self@.mappings,
173    { admit() }
174
175    pub proof fn push_level_owner_preserves_inv(self, guard_perm: GuardPerm<'rcu, C>)
176        requires
177            self.inv(),
178            self.level > 1,
179            forall |i: int|
180                #![trigger self.continuations[i]]
181                self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].guard_perm.addr() != guard_perm.addr(),
182        ensures
183            self.push_level_owner_spec(guard_perm).inv(),
184    {
185        let new_owner = self.push_level_owner_spec(guard_perm);
186        let new_level = (self.level - 1) as u8;
187
188        let old_cont = self.continuations[self.level - 1];
189        let child_node = old_cont.children[old_cont.idx as int].unwrap();
190        let (child, modified_cont) = old_cont.make_cont_spec(self.va.index[self.level - 2] as usize, guard_perm);
191
192        assert(child.inv()) by { admit() };
193
194        assert(new_owner.level == new_level);
195        assert(new_owner.va == self.va);
196        assert(new_owner.guard_level == self.guard_level);
197        assert(new_owner.prefix == self.prefix);
198        assert(new_owner.popped_too_high == false);
199        assert(new_owner.continuations[self.level - 1] == modified_cont);
200        assert(new_owner.continuations[self.level - 2] == child);
201
202        assert(modified_cont.entry_own == old_cont.entry_own);
203        assert(modified_cont.idx == old_cont.idx);
204        assert(modified_cont.tree_level == old_cont.tree_level);
205        assert(modified_cont.path == old_cont.path);
206        assert(modified_cont.guard_perm == old_cont.guard_perm);
207        assert(modified_cont.children == old_cont.children.update(old_cont.idx as int, None));
208
209        assert(child.entry_own == child_node.value);
210        assert(child.tree_level == old_cont.tree_level + 1);
211        assert(child.idx == self.va.index[self.level - 2] as usize);
212        assert(child.children == child_node.children);
213        assert(child.guard_perm == guard_perm);
214
215        assert(new_owner.va.inv());
216
217        assert(1 <= new_owner.level <= NR_LEVELS);
218
219        assert(new_owner.guard_level <= NR_LEVELS);
220
221        assert(!new_owner.popped_too_high ==> new_owner.level < new_owner.guard_level || new_owner.above_locked_range()) by {
222            if self.popped_too_high {
223                admit();
224            }
225        };
226
227        assert(new_owner.prefix.inv());
228
229        assert(new_owner.continuations[new_owner.level - 1].all_some()) by { admit() };
230
231        assert(modified_cont.all_but_index_some()) by {
232            assert(modified_cont.children[modified_cont.idx as int] is None);
233            assert forall |i: int| 0 <= i < modified_cont.idx implies
234                modified_cont.children[i] is Some by {
235                assert(modified_cont.children[i] == old_cont.children[i]);
236            };
237            assert forall |i: int| modified_cont.idx < i < NR_ENTRIES implies
238                modified_cont.children[i] is Some by {
239                assert(modified_cont.children[i] == old_cont.children[i]);
240            };
241        };
242
243        assert(forall|i: int| new_owner.level <= i < NR_LEVELS ==> {
244            (#[trigger] new_owner.continuations[i]).all_but_index_some()
245        }) by {
246            assert forall |i: int| new_owner.level <= i < NR_LEVELS implies
247                (#[trigger] new_owner.continuations[i]).all_but_index_some() by {
248                if i == self.level - 1 {
249                    assert(new_owner.continuations[i] == modified_cont);
250                } else {
251                    // i >= self.level, unchanged from old state
252                    assert(new_owner.continuations[i] == self.continuations[i]);
253                }
254            };
255        };
256
257        assert(modified_cont.inv()) by {
258            assert(modified_cont.children.len() == NR_ENTRIES) by {
259                assert(old_cont.children.len() == NR_ENTRIES);
260            };
261            assert(0 <= modified_cont.idx < NR_ENTRIES);
262            assert forall |i: int|
263                #![trigger modified_cont.children[i]]
264                0 <= i < NR_ENTRIES && modified_cont.children[i] is Some implies {
265                    &&& modified_cont.children[i].unwrap().value.path == modified_cont.path().push_tail(i as usize)
266                    &&& modified_cont.children[i].unwrap().value.parent_level == modified_cont.level()
267                    &&& modified_cont.children[i].unwrap().inv()
268                    &&& modified_cont.children[i].unwrap().level == modified_cont.tree_level + 1
269                    &&& <EntryOwner<C> as TreeNodeValue<NR_LEVELS>>::rel_children(modified_cont.entry_own, i, Some(modified_cont.children[i].unwrap().value))
270                } by {
271                assert(i != old_cont.idx as int);
272                assert(modified_cont.children[i] == old_cont.children[i]);
273            };
274            assert(modified_cont.entry_own.is_node());
275            assert(modified_cont.entry_own.inv());
276            assert(modified_cont.entry_own.node.unwrap().relate_guard_perm(modified_cont.guard_perm));
277            assert(modified_cont.tree_level == INC_LEVELS - modified_cont.level());
278            assert(modified_cont.tree_level < INC_LEVELS - 1);
279            assert(modified_cont.path().len() == modified_cont.tree_level);
280        };
281
282        assert(new_owner.level <= 4 ==> {
283            &&& new_owner.continuations.contains_key(3)
284            &&& new_owner.continuations[3].inv()
285            &&& new_owner.continuations[3].level() == 4
286            &&& new_owner.continuations[3].entry_own.parent_level == 5
287            &&& new_owner.va.index[3] == new_owner.continuations[3].idx
288        }) by {
289            if new_owner.level <= 4 {
290                if self.level == 4 {
291                    assert(new_owner.continuations[3] == modified_cont);
292                } else {
293                    assert(new_owner.continuations[3] == self.continuations[3]);
294                }
295            }
296        };
297
298        // Level 3 condition: new_level <= 3 ==> continuations[2] ...
299        assert(new_owner.level <= 3 ==> {
300            &&& new_owner.continuations.contains_key(2)
301            &&& new_owner.continuations[2].inv()
302            &&& new_owner.continuations[2].level() == 3
303            &&& new_owner.continuations[2].entry_own.parent_level == 4
304            &&& new_owner.va.index[2] == new_owner.continuations[2].idx
305            &&& new_owner.continuations[2].guard_perm.value().inner.inner@.ptr.addr() !=
306                new_owner.continuations[3].guard_perm.value().inner.inner@.ptr.addr()
307        }) by {
308            if new_owner.level <= 3 {
309                if self.level == 4 {
310                    assert(self.va.index.contains_key(2));
311                    // guard_perm distinctness: requires new guard_perm addr != old guard_perm addr
312                    assert(new_owner.continuations[2].guard_perm.value().inner.inner@.ptr.addr() !=
313                           new_owner.continuations[3].guard_perm.value().inner.inner@.ptr.addr()) by { admit() };
314                }
315            }
316        };
317
318        // Level 2 condition: new_level <= 2 ==> continuations[1] ...
319        assert(new_owner.level <= 2 ==> {
320            &&& new_owner.continuations[1].guard_perm.value().inner.inner@.ptr.addr() !=
321                new_owner.continuations[2].guard_perm.value().inner.inner@.ptr.addr()
322            &&& new_owner.continuations[1].guard_perm.value().inner.inner@.ptr.addr() !=
323                new_owner.continuations[3].guard_perm.value().inner.inner@.ptr.addr()
324        }) by {
325            if new_owner.level <= 2 {
326                if self.level == 3 {
327                    // Trigger va.inv() quantifier for index 1
328                    assert(self.va.index.contains_key(1));
329                    assert(new_owner.continuations[1].guard_perm.value().inner.inner@.ptr.addr() !=
330                           new_owner.continuations[2].guard_perm.value().inner.inner@.ptr.addr()) by { admit() };
331                    assert(new_owner.continuations[1].guard_perm.value().inner.inner@.ptr.addr() !=
332                           new_owner.continuations[3].guard_perm.value().inner.inner@.ptr.addr()) by { admit() };
333                }
334            }
335        };
336    }
337
338    pub proof fn push_level_owner_preserves_invs(self, guard_perm: GuardPerm<'rcu, C>, regions: MetaRegionOwners, guards: Guards<'rcu, C>)
339        requires
340            self.inv(),
341            self.level > 1,
342            self.only_current_locked(guards),
343            self.nodes_locked(guards),
344            self.relate_region(regions),
345            // The new guard_perm must be locked in guards
346            guards.lock_held(guard_perm.value().inner.inner@.ptr.addr()),
347        ensures
348            self.push_level_owner_spec(guard_perm).inv(),
349            self.push_level_owner_spec(guard_perm).children_not_locked(guards),
350            self.push_level_owner_spec(guard_perm).nodes_locked(guards),
351            self.push_level_owner_spec(guard_perm).relate_region(regions),
352    {
353        let new_owner = self.push_level_owner_spec(guard_perm);
354        let new_level = (self.level - 1) as u8;
355
356        let old_cont = self.continuations[self.level - 1];
357        let (child_cont, modified_cont) = old_cont.make_cont_spec(self.va.index[self.level - 2] as usize, guard_perm);
358        assert(forall |i: int|
359            #![trigger self.continuations[i]]
360            self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].guard_perm.addr() != guard_perm.addr()) by { admit() };
361        self.push_level_owner_preserves_inv(guard_perm);
362
363        let cur_entry = self.cur_entry_owner();
364        let cur_entry_addr = cur_entry.node.unwrap().meta_perm.addr();
365        let cur_entry_path = old_cont.path().push_tail(old_cont.idx as usize);
366
367        assert(cur_entry.relate_region(regions));
368
369        assert(new_owner.children_not_locked(guards)) by {
370            assert forall |i: int|
371                #![trigger new_owner.continuations[i]]
372                new_owner.level - 1 <= i < NR_LEVELS implies
373                new_owner.continuations[i].map_children(CursorOwner::<'rcu, C>::node_unlocked(guards)) by {
374
375                if i == self.level - 2 {
376                    assert(new_owner.continuations[i] == child_cont);
377                    admit();
378                } else if i == self.level - 1 {
379                    assert(new_owner.continuations[i] == modified_cont);
380                    assert(modified_cont.path() == old_cont.path());
381
382                    assert forall |j: int|
383                        #![trigger modified_cont.children[j]]
384                        0 <= j < modified_cont.children.len() && modified_cont.children[j] is Some implies
385                        modified_cont.children[j].unwrap().tree_predicate_map(
386                            modified_cont.path().push_tail(j as usize),
387                            CursorOwner::<'rcu, C>::node_unlocked(guards)) by {
388                        assert(j != old_cont.idx as int);
389                        assert(modified_cont.children[j] == old_cont.children[j]);
390                        let sibling_root_path = old_cont.path().push_tail(j as usize);
391                        assume(old_cont.path().inv());
392
393                        push_tail_different_indices_different_paths(old_cont.path(), j as usize, old_cont.idx);
394                        assert(sibling_root_path != cur_entry_path);
395
396                        admit();
397                    };
398                } else {
399                    assert(new_owner.continuations[i] == self.continuations[i]);
400                    admit();
401                }
402            };
403        };
404        assert(new_owner.nodes_locked(guards)) by {
405            assert forall |i: int|
406                #![trigger new_owner.continuations[i]]
407                new_owner.level - 1 <= i < NR_LEVELS implies
408                new_owner.continuations[i].node_locked(guards) by {
409
410                if i == self.level - 2 {
411                    assert(new_owner.continuations[i] == child_cont);
412                    assert(child_cont.guard_perm == guard_perm);
413                } else {
414                    assert(i >= self.level - 1);
415                    if i == self.level - 1 {
416                        assert(new_owner.continuations[i] == modified_cont);
417                        assert(modified_cont.guard_perm == old_cont.guard_perm);
418                    } else {
419                        assert(new_owner.continuations[i] == self.continuations[i]);
420                    }
421                }
422            };
423        };
424
425        assert(new_owner.relate_region(regions)) by {
426            let f = PageTableOwner::<C>::relate_region_pred(regions);
427
428            assert forall |i: int| #![auto]
429                new_owner.level - 1 <= i < NR_LEVELS implies {
430                    &&& f(new_owner.continuations[i].entry_own, new_owner.continuations[i].path())
431                    &&& new_owner.continuations[i].map_children(f)
432                } by {
433                admit();
434                if i == self.level - 2 {
435                    // child_cont:
436                    //   entry_own = old_cont.children[old_cont.idx].unwrap().value
437                    //   children = old_cont.children[old_cont.idx].unwrap().children
438                    assert(new_owner.continuations[i] == child_cont);
439
440                    // By self.relate_region, old_cont.map_children(f) holds
441                    // This means old_cont.children[old_cont.idx].unwrap().tree_predicate_map(f) holds
442                    // tree_predicate_map(f) = f(value, path) && forall children: tree_predicate_map(f)
443                    // So f(child_cont.entry_own, child_cont.path()) holds
444                    // And child_cont.map_children(f) holds (children satisfy tree_predicate_map(f))
445
446                    // The path for child_cont needs to match what tree_predicate_map used
447                    // This requires path consistency - admit for now
448                    admit();
449                } else if i == self.level - 1 {
450                    // modified_cont:
451                    //   entry_own = old_cont.entry_own (unchanged)
452                    //   children = old_cont.children.update(old_cont.idx, None)
453                    assert(new_owner.continuations[i] == modified_cont);
454                    assert(modified_cont.entry_own == old_cont.entry_own);
455                    assert(modified_cont.path() == old_cont.path());
456
457                    // f(entry_own, path) still holds since entry_own unchanged
458                    // For map_children(f): only checking Some children
459                    // Children with j != old_cont.idx are unchanged, still satisfy f
460                    // Child at old_cont.idx is now None, no need to check
461
462                    assert forall |j: int|
463                        #![trigger modified_cont.children[j]]
464                        0 <= j < modified_cont.children.len() && modified_cont.children[j] is Some implies
465                        modified_cont.children[j].unwrap().tree_predicate_map(modified_cont.path().push_tail(j as usize), f) by {
466                        assert(j != old_cont.idx as int);
467                        assert(modified_cont.children[j] == old_cont.children[j]);
468                        // old_cont.map_children(f) implies old_cont.children[j].tree_predicate_map(f)
469                    };
470                } else {
471                    // i > self.level - 1: continuation unchanged
472                    assert(new_owner.continuations[i] == self.continuations[i]);
473                    // By self.relate_region, this already satisfied the predicate
474                }
475            };
476        };
477    }
478
479    #[verifier::returns(proof)]
480    pub proof fn push_level_owner(tracked &mut self, tracked guard_perm: Tracked<GuardPerm<'rcu, C>>)
481        requires
482            old(self).inv(),
483            old(self).level > 1,
484        ensures
485            *self == old(self).push_level_owner_spec(guard_perm@),
486    {
487        assert(self.va.index.contains_key(self.level - 2));
488
489        let ghost self0 = *self;
490        let tracked mut cont = self.continuations.tracked_remove(self.level - 1);
491        let ghost cont0 = cont;
492        let tracked child = cont.make_cont(self.va.index[self.level - 2] as usize, guard_perm);
493
494        assert((child, cont) == cont0.make_cont_spec(self.va.index[self.level - 2] as usize, guard_perm@));
495
496        self.continuations.tracked_insert(self.level - 1, cont);
497        self.continuations.tracked_insert(self.level - 2, child);
498
499        assert(self.continuations == self0.continuations.insert(self.level - 1, cont).insert(self.level - 2, child));
500
501        self.popped_too_high = false;
502
503        self.level = (self.level - 1) as u8;
504    }
505
506    pub open spec fn pop_level_owner_spec(self) -> (Self, GuardPerm<'rcu, C>)
507    {
508        let child = self.continuations[self.level - 1];
509        let cont = self.continuations[self.level as int];
510        let (new_cont, guard_perm) = cont.restore_spec(child);
511        let new_continuations = self.continuations.insert(self.level as int, new_cont);
512        let new_continuations = new_continuations.remove(self.level - 1);
513        let new_level = (self.level + 1) as u8;
514        let popped_too_high = if new_level >= self.guard_level { true } else { false };
515        (Self {
516            continuations: new_continuations,
517            level: new_level,
518            popped_too_high: popped_too_high,
519            ..self
520        }, guard_perm)
521    }
522
523    pub proof fn pop_level_owner_preserves_inv(self)
524        requires
525            self.inv(),
526            self.level < NR_LEVELS,
527            self.in_locked_range(),
528        ensures
529            self.pop_level_owner_spec().0.inv(),
530    {
531        let child = self.continuations[self.level - 1];
532        assert(child.inv());
533        assert(forall |i: int| #![trigger child.children[i]]
534            0 <= i < NR_ENTRIES && child.children[i] is Some ==>
535            child.children[i].unwrap().inv());
536        let cont = self.continuations[self.level as int];
537        assert(cont.inv());
538        let (new_cont, _) = cont.restore_spec(child);
539
540        let child_node = OwnerSubtree {
541            value: child.entry_own,
542            level: child.tree_level,
543            children: child.children,
544        };
545
546        assert(new_cont.children[new_cont.idx as int].unwrap() == child_node);
547
548        assert forall |i:int|
549        #![trigger new_cont.children[i]]
550            0 <= i < NR_ENTRIES && new_cont.children[i] is Some implies
551            new_cont.children[i].unwrap().value.path == new_cont.path().push_tail(i as usize) by {
552                assume(child_node.value.path == new_cont.path().push_tail(i as usize));
553            };
554        admit();
555    }
556
557    pub proof fn pop_level_owner_preserves_invs(self, guards: Guards<'rcu, C>, regions: MetaRegionOwners)
558        requires
559            self.inv(),
560            self.level < NR_LEVELS,
561            self.in_locked_range(),
562            self.children_not_locked(guards),
563            self.nodes_locked(guards),
564            self.relate_region(regions),
565        ensures
566            self.pop_level_owner_spec().0.in_locked_range(),
567            self.pop_level_owner_spec().0.inv(),
568            self.pop_level_owner_spec().0.only_current_locked(guards),
569            self.pop_level_owner_spec().0.nodes_locked(guards),
570            self.pop_level_owner_spec().0.relate_region(regions),
571    {
572        let new_owner = self.pop_level_owner_spec().0;
573
574        self.pop_level_owner_preserves_inv();
575
576        assert(new_owner.only_current_locked(guards)) by { admit() };
577        admit();
578    }
579
580    /// Update va to a new value that shares the same indices at levels >= self.level.
581    /// This preserves invariants because:
582    /// 1. The new va satisfies va.inv()
583    /// 2. The indices at levels >= level match the continuation indices
584    /// 3. in_locked_range/above_locked_range depend on va but the preconditions ensure consistency
585    pub proof fn set_va_preserves_inv(self, new_va: AbstractVaddr)
586        requires
587            self.inv(),
588            new_va.inv(),
589            forall |i: int| #![auto] self.level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.va.index[i],
590            forall |i: int| #![auto] self.guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.prefix.index[i],
591        ensures
592            self.set_va_spec(new_va).inv(),
593    {
594        admit()
595    }
596
597    #[verifier::returns(proof)]
598    pub proof fn pop_level_owner(tracked &mut self) -> (tracked guard_perm: GuardPerm<'rcu, C>)
599        requires
600            old(self).inv(),
601            old(self).level < NR_LEVELS,
602        ensures
603            *self == old(self).pop_level_owner_spec().0,
604            guard_perm == old(self).pop_level_owner_spec().1,
605    {
606        let ghost self0 = *self;
607        let tracked mut parent = self.continuations.tracked_remove(self.level as int);
608        let tracked child = self.continuations.tracked_remove(self.level - 1);
609
610        let tracked guard_perm = parent.restore(child);
611
612        self.continuations.tracked_insert(self.level as int, parent);
613
614        assert(self.continuations == self0.continuations.insert(self.level as int, parent).remove(self.level - 1));
615
616        self.level = (self.level + 1) as u8;
617
618        if self.level >= self.guard_level {
619            self.popped_too_high = true;
620        }
621
622        guard_perm
623    }
624
625    pub open spec fn move_forward_owner_spec(self) -> Self
626        recommends
627            self.inv(),
628            self.level < NR_LEVELS,
629            self.in_locked_range(),
630        decreases NR_LEVELS - self.level when self.level <= NR_LEVELS
631    {
632        if self.index() + 1 < NR_ENTRIES {
633            self.inc_index().zero_below_level()
634        } else if self.level < NR_LEVELS {
635            self.pop_level_owner_spec().0.move_forward_owner_spec()
636        } else {
637            // Should never happen
638            Self {
639                popped_too_high: false,
640                ..self
641            }
642        }
643    }
644
645    pub proof fn move_forward_increases_va(self)
646        requires
647            self.inv(),
648            self.level <= NR_LEVELS,
649            self.in_locked_range(),
650        ensures
651            self.move_forward_owner_spec().va.to_vaddr() > self.va.to_vaddr(),
652        decreases NR_LEVELS - self.level
653    {
654        if self.index() + 1 < NR_ENTRIES {
655            self.inc_and_zero_increases_va();
656        } else if self.level < NR_LEVELS {
657            self.pop_level_owner_preserves_inv();
658            self.pop_level_owner_spec().0.move_forward_increases_va();
659        } else {
660            admit();
661        }
662    }
663
664    pub proof fn move_forward_not_popped_too_high(self)
665        requires
666            self.inv(),
667            self.level <= NR_LEVELS,
668            self.in_locked_range(),
669        ensures
670            !self.move_forward_owner_spec().popped_too_high,
671       decreases NR_LEVELS - self.level,
672    {
673        if self.index() + 1 < NR_ENTRIES {
674            self.inc_index().zero_preserves_all_but_va();
675        } else if self.level < NR_LEVELS {
676            self.pop_level_owner_preserves_inv();
677            self.pop_level_owner_spec().0.move_forward_not_popped_too_high();
678        }
679    }
680
681    pub proof fn move_forward_owner_decreases_steps(self)
682        requires
683            self.inv(),
684            self.level <= NR_LEVELS,
685        ensures
686            self.move_forward_owner_spec().max_steps() < self.max_steps()
687    { admit() }
688
689    pub proof fn move_forward_va_is_align_up(self)
690        requires
691            self.inv(),
692            self.level <= NR_LEVELS,
693            self.in_locked_range(),
694        ensures
695            self.move_forward_owner_spec().va == self.va.align_up(self.level as int),
696        decreases NR_LEVELS - self.level
697    {
698        admit()
699    }
700
701    pub proof fn move_forward_owner_preserves_mappings(self)
702    requires
703        self.inv(),
704        self.level > 1,
705    ensures
706        self.move_forward_owner_spec()@.mappings == self@.mappings,
707    { admit() }
708}
709
710}
ostd/specs/mm/page_table/cursor/cursor_steps.rs

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