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

1/// Cursor function-specific lemmas for `CursorOwner`.
2///
3/// Themes moved here from `owners.rs`:
4/// - **Theme 7**: PTE & entry modification invariant preservation
5///   (`protect_preserves_cursor_inv_metaregion`, `map_branch_none_*`)
6/// - **Theme 14**: Cursor path structure & jump utilities
7///   (`cursor_path_nesting`, `jump_above_locked_range_va_in_node`,
8///    `jump_not_in_node_level_lt_guard_minus_one`, `lemma_page_size_spec_5_eq_pow2_48`)
9use core::ops::Range;
10
11use vstd::prelude::*;
12
13use vstd::arithmetic::power2::pow2;
14use vstd_extra::{ghost_tree::*, ownership::*};
15
16use crate::specs::{
17    arch::*,
18    mm::{
19        frame::meta_region_owners::MetaRegionOwners,
20        page_table::{
21            AbstractVaddr, Mapping,
22            cursor::owners::{CursorContinuation, CursorOwner},
23            nat_align_down,
24            owners::*,
25        },
26    },
27};
28
29use crate::mm::{PagingLevel, Vaddr, page_size, page_table::*};
30
31verus! {
32
33broadcast use group_ghost_tree_lemmas;
34
35impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
36    pub proof fn protect_preserves_cursor_inv_metaregion(
37        self,
38        other: Self,
39        regions: MetaRegionOwners,
40    )
41        requires
42            self.inv(),
43            self.in_locked_range(),
44            !self.popped_too_high,
45            self.metaregion_sound(regions),
46            self.cur_entry_owner().is_frame(),
47            other.cur_entry_owner().is_frame(),
48            other.cur_entry_owner().inv(),
49            // protect preserves PA, path, parent_level
50            other.cur_entry_owner().frame().mapped_pa == self.cur_entry_owner().frame().mapped_pa,
51            other.cur_entry_owner().path == self.cur_entry_owner().path,
52            other.cur_entry_owner().parent_level == self.cur_entry_owner().parent_level,
53            // cursor level and structural fields unchanged
54            self.level == other.level,
55            self.guard_level == other.guard_level,
56            self.va == other.va,
57            self.prefix == other.prefix,
58            self.popped_too_high == other.popped_too_high,
59            // higher-level continuations unchanged
60            forall|i: int|
61                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
62                    == other.continuations[i],
63            // bottom continuation well-formed after protect
64            other.continuations[self.level - 1].inv(),
65            other.continuations[self.level - 1].all_some(),
66            other.continuations[self.level - 1].idx == self.continuations[self.level - 1].idx,
67            other.continuations[self.level - 1].entry_own.parent_level
68                == self.continuations[self.level - 1].entry_own.parent_level,
69            other.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
70                == self.continuations[self.level - 1].guard.inner.inner@.ptr.addr(),
71            other.continuations[self.level - 1].path() == self.continuations[self.level - 1].path(),
72            other.continuations.dom() =~= self.continuations.dom(),
73            forall|j: int|
74                0 <= j < NR_ENTRIES && j != self.continuations[self.level - 1].idx
75                    ==> #[trigger] other.continuations[self.level - 1].children[j]
76                    == self.continuations[self.level - 1].children[j],
77            ({
78                let new_child = other.continuations[self.level
79                    - 1].children[other.continuations[self.level - 1].idx as int]->0;
80                let new_path = other.continuations[self.level - 1].path().push_tail(
81                    other.continuations[self.level - 1].idx as int,
82                );
83                new_child.subtree_satisfies(
84                    new_path,
85                    PageTableOwner::<C>::metaregion_sound_pred(regions),
86                )
87            }),
88            other.continuations[self.level - 1].entry_own.metaregion_sound(regions),
89        ensures
90            other.inv(),
91            other.metaregion_sound(regions),
92    {
93        other.map_branch_none_inv_holds(self);
94
95        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
96        let L = self.level as int;
97        let idx = self.continuations[L - 1].idx as int;
98
99        assert forall|i: int|
100            #![trigger other.continuations[i]]
101            other.level - 1 <= i < NR_LEVELS implies other.continuations[i].map_children(f) by {
102            if i > L - 1 {
103                assert(other.continuations[i] == self.continuations[i]);
104                assert(self.continuations[i].map_children(f));
105            } else {
106                assert(i == L - 1);
107                let o_cont = other.continuations[L - 1];
108                let s_cont = self.continuations[L - 1];
109                reveal(CursorContinuation::inv_children);
110                assert forall|j: int|
111                    #![trigger o_cont.children[j]]
112                    0 <= j < o_cont.children.len()
113                        && o_cont.children[j] is Some implies o_cont.children[j].unwrap().subtree_satisfies(
114                o_cont.path().push_tail(j), f) by {
115                    if j != idx {
116                        assert(o_cont.children[j] == s_cont.children[j]);
117                        s_cont.inv_children_unroll(j);
118                    }
119                };
120            }
121        };
122
123        assert forall|i: int|
124            #![trigger other.continuations[i]]
125            other.level - 1 <= i
126                < NR_LEVELS implies other.continuations[i].entry_own.metaregion_sound(regions) by {
127            if i > L - 1 {
128                assert(other.continuations[i] == self.continuations[i]);
129                self.inv_continuation(i);
130            }
131        };
132    }
133
134    pub proof fn map_branch_none_inv_holds(self, owner0: Self)
135        requires
136            owner0.inv(),
137            // The map happens in the locked range and changes only the current
138            // continuation's slot at `idx` (a real, in-range slot). With this +
139            // "higher continuations unchanged", the root continuation's
140            // isolation clauses are preserved.
141            self.in_locked_range(),
142            !self.popped_too_high,
143            forall|j: int|
144                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx ==> (
145                #[trigger] self.continuations[self.level - 1].children[j])
146                    == owner0.continuations[owner0.level - 1].children[j],
147            self.level == owner0.level,
148            self.va == owner0.va,
149            self.guard_level == owner0.guard_level,
150            self.prefix == owner0.prefix,
151            self.popped_too_high == owner0.popped_too_high,
152            // Higher-level continuations unchanged
153            forall|i: int|
154                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
155                    == owner0.continuations[i],
156            // Bottom continuation is well-formed
157            self.continuations[self.level - 1].inv(),
158            self.continuations[self.level - 1].all_some(),
159            self.continuations[self.level - 1].idx == owner0.continuations[owner0.level - 1].idx,
160            self.continuations[self.level - 1].entry_own.parent_level
161                == owner0.continuations[owner0.level - 1].entry_own.parent_level,
162            // Guard address preserved (from parent_perms_preserved).
163            self.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
164                == owner0.continuations[owner0.level - 1].guard.inner.inner@.ptr.addr(),
165            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
166                - 1].path(),
167            self.va.index[self.level - 1] == self.continuations[self.level - 1].idx,
168            // Domain preserved: same keys as owner0.
169            self.continuations.dom() =~= owner0.continuations.dom(),
170        ensures
171            self.inv(),
172    {
173        let L = self.level as int;
174        assert(self.continuations[L - 1].level() == self.level);
175        assert(self.continuations.contains_key(L - 1));
176        // Isolation clauses for the root continuation (NR_LEVELS-1).
177        if self.level < NR_LEVELS {
178            // Root is above the current level ⟹ unchanged (higher-unchanged), so
179            // both clauses carry verbatim from `owner0.inv()`.
180            assert(self.continuations[NR_LEVELS - 1] == owner0.continuations[NR_LEVELS - 1]);
181        } else {
182            // Root IS the current continuation. The idx clause is vacuous
183            // (level == NR_LEVELS). For the outside-(borrowed||absent) clause:
184            // the map changed only the in-range slot `idx`, so every outside
185            // child keeps `owner0`'s value; `idx` is in-range (top index in
186            // [start, end), and `in_locked_range` rules out the sentinel).
187            owner0.in_locked_range_top_index_lt_top_end();
188            assert(self.continuations[NR_LEVELS - 1].idx == self.va.index[NR_LEVELS - 1]);
189            assert(self.continuations[NR_LEVELS - 1].idx == owner0.continuations[owner0.level
190                - 1].idx);
191            assert(C::TOP_LEVEL_INDEX_RANGE().start <= owner0.continuations[owner0.level - 1].idx
192                < C::TOP_LEVEL_INDEX_RANGE().end);
193            assert(forall|j: int|
194                0 <= j < NR_ENTRIES && !(C::TOP_LEVEL_INDEX_RANGE().start <= j
195                    < C::TOP_LEVEL_INDEX_RANGE().end) ==> (#[trigger] self.continuations[NR_LEVELS
196                    - 1].children[j]) is Some ==> (self.continuations[NR_LEVELS
197                    - 1].children[j].unwrap().value().is_borrowed() || self.continuations[NR_LEVELS
198                    - 1].children[j].unwrap().value().is_absent()));
199        }
200    }
201
202    /// After alloc_if_none (absent->node), `view_mappings` is unchanged (both contribute zero mappings).
203    pub proof fn map_branch_none_no_new_mappings(self, owner0: Self)
204        requires
205            owner0.inv(),
206            owner0.in_locked_range(),
207            self.inv(),
208            self.in_locked_range(),
209            self.level == owner0.level,
210            self.va == owner0.va,
211            forall|i: int|
212                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
213                    == owner0.continuations[i],
214            // child at idx changed from absent to empty node
215            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
216                - 1].idx as int] is Some,
217            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
218                - 1].idx as int]->0.value().is_absent(),
219            self.continuations[self.level - 1].children[self.continuations[self.level
220                - 1].idx as int] is Some,
221            self.continuations[self.level - 1].children[self.continuations[self.level
222                - 1].idx as int]->0.value().is_node(),
223            // Non-idx children and path preserved
224            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
225                - 1].path(),
226            forall|j: int|
227                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx as int
228                    ==> #[trigger] self.continuations[self.level - 1].children[j]
229                    == owner0.continuations[owner0.level - 1].children[j],
230            // The new node's subtree has empty view_rec (from alloc_if_none postcondition)
231            PageTableOwner(
232                self.continuations[self.level - 1].children[self.continuations[self.level
233                    - 1].idx as int]->0,
234            ).view_rec(
235                self.continuations[self.level - 1].path().push_tail(
236                    self.continuations[self.level - 1].idx as int,
237                ),
238            ) =~= Set::<Mapping>::empty(),
239        ensures
240            self.view_mappings() == owner0.view_mappings(),
241    {
242        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
243
244        let L = self.level as int;
245        let cont = self.continuations[L - 1];
246        let cont0 = owner0.continuations[L - 1];
247        let idx = cont0.idx as int;
248
249        assert(cont.view_mappings() == cont0.view_mappings()) by {
250            cont0.inv_children_unroll(idx);
251            PageTableOwner(cont0.children[idx].unwrap()).view_rec_absent_empty(
252                cont0.path().push_tail(idx as int),
253            );
254            assert forall|m: Mapping|
255                cont.view_mappings().contains(m) implies cont0.view_mappings().contains(m) by {
256                let j = choose|j: int|
257                    0 <= j < cont.children.len() && #[trigger] cont.children[j] is Some
258                        && PageTableOwner(cont.children[j].unwrap()).view_rec(
259                        cont.path().push_tail(j),
260                    ).contains(m);
261                if j == idx {
262                    // cont.children[idx]'s view_rec == empty (from precondition)
263                    assert(false);
264                } else {
265                    assert(cont.children[j] == cont0.children[j]);
266                }
267            };
268            assert forall|m: Mapping|
269                cont0.view_mappings().contains(m) implies cont.view_mappings().contains(m) by {
270                let j = choose|j: int|
271                    0 <= j < cont0.children.len() && #[trigger] cont0.children[j] is Some
272                        && PageTableOwner(cont0.children[j].unwrap()).view_rec(
273                        cont0.path().push_tail(j),
274                    ).contains(m);
275                if j == idx {
276                    // cont0.children[idx] is absent, view_rec is empty
277                    assert(false);
278                } else {
279                    assert(cont0.children[j] == cont.children[j]);
280                }
281            };
282        };
283        // Lift cont == cont0 to self.view_mappings() == owner0.view_mappings()
284        assert(self.view_mappings() == owner0.view_mappings()) by {
285            assert forall|m: Mapping|
286                self.view_mappings().contains(m) implies owner0.view_mappings().contains(m) by {
287                let i = choose|i: int|
288                    self.level - 1 <= i < NR_LEVELS
289                        && #[trigger] self.continuations[i].view_mappings().contains(m);
290                if i == L - 1 {
291                    assert(cont0.view_mappings().contains(m));
292                } else {
293                    assert(owner0.continuations[i] == self.continuations[i]);
294                }
295            };
296            assert forall|m: Mapping|
297                owner0.view_mappings().contains(m) implies self.view_mappings().contains(m) by {
298                let i = choose|i: int|
299                    owner0.level - 1 <= i < NR_LEVELS
300                        && #[trigger] owner0.continuations[i].view_mappings().contains(m);
301                if i == L - 1 {
302                    assert(cont.view_mappings().contains(m));
303                } else {
304                    assert(self.continuations[i] == owner0.continuations[i]);
305                }
306            };
307        };
308    }
309
310    /// After `map_branch_none` (alloc_if_none + push_level), the current entry is absent.
311    ///
312    /// Proof: `alloc_if_none` creates an empty PT node where all children are absent
313    /// (`allocated_empty_node_owner` line 172). `push_level` enters one of these children,
314    /// so `cur_entry_owner().is_absent()` holds.
315    pub proof fn map_branch_none_cur_entry_absent(self)
316        requires
317            self.inv(),
318            // All children of the current continuation are absent (from the empty node)
319            forall|i: int|
320                0 <= i < NR_ENTRIES ==> #[trigger] self.continuations[self.level
321                    - 1].children[i] is Some && self.continuations[self.level
322                    - 1].children[i]->0.value().is_absent(),
323        ensures
324            self.cur_entry_owner().is_absent(),
325    {
326    }
327
328    pub proof fn cursor_path_nesting(self, i: int, j: int)
329        requires
330            self.inv(),
331            self.level - 1 <= j < i,
332            i < NR_LEVELS,
333        ensures
334            self.continuations[j].path().len() as int > self.continuations[i].path().len(),
335            self.continuations[j].path()[self.continuations[i].path().len() as int]
336                == self.continuations[i].idx,
337    {
338        if i == 3 && j == 2 {
339        } else if i == 3 && j == 1 {
340            let p3 = self.continuations[3].path();
341            let p2 = self.continuations[2].path();
342            let idx3 = self.continuations[3].idx as int;
343            let idx2 = self.continuations[2].idx as int;
344            assert(p3.len() < p2.len());
345            assert(self.continuations[1].path() == p2.push_tail(idx2));
346            assert(p2.push_tail(idx2)[p3.len() as int] == p2[p3.len() as int]);
347        } else if i == 3 && j == 0 {
348            let p3 = self.continuations[3].path();
349            let p2 = self.continuations[2].path();
350            let p1 = self.continuations[1].path();
351            let idx3 = self.continuations[3].idx as int;
352            let idx2 = self.continuations[2].idx as int;
353            let idx1 = self.continuations[1].idx as int;
354            assert(p3.len() < p2.len());
355            assert(p3.len() < p1.len());
356            assert(p1.push_tail(idx1)[p3.len() as int] == p1[p3.len() as int]);
357            assert(p2.push_tail(idx2)[p3.len() as int] == p2[p3.len() as int]);
358        } else if i == 2 && j == 1 {
359        } else if i == 2 && j == 0 {
360            let p2 = self.continuations[2].path();
361            let p1 = self.continuations[1].path();
362            let idx2 = self.continuations[2].idx as int;
363            let idx1 = self.continuations[1].idx as int;
364            assert(p2.len() < p1.len());
365            assert(self.continuations[0].path() == p1.push_tail(idx1));
366            assert(p1.push_tail(idx1)[p2.len() as int] == p1[p2.len() as int]);
367            assert(p1 == p2.push_tail(idx2));
368            assert(p2.push_tail(idx2)[p2.len() as int] == idx2);
369        } else if i == 1 && j == 0 {
370        }
371    }
372
373    pub proof fn lemma_page_size_spec_5_eq_pow2_48()
374        ensures
375            page_size(5) == pow2(48nat) as usize,
376    {
377        crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
378        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
379        vstd::arithmetic::power2::lemma2_to64();
380        vstd::arithmetic::power2::lemma2_to64_rest();
381        vstd::arithmetic::power2::lemma_pow2_adds(12nat, 36nat);
382    }
383
384    pub proof fn jump_not_in_node_level_lt_guard_minus_one(
385        self,
386        level: PagingLevel,
387        va: Vaddr,
388        node_start: Vaddr,
389    )
390        requires
391            self.inv(),
392            self.locked_range().start <= va < self.locked_range().end,
393            1 <= level,
394            level + 1 <= self.guard_level,
395            self.locked_range().start <= node_start,
396            node_start + page_size((level + 1) as PagingLevel) <= self.locked_range().end,
397            !(node_start <= va && va < node_start + page_size((level + 1) as PagingLevel)),
398        ensures
399            level + 1 < self.guard_level,
400    {
401        if level + 1 == self.guard_level {
402            let pv = self.prefix.to_vaddr() as nat;
403            let ps = page_size(self.guard_level as PagingLevel) as nat;
404            self.prefix.align_down_concrete(self.guard_level as int);
405            self.prefix_aligned_to_guard_level();
406            self.prefix_plus_ps_no_overflow();
407            self.prefix.aligned_align_up_advances(self.guard_level as int);
408            AbstractVaddr::from_vaddr_to_vaddr_roundtrip(nat_align_down(pv, ps) as Vaddr);
409        }
410    }
411}
412
413} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_lemmas.rs

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