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

1//! Cursor function-specific lemmas for `CursorOwner`.
2use vstd::{arithmetic::power2::pow2, prelude::*};
3use vstd_extra::{ghost_tree::*, ownership::*};
4
5use crate::specs::{
6    arch::*,
7    mm::{
8        frame::meta_region_owners::MetaRegionOwners,
9        page_table::{
10            cursor::owners::{CursorContinuation, CursorOwner},
11            cursor::page_size_lemmas::lemma_page_size_next,
12            owners::*,
13            *,
14        },
15    },
16};
17
18use crate::mm::{PagingConsts, PagingConstsTrait, PagingLevel, Vaddr, page_size, page_table::*};
19use core::ops::Range;
20
21verus! {
22
23broadcast use group_ghost_tree_lemmas;
24
25impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
26    /// Restore a tree predicate after replacing only the current child subtree.
27    pub proof fn lemma_replaced_child_preserves_map_full_tree(
28        self,
29        old: Self,
30        f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
31        g: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
32    )
33        requires
34            self.inv(),
35            old.inv(),
36            self.level == old.level,
37            old.map_full_tree(f),
38            OwnerSubtree::implies(f, g),
39            forall|i: int|
40                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
41                    == old.continuations[i],
42            self.continuations[self.level - 1].path() == old.continuations[old.level - 1].path(),
43            self.index() == old.index(),
44            forall|j: int|
45                0 <= j < NR_ENTRIES && j != old.index() ==> #[trigger] self.continuations[self.level
46                    - 1].children[j] == old.continuations[old.level - 1].children[j],
47            self.cur_subtree().subtree_satisfies(self.cur_entry_owner().path, g),
48        ensures
49            self.map_full_tree(g),
50    {
51        assert forall|i: int|
52            self.level - 1 <= i < NR_LEVELS implies #[trigger] self.continuations[i].map_children(
53            g,
54        ) by {
55            if i == self.level - 1 {
56                self.continuations[i].lemma_map_children_lift_skip_idx(
57                    old.continuations[i],
58                    self.index() as int,
59                    f,
60                    g,
61                );
62            } else {
63                old.continuations[i].map_children_lift(f, g);
64            }
65        };
66    }
67
68    /// Replace the huge current mapping with the proven view of its split subtree.
69    pub proof fn lemma_split_current_mappings(self, old: Self)
70        requires
71            self.inv(),
72            old.inv(),
73            self.in_barrier_va(),
74            old.in_barrier_va(),
75            self.level == old.level,
76            self.va == old.va,
77            old.cur_entry_owner().is_frame(),
78            self.cur_entry_owner().is_node(),
79            self.index() == old.index(),
80            self.continuations[self.level - 1].path() == old.continuations[old.level - 1].path(),
81            forall|i: int|
82                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
83                    == old.continuations[i],
84            forall|j: int|
85                0 <= j < NR_ENTRIES && j != old.index() ==> #[trigger] self.continuations[self.level
86                    - 1].children[j] == old.continuations[old.level - 1].children[j],
87            1 < old.level < NR_LEVELS,
88            PageTableOwner(self.cur_subtree()).view_rec(self.cur_entry_owner().path) == Set::<
89                int,
90            >::range(0, NR_ENTRIES as int).map(
91                |i: int|
92                    CursorView::<C>::split_index(
93                        PageTableOwner(old.cur_subtree()).view_rec(
94                            old.cur_entry_owner().path,
95                        ).choose(),
96                        page_size::<PagingConsts>((old.level - 1) as PagingLevel),
97                        i as usize,
98                    ),
99            ),
100        ensures
101            self@ == old@.split_if_mapped_huge_spec(
102                page_size::<PagingConsts>((old.level - 1) as PagingLevel),
103            ),
104            old@.inv(),
105            old@.present(),
106            old@.query_mapping().page_size == page_size::<PagingConsts>(old.level),
107    {
108        hide(CursorContinuation::inv_children_rel);
109        hide(CursorContinuation::inv_children);
110        hide(CursorContinuation::pt_inv_children);
111        hide(CursorOwner::view_mappings);
112        hide(CursorContinuation::view_mappings);
113        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
114
115        old.lemma_inv_continuation(old.level - 1);
116        let old_cont = old.continuations[old.level - 1];
117        old_cont.lemma_inv_children_unroll(old_cont.idx as int);
118        old_cont.lemma_inv_children_rel_unroll(old_cont.idx as int);
119        old_cont.lemma_pt_inv_children_unroll(old_cont.idx as int);
120        self.lemma_cur_subtree_inv();
121        old.view_preserves_inv();
122        old.lemma_cur_subtree_inv();
123        old.cur_va_in_subtree_range();
124        old.lemma_cur_entry_frame_present();
125        let old_subtree = old.cur_subtree();
126        let path = old.cur_entry_owner().path;
127        let m = old@.query_mapping();
128        old.query_mapping_from_subtree(m);
129        assert(PageTableOwner(old_subtree).view_rec(path) == set![m]);
130        vstd::set::lemma_set_choose_len(set![m]);
131        let size = page_size::<PagingConsts>((old.level - 1) as PagingLevel);
132        lemma_page_size_next::<PagingConsts>((old.level - 1) as PagingLevel);
133        crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
134        assert(m.page_size / size == NR_ENTRIES) by (nonlinear_arith)
135            requires
136                size > 0,
137                m.page_size == size * NR_ENTRIES,
138        ;
139        let cont0 = old.continuations[old.level - 1];
140        let cont1 = self.continuations[self.level - 1];
141        cont1.lemma_inv_children_rel_unroll(cont1.idx as int);
142        cont0.view_mappings_take_child();
143        cont1.view_mappings_take_child();
144        cont0.take_child_preserves_inv();
145        cont1.take_child_preserves_inv();
146        let siblings0 = cont0.take_child().1;
147        let siblings1 = cont1.take_child().1;
148        assert(siblings0.view_mappings() == siblings1.view_mappings()) by {
149            assert forall|j: int| 0 <= j < NR_ENTRIES implies (#[trigger] siblings0.children[j])
150                == siblings1.children[j] by {};
151            assert forall|e: Mapping|
152                siblings0.view_mappings().contains(e) implies siblings1.view_mappings().contains(
153                e,
154            ) by {
155                let j = choose|j: int|
156                    0 <= j < NR_ENTRIES && (#[trigger] siblings0.children[j]) is Some
157                        && PageTableOwner(siblings0.children[j]->0).view_rec(
158                        siblings0.path().push_tail(j),
159                    ).contains(e);
160                siblings1.lemma_view_mappings_intro(e, j);
161            };
162            assert forall|e: Mapping|
163                siblings1.view_mappings().contains(e) implies siblings0.view_mappings().contains(
164                e,
165            ) by {
166                let j = choose|j: int|
167                    0 <= j < NR_ENTRIES && (#[trigger] siblings1.children[j]) is Some
168                        && PageTableOwner(siblings1.children[j]->0).view_rec(
169                        siblings1.path().push_tail(j),
170                    ).contains(e);
171                siblings0.lemma_view_mappings_intro(e, j);
172            };
173        };
174        let new_subtree = self.cur_subtree();
175        siblings1.view_mappings_put_child(new_subtree);
176        assert(siblings1.put_child(new_subtree).view_mappings() == cont1.view_mappings());
177        Self::view_mappings_replace_lowest(old, self, cont0, cont1);
178        assert(cont0.view_mappings().subset_of(old.view_mappings())) by {
179            assert forall|e: Mapping|
180                cont0.view_mappings().contains(e) implies old.view_mappings().contains(e) by {
181                old.lemma_view_mappings_intro(e, old.level - 1);
182            };
183        };
184        assert(self.view_mappings() =~= old.view_mappings() - set![m] + PageTableOwner(
185            new_subtree,
186        ).view_rec(self.cur_entry_owner().path));
187    }
188
189    /// Restoring a changed child and parent PTE preserves cursor and metadata invariants.
190    pub proof fn lemma_replace_preserves_cursor_inv_metaregion(
191        self,
192        other: Self,
193        regions: MetaRegionOwners,
194    )
195        requires
196            self.inv(),
197            self.in_barrier_va(),
198            !self.popped_too_high,
199            self.metaregion_sound(regions),
200            // cursor level and structural fields unchanged
201            self.level == other.level,
202            self.guard_level == other.guard_level,
203            self.va == other.va,
204            self.barrier_va == other.barrier_va,
205            self.prefix == other.prefix,
206            self.popped_too_high == other.popped_too_high,
207            // higher-level continuations unchanged
208            forall|i: int|
209                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
210                    == other.continuations[i],
211            // bottom continuation well-formed after protect
212            other.continuations[self.level - 1].inv(),
213            other.continuations[self.level - 1].all_some(),
214            other.continuations[self.level - 1].idx == self.continuations[self.level - 1].idx,
215            other.continuations[self.level - 1].entry_own.parent_level
216                == self.continuations[self.level - 1].entry_own.parent_level,
217            other.continuations[self.level - 1].guard.inner.inner@.slot_vaddr()
218                == self.continuations[self.level - 1].guard.inner.inner@.slot_vaddr(),
219            other.continuations[self.level - 1].path() == self.continuations[self.level - 1].path(),
220            other.continuations.dom() =~= self.continuations.dom(),
221            forall|j: int|
222                0 <= j < NR_ENTRIES && j != self.continuations[self.level - 1].idx
223                    ==> #[trigger] other.continuations[self.level - 1].children[j]
224                    == self.continuations[self.level - 1].children[j],
225            ({
226                let new_child = other.continuations[self.level
227                    - 1].children[other.continuations[self.level - 1].idx as int]->0;
228                let new_path = other.continuations[self.level - 1].path().push_tail(
229                    other.continuations[self.level - 1].idx as int,
230                );
231                new_child.subtree_satisfies(
232                    new_path,
233                    PageTableOwner::<C>::metaregion_sound_pred(regions),
234                )
235            }),
236            other.continuations[self.level - 1].entry_own.metaregion_sound(regions),
237        ensures
238            other.inv(),
239            other.metaregion_sound(regions),
240    {
241        self.lemma_cur_pte_index();
242        other.lemma_map_branch_none_inv_holds(self);
243
244        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
245        let L = self.level as int;
246        let idx = self.continuations[L - 1].idx as int;
247
248        assert forall|i: int|
249            #![trigger other.continuations[i]]
250            other.level - 1 <= i < NR_LEVELS implies other.continuations[i].map_children(f) by {
251            reveal(CursorContinuation::map_children);
252            if i > L - 1 {
253                assert(other.continuations[i] == self.continuations[i]);
254                assert(self.continuations[i].map_children(f));
255            } else {
256                assert(i == L - 1);
257                let o_cont = other.continuations[L - 1];
258                let s_cont = self.continuations[L - 1];
259                reveal(CursorContinuation::inv_children);
260                assert forall|j: int|
261                    #![trigger o_cont.children[j]]
262                    0 <= j < o_cont.children.len()
263                        && o_cont.children[j] is Some implies o_cont.children[j].unwrap().subtree_satisfies(
264                o_cont.path().push_tail(j), f) by {
265                    if j != idx {
266                        assert(o_cont.children[j] == s_cont.children[j]);
267                        s_cont.lemma_inv_children_unroll(j);
268                    }
269                };
270            }
271        };
272
273        reveal(CursorOwner::path_metaregion_sound);
274        assert forall|i: int|
275            #![trigger other.continuations[i]]
276            other.level - 1 <= i
277                < NR_LEVELS implies other.continuations[i].entry_own.metaregion_sound(regions) by {
278            if i > L - 1 {
279                assert(other.continuations[i] == self.continuations[i]);
280                self.lemma_inv_continuation(i);
281            }
282        };
283    }
284
285    pub proof fn lemma_map_branch_none_inv_holds(self, owner0: Self)
286        requires
287            owner0.inv(),
288            // The map happens in the locked range and changes only the current
289            // continuation's slot at `idx` (a real, in-range slot). With this +
290            // "higher continuations unchanged", the root continuation's
291            // isolation clauses are preserved.
292            self.in_barrier_va(),
293            !self.popped_too_high,
294            forall|j: int|
295                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx ==> (
296                #[trigger] self.continuations[self.level - 1].children[j])
297                    == owner0.continuations[owner0.level - 1].children[j],
298            self.level == owner0.level,
299            self.va == owner0.va,
300            self.barrier_va == owner0.barrier_va,
301            self.guard_level == owner0.guard_level,
302            self.prefix == owner0.prefix,
303            self.popped_too_high == owner0.popped_too_high,
304            // Higher-level continuations unchanged
305            forall|i: int|
306                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
307                    == owner0.continuations[i],
308            // Bottom continuation is well-formed
309            self.continuations[self.level - 1].inv(),
310            self.continuations[self.level - 1].all_some(),
311            self.continuations[self.level - 1].idx == owner0.continuations[owner0.level - 1].idx,
312            self.continuations[self.level - 1].entry_own.parent_level
313                == owner0.continuations[owner0.level - 1].entry_own.parent_level,
314            // Guard address preserved (from parent_perms_preserved).
315            self.continuations[self.level - 1].guard.inner.inner@.slot_vaddr()
316                == owner0.continuations[owner0.level - 1].guard.inner.inner@.slot_vaddr(),
317            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
318                - 1].path(),
319            pte_index_spec::<C>(self.cur_va(), self.level as PagingLevel)
320                == self.continuations[self.level - 1].idx,
321            // Domain preserved: same keys as owner0.
322            self.continuations.dom() =~= owner0.continuations.dom(),
323        ensures
324            self.inv(),
325    {
326        let L = self.level as int;
327        C::lemma_paging_consts_properties();
328        C::axiom_current_paging_consts_hardcoded();
329        lemma_pte_index_bound::<C>(self.cur_va(), self.level);
330        assert(pte_index_spec::<C>(self.va, self.level as PagingLevel)
331            == self.continuations[self.level - 1].idx);
332        assert(self.continuations[L - 1].level() == self.level);
333        assert(self.continuations.contains_key(L - 1));
334        // Isolation clauses for the root continuation (NR_LEVELS-1).
335        if self.level < NR_LEVELS {
336            // Root is above the current level ⟹ unchanged (higher-unchanged), so
337            // both clauses carry verbatim from `owner0.inv()`.
338            assert(self.continuations[NR_LEVELS - 1] == owner0.continuations[NR_LEVELS - 1]);
339        } else {
340            // Root IS the current continuation. The idx clause is vacuous
341            // (level == NR_LEVELS). For the outside-(borrowed||absent) clause:
342            // the map changed only the in-range slot `idx`, so every outside
343            // child keeps `owner0`'s value; `idx` is in-range (top index in
344            // [start, end), and `in_barrier_va` rules out the sentinel).
345            owner0.lemma_in_barrier_va_top_index_bounds();
346            assert(self.continuations[NR_LEVELS - 1].idx == pte_index_spec::<C>(
347                self.va,
348                NR_LEVELS as PagingLevel,
349            ));
350            assert(self.continuations[NR_LEVELS - 1].idx == owner0.continuations[owner0.level
351                - 1].idx);
352            assert(C::TOP_LEVEL_INDEX_RANGE().start <= owner0.continuations[owner0.level - 1].idx
353                < C::TOP_LEVEL_INDEX_RANGE().end);
354            assert(forall|j: int|
355                0 <= j < NR_ENTRIES && !(C::TOP_LEVEL_INDEX_RANGE().start <= j
356                    < C::TOP_LEVEL_INDEX_RANGE().end) ==> (#[trigger] self.continuations[NR_LEVELS
357                    - 1].children[j]) is Some ==> (self.continuations[NR_LEVELS
358                    - 1].children[j].unwrap().value().is_borrowed() || self.continuations[NR_LEVELS
359                    - 1].children[j].unwrap().value().is_absent()));
360        }
361    }
362
363    /// After alloc_if_none (absent->node), `view_mappings` is unchanged (both contribute zero mappings).
364    pub proof fn map_branch_none_no_new_mappings(self, owner0: Self)
365        requires
366            owner0.inv(),
367            owner0.in_barrier_va(),
368            self.inv(),
369            self.in_barrier_va(),
370            self.level == owner0.level,
371            self.va == owner0.va,
372            forall|i: int|
373                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
374                    == owner0.continuations[i],
375            // child at idx changed from absent to empty node
376            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
377                - 1].idx as int] is Some,
378            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
379                - 1].idx as int]->0.value().is_absent(),
380            self.continuations[self.level - 1].children[self.continuations[self.level
381                - 1].idx as int] is Some,
382            self.continuations[self.level - 1].children[self.continuations[self.level
383                - 1].idx as int]->0.value().is_node(),
384            // Non-idx children and path preserved
385            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
386                - 1].path(),
387            forall|j: int|
388                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx as int
389                    ==> #[trigger] self.continuations[self.level - 1].children[j]
390                    == owner0.continuations[owner0.level - 1].children[j],
391            // The new node's subtree has empty view_rec (from alloc_if_none postcondition)
392            PageTableOwner(
393                self.continuations[self.level - 1].children[self.continuations[self.level
394                    - 1].idx as int]->0,
395            ).view_rec(
396                self.continuations[self.level - 1].path().push_tail(
397                    self.continuations[self.level - 1].idx as int,
398                ),
399            ) =~= Set::<Mapping>::empty(),
400        ensures
401            self.view_mappings() == owner0.view_mappings(),
402    {
403        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
404
405        let L = self.level as int;
406        let cont = self.continuations[L - 1];
407        let cont0 = owner0.continuations[L - 1];
408        let idx = cont0.idx as int;
409
410        assert(cont.view_mappings() == cont0.view_mappings()) by {
411            cont0.lemma_inv_children_unroll(idx);
412            PageTableOwner(cont0.children[idx].unwrap()).lemma_view_rec_absent_empty(
413                cont0.path().push_tail(idx as int),
414            );
415            assert forall|m: Mapping|
416                cont.view_mappings().contains(m) implies cont0.view_mappings().contains(m) by {
417                let j = choose|j: int|
418                    0 <= j < cont.children.len() && #[trigger] cont.children[j] is Some
419                        && PageTableOwner(cont.children[j].unwrap()).view_rec(
420                        cont.path().push_tail(j),
421                    ).contains(m);
422                if j == idx {
423                    // cont.children[idx]'s view_rec == empty (from precondition)
424                    assert(false);
425                } else {
426                    assert(cont.children[j] == cont0.children[j]);
427                }
428            };
429            assert forall|m: Mapping|
430                cont0.view_mappings().contains(m) implies cont.view_mappings().contains(m) by {
431                let j = choose|j: int|
432                    0 <= j < cont0.children.len() && #[trigger] cont0.children[j] is Some
433                        && PageTableOwner(cont0.children[j].unwrap()).view_rec(
434                        cont0.path().push_tail(j),
435                    ).contains(m);
436                if j == idx {
437                    // cont0.children[idx] is absent, view_rec is empty
438                    assert(false);
439                } else {
440                    assert(cont0.children[j] == cont.children[j]);
441                }
442            };
443        };
444        // Lift cont == cont0 to self.view_mappings() == owner0.view_mappings()
445        assert(self.view_mappings() == owner0.view_mappings()) by {
446            assert forall|m: Mapping|
447                self.view_mappings().contains(m) implies owner0.view_mappings().contains(m) by {
448                let i = choose|i: int|
449                    self.level - 1 <= i < NR_LEVELS
450                        && #[trigger] self.continuations[i].view_mappings().contains(m);
451                if i == L - 1 {
452                    assert(cont0.view_mappings().contains(m));
453                } else {
454                    assert(owner0.continuations[i] == self.continuations[i]);
455                }
456            };
457            assert forall|m: Mapping|
458                owner0.view_mappings().contains(m) implies self.view_mappings().contains(m) by {
459                let i = choose|i: int|
460                    owner0.level - 1 <= i < NR_LEVELS
461                        && #[trigger] owner0.continuations[i].view_mappings().contains(m);
462                if i == L - 1 {
463                    assert(cont.view_mappings().contains(m));
464                } else {
465                    assert(self.continuations[i] == owner0.continuations[i]);
466                }
467            };
468        };
469    }
470}
471
472} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_lemmas.rs

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