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            Mapping,
11            cursor::owners::{CursorContinuation, CursorOwner},
12            lemma_pte_index_bound, nat_align_down,
13            owners::*,
14            pte_index_spec,
15        },
16    },
17};
18
19use crate::mm::{PagingConstsTrait, PagingLevel, Vaddr, page_size, page_table::*};
20use core::ops::Range;
21
22verus! {
23
24broadcast use group_ghost_tree_lemmas;
25
26impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
27    pub proof fn protect_preserves_cursor_inv_metaregion(
28        self,
29        other: Self,
30        regions: MetaRegionOwners,
31    )
32        requires
33            self.inv(),
34            self.in_locked_range(),
35            !self.popped_too_high,
36            self.metaregion_sound(regions),
37            self.cur_entry_owner().is_frame(),
38            other.cur_entry_owner().is_frame(),
39            other.cur_entry_owner().inv(),
40            // protect preserves PA, path, parent_level
41            other.cur_entry_owner().frame().mapped_pa == self.cur_entry_owner().frame().mapped_pa,
42            other.cur_entry_owner().path == self.cur_entry_owner().path,
43            other.cur_entry_owner().parent_level == self.cur_entry_owner().parent_level,
44            // cursor level and structural fields unchanged
45            self.level == other.level,
46            self.guard_level == other.guard_level,
47            self.va == other.va,
48            self.prefix == other.prefix,
49            self.popped_too_high == other.popped_too_high,
50            // higher-level continuations unchanged
51            forall|i: int|
52                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
53                    == other.continuations[i],
54            // bottom continuation well-formed after protect
55            other.continuations[self.level - 1].inv(),
56            other.continuations[self.level - 1].all_some(),
57            other.continuations[self.level - 1].idx == self.continuations[self.level - 1].idx,
58            other.continuations[self.level - 1].entry_own.parent_level
59                == self.continuations[self.level - 1].entry_own.parent_level,
60            other.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
61                == self.continuations[self.level - 1].guard.inner.inner@.ptr.addr(),
62            other.continuations[self.level - 1].path() == self.continuations[self.level - 1].path(),
63            other.continuations.dom() =~= self.continuations.dom(),
64            forall|j: int|
65                0 <= j < NR_ENTRIES && j != self.continuations[self.level - 1].idx
66                    ==> #[trigger] other.continuations[self.level - 1].children[j]
67                    == self.continuations[self.level - 1].children[j],
68            ({
69                let new_child = other.continuations[self.level
70                    - 1].children[other.continuations[self.level - 1].idx as int]->0;
71                let new_path = other.continuations[self.level - 1].path().push_tail(
72                    other.continuations[self.level - 1].idx as int,
73                );
74                new_child.subtree_satisfies(
75                    new_path,
76                    PageTableOwner::<C>::metaregion_sound_pred(regions),
77                )
78            }),
79            other.continuations[self.level - 1].entry_own.metaregion_sound(regions),
80        ensures
81            other.inv(),
82            other.metaregion_sound(regions),
83    {
84        self.lemma_cur_pte_index();
85        other.map_branch_none_inv_holds(self);
86
87        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
88        let L = self.level as int;
89        let idx = self.continuations[L - 1].idx as int;
90
91        assert forall|i: int|
92            #![trigger other.continuations[i]]
93            other.level - 1 <= i < NR_LEVELS implies other.continuations[i].map_children(f) by {
94            reveal(CursorContinuation::map_children);
95            if i > L - 1 {
96                assert(other.continuations[i] == self.continuations[i]);
97                assert(self.continuations[i].map_children(f));
98            } else {
99                assert(i == L - 1);
100                let o_cont = other.continuations[L - 1];
101                let s_cont = self.continuations[L - 1];
102                reveal(CursorContinuation::inv_children);
103                assert forall|j: int|
104                    #![trigger o_cont.children[j]]
105                    0 <= j < o_cont.children.len()
106                        && o_cont.children[j] is Some implies o_cont.children[j].unwrap().subtree_satisfies(
107                o_cont.path().push_tail(j), f) by {
108                    if j != idx {
109                        assert(o_cont.children[j] == s_cont.children[j]);
110                        s_cont.lemma_inv_children_unroll(j);
111                    }
112                };
113            }
114        };
115
116        reveal(CursorOwner::path_metaregion_sound);
117        assert forall|i: int|
118            #![trigger other.continuations[i]]
119            other.level - 1 <= i
120                < NR_LEVELS implies other.continuations[i].entry_own.metaregion_sound(regions) by {
121            if i > L - 1 {
122                assert(other.continuations[i] == self.continuations[i]);
123                self.lemma_inv_continuation(i);
124            }
125        };
126    }
127
128    pub proof fn map_branch_none_inv_holds(self, owner0: Self)
129        requires
130            owner0.inv(),
131            // The map happens in the locked range and changes only the current
132            // continuation's slot at `idx` (a real, in-range slot). With this +
133            // "higher continuations unchanged", the root continuation's
134            // isolation clauses are preserved.
135            self.in_locked_range(),
136            !self.popped_too_high,
137            forall|j: int|
138                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx ==> (
139                #[trigger] self.continuations[self.level - 1].children[j])
140                    == owner0.continuations[owner0.level - 1].children[j],
141            self.level == owner0.level,
142            self.va == owner0.va,
143            self.guard_level == owner0.guard_level,
144            self.prefix == owner0.prefix,
145            self.popped_too_high == owner0.popped_too_high,
146            // Higher-level continuations unchanged
147            forall|i: int|
148                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
149                    == owner0.continuations[i],
150            // Bottom continuation is well-formed
151            self.continuations[self.level - 1].inv(),
152            self.continuations[self.level - 1].all_some(),
153            self.continuations[self.level - 1].idx == owner0.continuations[owner0.level - 1].idx,
154            self.continuations[self.level - 1].entry_own.parent_level
155                == owner0.continuations[owner0.level - 1].entry_own.parent_level,
156            // Guard address preserved (from parent_perms_preserved).
157            self.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
158                == owner0.continuations[owner0.level - 1].guard.inner.inner@.ptr.addr(),
159            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
160                - 1].path(),
161            pte_index_spec::<C>(self.cur_va(), (self.level - 1 + 1) as PagingLevel)
162                == self.continuations[self.level - 1].idx,
163            // Domain preserved: same keys as owner0.
164            self.continuations.dom() =~= owner0.continuations.dom(),
165        ensures
166            self.inv(),
167    {
168        let L = self.level as int;
169        C::lemma_paging_consts_properties();
170        lemma_pte_index_bound::<C>(self.cur_va(), self.level);
171        assert(pte_index_spec::<C>(self.va, (self.level - 1 + 1) as PagingLevel)
172            == self.continuations[self.level - 1].idx);
173        assert(self.continuations[L - 1].level() == self.level);
174        assert(self.continuations.contains_key(L - 1));
175        // Isolation clauses for the root continuation (NR_LEVELS-1).
176        if self.level < NR_LEVELS {
177            // Root is above the current level ⟹ unchanged (higher-unchanged), so
178            // both clauses carry verbatim from `owner0.inv()`.
179            assert(self.continuations[NR_LEVELS - 1] == owner0.continuations[NR_LEVELS - 1]);
180        } else {
181            // Root IS the current continuation. The idx clause is vacuous
182            // (level == NR_LEVELS). For the outside-(borrowed||absent) clause:
183            // the map changed only the in-range slot `idx`, so every outside
184            // child keeps `owner0`'s value; `idx` is in-range (top index in
185            // [start, end), and `in_locked_range` rules out the sentinel).
186            owner0.lemma_in_locked_range_top_index_lt_top_end();
187            assert(self.continuations[NR_LEVELS - 1].idx == pte_index_spec::<C>(
188                self.va,
189                (NR_LEVELS - 1 + 1) as PagingLevel,
190            ));
191            assert(self.continuations[NR_LEVELS - 1].idx == owner0.continuations[owner0.level
192                - 1].idx);
193            assert(C::TOP_LEVEL_INDEX_RANGE().start <= owner0.continuations[owner0.level - 1].idx
194                < C::TOP_LEVEL_INDEX_RANGE().end);
195            assert(forall|j: int|
196                0 <= j < NR_ENTRIES && !(C::TOP_LEVEL_INDEX_RANGE().start <= j
197                    < C::TOP_LEVEL_INDEX_RANGE().end) ==> (#[trigger] self.continuations[NR_LEVELS
198                    - 1].children[j]) is Some ==> (self.continuations[NR_LEVELS
199                    - 1].children[j].unwrap().value().is_borrowed() || self.continuations[NR_LEVELS
200                    - 1].children[j].unwrap().value().is_absent()));
201        }
202    }
203
204    /// After alloc_if_none (absent->node), `view_mappings` is unchanged (both contribute zero mappings).
205    pub proof fn map_branch_none_no_new_mappings(self, owner0: Self)
206        requires
207            owner0.inv(),
208            owner0.in_locked_range(),
209            self.inv(),
210            self.in_locked_range(),
211            self.level == owner0.level,
212            self.va == owner0.va,
213            forall|i: int|
214                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
215                    == owner0.continuations[i],
216            // child at idx changed from absent to empty node
217            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
218                - 1].idx as int] is Some,
219            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
220                - 1].idx as int]->0.value().is_absent(),
221            self.continuations[self.level - 1].children[self.continuations[self.level
222                - 1].idx as int] is Some,
223            self.continuations[self.level - 1].children[self.continuations[self.level
224                - 1].idx as int]->0.value().is_node(),
225            // Non-idx children and path preserved
226            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
227                - 1].path(),
228            forall|j: int|
229                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx as int
230                    ==> #[trigger] self.continuations[self.level - 1].children[j]
231                    == owner0.continuations[owner0.level - 1].children[j],
232            // The new node's subtree has empty view_rec (from alloc_if_none postcondition)
233            PageTableOwner(
234                self.continuations[self.level - 1].children[self.continuations[self.level
235                    - 1].idx as int]->0,
236            ).view_rec(
237                self.continuations[self.level - 1].path().push_tail(
238                    self.continuations[self.level - 1].idx as int,
239                ),
240            ) =~= Set::<Mapping>::empty(),
241        ensures
242            self.view_mappings() == owner0.view_mappings(),
243    {
244        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
245
246        let L = self.level as int;
247        let cont = self.continuations[L - 1];
248        let cont0 = owner0.continuations[L - 1];
249        let idx = cont0.idx as int;
250
251        assert(cont.view_mappings() == cont0.view_mappings()) by {
252            cont0.lemma_inv_children_unroll(idx);
253            PageTableOwner(cont0.children[idx].unwrap()).view_rec_absent_empty(
254                cont0.path().push_tail(idx as int),
255            );
256            assert forall|m: Mapping|
257                cont.view_mappings().contains(m) implies cont0.view_mappings().contains(m) by {
258                let j = choose|j: int|
259                    0 <= j < cont.children.len() && #[trigger] cont.children[j] is Some
260                        && PageTableOwner(cont.children[j].unwrap()).view_rec(
261                        cont.path().push_tail(j),
262                    ).contains(m);
263                if j == idx {
264                    // cont.children[idx]'s view_rec == empty (from precondition)
265                    assert(false);
266                } else {
267                    assert(cont.children[j] == cont0.children[j]);
268                }
269            };
270            assert forall|m: Mapping|
271                cont0.view_mappings().contains(m) implies cont.view_mappings().contains(m) by {
272                let j = choose|j: int|
273                    0 <= j < cont0.children.len() && #[trigger] cont0.children[j] is Some
274                        && PageTableOwner(cont0.children[j].unwrap()).view_rec(
275                        cont0.path().push_tail(j),
276                    ).contains(m);
277                if j == idx {
278                    // cont0.children[idx] is absent, view_rec is empty
279                    assert(false);
280                } else {
281                    assert(cont0.children[j] == cont.children[j]);
282                }
283            };
284        };
285        // Lift cont == cont0 to self.view_mappings() == owner0.view_mappings()
286        assert(self.view_mappings() == owner0.view_mappings()) by {
287            assert forall|m: Mapping|
288                self.view_mappings().contains(m) implies owner0.view_mappings().contains(m) by {
289                let i = choose|i: int|
290                    self.level - 1 <= i < NR_LEVELS
291                        && #[trigger] self.continuations[i].view_mappings().contains(m);
292                if i == L - 1 {
293                    assert(cont0.view_mappings().contains(m));
294                } else {
295                    assert(owner0.continuations[i] == self.continuations[i]);
296                }
297            };
298            assert forall|m: Mapping|
299                owner0.view_mappings().contains(m) implies self.view_mappings().contains(m) by {
300                let i = choose|i: int|
301                    owner0.level - 1 <= i < NR_LEVELS
302                        && #[trigger] owner0.continuations[i].view_mappings().contains(m);
303                if i == L - 1 {
304                    assert(cont.view_mappings().contains(m));
305                } else {
306                    assert(self.continuations[i] == owner0.continuations[i]);
307                }
308            };
309        };
310    }
311}
312
313} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_lemmas.rs

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